working add4

Author: dtumad

OperationFramework/Add4Operation.lean

@@ -9,7 +9,7 @@ This is more explicit than saying that `(a.toNat + b.toNat) % 2^32 = cols.toNat`
 def spec (cols : Add4Operation (Fin p))
     (a b c d : Word (Fin p)) : Prop :=
   a.isUInt32 → b.isUInt32 → c.isUInt32 → d.isUInt32 →
-    (a.toNat + b.toNat) % 2^32 = cols.toNat
+    (a.toNat + b.toNat + c.toNat + d.toNat) % 2^32 = cols.toNat
 
 -- /-- Constraints on `AddOperation` as extracted from the source code. -/
 -- def extractedConstraints (cols : AddOperation (Fin p))
@@ -23,10 +23,10 @@ def spec (cols : Add4Operation (Fin p))
 
 /-- Cleaned up representation of the `AddOperation` constraints. -/
 def idealConstraints (cols : Add4Operation (Fin p))
-    (a b c d : Word (Fin p)) : Prop :=
+    (aw bw cw dw : Word (Fin p)) : Prop :=
   let carry0 := 0
-  let carry1 := (a[0] + b[0] - cols[0] + carry0) * baseInv
-  let carry2 := (a[1] + b[1] - cols[1] + carry1) * baseInv
+  let carry1 := (aw[0] + bw[0] + cw[0] + dw[0] - cols[0] + carry0) * baseInv
+  let carry2 := (aw[1] + bw[1] + cw[1] + dw[1] - cols[1] + carry1) * baseInv
   carry1 * (carry1 - 1) = 0 ∧ -- isBool check
   carry2 * (carry2 - 1) = 0 ∧ -- isBool check
   cols.isUInt32 -- slice range checks
@@ -37,27 +37,23 @@ def idealConstraints (cols : Add4Operation (Fin p))
 --     cols.extractedConstraints a b ↔ cols.idealConstraints a b := by
 --   simp [extractedConstraints, idealConstraints, Word.isUInt32]
 
--- /-- The extracted constraints on `AddOperation` imply the spec. -/
--- theorem correct [Fact (Nat.Prime p)]
---     (cols : AddOperation (Fin p))
---     (a : Word (Fin p)) (b : Word (Fin p)) :
---     cols.extractedConstraints a b → cols.spec a b := by
---   -- Unfold the definitions of constraints and spec
---   rw [extractedConstraints_iff_idealConstraints, idealConstraints, spec]
---   simp [sub_eq_zero, mul_eq_zero]
---   -- Introduce all of the hypothesis from the constraints
---   intros h1 h2 hcols_u32 ha_u32 hb_u32
---   -- Simplify the addition using the fact both limbs are u16 vals
---   erw [Word.add_mod_of_isUInt32_of_isUInt32 ha_u32 hb_u32, Word.toNat_add_toNat]
---   -- Split into two cases depending on if there was overflow
---   split_ifs with h_overflow
---     -- Split into cases depending on if the first limb addition had a carry
---     <;> cases h1 with | inl h1 => ?_ | inr h1 => ?_
---     <;> {
---       rw [h1] at h2
---       simp [Fin.add_def, Fin.sub_def, Fin.ext_iff, p, Word.toNat,
---         Word.isUInt32] at *
---       omega
---     }
+/-- The extracted constraints on `AddOperation` imply the spec. -/
+theorem correct [Fact (Nat.Prime p)]
+    (cols : Add4Operation (Fin p))
+    (aw bw cw dw: Word (Fin p)) :
+    cols.idealConstraints aw bw cw dw → cols.spec aw bw cw dw := by
+    -- Unfold the definitions of constraints and spec
+  rw [idealConstraints, spec]
+  simp [sub_eq_zero, mul_eq_zero]
+
+  -- Introduce all of the hypothesis from the constraints
+  intros h1 h2 hcols_u32 ha_u32 hb_u32
+
+  -- Split on if the lower limb leads to a carry
+  cases h1 with | inl h1 => ?_ | inr h1 => ?_
+  all_goals
+  { rw [h1] at h2
+    simp [Fin.add_def, Fin.sub_def, Fin.ext_iff, p, Word.toNat, Word.isUInt32] at *
+    omega }
 
 end Add4Operation

OperationFramework/AddOperation.lean

@@ -42,17 +42,15 @@ theorem correct [Fact (Nat.Prime p)]
   -- Unfold the definitions of constraints and spec
   rw [extractedConstraints_iff_idealConstraints, idealConstraints, spec]
   simp [sub_eq_zero, mul_eq_zero]
+
   -- Introduce all of the hypothesis from the constraints
   intros h1 h2 hcols_u32 ha_u32 hb_u32
 
-  by_cases h_overflow : a[0].val + b[0].val + base * (a[1].val + b[1].val) < 2 ^ 32
-  -- Split into two cases depending on if there was overflow
-    <;> cases h1 with | inl h1 => ?_ | inr h1 => ?_
-    <;> {
-      rw [h1] at h2
-      simp [Fin.add_def, Fin.sub_def, Fin.ext_iff, p, Word.toNat,
-        Word.isUInt32] at *
-      omega
-    }
+  -- Split on if the lower limb leads to a carry
+  cases h1 with | inl h1 => ?_ | inr h1 => ?_
+  all_goals
+  { rw [h1] at h2
+    simp [Fin.add_def, Fin.sub_def, Fin.ext_iff, p, Word.toNat, Word.isUInt32] at *
+    omega }
 
 end AddOperation