proof(#242): VCR-WASM-001 i64 transcription batch — 22 ops, 536→585 Qed

[avrabe]

VCR-WASM-001 (Track B, epic #242) — i64 integer family transcription batch

Extends the WasmCert-Coq refinement bridge from the i32 fragment (phases 1+2) to
the i64 integer family, transcribed by hand from the same pinned
coq9.0-wasm-2.2.0 sources with line-level provenance, mirroring the i32 batch.

Ops added (22)

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 (I64.op = wasmcert_i64_op) — a real Qed for all 22.
• Executor-level refinement (routes through the real exec_wasm_instr) — for
  the 16 WIRED ops: 3 shifts + 2 rotates + 11 comparisons (incl. eqz).

Provenance

• Arithmetic/bitwise/shift/compare reuse the generic Make functor citations
  shared with i32, read at wordsize 64 (Int64 at numerics.v:1038-1039).
• The two rotates newly cite CompCert 3.16 Integers.v:217-222 (rol/ror).
  The rotate proofs discharge a genuine n=0 boundary gap (synth re-normalizes
  the [64-n] sub-shift count mod 64 while the reference's is raw; reconciled
  via lor-idempotence at the boundary) — no admit, no axiom.

Named residual (honest, not forced)

i64 add/sub/mul/and/or/xor have op-level refinement ONLY — synth's
exec_wasm_instr returns None for those constructors (unwired in the model,
unlike their i32 twins). Wiring them is a semantics-model change, out of scope
for a transcription batch.

Still a transcription

The real external WasmCert dep stays blocked on the unfree CompCert 3.16 the
current nixpkgs pin (88d3861a) propagates via wasmcert 2.2.0; the "trusted
transcription" caveat is unchanged. Retires mechanically when a pin ships
wasmcert ≥ 2.2.1.

Verification

• Proofs GREEN via bazel test //coq:verify_proofs — observed on the
  hermetic Nix Rocq 9.0.1 toolchain (//coq:rocq_proofs PASSED).
• Rocq Qed 536 → 585 (WasmCertBridge.v 49 → 98). Docs (CLAUDE.md,
  coq/STATUS.md, README.md, roadmap) + claims.yaml bumped together;
  status.json/FEATURE_MATRIX.md regenerated; python3 scripts/claim_check.py claims.yaml → 25/25 claims hold.
• Frozen: no Rust / no byte changes (proofs + docs + rivet only).
• rivet: new SWVER-020 (verifies: VCR-WASM-001) closes the sw-verification
  gap; rivet validate error count unchanged (52, all pre-existing cross-repo).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L