add and mul intro rules strengthened

reilabs · Nov 9, 2024 · a2bb6d9 · a2bb6d9
1 parent 69b4f74
commit a2bb6d9
Show file tree

Hide file tree

Showing 2 changed files with 90 additions and 54 deletions.
diff --git a/Lampe/Lampe/Builtin/Arith.lean b/Lampe/Lampe/Builtin/Arith.lean
@@ -1,25 +1,24 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
-/--
-Captures the behavior of the signed integer remainder operation % in Noir.
-In particular, for two signed integers `a` and `b`, this returns ` a - ((a.sdiv b) * b)`
--/
-def intRem {s: Nat} (a b : I s) : I s := (a - (a.sdiv b) * b)
-
-example : intRem (BitVec.ofInt 8 (-128)) (BitVec.ofInt 8 (-1)) = 0 := by rfl
-example : intRem (BitVec.ofInt 8 (-128)) (BitVec.ofInt 8 (-3)) = -2 := by rfl
-example : intRem (BitVec.ofInt 8 (6)) (BitVec.ofInt 8 (-100)) = 6 := by rfl
-example : intRem (BitVec.ofInt 8 (127)) (BitVec.ofInt 8 (-3)) = 1 := by rfl
+@[reducible]
+def noOverflow {tp : Tp}
+  (a b : tp.denote p)
+  (op : Int → Int → Int) : Prop := match tp with
+| .u s => (op a.toInt b.toInt) < 2^s
+| .i s => bitsCanRepresent s (op a.toInt b.toInt)
+| .field => True
+| .bi => True
+| _ => False
 
 inductive addOmni : Omni where
 | u {p st s a b Q} :
-  ((a.toInt + b.toInt) < 2^s → Q (some (st, a + b)))
-  → ((a.toInt + b.toInt) >= 2^s → Q none)
+  (noOverflow a b (·+·) → Q (some (st, a + b)))
+  → (¬noOverflow a b (·+·) → Q none)
   → addOmni p st [.u s, .u s] (.u s) h![a, b] Q
 | i {p st s a b Q} :
-  (bitsCanRepresent s (a.toInt + b.toInt) → Q (some (st, a + b)))
-  → (¬(bitsCanRepresent s (a.toInt + b.toInt)) → Q none)
+  (noOverflow a b (·+·) → Q (some (st, a + b)))
+  → (¬noOverflow a b (·+·) → Q none)
   → addOmni p st [.i s, .i s] (.i s) h![a, b] Q
 | field {p st a b Q} :
   Q (some (st, a + b))
@@ -35,9 +34,6 @@ def add : Builtin := {
     unfold omni_conseq
     intros
     cases_type addOmni <;> tauto
-    rename _ + _ < 2^_ → _ => hok
-    rename _ + _ ≥ 2^_ → _ => herr
-    rename_i hm
     repeat (constructor; aesop; aesop)
   frame := by
     unfold omni_frame
@@ -49,12 +45,12 @@ def add : Builtin := {
 
 inductive mulOmni : Omni where
 | u {p st s a b Q} :
-  ((a.toInt * b.toInt) < 2^s → Q (some (st, a * b)))
-  → ((a.toInt * b.toInt) >= 2^s → Q none)
+  (noOverflow a b (·*·) → Q (some (st, a * b)))
+  → (¬noOverflow a b (·*·) → Q none)
   → mulOmni p st [.u s, .u s] (.u s) h![a, b] Q
 | i {p st s a b Q} :
-  (bitsCanRepresent s (a.toInt * b.toInt) → Q (some (st, a * b)))
-  → (¬(bitsCanRepresent s (a.toInt * b.toInt)) → Q none)
+  (noOverflow a b (·*·) → Q (some (st, a * b)))
+  → (¬noOverflow a b (·*·) → Q none)
   → mulOmni p st [.i s, .i s] (.i s) h![a, b] Q
 | field {p st a b Q} :
   Q (some (st, a * b))
@@ -145,6 +141,17 @@ def div : Builtin := {
     repeat (first | constructor | tauto | intro)
 }
 
+/--
+Captures the behavior of the signed integer remainder operation % in Noir.
+In particular, for two signed integers `a` and `b`, this returns ` a - ((a.sdiv b) * b)`
+-/
+def intRem {s: Nat} (a b : I s) : I s := (a - (a.sdiv b) * b)
+
+example : intRem (BitVec.ofInt 8 (-128)) (BitVec.ofInt 8 (-1)) = 0 := by rfl
+example : intRem (BitVec.ofInt 8 (-128)) (BitVec.ofInt 8 (-3)) = -2 := by rfl
+example : intRem (BitVec.ofInt 8 (6)) (BitVec.ofInt 8 (-100)) = 6 := by rfl
+example : intRem (BitVec.ofInt 8 (127)) (BitVec.ofInt 8 (-3)) = 1 := by rfl
+
 inductive remOmni : Omni where
 | u {p st s a b Q} :
   (b ≠ 0 → Q (some (st, a % b)))

diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
@@ -12,10 +12,9 @@ instance {tp} : Add (Tp.denote p tp) where
     | .bi => a + b
     | _ => sorry
 
-/-- [WARNING] Post-condition is weak! Use the typed versions. -/
-theorem weak_add_intro : STHoare p Γ ⟦⟧
+theorem add_intro : STHoare p Γ ⟦⟧
     (.call h![] [tp, tp] tp (.builtin .add) h![a, b])
-    (fun v => v = a + b) := by
+    (fun v => v = a + b ∧ (Builtin.noOverflow a b (·+·))) := by
   unfold STHoare
   intro H
   intros st h
@@ -26,9 +25,61 @@ theorem weak_add_intro : STHoare p Γ ⟦⟧
   apply SLP.ent_star_top at h
   cases tp
   <;> (constructor; simp only [SLP.true_star])
-  <;> repeat (first | assumption | intro)
-  . simp
-  . simp
+  <;> (
+    simp only [Builtin.noOverflow] at *
+    intros
+  )
+  <;> try tauto
+  all_goals try unfold bitsCanRepresent
+  . rename_i hno
+    simp only [hno, and_self, SLP.true_star]
+    tauto
+  . rename_i hno
+    simp only [hno, and_self, SLP.true_star]
+    tauto
+  . simp only [and_self, SLP.true_star]
+    tauto
+  . simp only [and_self, SLP.true_star]
+    tauto
+
+instance {tp} : Mul (Tp.denote p tp) where
+  mul := fun a b => match tp with
+    | .u _ => a * b
+    | .i _ => a * b
+    | .field => a * b
+    | .bi => a * b
+    | _ => sorry
+
+theorem mul_intro : STHoare p Γ ⟦⟧
+    (.call h![] [tp, tp] tp (.builtin .mul) h![a, b])
+    (fun v => v = a * b ∧ (Builtin.noOverflow a b (·*·))) := by
+  unfold STHoare
+  intro H
+  intros st h
+  beta_reduce
+  constructor
+  simp only [Builtin.mul]
+  rw [SLP.true_star] at h
+  apply SLP.ent_star_top at h
+  cases tp
+  <;> (constructor; simp only [SLP.true_star])
+  <;> (
+    simp only [Builtin.noOverflow] at *
+    intros
+  )
+  <;> try tauto
+  all_goals try unfold bitsCanRepresent
+  . rename_i hno
+    simp only [hno, and_self, SLP.true_star]
+    tauto
+  . rename_i hno
+    simp only [hno, and_self, SLP.true_star]
+    tauto
+  . simp only [and_self, SLP.true_star]
+    tauto
+  . simp only [and_self, SLP.true_star]
+    tauto
+
 
 instance {tp} : Sub (Tp.denote p tp) where
   sub := fun a b => match tp with
@@ -64,32 +115,6 @@ theorem weak_sub_intro : STHoare p Γ ⟦⟧
   . aesop
   . simp
 
-instance {tp} : Mul (Tp.denote p tp) where
-  mul := fun a b => match tp with
-    | .u _ => a * b
-    | .i _ => a * b
-    | .field => a * b
-    | .bi => a * b
-    | _ => sorry
-
-/-- [WARNING] Post-condition is weak! Use the typed versions. -/
-theorem weak_mul_intro : STHoare p Γ ⟦⟧
-    (.call h![] [tp, tp] tp (.builtin .mul) h![a, b])
-    (fun v => v = a * b) := by
-  unfold STHoare
-  intro H
-  intros st h
-  beta_reduce
-  constructor
-  simp only [Builtin.mul]
-  rw [SLP.true_star] at h
-  apply SLP.ent_star_top at h
-  cases tp
-  <;> (constructor; simp only [SLP.true_star])
-  <;> repeat (first | assumption | intro)
-  . simp
-  . simp
-
 instance {tp} : Div (Tp.denote p tp) where
   div := fun a b => match tp with
     | .u _ => a.udiv b
@@ -101,7 +126,11 @@ instance {tp} : Div (Tp.denote p tp) where
 /-- [WARNING] Post-condition is weak! Use the typed versions. -/
 theorem weak_div_intro : STHoare p Γ ⟦⟧
     (.call h![] [tp, tp] tp (.builtin .div) h![a, b])
-    (fun v => v = match tp with | .u _ => a.udiv b | .i _ => a.sdiv b | _ => a / b) := by
+    (fun v =>
+      v = match tp with
+      | .u _ => a.udiv b
+      | .i _ => a.sdiv b
+      | _ => a / b) := by
   unfold STHoare
   intro H
   intros st h