feat(vcr-isa): AddWithCarry family + flag-free ALU + shifts + moves bridged to Sail/ASL (#242, VCR-ISA-001)

[avrabe]

Summary

Round 2 of VCR-ISA-001 (epic #242), executing the spike's own priority list (docs/design/vcr-isa-001-spike.md §5, items 1–2 plus the moves stretch) with the exact transcription + bridge-lemma pattern PR #660 established: verbatim-quoted Sail execute clauses with file:line provenance (pin: rems-project/sail-arm @ 1bf2e5574ba9, arm-v9.4-a), hand transcription, and a Qed bridge theorem proving exec_instr ≡ the transcription on the full observable state.

coq/Synth/ARM/SailArmBridge.v: 81 Qed / 0 Admitted / 0 new axioms (round 1: 23).

Op classes bridged

Class	Instructions	Form
AddWithCarry family	SUB, SUBS, CMN, RSB, ADC, SBC (register)	exact state; SUBS = reg + all 4 NZCV; ADC/SBC take the live C flag as carry_in (the i64 ADDS;ADC / SUBS;SBC pair-codegen primitives)
Flag-free ALU	AND, ORR, EOR, MVN (register)	exact state (mod-2^32 distributes over Z.land/lor/lxor, testbit extensionality)
Shifts (immediate)	LSL/LSR/ASR/ROR #1..31	exact state, via a faithful Shift_C transcription (v8_base.sail:41273) + all four *_C primitives incl. shifter carry-out (builtins.sail:69–99)
Shifts (register)	LSL/LSR/ASR/ROR, UInt(R[s]<7:0>)	exact state under 0 < UInt(R[s]) < 32; amount = 0 bridged on the unsigned view
Moves	MOV (register), MOVW, MOVT	exact state; MOVT bitfield-insert ≡ our AND/ORR/LSL formulation under UInt(imm16) < 2^16

Documented gaps (in-file, gaps 5–10)

setflags=false only for ALU/shifts/moves (no ANDS/LSLS/MOVS in ArmSemantics.v — carry-out transcribed, nothing to bridge it to); shift 32 and register amounts ≥ 32 excluded; BIC absent from our model; MOVW carries pre-expanded imm32; RRX out of scope.

Finding (the bridge earning its keep): two latent divergences between the hand-written model and the ASL surfaced — LSR/ASR #32 (our mod-32 masking computes shift-by-0 where ARM zero/sign-fills) and register-controlled amounts ≥ 32 (ARM reads the low byte). Neither is reachable from Compilation.v (WASM masks shift amounts to 0..31), so they are latent model bugs, not miscompiles — exactly the class VCR-ISA-001 exists to surface.

Cost vs the spike's estimate

~Half a day wall-clock for six-plus op classes, vs the spike's 0.5–1 day per class: the flag-machinery amortization held exactly (SUB's flags ARE CMP's flags — one exact; ADC/SBC needed two ~10-line mod lemmas). Genuinely new machinery: the three bitwise mod-distribution lemmas and the Shift_C transcription.

Roadmap

VCR-ISA-001 proposed → approved in artifacts/verified-codegen-roadmap.yaml: two landed increments validate the revised (per-instruction transcribe-and-bridge) criterion on the i32 straight-line integer core. Explicitly NOT implemented: the PC-indexed executor (the trap-guard admits — this item's core motivation), MUL/UMULL/CLZ/RBIT, memory ops, and the whole RISC-V half.

Verification

• bazel test //coq:verify_proofs — green locally (hermetic Rocq 9 toolchain)
• cargo test -p synth-cli --test frozen_codegen_bytes — 10/10 (coq-only change, formality)
• cargo fmt --check / cargo clippy --workspace --all-targets -- -D warnings — clean (no Rust touched)

Refs #242.

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!