Claude/youthful fermat 90bhhu (#35)

* 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

* compiler: port Bytecode.res + Codegen.res + VM.res -> .affine

Modules 7-9 (251 + 526 + 727 = 1504 lines), all verified green with affinescript
check and the full 9-module harness. Completes the core compiler execution path.

Bytecode.affine: 44 opcodes (stack/vars/arith-with-position-metadata/comparison/
control-flow/arrays/haptics/the five Echo ops/print/halt) + Value/Chunk/
BytecodeProgram + value_to_string/opcode_to_string. paradoxType constructors
Px-prefixed to avoid colliding with Types' StabilityFactor::NullPropagation.

Codegen.affine: AST -> bytecode. Immutable Compiler threaded; compile_expr returns
the expression Location (so ExprStmt's trailing OpPop needs no re-traversal of a
consumed node); jump backpatching via array rebuild (set_code_at). Echo lowering
pushes args left-to-right then emits the dedicated OpEcho* op.

VM.affine: stack interpreter. Immutable Vm; stack is a [Value] with an sp mirror;
globals an assoc list. Runtime errors are values (Result + ExecResult =
ExContinue|ExHalt|ExError), not exceptions -- error strings preserved verbatim.
Echo runtime semantics byte-faithful: OpEchoToResidue debits echo_erase_cost (15.0),
erases the witness, pushes VResidue (idempotent on a residue); OpEchoInput errors on
a residue; OpEchoOutput returns the retained output. Pop-order, OpArray ordering,
and OpSub/OpDiv operand order all match VM.res arm-for-arm.

Documented faithful deviations: float pow uses repeated multiplication (integer-
exact; the stdlib has no ln/log) -- the only numeric divergence; the .res
"Not implemented" ops (OpLte/OpGte, OpCall) reproduced exactly; the Console *debug*
disassembler omitted (its pure helpers kept); real VM print/IO kept.

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

* compiler: port the remaining 8 compiler/src modules -> .affine

Completes the compiler/src ReScript->AffineScript port: all 17 modules are now
.affine. 2785 lines across Stability, Pretty, TokenStream, LayerNavigator,
Analyzer, FiveWhys, IncrementalLexer, IncrementalParser. All verified green with
affinescript check and the full 17-source harness.

- Stability: paradox/consequence/discovery detection + stability arithmetic.
- Pretty: AST->source pretty-printer (immutable Printer threaded through pp_*).
- TokenStream: proc-macro-style token-stream API + of_string lexer.
- LayerNavigator: 5-layer (Grammar/Parser/AST/Semantics/Runtime) views; owns Layer.
- Analyzer: paradox/report formatters, causality, forensic trace.
- FiveWhys: automated root-cause why-chains.
- IncrementalLexer / IncrementalParser: edit-driven re-lex / re-parse + splice.

Documented omissions (one AffineScript limitation, three call sites): the
record-constructor functions generate_report (Stability), analyze_program
(Analyzer) and create_layer_views (LayerNavigator) build records whose fields are
typed Dict<K,V> in the shipped types. Dict<K,V> is effectively a PHANTOM TYPE in
AffineScript -- accepted in annotations but with no value-level introduction (no
literal, no constructor, no Dict-returning builtin; the stdlib `dict` is a distinct
assoc-list type that does not unify). Those records therefore cannot be
constructed; every function that READS such a field is ported. Closing them needs
the Dict fields switched to the idiomatic assoc-list representation [(K,V)] (or
affinescript's Dict made constructable) -- tracked as a follow-up. format_diagnostic
is reimplemented locally (byte-faithful) since the shipped Types.affine omitted it.

Confirmed all three prior affinescript bugs (builtin-shadow bit once via a `length`
param). The Dict phantom-type is the fourth distinct affinescript limitation found
this migration.

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

* ci: refresh stale hyperpolymath/standards workflow pins

The required `Check Workflow Staleness` governance check failed because
governance.yml and scorecard.yml pinned the standards reusable workflows to
5a93d9d, which is out of the recency window (not a recognised ancestor of
standards HEAD; the window is <=50 commits behind HEAD or <=14 days old).

Re-pin both to the current standards HEAD
e8fe153b568af5e3534a261eee0258fa84fa6c5e (the SHA the check itself reports), so
the check passes and (auto-)merge unblocks for this and future PRs. mirror.yml's
separate pin was not flagged and is left as-is; there is no scorecard-enforcer.yml
in this repo to remove.

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

* cleanup: drop dead ReScript/TS duplicates; LSP via affinescript server

Part of task #8 (reduce the banned-language footprint):
- Delete playground/compiler/* (a dead, unwired duplicate mini-compiler;
  imported nowhere). NOTE it carried a unique ErrorInjector.res — flagged in
  case the educational error-injection demo should be re-introduced later.
- Delete bench/BenchLexer.res + bench/BenchParser.res (unreferenced benchmarks).
- Delete cli/lsp-server.ts (274-line TypeScript LSP) — superseded by the
  compiler's built-in `affinescript server` (JSON-RPC LSP on stdin/stdout);
  README.adoc updated to invoke it.

Compiler/src .affine harness still green (unaffected).

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