spike(vcr-isa-001): Sail/ASL-derived semantics bridge — AArch32 ADD/ADDS/CMP proven ≡ ArmSemantics.v (#242)

[avrabe]

VCR-ISA-001 feasibility spike (epic #242, Track B)

Bounded research spike: can we anchor ArmSemantics.v on an independently-derived ISA semantics (Sail, generated from Arm's own ASL) so a modeling bug can't hide? Deliverable is a decision-quality report + minimal working code — not a migration.

Survey (verified against the repos, not from memory)

• Sail tool: alive. Sail 0.20 (nixpkgs ocamlPackages.sail, installs in seconds) ships the --coq target (bbv|stdpp styles); rems-project/coq-sail is maintained.
• T32/A32 coverage: yes. sail-arm arm-v9.4-a (derived from Arm's 2023-03 ASL via asl_to_sail) contains every AArch32 instruction incl. all four ADD (register) encodings (instrs32.sail, 1.9 MB).
• Importing the generated Coq: NO-GO. The arm-v9.4-a Coq snapshot is a single 42 MB armv9.v + 1 MB types, pinned to stdpp-unstable (not in opam) and git-pinned coq-sail-stdpp; the 2019 v8.5 snapshot README says the build needs ~40 GB RAM and was checked against Coq 8.9.1. That cannot join our hermetic Rocq 9 / Stdlib-prefix Bazel toolchain or CI.

The bridge (the spike's crown) — landed, all Qed

coq/Synth/ARM/SailArmBridge.v (23 Qed / 0 Admitted, in //coq:verify_proofs, green): hand-transcribes AddWithCarry (v8_base.sail:13337) and the AArch32 ADD/CMP register-form execute clauses (instrs32.sail:457) from sail-arm @ 1bf2e5574ba9 with file:line provenance comments, then proves:

• sail_bridge_add_reg — our ADD ≡ R[d] := AddWithCarry(R[n], R[m], '0').result
• sail_bridge_adds_reg — our ADDS ≡ same, plus all four NZCV flags
• sail_bridge_cmp_reg — our CMP flags ≡ AddWithCarry(R[n], NOT(R[m]), '1') nzcv

The six hand-written flag definitions (compute_{n,z}_flag, compute_{c,v}_flag_{add,sub}) are proven equal to ASL's formulations — genuinely different formulas (ASL's V is SInt(result) != signed_sum; ours is the sign-pattern test), so the lemmas are non-vacuous. These definitions are the foundation under every CMP-based comparison lowering in Compilation.v and VcrSelRules.v.

Documented abstraction gaps (file header): shift_n = 0, d ≠ 15 (the PC-executor gap is NOT closed by this and remains the item's core prerequisite for the div/rem admits), no IT blocks, bits(32) as Z mod 2^32.

Cost per instruction (measured, not estimated)

~40 lines transcription + ~230 lines proof for the whole ADD family, with the flag machinery (the hard 60%) now reusable: SUB/SUBS/CMN/RSB near-free, ~0.5–1 day per remaining straight-line op class, memory ops widest gap. Full analysis in docs/design/vcr-isa-001-spike.md.

Recommendation

GO on VCR-ISA-001 via per-instruction transcribe-and-bridge (priority: AddWithCarry family → flag-free ALU → PC-executor refactor → memory). NO-GO on importing gen_coq output. RISC-V half unmeasured — sail-riscv's maintained Coq export may admit the import path there; evaluate separately.

Roadmap: VCR-ISA-001 stays proposed; the 2026-06-10 deep-research gate ("bounded feasibility spike must precede release commitment") is now answered with in-tree evidence.

• bazel test //coq:verify_proofs green (rocq_proofs + vcr_sel_rules_coverage)
• rivet validate — 0 non-xref errors (same as main baseline)
• No Rust touched

Refs #242 (VCR-ISA-001)

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!