From 45a7ecc6a05146ecbbd30e1c57c5befcaa4258ea Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 16 Jun 2026 14:51:40 +0100 Subject: [PATCH] =?UTF-8?q?feat(guest):=20make=20checked=5Fadd=20genuinely?= =?UTF-8?q?=20checked=20=E2=80=94=20overflow=20traps=20(was=20a=20wrapping?= =?UTF-8?q?=20misnomer)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit checked_add was a wrapping a +% b despite its name (the GAP-1b metamorphic gate surfaced the misnomer). Now a real checked add: @addWithOverflow + unreachable -> WASM trap on overflow (all build modes, like crash_unreachable) -> wasmex {:error,_}, BEAM survives; no-overflow returns the exact sum. Signature unchanged (ABI gate still 15/15). Flip the metamorphic oracle from the wrap32 ring to non-overflow=exact-sum / overflow=trap; fix the stale 'intentional wrap' bench row + comments; reconcile CHANGELOG + PROOF-STATUS GAP-1b. AFFIRMATION left untouched (frozen at a82bb31, where it was genuinely wrapping). Co-Authored-By: Claude Opus 4.8 (1M context) --- CHANGELOG.md | 13 ++++--- PROOF-STATUS.md | 4 +- benches/snif_eval.sh | 15 ++++---- demo/test/snif_metamorphic_test.exs | 58 +++++++++++++++-------------- zig/src/safe_nif.zig | 16 +++++--- 5 files changed, 58 insertions(+), 48 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e33168b..78f814f 100644 --- 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 index a605d97..f843e1f 100644 --- 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 index a9ad45c..58b3dd7 100644 --- 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 index a4517a3..f695d20 100644 --- 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 index 4c55b24..d3385b6 100644 --- 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 ---