Skip to content

Commit 219a90c

Browse files
PetarMaxdtumadGZGavinZhaoPetar Maksimovic
authored
64-bit ALU Verification, Part I (#70)
* initial changes * working build * finish updating bitwise and jal * build errors * revert sail change * outline mul operation * import missing * divRem and lt * organize files * fixes * some add proof * add ITypeReader * add AddiChip * add AddwOperation * add AddwChip * add ShiftLeftChip * add ShiftRightChip * add SubOperation * add SubChip * add SubwOperation * add SubwChip * working add op * fix add chip * feat: import RV64IM (#48) * import RV64IM * revert to regidx from SailM after BitVec instance fix * basic JAL outline with sailM * slightly less axiomatic * break out lemmas * Sync DivRemChip * python script to sync constraints * sync Operations * sync Compare * sync Readers * toStateProp with SailState * AirInteraction::Program for trusted properties * sync Reader AirInteraction::program * Sync JalrChip * Jalr LHS * pc valid limbs assumption * reusable simpM for monad simp * b_is_u64 from reader_cstrs * strip some whitespace for vim jumping * reduction to hash map inserts * not x0 case map ready except bit access * not x0 case except bitvec * fix some is_U64 sorrys * small cleanup * is x0 case pending x0 read/write handling * return 0 when read_reg * move simpM * match working case 0 and 1 * SailState.get_reg?_is_rX proof * correct write when op_a is not x0 * use the correct write behavior * well actually arg 2 is the match input * establish wX_bits with regidx_write * not x0 case correct write behavior * is x0 case op_a = 0 proof * op_b + imm divides 4 proof * incorporate op_b_val_plus_imm and state InteractionKind::Program constraints * mul4 BB and BitVec helpers * some sailM lemmas * working build * op_a_one case * most of a full proof * more general mul4 constraints * jalr sorry-less proof except misa * more jal * missing modulus * sorry-less AddOperation proof * remove wrong BitVec lemma * SailState.sp1_no_misa axiom * Jalr proof with correct signExtend * slightly better slightly worse * slightly better slightly worse * minor cleanup, partial proofs * EStateM lemmas * build error * proof of insert_insert_insert_cancel * axiom situation * working through more jalr cleanup * setup AddChip proof * clean jalr * swap jalr * proof of AddChip * ADDW * project-wide mcp setup for subtrees/workspaces * i_type Program assumptions * corrected i_type * trusted_instr for ADDW * more Program assumptions * JAL calculate imm with Nat to prevent BB overflow * u_type prevent overflow as well with Nat * no need op_c_(0|1) constraints in ADDIW case * shift w * u_type should only constrain op_b * ECALL and EBREAK * corrected ADDW * shift w no redundant op_b * catch stray LWU * M extension is just r_type * ADDW is just r_type or i_type * correct mixed up w_shift and shift * correct JAL/j_type * some commenting * ADDIW * streamlining proofs * streamlining ...W proofs * modular specifications * simpler Jalr proof * simpler Jal proof * LT opcodes * SLL * SLLs with sorried-out proofs * SR partly working, SL needs fixing * SL revisited * SL revisited - correction * SL revisited - correction * all SRA opcodes * full proofs for shifts * spec_sub * others_sub * Bitwise chips and infrastructure * Bitwise operations * all proofs except mul and divrem * initial mul reasoning * MulOperation * Restoring powers * Mul * bhword and core_mulw * better MUL proofs * minor corrections * mul operation with U64, some grind and aesop * some further automation and a bit of DivRem --------- Co-authored-by: Devon Tuma <[email protected]> Co-authored-by: Gavin Zhao <[email protected]> Co-authored-by: Petar Maksimovic <[email protected]>
1 parent 22692de commit 219a90c

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

64 files changed

+9863
-2236
lines changed

‎SP1Chips/AddChip.lean‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ variable
1818

1919
def spec_add (rs2 rs1 rd : regidx) : SailM Unit := do
2020
Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
21-
_ ← execute_RTYPE rs2 rs1 rd rop.ADD
21+
_ ← execute (.RTYPE (rs2, rs1, rd, rop.ADD))
2222
pure ()
2323

2424
def sp1_op_a : BitVec 5 :=
@@ -68,38 +68,40 @@ def sp1_op_c : BitVec 5 :=
6868

6969
def sp1_add : SailM Unit := do
7070
let op_a := sp1_op_a Main cstrs h_is_real
71-
Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3], Main[4], Main[5], 0] + 4)
71+
Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
7272
Sail.write_reg op_a (Word.toBitVec64 #v[Main[28], Main[29], Main[30], Main[31]])
7373

7474
open Sail
7575

76-
theorem correct
76+
set_option pp.parens true in
77+
theorem correct_add
7778
(state_cstrs : (constraints Main).initialState s) :
7879
let op_c := sp1_op_c Main cstrs h_is_real
7980
let op_b := sp1_op_b Main cstrs h_is_real
8081
let op_a := sp1_op_a Main cstrs h_is_real
8182
(spec_add (.Regidx op_c) (.Regidx op_b) (.Regidx op_a)).run s = (sp1_add Main cstrs h_is_real).run s
8283
:= by
83-
-- Obtain and simplify state and pure constraints
8484
simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddOperation.constraints, CPUState.constraints, RTypeReader.constraints, h_is_real] at state_cstrs
8585
obtain ⟨read_pc, trusted_instr_state, _, read_op_b, read_op_c⟩ := state_cstrs
8686
simp [constraints] at cstrs
8787
obtain ⟨add_op_cstrs, cpu_cstrs, reader_cstrs, rest⟩ := cstrs
88-
apply AddOperation.correct (h_is_real := h_is_real) at add_op_cstrs
8988
rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
9089
rw [RTypeReader.allHold_constraints_iff_is_real h_is_real] at reader_cstrs
9190
obtain ⟨ trusted_instr_prop, _, _, _, _, _, _, ⟨ ⟨ _, _, ⟨ _, is_U64_b, is_U64_c ⟩ ⟩, _ ⟩⟩ := reader_cstrs
9291
simp [Opcode.ofNat, Nat.ble] at trusted_instr_state trusted_instr_prop
93-
specialize add_op_cstrs is_U64_b is_U64_c
92+
93+
rw [h_is_real] at *
94+
apply AddOperation.spec is_U64_b is_U64_c at add_op_cstrs
9495
obtain ⟨ is_U64_val, is_add ⟩ := add_op_cstrs
9596
simp at *
9697

9798
-- Now the monadic manipulation
98-
simp [spec_add, sp1_add, execute_RTYPE]
99+
simp [spec_add, sp1_add, execute, execute_RTYPE']
99100
rw [run_readReg, read_pc]
100101
simp [sp1_op_b, read_op_b (by omega)]
101102
simp [sp1_op_c, read_op_c (by omega)]
102103
simp [sp1_op_a]
104+
rw [BabyBear.add4_into_pc_ofNat (by omega)]
103105

104106
by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
105107
. rw [← is_add]

‎SP1Chips/AddiChip.lean‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,101 @@ import SP1Operations.Operation.AddOperation
22
import SP1Operations.Reader.CPUState
33
import SP1Operations.Reader.ITypeReader
44
import SP1Chips.Addi.Constraints
5+
6+
import SP1Chips.Add.Constraints
7+
8+
open LeanRV64IM.Functions BitVec
9+
10+
namespace Addi
11+
12+
variable
13+
(Main : Vector (Fin BB) 30)
14+
(s : SailState)
15+
(cstrs : (constraints Main).allHold)
16+
(h_is_real : Main[29] = 1)
17+
18+
def spec_addi (imm : BitVec 12) (rs1 rd : regidx) : SailM Unit := do
19+
Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
20+
_ ← execute (.ITYPE (imm, rs1, rd, iop.ADDI))
21+
pure ()
22+
23+
def sp1_op_a : BitVec 5 :=
24+
by
25+
refine BitVec.ofNatLT Main[6] ?_
26+
simp
27+
show Main[6] < 32
28+
29+
have reader_cstrs := by
30+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
31+
exact cstrs.2.2.1
32+
33+
clear cstrs
34+
simp [ITypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at reader_cstrs
35+
36+
exact reader_cstrs.1.2.1
37+
38+
def sp1_op_b : BitVec 5 :=
39+
by
40+
refine BitVec.ofNatLT Main[14] ?_
41+
simp
42+
show Main[14] < 32
43+
44+
have reader_cstrs := by
45+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
46+
exact cstrs.2.2.1
47+
48+
clear cstrs
49+
simp [ITypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at reader_cstrs
50+
51+
exact reader_cstrs.1.1.1
52+
53+
def sp1_op_c : BitVec 12 := BitVec.ofNat 12 Main[21].val
54+
55+
def sp1_addi : SailM Unit := do
56+
let op_a := sp1_op_a Main cstrs h_is_real
57+
Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
58+
Sail.write_reg op_a (Word.toBitVec64 #v[Main[25], Main[26], Main[27], Main[28]])
59+
60+
open Sail
61+
62+
theorem correct_addi
63+
(state_cstrs : (constraints Main).initialState s) :
64+
let op_c := sp1_op_c Main
65+
let op_b := sp1_op_b Main cstrs h_is_real
66+
let op_a := sp1_op_a Main cstrs h_is_real
67+
(spec_addi op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addi Main cstrs h_is_real).run s
68+
:= by
69+
-- Obtain and simplify state and pure constraints
70+
simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddOperation.constraints, CPUState.constraints, ITypeReader.constraints, h_is_real] at state_cstrs
71+
obtain ⟨read_pc, trusted_instr_state, read_op_b, read_op_c⟩ := state_cstrs
72+
simp [constraints] at cstrs
73+
obtain ⟨add_op_cstrs, cpu_cstrs, reader_cstrs, rest⟩ := cstrs
74+
rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
75+
rw [ITypeReader.allHold_constraints_iff_is_real h_is_real] at reader_cstrs
76+
obtain ⟨ trusted_instr_prop, _, _, c0, c1, c2, c3, _, _, _, _, _, _, _, _, _, _, ⟨ is_U64_a, is_U64_b, _ ⟩⟩ := reader_cstrs
77+
simp_all [Opcode.ofNat, Nat.ble]
78+
have is_U64_c : Word.isU64 #v[Main[21], Main[22], Main[23], Main[24]]
79+
:= by apply Word.isU64_of_cases c0 c1 c2 c3
80+
81+
rw [h_is_real] at *
82+
apply AddOperation.spec is_U64_b is_U64_c at add_op_cstrs
83+
obtain ⟨ is_U64_val, is_add ⟩ := add_op_cstrs
84+
simp at *
85+
86+
-- Now the monadic manipulation
87+
simp [spec_addi, sp1_addi, execute, execute_ITYPE]
88+
rw [run_readReg, read_pc]
89+
simp [sp1_op_b, read_op_b]
90+
simp [sp1_op_c, read_op_c]
91+
simp [sp1_op_a]
92+
rw [BabyBear.add4_into_pc_ofNat (by omega)]
93+
94+
by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
95+
. rw [← is_add]
96+
simp [Word.toBitVec64, Word.toNat]
97+
. rw [if_neg (by simpa [← BitVec.toNat_inj])]
98+
rw [if_neg (by simpa [← BitVec.toNat_inj])]
99+
simp [Word.toBitVec64, Word.toNat]
100+
rfl
101+
102+
end Addi

‎SP1Chips/AddwChip.lean‎

Lines changed: 224 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,227 @@ import SP1Operations.Operation.AddwOperation
22
import SP1Operations.Reader.CPUState
33
import SP1Operations.Reader.ALUTypeReader
44
import SP1Chips.Addw.Constraints
5+
6+
open LeanRV64IM.Functions
7+
open BitVec
8+
9+
namespace Addw
10+
11+
variable
12+
(Main : Vector (Fin BB) 37)
13+
(s : SailState)
14+
(cstrs : (constraints Main).allHold)
15+
(h_is_real : Main[35] = 1)
16+
(h_is_addw : Main[31] = 0)
17+
18+
def spec_addw (rs2 rs1 rd : regidx) : SailM Unit := do
19+
Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
20+
_ ← execute_RTYPEW rs2 rs1 rd ropw.ADDW
21+
pure ()
22+
23+
def sp1_op_a : BitVec 5 :=
24+
by
25+
refine BitVec.ofNatLT Main[6] ?_
26+
simp
27+
show Main[6] < 32
28+
29+
have alu_cstrs := by
30+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
31+
exact cstrs.2.2.1
32+
33+
clear cstrs
34+
simp [ALUTypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at alu_cstrs
35+
36+
exact alu_cstrs.1.2.1
37+
38+
def sp1_op_b : BitVec 5 :=
39+
by
40+
refine BitVec.ofNatLT Main[14] ?_
41+
simp
42+
show Main[14] < 32
43+
44+
have alu_cstrs := by
45+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
46+
exact cstrs.2.2.1
47+
48+
clear cstrs
49+
have : (Main[31] = 0 ∨ Main[31] = 1) := by
50+
simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
51+
aesop
52+
53+
simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
54+
rcases this <;> simp_all
55+
56+
def sp1_op_c : BitVec 5 :=
57+
by
58+
refine BitVec.ofNatLT Main[21] ?_
59+
simp
60+
show Main[21] < 32
61+
62+
have alu_cstrs := by
63+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
64+
exact cstrs.2.2.1
65+
66+
clear cstrs
67+
simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble, h_is_addw] at alu_cstrs
68+
69+
exact alu_cstrs.1.2.1
70+
71+
def sp1_addw : SailM Unit := do
72+
let op_a := sp1_op_a Main cstrs h_is_real
73+
Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
74+
Sail.write_reg op_a (Word.toBitVec64 #v[Main[32], Main[33], Main[34] * 65535, Main[34] * 65535])
75+
76+
set_option maxHeartbeats 1000000 in
77+
theorem correct_addw
78+
(state_cstrs : (constraints Main).initialState s)
79+
(h_is_addw : Main[31] = 0) :
80+
let op_c := sp1_op_c Main cstrs h_is_real h_is_addw
81+
let op_b := sp1_op_b Main cstrs h_is_real h_is_addw
82+
let op_a := sp1_op_a Main cstrs h_is_real
83+
(spec_addw (.Regidx op_c) (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addw Main cstrs h_is_real).run s
84+
:= by
85+
simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddwOperation.constraints, CPUState.constraints, ALUTypeReader.constraints, U16MSBOperation.constraints, h_is_real] at state_cstrs
86+
obtain ⟨read_pc, trusted_instr_state, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
87+
simp [constraints] at cstrs
88+
obtain ⟨addw_op_cstrs, cpu_cstrs, alu_cstrs, _, _⟩ := cstrs
89+
rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
90+
rw [ALUTypeReader.allHold_constraints_iff_is_real h_is_real] at alu_cstrs
91+
obtain ⟨ trusted_instr_prop, _, _, _, _, _, _, _, _, _, _, _, _, _, _, is_U64_a, is_U64_b, is_U64_c , _, _ ⟩ := alu_cstrs
92+
simp [Opcode.ofNat, Nat.ble] at *
93+
simp_all
94+
obtain ⟨ _, _, is_U64_c ⟩ := is_U64_c
95+
96+
rw [h_is_real] at *
97+
apply AddwOperation.spec is_U64_b is_U64_c at addw_op_cstrs
98+
obtain ⟨ is_U32_val, is_addw, is_msb ⟩ := addw_op_cstrs
99+
simp_all
100+
101+
-- Now the monadic manipulation
102+
simp [spec_addw, sp1_addw, execute, execute_RTYPEW']
103+
rw [Sail.run_readReg, read_pc]
104+
simp [sp1_op_a, sp1_op_b, sp1_op_c, read_op_b, read_op_c]
105+
rw [exec_RTYPEW_pure_bv_to_w _ _ _ (by omega) (by omega)]
106+
simp [execute_RTYPEW_pure_w]
107+
rw [← is_addw] at is_msb
108+
rw [BabyBear.add4_into_pc_ofNat (by omega)]
109+
110+
by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
111+
. simp [Word.toBitVec64, Word.toNat]
112+
. rw [if_neg (by simpa [← BitVec.toNat_inj])]
113+
rw [if_neg (by simpa [← BitVec.toNat_inj])]
114+
simp [Word.toBitVec64, Word.toNat]
115+
rw [← is_addw]; congr
116+
rw [HWord.sign_extend_32_to_64_msb is_U32_val]
117+
simp [Word.toBitVec64, Word.toNat]
118+
119+
end Addw
120+
121+
namespace Addiw
122+
123+
open Addw
124+
125+
variable
126+
(Main : Vector (Fin BB) 37)
127+
(s : SailState)
128+
(cstrs : (constraints Main).allHold)
129+
(h_is_real : Main[35] = 1)
130+
(h_is_addiw : Main[31] = 1)
131+
132+
def spec_addiw (imm : BitVec 12) (rs1 rd : regidx) : SailM Unit := do
133+
Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
134+
_ ← execute_ADDIW imm rs1 rd
135+
pure ()
136+
137+
def sp1_op_a : BitVec 5 :=
138+
by
139+
refine BitVec.ofNatLT Main[6] ?_
140+
simp
141+
show Main[6] < 32
142+
143+
have alu_cstrs := by
144+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
145+
exact cstrs.2.2.1
146+
147+
clear cstrs
148+
simp [ALUTypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at alu_cstrs
149+
150+
exact alu_cstrs.1.2.1
151+
152+
def sp1_op_b : BitVec 5 :=
153+
by
154+
refine BitVec.ofNatLT Main[14] ?_
155+
simp
156+
show Main[14] < 32
157+
158+
have alu_cstrs := by
159+
simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
160+
exact cstrs.2.2.1
161+
162+
clear cstrs
163+
have : (Main[31] = 0 ∨ Main[31] = 1) := by
164+
simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
165+
aesop
166+
167+
simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
168+
rcases this <;> simp_all
169+
170+
def sp1_op_c : BitVec 12 := BitVec.ofNat 12 Main[21].val
171+
172+
def sp1_addiw : SailM Unit := do
173+
let op_a := sp1_op_a Main cstrs h_is_real
174+
-- TODO(gzgz): we can obtain this from the constraint compiler
175+
-- This comes from the Interaction.state in CPUState
176+
Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
177+
Sail.write_reg op_a (Word.toBitVec64 #v[Main[32], Main[33], Main[34] * 65535, Main[34] * 65535])
178+
179+
set_option maxHeartbeats 1000000 in
180+
theorem correct_addw
181+
(state_cstrs : (constraints Main).initialState s) :
182+
let op_c := sp1_op_c Main
183+
let op_b := sp1_op_b Main cstrs h_is_real h_is_addiw
184+
let op_a := sp1_op_a Main cstrs h_is_real
185+
(spec_addiw op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addiw Main cstrs h_is_real).run s
186+
:= by
187+
-- Obtain and simplify state and pure constraints
188+
simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddwOperation.constraints, CPUState.constraints, ALUTypeReader.constraints, U16MSBOperation.constraints, h_is_real] at state_cstrs
189+
obtain ⟨read_pc, trusted_instr_state, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
190+
simp [constraints] at cstrs
191+
obtain ⟨addw_op_cstrs, cpu_cstrs, alu_cstrs, _, _⟩ := cstrs
192+
rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
193+
rw [ALUTypeReader.allHold_constraints_iff_is_real h_is_real] at alu_cstrs
194+
obtain ⟨ trusted_instr_prop, _, _, ⟨ c0, c1, c2, c3 ⟩, _, _, _, _, _, _, _, _, _, _, _, is_U64_a, is_U64_b, _, _, _ ⟩ := alu_cstrs
195+
simp [Opcode.ofNat, Nat.ble] at *
196+
simp_all
197+
have is_U64_c : Word.isU64 #v[Main[21], Main[22], Main[23], Main[24]]
198+
:= by apply Word.isU64_of_cases c0 c1 c2 c3
199+
200+
rw [h_is_real] at *
201+
apply AddwOperation.spec is_U64_b is_U64_c at addw_op_cstrs
202+
obtain ⟨ is_U32_val, is_addw, is_msb ⟩ := addw_op_cstrs
203+
simp_all
204+
205+
obtain ⟨ h_f, h_imm_c ⟩ := trusted_instr_prop
206+
simp [h_is_addiw] at h_f h_imm_c
207+
obtain ⟨ h_c, h_is_imm_c ⟩ := h_imm_c
208+
209+
-- Now the monadic manipulation
210+
simp [spec_addiw, sp1_addiw, execute, execute_ADDIW']
211+
rw [Sail.run_readReg, read_pc]
212+
simp [sp1_op_a, sp1_op_b, sp1_op_c, read_op_b]
213+
rw [← h_is_imm_c]
214+
rw [exec_RTYPEW_pure_bv_to_w _ _ _ (by omega) (by omega)]
215+
simp [execute_RTYPEW_pure_w]
216+
rw [← is_addw] at is_msb
217+
rw [BabyBear.add4_into_pc_ofNat (by omega)]
218+
219+
by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
220+
. simp [Word.toBitVec64, Word.toNat]
221+
. rw [if_neg (by simpa [← BitVec.toNat_inj])]
222+
rw [if_neg (by simpa [← BitVec.toNat_inj])]
223+
simp [Word.toBitVec64, Word.toNat]
224+
rw [← is_addw]; congr
225+
rw [HWord.sign_extend_32_to_64_msb is_U32_val]
226+
simp [Word.toBitVec64, Word.toNat]
227+
228+
end Addiw

0 commit comments

Comments
 (0)