From c0478937152923bccfadc65b332084f778a6966b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 8 Jul 2026 22:59:26 +0200 Subject: [PATCH] feat(vcr-isa): AddWithCarry family + ALU + shifts + moves bridged to Sail/ASL (#242, VCR-ISA-001) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends coq/Synth/ARM/SailArmBridge.v per the spike's priority list (docs/design/vcr-isa-001-spike.md §5, items 1-2 + the moves stretch): - AddWithCarry family completed: SUB/SUBS (reg + all 4 NZCV), CMN, RSB, and ADC/SBC with the LIVE C flag as carry_in — the i64 lo/hi pair codegen primitives (ADDS;ADC / SUBS;SBC). - Flag-free ALU: AND/ORR/EOR/MVN (register), via mod-2^32 distribution over Z.land/Z.lor/Z.lxor (testbit extensionality). - Shifts: faithful Shift_C transcription (v8_base.sail:41273) with all four *_C primitives incl. shifter carry-out (builtins.sail:69-99); LSL/LSR/ASR/ROR bridged in immediate (1..31) and register (0 < UInt(R[s]) < 32) forms; amount = 0 bridged on the unsigned view. - Moves: MOV (register), MOVW, MOVT (bitfield-insert vs AND/ORR/LSL formulation, UInt(imm16) < 2^16). File now 81 Qed / 0 Admitted / 0 new axioms (round 1: 23). All quoted Sail pinned to rems-project/sail-arm @ 1bf2e5574ba9 with file:line provenance. New documented gaps 5-10 in-file; FINDING: two latent hand-model divergences from the ASL surfaced (LSR/ASR #32, register shift amounts >= 32 — unreachable from Compilation.v, WASM masks 0..31). Roadmap: VCR-ISA-001 proposed -> approved (method validated on the i32 straight-line integer core; PC executor, memory ops, RISC-V half remain). bazel test //coq:verify_proofs green. Co-Authored-By: Claude Fable 5 --- artifacts/verified-codegen-roadmap.yaml | 24 +- coq/BUILD.bazel | 8 +- coq/Synth/ARM/SailArmBridge.v | 930 +++++++++++++++++++++++- docs/design/vcr-isa-001-spike.md | 46 +- 4 files changed, 1001 insertions(+), 7 deletions(-) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 1d7382e1..f0212b85 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -617,7 +617,24 @@ artifacts: Sail memory vs Z->I32 model). RISC-V half unmeasured — sail-riscv's maintained Coq export may admit the import path there; re-evaluate separately. - status: proposed + + ROUND 2 LANDED (2026-07-08, same day): the spike's priority items (1) + and (2) + the moves stretch — SailArmBridge.v now 81 Qed / 0 Admitted / + 0 new axioms covering the FULL AddWithCarry family (ADD/ADDS/CMP + + SUB/SUBS/CMN/RSB + ADC/SBC with live-C carry_in — the i64 pair-codegen + primitives), flag-free ALU (AND/ORR/EOR/MVN), all four shifts in + immediate (1..31) and register (0 < amt < 32; amt = 0 on the unsigned + view) forms via a faithful Shift_C transcription incl. shifter + carry-out, and MOV/MOVW/MOVT. Measured cost ~0.5 day for six-plus + classes (well under the spike's per-class estimate; the flag-machinery + amortization held). BONUS FINDING: the bridge surfaced two latent + hand-model divergences from the ASL (LSR/ASR #32 and register shift + amounts >= 32 — unreachable from Compilation.v since WASM masks to + 0..31), documented in-file as gaps 6-7 — the exact bug class this item + exists to surface. Still open (why not implemented): PC-indexed + executor (the trap-guard admits, this item's core motivation), + MUL/UMULL/CLZ/RBIT/memory/branches, and the whole RISC-V half. + status: approved tags: [semantics, sail, isa, trust, rocq, track-b, unblocks-admits] links: - type: derives-from @@ -643,6 +660,11 @@ artifacts: transcribe-and-bridge against provenance-pinned Sail source, not against an imported generated model. RV32 export build remains unmeasured (the spike's ARM no-go on import does not transfer). + STATUS proposed -> approved (2026-07-08): two landed increments + (23 then 81 Qed, //coq:verify_proofs green) validate the revised + criterion's method on the i32 straight-line integer core; approved + means the approach is committed, NOT that the item is implemented — + the PC-executor refactor, memory ops, and the RISC-V half remain. - id: VCR-WASM-001 type: sw-req diff --git a/coq/BUILD.bazel b/coq/BUILD.bazel index be58d98f..4dc41206 100644 --- a/coq/BUILD.bazel +++ b/coq/BUILD.bazel @@ -73,9 +73,11 @@ rocq_library( deps = [":arm_semantics"], ) -# VCR-ISA-001 spike (#242): Sail/ASL-derived semantics bridge — AArch32 -# ADD/ADDS/CMP (register) transcribed from rems-project/sail-arm with -# line-level provenance, proven ≡ ArmSemantics.v on registers + NZCV. +# VCR-ISA-001 (#242): Sail/ASL-derived semantics bridge — the AArch32 +# integer core (AddWithCarry family ADD/ADDS/CMP/SUB/SUBS/CMN/RSB/ADC/SBC, +# flag-free ALU AND/ORR/EOR/MVN, LSL/LSR/ASR/ROR imm+reg via Shift_C, +# MOV/MOVW/MOVT) transcribed from rems-project/sail-arm with line-level +# provenance, proven ≡ ArmSemantics.v on registers + NZCV. rocq_library( name = "sail_arm_bridge", srcs = ["Synth/ARM/SailArmBridge.v"], diff --git a/coq/Synth/ARM/SailArmBridge.v b/coq/Synth/ARM/SailArmBridge.v index 0bd4ff50..00f37567 100644 --- a/coq/Synth/ARM/SailArmBridge.v +++ b/coq/Synth/ARM/SailArmBridge.v @@ -1,4 +1,11 @@ -(** * VCR-ISA-001 SPIKE — Sail/ASL-derived semantics bridge (AArch32 ADD/ADDS/CMP, register forms) +(** * VCR-ISA-001 — Sail/ASL-derived semantics bridge (AArch32 integer core) + + Round 1 (spike, PR #660): ADD/ADDS/CMP (register) + all four NZCV flags. + Round 2 (this increment): the rest of the AddWithCarry family + (SUB/SUBS/CMN/RSB/ADC/SBC), the flag-free ALU class (AND/ORR/EOR/MVN), + the shift class (LSL/LSR/ASR/ROR, immediate and register forms, via a + Shift_C transcription), and MOV/MOVW/MOVT. See the ROUND 2 section + header below for its provenance table and additional abstraction gaps. GOAL (epic #242, VCR-ISA-001). ArmSemantics.v is a HAND-WRITTEN ARM model: every correctness theorem in this suite (including the 21 VCR-SEL-001 rule @@ -474,3 +481,924 @@ Theorem sail_bridge_cmp_reg : forall s rn rm, Proof. intros. rewrite sail_cmp_r_flags_eq. reflexivity. Qed. + +(** ** ROUND 2 — AddWithCarry family + flag-free ALU + shifts + moves + + Same pin as round 1: rems-project/sail-arm @ master (commit 1bf2e5574ba9, + 2026-06-19), model arm-v9.4-a. Execute-clause provenance: + + - execute SUB (register) instrs32.sail:15676 + "(result, nzcv) = AddWithCarry(R_read(n), not_vec(shifted), 0b1)" + - execute RSB (register) instrs32.sail:10337 + "(result, nzcv) = AddWithCarry(not_vec(R_read(n)), shifted, 0b1)" + - execute ADC (register) instrs32.sail:119 + "(result, nzcv) = AddWithCarry(R_read(n), shifted, PSTATE.C)" + - execute SBC (register) instrs32.sail:10946 + "(result, nzcv) = AddWithCarry(R_read(n), not_vec(shifted), PSTATE.C)" + - execute CMN (register) instrs32.sail:2428 + "(result, nzcv) = AddWithCarry(R_read(n), shifted, 0b0)" (flags only) + - execute AND (register) instrs32.sail:1141 + "let result : bits(32) = R_read(n) & shifted" + - execute ORR (register) instrs32.sail:8478 + "let result : bits(32) = R_read(n) | shifted" + - execute EOR (register) instrs32.sail:3173 + "let result : bits(32) = EOR(R_read(n), shifted)" + (EOR = xor_vec, prelude.sail:216) + - execute MVN (register) instrs32.sail:8066 + "let result : bits(32) = not_vec(shifted)" + - execute LSL (immediate) instrs32.sail:6859 + "(result, carry) = Shift_C(R_read(m), SRType_LSL, shift_n, PSTATE.C)" + - execute LSR (immediate) instrs32.sail:6972 (SRType_LSR) + - execute ASR (immediate) instrs32.sail:1310 (SRType_ASR) + - ROR (immediate) has no execute clause of its own: it is the + MOV (register) instruction with shift_t = SRType_ROR, shift_n = + UInt(imm5) <> 0 (execute at instrs32.sail:7469; DecodeImmShift + v8_base.sail:41327 maps stype 0b11, imm5 <> 0 to (SRType_ROR, + UInt(imm5)); imm5 == 0 is SRType_RRX — out of scope, synth never + emits RRX) + - execute LSL (register) instrs32.sail:6909 + "let 'shift_n = UInt(R_read(m)[7 .. 0]); + (result, carry) = Shift_C(R_read(n), SRType_LSL, shift_n, PSTATE.C)" + - execute LSR (register) instrs32.sail:7019 (SRType_LSR) + - execute ASR (register) instrs32.sail:1357 (SRType_ASR) + - execute ROR (register) instrs32.sail:10205 (SRType_ROR) + - execute MOV (register) instrs32.sail:7469 + "(shifted, carry) = Shift_C(R_read(m), shift_t, shift_n, PSTATE.C); + let result : bits(32) = shifted" + - execute MOV (immediate) instrs32.sail:7315 + "let result : bits(32) = imm32" (MOVW = T3/A2 encoding, + imm32 = ZeroExtend(imm16, 32)) + - execute MOVT instrs32.sail:7722 + "R_set(d) = [R_read(d) with 31 .. 16 = imm16]" + + Shifter-helper provenance (quoted where transcribed below): + + - Shift_C v8_base.sail:41273 (amount == 0 => (value, carry_in)) + - LSL_C builtins.sail:69 + - LSR_C builtins.sail:78 + - ASR_C builtins.sail:88 + - ROR_C builtins.sail:99 + + ADDITIONAL ABSTRACTION GAPS (beyond gaps 1-4 in the file header; each is + a measured statement about what the theorems below do NOT cover): + + 5. setflags = false for the ALU/shift/move bridges. ArmSemantics.v has + no flag-setting AND/ORR/EOR/MVN/shift/MOV forms (no ANDS/LSLS/MOVS + arm_instr constructors), so the Sail setflags branch — N = result<31>, + Z = IsZero(result), C = shifter carry-out, V unchanged — has no + counterpart to bridge. The shifter carry-out IS transcribed faithfully + in sail_{lsl,lsr,asr,ror}_c below (the new C territory Shift_C opens), + so a future ANDS/LSLS/MOVS model extension only needs the bridge + lemma, not a new transcription. SUBS/ADDS/CMP/CMN are unaffected + (their flags come from AddWithCarry and ARE fully bridged). + 6. Immediate shifts bridge for shift_n in 1..31. shift_n = 32 + (LSR/ASR imm5 = 00000, DecodeImmShift v8_base.sail:41327) is a REAL + MODEL DIVERGENCE, not just a gap: I32.shru/shrs mask the amount + mod 32, so ArmSemantics.v computes a shift by 0 where ARM produces + 0 / the sign-fill. Compilation.v only emits WASM-masked amounts + (0..31), so no emitted program reaches the divergence — but the + hand-written model is WRONG about LSR/ASR #32 and a bridge for it + is intentionally impossible until the model is fixed. + 7. Register shifts bridge under 0 < UInt(R[s]) < 32. ARM reads the low + BYTE of the shift register (UInt(R[s]<7:0>), so amounts 32..255 + produce 0 / sign-fill / rotate-mod-32), while I32.shl/shru/shrs mask + mod 32 — same divergence class as gap 6 for dynamic amounts >= 32. + WASM shift semantics mask the amount mod 32 BEFORE the instruction, + so lowered code never presents an out-of-range amount. The amount = 0 + case is bridged separately on the unsigned view + (sail_bridge_*_reg_zero below): Shift_C with amount 0 returns the + input bits(32) unchanged, which in the Z-rendering is the RAW + representative, while our shift-by-0 normalizes through repr — the + two agree on I32.unsigned (the only observation WASM values make) + but not as raw Z, so the exact-state equality form does not apply. + 8. BIC (register) exists in the Sail model (instrs32.sail:1744) but + ArmSemantics.v has no BIC instruction — nothing to bridge (recorded + so the omission is a model gap, not an oversight). + 9. MOVW holds the already-expanded imm32: ArmInstructions.v's + MOVW rd imm takes an I32.int, not the encoding's 16-bit field, so + the bridge assumes imm = ZeroExtend(imm16, 32) (i.e. is exact only + when UInt(imm) < 2^16 — which is what the Rust encoder emits). + MOVT is bridged under the same UInt(imm16) < 2^16 hypothesis. + 10. RRX is out of scope entirely (synth never emits it; ArmSemantics.v + cannot represent it). *) + +(** *** Transcription: the remaining AddWithCarry users *) + +(** SUB (register), d <> 15, shift_n = 0: + "AddWithCarry(R_read(n), not_vec(shifted), 0b1)" (instrs32.sail:15676). + Same AddWithCarry + NOT shape as CMP — SUB additionally writes R[d]. *) +Definition sail_sub_r_result (rn_val rm_val : I32.int) : I32.int := + fst (sail_add_with_carry rn_val (sail_not rm_val) true). + +Definition sail_sub_r_flags (rn_val rm_val : I32.int) : condition_flags := + let '(_, (n, z, c, v)) := sail_add_with_carry rn_val (sail_not rm_val) true in + mkFlags n z c v. + +(** RSB (register): "AddWithCarry(not_vec(R_read(n)), shifted, 0b1)" + (instrs32.sail:10337) — the NOT lands on the FIRST operand. *) +Definition sail_rsb_r_result (rn_val rm_val : I32.int) : I32.int := + fst (sail_add_with_carry (sail_not rn_val) rm_val true). + +(** CMN (register): "AddWithCarry(R_read(n), shifted, 0b0)", flags only + (instrs32.sail:2428) — the ADDS flag computation without the write. *) +Definition sail_cmn_r_flags (rn_val rm_val : I32.int) : condition_flags := + let '(_, (n, z, c, v)) := sail_add_with_carry rn_val rm_val false in + mkFlags n z c v. + +(** ADC (register): "AddWithCarry(R_read(n), shifted, PSTATE.C)" + (instrs32.sail:119) — the first bridged op whose carry_in is the LIVE + C flag, not a constant. *) +Definition sail_adc_r_result (rn_val rm_val : I32.int) (c : bool) : I32.int := + fst (sail_add_with_carry rn_val rm_val c). + +(** SBC (register): "AddWithCarry(R_read(n), not_vec(shifted), PSTATE.C)" + (instrs32.sail:10946). *) +Definition sail_sbc_r_result (rn_val rm_val : I32.int) (c : bool) : I32.int := + fst (sail_add_with_carry rn_val (sail_not rm_val) c). + +(** *** Transcription: flag-free ALU (result paths; the setflags branch is + gap 5) *) + +(** AND/ORR/EOR on bits(32) — "R_read(n) & shifted" / "|" / "EOR(...)" + at shift_n = 0 (Shift_C identity, so shifted = R_read(m)). bits(32) + values are non-negative 32-bit words: rendered as Z.land/Z.lor/Z.lxor + on the unsigned views. *) +Definition sail_and_r (x y : I32.int) : I32.int := + I32.repr (Z.land (I32.unsigned x) (I32.unsigned y)). +Definition sail_orr_r (x y : I32.int) : I32.int := + I32.repr (Z.lor (I32.unsigned x) (I32.unsigned y)). +Definition sail_eor_r (x y : I32.int) : I32.int := + I32.repr (Z.lxor (I32.unsigned x) (I32.unsigned y)). + +(** MVN (register): "not_vec(shifted)" (instrs32.sail:8066) — [sail_not] + from round 1 is the transcription. *) + +(** *** Transcription: Shift_C and the four shifter primitives + + [LSL_C] — builtins.sail:69: + function LSL_C (x, shift) = { + let carry_out = if shift > 0 & shift <= 'N then x['N - shift] + else bitzero; + (sail_shiftleft(x, shift), [carry_out]) + } + sail_shiftleft on bits(32) truncates to 32 bits: repr (Z.shiftl ux n). *) +Definition sail_lsl_c (x : I32.int) (shift : Z) : I32.int * bool := + (I32.repr (Z.shiftl (I32.unsigned x) shift), + if (0 0 & shift <= 'N then x[shift - 1] + else bitzero; + (sail_shiftright(x, shift), [carry_out]) + sail_shiftright is the logical shift on the unsigned view. *) +Definition sail_lsr_c (x : I32.int) (shift : Z) : I32.int * bool := + (I32.repr (Z.shiftr (I32.unsigned x) shift), + if (0 = 'N then x['N - 1] else x['shift - 1]; + (sail_arith_shiftright(x, shift), [carry_out]) + sail_arith_shiftright shifts the sign-extended value: Z.shiftr (signed x). *) +Definition sail_asr_c (x : I32.int) (shift : Z) : I32.int * bool := + (I32.repr (Z.shiftr (I32.signed x) shift), + if shift =? 0 then false + else if 32 <=? shift then Z.testbit (I32.unsigned x) 31 + else Z.testbit (I32.unsigned x) (shift - 1)). + +(** [ROR_C] — builtins.sail:99: + let 'm = MOD(shift, 'N); + let result : bits('N) = LSR(x, m) | LSL(x, 'N - m); + let carry_out : bits(1) = [result['N - 1]]; + (LSR/LSL here are the truncating bit-vector shifts, no carry.) *) +Definition sail_ror_c (x : I32.int) (shift : Z) : I32.int * bool := + let m := shift mod 32 in + let result := I32.or (I32.repr (Z.shiftr (I32.unsigned x) m)) + (I32.repr (Z.shiftl (I32.unsigned x) (32 - m))) in + (result, Z.testbit (I32.unsigned result) 31). + +Inductive sail_srtype : Type := + | SRType_LSL_t + | SRType_LSR_t + | SRType_ASR_t + | SRType_ROR_t. + +(** [Shift_C] — v8_base.sail:41273: + function Shift_C (value_name, srtype, amount, carry_in) = { + assert(not_bool(srtype == SRType_RRX & amount != 1)); + if amount == 0 then { + (result, carry_out) = (value_name, carry_in) + } else { match srtype { SRType_LSL => LSL_C(value_name, amount), + ... } }; + } + SRType_RRX omitted (gap 10). The amount = 0 arm returns the input + bits(32) unchanged — in the Z-rendering, the raw representative + (see gap 7). *) +Definition sail_shift_c (x : I32.int) (t : sail_srtype) (amount : Z) + (carry_in : bool) : I32.int * bool := + if amount =? 0 then (x, carry_in) + else match t with + | SRType_LSL_t => sail_lsl_c x amount + | SRType_LSR_t => sail_lsr_c x amount + | SRType_ASR_t => sail_asr_c x amount + | SRType_ROR_t => sail_ror_c x amount + end. + +(** Register-controlled shift amount: "UInt(R_read(s)[7 .. 0])" — the low + byte of the shift register (instrs32.sail:6909/7019/1357/10205). *) +Definition sail_shift_amount8 (r : I32.int) : Z := + I32.unsigned r mod 256. + +(** MOVT: "[R_read(d) with 31 .. 16 = imm16]" (instrs32.sail:7722) — the + high half becomes imm16, the low half is preserved. Rendered as the OR + of the shifted 16-bit immediate and the low 16 bits of the old value. *) +Definition sail_movt_result (old imm16 : I32.int) : I32.int := + I32.repr (Z.lor (Z.shiftl (I32.unsigned imm16) 16) + (I32.unsigned old mod 65536)). + +(** *** Arithmetic helpers (round 2) *) + +Lemma unsigned_repr_small : forall n, + 0 <= n < I32.modulus -> I32.unsigned (I32.repr n) = n. +Proof. + intros. unfold I32.unsigned, I32.repr. + rewrite Zmod_mod. apply Z.mod_small. auto. +Qed. + +Lemma unsigned_repr_unsigned : forall x, + I32.unsigned (I32.repr (I32.unsigned x)) = I32.unsigned x. +Proof. + intros. unfold I32.unsigned, I32.repr. rewrite !Zmod_mod. reflexivity. +Qed. + +(** The signed representative reduces to the unsigned one mod 2^32. *) +Lemma signed_mod_modulus : forall x, + I32.signed x mod I32.modulus = I32.unsigned x. +Proof. + intros. unfold I32.signed. cbv zeta. + pose proof (unsigned_range x) as Hx. + destruct (Z.ltb_spec (I32.unsigned x) I32.half_modulus). + - apply Z.mod_small. lia. + - replace (I32.unsigned x - I32.modulus) + with (I32.unsigned x + (-1) * I32.modulus) by lia. + rewrite Z_mod_plus_full. apply Z.mod_small. lia. +Qed. + +(** mod 2^32 distributes over the bitwise operations (bit-extensionality). *) +Lemma land_mod_modulus : forall a b, + Z.land a b mod I32.modulus + = Z.land (a mod I32.modulus) (b mod I32.modulus). +Proof. + intros. unfold I32.modulus. + apply Z.bits_inj'. intros i Hi. + destruct (Z.ltb_spec i 32) as [L | L]. + - rewrite Z.mod_pow2_bits_low by lia. + rewrite !Z.land_spec. + rewrite !Z.mod_pow2_bits_low by lia. reflexivity. + - rewrite Z.mod_pow2_bits_high by lia. + rewrite Z.land_spec. + rewrite !Z.mod_pow2_bits_high by lia. reflexivity. +Qed. + +Lemma lor_mod_modulus : forall a b, + Z.lor a b mod I32.modulus + = Z.lor (a mod I32.modulus) (b mod I32.modulus). +Proof. + intros. unfold I32.modulus. + apply Z.bits_inj'. intros i Hi. + destruct (Z.ltb_spec i 32) as [L | L]. + - rewrite Z.mod_pow2_bits_low by lia. + rewrite !Z.lor_spec. + rewrite !Z.mod_pow2_bits_low by lia. reflexivity. + - rewrite Z.mod_pow2_bits_high by lia. + rewrite Z.lor_spec. + rewrite !Z.mod_pow2_bits_high by lia. reflexivity. +Qed. + +Lemma lxor_mod_modulus : forall a b, + Z.lxor a b mod I32.modulus + = Z.lxor (a mod I32.modulus) (b mod I32.modulus). +Proof. + intros. unfold I32.modulus. + apply Z.bits_inj'. intros i Hi. + destruct (Z.ltb_spec i 32) as [L | L]. + - rewrite Z.mod_pow2_bits_low by lia. + rewrite !Z.lxor_spec. + rewrite !Z.mod_pow2_bits_low by lia. reflexivity. + - rewrite Z.mod_pow2_bits_high by lia. + rewrite Z.lxor_spec. + rewrite !Z.mod_pow2_bits_high by lia. reflexivity. +Qed. + +(** Shifting the canonical representative left is shifting the raw one. *) +Lemma repr_shiftl_unsigned : forall x n, + 0 <= n -> + I32.repr (Z.shiftl (I32.unsigned x) n) = I32.repr (Z.shiftl x n). +Proof. + intros x n Hn. unfold I32.repr, I32.unsigned. + rewrite !Z.shiftl_mul_pow2 by lia. + apply Z.mul_mod_idemp_l. apply modulus_nz. +Qed. + +(** Sum of three with the first two canonicalized. *) +Lemma mod3_add : forall a b c, + (a mod I32.modulus + b mod I32.modulus + c) mod I32.modulus + = (a + b + c) mod I32.modulus. +Proof. + intros. + rewrite Zplus_mod. + rewrite (Zplus_mod (a mod I32.modulus) (b mod I32.modulus)). + rewrite !Zmod_mod. + rewrite (Zplus_mod (a + b) c). + rewrite (Zplus_mod a b). + reflexivity. +Qed. + +(** The RSB representative: (NOT x) + y + 1 = y - x on the unsigned view. *) +Lemma repr_rsb_unsigned : forall x y : I32.int, + I32.repr ((I32.modulus - 1 - I32.unsigned x) + I32.unsigned y + 1) + = I32.sub y x. +Proof. + intros. unfold I32.sub, I32.repr, I32.unsigned. + replace (I32.modulus - 1 - x mod I32.modulus + y mod I32.modulus + 1) + with ((y mod I32.modulus - x mod I32.modulus) + 1 * I32.modulus) by lia. + rewrite Z_mod_plus_full. + rewrite <- Zminus_mod. reflexivity. +Qed. + +(** Difference of three with the first two canonicalized. *) +Lemma mod3_sub : forall a b c, + (a mod I32.modulus - b mod I32.modulus - c) mod I32.modulus + = (a - b - c) mod I32.modulus. +Proof. + intros. + rewrite (Zminus_mod (a mod I32.modulus - b mod I32.modulus) c). + rewrite <- (Zminus_mod a b). + rewrite <- Zminus_mod. + reflexivity. +Qed. + +(** The SBC borrow representative: x + (NOT y) + 0 = x - y - 1. *) +Lemma repr_sbc_borrow_unsigned : forall x y : I32.int, + I32.repr (I32.unsigned x + (I32.modulus - 1 - I32.unsigned y) + 0) + = I32.sub (I32.sub x y) I32.one. +Proof. + intros. unfold I32.sub, I32.one, I32.repr, I32.unsigned. + replace (x mod I32.modulus + (I32.modulus - 1 - y mod I32.modulus) + 0) + with ((x mod I32.modulus - y mod I32.modulus - 1) + 1 * I32.modulus) + by lia. + rewrite Z_mod_plus_full. + rewrite mod3_sub. + rewrite (Z.mod_small 1) by (rewrite modulus_val; lia). + rewrite Zminus_mod_idemp_l. reflexivity. +Qed. + +(** Shift-by-small-immediate collapses the operand-masking in I32.shl etc. *) +Lemma shl_repr_small : forall x n, + 0 <= n < 32 -> + I32.shl x (I32.repr n) = I32.repr (Z.shiftl x n). +Proof. + intros x n Hn. unfold I32.shl. + rewrite unsigned_repr_small by (rewrite modulus_val; lia). + rewrite Z.mod_small by lia. reflexivity. +Qed. + +Lemma shru_repr_small : forall x n, + 0 <= n < 32 -> + I32.shru x (I32.repr n) = I32.repr (Z.shiftr (I32.unsigned x) n). +Proof. + intros x n Hn. unfold I32.shru. + rewrite unsigned_repr_small by (rewrite modulus_val; lia). + rewrite Z.mod_small by lia. reflexivity. +Qed. + +Lemma shrs_repr_small : forall x n, + 0 <= n < 32 -> + I32.shrs x (I32.repr n) = I32.repr (Z.shiftr (I32.signed x) n). +Proof. + intros x n Hn. unfold I32.shrs. + rewrite unsigned_repr_small by (rewrite modulus_val; lia). + rewrite Z.mod_small by lia. reflexivity. +Qed. + +(** Normalizing the shift-amount register through repr/unsigned is invisible + to the I32 shift operations (they only read the unsigned view). *) +Lemma shl_amt_norm : forall x y, + I32.shl x (I32.repr (I32.unsigned y)) = I32.shl x y. +Proof. + intros. unfold I32.shl. rewrite unsigned_repr_unsigned. reflexivity. +Qed. + +Lemma shru_amt_norm : forall x y, + I32.shru x (I32.repr (I32.unsigned y)) = I32.shru x y. +Proof. + intros. unfold I32.shru. rewrite unsigned_repr_unsigned. reflexivity. +Qed. + +Lemma shrs_amt_norm : forall x y, + I32.shrs x (I32.repr (I32.unsigned y)) = I32.shrs x y. +Proof. + intros. unfold I32.shrs. rewrite unsigned_repr_unsigned. reflexivity. +Qed. + +Lemma rotr_amt_norm : forall x y, + I32.rotr x (I32.repr (I32.unsigned y)) = I32.rotr x y. +Proof. + intros. unfold I32.rotr. rewrite unsigned_repr_unsigned. reflexivity. +Qed. + +(** *** Value bridges: AddWithCarry family *) + +(** SUB's AddWithCarry(x, NOT y, '1') result equals our I32.sub. *) +Lemma sail_sub_r_result_eq : forall x y, + sail_sub_r_result x y = I32.sub x y. +Proof. + intros. unfold sail_sub_r_result, sail_add_with_carry. + cbv beta iota zeta. cbn [fst]. + rewrite unsigned_not. apply repr_sub_unsigned. +Qed. + +(** SUB's flags are CMP's flags (same AddWithCarry call) — proven in round 1. *) +Lemma sail_sub_r_flags_eq : forall x y, + sail_sub_r_flags x y + = update_flags_arith (I32.sub x y) (compute_c_flag_sub x y) + (compute_v_flag_sub x y). +Proof. + exact sail_cmp_r_flags_eq. +Qed. + +(** CMN's flags are ADDS's flags (same AddWithCarry call) — round 1 again. *) +Lemma sail_cmn_r_flags_eq : forall x y, + sail_cmn_r_flags x y + = update_flags_arith (I32.add x y) (compute_c_flag_add x y) + (compute_v_flag_add x y (I32.add x y)). +Proof. + exact sail_add_r_flags_eq. +Qed. + +(** RSB's AddWithCarry(NOT x, y, '1') result equals our I32.sub y x. *) +Lemma sail_rsb_r_result_eq : forall x y, + sail_rsb_r_result x y = I32.sub y x. +Proof. + intros. unfold sail_rsb_r_result, sail_add_with_carry. + cbv beta iota zeta. cbn [fst]. + rewrite unsigned_not. apply repr_rsb_unsigned. +Qed. + +(** ADC's AddWithCarry(x, y, C) result equals our (x + y) + C. *) +Lemma sail_adc_r_result_eq : forall x y c, + sail_adc_r_result x y c + = I32.add (I32.add x y) (if c then I32.one else I32.zero). +Proof. + intros. destruct c; + unfold sail_adc_r_result, sail_add_with_carry; + cbv beta iota zeta; cbn [fst]; + unfold I32.add, I32.one, I32.zero, I32.repr, I32.unsigned; + rewrite mod3_add; rewrite <- Zplus_mod; reflexivity. +Qed. + +(** SBC's AddWithCarry(x, NOT y, C) result equals our (x - y) - NOT(C). *) +Lemma sail_sbc_r_result_eq : forall x y c, + sail_sbc_r_result x y c + = I32.sub (I32.sub x y) (if c then I32.zero else I32.one). +Proof. + intros. destruct c; + unfold sail_sbc_r_result, sail_add_with_carry; + cbv beta iota zeta; cbn [fst]; + rewrite unsigned_not. + - (* carry set: x + NOT y + 1 = x - y; subtracting zero renormalizes *) + rewrite repr_sub_unsigned. + unfold I32.sub, I32.zero, I32.repr, I32.unsigned. + rewrite (Z.mod_small 0) by (rewrite modulus_val; lia). + rewrite Z.sub_0_r. rewrite Zmod_mod. reflexivity. + - (* carry clear: x + NOT y + 0 = x - y - 1 *) + apply repr_sbc_borrow_unsigned. +Qed. + +(** *** Value bridges: flag-free ALU *) + +(** Sail's bits(32) AND on canonical representatives equals I32.and on raw + ones — mod 2^32 distributes over Z.land. *) +Lemma sail_and_r_eq : forall x y, sail_and_r x y = I32.and x y. +Proof. + intros. unfold sail_and_r, I32.and, I32.repr, I32.unsigned. + rewrite <- land_mod_modulus. apply Zmod_mod. +Qed. + +Lemma sail_orr_r_eq : forall x y, sail_orr_r x y = I32.or x y. +Proof. + intros. unfold sail_orr_r, I32.or, I32.repr, I32.unsigned. + rewrite <- lor_mod_modulus. apply Zmod_mod. +Qed. + +Lemma sail_eor_r_eq : forall x y, sail_eor_r x y = I32.xor x y. +Proof. + intros. unfold sail_eor_r, I32.xor, I32.repr, I32.unsigned. + rewrite <- lxor_mod_modulus. apply Zmod_mod. +Qed. + +(** *** Value bridges: Shift_C at amounts 1..31 *) + +Lemma sail_shift_c_lsl_eq : forall x n cin, + 0 < n < 32 -> + fst (sail_shift_c x SRType_LSL_t n cin) = I32.shl x (I32.repr n). +Proof. + intros x n cin Hn. unfold sail_shift_c. + destruct (Z.eqb_spec n 0); [lia |]. + unfold sail_lsl_c. cbn [fst]. + rewrite shl_repr_small by lia. + apply repr_shiftl_unsigned. lia. +Qed. + +Lemma sail_shift_c_lsr_eq : forall x n cin, + 0 < n < 32 -> + fst (sail_shift_c x SRType_LSR_t n cin) = I32.shru x (I32.repr n). +Proof. + intros x n cin Hn. unfold sail_shift_c. + destruct (Z.eqb_spec n 0); [lia |]. + unfold sail_lsr_c. cbn [fst]. + rewrite shru_repr_small by lia. reflexivity. +Qed. + +Lemma sail_shift_c_asr_eq : forall x n cin, + 0 < n < 32 -> + fst (sail_shift_c x SRType_ASR_t n cin) = I32.shrs x (I32.repr n). +Proof. + intros x n cin Hn. unfold sail_shift_c. + destruct (Z.eqb_spec n 0); [lia |]. + unfold sail_asr_c. cbn [fst]. + rewrite shrs_repr_small by lia. reflexivity. +Qed. + +Lemma sail_shift_c_ror_eq : forall x n cin, + 0 < n < 32 -> + fst (sail_shift_c x SRType_ROR_t n cin) = I32.rotr x (I32.repr n). +Proof. + intros x n cin Hn. unfold sail_shift_c. + destruct (Z.eqb_spec n 0); [lia |]. + unfold sail_ror_c. cbv zeta. cbn [fst]. + unfold I32.rotr. + rewrite unsigned_repr_small by (rewrite modulus_val; lia). + rewrite (Z.mod_small n 32) by lia. + rewrite shru_repr_small by lia. + rewrite shl_repr_small by lia. + rewrite (repr_shiftl_unsigned x (32 - n)) by lia. + reflexivity. +Qed. + +(** Shift_C at amount 0 is the identity on the value (raw representative). *) +Lemma sail_shift_c_zero : forall x t cin, + fst (sail_shift_c x t 0 cin) = x. +Proof. + intros. reflexivity. +Qed. + +(** *** Whole-instruction bridge theorems — AddWithCarry family *) + +(** SUB (register), setflags = false. Register write agrees EXACTLY. *) +Theorem sail_bridge_sub_reg : forall s rd rn rm, + exec_instr (SUB rd rn (Reg rm)) s + = Some (set_reg s rd (sail_sub_r_result (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_sub_r_result_eq. reflexivity. +Qed. + +(** SUBS (register): register write AND all four NZCV flags agree EXACTLY. *) +Theorem sail_bridge_subs_reg : forall s rd rn rm, + exec_instr (SUBS rd rn (Reg rm)) s + = Some (set_flags + (set_reg s rd (sail_sub_r_result (get_reg s rn) (get_reg s rm))) + (sail_sub_r_flags (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_sub_r_result_eq, sail_sub_r_flags_eq. reflexivity. +Qed. + +(** CMN (register): flags-only, all four NZCV agree EXACTLY. *) +Theorem sail_bridge_cmn_reg : forall s rn rm, + exec_instr (CMN rn (Reg rm)) s + = Some (set_flags s (sail_cmn_r_flags (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_cmn_r_flags_eq. reflexivity. +Qed. + +(** RSB (register), setflags = false (ArmSemantics.v has no RSBS). *) +Theorem sail_bridge_rsb_reg : forall s rd rn rm, + exec_instr (RSB rd rn (Reg rm)) s + = Some (set_reg s rd (sail_rsb_r_result (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_rsb_r_result_eq. reflexivity. +Qed. + +(** ADC (register), setflags = false: the carry_in is the LIVE C flag — + exactly what the i64 lo/hi pair codegen (ADDS;ADC) relies on. *) +Theorem sail_bridge_adc_reg : forall s rd rn rm, + exec_instr (ADC rd rn (Reg rm)) s + = Some (set_reg s rd + (sail_adc_r_result (get_reg s rn) (get_reg s rm) + (s.(flags).(flag_c)))). +Proof. + intros. rewrite sail_adc_r_result_eq. reflexivity. +Qed. + +(** SBC (register), setflags = false: borrow = NOT(C), the SUBS;SBC pair. *) +Theorem sail_bridge_sbc_reg : forall s rd rn rm, + exec_instr (SBC rd rn (Reg rm)) s + = Some (set_reg s rd + (sail_sbc_r_result (get_reg s rn) (get_reg s rm) + (s.(flags).(flag_c)))). +Proof. + intros. rewrite sail_sbc_r_result_eq. reflexivity. +Qed. + +(** *** Whole-instruction bridge theorems — flag-free ALU *) + +Theorem sail_bridge_and_reg : forall s rd rn rm, + exec_instr (AND rd rn (Reg rm)) s + = Some (set_reg s rd (sail_and_r (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_and_r_eq. reflexivity. +Qed. + +Theorem sail_bridge_orr_reg : forall s rd rn rm, + exec_instr (ORR rd rn (Reg rm)) s + = Some (set_reg s rd (sail_orr_r (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_orr_r_eq. reflexivity. +Qed. + +Theorem sail_bridge_eor_reg : forall s rd rn rm, + exec_instr (EOR rd rn (Reg rm)) s + = Some (set_reg s rd (sail_eor_r (get_reg s rn) (get_reg s rm))). +Proof. + intros. rewrite sail_eor_r_eq. reflexivity. +Qed. + +(** MVN (register): our MVN and the round-1 [sail_not] transcription are the + same Z-rendering — the bridge records the correspondence at the + instruction level. *) +Theorem sail_bridge_mvn_reg : forall s rd rm, + exec_instr (MVN rd (Reg rm)) s + = Some (set_reg s rd (sail_not (get_reg s rm))). +Proof. + intros. reflexivity. +Qed. + +(** *** Whole-instruction bridge theorems — shifts (immediate forms) *) + +Theorem sail_bridge_lsl_imm : forall s rd rm shift cin, + (0 < shift < 32)%nat -> + exec_instr (LSL rd rm shift) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rm) SRType_LSL_t + (Z.of_nat shift) cin))). +Proof. + intros. rewrite sail_shift_c_lsl_eq by lia. reflexivity. +Qed. + +Theorem sail_bridge_lsr_imm : forall s rd rm shift cin, + (0 < shift < 32)%nat -> + exec_instr (LSR rd rm shift) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rm) SRType_LSR_t + (Z.of_nat shift) cin))). +Proof. + intros. rewrite sail_shift_c_lsr_eq by lia. reflexivity. +Qed. + +Theorem sail_bridge_asr_imm : forall s rd rm shift cin, + (0 < shift < 32)%nat -> + exec_instr (ASR rd rm shift) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rm) SRType_ASR_t + (Z.of_nat shift) cin))). +Proof. + intros. rewrite sail_shift_c_asr_eq by lia. reflexivity. +Qed. + +(** ROR (immediate) is MOV (register) with shift_t = SRType_ROR (see the + provenance table: DecodeImmShift stype 0b11, imm5 <> 0). *) +Theorem sail_bridge_ror_imm : forall s rd rm shift cin, + (0 < shift < 32)%nat -> + exec_instr (ROR rd rm shift) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rm) SRType_ROR_t + (Z.of_nat shift) cin))). +Proof. + intros. rewrite sail_shift_c_ror_eq by lia. reflexivity. +Qed. + +(** *** Whole-instruction bridge theorems — shifts (register forms) + + Hypothesis 0 < UInt(R[s]) < 32 per gap 7: within it, the low-byte + extraction UInt(R[s]<7:0>) is the identity and Sail's shift agrees with + the mod-32 model. WASM lowerings always mask the amount first. *) + +Theorem sail_bridge_lsl_reg : forall s rd rn rs cin, + 0 < I32.unsigned (get_reg s rs) < 32 -> + exec_instr (LSL_reg rd rn rs) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rn) SRType_LSL_t + (sail_shift_amount8 (get_reg s rs)) cin))). +Proof. + intros s rd rn rs cin H. + unfold sail_shift_amount8. rewrite Z.mod_small by lia. + rewrite sail_shift_c_lsl_eq by lia. + rewrite shl_amt_norm. reflexivity. +Qed. + +Theorem sail_bridge_lsr_reg : forall s rd rn rs cin, + 0 < I32.unsigned (get_reg s rs) < 32 -> + exec_instr (LSR_reg rd rn rs) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rn) SRType_LSR_t + (sail_shift_amount8 (get_reg s rs)) cin))). +Proof. + intros s rd rn rs cin H. + unfold sail_shift_amount8. rewrite Z.mod_small by lia. + rewrite sail_shift_c_lsr_eq by lia. + rewrite shru_amt_norm. reflexivity. +Qed. + +Theorem sail_bridge_asr_reg : forall s rd rn rs cin, + 0 < I32.unsigned (get_reg s rs) < 32 -> + exec_instr (ASR_reg rd rn rs) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rn) SRType_ASR_t + (sail_shift_amount8 (get_reg s rs)) cin))). +Proof. + intros s rd rn rs cin H. + unfold sail_shift_amount8. rewrite Z.mod_small by lia. + rewrite sail_shift_c_asr_eq by lia. + rewrite shrs_amt_norm. reflexivity. +Qed. + +Theorem sail_bridge_ror_reg : forall s rd rn rs cin, + 0 < I32.unsigned (get_reg s rs) < 32 -> + exec_instr (ROR_reg rd rn rs) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rn) SRType_ROR_t + (sail_shift_amount8 (get_reg s rs)) cin))). +Proof. + intros s rd rn rs cin H. + unfold sail_shift_amount8. rewrite Z.mod_small by lia. + rewrite sail_shift_c_ror_eq by lia. + rewrite rotr_amt_norm. reflexivity. +Qed. + +(** *** Register shifts at amount 0 — unsigned-view agreement (gap 7) + + Shift_C returns the raw input; our shifts renormalize through repr. + The two agree on I32.unsigned — the observation WASM values make — + so the amount-0 case is bridged on that view. *) + +Theorem sail_bridge_lsl_reg_zero : forall s rd rn rs cin, + I32.unsigned (get_reg s rs) = 0 -> + exists s', + exec_instr (LSL_reg rd rn rs) s = Some s' + /\ I32.unsigned (get_reg s' rd) + = I32.unsigned (fst (sail_shift_c (get_reg s rn) SRType_LSL_t 0 cin)). +Proof. + intros s rd rn rs cin H. + eexists. split; [reflexivity |]. + rewrite get_set_reg_eq. + rewrite sail_shift_c_zero. + unfold I32.shl. rewrite H. + rewrite Z.mod_0_l by lia. + rewrite Z.shiftl_0_r. + unfold I32.unsigned, I32.repr. apply Zmod_mod. +Qed. + +Theorem sail_bridge_lsr_reg_zero : forall s rd rn rs cin, + I32.unsigned (get_reg s rs) = 0 -> + exists s', + exec_instr (LSR_reg rd rn rs) s = Some s' + /\ I32.unsigned (get_reg s' rd) + = I32.unsigned (fst (sail_shift_c (get_reg s rn) SRType_LSR_t 0 cin)). +Proof. + intros s rd rn rs cin H. + eexists. split; [reflexivity |]. + rewrite get_set_reg_eq. + rewrite sail_shift_c_zero. + unfold I32.shru. rewrite H. + rewrite Z.mod_0_l by lia. + rewrite Z.shiftr_0_r. + apply unsigned_repr_unsigned. +Qed. + +Theorem sail_bridge_asr_reg_zero : forall s rd rn rs cin, + I32.unsigned (get_reg s rs) = 0 -> + exists s', + exec_instr (ASR_reg rd rn rs) s = Some s' + /\ I32.unsigned (get_reg s' rd) + = I32.unsigned (fst (sail_shift_c (get_reg s rn) SRType_ASR_t 0 cin)). +Proof. + intros s rd rn rs cin H. + eexists. split; [reflexivity |]. + rewrite get_set_reg_eq. + rewrite sail_shift_c_zero. + unfold I32.shrs. rewrite H. + rewrite Z.mod_0_l by lia. + rewrite Z.shiftr_0_r. + unfold I32.unsigned at 1. unfold I32.repr. + rewrite Zmod_mod. apply signed_mod_modulus. +Qed. + +Theorem sail_bridge_ror_reg_zero : forall s rd rn rs cin, + I32.unsigned (get_reg s rs) = 0 -> + exists s', + exec_instr (ROR_reg rd rn rs) s = Some s' + /\ I32.unsigned (get_reg s' rd) + = I32.unsigned (fst (sail_shift_c (get_reg s rn) SRType_ROR_t 0 cin)). +Proof. + intros s rd rn rs cin H. + eexists. split; [reflexivity |]. + rewrite get_set_reg_eq. + rewrite sail_shift_c_zero. + unfold I32.rotr. cbv zeta. rewrite H. + rewrite Z.mod_0_l by lia. + rewrite Z.sub_0_r. + rewrite shru_repr_small by lia. + rewrite Z.shiftr_0_r. + (* shl x (repr 32): the mod-32 mask makes it a shift by 0 *) + unfold I32.shl. + assert (H32 : I32.unsigned (I32.repr 32) = 32) + by (apply unsigned_repr_small; rewrite modulus_val; lia). + rewrite H32. + rewrite Z_mod_same_full. + rewrite Z.shiftl_0_r. + unfold I32.or, I32.unsigned, I32.repr. + rewrite !Zmod_mod. + rewrite Z.lor_diag. + apply Zmod_mod. +Qed. + +(** *** Whole-instruction bridge theorems — moves *) + +(** MOV (register) is MOV_r with shift_t = SRType_LSL, shift_n = 0: the + result is the Shift_C identity on R[m]. *) +Theorem sail_bridge_mov_reg : forall s rd rm cin, + exec_instr (MOV rd (Reg rm)) s + = Some (set_reg s rd + (fst (sail_shift_c (get_reg s rm) SRType_LSL_t 0 cin))). +Proof. + intros. reflexivity. +Qed. + +(** MOVW: MOV (immediate) with result = imm32 (gap 9: our MOVW carries the + already-expanded imm32, so the execute clause is the identity on it). *) +Theorem sail_bridge_movw : forall s rd imm, + exec_instr (MOVW rd imm) s = Some (set_reg s rd imm). +Proof. + intros. reflexivity. +Qed. + +(** MOVT bitfield-insert equals our AND/OR/SHL formulation, for encodable + (16-bit) immediates. *) +Lemma sail_movt_result_eq : forall old imm, + 0 <= I32.unsigned imm < 65536 -> + sail_movt_result old imm + = I32.or (I32.and old (I32.repr 0xFFFF)) (I32.shl imm (I32.repr 16)). +Proof. + intros old imm Himm. + (* the AND mask: Z.land old 0xFFFF = old mod 65536 (Z.land_ones) *) + assert (HA : Z.land old (I32.repr 65535) = old mod 65536). + { change (I32.repr 65535) with (Z.ones 16). + rewrite Z.land_ones by lia. + change (2 ^ 16) with 65536. reflexivity. } + (* low half: (old mod 2^32) mod 2^16 = old mod 2^16 *) + assert (Hlow : I32.unsigned old mod 65536 = old mod 65536). + { unfold I32.unsigned, I32.modulus. + change 65536 with (2 ^ 16). + rewrite <- !Z.land_ones by lia. + rewrite <- Z.land_assoc. + change (Z.land (Z.ones 32) (Z.ones 16)) with (Z.ones 16). + reflexivity. } + (* high half: shifting the canonical representative = shifting raw *) + assert (HC : I32.shl imm (I32.repr 16) + = I32.repr (Z.shiftl (I32.unsigned imm) 16)). + { rewrite shl_repr_small by lia. + symmetry. apply repr_shiftl_unsigned. lia. } + assert (Hb : 0 <= old mod 65536 < 65536) + by (apply Z.mod_pos_bound; lia). + unfold sail_movt_result, I32.or, I32.and. + rewrite HC, HA, Hlow. + unfold I32.repr. + rewrite (Z.mod_small (old mod 65536)) by (rewrite modulus_val; lia). + rewrite (Z.mod_small (Z.shiftl (I32.unsigned imm) 16)) + by (rewrite Z.shiftl_mul_pow2 by lia; + change (2 ^ 16) with 65536; rewrite modulus_val; lia). + rewrite Z.lor_comm. reflexivity. +Qed. + +(** MOVT: the destination's high half becomes imm16, low half preserved. *) +Theorem sail_bridge_movt : forall s rd imm, + 0 <= I32.unsigned imm < 65536 -> + exec_instr (MOVT rd imm) s + = Some (set_reg s rd (sail_movt_result (get_reg s rd) imm)). +Proof. + intros. rewrite sail_movt_result_eq by auto. reflexivity. +Qed. diff --git a/docs/design/vcr-isa-001-spike.md b/docs/design/vcr-isa-001-spike.md index d23c723a..a02b71ad 100644 --- a/docs/design/vcr-isa-001-spike.md +++ b/docs/design/vcr-isa-001-spike.md @@ -1,5 +1,11 @@ # VCR-ISA-001 Feasibility Spike — Sail/ASL-derived ARM semantics (2026-07-08) +> **Status update (round 2, same day):** the spike's priority list items (1) +> and (2) — the remaining AddWithCarry family and the flag-free ALU/shift +> class — plus the MOV/MOVW/MOVT stretch are now landed in the same file. +> `SailArmBridge.v` stands at **81 Qed / 0 Admitted / 0 new axioms** +> (was 23). See §6 for the coverage table and measured round-2 cost. + **Verdict: GO — but on the transcribe-and-bridge path, not the import path.** Importing the Sail-generated Rocq model wholesale is a no-go at synth's scale (measured below). Hand-transcribing the Sail execute semantics per instruction @@ -127,9 +133,45 @@ needs a deliberate abstraction statement, not a mechanical bridge). alive) and REFUTED for the generated-ARM-artifact path, with the working alternative landed in-tree. +## 6. Round 2 — coverage table + measured cost (2026-07-08) + +Executed per the §5 priority list, items (1) and (2), plus the moves stretch. +Same pin (sail-arm @ `1bf2e5574ba9`), same pattern: verbatim-quoted execute +clause with file:line, hand transcription, bridge lemma vs `exec_instr`, Qed. + +| Op class | Instructions | Bridge form | Status | +|---|---|---|---| +| AddWithCarry family (round 1) | ADD, ADDS, CMP (register) | exact state (reg + all 4 NZCV) | Qed (23) | +| AddWithCarry family (round 2) | SUB, SUBS, CMN, RSB, **ADC, SBC** (register) | exact state; SUBS = reg + all 4 NZCV; ADC/SBC carry_in = live C flag | Qed | +| Flag-free ALU | AND, ORR, EOR, MVN (register) | exact state (setflags=false; no ANDS/… in our model) | Qed | +| Shifts, immediate | LSL/LSR/ASR/ROR #1..31 (via Shift_C + LSL_C/LSR_C/ASR_C/ROR_C transcriptions) | exact state under 1 ≤ shift_n ≤ 31 | Qed | +| Shifts, register | LSL/LSR/ASR/ROR reg-amount (UInt(R[s]<7:0>)) | exact state under 0 < UInt(R[s]) < 32; amount = 0 bridged on the unsigned view | Qed | +| Moves | MOV (register), MOVW, MOVT (UInt(imm16) < 2^16) | exact state | Qed | +| NOT COVERED | MUL/MLA/MLS/UMULL, SDIV/UDIV, CLZ/RBIT (axiomatized our side), loads/stores, branches/PC, IT blocks, RRX, BIC (absent from ArmSemantics.v) | — | future increments | + +**Measured round-2 cost:** one working session (~half a day wall-clock) for +six-plus op classes — well under the §3 estimate of 0.5–1 day *per class*. +The §3 amortization claim held exactly: SUB/SUBS/CMN/RSB reused the round-1 +AddWithCarry + flag lemmas nearly for free (SUB's flags ARE CMP's flags — +one `exact`), and ADC/SBC needed only two ~10-line mod-arithmetic lemmas. +The genuinely new machinery was (a) mod-2^32 distribution over +`Z.land/Z.lor/Z.lxor` (three testbit-extensionality lemmas) for the ALU +class, and (b) the `Shift_C` transcription with its four `*_C` primitives +including the shifter carry-out (transcribed faithfully; unused by the +bridges because our model has no flag-setting shifts — recorded as gap 5). + +**Findings (the bridge earning its keep):** two real divergences between +ArmSemantics.v and the ASL, both documented in-file as gaps 6-7: +LSR/ASR #32 (imm5 = 00000 encodes shift 32; our mod-32 model computes a +shift by 0 where ARM zero/sign-fills) and register-controlled amounts ≥ 32 +(ARM uses the low byte, 32..255 saturate; our model masks mod 32). 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. + ## Artifacts -- `coq/Synth/ARM/SailArmBridge.v` — 23 Qed / 0 Admitted, in - `//coq:verify_proofs` (green). +- `coq/Synth/ARM/SailArmBridge.v` — 81 Qed / 0 Admitted / 0 new axioms + (round 1: 23), in `//coq:verify_proofs` (green). - `coq/BUILD.bazel` `:sail_arm_bridge`, `coq/_CoqProject` entry. - This report.