ReScript→AffineScript migration: finish the compiler/src port (modules 7–17)

PROOF-NEEDS.md

@@ -4,11 +4,91 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # PROOF-NEEDS.md
 
-## Template ABI Cleanup (2026-03-29)
+> Engineering ledger for the error-lang **formal core**. This is the honest
+> substrate beneath the language's deliberately tongue-in-cheek "100%
+> production-ready, formally verified" self-presentation: it records what is
+> *actually* machine-checked, what is not, and how to reproduce the checks.
+> The language may dissemble about itself on purpose — this file does not.
 
-Template ABI removed -- was creating false impression of formal verification.
-The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
-scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
+## Formal core (`src/abi/`)
 
-When this project needs formal ABI verification, create domain-specific Idris2 proofs
-following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.
+Three properties of the computational-haptics engine are proved in Idris2 and
+**machine-checked under Idris 2, version 0.8.0**, with **no escape hatches**
+(no `believe_me`, `assert_total`, `cast`-coerced equality, or `postulate`):
+
+| Property | Module | Status |
+|---|---|---|
+| Stability score ∈ [0, 100] | `src/abi/Stability.idr` | ✅ proved (`stabilityUpperBound`, `stabilityLowerBound`) |
+| Positional-operator determinism | `src/abi/Positional.idr` | ✅ proved (`positionalDeterministic`) + sanity evaluations |
+| Paradox-factor monotonicity | `src/abi/Paradox.idr` | ⚠️ partial — two factors proved, blanket claim retracted (below) |
+
+`src/abi/Foreign.idr` is an honest, self-contained ABI **binding-declaration**
+layer (it asserts no theorems). All four modules are listed in
+`src/abi/error-lang-abi.ipkg`.
+
+### Reproduce
+
+```sh
+# idris2 is not in apt here, and the ziglang/deno mirrors are blocked by the
+# environment network policy, so build the proof checker from source via Chez:
+sudo apt-get install -y chezscheme libgmp-dev make gcc
+git clone https://github.com/idris-lang/Idris2 && cd Idris2
+make bootstrap SCHEME=chezscheme && make install
+export PATH="$HOME/.idris2/bin:$PATH"
+
+# then, from the error-lang repo root:
+./verification/check-proofs.sh
+# or:  cd src/abi && idris2 --typecheck error-lang-abi.ipkg
+```
+
+### The monotonicity retraction (an honest finding)
+
+The previously-advertised property *"paradox detection is monotonic with
+complexity"* is **false of the implementation** — and attempting to prove it
+honestly is what surfaced that. `error_lang_detect_paradoxes`
+(`ffi/zig/src/main.zig`) gates `scope_leakage` on `isPrime(line_count)`, which
+is not monotone: line **7** is prime → active, line **8** is composite →
+inactive, even though 8 > 7.
+
+`src/abi/Paradox.idr` therefore proves the part that *is* true — the two
+threshold-gated factors are monotone in their driving metric
+(`superpositionMonotone` for `var_count > 10`; `temporalMonotone` for
+`depth > 5`) — and retracts the blanket claim, recording the scope-leakage
+obstruction explicitly. Non-monotone scope leakage is intentional; it is the
+pedagogical point of the paradox. The difference now is that the proof says so
+out loud, instead of hiding it behind `cast Refl`.
+
+## What was removed (2026-06-23)
+
+`src/abi/Foreign.idr` previously carried three "Safety Proofs" —
+`stabilityBounded`, `positionalDeterministic`, `paradoxMonotonic` — that were
+**not proofs**. Each manufactured its evidence with `cast ()` / `cast Refl`
+over an `IO` action (e.g. calling an FFI function twice and coercing
+`Refl : x = x` onto the two distinct results, with a comment that it "should
+hold in practice"). An earlier note in this file claimed these files had been
+removed; in fact `Foreign.idr` was still present and still exported the fakes.
+
+They are now deleted and replaced by the genuine, machine-checked modules above.
+
+## Open obligations
+
+1. **CI gate.** Add an Idris2 `--typecheck error-lang-abi.ipkg` job so the core
+   is checked on every push. (The dev image has no idris2 by default; it was
+   built from source for this change.)
+2. **Implementation conformance.** The proofs are stated over abstract models
+   that mirror `ffi/zig/src/main.zig` and `compiler/src/Types.res`. Two of those
+   implementations **disagree**: positional behaviour is `column % 2` (two-way)
+   in the Zig FFI but `(line*31 + column) mod 4` (four-way) in `Stability.res`.
+   Reconcile them, then bind the proofs to the chosen implementation by
+   extraction or conformance tests rather than parallel models.
+3. **Zig weighted-average path.** `error_lang_calculate_stability` is a convex
+   combination (weights sum to 1) of per-factor scores in [0,100]; its [0,100]
+   bound holds for a *different* reason than the `Stability.res` clamp proved
+   here. Prove that path too.
+4. **Programs not executed in this environment.** Under the current network
+   policy the Deno runtime's JSR std deps (`jsr.io`) and Zig 0.13.0
+   (`ziglang.org`) are unreachable, and the ReScript compiler does not currently
+   build (`return` is not valid ReScript — `VM.res:407`; `dict<string, int>`
+   applies the one-argument `dict` constructor to two arguments —
+   `Types.res:233`). These were **not** run or fixed as part of this change and
+   are tracked as separate work — they are not claimed to pass.

compiler/src/Analyzer.affine

@@ -0,0 +1,233 @@
+// SPDX-License-Identifier: MPL-2.0
+// Analyzer.affine — static analysis & paradox detection
+// (ported from compiler/src/Analyzer.res).
+//
+// ── AffineScript port conventions ──
+//   * `open Types` + `open Stability` -> `use Types::*;` + `use Stability::*;`.
+//     The `Paradox`/`Consequence`/`Discovery` enums and the
+//     `operator_behavior_from_position` / `alternative_operator_behaviors` /
+//     `is_context_collapse` / `stability_bar` / `consequence_emoji` helpers
+//     are reused from Stability.affine verbatim.
+//   * ReScript inline-record variants -> positional (matching Stability's
+//     positional constructors and Types' positional AST/StabilityFactor ctors).
+//   * Backtick `${…}` templates with embedded newlines -> `++` concatenation
+//     with `\n`; emoji/box glyphs preserved. `Array.map(...)->Array.joinWith` ->
+//     `join(map(...), sep)`; `Array.slice(~start,~end)` -> `xs[a:b]`;
+//     `Array.mapWithIndex` -> an index-carrying loop.
+//
+// ── Faithfulness notes: documented gaps / simplifications vs Analyzer.res ──
+//   * `analyze_program` is OMITTED. It constructs an `AnalysisResult` whose
+//     `stabilityReport` field is a `Types::StabilityReport`, and it does so by
+//     calling `Stability::generate_report` — both of which are unconstructable
+//     because `StabilityReport.breakdown : Dict<String,Int>` has no value-level
+//     introduction in AffineScript (full rationale in Stability.affine's
+//     header). The AST walk it performs (paradox detection via
+//     `is_context_collapse` on let-names and `operator_behavior_from_position`
+//     on +/-/* binaries, plus mutable-state factor accumulation) cannot be
+//     surfaced without building that result record, so it is not ported.
+//     Consumers that already hold an `AnalysisResult` work: `forensic_analysis`
+//     (which only READS `analysis.stabilityReport.factors`) is ported, as is
+//     `format_stability_report` (which READS a `StabilityReport`).
+//   * Everything else is ported with identical strings/arithmetic: the
+//     `Paradox`/`Consequence`/etc. constructors, `trace_causality`,
+//     `generate_alternatives`, `forensic_analysis`, `format_paradox`, and
+//     `format_stability_report` (including the top-3 recommendation slice).
+//   * No `runTests`/Console code exists in Analyzer.res, so nothing else omitted.
+
+module Analyzer;
+
+use prelude::*;
+use string::{join};
+use Types::*;
+use Stability::*;
+
+// ============================================
+// Program Analysis (result type)
+// ============================================
+
+// `stabilityReport` is a `Types::StabilityReport` (phantom `Dict` field — see
+// header); the struct can be declared but not constructed here.
+pub struct AnalysisResult {
+  paradoxes: [Paradox],
+  consequences: [Consequence],
+  stabilityReport: StabilityReport,
+  discoveries: [Discovery]
+}
+
+// NOTE: `analyze_program` (Analyzer.res) is intentionally not ported — it
+// builds an `AnalysisResult` containing a `Types::StabilityReport`, which is
+// unconstructable in AffineScript (see header / Stability.affine).
+
+// ============================================
+// Causality Tracing
+// ============================================
+
+pub struct CausalityChain {
+  symptom: String,
+  symptomLocation: Location,
+  chain: [(String, Location)],
+  rootCause: String,
+  rootLocation: Location
+}
+
+pub fn trace_causality(symptom: String, symptom_loc: Location, prog: Program) -> CausalityChain {
+  // Simplified causality tracing — in a real implementation this would track
+  // data flow through the AST.
+  #{ symptom: symptom,
+     symptomLocation: symptom_loc,
+     chain: [("Type mismatch propagated from", symptom_loc)],
+     rootCause: "Unvalidated user input",
+     rootLocation: symptom_loc }
+}
+
+// ============================================
+// Alternative Code Generation
+// ============================================
+
+pub struct Alternative {
+  description: String,
+  code: String,
+  stabilityScore: Int,
+  improvements: [String]
+}
+
+pub fn generate_alternatives(stmt: Stmt, current_stability: Int) -> [Alternative] {
+  match stmt {
+    LetStmt(mutable_, name, _type, _value, _loc) =>
+      if mutable_ {
+        [
+          #{ description: "Use immutable binding",
+             code: "let " ++ name ++ " = ...",
+             stabilityScore: current_stability + 15,
+             improvements: [
+               "No mutation risk",
+               "Thread-safe by default",
+               "Easier to reason about"
+             ] }
+        ]
+      } else {
+        []
+      },
+    _ => []
+  }
+}
+
+// ============================================
+// Forensic Analysis (Deep Dive)
+// ============================================
+
+pub struct ForensicTrace {
+  target: String,
+  targetLocation: Location,
+  instabilityFactors: [(String, Int, String)], // (description, impact, reason)
+  probabilityMap: [(String, Int)],             // (scenario, probability %)
+  suggestedFix: String
+}
+
+fn factor_description(factor: StabilityFactor) -> String {
+  match factor {
+    MutableState(_m, _r) => "Mutable state detected",
+    TypeInstability(_x) => "Type changed dynamically",
+    _ => "Unknown factor"
+  }
+}
+
+pub fn forensic_analysis(target: String, target_loc: Location, analysis: AnalysisResult) -> ForensicTrace {
+  // Find all factors affecting this target.
+  let factors = map(analysis.stabilityReport.factors, |factor| {
+    let impact = stability_impact(factor);
+    (factor_description(factor), impact, "See stability report")
+  });
+
+  let probability_map = [
+    ("Standard behavior", 40),
+    ("Positional override", 30),
+    ("Context collapse", 20),
+    ("Temporal corruption", 10)
+  ];
+
+  #{ target: target,
+     targetLocation: target_loc,
+     instabilityFactors: factors,
+     probabilityMap: probability_map,
+     suggestedFix: "Move to different position or add explicit type" }
+}
+
+// ============================================
+// Visualization Formatters
+// ============================================
+
+pub fn format_paradox(paradox: Paradox) -> String {
+  match paradox {
+    ContextCollapseKeyword(keyword, line, _depth, _isKw, reason) =>
+      "⚡ QUANTUM KEYWORD at line " ++ int_to_string(line) ++ "\n" ++
+      "   '" ++ keyword ++ "' is both keyword AND identifier\n" ++
+      "   Reason: " ++ reason,
+
+    PositionalOperator(operator, line, column, behavior, alternatives) =>
+      "🎲 POSITIONAL OPERATOR at line " ++ int_to_string(line) ++ ":" ++ int_to_string(column) ++ "\n" ++
+      "   '" ++ operator ++ "' behaves as: " ++ behavior ++ "\n" ++
+      "   Alternative positions:\n" ++
+      join(map(alternatives, |pair| {
+        let (col, beh) = pair;
+        "     Col " ++ int_to_string(col) ++ ": " ++ beh
+      }), "\n"),
+
+    TypeSuperposition(variable, _line, possible_types, collapse_target) =>
+      "🌀 TYPE SUPERPOSITION\n" ++
+      "   Variable '" ++ variable ++ "' exists as: " ++ join(possible_types, " | ") ++ "\n" ++
+      "   Will collapse to: " ++ collapse_target,
+
+    ScopeLeakage(variable, declared_line, access_line, _runNumber, leak_reason) =>
+      "🕐 SCOPE LEAKAGE\n" ++
+      "   Variable '" ++ variable ++ "' declared at line " ++ int_to_string(declared_line) ++ "\n" ++
+      "   Accessible at line " ++ int_to_string(access_line) ++ "\n" ++
+      "   Reason: " ++ leak_reason,
+
+    TemporalCorruption(variable, _line, _affectedByRun, mechanism) =>
+      "⏰ TEMPORAL CORRUPTION\n" ++
+      "   Variable '" ++ variable ++ "' affected by historical state\n" ++
+      "   Mechanism: " ++ mechanism
+  }
+}
+
+fn factor_line(factor: StabilityFactor) -> String {
+  let emoji = consequence_emoji(factor);
+  let impact = stability_impact(factor);
+  let desc = match factor {
+    MutableState(mutations, readers) =>
+      "Mutable state (" ++ int_to_string(mutations) ++ " mutations, " ++ int_to_string(readers) ++ " readers)",
+    TypeInstability(reassignments) =>
+      "Type instability (" ++ int_to_string(reassignments) ++ " reassignments)",
+    NullPropagation(depth) =>
+      "Null propagation (depth " ++ int_to_string(depth) ++ ")",
+    _ => "Other factor"
+  };
+  emoji ++ " " ++ desc ++ ": " ++ int_to_string(impact) ++ " points"
+}
+
+pub fn format_stability_report(report: StabilityReport) -> String {
+  let bar = stability_bar(report.score);
+
+  let factor_list = join(map(report.factors, factor_line), "\n   ");
+
+  // Top-3 recommendations with 1-based numbering.
+  let recs = report.recommendations;
+  let top = if len(recs) > 3 { recs[0:3] } else { recs };
+  let mut rec_lines = "";
+  let mut i = 0;
+  let n = len(top);
+  while i < n {
+    if i > 0 { rec_lines = rec_lines ++ "\n"; }
+    rec_lines = rec_lines ++ "   " ++ int_to_string(i + 1) ++ ". " ++ top[i];
+    i = i + 1;
+  }
+
+  "\n🎯 STABILITY REPORT\n" ++
+  "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━\n\n" ++
+  bar ++ "\n\n" ++
+  "Breakdown:\n" ++
+  "   " ++ factor_list ++ "\n\n" ++
+  "💡 Top Recommendations:\n" ++
+  rec_lines ++ "\n"
+}