ReScript→AffineScript migration: Cst.affine (module 3)

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/Cst.affine

@@ -0,0 +1,228 @@
+// SPDX-License-Identifier: MPL-2.0
+// Cst.affine — Concrete Syntax Tree for Error-Lang (ported from compiler/src/Cst.res).
+//
+// A CST preserves all source text (whitespace, comments, exact tokens) so source
+// round-trips. Ported to AffineScript's functional style (no mut struct fields /
+// record spread): stateful classify_trivia loops a `let mut` local; lex_with_trivia
+// folds raw tokens carrying the last token in hand (so newline-trailing-trivia and
+// trailing source are attached without array-index mutation).
+//
+// Selective `Types` import: Cst's node kinds (MainBlock/FunctionDecl/LetStmt/...)
+// would collide with Types' Decl/Stmt constructors under a glob import, so only the
+// token/location types (+ the Newline constructor for matching) are imported.
+//
+// Omitted vs Cst.res (documented):
+//   - node_at: returning a deepest *subtree* needs a node used both to recurse into
+//     and to return — not expressible under affine ownership without a shared/clone
+//     type. Auxiliary (IDE cursor lookup); deferred.
+//   - run_tests: the test harness (Console-based) is not part of the compiler.
+
+module Cst;
+
+use prelude::*;
+use string::{length, substring, join, char_at};
+use collections::{flat_map};
+use Types::{TokenType, Position, Location, Token, Newline};
+use Lexer::{lex};
+
+// ---- trivia ----
+
+enum TriviaKind { TkWhitespace, TkLineComment, TkNewline }
+
+struct Trivia {
+  kind: TriviaKind,
+  text: String,
+  loc: Location
+}
+
+struct CstToken {
+  tokenKind: TokenType,
+  text: String,
+  leadingTrivia: [Trivia],
+  trailingTrivia: [Trivia],
+  loc: Location
+}
+
+enum CstNodeKind {
+  SourceFile, MainBlock, FunctionDecl, StructDecl, LetStmt, IfStmt, WhileStmt,
+  ForStmt, ReturnStmt, BreakStmt, ContinueStmt, PrintStmt, GutterBlock, ExprStmt,
+  BinaryExpr, UnaryExpr, CallExpr, IndexExpr, MemberExpr, TernaryExpr, LambdaExpr,
+  ArrayLitExpr, ParamList, ArgList, ErrorNode
+}
+
+enum CstNode {
+  NodeToken(CstToken),
+  NodeTree(CstTree)
+}
+
+struct CstTree {
+  kind: CstNodeKind,
+  children: [CstNode],
+  loc: Location
+}
+
+// ---- location helpers ----
+
+fn mk_pos(line: Int, column: Int, offset: Int) -> Position {
+  #{ line: line, column: column, offset: offset }
+}
+
+fn mk_loc(start_off: Int, end_off: Int, file: String) -> Location {
+  #{ start: mk_pos(0, 0, start_off), end_: mk_pos(0, 0, end_off), file: file }
+}
+
+fn code_at_str(s: String, i: Int) -> Int {
+  match char_at(s, i) {
+    Some(c) => char_to_int(c),
+    None => -1
+  }
+}
+
+fn is_ws_code(c: Int) -> Bool { c == 32 || c == 9 || c == 13 }
+
+// ---- source reconstruction (round-trip) ----
+
+fn trivia_text(t: Trivia) -> String { t.text }
+
+pub fn to_source(node: CstNode) -> String {
+  match node {
+    NodeToken(tok) => {
+      let leading = join(map(tok.leadingTrivia, trivia_text), "");
+      let trailing = join(map(tok.trailingTrivia, trivia_text), "");
+      leading ++ tok.text ++ trailing
+    },
+    NodeTree(tree) => tree_to_source(tree)
+  }
+}
+
+pub fn tree_to_source(tree: CstTree) -> String {
+  join(map(tree.children, to_source), "")
+}
+
+// ---- token collection (document order) ----
+
+fn node_tokens(node: CstNode) -> [CstToken] {
+  match node {
+    NodeToken(tok) => [tok],
+    NodeTree(subtree) => tokens(subtree)
+  }
+}
+
+pub fn tokens(tree: CstTree) -> [CstToken] {
+  flat_map(node_tokens, tree.children)
+}
+
+// ---- trivia classification (gap of source -> trivia items) ----
+
+pub fn classify_trivia(gap: String, file: String, base_offset: Int) -> [Trivia] {
+  let mut result = [];
+  let mut i = 0;
+  let glen = length(gap);
+  while i < glen {
+    let c = code_at_str(gap, i);
+    if c == 35 { // '#': line comment to end of line
+      let start = i;
+      let mut j = i;
+      while (j < glen) && (code_at_str(gap, j) != 10) { j = j + 1; }
+      let loc = mk_loc(base_offset + start, base_offset + j, file);
+      result = result ++ [#{ kind: TkLineComment, text: substring(gap, start, j), loc: loc }];
+      i = j;
+    } else if c == 10 { // newline
+      let loc = mk_loc(base_offset + i, base_offset + i + 1, file);
+      result = result ++ [#{ kind: TkNewline, text: "\n", loc: loc }];
+      i = i + 1;
+    } else if is_ws_code(c) { // contiguous whitespace
+      let start = i;
+      let mut j = i;
+      while (j < glen) && is_ws_code(code_at_str(gap, j)) { j = j + 1; }
+      let loc = mk_loc(base_offset + start, base_offset + j, file);
+      result = result ++ [#{ kind: TkWhitespace, text: substring(gap, start, j), loc: loc }];
+      i = j;
+    } else { // anything else (shouldn't occur in gaps)
+      let loc = mk_loc(base_offset + i, base_offset + i + 1, file);
+      result = result ++ [#{ kind: TkWhitespace, text: substring(gap, i, i + 1), loc: loc }];
+      i = i + 1;
+    }
+  }
+  result
+}
+
+// ---- trivia-aware lexing ----
+
+struct LexAcc {
+  committed: [CstToken],
+  last: Option<CstToken>,
+  prev_end: Int
+}
+
+fn set_trailing(t: CstToken, trailing: [Trivia]) -> CstToken {
+  #{ tokenKind: t.tokenKind, text: t.text, leadingTrivia: t.leadingTrivia,
+     trailingTrivia: trailing, loc: t.loc }
+}
+
+pub fn lex_with_trivia(source: String, file: String, run_number: Int) -> [CstToken] {
+  let (raw_tokens, _diags) = lex(source, file, run_number);
+
+  let final = fold(raw_tokens, #{ committed: [], last: None, prev_end: 0 }, |acc, tok| {
+    let tok_start = tok.loc.start.offset;
+    let tok_end = tok.loc.end_.offset;
+    let leading = if tok_start > acc.prev_end {
+      classify_trivia(substring(source, acc.prev_end, tok_start), file, acc.prev_end)
+    } else {
+      []
+    };
+    match tok.type_ {
+      Newline => {
+        let nl = #{ kind: TkNewline, text: tok.lexeme, loc: tok.loc };
+        match acc.last {
+          None => {
+            let synth = #{ tokenKind: tok.type_, text: tok.lexeme, leadingTrivia: leading,
+                           trailingTrivia: [], loc: tok.loc };
+            #{ committed: acc.committed, last: Some(synth), prev_end: tok_end }
+          },
+          Some(lt) => {
+            let updated = set_trailing(lt, lt.trailingTrivia ++ leading ++ [nl]);
+            #{ committed: acc.committed, last: Some(updated), prev_end: tok_end }
+          }
+        }
+      },
+      _ => {
+        let new_committed = match acc.last {
+          Some(lt) => acc.committed ++ [lt],
+          None => acc.committed
+        };
+        let new_tok = #{ tokenKind: tok.type_, text: tok.lexeme, leadingTrivia: leading,
+                         trailingTrivia: [], loc: tok.loc };
+        #{ committed: new_committed, last: Some(new_tok), prev_end: tok_end }
+      }
+    }
+  });
+
+  // attach trailing source after the last token, then commit the last token
+  let total_len = length(source);
+  match final.last {
+    None => final.committed,
+    Some(lt) => {
+      let lt2 = if final.prev_end < total_len {
+        set_trailing(lt, lt.trailingTrivia ++ classify_trivia(substring(source, final.prev_end, total_len), file, final.prev_end))
+      } else {
+        lt
+      };
+      final.committed ++ [lt2]
+    }
+  }
+}
+
+// ---- public API ----
+
+pub fn parse_to_cst(source: String, file: String, run_number: Int) -> CstTree {
+  let cst_tokens = lex_with_trivia(source, file, run_number);
+  let children = map(cst_tokens, |tok| NodeToken(tok));
+  let n = len(cst_tokens);
+  let loc = if n == 0 {
+    mk_loc(0, 0, file)
+  } else {
+    #{ start: cst_tokens[0].loc.start, end_: cst_tokens[n - 1].loc.end_, file: file }
+  };
+  #{ kind: SourceFile, children: children, loc: loc }
+}