suprising

Author: dtumad

OperationFramework/Add4Operation.lean

@@ -2,15 +2,14 @@ import OperationFramework.Basic
 
 @[reducible] def Add4Operation (T : Type) := Word T
 
-namespace AddOperation
+namespace Add4Operation
 
-/-- `Add4Operation` should either give the direct sum of the two input values, with one possible overflow.
+/-- `AddOperation` should either give the direct sum of the two input values, with one possible overflow.
 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 →
-    let no_wrap_sum : ℕ := a.toNat + b.toNat + c.toNat + d.toNat
-    no_wrap_sum % 2^32 = cols.toNat
+    (a.toNat + b.toNat) % 2^32 = cols.toNat
 
 -- /-- Constraints on `AddOperation` as extracted from the source code. -/
 -- def extractedConstraints (cols : AddOperation (Fin p))
@@ -22,37 +21,43 @@ def spec (cols : Add4Operation (Fin p))
 --     ((((a[0] + b[0]) - cols[0]) + 0) * 2013235201)) * 2013235201) - 1)) = 0 ∧
 --     cols[0].val < base ∧ cols[1].val < base
 
--- /-- Cleaned up representation of the `AddOperation` constraints. -/
--- def idealConstraints (cols : AddOperation (Fin p))
---     (a : Word (Fin p))
---     (b : 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
---   carry1 * (carry1 - 1) = 0 ∧ -- isBool check
---   carry2 * (carry2 - 1) = 0 ∧ -- isBool check
---   cols.isUInt32 -- slice range checks
+/-- Cleaned up representation of the `AddOperation` constraints. -/
+def idealConstraints (cols : Add4Operation (Fin p))
+    (a b c d : 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
+  carry1 * (carry1 - 1) = 0 ∧ -- isBool check
+  carry2 * (carry2 - 1) = 0 ∧ -- isBool check
+  cols.isUInt32 -- slice range checks
 
 -- /-- The idealized constraints are logically equivalent to the extracted ones. -/
 -- lemma extractedConstraints_iff_idealConstraints (cols : AddOperation (Fin p))
 --     (a : Word (Fin p)) (b : Word (Fin p)) :
 --     cols.extractedConstraints a b ↔ cols.idealConstraints a b := by
 --   simp [extractedConstraints, idealConstraints, Word.isUInt32]
 
--- /-- The constraints on `AddOperation` imply the expected spec. -/
+-- /-- 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
---   rw [extractedConstraints_iff_idealConstraints]
---   simp [idealConstraints, spec, toNat_add_toNat, Word.isUInt32, sub_eq_zero]
-
---   intros h1 h2
+--   -- 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
---     <;> simp [h_overflow, Word.toNat]
+--     -- 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, sub_eq_zero, p] at *
---           omega
-
-end AddOperation
+--     <;> {
+--       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

@@ -4,16 +4,14 @@ import OperationFramework.Basic
 
 namespace AddOperation
 
-/-- `AddOperation` should either give the direct sum of the two input values, with one possible overflow.
-This is more explicit than saying that `(a.toNat + b.toNat) % 2^32 = cols.toNat`. -/
-def spec (cols : AddOperation (Fin p))
-    (a : Word (Fin p)) (b : Word (Fin p)) : Prop :=
+/-- `AddOperation` should result in wrapping addition of the outputs. -/
+def spec (cols : AddOperation (Fin p)) (a b : Word (Fin p)) : Prop :=
   a.isUInt32 → b.isUInt32 →
     (a.toNat + b.toNat) % 2^32 = cols.toNat
 
 /-- Constraints on `AddOperation` as extracted from the source code. -/
 def extractedConstraints (cols : AddOperation (Fin p))
-    (a : Word (Fin p)) (b : Word (Fin p)) : Prop :=
+    (a b : Word (Fin p)) : Prop :=
   (((((a[0] + b[0]) - cols[0]) + (0 : Fin p)) *
     (2013235201 : Fin p)) * (((((a[0] + b[0]) - cols[0]) + 0) * 2013235201) - 1)) = 0 ∧
     (((((a[1] + b[1]) - cols[1]) + ((((a[0] + b[0]) - cols[0]) + (0 : Fin p)) *
@@ -23,8 +21,7 @@ def extractedConstraints (cols : AddOperation (Fin p))
 
 /-- Cleaned up representation of the `AddOperation` constraints. -/
 def idealConstraints (cols : AddOperation (Fin p))
-    (a : Word (Fin p))
-    (b : Word (Fin p)) : Prop :=
+    (a b : 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
@@ -33,34 +30,29 @@ def idealConstraints (cols : AddOperation (Fin p))
   cols.isUInt32 -- slice range checks
 
 /-- The idealized constraints are logically equivalent to the extracted ones. -/
-lemma extractedConstraints_iff_idealConstraints (cols : AddOperation (Fin p))
-    (a : Word (Fin p)) (b : Word (Fin p)) :
+lemma extractedConstraints_iff_idealConstraints
+    (cols : AddOperation (Fin p)) (a b : Word (Fin p)) :
     cols.extractedConstraints a b ↔ cols.idealConstraints a b := by
   simp [extractedConstraints, idealConstraints, Word.isUInt32]
 
-/-- The constraints on `AddOperation` imply the expected spec. -/
+/-- 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 : AddOperation (Fin p)) (a b : Word (Fin p)) :
     cols.extractedConstraints a b → cols.spec a b := by
-  rw [extractedConstraints_iff_idealConstraints]
-  -- rw [idealConstraints]
-  simp [idealConstraints, spec, mul_eq_zero, sub_eq_zero]
+  -- 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
 
-  erw [add_mod_of_isUInt32_isUInt32 ha_u32 hb_u32]
-  simp [Word.isUInt32, toNat_add_toNat]
-  simp [Word.isUInt32] at ha_u32 hb_u32 hcols_u32
-  -- intros h1 h2
-  split_ifs with h_overflow
-    <;> simp [h_overflow, Word.toNat]
+  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, sub_eq_zero, p] at *
-          cases ha_u32
-          cases hb_u32
-          cases hcols_u32
-
-          omega
+    <;> {
+      rw [h1] at h2
+      simp [Fin.add_def, Fin.sub_def, Fin.ext_iff, p, Word.toNat,
+        Word.isUInt32] at *
+      omega
+    }
 
 end AddOperation

OperationFramework/Basic.lean

@@ -5,18 +5,19 @@ This file defines basic constants and structures to use in verifying
 the constraints of an operation against a spec
 -/
 
+-- Finite fields over primes have no zero divisors (pulled from `ZMod` instance).
 instance {p : ℕ} [hp : Fact (Nat.Prime (p + 1))] : NoZeroDivisors (Fin (p + 1)) := by
   have : IsDomain (ZMod (p + 1)) := ZMod.instIsDomain (hp := ⟨hp.1⟩)
   simp [ZMod] at this
   infer_instance
 
-abbrev WORD_SIZE := 2
-abbrev p := 2013265921
+abbrev WORD_SIZE := 2 -- two limbs
+abbrev p := 2013265921 -- babybear
 
 section base
 
-abbrev base : Fin p := 65536
-abbrev baseInv : Fin p := 2013235201
+abbrev base : Fin p := 65536 -- 2^16
+abbrev baseInv : Fin p := 2013235201 -- (2^16)⁻¹
 
 @[simp] lemma val_base : base.val = 65536 := rfl
 @[simp] lemma val_baseInv : baseInv.val = 2013235201 := rfl
@@ -38,6 +39,7 @@ abbrev baseInv : Fin p := 2013235201
 
 end base
 
+/-- Words over a type as vector of values. -/
 @[reducible] def Word (T : Type) := Vector T WORD_SIZE
 
 namespace Word
@@ -64,14 +66,30 @@ section isUInt32
 def isUInt32 (w : Word (Fin p)) : Prop :=
   w[0].val < base ∧ w[1].val < base
 
-lemma add_mod_of_isUInt32_isUInt32 {a b : Word (Fin p)}
+lemma add₂_mod_of_isUInt32 {a b : Word (Fin p)}
     (h : a.isUInt32) (h' : b.isUInt32) :
     let no_wrap_sum : ℕ := a.toNat + b.toNat
     no_wrap_sum % 2^32 = if no_wrap_sum < 2^32
       then no_wrap_sum else no_wrap_sum - 2^32 := by
   simp [isUInt32, toNat] at *
   split_ifs <;> omega
 
+lemma add₂_mod_of_limbs_lt_base {a b : Word (Fin p)}
+    (h1 : a[0].val < base) (h2 : a[1].val < base)
+    (h3 : b[0].val < base) (h4 : b[1].val < base) :
+    let no_wrap_sum : ℕ := a.toNat + b.toNat
+    no_wrap_sum % 2^32 = if no_wrap_sum < 2^32
+      then no_wrap_sum else no_wrap_sum - 2^32 := by
+  refine add₂_mod_of_isUInt32 ?_ ?_ <;>
+    simp [isUInt32] at * <;> trivial
+
+lemma add₄_mod_of_isUInt32 {a b c d : Word (Fin p)}
+    (h : a.isUInt32) (h : b.isUInt32) (h : c.isUInt32) (h : d.isUInt32) :
+    let no_wrap_sum : ℕ := a.toNat + b.toNat + c.toNat + d.toNat
+    no_wrap_sum % 2^32 = sorry := by
+  sorry
+
+
 end isUInt32
 
 end Word