From 9580cd7c2e9695e8f6734c5ef91fe4d9ad6a37ff Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Thu, 19 Sep 2024 11:52:22 -0500
Subject: [PATCH] feat: Decidable instances for mem_legal', mem_subset',
 mem_separate' (#170)

# Before your submission:

### Description:

We use this to allow `#eval decide (mem_subset' 10 100 10 100)` for
interactive use-cases, and for proofs, where these goals can be
dispatched by `decide`.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

`make all` succeeds, conformance succeeds locally.

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Co-authored-by: Shilpi Goel <shigoel@gmail.com>
---
 Arm/Memory/Separate.lean | 50 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index bb33914b..a05cc413 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -228,6 +228,21 @@ def mem_legal'.of_omega (h : a.toNat + n ≤ 2^64) : mem_legal' a n := h
 
 theorem mem_legal'.omega_def (h : mem_legal' a n) : a.toNat + n ≤ 2^64 := h
 
+/-- The linear constraint is equivalent to `mem_legal'`. -/
+theorem mem_legal'.iff_omega (a : BitVec 64) (n : Nat) :
+    (a.toNat + n ≤ 2^64) ↔ mem_legal' a n := by
+  constructor
+  · intros h
+    apply mem_legal'.of_omega h
+  · intros h
+    apply h.omega_def
+
+instance : Decidable (mem_legal' a n) :=
+  if h : a.toNat + n ≤ 2^64 then
+    isTrue (mem_legal'.of_omega h)
+  else
+    isFalse (fun h' => h h')
+
 /--
 @bollu: have proof automation exploit this.
 Equation lemma for `mem_legal'`.
@@ -324,6 +339,23 @@ theorem mem_separate'.of_omega
   · unfold mem_legal'; omega
   · omega
 
+/-- The linear constraint is equivalent to `mem_separate'`. -/
+theorem mem_separate'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    (a.toNat + an ≤ 2^64 ∧
+    b.toNat + bn ≤ 2^64 ∧
+    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) ↔ mem_separate' a an b bn := by
+  constructor
+  · intros h
+    apply mem_separate'.of_omega h
+  · intros h
+    apply h.omega_def
+
+instance : Decidable (mem_separate' a an b bn) :=
+  if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) then
+    isTrue (mem_separate'.of_omega h)
+  else
+    isFalse (fun h' => h ⟨h'.ha.omega_def, h'.hb.omega_def, h'.h⟩)
+
 theorem BitVec.not_le_eq_lt {a b : BitVec w₁} : (¬ (a ≤ b)) ↔ b < a := by
   rw [BitVec.le_def, BitVec.lt_def]
   omega
@@ -390,6 +422,24 @@ constructor
 · rw [BitVec.le_def]; omega
 · omega
 
+/-- The linear constraint is equivalent to `mem_subset'`. -/
+theorem mem_subset'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    (a.toNat + an ≤ 2^64 ∧
+    b.toNat + bn ≤ 2^64 ∧
+    b.toNat ≤ a.toNat ∧
+    a.toNat + an ≤ b.toNat + bn) ↔ mem_subset' a an b bn := by
+  constructor
+  · intros h
+    apply mem_subset'.of_omega h
+  · intros h
+    apply h.omega_def
+
+instance : Decidable (mem_subset' a an b bn) :=
+  if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) then
+    isTrue (mem_subset'.of_omega h)
+  else
+    isFalse (fun h' => h ⟨h'.ha.omega_def, h'.hb.omega_def, h'.hstart, h'.hend⟩)
+
 theorem mem_subset'_refl (h : mem_legal' a an) : mem_subset' a an a an where
   ha := h
   hb := h