feat: add automation support for pairwise memory separation (#126)

This is stacked on top of #123 , since we want to state this, for a
given `ms : List MemoryRegion`, `ms.pairwise MemoryRegion.Separate`.
This, of course, needs us to have the `MemoryRegion` abstraction in the
first place.

---------

Co-authored-by: Shilpi Goel <[email protected]>

Arm/Memory/Separate.lean

@@ -328,6 +328,12 @@ theorem BitVec.not_le_eq_lt {a b : BitVec w₁} : (¬ (a ≤ b)) ↔ b < a := by
   rw [BitVec.le_def, BitVec.lt_def]
   omega
 
+theorem mem_separate'_comm (h : mem_separate' a an b bn) :
+    mem_separate' b bn a an := by
+  have := h.omega_def
+  apply mem_separate'.of_omega
+  omega
+
 /-#
 This is a theorem we ought to prove, which establishes the equivalence
 between the old and new defintions of 'mem_separate'.
@@ -492,7 +498,7 @@ theorem Memory.read_bytes_write_bytes_eq_of_mem_subset'
   · subst hxn
     exfalso
     have h := i.isLt
-    simp at h
+    simp only [Nat.reduceMul, Nat.zero_mul, Nat.not_lt_zero] at h
   · by_cases h₁ : ↑i < xn * 8
     · simp only [h₁]
       simp only [decide_True, Bool.true_and]
@@ -560,4 +566,53 @@ theorem Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
       bv_omega
     · simp only [h, ↓reduceIte]
 
+/-- A region of memory, given by (base pointer, length) -/
+abbrev Memory.Region := BitVec 64 × Nat
+
+def Memory.Region.mk (a : BitVec 64) (n : Nat) : Memory.Region := (a, n)
+
+/-- A hypothesis that memory regions `a` and `b` are separate. -/
+def Memory.Region.separate (a b : Memory.Region) : Prop :=
+  mem_separate' a.fst a.snd b.fst b.snd
+
+/-- A list of memory regions, that are known to be pairwise disjoint. -/
+def Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop :=
+  mems.Pairwise Memory.Region.separate
+
+/-- If `i ≠ j`, then prove that `mems[i] ⟂ mems[j]`.
+The theorem is stated in mildly awkward fashion for ease of use during proof automation.
+-/
+def Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
+  (h : Memory.Region.pairwiseSeparate mems)
+  (i j : Nat)
+  (hij : i ≠ j)
+  (a b : Memory.Region)
+  (ha : mems.get? i = some a) (hb : mems.get? j = some b) :
+    mem_separate' a.fst a.snd b.fst b.snd := by
+  induction h generalizing a b i j
+  case nil => simp only [List.get?_eq_getElem?, List.getElem?_nil, reduceCtorEq] at ha
+  case cons x xs ihx _ihxs ihxs' =>
+    simp only [List.get?_eq_getElem?] at ha hb
+    rcases i with rfl | i'
+    · simp at ha
+      · rcases j with rfl | j'
+        · simp only [ne_eq, not_true_eq_false] at hij
+        · subst ha
+          simp only [List.getElem?_cons_succ] at hb
+          apply ihx
+          exact List.getElem?_mem hb
+    · rcases j with rfl | j'
+      · simp only [List.length_cons, Nat.zero_lt_succ, List.getElem?_eq_getElem,
+        List.getElem_cons_zero, Option.some.injEq] at hb
+        · subst hb
+          simp only [List.getElem?_cons_succ] at ha
+          apply mem_separate'_comm
+          apply ihx
+          exact List.getElem?_mem ha
+      · simp only [List.getElem?_cons_succ] at ha hb
+        apply ihxs' i' j'
+        · omega
+        · simp only [List.get?_eq_getElem?, ha]
+        · simp only [List.get?_eq_getElem?, hb]
+
 end NewDefinitions