hyperpolymath · hyperpolymath · Jun 16, 2026 · Jun 16, 2026 · Jun 16, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -25,10 +25,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   invocation (no `--source-dir`, never resolved the `ABI.*` graph) and silently passed
   when the prover was absent (SKIP = exit 0). Now uses the correct invocation and
   fails-on-skip.
-- **`checked_add` doc-comment corrected.** The comment claimed "overflow -> trap" but the body is
-  `a +% b` (wrapping); the GAP-1b metamorphic gate surfaced the contradiction. The comment now
-  states the wrapping behaviour accurately (the trapping-overflow demo is `crash_overflow`); the
-  export name is unchanged.
+- **`checked_add` made genuinely checked.** The export was a wrapping `a +% b` despite its name
+  (the GAP-1b metamorphic gate surfaced the misnomer). It is now a real checked add: overflow
+  TRAPS (`@addWithOverflow` + `unreachable` → WASM trap → `{:error, _}`, BEAM survives) in all
+  build modes, and a non-overflowing add returns the exact sum. Signature unchanged (the ABI gate
+  stays green); the metamorphic oracle now asserts trap-on-overflow.
 
 ### Changed
 - Project gloss **"Safe NIFs" → "Safer NIFs"** (acronym SNIF unchanged): WASM sandboxing
@@ -51,7 +52,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   Zig export sites; `verification/tools/abi_conformance.py` is now guest-aware (per-guest model
   manifest, multi-value/void parsing). The conformance gate now runs in CI (`proofs.yml`, CI-1).
 - **GAP-1b behaviour gate.** `demo/test/snif_metamorphic_test.exs` — dependency-free metamorphic
-  relations over the scalar kernels (fibonacci recurrence + base cases; `checked_add` `wrap32`
-  oracle + boundary-wrap).
+  relations over the scalar kernels (fibonacci recurrence + base cases; `checked_add`
+  non-overflow = exact-sum / overflow = trap oracle).
 - `AFFIRMATION.adoc` — point-in-time, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION
   trio); SPDX header parked for the owner to add + sign.
diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md
@@ -223,7 +223,7 @@ obligations (e.g. the Coq slot → the WasmCert-Coq isolation theorem).
 | SEC-1-TCB | Discharge **"wasmtime ⊨ FaithfulRuntime"** in-prover: prove that wasmtime + the wasmex embedding actually realise the primitive single-step facts (WASM trap-soundness; trap → `{:error,_}`; host scheduler resumed unchanged) that `SnifIsolation.agda` assumes as its TCB record | SEC | Coq (WasmCert-Coq) | SEC-1's **operational** layer is now PROVEN-MODULO-EXPLICIT-TCB in Agda (`Model.isolation`). This row is the REMAINING half: machine-verifying the runtime-faithfulness assumption that is currently in the theorem's *type* but not proven. |
 | ABI-6 | Buffer/array marshalling round-trip + in-bounds (unblocks "powerful" NIFs; FFT) | ABI | Idris2 | `Compliance.WasmArray*` is only a framework today |
 | ABI-7 | ◐ **Coverage 15 of 20 — buffer_abi DONE 2026-06-16.** `safe_nif` (8, `Foreign.idr`) + `buffer_abi` (7, `BufferAbi.idr`, incl. 3 void returns) are modelled+gated, both in the `abi_conformance.py` guest manifest. **Remaining (ledgered):** `zig/src/burble_fft.zig` (5 — `fft`/`ifft`/… use `(ptr,len)` slice marshalling = ABI-6, and it is not built into any artifact) + the Rust buffer guest | ABI | Idris2 + Python | Buffer guest closed; FFT + Rust pending the multi-language buffer-ABI gate |
-| GAP-1b | ◐ **Behaviour faithfulness — scalar kernels DONE 2026-06-16.** `demo/test/snif_metamorphic_test.exs` (dep-free, 9 metamorphic tests, green on OTP 25). **Load-bearing relations (do not delete):** the `fibonacci` recurrence n=2..40 + base cases (uniquely determines fib), and the `checked_add` `wrap32` oracle over a 100-case boundary-spanning family + the boundary-wrap test. Buffer kernels (`sum_f32` permutation/additivity) are next | TP | metamorphic tests (extraction long-term) | Surfaced a finding: `checked_add` is a **misnomer** — it is wrapping (`a +% b`), not trapping (the trapping demo is `crash_overflow`); doc-comment corrected |
+| GAP-1b | ◐ **Behaviour faithfulness — scalar kernels DONE 2026-06-16.** `demo/test/snif_metamorphic_test.exs` (dep-free, 9 metamorphic tests, green on OTP 25). **Load-bearing relations (do not delete):** the `fibonacci` recurrence n=2..40 + base cases (uniquely determines fib), and the `checked_add` oracle over a 100-case boundary-spanning family (non-overflow = exact sum; overflow = `{:error,_}`) + the boundary-trap test. Buffer kernels (`sum_f32` permutation/additivity) are next | TP | metamorphic tests (extraction long-term) | The gate first surfaced that `checked_add` was a **misnomer** (wrapping `a +% b`); **resolved 2026-06-16 by making it genuinely checked** — overflow traps (`@addWithOverflow` + `unreachable`, all modes) |
 | CI-1 | ✅ **DONE 2026-06-16**: `abi-conformance` now runs as a CI job in `.github/workflows/proofs.yml` (builds both guests, fails on signature drift) | ABI | CI wiring | Making it a *required* status check is the owner-only branch-protection step |
 | MODEL-1 | ◐ **Largely RESOLVED by F2 (SNIFs 2).** The 6 `error_reason` origins are now modelled via `TrapOrigin` (guestFault/hostBudget/preExec) + the `call` front-end in `SnifIsolation`. **Residual:** the `snif_alloc`-returns-0 OOM "third outcome" is not yet modelled as a distinct verdict | TP | Agda | Taxonomy half done; only the OOM-sentinel nuance remains |
 
@@ -235,4 +235,4 @@ obligations (e.g. the Coq slot → the WasmCert-Coq isolation theorem).
 | 2026-04-16 | (Claimed) all 7 proofs complete — see History correction; not actually compiling | Claude Code |
 | 2026-06-16 | All 7 proofs **genuinely** machine-checked (clean-cache); real gate wired; scaffold de-counted; scope honesty added | Claude Opus 4.8 |
 | 2026-06-16 | **SEC-1 (`Model.isolation`) PROVEN-MODULO-EXPLICIT-TCB** in Agda (`SnifIsolation.agda`, `--safe --without-K`, clean-cache exit 0); TCB = `FaithfulRuntime` record hypothesis (primitive single-step facts), non-circularity + non-vacuity confirmed by mutation; WASM-opsem discharge ("wasmtime ⊨ FaithfulRuntime") remains as SEC-1-TCB | Claude Opus 4.8 (1M context) |
-| 2026-06-16 | **SNIFs 2.** SEC-1 sharpened: F1 deniability wired operationally (`run-deniable`/`fault-via-observe` + `SecretWitness`), F2 6-origin `TrapOrigin` taxonomy + `call` front-end (`PreExecWitness`), F5 non-trivial-`Alive` recovery witness (`PartialAlive`) — all mutation-confirmed load-bearing by a 4-skeptic re-audit. ABI-7: `buffer_abi` modelled+gated (`BufferAbi.idr`, 15/20 sites); guest-aware `abi_conformance.py`; CI-1 conformance job added; GAP-1b scalar metamorphic gate (found + corrected the `checked_add` misnomer). | Claude Opus 4.8 (1M context) |
+| 2026-06-16 | **SNIFs 2.** SEC-1 sharpened: F1 deniability wired operationally (`run-deniable`/`fault-via-observe` + `SecretWitness`), F2 6-origin `TrapOrigin` taxonomy + `call` front-end (`PreExecWitness`), F5 non-trivial-`Alive` recovery witness (`PartialAlive`) — all mutation-confirmed load-bearing by a 4-skeptic re-audit. ABI-7: `buffer_abi` modelled+gated (`BufferAbi.idr`, 15/20 sites); guest-aware `abi_conformance.py`; CI-1 conformance job added; GAP-1b scalar metamorphic gate (found the `checked_add` misnomer, then made it genuinely checked — overflow traps). | Claude Opus 4.8 (1M context) |
diff --git a/benches/snif_eval.sh b/benches/snif_eval.sh
@@ -146,12 +146,13 @@ invoke "$SAFE" fibonacci 20; fib_safe="$G_OUT"
 invoke "$FAST" fibonacci 20; fib_fast="$G_OUT"
 add_row "{\"kind\":\"control\",\"fn\":\"fibonacci(20)\",\"safe_out\":$(jstr "$fib_safe"),\"fast_out\":$(jstr "$fib_fast"),\"expect\":\"6765\"}"
 
-# checked_add uses wrapping (+%) by design: i32::MAX + 1 wraps in BOTH modes (NOT
-# a trap) — this is intentional and documented in the source. Record it so the
-# table shows the deliberate wrap rather than implying it is a discrimination row.
-invoke "$SAFE" checked_add 2147483647 1; ca_safe="$G_OUT"
-invoke "$FAST" checked_add 2147483647 1; ca_fast="$G_OUT"
-add_row "{\"kind\":\"control\",\"fn\":\"checked_add(MAX,1)\",\"safe_out\":$(jstr "$ca_safe"),\"fast_out\":$(jstr "$ca_fast"),\"expect\":\"-2147483648 (intentional wrap, both modes)\"}"
+# checked_add is genuinely CHECKED: a non-overflowing add returns the exact sum
+# (this control row uses MAX-1 + 1 = MAX). An OVERFLOWING call (e.g. MAX + 1) FAULTS
+# in BOTH modes (overflow -> `unreachable` -> WASM trap), unlike crash_overflow which
+# only traps under ReleaseSafe — so this is a value row, not a discrimination row.
+invoke "$SAFE" checked_add 2147483646 1; ca_safe="$G_OUT"
+invoke "$FAST" checked_add 2147483646 1; ca_fast="$G_OUT"
+add_row "{\"kind\":\"control\",\"fn\":\"checked_add(MAX-1,1)\",\"safe_out\":$(jstr "$ca_safe"),\"fast_out\":$(jstr "$ca_fast"),\"expect\":\"2147483647 (exact sum; an overflowing add would trap in both modes)\"}"
 
 # ── (4) liveness / DoS guard (language-agnostic) ──────────────────────────────
 # Too little fuel -> deterministic "all fuel consumed" trap; enough -> result.
@@ -279,7 +280,7 @@ fmt_num() { printf "%.3f" "$1" 2>/dev/null || printf "%s" "$1"; }
   printf " %-22s | %-13s | %-13s | %s\n" "fn" "Safe" "Fast" "expect"
   printf " %-22s | %-13s | %-13s | %s\n" "still_alive"        "$sa_safe"  "$sa_fast"  "42"
   printf " %-22s | %-13s | %-13s | %s\n" "fibonacci(20)"      "$fib_safe" "$fib_fast" "6765"
-  printf " %-22s | %-13s | %-13s | %s\n" "checked_add(MAX,1)" "$ca_safe"  "$ca_fast"  "-2147483648 (intentional wrap)"
+  printf " %-22s | %-13s | %-13s | %s\n" "checked_add(MAX-1,1)" "$ca_safe"  "$ca_fast"  "2147483647 (exact sum; overflow traps)"
   echo
   echo " (4) LIVENESS / DoS GUARD  —  fuel (the wasmex-0.14 mechanism)"
   echo " -------------------------------------------------------------------------------------------"

diff --git a/demo/test/snif_metamorphic_test.exs b/demo/test/snif_metamorphic_test.exs
@@ -62,40 +62,36 @@ defmodule SnifMetamorphicTest do
     assert val!("fibonacci", [46]) == 1_836_311_903
   end
 
-  # ── checked_add: a WRAPPING i32 add (`a +% b`, intentional per zig/src/safe_nif.zig) ──
+  # ── checked_add: a genuinely CHECKED i32 add — overflow TRAPS (see zig/src/safe_nif.zig) ──
   #
-  # NOTE: the export name "checked_add" is a MISNOMER in the guest source — it is two's-
-  # complement WRAPPING addition, not a trapping/checked one (the trapping overflow demo is
-  # the separate `crash_overflow`). This gate verifies the kernel's ACTUAL behaviour: the
-  # i32 modular ring. (Finding surfaced by this very gate — see PROOF-STATUS GAP-1b.)
-
-  # Signed-i32 wrap of an arbitrary integer (the +% oracle).
-  defp wrap32(x) do
-    import Bitwise
-    m = band(x, 0xFFFFFFFF)
-    if m >= 0x8000_0000, do: m - 0x1_0000_0000, else: m
-  end
+  # The guest computes a + b via `@addWithOverflow` and hits `unreachable` on overflow, so an
+  # overflowing call FAULTS (-> {:error, _}, BEAM survives) instead of returning a value; a
+  # non-overflowing call returns the exact sum. (History: this export was a wrapping `a +% b`
+  # despite its name — the misnomer this gate originally surfaced — and was then made genuinely
+  # checked, the behaviour the name promises. See PROOF-STATUS GAP-1b.)
+
+  # Does a + b overflow signed i32? (arbitrary-precision host-side oracle.)
+  defp overflows_i32?(a, b), do: a + b > @i32_max or a + b < @i32_min
 
-  test "checked_add METAMORPHIC commutativity: add(a,b) = add(b,a) (incl. boundary)" do
-    pairs = [{1, 2}, {-5, 9}, {1000, 24}, {-7, -8}, {@i32_max, 1}, {@i32_min, -1}]
+  test "checked_add METAMORPHIC commutativity on non-overflowing pairs: add(a,b) = add(b,a)" do
+    pairs = [{1, 2}, {-5, 9}, {1000, 24}, {-7, -8}, {@i32_max - 3, 2}, {@i32_min + 3, -2}]
 
     Enum.each(pairs, fn {a, b} ->
+      refute overflows_i32?(a, b), "test pair (#{a},#{b}) must not overflow"
       assert val!("checked_add", [a, b]) == val!("checked_add", [b, a]),
              "commutativity broken at (#{a},#{b})"
     end)
   end
 
-  test "checked_add METAMORPHIC identity: add(a,0) = a and add(0,a) = a" do
+  test "checked_add METAMORPHIC identity: add(a,0) = a and add(0,a) = a (adding 0 never overflows)" do
     Enum.each([0, 1, -1, 42, -42, @i32_max, @i32_min], fn a ->
       assert val!("checked_add", [a, 0]) == a
       assert val!("checked_add", [0, a]) == a
     end)
   end
 
-  test "checked_add METAMORPHIC associativity EVERYWHERE (modular ring, incl. boundary)" do
-    # Wrapping add is associative for ALL inputs (it is the Z/2^32 ring), unlike a trapping
-    # add — so boundary triples that would trap a checked add must still associate here.
-    triples = [{1, 2, 3}, {-4, 5, -6}, {@i32_max, 1, 1}, {@i32_min, -1, -1}, {@i32_max, @i32_max, 2}]
+  test "checked_add METAMORPHIC associativity where no intermediate overflows" do
+    triples = [{1, 2, 3}, {-4, 5, -6}, {100, 200, 300}, {-1, -1, -1}]
 
     Enum.each(triples, fn {a, b, c} ->
       left = val!("checked_add", [val!("checked_add", [a, b]), c])
@@ -104,21 +100,29 @@ defmodule SnifMetamorphicTest do
     end)
   end
 
-  test "checked_add WRAPS at the i32 boundary (the defining +% behaviour, vs a trapping add)" do
-    # i32_max + 1 wraps to i32_min; i32_min + (-1) wraps to i32_max — a TRUE value, not {:error}.
-    assert val!("checked_add", [@i32_max, 1]) == @i32_min
-    assert val!("checked_add", [@i32_min, -1]) == @i32_max
-    # ...and one short of the boundary does not wrap.
+  test "checked_add is CHECKED: overflow at the boundary TRAPS (BEAM survives); just-below does not" do
+    # The defining behaviour: i32_max + 1 and i32_min + (-1) FAULT, they do not wrap.
+    assert {:error, _} = Loader.call(@safe, "checked_add", [@i32_max, 1])
+    assert {:error, _} = Loader.call(@safe, "checked_add", [@i32_min, -1])
+    assert {:error, _} = Loader.call(@safe, "checked_add", [@i32_max, @i32_max])
+    # ...one short of the boundary is fine (so it is not "always traps").
     assert val!("checked_add", [@i32_max - 1, 1]) == @i32_max
     assert val!("checked_add", [@i32_min + 1, -1]) == @i32_min
+    # ...and the boundary trap did not take the BEAM with it.
+    assert val!("still_alive", []) == 42
   end
 
-  test "checked_add ORACLE: add(a,b) = wrap32(a+b) across a boundary-spanning family" do
+  test "checked_add ORACLE: non-overflow = exact sum; overflow = {:error,_}, over a boundary family" do
     family = [-3, -1, 0, 1, 3, @i32_max - 1, @i32_max, @i32_min, @i32_min + 1, 1_000_000_000]
 
     for a <- family, b <- family do
-      assert val!("checked_add", [a, b]) == wrap32(a + b),
-             "modular mismatch at (#{a},#{b})"
+      if overflows_i32?(a, b) do
+        assert {:error, _} = Loader.call(@safe, "checked_add", [a, b]),
+               "expected a trap on overflow at (#{a},#{b})"
+      else
+        assert val!("checked_add", [a, b]) == a + b,
+               "expected the exact sum at (#{a},#{b})"
+      end
     end
   end
 end
diff --git a/zig/src/safe_nif.zig b/zig/src/safe_nif.zig
@@ -49,13 +49,17 @@ export fn fibonacci(n: i32) i64 {
     return b;
 }
 
-/// Two's-complement WRAPPING i32 addition (`a +% b`). NOTE: despite the historical name
-/// `checked_add`, this does NOT trap on overflow — it wraps (i32_max + 1 = i32_min), in BOTH
-/// ReleaseSafe and ReleaseFast (`+%` is defined wrapping, not UB, so the build mode is irrelevant).
-/// The trapping-overflow demo is `crash_overflow`. Behaviour pinned by the GAP-1b metamorphic
-/// `wrap32` oracle in `demo/test/snif_metamorphic_test.exs`.
+/// Genuinely CHECKED i32 addition (the name now matches the behaviour). On overflow the guest
+/// TRAPS: `@addWithOverflow` computes the result + an overflow bit with no UB, and on overflow we
+/// hit `unreachable`, which in this wasm32-freestanding target emits the WASM `unreachable`
+/// instruction and traps in ALL build modes (-> wasmex `{:error, _}`, BEAM survives) — like
+/// `crash_unreachable`, and unlike `crash_overflow` which only traps under ReleaseSafe. With no
+/// overflow it returns the exact sum. Behaviour pinned by the GAP-1b metamorphic boundary-trap
+/// oracle in `demo/test/snif_metamorphic_test.exs`.
 export fn checked_add(a: i32, b: i32) i32 {
-    return a +% b; // wrapping add — intentional; see the doc-comment above
+    const r = @addWithOverflow(a, b);
+    if (r[1] != 0) unreachable; // overflow -> WASM unreachable -> trap
+    return r[0];
 }
 
 // --- Crash isolation demos ---