diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean index 2f8999f7..61925cca 100644 --- a/Arm/BitVec.lean +++ b/Arm/BitVec.lean @@ -239,9 +239,11 @@ attribute [bitvec_rules] Nat.reduceBneDiff attribute [bitvec_rules] Nat.reduceLTLE attribute [bitvec_rules] Nat.reduceLeDiff attribute [bitvec_rules] Nat.reduceSubDiff +attribute [bitvec_rules] BitVec.toNat_ofNat -- Some Fin lemmas useful for bitvector reasoning: attribute [bitvec_rules] Fin.eta +attribute [bitvec_rules] Fin.isLt attribute [bitvec_rules] Fin.isValue -- To normalize Fin literals -- Some lemmas useful for clean-up after the use of simp/ground @@ -429,11 +431,21 @@ theorem nat_bitvec_sub (x y : BitVec n) : have : (x - y).toNat = ((2^n - y.toNat) + x.toNat) % 2^n := rfl rw [this, Nat.add_comm] + +theorem toNat_ofNat_lt {n w₁ : Nat} (hn : n < 2^w₁) : + (BitVec.ofNat w₁ n).toNat = n := by + simp only [toNat_ofNat, Nat.mod_eq_of_lt hn] + + ---------------------------- Comparison Lemmas ----------------------- @[simp] protected theorem not_lt {n : Nat} {a b : BitVec n} : ¬ a < b ↔ b ≤ a := by exact Fin.not_lt .. +theorem ge_of_not_lt (x y : BitVec w₁) (h : ¬ (x < y)) : x ≥ y := by + simp_all only [BitVec.le_def, BitVec.lt_def] + omega + protected theorem le_of_eq (x y : BitVec n) (h : x = y) : x <= y := by simp [←nat_bitvec_le] @@ -672,6 +684,23 @@ protected theorem shift_left_zero_eq (n : Nat) (x : BitVec n) : x <<< 0 = x := b intro i simp only [toNat_shiftLeft, Nat.shiftLeft_zero, toNat_mod_cancel] +---------------------------- Negate Lemmas --------------------------- + +@[simp] +theorem neg_neg (x : BitVec w₁) : - (- x) = x := by + apply BitVec.eq_of_toNat_eq + simp only [toNat_neg] + by_cases h : x.toNat = 0 + · simp [h] + · rw [Nat.mod_eq_of_lt (a := 2^w₁ - x.toNat) (by omega)] + rw [Nat.sub_sub_eq_min] + rw [Nat.min_def] + simp [show ¬ 2^w₁ ≤ x.toNat by omega] + +theorem neg_eq_sub_zero (x : BitVec w₁) : - x = 0 - x := by + apply BitVec.eq_of_toNat_eq + simp only [toNat_neg, ofNat_eq_ofNat, toNat_sub, toNat_ofNat, Nat.zero_mod, Nat.add_zero] + ---------------------------------------------------------------------- /- Bitvector pattern component syntax category, originally written by @@ -847,6 +876,12 @@ theorem toNat_sub_eq_toNat_sub_toNat_of_le {x y : BitVec w} (h : y ≤ x) : · rw [Nat.sub_add_eq_add_sub_of_le_of_le (by omega) (by omega), Nat.add_mod, Nat.mod_self, Nat.zero_add, Nat.mod_mod, Nat.mod_eq_of_lt (by omega)] +/- Subtracting bitvectors when there is overflow. -/ +theorem toNat_sub_eq_two_pow_sub_add_of_lt + {a b : BitVec w₁} (hab : a.toNat < b.toNat) : (a - b).toNat = 2^w₁ - b.toNat + a.toNat := by + simp only [toNat_sub] + rw [Nat.mod_eq_of_lt (by omega)] + theorem neq_of_lt {x y : BitVec w₁} (h : x < y) : x ≠ y := by rintro rfl simp [BitVec.lt_def] at h @@ -861,6 +896,36 @@ theorem toNat_add_eq_toNat_add_toNat {x y : BitVec w} (h : x.toNat + y.toNat < 2 (x + y).toNat = x.toNat + y.toNat := by rw [BitVec.toNat_add, Nat.mod_eq_of_lt h] +theorem le_add_self_of_lt (a b : BitVec w₁) (hab : a.toNat + b.toNat < 2^w₁) : + a ≤ a + b := by + rw [BitVec.le_def] + rw [BitVec.toNat_add_eq_toNat_add_toNat (by omega)] + omega + +theorem add_sub_cancel_left {a b : BitVec w₁} + (hab : a.toNat + b.toNat < 2^w₁) : (a + b) - a = b := by + apply BitVec.eq_of_toNat_eq + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le] + · rw [BitVec.toNat_add_eq_toNat_add_toNat (by omega)] + omega + · apply BitVec.le_add_self_of_lt + omega + +theorem le_add_iff_sub_le {a b c : BitVec w₁} + (hac : c ≤ a) (hbc : b.toNat + c.toNat < 2^w₁) : + (a ≤ b + c) ↔ (a - c ≤ b) := by + simp_all only [BitVec.le_def] + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le (by rw [BitVec.le_def]; omega)] + rw [BitVec.toNat_add_eq_toNat_add_toNat (by omega)] + omega + +theorem sub_le_sub_iff_right (a b c : BitVec w₁) (hac : c ≤ a) + (hbc : c ≤ b) : (a - c ≤ b - c) ↔ a ≤ b := by + simp_all only [BitVec.le_def] + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le (by rw [BitVec.le_def]; omega)] + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le (by rw [BitVec.le_def]; omega)] + omega + /-! ### Least Significant Byte -/ /-- Definition to extract the `n`th least significant *Byte* from a bitvector. -/ diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean index 94e2b4ea..1012aaf9 100644 --- a/Arm/Memory/Separate.lean +++ b/Arm/Memory/Separate.lean @@ -1,9 +1,10 @@ /- Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author(s): Shilpi Goel +Author(s): Shilpi Goel, Siddharth Bhat -/ import Arm.State +import Arm.BitVec section Separate @@ -115,6 +116,480 @@ example : mem_subset (BitVec.ofNat 64 (2^64 - 1)) 0#64 0#64 (BitVec.ofNat 64 (2^ def mem_legal (a1 a2 : BitVec 64) : Bool := a1 <= a2 +/- +Given two legal memory regions `[a1, a2]` and `[b1, b2]` that are separated, +it must be the case either: + - the first one ends before the second one starts (`a2 < b1`), + - or, the first one starts after the second one ends `(a1 > b2)`, +-/ +theorem lt_or_gt_of_mem_separate_of_mem_legal_of_mem_legal (h : mem_separate a1 a2 b1 b2) + (ha : mem_legal a1 a2) (hb : mem_legal b1 b2) : + a2 < b1 ∨ a1 > b2 := by + unfold mem_separate mem_overlap at h + obtain ⟨⟨⟨h₁, h₂⟩, h₃⟩, h₄⟩ := by simpa only [Bool.not_or, Bool.and_eq_true, + Bool.not_eq_true', decide_eq_false_iff_not] using h + simp only [mem_legal, decide_eq_true_eq] at ha hb + rw [BitVec.le_def] at ha hb + rw [BitVec.le_def] at h₁ h₂ h₃ h₄ + rw [BitVec.lt_def, BitVec.gt_def] + by_cases h₅ : a2.toNat < b1.toNat + · simp only [h₅, gt_iff_lt, BitVec.val_bitvec_lt, true_or] + · by_cases h₆ : a1.toNat > b2.toNat + · simp only [BitVec.val_bitvec_lt, gt_iff_lt, h₆, or_true] + · exfalso + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le ha] at h₁ h₂ + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le hb] at h₃ h₄ + have h₅' : b1.toNat ≤ a2.toNat := by omega + have h₆' : a1.toNat ≤ b2.toNat := by omega + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le h₅'] at h₄ + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le h₆'] at h₂ + omega + +/-- +Given two legal memory regions `[a1, a2]` and `[b1, b2]`, +such that either the first one ends before the second one starts (`a2 < b1`), +or the first one starts after the second one ends `(a1 > b2)`, +the memory regions are separate. +-/ +theorem mem_separate_of_lt_or_gt_of_mem_legal_of_mem_legal (h : a2 < b1 ∨ a1 > b2) + (ha : mem_legal a1 a2) (hb : mem_legal b1 b2) : + mem_separate a1 a2 b1 b2 := by + unfold mem_separate mem_overlap + simp only [Bool.not_or, Bool.and_eq_true, Bool.not_eq_true', decide_eq_false_iff_not] + unfold mem_legal at ha hb + simp only [decide_eq_true_eq] at ha hb + rw [BitVec.le_def] at ha hb + simp only[BitVec.le_def] + rw [BitVec.lt_def, BitVec.gt_def] at h + rcases h with h | h + · rw [toNat_sub_eq_toNat_sub_toNat_of_le ha] + have ha1b1 : a1.toNat ≤ b1.toNat := by omega + rw [toNat_sub_eq_toNat_sub_toNat_of_le ha1b1] + have ha1b2 : a1.toNat ≤ b2.toNat := by omega + rw [toNat_sub_eq_toNat_sub_toNat_of_le ha1b2] + rw [toNat_sub_eq_toNat_sub_toNat_of_le hb] + have ha1b1' : a1.toNat < b1.toNat := by omega + rw [toNat_sub_eq_two_pow_sub_add_of_lt ha1b1'] + rw [toNat_sub_eq_two_pow_sub_add_of_lt h] + omega + · rw [toNat_sub_eq_toNat_sub_toNat_of_le ha] + rw [toNat_sub_eq_toNat_sub_toNat_of_le hb] + have ha2b1 : b1.toNat ≤ a2.toNat := by omega + rw [toNat_sub_eq_toNat_sub_toNat_of_le ha2b1] + have ha1b1 : b1.toNat ≤ a1.toNat := by omega + rw [toNat_sub_eq_toNat_sub_toNat_of_le ha1b1] + have hb1a1 : b1.toNat < a1.toNat := by omega + rw [toNat_sub_eq_two_pow_sub_add_of_lt hb1a1] + have hb2a1 : b2.toNat < a1.toNat := by omega + rw [toNat_sub_eq_two_pow_sub_add_of_lt hb2a1] + omega + +/-- +Given two legal memory regions `[a1, a2]` and `[b1, b2]`, +being separate is *equivalent* to: +- either the first one ends before the second one starts (`a2 < b1`), +- or the first one starts after the second one ends `(a1 > b2)`, +-/ +theorem mem_separate_iff_lt_or_gt_of_mem_legal_of_mem_legal + (ha : mem_legal a1 a2) (hb : mem_legal b1 b2) : + a2 < b1 ∨ a1 > b2 ↔ mem_separate a1 a2 b1 b2 := by + constructor + · intros h + apply mem_separate_of_lt_or_gt_of_mem_legal_of_mem_legal <;> assumption + · intros h + apply lt_or_gt_of_mem_separate_of_mem_legal_of_mem_legal <;> assumption + +/-- +If we express a memory region as `[a..(a+n)]` for `(n : Nat)`, +and this memory region is legal, then we could not have had any wraparound. +Thus, it must be the case that (a + n).toNat = a.toNat + n +-/ +theorem add_lt_of_mem_legal_of_lt + (h : mem_legal a (a + n)) : + a.toNat + n.toNat < 2^64 := by + simp only [mem_legal, decide_eq_true_eq, + le_def, toNat_add, Nat.reducePow] at h + by_cases hadd : a.toNat + n.toNat < 2^64 + · assumption + · exfalso + have ha : a.toNat < 2^64 := a.isLt; + have h₂ : a.toNat + n.toNat - 2^64 < 2^64 := by omega + have hmod : (a.toNat + n.toNat) % 18446744073709551616 = a.toNat + n.toNat - 2^64 := by + rw [Nat.mod_eq_sub_mod] + rw [Nat.mod_eq_of_lt h₂] + omega + rw [hmod] at h + omega + +/-- +If we express a memory region as `[a..(a+n)]` for `(n : Nat)`, +and this memory region is legal, then we could not have had any wraparound. +Thus, it must be the case that (a + n).toNat = a.toNat + n +-/ +theorem toNat_add_distrib_of_mem_legal_of_lt + (h : mem_legal a (a + n)) : + (a + n).toNat = a.toNat + n.toNat := by + simp only [add_def, toNat_ofNat, Nat.reducePow] + rw [Nat.mod_eq_of_lt] + apply add_lt_of_mem_legal_of_lt h + end Separate ----------------------------------------------------------------------- +/-# + +### New Memory Model + +The new memory model is different from the old one in two ways: + +1. It uses (base pointer, length) to keep track of memory regions instead of closed intervals of [pointer 1, pointer 2]. +2. To facilitate the new representation, it bakes in the assumption that the memory region is legal + (i.e. no wraparound). +3. More softly, it tries to keep reasoning in terms of `Nat` rather than `BitVec` in order to allow easier + automation via `omega` for proving disjointedness / subset assumptions. + +All of the new definitions are named after the old definitions with a prime (') after their name. +For robustness (and confidence), we plan to prove theorems that establish the equivalence of the old and new memory models. +-/ +section NewDefinitions + +/-- +`mem_legal' a n` witnessses that `(a + n)` does not overflow, and thus `[a..a+n)` is a valid range +of memory. Note that the interval is left closed, right open, and thus `n` is the number of bytes in the memory range. +-/ +def mem_legal' (a : BitVec 64) (n : Nat) : Prop := + a.toNat + n ≤ 2^64 + +/-- +@bollu: have proof automation exploit this. +Equation lemma for `mem_legal'`. +-/ +theorem mem_legal'_def (h : mem_legal' a n) : a.toNat + n ≤ 2^64 := h + +/-- +The maximum size of the range we can choose to allocate is 2^64. +@bollu: have proof automation exploit this. +-/ +theorem mem_legal'.size_le_two_pow (h : mem_legal' a n) : n ≤ 2 ^ 64 := by + rw [mem_legal'] at h + omega + +/-- +Legal in the new sense implies legal in the old sense. +-/ +theorem mem_legal_of_mem_legal' (h : mem_legal' a n) : + mem_legal a (a + (BitVec.ofNat 64 (n - 1))) := by + simp only [mem_legal', mem_legal, BitVec.le_def] at h ⊢ + rw [BitVec.toNat_add_eq_toNat_add_toNat] + simp only [BitVec.toNat_ofNat, Nat.reducePow, Nat.le_add_right, decide_True] + rw [BitVec.toNat_ofNat] + rw [Nat.mod_eq_of_lt (by omega)] + omega + + +/-- +Legal in the new sense implies legal in the old sense. +Note that the subtraction could also have been written as `(b - a).toNat + 1` +-/ +theorem mem_legal'_of_mem_legal (h: mem_legal a b) : mem_legal' a (b.toNat - a.toNat + 1) := by + simp only [mem_legal, decide_eq_true_eq] at h + rw [mem_legal'] + rw [BitVec.le_def] at h + omega + + +def mem_legal'_of_mem_legal'_of_lt (h : mem_legal' a n) (m : Nat) (hm : m ≤ n) : + mem_legal' a m := by + simp only [mem_legal', Nat.reducePow] at h ⊢ + omega + +/-- +`mem_legal` is equivalent to `mem_legal'`. +-/ +theorem mem_legal_iff_mem_legal' : mem_legal a b ↔ + mem_legal' a ((b - a).toNat + 1) := by + constructor + · intros h + simp only [mem_legal, decide_eq_true_eq] at h + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le h] + · simp only [mem_legal'] + omega + · intros h + simp only [mem_legal'] at h + simp only [mem_legal, BitVec.le_def, decide_eq_true_eq] + apply Classical.byContradiction + intros h₂ + rw [BitVec.toNat_sub_eq_two_pow_sub_add_of_lt (by omega)] at h + omega + +/-- +`mem_separate' a an b bn` asserts that two memory regions [a..an) and [b..bn) are separate. +Note that we use *half open* intervals. +In prose, we may notate this as `[a..an) ⟂ [b..bn)`. +See also: Why numbering should start at zero (https://www.cs.utexas.edu/~EWD/ewd08xx/EWD831.PDF) +-/ +structure mem_separate' (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) : Prop where + ha : mem_legal' a an + hb : mem_legal' b bn + h : a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn + +theorem BitVec.not_le_eq_lt {a b : BitVec w₁} : (¬ (a ≤ b)) ↔ b < a := by + rw [BitVec.le_def, BitVec.lt_def] + omega + +/-# +This is a theorem we ought to prove, which establishes the equivalence +between the old and new defintions of 'mem_separate'. +However, the proof is finicky, and so we leave it commented for now. +-/ +/- +theorem mem_separate_of_mem_separate' (h : mem_separate' a an b bn) + (ha' : a' = a + (BitVec.ofNat w₁ (an - 1) ) (hb' : b' = b + (BitVec.ofNat w₁ (bn - 1))) + (hlegala : mem_legal a an) (hlegalb: mem_legal b bn) : + mem_separate a a' b b' := by + simp [mem_separate] + simp [mem_overlap] + obtain ⟨ha, hb, hsep⟩ := h + simp [mem_legal'] at ha hb + subst ha' + subst hb' + apply Classical.byContradiction + intro hcontra + · sorry + · sorry +-/ + +/-- `mem_subset' a an b bn` witnesses that `[a..a+an)` is a subset of `[b..b+bn)`. +In prose, we may notate this as `[a..an) ≤ [b..bn)`. +-/ +structure mem_subset' (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) : Prop where + ha : mem_legal' a an + hb : mem_legal' b bn + hstart : b ≤ a + hend : a.toNat + an ≤ b.toNat + bn + +theorem mem_subset'_refl (h : mem_legal' a an) : mem_subset' a an a an where + ha := h + hb := h + hstart := by simp only [BitVec.le_def, Nat.le_refl] + hend := by simp only [Nat.le_refl] + +/-- +If `[a'..a'+an')` begins at least where `[a..an)` begins, +and ends before `[a..an)` ends, and if `[a..an)` is a subset of `[b..bn)`, +then `[a'..a'+an')` is a subset of `[b..bn)`. +-/ +theorem mem_subset'_of_le_of_le {a' : BitVec 64} (h : mem_subset' a an b bn) + (ha' : a.toNat ≤ a'.toNat) (han' : a'.toNat + an' ≤ a.toNat + an) : + mem_subset' a' an' b bn where + ha := by + obtain ⟨ha, hb, hstart, hend⟩ := h + simp only [mem_legal', Nat.reducePow] at ha hb ⊢ + simp_all only [BitVec.le_def] + omega + hb := h.hb + hstart := by + obtain ⟨ha, hb, hstart, hend⟩ := h + simp only [mem_legal', Nat.reducePow] at ha hb + simp_all only [BitVec.le_def] + omega + hend := by + obtain ⟨ha, hb, hstart, hend⟩ := h + simp only [mem_legal', Nat.reducePow] at ha hb + simp_all only [BitVec.le_def] + omega + +/-- +If `[a..an)` is a subset of `[b..bn)`, +then `[a..an')` is a subset of `[b..bn)` if `an' ≤ an`. +-/ +theorem mem_subset'_of_length_le (h : mem_subset' a an b bn) + (han' : an' ≤ an) : mem_subset' a an' b bn := by + apply mem_subset'_of_le_of_le h + · simp only [Nat.le_refl] + · omega + +/-- if `[a..an) ≤ [b..bn)` and `[b..bn) ⟂ [c..cn)`, +then `[a..an) ⟂ [c..cn)`. +(Recall that `⟂` stands for `mem_separate'`.) +-/ +theorem mem_separate'_of_mem_separate'_of_mem_subset' + (hsep : mem_separate' b bn c cn) + (hsub : mem_subset' a an b bn) : + mem_separate' a an c cn := by + obtain ⟨_, hsep₂, hsep₃⟩ := hsep + obtain ⟨hsub₁, _, hsub₃, hsub₄⟩ := hsub + simp_all only [BitVec.le_def] + constructor <;> + solve + | omega + | assumption + +private theorem Nat.sub_mod_eq_of_lt_of_le {x y : Nat} (hx : x < n) (hy : y ≤ x) : + (x - y) % n = (x % n) - (y % n) := by + rw [Nat.mod_eq_of_lt (by omega)] + rw [Nat.mod_eq_of_lt (by omega)] + rw [Nat.mod_eq_of_lt (by omega)] + +-- `mem_subset'` implies mem_subset. +theorem mem_subset_of_mem_subset' (h : mem_subset' a an b bn) (han : an > 0) (hbn : bn > 0) : + mem_subset a (a + BitVec.ofNat 64 (an - 1)) b (b + BitVec.ofNat 64 (bn - 1)):= by + unfold mem_subset + obtain ⟨ha, hb, hstart, hend⟩ := h + unfold mem_legal' at ha hb + simp only [bitvec_rules, minimal_theory] + by_cases hb : bn = 2^64 + · left + apply BitVec.eq_of_toNat_eq + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le ] + · rw [BitVec.toNat_add_eq_toNat_add_toNat] + · simp only [BitVec.toNat_ofNat, Nat.reducePow, Nat.reduceMod] + rw [Nat.mod_eq_of_lt (by omega)] + omega + · simp only [BitVec.toNat_ofNat, Nat.reducePow] + rw [Nat.mod_eq_of_lt (by omega)] + omega + · simp only [BitVec.le_def, BitVec.toNat_add, BitVec.toNat_ofNat, Nat.reducePow, + Nat.add_mod_mod] + rw [Nat.mod_eq_of_lt (by omega)] + omega + · have hbn : (BitVec.ofNat 64 (bn - 1)).toNat = (bn - 1) := by simp; omega + have han : (BitVec.ofNat 64 (an - 1)).toNat = (an - 1) := by simp; omega + rw [BitVec.le_def] at hstart + right + constructor + · rw [BitVec.add_sub_cancel_left] + · apply (BitVec.le_add_iff_sub_le _ _).mp + · rw [BitVec.le_def, BitVec.toNat_add, han, BitVec.toNat_add, hbn]; omega + . rw [BitVec.le_def, BitVec.toNat_add, han]; omega + · rw [hbn]; omega + · rw [hbn]; omega + · rw [BitVec.sub_le_sub_iff_right] + · rw [BitVec.le_def, BitVec.toNat_add, han] + omega + · assumption + · rw [BitVec.le_def, BitVec.toNat_add, han] + omega + +/- value of read_mem_bytes when separate. -/ +theorem read_mem_bytes_write_mem_bytes_eq_read_mem_bytes_of_mem_separate' + (hsep : mem_separate' x xn y yn) -- separation + (val : BitVec (yn * 8)) : + read_mem_bytes xn x (write_mem_bytes yn y val mem) = + read_mem_bytes xn x mem := by + simp only [bitvec_rules, minimal_theory, memory_rules] + apply BitVec.eq_of_getLsb_eq + intros i + obtain ⟨hsrc, hdest, hsplit⟩ := hsep + rw [Memory.getLsb_read_bytes, Memory.getLsb_write_bytes, Memory.getLsb_read_bytes] + simp only [i.isLt] + simp only [decide_True, ite_eq_left_iff, Bool.true_and] + intros h₁ + intros h₂ + -- we need to make use of mem_separate to show that src_addr + i / 8 < dest_addr | src_addr + i/7 ≥ dest_addr + 16 + exfalso + · rcases hsplit with this | this + · simp only [bitvec_rules, minimal_theory, BitVec.not_lt, BitVec.le_def, BitVec.toNat_add, + BitVec.toNat_ofNat] at h₁ + omega + · have hcontra_h2 : x.toNat + 16 < y.toNat + 16 := by + simp at this + have hi : (i : Nat) / 8 < xn := by + apply Nat.div_lt_of_lt_mul + simp only [Nat.mul_comm, Fin.is_lt] + rw [BitVec.toNat_add_eq_toNat_add_toNat] at h₂ + · omega + · have := mem_legal'_def hsrc + apply Nat.lt_of_lt_of_le _ this + apply Nat.add_lt_add_iff_left.mpr + simp + rw [Nat.mod_eq_of_lt] + omega + omega + omega + · have := hsrc.size_le_two_pow + omega + · have := mem_legal'_def hdest + omega + · have := hsrc.size_le_two_pow + omega + +/- value of `read_mem_bytes'` when subset. -/ +theorem read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset + (hsep : mem_subset' x xn y yn) -- subset relation. + (val : BitVec (yn * 8)) : + Memory.read_bytes xn x (Memory.write_bytes yn y val mem) = + val.extractLsBytes (x.toNat - y.toNat) xn := by + apply BitVec.eq_of_getLsb_eq + intros i + obtain ⟨hx, hy, hstart, hend⟩ := hsep + + obtain hx' := hx.size_le_two_pow + obtain hy' := mem_legal'_def hy + + rw [Memory.getLsb_read_bytes (by omega)] + rw [Memory.getLsb_write_bytes (by omega)] + rw [BitVec.getLsb_extractLsByte] + rw [BitVec.getLsb_extractLsBytes] + by_cases hxn : xn = 0 + · subst hxn + exfalso + have h := i.isLt + simp at h + · simp only [show (0 < xn) by omega] + simp only [show ((x.toNat - y.toNat) * 8 + xn * 8 - 1 - (x.toNat - y.toNat) * 8) = xn * 8 - 1 by omega] + by_cases h₁ : ↑i < xn * 8 + · simp only [h₁] + simp only [show (i ≤ xn * 8 - 1) by omega] + simp only [decide_True, Bool.true_and] + obtain ⟨i, hi⟩ := i + simp only at h₁ + simp only [] + have h₁' : (BitVec.ofNat 64 (i / 8)).toNat = (i / 8) := by + apply BitVec.toNat_ofNat_lt + omega + have hadd : (x + BitVec.ofNat 64 (↑i / 8)).toNat = x.toNat + (i / 8) := by + rw [BitVec.toNat_add_eq_toNat_add_toNat (by omega)] + rw [BitVec.toNat_ofNat_lt (by omega)] + simp only [BitVec.lt_def] + simp only [hadd] + by_cases h₂ : (x.toNat + i/ 8) < y.toNat + · -- contradiction + exfalso + rw [BitVec.le_def] at hstart + omega + · simp only [h₂, if_false] + by_cases h₃ : x.toNat + i / 8 ≥ y.toNat + yn + · rw [BitVec.le_def] at hstart + omega + · simp only [h₃, if_false] + simp only [show i % 8 ≤ 7 by omega] + simp only [decide_True, Bool.true_and] + -- ⊢ val.getLsb ((x + BitVec.ofNat 64 (i / 8) - y).toNat * 8 + i % 8) = val.getLsb ((y.toNat - x.toNat) * 8 + i) + /- + This is clearly true, it simplifes to (x.toNat - y.toNat) * 8 + (i/8)*8 + i % 8. + which equals (x.toNat - y.toNat + i) + -/ + congr 1 + rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le (by rw [BitVec.le_def]; omega)] + rw [BitVec.toNat_add_eq_toNat_add_toNat (by omega)] + rw [BitVec.toNat_ofNat_lt (by omega)] + have himod : (i / 8) * 8 + (i % 8) = i := by omega + rw [Nat.mul_sub_right_distrib, Nat.mul_sub_right_distrib, + Nat.add_mul] + conv => + rhs + rw [← himod] + rw [BitVec.le_def] at hstart + omega + · simp only [h₁, bitvec_rules, minimal_theory] + intros h + apply BitVec.getLsb_ge + omega + +/-- +info: 'read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in #print axioms read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset + + +end NewDefinitions diff --git a/Arm/MinTheory.lean b/Arm/MinTheory.lean index ef05b933..8f302e87 100644 --- a/Arm/MinTheory.lean +++ b/Arm/MinTheory.lean @@ -89,6 +89,8 @@ attribute [minimal_theory] bne_self_eq_false' attribute [minimal_theory] decide_False attribute [minimal_theory] decide_True attribute [minimal_theory] bne_iff_ne +attribute [minimal_theory] Bool.false_eq +attribute [minimal_theory] Bool.and_eq_false_imp attribute [minimal_theory] Nat.le_zero_eq attribute [minimal_theory] Nat.zero_add diff --git a/Arm/State.lean b/Arm/State.lean index a37d8b42..8315d24a 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author(s): Shilpi Goel +Author(s): Shilpi Goel, Siddharth Bhat -/ import Lean.Data.Format import Arm.BitVec @@ -715,6 +715,7 @@ def read_bytes (n : Nat) (addr : BitVec 64) (m : Memory) : BitVec (n * 8) := have h : n' * 8 + 8 = (n' + 1) * 8 := by simp_arith BitVec.cast h (rest ++ byte) +@[memory_rules] theorem State.read_mem_bytes_eq_mem_read_bytes (s : ArmState) : read_mem_bytes n addr s = s.mem.read_bytes n addr := by induction n generalizing addr s @@ -854,6 +855,7 @@ theorem write_bytes_eq_of_le {mem : Memory} {ix base : BitVec 64} · rw [BitVec.toNat_add_eq_toNat_add_toNat] · simp only [BitVec.toNat_ofNat, Nat.reducePow, Nat.reduceMod]; omega · simp only [BitVec.toNat_ofNat, Nat.reducePow, Nat.reduceMod]; omega + theorem write_bytes_eq_of_ge {mem : Memory} {ix base : BitVec 64} (hix : ix.toNat ≥ base.toNat + n) (hnowrap : base.toNat + n ≤ 2^64) :