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

* error-lang: replace fabricated ABI "proofs" with machine-checked ones

The three "Safety Proofs" in src/abi/Foreign.idr (stabilityBounded,
positionalDeterministic, paradoxMonotonic) were not proofs: each fabricated
its evidence with cast ()/cast Refl over an IO action. Replace them with
genuine, self-contained Idris2 modules, machine-checked under Idris 2 v0.8.0
(no believe_me / assert_total / cast / postulate):

- Stability.idr  : stability score is bounded in [0,100] (clamp model of
                   compiler/src/Types.res calculateStability).
- Positional.idr : positional-operator behaviour is deterministic over the
                   pure model of the Zig FFI (a genuine Refl, not IO cast Refl).
- Paradox.idr    : the two threshold-gated factors are monotone; the blanket
                   "paradox detection monotonic" claim is RETRACTED -- proving
                   it honestly surfaced that scope_leakage is prime-gated and
                   therefore non-monotone (line 7 prime, line 8 not).

Foreign.idr is reduced to an honest, self-contained ABI binding layer.
Add error-lang-abi.ipkg and verification/check-proofs.sh (idris2 --check all
four modules). Rewrite PROOF-NEEDS.md to record what is proved, what is
retracted, the toolchain, and open conformance obligations.

The language's satirical "100% production-ready / formally verified"
self-presentation in README/WHITEPAPER is intentional and left intact; this
change only makes the underlying proof artifacts real and honest.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

* docs: design Error-Lang as a Trope IR front end (trope-particularity integration)

Adds docs/Trope-Particularity-Integration.adoc — a design (not yet implemented)
for lowering Error-Lang's Echo operations and stability factors to the
language-neutral Trope IR (hyperpolymath/trope-checker, v0.1 prevent profile)
and consuming the verified verdict + witness.

- Object/effect/grade correspondence: Echo<A,B> <-> Trope[Phi], EchoR <->
  FloatingQuality, echo/echo_to_residue/echo_input/echo_output <-> preserve/
  detach/project. echo_to_residue IS detach (bond=Severed, irrecoverable),
  matching the [Stab-Erase] debit and "decomposition must be visible".
- stabilityFactor -> grade mapping; the silent instabilities (GlobalState,
  RaceCondition) land on the deceptive Conflated bottom -> a lowering fault
  under the prevent profile.
- Verdict mapping: scalar calculateStability -> use-model floor + p-sufficient/
  p-insufficient + witness edge (the invariant-path argmin Stability.idr already
  reasons about).
- Architecture (reference, never vendor; schema is the trust boundary), the
  per-front-end O2 lowering-correctness obligations (L-Echo/L-Grade/L-Silent/
  L-Floor), and a 4-phase plan.

Builds on docs/Echo-Decomposition.adoc; references echo-types, trope-checker and
trope-particularity-workbench by URL only.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

* docs: qualify external repo paths to clear structural_drift (SD022)

Hypatia structural_drift flagged `src/idris2/` and `src/aggregate/` in the
trope-integration design as dangling references "surviving a directory rename".
Both are deliberately *external*: the trope-checker repo's Idris2 core and the
panic-attack repo's aggregate module. Reword as unambiguously external (drop the
bare `src/<dir>/` form) so the heuristic no longer reads them as internal
error-lang tree paths. No substantive content change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

* compiler: begin ReScript->AffineScript migration — port Types.res

First module of the compiler's migration to AffineScript (the Hyperpolymath
language policy bans ReScript). Adds compiler/src/Types.affine, a faithful port
of compiler/src/Types.res, verified green with `affinescript check`:

- all token / AST / error / stability types (structs + enums + match)
- ReScript inline-record variants lowered to positional constructor args
- token variants Float/String renamed FloatTok/StringTok (reserved type keywords
  in AffineScript)
- Echo types (TyEcho / TyEchoResidue) shaped Trope-IR-ready per
  docs/Trope-Particularity-Integration.adoc (Phase 0)
- make_default_state, stability_impact, calculate_stability, error_code_to_string

Toolchain, so the .affine sources are reproducibly CI-verifiable:
- scripts/install-affinescript-toolchain.sh — builds the AffineScript compiler
  from distro OCaml packages (independent of opam.ocaml.org) + installs the
  binary and stdlib under a discoverable share/ path
- verification/check-affinescript.sh — typechecks all compiler/src/*.affine

Types.res is retained until its dependents migrate; format_diagnostic is deferred
pending the string / affine-borrow pass.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

* compiler: fix AffineScript module system to unblock the per-module port

The .res -> .affine port needs sibling compiler modules to import the shared AST
(Location/Token/Position/...) from Types. AffineScript's module resolver exported
imported enum constructors but dropped imported struct/alias type definitions, so
cross-module struct field access failed ("Field not found"). Per the chosen
approach (fix the resolver, not single-file/accessors):

- patches/affinescript-module-struct-fields.patch: threads imported modules'
  type_env + constructor_env into the importing module's typecheck context
  (typecheck.ml check_program gains ?import_type_env/?import_constructor_env;
  resolve.ml import_type_defs copies them across all three import forms;
  bin/main.ml passes them at the check/compile/eval entry points). Documented in
  patches/README.adoc; pending upstream to hyperpolymath/affinescript.
- compiler/src/Types.affine: now a proper `module Types;` with `pub` exports.
- verification/check-affinescript.sh: checks from compiler/src so `use Types::{...}`
  resolves via the loader's current-dir search.
- scripts/install-affinescript-toolchain.sh: applies the patch after cloning,
  before building (idempotent).

Verified: a module importing Types' structs with nested field access, struct
construction, and enum-field matching type-checks; affinescript's own stdlib
cross-module imports (http_fetch/option/io) still pass.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

* compiler: port Lexer.res -> Lexer.affine

Second compiler module. Lexer.affine imports Types (`use Types::*;`) and ports the
tokenizer in AffineScript's functional style: with no mutable struct fields or
record-spread, state-mutating helpers take a LexerState and return a new one, and
the scanners + driver loop a `let mut` local. Single chars are Char (char_at /
char_to_int); lexemes and the escape buffer use substring; numeric literals use
the parse_int / parse_float builtins; the keyword Dict becomes a string-equality
lookup. Verified green with `affinescript check`.

Faithful for the core path (identifiers/keywords, decimal int + float + exponent,
strings with escapes, all operators/delimiters, comments, newline + EOF, error
recovery + diagnostics E0001-E0004). Documented parity gaps for a follow-up pass:
hex/binary integer prefixes, triple-quoted strings + \0 escape, smart-quote E0007.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

* compiler: port Cst.res -> Cst.affine (concrete syntax tree + trivia)

Third module. Trivia-preserving CST with source round-trip. Functional port:
classify_trivia loops a `let mut` local; lex_with_trivia folds the raw tokens
carrying the last token in hand, so newline-trailing-trivia and trailing source
attach without array-index mutation. Selective `Types` import (Cst's node kinds
collide with Types' Decl/Stmt constructors). Verified with `affinescript check`.

Omitted, documented in-file:
- 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 Console-based test harness is not compiler code.

Encountered an affinescript resolver bug along the way: a local `let len = ...`
shadows the builtin `len` *globally* (so a later `len(xs)` typed as Int). Worked
around by renaming the local; worth an upstream fix in affinescript.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: hyperpolymath

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 }
+}