pulseengine · avrabe · Jul 18, 2026 · Jul 17, 2026
diff --git a/CLAUDE.md b/CLAUDE.md
@@ -89,7 +89,7 @@ cd coq && make proofs
 
 ### Proof Status
 
-See `coq/STATUS.md` for the complete coverage matrix. Current: 585 Qed / 3 Admitted
+See `coq/STATUS.md` for the complete coverage matrix. Current: 591 Qed / 3 Admitted
 (+2 `admit.` tactics) across `coq/Synth/`. The 50 selector-DSL rule theorems
 (`VcrSelRules.v`) are stated directly about the GENERATED model (VCR-ISA-001
 #667: `rule_X := Gen.rule_X`, single source `VcrSelRulesGenerated.v` emitted

diff --git a/artifacts/status.json b/artifacts/status.json
@@ -10,12 +10,12 @@
   "rocq_admit_tactics": 2,
   "rocq_admitted": 3,
   "rocq_axioms": 93,
-  "rocq_qed": 585,
+  "rocq_qed": 591,
   "sail_bridge_qed": 92,
   "sel_dsl_pilot_qed": 7,
   "sel_dsl_rule_qed": 50,
   "sel_dsl_rules": 50,
   "version": "0.49.0",
   "verus_spec_fns": 8,
-  "wasmcert_bridge_qed": 98
+  "wasmcert_bridge_qed": 104
 }
diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml
@@ -478,12 +478,12 @@ artifacts:
       32/64; CompCert 3.16 Integers.v for the underlying ops incl. rol/ror
       217-222). WasmCertBridge.v proves a real-Qed op-level refinement lemma per
       op AND an executor-level lemma routing through the real exec_wasm_instr for
-      every WIRED op. HONEST SCOPE (named, not fabricated): (1) it is still a
-      hand TRANSCRIPTION of the pinned sources, not the real external dep — that
-      stays blocked on the unfree CompCert 3.16 the current nixpkgs pin
-      propagates; (2) the 6 i64 arithmetic/bitwise ops have op-level refinement
-      ONLY, because exec_wasm_instr returns None for their constructors (unwired
-      in the model). The WASM-side analogue of SailArmBridge.v (VCR-ISA-001).
+      EVERY i32 op and ALL 22 i64 ops (the six arithmetic/bitwise ops were wired
+      into exec_wasm_instr in the v0.50 batch — see SWVER-021). HONEST SCOPE
+      (named, not fabricated): it is still a hand TRANSCRIPTION of the pinned
+      sources, not the real external dep — that stays blocked on the unfree
+      CompCert 3.16 the current nixpkgs pin propagates. The WASM-side analogue of
+      SailArmBridge.v (VCR-ISA-001).
     status: implemented
     tags: [vcr-wasm, wasmcert, rocq, refinement, transcription, epic-242]
     links:
@@ -494,8 +494,42 @@ artifacts:
       steps:
         run: "bazel test //coq:verify_proofs"
         coverage: >
-          coq/Synth/WASM/WasmCertBridge.v (98 Qed: i32 + i64 op-level and
+          coq/Synth/WASM/WasmCertBridge.v (104 Qed: i32 + i64 op-level and
           executor-level refinement lemmas + encoding/bit-level/rotate-boundary
           helpers) against coq/Synth/WASM/WasmCertReference.v; re-derived Qed
-          total 585 CI-gated by scripts/claim_check.py (claims.yaml
+          total 591 CI-gated by scripts/claim_check.py (claims.yaml
           wasmcert_bridge_qed flows to artifacts/status.json)
+
+  - id: SWVER-021
+    type: sw-verification
+    title: i64 add/sub/mul/and/or/xor wired into exec_wasm_instr — executor-level refinement (#242)
+    description: >
+      Verifies VCR-WASM-001: closes the former "op-level-only" residual for the
+      six i64 arithmetic/bitwise ops. exec_wasm_instr previously returned None
+      for the I64Add/I64Sub/I64Mul/I64And/I64Or/I64Xor constructors, so those
+      ops carried an op-level refinement lemma (I64.op = wasmcert_i64_op) but no
+      executor-level lemma through the real executor. This batch WIRES the six
+      ops into the model's match (pop2_i64 / VI64, mirroring their proven i32
+      twins) and lands the six executor-level refinement theorems
+      (i64_{add,sub,mul,and,or,xor}_exec_refines_wasmcert), so all 22 i64
+      integer ops now carry BOTH op-level and executor-level refinement.
+      exec_wasm_instr is the semantics model, NOT the code generator: the change
+      is byte-invisible (frozen_codegen_bytes 10/10 unchanged). HONEST SCOPE
+      (named): the reference remains a hand transcription of the pinned
+      coq9.0-wasm-2.2.0 sources; remaining WASM op coverage (div/rem trap rules,
+      clz/ctz/popcnt, wrap/extend/reinterpret conversions, memory, control flow)
+      is the named follow-up.
+    status: implemented
+    tags: [vcr-wasm, wasmcert, rocq, refinement, executor, epic-242]
+    links:
+      - type: verifies
+        target: VCR-WASM-001
+    fields:
+      method: formal-proof
+      steps:
+        run: "bazel test //coq:verify_proofs && cargo test -p synth-cli --test frozen_codegen_bytes"
+        coverage: >
+          coq/Synth/WASM/WasmSemantics.v (six i64 arithmetic/bitwise arms wired
+          via pop2_i64 / VI64) + coq/Synth/WASM/WasmCertBridge.v (six
+          i64_*_exec_refines_wasmcert theorems, +6 Qed → 591 total); frozen
+          10/10 confirms the semantics-model change does not alter compiled bytes
diff --git a/claims.yaml b/claims.yaml
@@ -189,29 +189,29 @@ claims:
   # ---------------------------------------------------------------------------
   - id: SYNTH-PROOF-COUNT-CLAUDE-MD
     doc: CLAUDE.md
-    text: "585 Qed / 3 Admitted"
+    text: "591 Qed / 3 Admitted"
     evidence:
       - kind: count-eq
         pattern: 'Qed\.'
         glob: ['coq/Synth/**/*.v']
-        expect: 585
+        expect: 591
       - kind: count-eq
         pattern: 'Admitted\.'
         glob: ['coq/Synth/**/*.v']
         expect: 3
 
   - id: SYNTH-PROOF-COUNT-STATUS-MD
     doc: coq/STATUS.md
-    text: "585 Qed / 3 Admitted"
+    text: "591 Qed / 3 Admitted"
     evidence:
       - kind: count-eq                       # headline + Total line must both agree
-        pattern: '585 Qed / 3 Admitted'
+        pattern: '591 Qed / 3 Admitted'
         glob: ['coq/STATUS.md']
         expect: 2
       - kind: count-eq
         pattern: 'Qed\.'
         glob: ['coq/Synth/**/*.v']
-        expect: 585
+        expect: 591
       - kind: count-eq
         pattern: 'Admitted\.'
         glob: ['coq/Synth/**/*.v']

diff --git a/coq/STATUS.md b/coq/STATUS.md
@@ -1,16 +1,17 @@
 # Rocq Proof Suite — Honest Status
 
-**Last Updated: 2026-07-17 (VCR-WASM-001 phase 3: recount 585 Qed / 3 Admitted,
-+2 admit., crude `grep "Qed\."` over `coq/Synth/**/*.v` — same method as prior
-recounts; +49 vs the prior 536 are the WasmCert-Coq i64 refinement batch in
-`WasmCertBridge.v` (22 i64 ops transcribed from the same pinned
-coq9.0-wasm-2.2.0 sources with line-level provenance: op-level refinement for
-all 22 add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge,
-plus executor-level for the 16 WIRED ops — the shifts, the two rotates, the 12
-comparisons; the 6 i64 arithmetic/bitwise ops are op-level-only, a NAMED
-residual because `exec_wasm_instr` returns `None` for those constructors; still
-a hand transcription, not the real external dep). The prior +47 vs 489 was the
-i32 batch (19 ops);
+**Last Updated: 2026-07-17 (VCR-WASM-001 phase 3 wiring: recount 591 Qed / 3 Admitted,
++2 admit., crude `grep "Qed\."` over `coq/Synth/**/*.v` — same method
+as prior recounts; +6 vs the prior 585 are the six i64 arithmetic/bitwise
+executor-level refinement theorems in `WasmCertBridge.v`
+(add/sub/mul/and/or/xor). Those six ops are now WIRED in `exec_wasm_instr`
+(pop2_i64 / VI64, mirroring their i32 twins), so their executor-level
+refinement lands — the former "op-level-only" residual is CLOSED and ALL 22 i64
+integer ops now carry BOTH op-level and executor-level refinement. Still a hand
+transcription, not the real external dep. The prior +49 vs 536 was the
+WasmCert-Coq i64 op-level batch (22 ops transcribed from the same pinned
+coq9.0-wasm-2.2.0 sources with line-level provenance); the +47 vs 489 before
+that was the i32 batch (19 ops);
 prior recount context (#166): the
 -40 vs the prior 512 are the retired VCR-ISA-001 #667 cross-check lemmas of
 `VcrSelRulesGenCheck.v`: `VcrSelRules.v` now DEFINES every `rule_X` as the
@@ -183,7 +184,7 @@ and predates the VcrSelRules (42), VcrSelPilot (7) and SailArmBridge (92) Qed;
 see the per-file breakdown below for current per-file counts. The T3 row and
 the headline total are re-derived by the claim gate.
 
-**Total: 585 Qed / 3 Admitted (+2 admit.) across all files** (recount 2026-07-17, CI-gated via `claims.yaml`)
+**Total: 591 Qed / 3 Admitted (+2 admit.) across all files** (recount 2026-07-17, CI-gated via `claims.yaml`)
 
 v0.10.0 PR 1: +2 T1 Qed (i64_add_correct, i64_sub_correct) and +9
 infrastructure Qed (combine_i32_unsigned, carry_split_add,
@@ -465,7 +466,7 @@ Recount 2026-07-10 (`grep -oE 'Qed\.'` / `'Admitted\.'` per file):
 | StateMonad.v | 3 | 0 | Infra |
 | WasmValues.v | 2 | 0 | Infra |
 | WasmCertReference.v | 0 | 0 | definitions only (VCR-WASM-001: WasmCert-Coq i32 AND i64 rules transcribed from the pinned coq9.0-wasm-2.2.0 sources with line-level provenance). PHASE 3 (v0.48, #242): the extra-coq-package bazel/nix HOOK is LANDED (blocker (1) closed) but the REAL dep stays PENDING and this file stays a hand transcription — nixpkgs pin 88d3861a ships wasmcert 2.2.0, which propagates the UNFREE compcert 3.16 (inria-compcert, meta.license.free=false); wasmcert >= 2.2.1 (drops CompCert) not yet in the pin, so the "trusted transcription" caveat is NOT yet retired |
-| WasmCertBridge.v | 98 | 0 | Infra/T1-analogue (VCR-WASM-001 phase 2: 19 i32 ops; phase 3 (#242): 22 i64 ops — add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge, each with an op-level refinement Qed against the WasmCert reference, plus an executor-level Qed through the real `exec_wasm_instr` for the 16 WIRED ops (shifts + 2 rotates + 11 comparisons (incl. eqz)); the 6 i64 arithmetic/bitwise ops are op-level-only, a NAMED residual because `exec_wasm_instr` returns `None` for those constructors — plus the i64 encoding/bit-level/rotate-boundary helper Qed) |
+| WasmCertBridge.v | 104 | 0 | Infra/T1-analogue (VCR-WASM-001 phase 2: 19 i32 ops; phase 3 (#242): 22 i64 ops — add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge, each with an op-level refinement Qed against the WasmCert reference, PLUS an executor-level Qed through the real `exec_wasm_instr` for ALL 22 ops. The v0.50 wiring batch (#242) WIRED the six arithmetic/bitwise ops (add/sub/mul/and/or/xor) into `exec_wasm_instr` (pop2_i64 / VI64), closing the former op-level-only residual — plus the i64 encoding/bit-level/rotate-boundary helper Qed) |
 | VcrSelPilot.v | 7 | 0 | T1 (register-polymorphic; VCR-SEL-001 go/abandon measurement) |
 | VcrSelRules.v | 42 | 0 | T1 (register-polymorphic; the WIRED VCR-SEL-001 increment-1+2+3+4 rule table — 40 rule theorems 1:1 with `coq/vcr_sel_rules.manifest`, coverage-gated by `//coq:vcr_sel_rules_coverage`, + 2 mod-32 helper lemmas #683. VCR-ISA-001 #667 increment 2: every `rule_X` is DEFINED as the GENERATED `Gen.rule_X` of `VcrSelRulesGenerated.v` — emitted from the shipped `sel_dsl::RULES` — so the theorems are stated directly about the shipped sequences; a table change regenerates `Gen` and breaks the matching Qed. The former `VcrSelRulesGenCheck.v` 40-lemma `reflexivity` gate is retired as vacuous/subsumed) |
 | **Total** | **585** | **3** | (+2 `admit.`; headline re-derived by the claim gate) |

diff --git a/coq/Synth/WASM/WasmCertBridge.v b/coq/Synth/WASM/WasmCertBridge.v
@@ -9,10 +9,11 @@
       [exec_wasm_instr].
     - PHASE 3 (i64 batch, #242): add, sub, mul, and, or, xor, shl, shr_u,
       shr_s, rotl, rotr, eqz, eq, ne, lt_u, lt_s, gt_u, gt_s, le_u, le_s,
-      ge_u, ge_s — op-level refinement for all 22, plus executor-level for the
-      16 ops WIRED in [exec_wasm_instr] (the shifts, the two rotates, and the
-      11 comparisons (incl. eqz); see the named residual below for the 6 arithmetic/
-      bitwise ops the model does not yet route).
+      ge_u, ge_s — op-level refinement for all 22, plus executor-level for ALL
+      22 ops. As of the v0.50 wiring batch (#242) the six arithmetic/bitwise
+      ops (add/sub/mul/and/or/xor) are WIRED in [exec_wasm_instr] (pop2_i64 /
+      VI64, mirroring their i32 twins), so their executor-level refinement now
+      lands too — the former "op-level-only" residual is CLOSED.
     It is the WASM-side analogue of SailArmBridge.v's per-instruction bridge
     lemmas (VCR-ISA-001 / #667).
 
@@ -28,12 +29,13 @@
     wasmcert >= 2.2.1.
 
     NAMED RESIDUALS (not forced, not admitted):
-    - i64 add/sub/mul/and/or/xor have OP-LEVEL refinement only: synth's
-      [exec_wasm_instr] returns [None] for the [I64Add]/…/[I64Xor] constructors
-      (they are not wired in the model's match, unlike their i32 twins). Wiring
-      them is a semantics-model change, out of scope for a transcription batch.
-    - Remaining op coverage (div/rem trap rules, clz/ctz/popcnt, memory,
-      control flow) is the named follow-up for both widths.
+    - (CLOSED, v0.50 #242) i64 add/sub/mul/and/or/xor are now WIRED in
+      [exec_wasm_instr] and carry executor-level refinement — they previously
+      had OP-LEVEL refinement only because the model's match returned [None] for
+      those constructors. That gap is gone.
+    - Remaining op coverage (div/rem trap rules, clz/ctz/popcnt, the
+      wrap/extend/reinterpret conversions, memory, control flow) is the named
+      follow-up for both widths.
 
     NON-VACUITY (why a WRONG synth semantics fails this file):
     - No op-level lemma is [reflexivity]-only where a real gap exists:
@@ -652,14 +654,13 @@ Qed.
     helpers below are the wordsize-64 duplicates of the i32 helpers (the same
     raw-vs-normalized [Z.testbit] / shift-count-collapse content, at 2^64).
 
-    HONEST SCOPE (named residuals). Two classes are DELIBERATELY not given
-    executor-level refinement:
-    - i64 add/sub/mul/and/or/xor: synth's [exec_wasm_instr] returns [None] for
-      these constructors ([I64Add]/[I64Sub]/…/[I64Xor] are not wired in the
-      model's match, unlike their i32 counterparts). We prove the OP-LEVEL
-      refinement ([I64.op = wasmcert_i64_op], genuine raw-vs-normalized content),
-      and NAME the missing executor routing as a residual — wiring them into the
-      model is a semantics change, out of scope for a transcription batch.
+    HONEST SCOPE. As of the v0.50 wiring batch (#242) ALL 22 i64 integer ops
+    carry BOTH op-level and executor-level refinement:
+    - i64 add/sub/mul/and/or/xor: now WIRED in synth's [exec_wasm_instr]
+      ([I64Add]/[I64Sub]/…/[I64Xor], pop2_i64 / VI64, mirroring their i32
+      counterparts). Both the OP-LEVEL refinement ([I64.op = wasmcert_i64_op],
+      genuine raw-vs-normalized content) AND the executor-level routing are
+      proven — the former "op-level-only" residual is CLOSED.
     - i64 rotl/rotr: transcribed at the reference level (WasmCertReference.v) and
       proven op-level here; see the note at the rotate lemmas for the [n = 0]
       boundary discharge. *)
@@ -1028,6 +1029,87 @@ Proof.
     reflexivity.
 Qed.
 
+(** ** i64 executor-level refinement: arithmetic + bitwise.
+    [exec_wasm_instr] pushes exactly the WasmCert reference result. These six
+    ops (add/sub/mul/and/or/xor) are now WIRED in the model's match (pop2_i64 /
+    VI64), so their executor-level refinement lands with the same shape as the
+    i32 twins and the i64 shifts — closing the former "op-level-only" residual.
+    If an op were miswired (wrong operation, wrong operand order, wrong stack
+    shape) the theorem would be unprovable: the pushed value is pinned to the
+    INDEPENDENT reference. *)
+
+Theorem i64_add_exec_refines_wasmcert : forall v1 v2 s stack',
+  s.(stack) = VI64 v2 :: VI64 v1 :: stack' ->
+  exec_wasm_instr I64Add s =
+  Some (mkWasmState
+          (VI64 (wasmcert_i64_add v1 v2) :: stack')
+          s.(locals) s.(globals) s.(memory)).
+Proof.
+  intros v1 v2 s stack' Hstack.
+  unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack.
+  rewrite <- i64_add_refines_wasmcert_op. reflexivity.
+Qed.
+
+Theorem i64_sub_exec_refines_wasmcert : forall v1 v2 s stack',
+  s.(stack) = VI64 v2 :: VI64 v1 :: stack' ->
+  exec_wasm_instr I64Sub s =
+  Some (mkWasmState
+          (VI64 (wasmcert_i64_sub v1 v2) :: stack')
+          s.(locals) s.(globals) s.(memory)).
+Proof.
+  intros v1 v2 s stack' Hstack.
+  unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack.
+  rewrite <- i64_sub_refines_wasmcert_op. reflexivity.
+Qed.
+
+Theorem i64_mul_exec_refines_wasmcert : forall v1 v2 s stack',
+  s.(stack) = VI64 v2 :: VI64 v1 :: stack' ->
+  exec_wasm_instr I64Mul s =
+  Some (mkWasmState
+          (VI64 (wasmcert_i64_mul v1 v2) :: stack')
+          s.(locals) s.(globals) s.(memory)).
+Proof.
+  intros v1 v2 s stack' Hstack.
+  unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack.
+  rewrite <- i64_mul_refines_wasmcert_op. reflexivity.
+Qed.
+
+Theorem i64_and_exec_refines_wasmcert : forall v1 v2 s stack',
+  s.(stack) = VI64 v2 :: VI64 v1 :: stack' ->
+  exec_wasm_instr I64And s =
+  Some (mkWasmState
+          (VI64 (wasmcert_i64_and v1 v2) :: stack')
+          s.(locals) s.(globals) s.(memory)).
+Proof.
+  intros v1 v2 s stack' Hstack.
+  unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack.
+  rewrite <- i64_and_refines_wasmcert_op. reflexivity.
+Qed.
+
+Theorem i64_or_exec_refines_wasmcert : forall v1 v2 s stack',
+  s.(stack) = VI64 v2 :: VI64 v1 :: stack' ->
+  exec_wasm_instr I64Or s =
+  Some (mkWasmState
+          (VI64 (wasmcert_i64_or v1 v2) :: stack')
+          s.(locals) s.(globals) s.(memory)).
+Proof.
+  intros v1 v2 s stack' Hstack.
+  unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack.
+  rewrite <- i64_or_refines_wasmcert_op. reflexivity.
+Qed.
+
+Theorem i64_xor_exec_refines_wasmcert : forall v1 v2 s stack',
+  s.(stack) = VI64 v2 :: VI64 v1 :: stack' ->
+  exec_wasm_instr I64Xor s =
+  Some (mkWasmState
+          (VI64 (wasmcert_i64_xor v1 v2) :: stack')
+          s.(locals) s.(globals) s.(memory)).
+Proof.
+  intros v1 v2 s stack' Hstack.
+  unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack.
+  rewrite <- i64_xor_refines_wasmcert_op. reflexivity.
+Qed.
+
 (** ** i64 executor-level refinement: shifts.
     [exec_wasm_instr] pushes exactly the WasmCert reference result. Mirrors the
     i32 exec lemmas but through the i64 stack path (pop2_i64 / VI64). *)

diff --git a/coq/Synth/WASM/WasmSemantics.v b/coq/Synth/WASM/WasmSemantics.v
@@ -324,6 +324,56 @@ Definition exec_wasm_instr (i : wasm_instr) (s : wasm_state) : option wasm_state
       | None => None
       end
 
+  (* i64 arithmetic operations (mirror the i32 arms via pop2_i64 / VI64) *)
+  | I64Add =>
+      match pop2_i64 s with
+      | Some (v1, v2, s') =>
+          let result := I64.add v1 v2 in
+          Some (push_value (VI64 result) s')
+      | None => None
+      end
+
+  | I64Sub =>
+      match pop2_i64 s with
+      | Some (v1, v2, s') =>
+          let result := I64.sub v1 v2 in
+          Some (push_value (VI64 result) s')
+      | None => None
+      end
+
+  | I64Mul =>
+      match pop2_i64 s with
+      | Some (v1, v2, s') =>
+          let result := I64.mul v1 v2 in
+          Some (push_value (VI64 result) s')
+      | None => None
+      end
+
+  (* i64 bitwise operations *)
+  | I64And =>
+      match pop2_i64 s with
+      | Some (v1, v2, s') =>
+          let result := I64.and v1 v2 in
+          Some (push_value (VI64 result) s')
+      | None => None
+      end
+
+  | I64Or =>
+      match pop2_i64 s with
+      | Some (v1, v2, s') =>
+          let result := I64.or v1 v2 in
+          Some (push_value (VI64 result) s')
+      | None => None
+      end
+
+  | I64Xor =>
+      match pop2_i64 s with
+      | Some (v1, v2, s') =>
+          let result := I64.xor v1 v2 in
+          Some (push_value (VI64 result) s')
+      | None => None
+      end
+
   (* i64 comparison operations *)
   | I64Eqz =>
       match pop_i64 s with