FEAT-048 (v3.0): mechanized i32.add soundness vs official wrapping semantics (REQ-002, G-005)#87
Merged
Conversation
…mantics (REQ-002, G-005) Closes the stated-but-unproven REQ-002 gap: Soundness.v proved scry's interval add sound over UNBOUNDED Z (the no-wrap core, ⊤ otherwise), but not against the OFFICIAL Wasm i32.add — two's-complement wraparound mod 2^32. proofs/rocq/WrapAdd.v models the official wrapping semantics directly (`wrap z = (z + 2^31) mod 2^32 - 2^31` — the same function WasmCert-Coq (TE-004) mechanizes; a literal WasmCert-Coq import is deferred, honestly scoped in the file header) and proves scry's SHIPPED i32_add branch logic sound against it, INCLUDING the wrap case: - `straddles` mirrors the shipped `lo < i32::MIN || hi > i32::MAX` widen-to-⊤ test; - in-range branch: the real sum stays in i32, so `wrap(x+y) = x+y` (wrap_id via Z.mod_small) ∈ the exact interval; - widen branch: ⊤ = all i32 ∋ `wrap(x+y)` (wrap_in_i32 via Z.mod_pos_bound). Admit-free, no axioms. The recorded-false Verus join proof (join_proofs.rs) is already REPAIRED to the semantic γ-equality statement (`γ(join(a,b)) == γ(join(b,a))`, true across all bottom-encodings where structural == was false) and the Verus CI job verifies it — satisfying the other half of the AC. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #87 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
Rocq CI: Z.mod_pos_bound wants '0 < W' but W_pos stated 'W > 0' (not definitionally unified in Rocq 9.0). Also switch the orb-false case analysis to the robust orb_false_iff lemma (with an explicit Bool require) instead of destruct+simpl, which cannot reduce 'orb var true'. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The differentiator — make REQ-002's "proven vs the official Wasm semantics"
literally true for the
i32.addtransfer, including the WRAP case.The gap it closes
Soundness.vproved scry's intervaladdsound over unbounded ℤ (the no-wrapsub-range, ⊤ otherwise). That never established soundness against the official
i32.add— two's-complement wraparound mod 2³².proofs/rocq/WrapAdd.v(admit-free)Models the official wrapping semantics directly —
wrap z = (z + 2³¹) mod 2³² − 2³¹, the same function WasmCert-Coq (TE-004)mechanizes — and proves scry's shipped
i32_addbranch logic sound againstit, including the wrap case:
straddlesmirrors the shippedlo < i32::MIN || hi > i32::MAXwiden-to-⊤ test;wrap(x+y) = x+y(wrap_id) ∈ theexact interval;
wrap(x+y)(wrap_in_i32).Honesty (assessor-facing)
The file header is explicit: this mechanizes the same mathematical semantics
the spec mandates (and WasmCert-Coq formalizes), rather than importing the
WasmCert-Coq development (a literal dependency is deferred/DD-noted). No
overclaim of a WasmCert-Coq import scry doesn't have.
The false Verus join proof
Already repaired:
proofs/verus/join_proofs.rsis the semantic γ-equalitystatement (
γ(join(a,b)) == γ(join(b,a)), true across all bottom-encodings wherestructural
==was false), and the Verus Formal Proofs CI job verifies it —satisfying the other half of the AC.
Falsification statement
scry claims its
i32_addresult contains the official wrappingi32.addof anyoperand-interval values, on every input. FALSE if
WrapAdd.v'si32_add_wrap_sounddoes not hold (it is machine-checked, admit-free).rivet validatePASS. The Rocq Formal Proofs CI job is the authoritative checkfor
WrapAdd.v(local barecoqclacks the Stdlib path the Bazel rocqtoolchain wires;
Pentagon.v/Float.vuse identical imports and are CI-green).🤖 Generated with Claude Code