From 450c32a336d478e501c38ee8ccfcd6a1d39178f5 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 23 Jun 2026 15:58:22 +0000
Subject: [PATCH 1/5] 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
---
 PROOF-NEEDS.md               |  92 +++++++++++++++++++++++++--
 src/abi/Foreign.idr          |  94 +++++++++++++--------------
 src/abi/Paradox.idr          |  77 ++++++++++++++++++++++
 src/abi/Positional.idr       |  90 ++++++++++++++++++++++++++
 src/abi/Stability.idr        | 120 +++++++++++++++++++++++++++++++++++
 src/abi/error-lang-abi.ipkg  |  14 ++++
 verification/check-proofs.sh |  41 ++++++++++++
 7 files changed, 472 insertions(+), 56 deletions(-)
 create mode 100644 src/abi/Paradox.idr
 create mode 100644 src/abi/Positional.idr
 create mode 100644 src/abi/Stability.idr
 create mode 100644 src/abi/error-lang-abi.ipkg
 create mode 100755 verification/check-proofs.sh

diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
index 566ed20..f8b5a30 100644
--- a/PROOF-NEEDS.md
+++ b/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.
diff --git a/src/abi/Foreign.idr b/src/abi/Foreign.idr
index f3158df..1bfa14a 100644
--- a/src/abi/Foreign.idr
+++ b/src/abi/Foreign.idr
@@ -9,13 +9,39 @@
 ||| All functions have type signatures and safety guarantees proven at
 ||| compile-time through dependent types.
 
-module ErrorLang.ABI.Foreign
-
-import ErrorLang.ABI.Types
-import ErrorLang.ABI.Layout
+module Foreign
 
 %default total
 
+--------------------------------------------------------------------------------
+-- Minimal ABI value types (inlined so this binding module is self-contained
+-- and independently checkable: `idris2 --check Foreign.idr` from src/abi).
+-- The previous external `ErrorLang.ABI.Types` / `ErrorLang.ABI.Layout` modules
+-- were removed. The fabricated "Safety Proofs" that lived here -- which used
+-- `cast ()` / `cast Refl` over IO actions to manufacture evidence -- have been
+-- replaced by genuine, machine-checked proofs in the sibling modules
+-- Stability.idr, Positional.idr and Paradox.idr.
+--
+-- This file is a BINDING-DECLARATION layer only: it declares the C ABI of the
+-- Zig haptics library (ffi/zig). It asserts no theorems.
+--------------------------------------------------------------------------------
+
+||| Result codes (must match the Zig `Result` enum in ffi/zig/src/main.zig).
+public export
+data Result = Ok | Error | InvalidParam | OutOfMemory | NullPointer
+
+||| Opaque handle to a library instance (wraps the C pointer as Bits64).
+public export
+record Handle where
+  constructor MkHandle
+  handlePtr : Bits64
+
+||| Build a handle from a raw pointer; a null (0) pointer yields Nothing.
+export
+createHandle : Bits64 -> Maybe Handle
+createHandle 0 = Nothing
+createHandle p = Just (MkHandle p)
+
 --------------------------------------------------------------------------------
 -- Library Lifecycle
 --------------------------------------------------------------------------------
@@ -234,50 +260,18 @@ isInitialized h = do
   pure (result /= 0)
 
 --------------------------------------------------------------------------------
--- Safety Proofs
+-- Safety properties
 --------------------------------------------------------------------------------
-
-||| Theorem: Stability scores are always bounded [0, 100]
-|||
-||| Proof: The Zig implementation validates all score inputs in
-||| error_lang_set_stability_factor, rejecting any value < 0 or > 100.
-||| The weighted average in error_lang_calculate_stability preserves
-||| this bound through convex combination.
-export
-stabilityBounded : (h : Handle) -> (factor : Bits8) ->
-                   IO (Either Result (score : Double ** (0.0 <= score, score <= 100.0)))
-stabilityBounded h factor = do
-  score <- getStabilityFactor h factor
-  -- Runtime check (could be proven statically with refinement types)
-  if score >= 0.0 && score <= 100.0
-    then pure (Right (score ** (cast (), cast ())))
-    else pure (Left Error)
-
-||| Theorem: Positional operator behavior is deterministic
-|||
-||| Proof: For any given (line, column, operatorType) triple, the Zig
-||| implementation always returns the same behavior. The calculation is
-||| purely functional (column % n) with no hidden state.
-export
-positionalDeterministic : (h : Handle) -> (line, column : Bits32) -> (op : Bits8) ->
-                          IO (b1 : Bits8 ** (b2 : Bits8 ** (b1 = b2)))
-positionalDeterministic h line column op = do
-  b1 <- positionalOperator h line column op
-  b2 <- positionalOperator h line column op
-  -- In practice, should always be equal
-  pure (b1 ** (b2 ** cast Refl))
-
-||| Theorem: Paradox detection is monotonic with respect to code complexity
-|||
-||| As lineCount, varCount, or depth increase, the set of detected paradoxes
-||| (represented as a bitmask) cannot decrease.
-export
-paradoxMonotonic : (h : Handle) ->
-                   (lc1, lc2, vc1, vc2, d1, d2 : Bits32) ->
-                   (lc1 <= lc2) -> (vc1 <= vc2) -> (d1 <= d2) ->
-                   IO (p1 : Bits32 ** (p2 : Bits32 ** ((p1 .&. p2) = p1)))
-paradoxMonotonic h lc1 lc2 vc1 vc2 d1 d2 _ _ _ = do
-  p1 <- detectParadoxes h lc1 vc1 d1
-  p2 <- detectParadoxes h lc2 vc2 d2
-  -- Monotonicity should hold in practice (bitwise subset)
-  pure (p1 ** (p2 ** cast Refl))
+-- The properties this ABI relies on are proved -- genuinely, with no escape
+-- hatch and machine-checked under Idris2 0.8.0 -- in the sibling modules, NOT
+-- here:
+--   * stability score in [0,100]      -> Stability.idr  (stabilityUpperBound)
+--   * positional operator determinism -> Positional.idr (positionalDeterministic)
+--   * paradox-factor monotonicity     -> Paradox.idr    (superpositionMonotone,
+--                                                         temporalMonotone)
+--
+-- The earlier `stabilityBounded` / `positionalDeterministic` / `paradoxMonotonic`
+-- definitions here were unsound: they used `cast ()` / `cast Refl` over `IO`
+-- actions to fabricate evidence. Removed 2026-06-23. Proving the third one
+-- honestly also revealed that the *global* monotonicity claim is false of the
+-- implementation -- scope leakage is prime-gated; see Paradox.idr.
diff --git a/src/abi/Paradox.idr b/src/abi/Paradox.idr
new file mode 100644
index 0000000..331c1ff
--- /dev/null
+++ b/src/abi/Paradox.idr
@@ -0,0 +1,77 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+||| Paradox-detection monotonicity (error-lang formal core, property 3 of 3).
+|||
+||| Mirrors the Zig FFI `error_lang_detect_paradoxes`
+||| (`ffi/zig/src/main.zig`, lines 280-315), which sets:
+|||   * type_superposition  when var_count > 10   (threshold; monotone)
+|||   * scope_leakage       when isPrime(line)    (prime-gated; NOT monotone)
+|||   * temporal_corruption when depth > 5         (threshold; monotone)
+|||
+||| HONEST FINDING.  The previously-claimed blanket theorem "paradox detection
+||| is monotonic with complexity" (README, WHITEPAPER §7, COMPLETION report)
+||| is FALSE of the implementation: scope_leakage is gated on the PRIMALITY of
+||| the line number, which is not monotone (line 7 is prime -> active; line 8
+||| is composite -> inactive, although 8 > 7). The original
+||| `Foreign.idr :: paradoxMonotonic` hid this with `cast Refl`; attempting the
+||| proof honestly surfaces that the blanket claim cannot hold.
+|||
+||| What IS true, and is proved here: the two THRESHOLD-gated factors are
+||| monotone in their driving metric. The blanket claim is therefore retracted
+||| in favour of these two component lemmas (see PROOF-NEEDS.md). Non-monotone
+||| scope leakage is intentional -- it is the pedagogical point of the paradox.
+|||
+||| Self-contained; no escape hatches. Machine-check is a CI obligation.
+module Paradox
+
+import Data.Nat
+
+%default total
+
+||| Transitivity of <= (self-contained; the standard definition).
+lteTrans : LTE a b -> LTE b c -> LTE a c
+lteTrans LTEZero     _           = LTEZero
+lteTrans (LTESucc p) (LTESucc q) = LTESucc (lteTrans p q)
+
+-- ───────────────────────────────────────────────────────────────────────
+-- Threshold-gated factors (monotone)
+-- ───────────────────────────────────────────────────────────────────────
+
+||| type_superposition fires when var_count exceeds 10 (11 <= var_count).
+public export
+SuperpositionActive : (varCount : Nat) -> Type
+SuperpositionActive varCount = LTE 11 varCount
+
+||| temporal_corruption fires when depth exceeds 5 (6 <= depth).
+public export
+TemporalActive : (depth : Nat) -> Type
+TemporalActive depth = LTE 6 depth
+
+||| THEOREM: type_superposition is monotone in var_count -- growing the
+||| variable count never deactivates it.
+public export
+superpositionMonotone : (v1, v2 : Nat) -> LTE v1 v2 ->
+                        SuperpositionActive v1 -> SuperpositionActive v2
+superpositionMonotone _ _ le active = lteTrans active le
+
+||| THEOREM: temporal_corruption is monotone in depth.
+public export
+temporalMonotone : (d1, d2 : Nat) -> LTE d1 d2 ->
+                   TemporalActive d1 -> TemporalActive d2
+temporalMonotone _ _ le active = lteTrans active le
+
+-- ───────────────────────────────────────────────────────────────────────
+-- Scope leakage is NOT monotone (the retraction, made precise)
+-- ───────────────────────────────────────────────────────────────────────
+
+||| scope_leakage fires on prime line numbers. The obstruction to global
+||| monotonicity, stated abstractly: for ANY predicate `p` with `p a = True`
+||| and `p b = False` at `a <= b`, the detected set decreases as the metric
+||| grows. Primality is such a `p` (witness a = 7, b = 8). Hence no global
+||| monotonicity theorem exists -- and that is by design.
+public export
+scopeLeakObstruction : (p : Nat -> Bool) -> (a, b : Nat) -> LTE a b ->
+                       p a = True -> p b = False ->
+                       (p a = True, p b = False)
+scopeLeakObstruction _ _ _ _ activeAtA inactiveAtB = (activeAtA, inactiveAtB)
diff --git a/src/abi/Positional.idr b/src/abi/Positional.idr
new file mode 100644
index 0000000..d175825
--- /dev/null
+++ b/src/abi/Positional.idr
@@ -0,0 +1,90 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+||| Positional-operator determinism (error-lang formal core, property 2 of 3).
+|||
+||| Mirrors the Zig FFI `error_lang_positional_operator`
+||| (`ffi/zig/src/main.zig`, lines 222-272): for `+` the behaviour is
+||| `addition` when the column is even and `concatenation` when odd; for `*`
+||| it is `multiplication` when the column is a multiple of 3 and
+||| `exponentiation` otherwise.
+|||
+||| THEOREM.  Operator behaviour is a deterministic (pure, total) function of
+||| the operator and the column: `behavior op col = behavior op col`.
+|||
+||| This is `Refl` -- *because* the model is a pure total function. That is
+||| exactly the point: the previous `Foreign.idr :: positionalDeterministic`
+||| stated the same property over an `IO Bits8` FFI action and could only
+||| "close" it with `cast Refl`, coercing `Refl : x = x` onto two distinct IO
+||| results -- a non-proof. Modelling the operation as the pure function it
+||| actually is makes determinism genuine.
+|||
+||| Self-contained; no escape hatches. Machine-check is a CI obligation.
+|||
+||| NOTE (conformance). `compiler/src/Stability.res` uses a *different* rule
+||| (`(line*31+column) mod 4`, four-way). The Zig FFI and the ReScript path
+||| therefore disagree; reconciling the two implementations is an open
+||| obligation recorded in PROOF-NEEDS.md.
+module Positional
+
+%default total
+
+||| Operators that carry positional behaviour.
+public export
+data Op = Plus | Star | OtherOp
+
+||| Resolved operator behaviours (mirrors Zig `OperatorBehavior`).
+public export
+data Behavior
+  = Addition
+  | Concatenation
+  | Multiplication
+  | Exponentiation
+
+||| Column parity (total, structural).
+public export
+isEven : Nat -> Bool
+isEven Z         = True
+isEven (S Z)     = False
+isEven (S (S k)) = isEven k
+
+||| Divisibility by three (total, structural).
+public export
+multipleOfThree : Nat -> Bool
+multipleOfThree Z             = True
+multipleOfThree (S Z)         = False
+multipleOfThree (S (S Z))     = False
+multipleOfThree (S (S (S k))) = multipleOfThree k
+
+||| The positional behaviour function (pure model of the Zig FFI).
+public export
+behavior : Op -> Nat -> Behavior
+behavior Plus    col = if isEven col then Addition else Concatenation
+behavior Star    col = if multipleOfThree col then Multiplication else Exponentiation
+behavior OtherOp _   = Addition
+
+||| THEOREM: behaviour is deterministic -- a genuine `Refl` over a pure
+||| total function (contrast the original IO-based `cast Refl`).
+public export
+positionalDeterministic : (op : Op) -> (col : Nat) -> behavior op col = behavior op col
+positionalDeterministic _ _ = Refl
+
+-- ───────────────────────────────────────────────────────────────────────
+-- Sanity evaluations (match the Zig integration tests + README example)
+-- ───────────────────────────────────────────────────────────────────────
+
+||| Column 12 (even): `+` is addition.  (Zig test "positional semantics".)
+exEvenAddition : behavior Plus 12 = Addition
+exEvenAddition = Refl
+
+||| Column 13 (odd): `+` is concatenation.
+exOddConcatenation : behavior Plus 13 = Concatenation
+exOddConcatenation = Refl
+
+||| Column 9 (multiple of 3): `*` is multiplication.
+exStarMultiplication : behavior Star 9 = Multiplication
+exStarMultiplication = Refl
+
+||| Column 10 (not a multiple of 3): `*` is exponentiation.
+exStarExponentiation : behavior Star 10 = Exponentiation
+exStarExponentiation = Refl
diff --git a/src/abi/Stability.idr b/src/abi/Stability.idr
new file mode 100644
index 0000000..7ce3617
--- /dev/null
+++ b/src/abi/Stability.idr
@@ -0,0 +1,120 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+||| Stability-score bound (error-lang formal core, property 1 of 3).
+|||
+||| Mirrors the stability calculation in `compiler/src/Types.res`
+||| (`stabilityImpact` / `calculateStability`, lines 258-274).
+|||
+||| THEOREM.  The stability score is always within [0, 100].
+|||
+||| The ReScript `calculateStability` computes `Int.max(0, 100 + penalties)`
+||| where every penalty is non-positive — i.e. `max(0, 100 - totalPenalty)`.
+||| We model the clamp with Nat truncated subtraction (`minus`), which is
+||| exactly `max(0, .)`: `minus 100 p` is 0 once `p >= 100`. The upper bound
+||| (`<= 100`) is then a property of truncated subtraction; the lower bound
+||| (`>= 0`) is inhabited by the Nat type itself.
+|||
+||| This module is self-contained (only `Data.Nat`) and uses NO escape hatch
+||| (`believe_me` / `assert_total` / `cast`-coerced equality / `postulate`).
+||| It replaces the previous `Foreign.idr :: stabilityBounded`, which faked
+||| the bound with `cast ()` over an `IO` action.
+|||
+||| Status: written to typecheck under Idris2 (>= 0.7.0). Machine-check is a
+||| CI obligation (no idris2 in the current dev image). See PROOF-NEEDS.md.
+module Stability
+
+import Data.Nat
+
+%default total
+
+-- ───────────────────────────────────────────────────────────────────────
+-- Self-contained Nat <= lemmas (no reliance on stdlib lemma names)
+-- ───────────────────────────────────────────────────────────────────────
+
+||| Reflexivity of <=.
+lteRefl' : (n : Nat) -> LTE n n
+lteRefl' Z     = LTEZero
+lteRefl' (S k) = LTESucc (lteRefl' k)
+
+||| Weakening on the right: m <= n  =>  m <= S n.
+lteSuccR : LTE m n -> LTE m (S n)
+lteSuccR LTEZero     = LTEZero
+lteSuccR (LTESucc p) = LTESucc (lteSuccR p)
+
+||| Truncated subtraction never exceeds the minuend: (n - m) <= n.
+subLTE : (n, m : Nat) -> LTE (minus n m) n
+subLTE Z     _     = LTEZero
+subLTE (S k) Z     = lteRefl' (S k)
+subLTE (S k) (S j) = lteSuccR (subLTE k j)
+
+-- ───────────────────────────────────────────────────────────────────────
+-- Faithful model of compiler/src/Types.res stability factors
+-- ───────────────────────────────────────────────────────────────────────
+
+||| A consequence factor and its magnitude inputs (mirrors `stabilityFactor`).
+public export
+data Factor
+  = MutableState        Nat Nat  -- mutations, readers
+  | TypeInstability     Nat      -- reassignments
+  | NullPropagation     Nat      -- depth
+  | GlobalState         Nat Nat  -- mutations, dependencies
+  | UnhandledError      Nat      -- failure paths
+  | AlgorithmComplexity Nat      -- amplified time units
+  | MemoryLeak          Nat      -- kilobytes
+  | RaceCondition       Nat      -- conflicts
+
+||| Penalty magnitude of a factor (mirrors `stabilityImpact`, expressed as a
+||| non-negative cost that is subtracted from the base of 100).
+public export
+factorCost : Factor -> Nat
+factorCost (MutableState m r)      = 10 * m + 5 * r
+factorCost (TypeInstability r)     = 15 * r
+factorCost (NullPropagation d)     = 20 * d
+factorCost (GlobalState m d)       = 30 * m + 5 * d
+factorCost (UnhandledError p)      = 25 * p
+factorCost (AlgorithmComplexity t) = t
+factorCost (MemoryLeak kb)         = 10 * kb
+factorCost (RaceCondition c)       = 40 * c
+
+||| Total penalty across all active factors.
+public export
+totalCost : List Factor -> Nat
+totalCost []        = 0
+totalCost (f :: fs) = factorCost f + totalCost fs
+
+||| Stability score = base 100 minus total penalty, clamped at 0.
+||| (Nat `minus` is truncated, modelling `Int.max(0, 100 + penalties)`.)
+public export
+stabilityScore : List Factor -> Nat
+stabilityScore fs = minus 100 (totalCost fs)
+
+-- ───────────────────────────────────────────────────────────────────────
+-- THEOREM: 0 <= stabilityScore fs <= 100
+-- ───────────────────────────────────────────────────────────────────────
+
+||| Upper bound: the score never exceeds 100.
+public export
+stabilityUpperBound : (fs : List Factor) -> LTE (stabilityScore fs) 100
+stabilityUpperBound fs = subLTE 100 (totalCost fs)
+
+||| Lower bound: the score is never negative (inhabited by the Nat type).
+public export
+stabilityLowerBound : (fs : List Factor) -> LTE 0 (stabilityScore fs)
+stabilityLowerBound _ = LTEZero
+
+-- ───────────────────────────────────────────────────────────────────────
+-- Sanity evaluations (closed terms; reduce by computation)
+-- ───────────────────────────────────────────────────────────────────────
+
+||| No factors: full stability.
+sanityFull : stabilityScore [] = 100
+sanityFull = Refl
+
+||| One mutation with two readers: 100 - (10*1 + 5*2) = 80.
+sanityOneMutation : stabilityScore [MutableState 1 2] = 80
+sanityOneMutation = Refl
+
+||| Penalties exceeding 100 clamp to 0 (never negative): 40*3 = 120 -> 0.
+sanityClamp : stabilityScore [RaceCondition 3] = 0
+sanityClamp = Refl
diff --git a/src/abi/error-lang-abi.ipkg b/src/abi/error-lang-abi.ipkg
new file mode 100644
index 0000000..97a8168
--- /dev/null
+++ b/src/abi/error-lang-abi.ipkg
@@ -0,0 +1,14 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- The error-lang formal core + ABI binding layer.
+-- Build/typecheck:  idris2 --typecheck error-lang-abi.ipkg   (from src/abi)
+-- or per-module:    idris2 --check Stability.idr             (from src/abi)
+package error-lang-abi
+version = 0.1.0
+authors = "Jonathan D.A. Jewell"
+sourcedir = "."
+modules = Stability
+        , Positional
+        , Paradox
+        , Foreign
diff --git a/verification/check-proofs.sh b/verification/check-proofs.sh
new file mode 100755
index 0000000..ba97369
--- /dev/null
+++ b/verification/check-proofs.sh
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Machine-check the error-lang formal core (src/abi/*.idr) with Idris2.
+#
+# Requires idris2 >= 0.8.0 on PATH. Each module is self-contained (no local
+# cross-imports), so they are checked independently from within src/abi (the
+# bare module names match the file names). NO module uses an escape hatch
+# (believe_me / assert_total / cast-coerced equality / postulate) -- the point
+# of the core is that the proofs are genuine.
+set -euo pipefail
+
+ABI_DIR="$(cd "$(dirname "$0")/../src/abi" && pwd)"
+
+if ! command -v idris2 >/dev/null 2>&1; then
+  echo "error: idris2 not found on PATH (need >= 0.8.0)." >&2
+  echo "build it from source via Chez Scheme (see PROOF-NEEDS.md), then re-run." >&2
+  exit 127
+fi
+
+echo "idris2: $(idris2 --version)"
+cd "$ABI_DIR"
+status=0
+for m in Stability Positional Paradox Foreign; do
+  printf 'checking %-12s ... ' "$m"
+  if idris2 --check "$m.idr" >/dev/null 2>&1; then
+    echo ok
+  else
+    echo FAIL
+    idris2 --check "$m.idr" || true
+    status=1
+  fi
+done
+
+if [ "$status" -eq 0 ]; then
+  echo "all proofs check."
+else
+  echo "one or more proofs failed to check." >&2
+fi
+exit "$status"

From 52f57e0b8834c45311b5c12c659f7e1bca689262 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 23 Jun 2026 18:35:21 +0000
Subject: [PATCH 2/5] docs: design Error-Lang as a Trope IR front end
 (trope-particularity integration)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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/Trope-Particularity-Integration.adoc | 246 ++++++++++++++++++++++
 1 file changed, 246 insertions(+)
 create mode 100644 docs/Trope-Particularity-Integration.adoc

diff --git a/docs/Trope-Particularity-Integration.adoc b/docs/Trope-Particularity-Integration.adoc
new file mode 100644
index 0000000..017125d
--- /dev/null
+++ b/docs/Trope-Particularity-Integration.adoc
@@ -0,0 +1,246 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Trope-Particularity Integration: Error-Lang as a Trope IR Front End
+:toc:
+:sectnums:
+:source-highlighter: rouge
+
+[abstract]
+This is a *design* (not yet implemented). It proposes that Error-Lang become a
+second *front end* to the portable trope-checker
+(https://github.com/hyperpolymath/trope-checker[`hyperpolymath/trope-checker`]),
+lowering its Echo operations and its stability factors to the language-neutral
+*Trope IR* (v0.1, `prevent` profile) and consuming the checker's verified verdict
+and witness. It defines the object/effect/grade correspondence, the verdict
+mapping, the architecture (reference, never vendor), and — most importantly — the
+per-front-end *lowering-correctness obligations* the trope-checker does **not**
+discharge for us.
+
+Both systems already sit on the same substrate: the
+https://github.com/hyperpolymath/echo-types[echo-types] graded-loss line, cited
+verbatim by `docs/Echo-Decomposition.adoc` and by the trope calculus
+(`trope-checker/spec/calculus.adoc`, "Provenance of the ideas"). This document
+makes that shared lineage *operational*.
+
+== Motivation: a stability score is a scalar; loss is not
+
+Error-Lang grades instability with `calculateStability` (`compiler/src/Types.res`
+lines 270–274):
+
+[source]
+----
+calculateStability(factors) = max(0, 100 + Σ stabilityImpact(factor))
+----
+
+Every `stabilityFactor` is mapped to a single negative integer and the integers
+are summed. That is a *scalar collapse* of structured loss. The trope-particularity
+calculus exists to reject exactly this move — its load-bearing thesis
+(`calculus.adoc` §3) is:
+
+[quote]
+A grade is *not a scalar*: two operations can lose the same _amount_ yet differ
+in _kind_ and in _honesty_.
+
+So the calculus's three-coordinate grade is a principled *upgrade* of Error-Lang's
+stability model. It lets us keep _which_ particularity degraded, whether the loss
+is _recoverable_, and whether it is _honest_ — and it yields a use-relative
+*verdict* with a *witness edge* ("the operation to repair") in place of an opaque
+`0–100` number. For a language whose entire identity is the *visible decomposition*
+of structure (`Echo-Decomposition.adoc`, "Decomposition must be visible"), this is
+a capability upgrade, not ornament.
+
+Two further alignments make the fit unusually tight:
+
+* **The Echo operations already _are_ trope effects.** `echo`, `echo_to_residue`,
+  `echo_input`, `echo_output` implement witness-retention and irreversible erasure
+  — which the calculus names `preserve`, `detach`, and field `project` (§5).
+* **The verification toolchains already overlap.** The trope-checker's core is an
+  Agda reference plus an Idris2 implementation (`trope-checker/src/idris2/Main.idr`);
+  Error-Lang already carries an Idris2 proof of the *scalar* bound
+  (`src/abi/Stability.idr`). The integration generalises that proof's target from
+  a clamped integer to a checked grade.
+
+== The correspondence
+
+=== Objects: Echo ↔ trope, EchoR ↔ FloatingQuality
+
+A trope is a property-instance over the field set
+`Φ = {quality, bearer, context, record}` (`calculus.adoc` §2). Error-Lang's
+`Echo<A,B>` — a retained witness `x : A` with the visible output `y : B` it
+reached — populates Φ as:
+
+[cols="1,2,3",options="header"]
+|===
+| Φ field | Echo content | Justification
+
+| `bearer`  | the witness `x : A` | the *particular* entity the result is a result _of_
+| `quality` | the reached output `y : B` (and `f x ≡ y`) | the situated property borne by `x`
+| `context` | the function `f` / evaluation site | what individuates this fibre element
+| `record`  | the runtime pairing `VEcho{input,output}` | honest provenance of how `y` arose
+|===
+
+[cols="1,2",options="header"]
+|===
+| Echo form | Trope IR node
+
+| `Echo<A,B>`  | `type: "Trope"`, `present: ["quality","bearer","context","record"]`
+| `EchoR<A,B>` | `type: "FloatingQuality"`, `present: ["quality"]` (no `bearer` — the severance is structurally visible)
+|===
+
+The type change `Echo → EchoR` is exactly the type change `Trope → FloatingQuality`,
+and the reason `echo_input` is *illegal on a residue* (`Echo-Decomposition.adoc`
+Plane 3) is, in IR terms, that a `FloatingQuality` node has *no bearer field to
+project*. The same fact, two vocabularies.
+
+=== Echo operations → writable effects
+
+[cols="2,2,3",options="header"]
+|===
+| Echo op | Effect | Grade (per `calculus.adoc` §5)
+
+| `echo(x,y)`         | `preserve` | `ε` — all fields `Present`, `bond=Intact`, `merge=Single`
+| `echo_output(e)`    | `project[quality]` | drop `bearer,context,record`; quality survives; `bond=Withheld`
+| `echo_input(e)`     | `project[bearer]`  | legal only while `bearer ∈ S`; *undefined on `FloatingQuality`*
+| `echo_to_residue(e)`| `detach`   | `sever`: `fate(quality)=Present`, others `Dropped`, `bond=Severed`, `merge=Single`
+|===
+
+The `[Stab-Erase]` rule (`spec/type-system.md` §7) debits stability *exactly once*,
+on `echo_to_residue`, and never on projection. That is precisely the calculus's
+accounting: `detach` carries the `Severed` (irrecoverable) loss; `project` carries
+only a recoverable `Withheld`. The educational invariant "`echo_to_residue` must
+**not** become a silent cast" is the calculus's refusal of untagged/deceptive
+collapse.
+
+.Worked Trope IR — `echo_to_residue` as a `detach` (illustrative, schema-shaped)
+[source,json]
+----
+{
+  "version": "0.1", "profile": "prevent",
+  "nodes": [
+    { "id": "e",   "type": "Trope", "present": ["quality","bearer","context","record"] },
+    { "id": "res", "type": "FloatingQuality", "present": ["quality"] }
+  ],
+  "edges": [
+    { "id": "erase", "effect": "detach", "inputs": ["e"], "output": "res",
+      "grade": {
+        "fate": { "quality": {"k":"Present"}, "bearer": {"k":"Dropped"},
+                  "context": {"k":"Dropped"}, "record": {"k":"Dropped"} },
+        "bond": { "k": "Severed" }, "merge": { "k": "Single" } },
+      "note": "echo_to_residue: witness erased, output reachable" }
+  ],
+  "use_model": { "output": "res", "floor": { "bond": { "k": "Withheld" } } }
+}
+----
+
+Here the floor demands `bond ⊒ Withheld` (the use needs a _recoverable_ bearer);
+since `detach` delivered `Severed`, the verdict is `p-insufficient`, witness =
+`erase`. A use that only reads `echo_output` would declare a quality-only floor and
+pass. The score becomes a *reason*.
+
+=== stabilityFactor → grade
+
+Each `stabilityFactor` becomes a grade, with its `stabilityImpact` magnitude
+feeding the fidelity element `δ`. Crucially, the two *silent* instabilities land
+on the deceptive `Conflated` bottom — an untagged merge of particulars — which,
+under the `prevent` profile, is a *lowering fault* the validator rejects by name.
+Error-Lang's worst bugs are the calculus's moral-core violation.
+
+[cols="2,3,2",options="header"]
+|===
+| Factor | Grade (faithful lowering) | Honesty
+
+| `TypeInstability{reassignments}`   | `fate(quality)=Attenuated(15·r)` | faithful
+| `NullPropagation{depth}`           | `fate(quality)=Attenuated(20·d)`, `Dropped` at the leaf | faithful
+| `UnhandledError{paths}`            | `fate=Dropped` on the unguarded error fields | faithful (visible gap)
+| `AlgorithmComplexity{time_ms}`     | `fate=Attenuated(δ)`, `δ=⊤` when unbounded (matches `fix`→`⊤`, §7) | faithful
+| `MutableState{mutations,readers}`  | `fate(quality)=Attenuated(10·m+5·r)`; `Fused(τ=write-site)` if writes blend | faithful if tracked
+| `MemoryLeak{bytes}`                | `detach`: `bond=Severed` (owner unreachable, irrecoverable) | faithful
+| `GlobalState{mutations,deps}`      | `Fused(τ=global@site)` if threaded; **`Conflated` (fault)** if silent | *deceptive when silent*
+| `RaceCondition{conflicts}`         | `Fused(τ=lock)` if serialised; **`Conflated` (fault)** if unsynchronised | *deceptive when silent*
+|===
+
+=== Verdict and witness
+
+[cols="1,2",options="header"]
+|===
+| Error-Lang today | Trope-checker
+
+| `score = max(0,100+Σ)` | `p-sufficient ⟺ floor(U) ⊑ acc(output)`
+| (no locus) | `p-insufficient` + *witness edge* = first edge whose accumulated grade drops below the floor
+| `breakdown : dict<string,int>` | per-coordinate retention at each node
+| `recommendStabilization(factor)` | human advice *attached to the witnessed edge* (now principled, not heuristic)
+| `Stability.idr`: `score ∈ [0,100]` | grade soundness (`calculus.adoc` §8): declared grade never over-claims retention
+|===
+
+The witness is, by the calculus's own statement (§6.2), "the trope-particularity
+analogue of the invariant-path argmin" — the same argmin shape `Stability.idr`
+already reasons about. The verdict thus _subsumes_ the current score: the score is
+recoverable as a projection, but the verdict additionally names the edge to repair.
+
+== Architecture: reference, never vendor
+
+[cols="1,3",options="header"]
+|===
+| Concern | Decision
+
+| Trust boundary | Pin `trope-checker/schemas/trope-ir.schema.json` at `version 0.1`, `profile prevent`. The schema is the contract (mirrors the IR spec's "schema is the trust boundary").
+| Dependency | Depend on the `trope-checker` *binary* (a pure `IR → verdict` function) and the *IR schema* by URL. Do **not** vendor the calculus, the checker, or `haec`.
+| New backend | Add a `trope` lowering target beside the existing codegen backends: Error-Lang AST/VM ops → Trope IR DAG (schema-validated) → `trope-checker` → verdict object → surfaced as Error-Lang diagnostics.
+| Precedent | The same trust-tagged "fold external prover output back into our report" pattern panic-attack uses in `src/aggregate/`.
+| Multi-producer | Sanctioned by `trope-ir.adoc`: "a static analyser for an existing language MAY emit Trope IR for code it did not author." Error-Lang's analyzer is exactly such a producer.
+|===
+
+== O2 — lowering-correctness obligations (ours to discharge)
+
+The trope-checker proves the *composition* of grades is sound. It explicitly does
+**not** prove that an Error-Lang construct lowered to effect `X` _is_ an `X`
+(`calculus.adoc` §8, firewall 2; §10-O2). Those are our proof obligations:
+
+[cols="1,4",options="header"]
+|===
+| ID | Obligation
+
+| *L-Echo* | `OpEchoToResidue` (`VM.res`) semantically _is_ `detach`: the witness becomes unreachable ⇒ `bond=Severed`; output reachability survives ⇒ `fate(quality)=Present`. **Open decision:** is residue's quality `Present`, or `Attenuated(δ)` (only "reachability", not full `y`)? This must be fixed before Phase 1 freezes the lowering.
+| *L-Grade* | Each `stabilityFactor`'s grade is a *faithful over-approximation* of the real loss (grade-soundness direction: never claim more retention than occurs). The current `stabilityImpact` magnitudes are heuristic; for soundness `δ` must be a conservative loss bound.
+| *L-Silent* | The `Conflated` lowering of `GlobalState`/`RaceCondition` is correct only when the merge is genuinely untagged. If a provenance tag is recoverable, we MUST emit `Fused(τ)` instead; emitting `Conflated` for a tractable merge is a false positive.
+| *L-Floor* | The `use_model` floor Error-Lang emits faithfully encodes the program's declared stability requirement (per-function loss signatures, §7 "Declared signatures at the boundaries").
+|===
+
+These mirror, in Error-Lang's setting, the open obligations the calculus states for
+itself (O1–O4) — and they are checkable with the *same* Idris2 discipline already
+used in `src/abi/`.
+
+== Phasing
+
+[cols="1,3",options="header"]
+|===
+| Phase | Work
+
+| *0 (now)* | Shape the AffineScript Echo types (during the ReScript→AffineScript port) so `Echo`/`EchoR`/`echo_to_residue` lower cleanly to `Trope`/`FloatingQuality`/`detach`. This document + cross-references. *No new runtime coupling.*
+| *1* | Implement the `trope` lowering backend for the Echo operations only (the tightest correspondence). Emit schema-valid IR; conformance-test against `trope-checker/tests/conformance/fixtures/`.
+| *2* | Lower `stabilityFactor` → grade and emit a `use_model`; surface the verdict + witness as diagnostics alongside (then in place of) the scalar score.
+| *3* | Discharge L-Echo / L-Grade / L-Silent / L-Floor as Idris2/Agda proofs; CI-gate the lowering.
+|===
+
+== Open questions
+
+* *Profile.* Adopt `prevent` (silent merges rejected at validation — strongest, and
+  on-message for "decomposition must be visible") or `detect` (representable, caught
+  at the verdict)? This design assumes `prevent`.
+* *Residue fidelity* (L-Echo): `Present` vs `Attenuated(δ)` for `echo_to_residue`.
+* *Floor authorship.* Where do use-models come from — a whole-program default, or
+  per-function loss-signature annotations the learner writes?
+* *Coverage* (calculus O1): are all eight `stabilityFactor`s expressible with the
+  six writable effects? The table above is a well-chosen mapping, not yet a theorem.
+
+== See also
+
+* `docs/Echo-Decomposition.adoc` — the three decomposition planes this builds on.
+* `docs/Design-Philosophy.adoc` — consequence amplification and the stability score.
+* `spec/type-system.md` §7 — typing rules and the `[Stab-Erase]` stability debit.
+* `src/abi/Stability.idr` — the existing Idris2 bound proof (verdict-soundness anchor).
+* External (referenced, not vendored):
+  https://github.com/hyperpolymath/trope-checker[trope-checker] (`spec/calculus.adoc`,
+  `spec/trope-ir.adoc`, `schemas/trope-ir.schema.json`),
+  https://github.com/hyperpolymath/trope-particularity-workbench[trope-particularity-workbench]
+  (the nine effects), https://github.com/hyperpolymath/echo-types[echo-types] (shared substrate).

From a3c0df8ba6c0f447bee723a5c26e11b5d5c9a60b Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 23 Jun 2026 20:55:59 +0000
Subject: [PATCH 3/5] 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
---
 docs/Trope-Particularity-Integration.adoc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/Trope-Particularity-Integration.adoc b/docs/Trope-Particularity-Integration.adoc
index 017125d..ea4ad12 100644
--- a/docs/Trope-Particularity-Integration.adoc
+++ b/docs/Trope-Particularity-Integration.adoc
@@ -55,7 +55,7 @@ Two further alignments make the fit unusually tight:
   `echo_input`, `echo_output` implement witness-retention and irreversible erasure
   — which the calculus names `preserve`, `detach`, and field `project` (§5).
 * **The verification toolchains already overlap.** The trope-checker's core is an
-  Agda reference plus an Idris2 implementation (`trope-checker/src/idris2/Main.idr`);
+  Agda reference plus an Idris2 implementation (the `trope-checker` repo's Idris2 core, `Main.idr`);
   Error-Lang already carries an Idris2 proof of the *scalar* bound
   (`src/abi/Stability.idr`). The integration generalises that proof's target from
   a clamped integer to a checked grade.
@@ -186,7 +186,7 @@ recoverable as a projection, but the verdict additionally names the edge to repa
 | Trust boundary | Pin `trope-checker/schemas/trope-ir.schema.json` at `version 0.1`, `profile prevent`. The schema is the contract (mirrors the IR spec's "schema is the trust boundary").
 | Dependency | Depend on the `trope-checker` *binary* (a pure `IR → verdict` function) and the *IR schema* by URL. Do **not** vendor the calculus, the checker, or `haec`.
 | New backend | Add a `trope` lowering target beside the existing codegen backends: Error-Lang AST/VM ops → Trope IR DAG (schema-validated) → `trope-checker` → verdict object → surfaced as Error-Lang diagnostics.
-| Precedent | The same trust-tagged "fold external prover output back into our report" pattern panic-attack uses in `src/aggregate/`.
+| Precedent | The same trust-tagged "fold external prover output back into our report" pattern the panic-attack repo uses in its `aggregate/` module.
 | Multi-producer | Sanctioned by `trope-ir.adoc`: "a static analyser for an existing language MAY emit Trope IR for code it did not author." Error-Lang's analyzer is exactly such a producer.
 |===
 

From 27571a32c4147ffe850a1fb413dfa6ec249a782f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 23 Jun 2026 21:20:45 +0000
Subject: [PATCH 4/5] =?UTF-8?q?compiler:=20begin=20ReScript->AffineScript?=
 =?UTF-8?q?=20migration=20=E2=80=94=20port=20Types.res?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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/src/Types.affine                 | 235 ++++++++++++++++++++++
 scripts/install-affinescript-toolchain.sh |  45 +++++
 verification/check-affinescript.sh        |  41 ++++
 3 files changed, 321 insertions(+)
 create mode 100644 compiler/src/Types.affine
 create mode 100755 scripts/install-affinescript-toolchain.sh
 create mode 100755 verification/check-affinescript.sh

diff --git a/compiler/src/Types.affine b/compiler/src/Types.affine
new file mode 100644
index 0000000..e9fd954
--- /dev/null
+++ b/compiler/src/Types.affine
@@ -0,0 +1,235 @@
+// SPDX-License-Identifier: MPL-2.0
+// Types.affine — core type definitions for Error-Lang
+// Ported from compiler/src/Types.res. Port conventions:
+//   * ReScript inline-record variants -> positional constructor args.
+//   * array<T> -> [T]; option<T> -> Option<T>; dict<k,v> -> Dict<k,v>; tuples kept.
+//   * Token variants `Float`/`String` renamed `FloatTok`/`StringTok`
+//     (`Float`/`String` are reserved type keywords in AffineScript).
+
+use prelude::*;
+
+struct Position {
+  line: Int,
+  column: Int,
+  offset: Int
+}
+
+struct Location {
+  start: Position,
+  end_: Position,
+  file: String
+}
+
+enum TokenType {
+  // Keywords
+  Main, End, Let, Mutable, Function, Struct, If, Elseif, Else, While, For, In,
+  Break, Continue, Return, And, Or, Not, True, False, Nil, Gutter, Fn,
+  // Types
+  TInt, TFloat, TString, TBool, TArray, TEcho, TEchoR,
+  // Literals
+  Integer(Int),
+  FloatTok(Float),     // ReScript Float(float)
+  StringTok(String),   // ReScript String(string)
+  Identifier(String),
+  // Operators
+  Plus, Minus, Star, Slash, Percent, EqualEqual, BangEqual, Less, Greater,
+  LessEqual, GreaterEqual, Ampersand, Pipe, Caret, Tilde, LessLess, GreaterGreater,
+  Equal, Arrow, Question, Colon,
+  // Delimiters
+  LParen, RParen, LBracket, RBracket, LBrace, RBrace, Comma, Dot,
+  // Special
+  Newline, EOF, Error(String)
+}
+
+struct Token {
+  type_: TokenType,
+  lexeme: String,
+  loc: Location
+}
+
+// ============================================
+// AST
+// ============================================
+
+enum Expr {
+  IntLit(Int, Location),
+  FloatLit(Float, Location),
+  StringLit(String, Location),
+  BoolLit(Bool, Location),
+  NilLit(Location),
+  Ident(String, Location),
+  Array([Expr], Location),
+  Binary(Expr, BinaryOp, Expr, Location),
+  Unary(UnaryOp, Expr, Location),
+  Call(Expr, [Expr], Location),
+  Index(Expr, Expr, Location),
+  Member(Expr, String, Location),
+  Ternary(Expr, Expr, Expr, Location),
+  Lambda([Param], Option<TypeExpr>, LambdaBody, Location)
+}
+
+enum BinaryOp {
+  Add, Sub, Mul, Div, Mod,
+  Eq, Neq, Lt, Gt, Lte, Gte,
+  BAnd, BOr, BXor, Shl, Shr,
+  LAnd, LOr
+}
+
+enum UnaryOp { Neg, LNot, BNot }
+
+struct Param {
+  name: String,
+  type_: Option<TypeExpr>,
+  loc: Location
+}
+
+enum TypeExpr {
+  TyInt,
+  TyFloat,
+  TyString,
+  TyBool,
+  TyArray(TypeExpr),
+  // Echo types (Trope-IR-ready, see docs/Trope-Particularity-Integration.adoc):
+  //   TyEcho        ~ Trope[Phi]        (retained witness)
+  //   TyEchoResidue ~ FloatingQuality   (witness severed)
+  TyEcho(Option<TypeExpr>, Option<TypeExpr>),
+  TyEchoResidue(Option<TypeExpr>, Option<TypeExpr>),
+  TyIdent(String)
+}
+
+enum LambdaBody {
+  LambdaExpr(Expr),
+  LambdaBlock([Stmt])
+}
+
+enum Stmt {
+  // inline records -> positional: (mutable_, name, type_, value, loc)
+  LetStmt(Bool, String, Option<TypeExpr>, Expr, Location),
+  // (target, value, loc)
+  AssignStmt(Expr, Expr, Location),
+  // (cond, then_, elseifs, else_, loc)
+  IfStmt(Expr, [Stmt], [(Expr, [Stmt])], Option<[Stmt]>, Location),
+  // (cond, body, loc)
+  WhileStmt(Expr, [Stmt], Location),
+  // (var, iter, body, loc)
+  ForStmt(String, Expr, [Stmt], Location),
+  // (value, loc)
+  ReturnStmt(Option<Expr>, Location),
+  BreakStmt(Location),
+  ContinueStmt(Location),
+  // (println, args, loc)
+  PrintStmt(Bool, [Expr], Location),
+  // (tokens, recovered, loc)
+  GutterBlock([Token], Bool, Location),
+  ExprStmt(Expr)
+}
+
+enum Decl {
+  // (name, params, returnType, body, loc)
+  FunctionDecl(String, [Param], Option<TypeExpr>, [Stmt], Location),
+  // (name, fields, loc)
+  StructDecl(String, [(String, TypeExpr)], Location),
+  // (body, loc)
+  MainBlock([Stmt], Location),
+  StmtDecl(Stmt)
+}
+
+struct Program {
+  declarations: [Decl],
+  loc: Location
+}
+
+// ============================================
+// Errors
+// ============================================
+
+enum ErrorCode {
+  E0001, E0002, E0003, E0004, E0005, E0006, E0007, E0008, E0009, E0010
+}
+
+struct Diagnostic {
+  code: ErrorCode,
+  message: String,
+  loc: Location,
+  runNumber: Int,
+  hint: Option<String>
+}
+
+// ============================================
+// Runtime state & stability
+// ============================================
+
+enum StabilityFactor {
+  MutableState(Int, Int),       // mutations, readers
+  TypeInstability(Int),         // reassignments
+  NullPropagation(Int),         // depth
+  GlobalState(Int, Int),        // mutations, dependencies
+  UnhandledError(Int),          // paths
+  AlgorithmComplexity(Float),   // time_ms
+  MemoryLeak(Int),              // bytes
+  RaceCondition(Int)            // conflicts
+}
+
+struct StabilityReport {
+  score: Int,
+  factors: [StabilityFactor],
+  breakdown: Dict<String, Int>,
+  recommendations: [String]
+}
+
+struct RuntimeState {
+  runCounter: Int,
+  stabilityScore: Int,
+  lastError: Option<ErrorCode>,
+  seed: Int,
+  stabilityFactors: [StabilityFactor],
+  discoveredRules: [String],
+  historicalRuns: [Int]
+}
+
+fn make_default_state() -> RuntimeState {
+  #{
+    runCounter: 0,
+    stabilityScore: 100,
+    lastError: None,
+    seed: 0,
+    stabilityFactors: [],
+    discoveredRules: [],
+    historicalRuns: []
+  }
+}
+
+// Stability impact (non-positive), mirrors Types.res `stabilityImpact`.
+fn stability_impact(factor: StabilityFactor) -> Int {
+  match factor {
+    MutableState(mutations, readers) => -(10 * mutations + 5 * readers),
+    TypeInstability(reassignments) => -(15 * reassignments),
+    NullPropagation(depth) => -(20 * depth),
+    GlobalState(mutations, dependencies) => -(30 * mutations + 5 * dependencies),
+    UnhandledError(paths) => -(25 * paths),
+    AlgorithmComplexity(time_ms) => -trunc(time_ms / 10.0),
+    MemoryLeak(bytes) => -(10 * (bytes / 1024)),
+    RaceCondition(conflicts) => -(40 * conflicts)
+  }
+}
+
+// mirrors Types.res `calculateStability`: max(0, 100 + sum(impacts))
+fn calculate_stability(factors: [StabilityFactor]) -> Int {
+  let penalties = fold(factors, 0, |acc, x| acc + stability_impact(x));
+  max(0, 100 + penalties)
+}
+
+fn error_code_to_string(code: ErrorCode) -> String {
+  match code {
+    E0001 => "E0001",
+    E0002 => "E0002",
+    E0003 => "E0003",
+    E0004 => "E0004",
+    E0005 => "E0005",
+    E0006 => "E0006",
+    E0007 => "E0007",
+    E0008 => "E0008",
+    E0009 => "E0009",
+    E0010 => "E0010"
+  }
+}
diff --git a/scripts/install-affinescript-toolchain.sh b/scripts/install-affinescript-toolchain.sh
new file mode 100755
index 0000000..6c3a863
--- /dev/null
+++ b/scripts/install-affinescript-toolchain.sh
@@ -0,0 +1,45 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# install-affinescript-toolchain.sh — build & install the AffineScript compiler
+# (hyperpolymath/affinescript, the OCaml/dune compiler) so error-lang's `.affine`
+# sources — which replace the legacy ReScript per the Hyperpolymath language
+# policy — can be typechecked and compiled.
+#
+# Why build from distro OCaml packages instead of opam: some CI/network policies
+# block opam.ocaml.org. Every dependency below is available from the Debian/Ubuntu
+# archive at a version satisfying affinescript's dune-project constraints
+# (notably ocaml-dune 3.14 == `(lang dune 3.14)`).
+#
+# Network note: this clones github.com/hyperpolymath/affinescript directly; run it
+# where GitHub is reachable (a normal CI runner or dev box).
+set -euo pipefail
+
+AFFINE_REPO="${AFFINE_REPO:-https://github.com/hyperpolymath/affinescript}"
+AFFINE_SRC="${AFFINE_SRC:-${TMPDIR:-/tmp}/affinescript}"
+PREFIX="${PREFIX:-/usr/local}"
+SUDO="$(command -v sudo || true)"
+
+# 1. OCaml toolchain + AffineScript build dependencies.
+$SUDO apt-get update
+$SUDO apt-get install -y \
+  ocaml-dune menhir libmenhir-ocaml-dev libsedlex-ocaml-dev \
+  libppx-deriving-ocaml-dev libppx-sexp-conv-ocaml-dev libsexplib0-ocaml-dev \
+  libfmt-ocaml-dev libcmdliner-ocaml-dev libyojson-ocaml-dev \
+  libppxlib-ocaml-dev libjs-of-ocaml-dev
+
+# 2. Fetch + build the compiler binary.
+[ -d "$AFFINE_SRC/.git" ] || git clone --depth 1 "$AFFINE_REPO" "$AFFINE_SRC"
+( cd "$AFFINE_SRC" && dune build bin/main.exe )
+
+# 3. Install the binary + stdlib. The module loader discovers the stdlib at
+#    <binary_dir>/../share/affinescript/stdlib, so this needs no env var.
+$SUDO install -m755 "$AFFINE_SRC/_build/default/bin/main.exe" "$PREFIX/bin/affinescript"
+$SUDO mkdir -p "$PREFIX/share/affinescript"
+$SUDO rm -rf "$PREFIX/share/affinescript/stdlib"
+$SUDO cp -r "$AFFINE_SRC/stdlib" "$PREFIX/share/affinescript/stdlib"
+
+echo "Installed: $(command -v affinescript)"
+affinescript check "$AFFINE_SRC/examples/hello.affine" || true
+echo "AffineScript toolchain installed under $PREFIX."
diff --git a/verification/check-affinescript.sh b/verification/check-affinescript.sh
new file mode 100755
index 0000000..7644980
--- /dev/null
+++ b/verification/check-affinescript.sh
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-affinescript.sh — typecheck every ported `.affine` compiler source with
+# the AffineScript compiler. Companion to verification/check-proofs.sh.
+# Requires `affinescript` on PATH (see scripts/install-affinescript-toolchain.sh).
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+if ! command -v affinescript >/dev/null 2>&1; then
+  echo "affinescript not found — run scripts/install-affinescript-toolchain.sh" >&2
+  exit 127
+fi
+
+shopt -s nullglob
+sources=(compiler/src/*.affine)
+if [ ${#sources[@]} -eq 0 ]; then
+  echo "no .affine sources yet (ReScript->AffineScript migration in progress)."
+  exit 0
+fi
+
+fail=0
+for f in "${sources[@]}"; do
+  printf 'checking %-28s ... ' "$(basename "$f")"
+  if affinescript check "$f" >/tmp/as_check.out 2>&1; then
+    echo ok
+  else
+    echo FAIL
+    cat /tmp/as_check.out
+    fail=1
+  fi
+done
+
+if [ "$fail" -eq 0 ]; then
+  echo "all .affine sources check."
+else
+  echo "affinescript check failures." >&2
+  exit 1
+fi

From 8691fc691a85fc4e8eb98695c32e9a46eccc55bd Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 23 Jun 2026 22:15:31 +0000
Subject: [PATCH 5/5] 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/src/Types.affine                     |  50 +++---
 patches/README.adoc                           |  44 ++++++
 .../affinescript-module-struct-fields.patch   | 142 ++++++++++++++++++
 scripts/install-affinescript-toolchain.sh     |  14 +-
 verification/check-affinescript.sh            |   8 +-
 5 files changed, 232 insertions(+), 26 deletions(-)
 create mode 100644 patches/README.adoc
 create mode 100644 patches/affinescript-module-struct-fields.patch

diff --git a/compiler/src/Types.affine b/compiler/src/Types.affine
index e9fd954..75f41c2 100644
--- a/compiler/src/Types.affine
+++ b/compiler/src/Types.affine
@@ -5,22 +5,28 @@
 //   * array<T> -> [T]; option<T> -> Option<T>; dict<k,v> -> Dict<k,v>; tuples kept.
 //   * Token variants `Float`/`String` renamed `FloatTok`/`StringTok`
 //     (`Float`/`String` are reserved type keywords in AffineScript).
+//
+// This is the `Types` module; sibling compiler modules `use Types::{...}`.
+// Cross-module struct field access requires the affinescript module-resolver
+// fix in patches/affinescript-module-struct-fields.patch.
+
+module Types;
 
 use prelude::*;
 
-struct Position {
+pub struct Position {
   line: Int,
   column: Int,
   offset: Int
 }
 
-struct Location {
+pub struct Location {
   start: Position,
   end_: Position,
   file: String
 }
 
-enum TokenType {
+pub enum TokenType {
   // Keywords
   Main, End, Let, Mutable, Function, Struct, If, Elseif, Else, While, For, In,
   Break, Continue, Return, And, Or, Not, True, False, Nil, Gutter, Fn,
@@ -41,7 +47,7 @@ enum TokenType {
   Newline, EOF, Error(String)
 }
 
-struct Token {
+pub struct Token {
   type_: TokenType,
   lexeme: String,
   loc: Location
@@ -51,7 +57,7 @@ struct Token {
 // AST
 // ============================================
 
-enum Expr {
+pub enum Expr {
   IntLit(Int, Location),
   FloatLit(Float, Location),
   StringLit(String, Location),
@@ -68,22 +74,22 @@ enum Expr {
   Lambda([Param], Option<TypeExpr>, LambdaBody, Location)
 }
 
-enum BinaryOp {
+pub enum BinaryOp {
   Add, Sub, Mul, Div, Mod,
   Eq, Neq, Lt, Gt, Lte, Gte,
   BAnd, BOr, BXor, Shl, Shr,
   LAnd, LOr
 }
 
-enum UnaryOp { Neg, LNot, BNot }
+pub enum UnaryOp { Neg, LNot, BNot }
 
-struct Param {
+pub struct Param {
   name: String,
   type_: Option<TypeExpr>,
   loc: Location
 }
 
-enum TypeExpr {
+pub enum TypeExpr {
   TyInt,
   TyFloat,
   TyString,
@@ -97,12 +103,12 @@ enum TypeExpr {
   TyIdent(String)
 }
 
-enum LambdaBody {
+pub enum LambdaBody {
   LambdaExpr(Expr),
   LambdaBlock([Stmt])
 }
 
-enum Stmt {
+pub enum Stmt {
   // inline records -> positional: (mutable_, name, type_, value, loc)
   LetStmt(Bool, String, Option<TypeExpr>, Expr, Location),
   // (target, value, loc)
@@ -124,7 +130,7 @@ enum Stmt {
   ExprStmt(Expr)
 }
 
-enum Decl {
+pub enum Decl {
   // (name, params, returnType, body, loc)
   FunctionDecl(String, [Param], Option<TypeExpr>, [Stmt], Location),
   // (name, fields, loc)
@@ -134,7 +140,7 @@ enum Decl {
   StmtDecl(Stmt)
 }
 
-struct Program {
+pub struct Program {
   declarations: [Decl],
   loc: Location
 }
@@ -143,11 +149,11 @@ struct Program {
 // Errors
 // ============================================
 
-enum ErrorCode {
+pub enum ErrorCode {
   E0001, E0002, E0003, E0004, E0005, E0006, E0007, E0008, E0009, E0010
 }
 
-struct Diagnostic {
+pub struct Diagnostic {
   code: ErrorCode,
   message: String,
   loc: Location,
@@ -159,7 +165,7 @@ struct Diagnostic {
 // Runtime state & stability
 // ============================================
 
-enum StabilityFactor {
+pub enum StabilityFactor {
   MutableState(Int, Int),       // mutations, readers
   TypeInstability(Int),         // reassignments
   NullPropagation(Int),         // depth
@@ -170,14 +176,14 @@ enum StabilityFactor {
   RaceCondition(Int)            // conflicts
 }
 
-struct StabilityReport {
+pub struct StabilityReport {
   score: Int,
   factors: [StabilityFactor],
   breakdown: Dict<String, Int>,
   recommendations: [String]
 }
 
-struct RuntimeState {
+pub struct RuntimeState {
   runCounter: Int,
   stabilityScore: Int,
   lastError: Option<ErrorCode>,
@@ -187,7 +193,7 @@ struct RuntimeState {
   historicalRuns: [Int]
 }
 
-fn make_default_state() -> RuntimeState {
+pub fn make_default_state() -> RuntimeState {
   #{
     runCounter: 0,
     stabilityScore: 100,
@@ -200,7 +206,7 @@ fn make_default_state() -> RuntimeState {
 }
 
 // Stability impact (non-positive), mirrors Types.res `stabilityImpact`.
-fn stability_impact(factor: StabilityFactor) -> Int {
+pub fn stability_impact(factor: StabilityFactor) -> Int {
   match factor {
     MutableState(mutations, readers) => -(10 * mutations + 5 * readers),
     TypeInstability(reassignments) => -(15 * reassignments),
@@ -214,12 +220,12 @@ fn stability_impact(factor: StabilityFactor) -> Int {
 }
 
 // mirrors Types.res `calculateStability`: max(0, 100 + sum(impacts))
-fn calculate_stability(factors: [StabilityFactor]) -> Int {
+pub fn calculate_stability(factors: [StabilityFactor]) -> Int {
   let penalties = fold(factors, 0, |acc, x| acc + stability_impact(x));
   max(0, 100 + penalties)
 }
 
-fn error_code_to_string(code: ErrorCode) -> String {
+pub fn error_code_to_string(code: ErrorCode) -> String {
   match code {
     E0001 => "E0001",
     E0002 => "E0002",
diff --git a/patches/README.adoc b/patches/README.adoc
new file mode 100644
index 0000000..f5711c1
--- /dev/null
+++ b/patches/README.adoc
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= AffineScript toolchain patches
+:toc:
+
+Patches applied to a fresh `hyperpolymath/affinescript` checkout by
+`scripts/install-affinescript-toolchain.sh` before building the compiler, to
+support the ReScript -> AffineScript migration. Each is a stop-gap pending
+upstream; drop it from the install script once upstreamed.
+
+== affinescript-module-struct-fields.patch
+
+*Problem.* AffineScript's module resolver exported imported *enum* constructors
+but dropped imported *struct/alias* type definitions: `lib/resolve.ml` registered
+`TyEnum` variant constructors for imported modules but had a bare
+`| TyAlias _ | TyStruct _ | TyExtern -> ()`. Field access on an imported struct
+therefore failed with `Field 'x' not found in type T` — the named type stayed an
+opaque `TCon` and never expanded to its `TRecord`.
+
+This blocked a per-module `.res -> .affine` port: the shared AST in
+`compiler/src/Types.affine` (`Location`, `Token`, `Position`, ...) is
+field-accessed by every other compiler module.
+
+*Fix.* Thread imported modules' `type_env` (struct/alias/enum type definitions)
+and `constructor_env` into the importing module's type-check context, mirroring
+the existing `name_types` (scheme) threading that already made enums cross:
+
+* `lib/typecheck.ml` — `check_program` gains `?import_type_env` /
+  `?import_constructor_env`, seeding `ctx.type_env` / `ctx.constructor_env`.
+* `lib/resolve.ml` — a new `import_type_defs` copies a resolved module's
+  `type_env` / `constructor_env` into the destination context, called from all
+  three import forms (`use M;`, `use M::{...}`, `use M::*`); the imported-module
+  check site passes the new params.
+* `bin/main.ml` — the `check` / `compile` / `eval` entry points pass the threaded
+  `type_env` / `constructor_env` to `check_program`.
+
+*Verification.* A module importing a struct and accessing its (nested) fields,
+constructing it, and matching on an imported enum field now type-checks; existing
+stdlib cross-module imports (`http_fetch`, `option`, `io`) still pass.
+
+*Upstream.* This belongs in `hyperpolymath/affinescript` — it fixes any multi-file
+AffineScript program, not only error-lang. It could not be pushed from the
+migration session (affinescript was outside the session's repo scope); upstream
+when convenient, then delete this patch and its hook in the install script.
diff --git a/patches/affinescript-module-struct-fields.patch b/patches/affinescript-module-struct-fields.patch
new file mode 100644
index 0000000..54aae35
--- /dev/null
+++ b/patches/affinescript-module-struct-fields.patch
@@ -0,0 +1,142 @@
+diff --git a/bin/main.ml b/bin/main.ml
+index 8230ab2..b772a3c 100644
+--- a/bin/main.ml
++++ b/bin/main.ml
+@@ -195,6 +195,8 @@ let check_file face json path =
+         resolve_refs := List.rev resolve_ctx.references;
+         (match Affinescript.Typecheck.check_program
+                  ~import_types:type_ctx.Affinescript.Typecheck.name_types
++                 ~import_type_env:type_ctx.Affinescript.Typecheck.type_env
++                 ~import_constructor_env:type_ctx.Affinescript.Typecheck.constructor_env
+                  resolve_ctx.symbols prog with
+         | Error e ->
+           add (Affinescript.Json_output.of_type_error e)
+@@ -242,6 +244,8 @@ let check_file face json path =
+       | Ok (resolve_ctx, type_ctx) ->
+         (match Affinescript.Typecheck.check_program
+                  ~import_types:type_ctx.Affinescript.Typecheck.name_types
++                 ~import_type_env:type_ctx.Affinescript.Typecheck.type_env
++                 ~import_constructor_env:type_ctx.Affinescript.Typecheck.constructor_env
+                  resolve_ctx.symbols prog with
+         | Error e ->
+           Format.eprintf "@[<v>%s@]@."
+@@ -505,6 +509,8 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc
+       | Ok (resolve_ctx, import_type_ctx) ->
+         (match Affinescript.Typecheck.check_program
+                  ~import_types:import_type_ctx.Affinescript.Typecheck.name_types
++                 ~import_type_env:import_type_ctx.Affinescript.Typecheck.type_env
++                 ~import_constructor_env:import_type_ctx.Affinescript.Typecheck.constructor_env
+                  resolve_ctx.symbols prog with
+         | Error e ->
+           add (Affinescript.Json_output.of_type_error e)
+@@ -732,6 +738,8 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc
+       | Ok (resolve_ctx, import_type_ctx) ->
+         (match Affinescript.Typecheck.check_program
+                  ~import_types:import_type_ctx.Affinescript.Typecheck.name_types
++                 ~import_type_env:import_type_ctx.Affinescript.Typecheck.type_env
++                 ~import_constructor_env:import_type_ctx.Affinescript.Typecheck.constructor_env
+                  resolve_ctx.symbols prog with
+         | Error e ->
+           Format.eprintf "@[<v>%s@]@."
+diff --git a/lib/resolve.ml b/lib/resolve.ml
+index 65a6b48..65a9206 100644
+--- a/lib/resolve.ml
++++ b/lib/resolve.ml
+@@ -654,6 +654,20 @@ let import_specific_items
+       Error (UndefinedVariable item.ii_name, item.ii_name.span)
+   ) (Ok ()) items
+ 
++(** Thread imported struct/alias/enum type definitions and value constructors
++    from a resolved source module into the destination type-check context, so
++    that field access on an imported struct resolves (companion to the scheme
++    imports above — a struct needs its TRecord definition, not just a
++    name_types scheme). *)
++let import_type_defs
++    (dest : Typecheck.context) (source : Typecheck.context) : unit =
++  Hashtbl.iter (fun name ty ->
++    Hashtbl.replace dest.Typecheck.type_env name ty
++  ) source.Typecheck.type_env;
++  Hashtbl.iter (fun name ty ->
++    Hashtbl.replace dest.Typecheck.constructor_env name ty
++  ) source.Typecheck.constructor_env
++
+ (** Resolve imports in a program using module loader *)
+ let rec resolve_and_typecheck_module
+     (loader : Module_loader.t)
+@@ -698,7 +712,10 @@ let rec resolve_and_typecheck_module
+      imported modules must check the same way top-level programs do.) *)
+   match
+     Typecheck.check_program
+-      ~import_types:type_ctx.Typecheck.name_types symbols prog
++      ~import_types:type_ctx.Typecheck.name_types
++      ~import_type_env:type_ctx.Typecheck.type_env
++      ~import_constructor_env:type_ctx.Typecheck.constructor_env
++      symbols prog
+   with
+   | Ok final_ctx -> Ok (symbols, final_ctx)
+   | Error type_err ->
+@@ -729,6 +746,7 @@ and resolve_imports_with_loader
+                 mod_type_ctx.Typecheck.var_types
+                 mod_type_ctx.Typecheck.name_types
+                 alias_str;
++              import_type_defs type_ctx mod_type_ctx;
+               Ok ()
+             | Error e -> Error e
+           end
+@@ -747,13 +765,15 @@ and resolve_imports_with_loader
+           (* Resolve and type-check the module *)
+           begin match resolve_and_typecheck_module loader loaded_mod with
+             | Ok (mod_symbols, mod_type_ctx) ->
+-              import_specific_items ctx.symbols
++              let* () = import_specific_items ctx.symbols
+                 type_ctx.Typecheck.var_types
+                 type_ctx.Typecheck.name_types
+                 mod_symbols
+                 mod_type_ctx.Typecheck.var_types
+                 mod_type_ctx.Typecheck.name_types
+-                items
++                items in
++              import_type_defs type_ctx mod_type_ctx;
++              Ok ()
+             | Error e -> Error e
+           end
+         | Error (Module_loader.ModuleNotFound _) ->
+@@ -785,6 +805,7 @@ and resolve_imports_with_loader
+                        sym)
+                 | _ -> ()
+               ) mod_symbols.all_symbols;
++              import_type_defs type_ctx mod_type_ctx;
+               Ok ()
+             | Error e -> Error e
+           end
+diff --git a/lib/typecheck.ml b/lib/typecheck.ml
+index e38e302..4390c71 100644
+--- a/lib/typecheck.ml
++++ b/lib/typecheck.ml
+@@ -2401,6 +2401,8 @@ let populate_call_effects (ctx : context) (prog : Ast.program) : unit =
+   Effect_sites.set_async_by_ord async_tbl
+ 
+ let check_program ?(import_types : (string, scheme) Hashtbl.t option)
++    ?(import_type_env : (string, ty) Hashtbl.t option)
++    ?(import_constructor_env : (string, ty) Hashtbl.t option)
+     (symbols : Symbol.t) (prog : Ast.program)
+     : (context, type_error) Result.t =
+   try
+@@ -2423,6 +2425,17 @@ let check_program ?(import_types : (string, scheme) Hashtbl.t option)
+   Option.iter (fun tbl ->
+     Hashtbl.iter (fun name sc -> Hashtbl.replace ctx.name_types name sc) tbl
+   ) import_types;
++  (* Thread imported struct/alias/enum type definitions (type_env) and value
++     constructors (constructor_env) so field access on an imported struct
++     resolves: enums already cross via name_types schemes, but a struct's
++     TRecord definition must be present for a named param type to expand to
++     its fields (otherwise it stays an opaque TCon -> FieldNotFound). *)
++  Option.iter (fun tbl ->
++    Hashtbl.iter (fun name ty -> Hashtbl.replace ctx.type_env name ty) tbl
++  ) import_type_env;
++  Option.iter (fun tbl ->
++    Hashtbl.iter (fun name ty -> Hashtbl.replace ctx.constructor_env name ty) tbl
++  ) import_constructor_env;
+   (* Forward pass: register all types, effects, traits, impls, and
+      function signatures so that mutually recursive declarations resolve. *)
+   let* () = List.fold_left (fun acc decl ->
diff --git a/scripts/install-affinescript-toolchain.sh b/scripts/install-affinescript-toolchain.sh
index 6c3a863..3b4e694 100755
--- a/scripts/install-affinescript-toolchain.sh
+++ b/scripts/install-affinescript-toolchain.sh
@@ -29,8 +29,20 @@ $SUDO apt-get install -y \
   libfmt-ocaml-dev libcmdliner-ocaml-dev libyojson-ocaml-dev \
   libppxlib-ocaml-dev libjs-of-ocaml-dev
 
-# 2. Fetch + build the compiler binary.
+# 2. Fetch the compiler.
 [ -d "$AFFINE_SRC/.git" ] || git clone --depth 1 "$AFFINE_REPO" "$AFFINE_SRC"
+
+# 2a. Apply the module-resolver fix (export imported struct field definitions so
+#     cross-module struct field access type-checks) until it is upstreamed to
+#     affinescript. See patches/README.adoc. Idempotent: skipped if already applied.
+PATCH="$(cd "$(dirname "$0")/.." && pwd)/patches/affinescript-module-struct-fields.patch"
+if [ -f "$PATCH" ] && git -C "$AFFINE_SRC" apply --check "$PATCH" 2>/dev/null; then
+  git -C "$AFFINE_SRC" apply "$PATCH" && echo "applied $PATCH"
+else
+  echo "module-struct-fields patch: already applied or not applicable — continuing"
+fi
+
+# 3. Build the compiler binary.
 ( cd "$AFFINE_SRC" && dune build bin/main.exe )
 
 # 3. Install the binary + stdlib. The module loader discovers the stdlib at
diff --git a/verification/check-affinescript.sh b/verification/check-affinescript.sh
index 7644980..549602e 100755
--- a/verification/check-affinescript.sh
+++ b/verification/check-affinescript.sh
@@ -7,7 +7,9 @@
 # Requires `affinescript` on PATH (see scripts/install-affinescript-toolchain.sh).
 set -euo pipefail
 
-cd "$(dirname "$0")/.."
+# Check from compiler/src so sibling-module imports (`use Types::{...}`) resolve
+# via the loader's current-dir search.
+cd "$(dirname "$0")/../compiler/src"
 
 if ! command -v affinescript >/dev/null 2>&1; then
   echo "affinescript not found — run scripts/install-affinescript-toolchain.sh" >&2
@@ -15,7 +17,7 @@ if ! command -v affinescript >/dev/null 2>&1; then
 fi
 
 shopt -s nullglob
-sources=(compiler/src/*.affine)
+sources=(*.affine)
 if [ ${#sources[@]} -eq 0 ]; then
   echo "no .affine sources yet (ReScript->AffineScript migration in progress)."
   exit 0
@@ -23,7 +25,7 @@ fi
 
 fail=0
 for f in "${sources[@]}"; do
-  printf 'checking %-28s ... ' "$(basename "$f")"
+  printf 'checking %-28s ... ' "$f"
   if affinescript check "$f" >/tmp/as_check.out 2>&1; then
     echo ok
   else