| import CM0.Run |
|
|
| /-! |
| |
|
|
| Division on a core without a divide instruction, proved. ARMv6-M has no `udiv`/`sdiv`, so the |
| lowering divides with the loop `udivCode` (restoring division, one quotient bit per round): |
|
|
| r2 := 0 |
| loop: if (r0 >>> r3) ≥ r1 then { r0 := r0 - (r1 <<< r3) |
| if r3 = 0 then exit |
|
|
| * `udiv_loop`: the invariant. Before the round for bit `i`, `a = r2 · b + r0` and |
| `r0 < b · 2^(i+1)` (as natural numbers). A round keeps it for `i - 1`: the test |
| `(r0 >>> i) ≥ b` is `r0 ≥ b · 2^i`, and when it holds `b <<< i` and `r2 + 2^i` do not wrap. |
| After the round for bit 0, `r0 < b`, so `r2 = a / b`. |
| * `udiv_seq`: `udivSeq` leaves `a.udiv b` in `r0`. |
| * `sdiv_seq`: `sdivSeq` leaves `a.sdiv b` in `r0`: it divides the absolute values and negates |
| when the signs differ, which is `BitVec.sdiv` case by case on the two sign bits. |
|
|
| Each sequence changes only scratch registers (`r0 r1 r2 r3 r7 r10`) and no memory. |
| -/ |
|
|
| namespace WordDialect |
| namespace CM0 |
|
|
| open Reg |
|
|
| /-- The registers a division sequence may change. -/ |
| def DivScratch (r : Reg) : Prop := r = r0 ∨ r = r1 ∨ r = r2 ∨ r = r3 ∨ r = r7 ∨ r = r10 |
|
|
| /-- The registers the loop `udivCode` changes. -/ |
| def LoopScratch (r : Reg) : Prop := r = r0 ∨ r = r2 ∨ r = r3 ∨ r = r7 |
|
|
| theorem zero_sle (x : W) : (0#32).sle x = !x.msb := by |
| rw [BitVec.sle_eq_decide, BitVec.msb_eq_toInt] |
| by_cases h : x.toInt < 0 < |
|
|
| theorem toNat_ofNat_lt {i : Nat} (h : i < 2 ^ 32) : (BitVec.ofNat 32 i).toNat = i := by |
| simp [BitVec.toNat_ofNat, Nat.mod_eq_of_lt h] |
|
|
| theorem ofNat_m1 : BitVec.ofInt 32 (-1) = BitVec.ofNat 32 (2 ^ 32 - 1) := by decide |
|
|
| theorem ofNat_pred {i : Nat} (h0 : 0 < i) (h : i < 2 ^ 32) : |
| BitVec.ofNat 32 i + BitVec.ofInt 32 (-1) = BitVec.ofNat 32 (i - 1) := by |
| rw [ofNat_m1, ← BitVec.ofNat_add] |
| apply BitVec.eq_of_toNat_eq |
| simp only [BitVec.toNat_ofNat] |
| omega |
|
|
| theorem ofNat_eq_zero {i : Nat} (h : i < 2 ^ 32) : BitVec.ofNat 32 i = 0#32 ↔ i = 0 := by |
| constructor |
| · intro e |
| · rintro rfl |
|
|
| /-- The comparison in a round: `(r >>> i) <u b` exactly when `r < b · 2^i`. -/ |
| theorem ult_shift (r b : W) (i : Nat) : |
| (r >>> i).ult b = decide (r.toNat < b.toNat * 2 ^ i) := by |
| simp only [BitVec.ult, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow] |
| exact decide_eq_decide.mpr (Nat.div_lt_iff_lt_mul (Nat.two_pow_pos i)) |
|
|
| theorem shl_toNat_of_le (b : W) (i : Nat) (h : b.toNat * 2 ^ i < 2 ^ 32) : |
| (b <<< i).toNat = b.toNat * 2 ^ i := by |
| simp [BitVec.toNat_shiftLeft, Nat.shiftLeft_eq, Nat.mod_eq_of_lt h] |
|
|
| theorem sub_toNat_of_le (r t : W) (h : t.toNat ≤ r.toNat) : (r - t).toNat = r.toNat - t.toNat := by |
| rw [BitVec.toNat_sub] |
| have := r.isLt |
| omega |
|
|
| theorem add_toNat_of_lt (q t : W) (h : q.toNat + t.toNat < 2 ^ 32) : |
| (q + t).toNat = q.toNat + t.toNat := by |
| rw [BitVec.toNat_add, Nat.mod_eq_of_lt h] |
|
|
| section Loop |
|
|
| variable {code : List (Instr Nat)} {q : Nat} |
|
|
| /-- One round, from the top of the loop (index `q + 2`) to the loop test (index `q + 11`), for |
| bit `i`: it keeps `a = r2 · b + r0` and brings `r0` below `b · 2^i`. -/ |
| theorem udiv_round |
| (f2 : code[q + 2]? = some (.movRR r7 r0)) (f3 : code[q + 3]? = some (.lsr r7 r3)) |
| (f4 : code[q + 4]? = some (.bcc .ult r7 r1 (q + 11))) (f5 : code[q + 5]? = some (.movRR r7 r1)) |
| (f6 : code[q + 6]? = some (.lsl r7 r3)) (f7 : code[q + 7]? = some (.sub r0 r7)) |
| (f8 : code[q + 8]? = some (.movImm r7 1#32)) (f9 : code[q + 9]? = some (.lsl r7 r3)) |
| (f10 : code[q + 10]? = some (.add r2 r7)) |
| {b : W} (hbpos : 0 < b.toNat) {a : Nat} (ha : a < 2 ^ 32) {i : Nat} (hi : i < 32) {m : M} |
| (hpc : m.pc = q + 2) (h1 : m.regs r1 = b) (h3 : m.regs r3 = BitVec.ofNat 32 i) |
| (hinv : a = (m.regs r2).toNat * b.toNat + (m.regs r0).toNat) |
| (hlt : (m.regs r0).toNat < b.toNat * 2 ^ (i + 1)) : |
| ∃ m', RSteps code m m' ∧ m'.pc = q + 11 ∧ m'.regs r1 = b ∧ m'.regs r3 = BitVec.ofNat 32 i ∧ |
| a = (m'.regs r2).toNat * b.toNat + (m'.regs r0).toNat ∧ |
| (m'.regs r0).toNat < b.toNat * 2 ^ i ∧ m'.mem = m.mem ∧ |
| ∀ r, ¬ LoopScratch r → m'.regs r = m.regs r := by |
| have hi32 : i % 256 = i := Nat.mod_eq_of_lt (by omega) |
| have h3n : (m.regs r3).toNat % 256 = i := by rw [h3, toNat_ofNat_lt (by omega), hi32] |
| let R := m.regs r0 |
| let Q := m.regs r2 |
| let m1 := m.mov r7 R |
| have s2 : step code m = .next m1 := by rw [rstep_of_fetch (by rw [hpc] |
| let m2 := m1.arith r7 (R >>> i) |
| have s3 : step code m1 = .next m2 := by |
| have : m1.pc = q + 3 := by simp [m1, M.mov, M.adv, M.setReg, hpc] |
| rw [rstep_of_fetch (by rw [this] |
| have e7 : m1.regs r7 = R := by simp [m1, M.mov, M.adv, M.setReg] |
| have e3 : (m1.regs r3).toNat % 256 = i := by |
| have : m1.regs r3 = m.regs r3 := by simp [m1, M.mov, M.adv, M.setReg] |
| rw [this, h3n] |
| simp only [exec] |
| have hm2pc : m2.pc = q + 4 := by simp [m2, m1, M.mov, M.adv, M.setReg, M.arith, hpc] |
| have hm2r7 : m2.regs r7 = R >>> i := by simp [m2, M.arith, M.setReg] |
| have hm2r1 : m2.regs r1 = b := by simp [m2, m1, M.arith, M.mov, M.adv, M.setReg, h1] |
| have hfr2 : ∀ r, ¬ LoopScratch r → m2.regs r = m.regs r := by |
| intro r hr |
| have : r ≠ r7 := fun e => hr (by simp [LoopScratch, e]) |
| simp [m2, m1, M.arith, M.mov, M.adv, M.setReg, this] |
| have hcond : Cond.eval .ult (m2.regs r7) (m2.regs r1) = decide (R.toNat < b.toNat * 2 ^ i) := by |
| rw [hm2r7, hm2r1] |
| by_cases hskip : R.toNat < b.toNat * 2 ^ i |
| · -- the bit is 0: skip to the test |
| let m3 : M := { m2 with pc := q + 11 } |
| have s4 : step code m2 = .next m3 := by |
| rw [rstep_of_fetch (by rw [hm2pc] |
| simp only [exec, hcond, hskip, decide_true, ite_true] |
| refine ⟨m3, .cons s2 (.cons s3 (.single s4)), rfl, hm2r1, ?_, ?_, hskip, ?_, ?_⟩ |
| · show m2.regs r3 = _ |
| simp [m2, m1, M.arith, M.mov, M.adv, M.setReg, h3] |
| · show a = (m2.regs r2).toNat * b.toNat + (m2.regs r0).toNat |
| have e2 : m2.regs r2 = Q := by simp [m2, m1, M.arith, M.mov, M.adv, M.setReg, Q] |
| have e0 : m2.regs r0 = R := by simp [m2, m1, M.arith, M.mov, M.adv, M.setReg, R] |
| rw [e2, e0] |
| · simp [m3, m2, m1, M.arith, M.mov, M.adv, M.setReg] |
| · intro r hr |
| · -- the bit is 1: subtract `b <<< i`, add `1 <<< i` |
| have hge : b.toNat * 2 ^ i ≤ R.toNat := by omega |
| have hRlt := R.isLt |
| let m3 := m2.adv |
| have s4 : step code m2 = .next m3 := by |
| rw [rstep_of_fetch (by rw [hm2pc] |
| simp only [exec, hcond, hskip, decide_false] |
| let m4 := m3.mov r7 b |
| have s5 : step code m3 = .next m4 := by |
| have : m3.pc = q + 5 := by simp [m3, M.adv, hm2pc] |
| rw [rstep_of_fetch (by rw [this] |
| simp [exec, m4, m3, M.adv, hm2r1] |
| let m5 := m4.arith r7 (b <<< i) |
| have s6 : step code m4 = .next m5 := by |
| have : m4.pc = q + 6 := by simp [m4, m3, M.mov, M.adv, M.setReg, hm2pc] |
| rw [rstep_of_fetch (by rw [this] |
| have e3 : m4.regs r3 = BitVec.ofNat 32 i := by |
| simp [m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg, h3] |
| have e3n : (m4.regs r3).toNat % 256 = i := by rw [e3, toNat_ofNat_lt (by omega), hi32] |
| have e7 : m4.regs r7 = b := by simp [m4, M.mov, M.adv, M.setReg] |
| simp only [exec] |
| let m6 := m5.arith r0 (R - b <<< i) |
| have s7 : step code m5 = .next m6 := by |
| have : m5.pc = q + 7 := by simp [m5, m4, m3, M.mov, M.adv, M.arith, M.setReg, hm2pc] |
| rw [rstep_of_fetch (by rw [this] |
| have e0 : m5.regs r0 = R := by simp [m5, m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg, R] |
| have e7 : m5.regs r7 = b <<< i := by simp [m5, M.arith, M.setReg] |
| simp only [exec] |
| let m7 := m6.mov r7 1#32 |
| have s8 : step code m6 = .next m7 := by |
| have : m6.pc = q + 8 := by simp [m6, m5, m4, m3, M.mov, M.adv, M.arith, M.setReg, hm2pc] |
| rw [rstep_of_fetch (by rw [this] |
| let m8 := m7.arith r7 (1#32 <<< i) |
| have s9 : step code m7 = .next m8 := by |
| have : m7.pc = q + 9 := by simp [m7, m6, m5, m4, m3, M.mov, M.adv, M.arith, M.setReg, hm2pc] |
| rw [rstep_of_fetch (by rw [this] |
| have e3 : m7.regs r3 = BitVec.ofNat 32 i := by |
| simp [m7, m6, m5, m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg, h3] |
| have e3n : (m7.regs r3).toNat % 256 = i := by rw [e3, toNat_ofNat_lt (by omega), hi32] |
| have e7 : m7.regs r7 = 1#32 := by simp [m7, M.mov, M.adv, M.setReg] |
| simp only [exec] |
| let m9 := m8.arith r2 (Q + 1#32 <<< i) |
| have s10 : step code m8 = .next m9 := by |
| have : m8.pc = q + 10 := by |
| simp [m8, m7, m6, m5, m4, m3, M.mov, M.adv, M.arith, M.setReg, hm2pc] |
| rw [rstep_of_fetch (by rw [this] |
| have e2 : m8.regs r2 = Q := by |
| simp [m8, m7, m6, m5, m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg, Q] |
| have e7 : m8.regs r7 = 1#32 <<< i := by simp [m8, M.arith, M.setReg] |
| simp only [exec] |
| have e9r0 : m9.regs r0 = R - b <<< i := by |
| simp [m9, m8, m7, m6, M.mov, M.adv, M.arith, M.setReg] |
| have e9r2 : m9.regs r2 = Q + 1#32 <<< i := by simp [m9, M.arith, M.setReg] |
| -- arithmetic |
| have hpow : 2 ^ i < 2 ^ 32 := Nat.pow_lt_pow_right (by omega) hi |
| have hbsh : (b <<< i).toNat = b.toNat * 2 ^ i := shl_toNat_of_le b i (by omega) |
| have hR' : (R - b <<< i).toNat = R.toNat - b.toNat * 2 ^ i := by |
| rw [sub_toNat_of_le R _ (by rw [hbsh]; exact hge), hbsh] |
| have h1sh : (1#32 <<< i).toNat = 2 ^ i := by |
| rw [shl_toNat_of_le 1#32 i (by simpa using hpow)]; simp |
| have hQb : (Q.toNat + 2 ^ i) ≤ (Q.toNat + 2 ^ i) * b.toNat := Nat.le_mul_of_pos_right _ hbpos |
| have hdist : (Q.toNat + 2 ^ i) * b.toNat = Q.toNat * b.toNat + b.toNat * 2 ^ i := by |
| rw [Nat.add_mul, Nat.mul_comm (2 ^ i)] |
| have hinv' : a = Q.toNat * b.toNat + R.toNat := hinv |
| have hQ' : (Q + 1#32 <<< i).toNat = Q.toNat + 2 ^ i := by |
| rw [add_toNat_of_lt Q _ (by rw [h1sh]; omega), h1sh] |
| have hpow2 : 2 ^ (i + 1) = 2 * 2 ^ i := by rw [Nat.pow_succ, Nat.mul_comm] |
| have hlt' : R.toNat < b.toNat * 2 ^ (i + 1) := hlt |
| rw [hpow2, Nat.mul_left_comm] at hlt' |
| refine ⟨m9, .cons s2 (.cons s3 (.cons s4 (.cons s5 (.cons s6 (.cons s7 (.cons s8 (.cons s9 |
| (.single s10)))))))), ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ |
| · simp [m9, m8, m7, m6, m5, m4, m3, M.mov, M.adv, M.arith, M.setReg, hm2pc] |
| · simp [m9, m8, m7, m6, m5, m4, m3, M.mov, M.adv, M.arith, M.setReg, hm2r1] |
| · simp [m9, m8, m7, m6, m5, m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg, h3] |
| · rw [e9r2, e9r0, hQ', hR', hdist]; omega |
| · rw [e9r0, hR'] |
| · simp [m9, m8, m7, m6, m5, m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg] |
| · intro r hr |
| have h7 : r ≠ r7 := fun e => hr (by simp [LoopScratch, e]) |
| have h0 : r ≠ r0 := fun e => hr (by simp [LoopScratch, e]) |
| have h2 : r ≠ r2 := fun e => hr (by simp [LoopScratch, e]) |
| simp [m9, m8, m7, m6, m5, m4, m3, m2, m1, M.mov, M.adv, M.arith, M.setReg, h7, h0, h2] |
|
|
| /-- **The loop invariant.** From the top of the round for bit `i`, the loop reaches its exit |
| with `r2 = a / b`. -/ |
| theorem udiv_loop (hat : RAt code q (udivCode q)) {b : W} (hb : b ≠ 0#32) {a : Nat} |
| (ha : a < 2 ^ 32) : |
| ∀ i (m : M), i < 32 → m.pc = q + 2 → m.regs r1 = b → m.regs r3 = BitVec.ofNat 32 i → |
| a = (m.regs r2).toNat * b.toNat + (m.regs r0).toNat → |
| (m.regs r0).toNat < b.toNat * 2 ^ (i + 1) → |
| ∃ m', RSteps code m m' ∧ m'.pc = q + 14 ∧ (m'.regs r2).toNat = a / b.toNat ∧ |
| m'.mem = m.mem ∧ ∀ r, ¬ LoopScratch r → m'.regs r = m.regs r := by |
| have hbpos : 0 < b.toNat := by |
| rcases Nat.eq_zero_or_pos b.toNat with h | h |
| · exact absurd (BitVec.eq_of_toNat_eq (by simpa using h)) hb |
| · exact h |
| simp only [udivCode, RAt] at hat |
| obtain ⟨_, _, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, _⟩ := hat |
| have f2' : code[q + 2]? = some (.movRR r7 r0) := by simpa using f2 |
| have f3' : code[q + 3]? = some (.lsr r7 r3) := by simpa using f3 |
| have f4' : code[q + 4]? = some (.bcc .ult r7 r1 (q + 11)) := by simpa using f4 |
| have f5' : code[q + 5]? = some (.movRR r7 r1) := by simpa using f5 |
| have f6' : code[q + 6]? = some (.lsl r7 r3) := by simpa using f6 |
| have f7' : code[q + 7]? = some (.sub r0 r7) := by simpa using f7 |
| have f8' : code[q + 8]? = some (.movImm r7 1#32) := by simpa using f8 |
| have f9' : code[q + 9]? = some (.lsl r7 r3) := by simpa using f9 |
| have f10' : code[q + 10]? = some (.add r2 r7) := by simpa using f10 |
| have f11' : code[q + 11]? = some (.beqz r3 (q + 14)) := by simpa using f11 |
| have f12' : code[q + 12]? = some (.addImm r3 (-1)) := by simpa using f12 |
| have f13' : code[q + 13]? = some (.jmp (q + 2)) := by simpa using f13 |
| intro i |
| induction i with |
| | zero => |
| intro m hi hpc h1 h3 hinv hlt |
| obtain ⟨m1, hs1, hpc1, _, h31, hinv1, hlt1, hm1, hfr1⟩ := |
| udiv_round f2' f3' f4' f5' f6' f7' f8' f9' f10' hbpos ha hi hpc h1 h3 hinv hlt |
| -- `r3 = 0`: leave the loop |
| let m2 : M := { m1 with pc := q + 14 } |
| have s11 : step code m1 = .next m2 := by |
| rw [rstep_of_fetch (by rw [hpc1]; exact f11')] |
| simp only [exec, h31] |
| refine ⟨m2, hs1.trans (.single s11), rfl, ?_, hm1, hfr1⟩ |
| show (m1.regs r2).toNat = a / b.toNat |
| have hlt1' : (m1.regs r0).toNat < b.toNat := by simpa using hlt1 |
| symm |
| apply Nat.div_eq_of_lt_le |
| · omega |
| · rw [Nat.add_mul, Nat.one_mul]; omega |
| | succ k ih => |
| intro m hi hpc h1 h3 hinv hlt |
| obtain ⟨m1, hs1, hpc1, h11, h31, hinv1, hlt1, hm1, hfr1⟩ := |
| udiv_round f2' f3' f4' f5' f6' f7' f8' f9' f10' hbpos ha hi hpc h1 h3 hinv hlt |
| -- `r3 ≠ 0`: count down and go round again |
| let m2 := m1.adv |
| have hne : ¬ BitVec.ofNat 32 (k + 1) = 0#32 := fun e => by |
| have := (ofNat_eq_zero (by omega : k + 1 < 2 ^ 32)).mp e |
| have s11 : step code m1 = .next m2 := by |
| rw [rstep_of_fetch (by rw [hpc1] |
| simp only [exec, h31, hne, ite_false] |
| let m3 := m2.arith r3 (BitVec.ofNat 32 k) |
| have s12 : step code m2 = .next m3 := by |
| have : m2.pc = q + 12 := by simp [m2, M.adv, hpc1] |
| rw [rstep_of_fetch (by rw [this] |
| have e3 : m2.regs r3 = BitVec.ofNat 32 (k + 1) := by simp [m2, M.adv, h31] |
| simp only [exec] |
| let m4 : M := { m3 with pc := q + 2 } |
| have s13 : step code m3 = .next m4 := by |
| have : m3.pc = q + 13 := by simp [m3, m2, M.adv, M.arith, hpc1] |
| rw [rstep_of_fetch (by rw [this] |
| have e0 : m4.regs r0 = m1.regs r0 := by simp [m4, m3, m2, M.adv, M.arith, M.setReg] |
| have e2 : m4.regs r2 = m1.regs r2 := by simp [m4, m3, m2, M.adv, M.arith, M.setReg] |
| obtain ⟨m', hs', hpc', hq', hm', hfr'⟩ := ih m4 (by omega) rfl |
| (by simp [m4, m3, m2, M.adv, M.arith, M.setReg, h11]) |
| (by simp [m4, m3, M.arith, M.setReg]) (by rw [e0, e2] |
| (by rw [e0] |
| refine ⟨m', hs1.trans (.cons s11 (.cons s12 (.cons s13 hs'))), hpc', hq', ?_, ?_⟩ |
| · rw [hm', ← hm1]; simp [m4, m3, m2, M.adv, M.arith, M.setReg] |
| · intro r hr |
| have h3' : r ≠ r3 := fun e => hr (by simp [LoopScratch, e]) |
| rw [hfr' r hr, ← hfr1 r hr]; simp [m4, m3, m2, M.adv, M.arith, M.setReg, h3'] |
|
|
| /-- The loop alone: `udivCode` at `q`, entered with `r0 = a` and `r1 = b ≠ 0`, ends at `q + 14` |
| with `r2 = a.udiv b`, having changed only `r0 r2 r3 r7`. -/ |
| theorem udiv_code (hat : RAt code q (udivCode q)) {m : M} (hpc : m.pc = q) {a b : W} |
| (h0 : m.regs r0 = a) (h1 : m.regs r1 = b) (hb : b ≠ 0#32) : |
| ∃ m', RSteps code m m' ∧ m'.pc = q + 14 ∧ m'.regs r2 = a.udiv b ∧ m'.mem = m.mem ∧ |
| ∀ r, ¬ LoopScratch r → m'.regs r = m.regs r := by |
| have hbpos : 0 < b.toNat := by |
| rcases Nat.eq_zero_or_pos b.toNat with h | h |
| · exact absurd (BitVec.eq_of_toNat_eq (by simpa using h)) hb |
| · exact h |
| have hat' := hat |
| simp only [udivCode, RAt] at hat' |
| obtain ⟨f0, f1, _⟩ := hat' |
| let m1 := m.mov r2 0#32 |
| have s0 : step code m = .next m1 := by rw [rstep_of_fetch (by rw [hpc]; exact f0)]; rfl |
| let m2 := m1.mov r3 31#32 |
| have s1 : step code m1 = .next m2 := by |
| have : m1.pc = q + 1 := by simp [m1, M.mov, M.adv, M.setReg, hpc] |
| rw [rstep_of_fetch (by rw [this]; exact f1)]; rfl |
| have ha := a.isLt |
| obtain ⟨m3, hs3, hpc3, hq3, hm3, hfr3⟩ := udiv_loop hat hb (a := a.toNat) ha 31 m2 (by omega) |
| (by simp [m2, m1, M.mov, M.adv, M.setReg, hpc]) (by simp [m2, m1, M.mov, M.adv, M.setReg, h1]) |
| (by simp [m2, M.mov, M.adv, M.setReg]) |
| (by simp [m2, m1, M.mov, M.adv, M.setReg, h0]) |
| (by |
| have : (m2.regs r0).toNat = a.toNat := by simp [m2, m1, M.mov, M.adv, M.setReg, h0] |
| rw [this] |
| have : 2 ^ 32 ≤ b.toNat * 2 ^ (31 + 1) := Nat.le_mul_of_pos_left _ hbpos |
| omega) |
| refine ⟨m3, .cons s0 (.cons s1 hs3), hpc3, ?_, ?_, ?_⟩ |
| · apply BitVec.eq_of_toNat_eq |
| rw [hq3]; exact BitVec.toNat_udiv.symm |
| · simp [hm3, m2, m1, M.mov, M.adv, M.setReg] |
| · intro r hr |
| have h2' : r ≠ r2 := fun e => hr (by simp [LoopScratch, e]) |
| have h3' : r ≠ r3 := fun e => hr (by simp [LoopScratch, e]) |
| simp [hfr3 r hr, m2, m1, M.mov, M.adv, M.setReg, h2', h3'] |
| |
| /-- **Unsigned division.** `udivSeq` at `q`, entered with `r0 = a` and `r1 = b ≠ 0`, ends at |
| `q + 15` with `r0 = a.udiv b`, having changed only scratch registers. -/ |
| theorem udiv_seq (hat : RAt code q (udivSeq q)) {m : M} (hpc : m.pc = q) {a b : W} |
| (h0 : m.regs r0 = a) (h1 : m.regs r1 = b) (hb : b ≠ 0#32) : |
| ∃ m', RSteps code m m' ∧ m'.pc = q + 15 ∧ m'.regs r0 = a.udiv b ∧ m'.mem = m.mem ∧ |
| ∀ r, ¬ DivScratch r → m'.regs r = m.regs r := by |
| obtain ⟨hatc, hatt⟩ := rat_append.mp hat |
| obtain ⟨m3, hs3, hpc3, hq3, hm3, hfr3⟩ := udiv_code hatc hpc h0 h1 hb |
| obtain ⟨f14⟩ : code[q + 14]? = some (.movRR r0 r2) ∧ True := by |
| simpa [udivCode, RAt] using hatt |
| let m4 := m3.mov r0 (m3.regs r2) |
| have s14 : step code m3 = .next m4 := by rw [rstep_of_fetch (by rw [hpc3]; exact f14)]; rfl |
| refine ⟨m4, hs3.trans (.single s14), ?_, ?_, ?_, ?_⟩ |
| · simp [m4, M.mov, M.adv, M.setReg, hpc3] |
| · simp [m4, M.mov, M.adv, M.setReg, hq3] |
| · simp [m4, M.mov, M.adv, M.setReg, hm3] |
| · intro r hr |
| have h0' : r ≠ r0 := fun e => hr (by simp [DivScratch, e]) |
| have hl : ¬ LoopScratch r := by |
| rintro (e | e | e | e) < |
| simp [m4, M.mov, M.adv, M.setReg, h0', hfr3 r hl] |
| |
| /-- The absolute value the sequence computes: `neg` when the sign bit is set. -/ |
| def absW (x : W) : W := if x.msb then 0#32 - x else x |
| |
| theorem absW_ne_zero {x : W} (h : x ≠ 0#32) : absW x ≠ 0#32 := by |
| unfold absW; split |
| · intro e; apply h |
| have : -x = 0#32 := by rw [← BitVec.zero_sub]; exact e |
| exact BitVec.neg_eq_zero_iff.mp this |
| · exact h |
| |
| /-- Dividing the absolute values and negating when the signs differ is `BitVec.sdiv`. -/ |
| theorem sdiv_by_abs (a b : W) : |
| (if (a ^^^ b).msb then 0#32 - (absW a).udiv (absW b) else (absW a).udiv (absW b)) = |
| a.sdiv b := by |
| unfold absW BitVec.sdiv |
| rw [BitVec.msb_xor] |
| cases a.msb <;> cases b.msb <;> simp [BitVec.zero_sub] <;> rfl |
| |
| /-- **Signed division.** `sdivSeq` at `q`, entered with `r0 = a` and `r1 = b ≠ 0`, ends at |
| `q + 27` with `r0 = a.sdiv b`, having changed only scratch registers. -/ |
| theorem sdiv_seq (hat : RAt code q (sdivSeq q)) {m : M} (hpc : m.pc = q) {a b : W} |
| (h0 : m.regs r0 = a) (h1 : m.regs r1 = b) (hb : b ≠ 0#32) : |
| ∃ m', RSteps code m m' ∧ m'.pc = q + 27 ∧ m'.regs r0 = a.sdiv b ∧ m'.mem = m.mem ∧ |
| ∀ r, ¬ DivScratch r → m'.regs r = m.regs r := by |
| obtain ⟨hpre, hrest⟩ := rat_append.mp (by simpa [sdivSeq, List.append_assoc] using hat : |
| RAt code q ([.movRR r3 r0, .xor r3 r1, .movRR r10 r3, .movImm r2 0#32, |
| .bcc .sge r0 r2 (q + 6), .neg r0, .bcc .sge r1 r2 (q + 8), .neg r1] ++ |
| (udivCode (q + 8) ++ [.movRR r3 r10, .movImm r7 0#32, .bcc .sge r3 r7 (q + 26), .neg r2, |
| .movRR r0 r2]))) |
| obtain ⟨hloop, hpost⟩ := rat_append.mp hrest |
| simp only [RAt, List.length_cons, List.length_nil] at hpre hpost |
| obtain ⟨f0, f1, f2, f3, f4, f5, f6, f7, _⟩ := hpre |
| have hlen : (udivCode (q + 8)).length = 14 := by simp [udivCode] |
| rw [hlen] at hpost |
| obtain ⟨g0, g1, g2, g3, g4, _⟩ := hpost |
| -- the sign of the result, kept in `r10` |
| let m1 := m.mov r3 a |
| have s0 : step code m = .next m1 := by |
| rw [rstep_of_fetch (by rw [hpc]; exact f0)]; simp only [exec, h0]; rfl |
| let m2 := m1.arith r3 (a ^^^ b) |
| have s1 : step code m1 = .next m2 := by |
| have : m1.pc = q + 1 := by simp [m1, M.mov, M.adv, M.setReg, hpc] |
| rw [rstep_of_fetch (by simpa [this] using f1)] |
| have e3 : m1.regs r3 = a := by simp [m1, M.mov, M.adv, M.setReg] |
| have e1 : m1.regs r1 = b := by simp [m1, M.mov, M.adv, M.setReg, h1] |
| simp only [exec]; rw [e3, e1] |
| let m3 := m2.mov r10 (a ^^^ b) |
| have s2 : step code m2 = .next m3 := by |
| have : m2.pc = q + 2 := by simp [m2, m1, M.mov, M.adv, M.setReg, M.arith, hpc] |
| rw [rstep_of_fetch (by simpa [this] using f2)] |
| have e3 : m2.regs r3 = a ^^^ b := by simp [m2, M.arith, M.setReg] |
| simp only [exec]; rw [e3] |
| let m4 := m3.mov r2 0#32 |
| have s3 : step code m3 = .next m4 := by |
| have : m3.pc = q + 3 := by simp [m3, m2, m1, M.mov, M.adv, M.setReg, M.arith, hpc] |
| rw [rstep_of_fetch (by simpa [this] using f3)]; rfl |
| have hm4pc : m4.pc = q + 4 := by simp [m4, m3, m2, m1, M.mov, M.adv, M.setReg, M.arith, hpc] |
| have hm4r0 : m4.regs r0 = a := by simp [m4, m3, m2, m1, M.mov, M.adv, M.setReg, M.arith, h0] |
| have hm4r1 : m4.regs r1 = b := by simp [m4, m3, m2, m1, M.mov, M.adv, M.setReg, M.arith, h1] |
| have hm4r2 : m4.regs r2 = 0#32 := by simp [m4, M.mov, M.adv, M.setReg] |
| -- `r0 := |a|` |
| obtain ⟨m6, hs6, hpc6, h6r0, h6o⟩ : ∃ m6, RSteps code m4 m6 ∧ m6.pc = q + 6 ∧ |
| m6.regs r0 = absW a ∧ (∀ r, r ≠ r0 → m6.regs r = m4.regs r) ∧ m6.mem = m4.mem := by |
| by_cases ha : a.msb |
| · let m5 := m4.adv |
| have s4 : step code m4 = .next m5 := by |
| rw [rstep_of_fetch (by simpa [hm4pc] using f4)] |
| simp [exec, Cond.eval, hm4r0, hm4r2, zero_sle, ha, m5] |
| let m6 := m5.arith r0 (0#32 - a) |
| have s5 : step code m5 = .next m6 := by |
| have : m5.pc = q + 5 := by simp [m5, M.adv, hm4pc] |
| rw [rstep_of_fetch (by simpa [this] using f5)] |
| have e0 : m5.regs r0 = a := by simp [m5, M.adv, hm4r0] |
| simp only [exec]; rw [e0] |
| refine ⟨m6, .cons s4 (.single s5), by simp [m6, m5, M.arith, M.adv, hm4pc], ?_, ?_, ?_⟩ |
| · simp [m6, M.arith, M.setReg, absW, ha] |
| · intro r hr; simp [m6, m5, M.arith, M.adv, M.setReg, hr] |
| · simp [m6, m5, M.arith, M.adv, M.setReg] |
| · let m6 : M := { m4 with pc := q + 6 } |
| have s4 : step code m4 = .next m6 := by |
| rw [rstep_of_fetch (by simpa [hm4pc] using f4)] |
| simp [exec, Cond.eval, hm4r0, hm4r2, zero_sle, ha, m6] |
| exact ⟨m6, .single s4, rfl, by simp [m6, hm4r0, absW, ha], fun r _ => rfl, rfl⟩ |
| -- `r1 := |b|` |
| have hm6r1 : m6.regs r1 = b := by rw [h6o.1 r1 (by decide), hm4r1] |
| have hm6r2 : m6.regs r2 = 0#32 := by rw [h6o.1 r2 (by decide), hm4r2] |
| obtain ⟨m8, hs8, hpc8, h8r1, h8o, h8m⟩ : ∃ m8, RSteps code m6 m8 ∧ m8.pc = q + 8 ∧ |
| m8.regs r1 = absW b ∧ (∀ r, r ≠ r1 → m8.regs r = m6.regs r) ∧ m8.mem = m6.mem := by |
| by_cases hbm : b.msb |
| · let m7 := m6.adv |
| have s6 : step code m6 = .next m7 := by |
| rw [rstep_of_fetch (by simpa [hpc6] using f6)] |
| simp [exec, Cond.eval, hm6r1, hm6r2, zero_sle, hbm, m7] |
| let m8 := m7.arith r1 (0#32 - b) |
| have s7 : step code m7 = .next m8 := by |
| have : m7.pc = q + 7 := by simp [m7, M.adv, hpc6] |
| rw [rstep_of_fetch (by simpa [this] using f7)] |
| have e1 : m7.regs r1 = b := by simp [m7, M.adv, hm6r1] |
| simp only [exec]; rw [e1] |
| refine ⟨m8, .cons s6 (.single s7), by simp [m8, m7, M.arith, M.adv, hpc6], ?_, ?_, ?_⟩ |
| · simp [m8, M.arith, M.setReg, absW, hbm] |
| · intro r hr; simp [m8, m7, M.arith, M.adv, M.setReg, hr] |
| · simp [m8, m7, M.arith, M.adv, M.setReg] |
| · let m8 : M := { m6 with pc := q + 8 } |
| have s6 : step code m6 = .next m8 := by |
| rw [rstep_of_fetch (by simpa [hpc6] using f6)] |
| simp [exec, Cond.eval, hm6r1, hm6r2, zero_sle, hbm, m8] |
| exact ⟨m8, .single s6, rfl, by simp [m8, hm6r1, absW, hbm], fun r _ => rfl, rfl⟩ |
| have h8r0 : m8.regs r0 = absW a := by rw [h8o r0 (by decide), h6r0] |
| -- divide the absolute values |
| obtain ⟨m9, hs9, hpc9, h9r2, h9m, h9fr⟩ := |
| udiv_code hloop hpc8 h8r0 h8r1 (absW_ne_zero hb) |
| have h9r10 : m9.regs r10 = a ^^^ b := by |
| rw [h9fr r10 (by simp [LoopScratch]), h8o r10 (by decide), h6o.1 r10 (by decide)] |
| simp [m4, m3, M.mov, M.adv, M.setReg] |
| -- negate when the signs differ |
| let Q := (absW a).udiv (absW b) |
| let m10 := m9.mov r3 (a ^^^ b) |
| have s22 : step code m9 = .next m10 := by |
| rw [rstep_of_fetch (by simpa [hpc9] using g0)]; simp only [exec, h9r10]; rfl |
| let m11 := m10.mov r7 0#32 |
| have s23 : step code m10 = .next m11 := by |
| have : m10.pc = q + 8 + 14 + 1 := by simp [m10, M.mov, M.adv, M.setReg, hpc9] |
| rw [rstep_of_fetch (by simpa [this] using g1)]; rfl |
| have hm11pc : m11.pc = q + 8 + 14 + 2 := by simp [m11, m10, M.mov, M.adv, M.setReg, hpc9] |
| have hm11r3 : m11.regs r3 = a ^^^ b := by simp [m11, m10, M.mov, M.adv, M.setReg] |
| have hm11r7 : m11.regs r7 = 0#32 := by simp [m11, M.mov, M.adv, M.setReg] |
| have hm11r2 : m11.regs r2 = Q := by simp [m11, m10, M.mov, M.adv, M.setReg, h9r2, Q] |
| obtain ⟨m13, hs13, hpc13, h13r2, h13o, h13m⟩ : ∃ m13, RSteps code m11 m13 ∧ m13.pc = q + 26 ∧ |
| m13.regs r2 = (if (a ^^^ b).msb then 0#32 - Q else Q) ∧ |
| (∀ r, r ≠ r2 → m13.regs r = m11.regs r) ∧ m13.mem = m11.mem := by |
| by_cases hs : (a ^^^ b).msb |
| · let m12 := m11.adv |
| have s24 : step code m11 = .next m12 := by |
| rw [rstep_of_fetch (by simpa [hm11pc] using g2)] |
| simp [exec, Cond.eval, hm11r3, hm11r7, zero_sle, hs, m12] |
| let m13 := m12.arith r2 (0#32 - Q) |
| have s25 : step code m12 = .next m13 := by |
| have : m12.pc = q + 8 + 14 + 3 := by simp [m12, M.adv, hm11pc] |
| rw [rstep_of_fetch (by simpa [this] using g3)] |
| have e2 : m12.regs r2 = Q := by simp [m12, M.adv, hm11r2] |
| simp only [exec]; rw [e2] |
| refine ⟨m13, .cons s24 (.single s25), by simp [m13, m12, M.arith, M.adv, hm11pc], |
| ?_, ?_, ?_⟩ |
| · simp [m13, M.arith, M.setReg, hs] |
| · intro r hr; simp [m13, m12, M.arith, M.adv, M.setReg, hr] |
| · simp [m13, m12, M.arith, M.adv, M.setReg] |
| · let m13 : M := { m11 with pc := q + 26 } |
| have s24 : step code m11 = .next m13 := by |
| rw [rstep_of_fetch (by simpa [hm11pc] using g2)] |
| simp [exec, Cond.eval, hm11r3, hm11r7, zero_sle, hs, m13] |
| exact ⟨m13, .single s24, rfl, by simp [m13, hm11r2, hs], fun r _ => rfl, rfl⟩ |
| let m14 := m13.mov r0 (m13.regs r2) |
| have s26 : step code m13 = .next m14 := by |
| rw [rstep_of_fetch (by simpa [hpc13] using g4)]; rfl |
| refine ⟨m14, .cons s0 (.cons s1 (.cons s2 (.cons s3 (hs6.trans (hs8.trans (hs9.trans |
| (.cons s22 (.cons s23 (hs13.trans (.single s26)))))))))), ?_, ?_, ?_, ?_⟩ |
| · simp [m14, M.mov, M.adv, M.setReg, hpc13] |
| · simp only [m14, M.mov, M.adv, M.setReg, ite_true, h13r2]; exact sdiv_by_abs a b |
| · simp [m14, M.mov, M.adv, M.setReg, h13m, m11, m10, h9m, h8m, h6o.2, m4, m3, m2, m1, M.arith] |
| · intro r hr |
| have hl : ¬ LoopScratch r := by |
| rintro (e | e | e | e) <;> exact hr (by simp [DivScratch, e]) |
| have h0' : r ≠ r0 := fun e => hr (by simp [DivScratch, e]) |
| have h1' : r ≠ r1 := fun e => hr (by simp [DivScratch, e]) |
| have h2' : r ≠ r2 := fun e => hr (by simp [DivScratch, e]) |
| have h3' : r ≠ r3 := fun e => hr (by simp [DivScratch, e]) |
| have h7' : r ≠ r7 := fun e => hr (by simp [DivScratch, e]) |
| have h10' : r ≠ r10 := fun e => hr (by simp [DivScratch, e]) |
| simp only [m14, M.mov, M.adv, M.setReg, h0', ite_false] |
| rw [h13o r h2', show m11.regs r = m9.regs r by simp [m11, m10, M.mov, M.adv, M.setReg, h3', h7'], |
| h9fr r hl, h8o r h1', h6o.1 r h0'] |
| simp [m4, m3, m2, m1, M.mov, M.adv, M.setReg, M.arith, h2', h10', h3'] |
|
|
| end Loop |
|
|
| end CM0 |
| end WordDialect |
|
|
