hyperpolymath · hyperpolymath · Jun 23, 2026 · Jun 23, 2026
@@ -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.
@@ -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.
@@ -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)
@@ -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