is_zero done

Author: dtumad

OperationFramework/IsZeroOperation.lean

@@ -7,34 +7,46 @@ structure IsZeroOperation (T : Type) where
 namespace IsZeroOperation
 
 /-- `IsZeroOperation` should result in wrapping addition of the outputs. -/
-def spec (cols : IsZeroOperation (Fin p)) (a : Fin p) : Prop :=
-  a = 0 ↔ cols.result = 1
-
-/-- Constraints on `IsZeroOperation` as extracted from the source code. -/
-def extractedConstraints (cols : IsZeroOperation (Fin p)) (a : Fin p) : Prop :=
-  sorry
+def spec (cols : IsZeroOperation (Fin p)) (a : Fin p) (is_real : Fin p) : Prop :=
+  is_real ≠ 0 → (a = 0 ↔ cols.result = 1)
+
+/-- Constraints on `IsZeroOperation` as extracted from the source code:
+Asserting expr 8: `(is_real * ((1 - (cols.inverse * a)) - cols.result))`
+Asserting expr 11: `(is_real * (cols.result * (cols.result - 1)))`
+Asserting expr 13: `(is_real * (cols.result * a))` -/
+def extractedConstraints (cols : IsZeroOperation (Fin p))
+    (a : Fin p) (is_real : Fin p) : Prop :=
+  (is_real * ((1 - (cols.inverse * a)) - cols.result)) = 0 ∧
+  (is_real * (cols.result * (cols.result - 1))) = 0 ∧
+  (is_real * (cols.result * a)) = 0
 
 /-- Cleaned up representation of the `IsZeroOperation` constraints. -/
-def idealConstraints (cols : IsZeroOperation (Fin p)) (a : Fin p) : Prop :=
-  let is_zero := 1 - cols.inverse * a
-  is_zero - cols.result = 0 ∧
-  cols.result * (cols.result - 1) = 0 ∧
-  (cols.result ≠ 0 → a = 0)
+def idealConstraints (cols : IsZeroOperation (Fin p))
+    (a : Fin p) (is_real : Fin p) : Prop :=
+  is_real ≠ 0 → (
+    1 - (cols.inverse * a) = cols.result ∧
+    (cols.result = 0 ∨ cols.result = 1) ∧
+    (cols.result = 0 ∨ a = 0)
+  )
 
 /-- The idealized constraints are logically equivalent to the extracted ones. -/
-lemma extractedConstraints_iff_idealConstraints
-    (cols : IsZeroOperation (Fin p)) (a : Fin p) :
-    cols.extractedConstraints a ↔ cols.idealConstraints a := by
-  sorry
-
-/-- The extracted constraints on `AddOperation` imply the spec. -/
-theorem correct [Fact (Nat.Prime p)]
-    (cols : IsZeroOperation (Fin p)) (a : Fin p) :
-    cols.extractedConstraints a → cols.spec a := by
+lemma extractedConstraints_iff_idealConstraints [Fact (Nat.Prime p)]
+    (cols : IsZeroOperation (Fin p)) (a : Fin p) (is_real : Fin p) :
+    cols.extractedConstraints a is_real ↔ cols.idealConstraints a is_real := by
+  by_cases hreal : is_real = 0
+  · simp [extractedConstraints, idealConstraints, hreal]
+  · simp [extractedConstraints, idealConstraints, hreal, sub_eq_zero]
+
+/-- The extracted constraints on `IsZeroOperation` imply the spec. -/
+theorem correct [Fact (Nat.Prime p)] (cols : IsZeroOperation (Fin p))
+    (a : Fin p) (is_real : Fin p) :
+    cols.extractedConstraints a is_real → cols.spec a is_real := by
   simp [extractedConstraints_iff_idealConstraints, idealConstraints, spec,
     mul_eq_zero, sub_eq_zero]
-  refine fun h h' h'' => ⟨fun h' => ?_, fun h' => ?_⟩
-    <;> simp [h', eq_comm (a := cols.result)] at *
-    <;> assumption
+  refine fun h hreal => ⟨fun h' => ?_, fun h' => ?_⟩
+  · simp [h', hreal, eq_comm (a := cols.result)] at *
+    exact h.1
+  · simp [h', hreal, eq_comm (a := cols.result)] at *
+    exact h.2
 
 end IsZeroOperation