ReScript→AffineScript migration: Parser + TypeChecker + TypeSuperposition (modules 4–6) (#29)

* 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

* compiler: port Parser.res -> Parser.affine (recursive-descent parser)

Fourth and largest module (1150 lines). Complete error-tolerant recursive-descent
parser, faithful grammar and precedence. Functional state-threading: ParserState
is immutable; producers return (Option<X>, ParserState) and callers thread via
`let (x, st) = f(st)`; ReScript `ref` accumulators became `let mut` locals with
(acc, state) while-loops.

Full coverage: the expression ladder (ternary -> logical-or/and -> equality ->
comparison -> term -> factor -> unary -> postfix -> primary), array/lambda/grouped
primaries, call/index/member postfix chains; type expressions incl. Echo<A,B> /
EchoR<A,B> and the >>-split close-angle; the full statement set incl. gutter-block
error recovery; function/struct/main declarations; and the `parse` driver returning
(Program, [Diagnostic]). Verified green with `affinescript check` and the full
harness (Types/Lexer/Cst/Parser all ok).

Documented faithful deviations: the >>-split token rewrite reproduced via array
rebuild (tokens are immutable); the pre-existing node-`start` quirk reproduced
exactly rather than corrected; minor error-recovery loop hardening to guarantee
progress on a stray token.

AffineScript checker bug found + worked around: an if-statement immediately
followed by a tuple literal in tail position fails with E0104 "Expected a function,
got Unit" (the if's () is applied to the tuple). Used explicit `return (...)`.
Third affinescript bug this migration (after the module-resolver struct-field gap
and the global `len` builtin-shadow); all worth upstreaming.

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

* compiler: port TypeChecker.res + TypeSuperposition.res -> .affine

Modules 5 + 6 (1123 + 323 lines), both verified green with affinescript check and
the full harness (all six modules ok).

TypeChecker.affine: the static checker. The .res's shared-mutable env (fresh-var
counter + substitution map) and checkResult.errors are unified into one immutable,
threaded CheckState, returned via (result, CheckState) tuples. The lexical
environment is a frame-stack [[(String, Binding)]] (head = innermost); the
substitution map is an Int-keyed assoc list. Unification is faithful arm-for-arm
including numeric widening and the Echo/EchoR rule: same-kind structural only,
Echo<_,_> deliberately NOT unifying with EchoR<_,_> (erasure is irreversible). The
Echo builtins (echo / echo_to_residue / residue_strictly_loses / echo_input /
echo_output) mirror the .res including the [Stab-Erase] diagnostics. Internal `ty`
constructors are C-prefixed (CInt..CVar) to avoid colliding with Types' TypeExpr.

TypeSuperposition.affine: the quantum-type demo (Collapsed | Superposition(...));
the deterministic collapse index is byte-faithful.

Documented faithful deviations: the .res `exprLoc` helper is omitted — `infer_expr`
returns the expression's own Location (a copyable summary) alongside the type, so
diagnostics keep exact locations without re-traversing a consumed node;
Array.zip/every/forEach over state-mutating callbacks become state-threading folds;
minor local renames to avoid global-constructor collisions. No type rule,
diagnostic, Echo/EchoR behaviour, or collapse arithmetic was changed.

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