Added cmp8 and cmp9

ProvenZk/Gates.lean

@@ -4,46 +4,45 @@ import Mathlib.Init.Data.Nat.Bitwise
 
 import ProvenZk.Binary
 
-namespace Gates
+namespace GatesDef
 variable {N : Nat}
 variable [Fact (Nat.Prime N)]
-def is_bool (a : ZMod N): Prop := (1-a)*a = 0 --a = 0 ∨ a = 1
+def is_bool (a : ZMod N): Prop := (1-a)*a = 0
 def add (a b : ZMod N): ZMod N := a + b
 def mul_acc (a b c : ZMod N): ZMod N := a + (b * c)
 def neg (a : ZMod N): ZMod N := a * (-1)
 def sub (a b : ZMod N): ZMod N := a - b
 def mul (a b : ZMod N): ZMod N := a * b
-def div_unchecked (a b out : ZMod N): Prop := (b ≠ 0 ∧ out*b = a) ∨ (a = 0 ∧ b = 0 ∧ out = 0) --(b ≠ 0 ∧ out = a * (1 / b)) ∨ (a = 0 ∧ b = 0 ∧ out = 0)
-def div (a b out : ZMod N): Prop := b ≠ 0 ∧ out*b = a --b ≠ 0 ∧ out = a * (1 / b)
-def inv (a out : ZMod N): Prop := a ≠ 0 ∧ out*a = 1 --a ≠ 0 ∧ out = 1 / a
+def div_unchecked (a b out : ZMod N): Prop := (b ≠ 0 ∧ out*b = a) ∨ (a = 0 ∧ b = 0 ∧ out = 0)
+def div (a b out : ZMod N): Prop := b ≠ 0 ∧ out*b = a
+def inv (a out : ZMod N): Prop := a ≠ 0 ∧ out*a = 1
 def xor (a b out : ZMod N): Prop := is_bool a ∧ is_bool b ∧ out = a+b-a*b-a*b
 def or (a b out : ZMod N): Prop := is_bool a ∧ is_bool b ∧ out = a+b-a*b
 def and (a b out : ZMod N): Prop := is_bool a ∧ is_bool b ∧ out = a*b
-def select (b i1 i2 out : ZMod N): Prop := is_bool b ∧ out = i2 - b*(i2-i1) --((b = 1 ∧ out = i1) ∨ (b = 0 ∧ out = i2))
-def lookup (b0 b1 i0 i1 i2 i3 out : ZMod N): Prop := is_bool b0 ∧ is_bool b1 ∧
+def select (b i1 i2 out : ZMod N): Prop := is_bool b ∧ out = i2 - b*(i2-i1)
+def lookup (b0 b1 i0 i1 i2 i3 out : ZMod N): Prop :=
+  is_bool b0 ∧ is_bool b1 ∧
   out = (i2 - i0) * b1 + i0 + (((i3 - i2 - i1 + i0) * b1 + i1 - i0) * b0)
-/-(
-  (b0 = 0 ∧ b1 = 0 ∧ out = i0) ∨
-  (b0 = 1 ∧ b1 = 0 ∧ out = i1) ∨
-  (b0 = 0 ∧ b1 = 1 ∧ out = i2) ∨
-  (b0 = 1 ∧ b1 = 1 ∧ out = i3)
-)-/
+
+-- In gnark 8 the number is decomposed in a binary vector with the length of the field order
+-- however this doesn't guarantee that the number is unique.
 def cmp_8 (a b out : ZMod N): Prop :=
   ((recover_binary_nat (nat_to_bits_le_full_n (binary_length N) a.val)) % N = a.val) ∧
   ((recover_binary_nat (nat_to_bits_le_full_n (binary_length N) b.val)) % N = b.val) ∧
   ((a = b ∧ out = 0) ∨
-  (ZMod.val a < ZMod.val b ∧ out = -1) ∨
-  (ZMod.val a > ZMod.val b ∧ out = 1))
+  (a.val < b.val ∧ out = -1) ∨
+  (a.val > b.val ∧ out = 1))
 
+-- In gnark 9 the number is reduced to the smallest representation, ensuring it is unique.
 def cmp_9 (a b out : ZMod N): Prop :=
   ((recover_binary_nat (nat_to_bits_le_full_n (binary_length N) a.val)) = a.val) ∧
   ((recover_binary_nat (nat_to_bits_le_full_n (binary_length N) b.val)) = b.val) ∧
   ((a = b ∧ out = 0) ∨
-  (ZMod.val a < ZMod.val b ∧ out = -1) ∨
-  (ZMod.val a > ZMod.val b ∧ out = 1))
+  (a.val < b.val ∧ out = -1) ∨
+  (a.val > b.val ∧ out = 1))
 
 -- Inverse is calculated using a Hint at circuit execution
-def is_zero (a out: ZMod N): Prop := (a ≠ 0 ∧ out = 1-(a*(1/a))) ∨ (a = 0 ∧ out = 1)  -- (a = 0 ∧ out = 1) ∨ (a != 0 ∧ out = 0)
+def is_zero (a out: ZMod N): Prop := (a ≠ 0 ∧ out = 1-(a*(1/a))) ∨ (a = 0 ∧ out = 1)
 def eq (a b : ZMod N): Prop := a = b
 def ne (a b : ZMod N): Prop := a ≠ b
 def le (a b : ZMod N): Prop :=
@@ -56,11 +55,8 @@ def le (a b : ZMod N): Prop :=
 def to_binary (a : ZMod N) (d : Nat) (out : Vector (ZMod N) d): Prop :=
   (@recover_binary_zmod' d N out).val = (a.val % 2^d) ∧ is_vector_binary out
 def from_binary {d} (a : Vector (ZMod N) d) (out : ZMod N) : Prop :=
-  (@recover_binary_zmod' d N a).val = (out.val % 2^d)
-end Gates
-
-variable {N : Nat}
-variable [Fact (Nat.Prime N)]
+  (@recover_binary_zmod' d N a).val = (out.val % 2^d) ∧ is_vector_binary a
+end GatesDef
 
 structure Gates_base (α : Type) : Type where
   is_bool : α → Prop
@@ -85,28 +81,30 @@ structure Gates_base (α : Type) : Type where
   to_binary : α → (n : Nat) → Vector α n → Prop
   from_binary : Vector α d → α → Prop
 
-def GatesGnark_8 : Gates_base (ZMod N) := {
-  is_bool := Gates.is_bool,
-  add := Gates.add,
-  mul_acc := Gates.mul_acc,
-  neg := Gates.neg,
-  sub := Gates.sub,
-  mul := Gates.mul,
-  div_unchecked := Gates.div_unchecked,
-  div := Gates.div,
-  inv := Gates.inv,
-  xor := Gates.xor,
-  or := Gates.or,
-  and := Gates.and,
-  select := Gates.select,
-  lookup := Gates.lookup,
-  cmp := Gates.cmp_8,
-  is_zero := Gates.is_zero,
-  eq := Gates.eq,
-  ne := Gates.ne,
-  le := Gates.le,
-  to_binary := Gates.to_binary,
-  from_binary := Gates.from_binary
+def GatesGnark_8 {N : Nat} [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
+  is_bool := GatesDef.is_bool,
+  add := GatesDef.add,
+  mul_acc := GatesDef.mul_acc,
+  neg := GatesDef.neg,
+  sub := GatesDef.sub,
+  mul := GatesDef.mul,
+  div_unchecked := GatesDef.div_unchecked,
+  div := GatesDef.div,
+  inv := GatesDef.inv,
+  xor := GatesDef.xor,
+  or := GatesDef.or,
+  and := GatesDef.and,
+  select := GatesDef.select,
+  lookup := GatesDef.lookup,
+  cmp := GatesDef.cmp_8,
+  is_zero := GatesDef.is_zero,
+  eq := GatesDef.eq,
+  ne := GatesDef.ne,
+  le := GatesDef.le,
+  to_binary := GatesDef.to_binary,
+  from_binary := GatesDef.from_binary
 }
 
---def GatesGnark_9 := { GatesGnark_8 with cmp := Gates.cmp_9  }
+def GatesGnark_9 {N : Nat} [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
+  GatesGnark_8 with cmp := GatesDef.cmp_9
+}

ProvenZk/GatesEquivalence.lean

@@ -37,8 +37,8 @@ theorem eq_mul_sides (a b out: ZMod N) : b ≠ 0 → ((out = a * b⁻¹) ↔ (ou
 
 @[simp]
 lemma is_bool_equivalence {a : ZMod N} :
-  Gates.is_bool a ↔ a = 0 ∨ a = 1 := by
-  unfold Gates.is_bool
+  GatesDef.is_bool a ↔ a = 0 ∨ a = 1 := by
+  unfold GatesDef.is_bool
   simp
   have : 1-a = 0 ↔ 1-a+a = a := by
     apply Iff.intro
@@ -54,8 +54,8 @@ lemma is_bool_equivalence {a : ZMod N} :
 
 @[simp]
 lemma div_equivalence {a b out : ZMod N} :
-  Gates.div a b out ↔ b ≠ 0 ∧ out = a * (1 / b) := by
-  unfold Gates.div
+  GatesDef.div a b out ↔ b ≠ 0 ∧ out = a * (1 / b) := by
+  unfold GatesDef.div
   rw [and_congr_right_iff]
   intro h
   rw [one_div, eq_mul_sides]
@@ -65,15 +65,15 @@ lemma div_equivalence {a b out : ZMod N} :
 
 @[simp]
 lemma div_unchecked_equivalence {a b out : ZMod N} :
-  Gates.div_unchecked a b out ↔ ((b ≠ 0 ∧ out = a * (1 / b)) ∨ (a = 0 ∧ b = 0 ∧ out = 0)) := by
-  unfold Gates.div_unchecked
-  rw [<-Gates.div]
+  GatesDef.div_unchecked a b out ↔ ((b ≠ 0 ∧ out = a * (1 / b)) ∨ (a = 0 ∧ b = 0 ∧ out = 0)) := by
+  unfold GatesDef.div_unchecked
+  rw [<-GatesDef.div]
   rw [<-div_equivalence]
 
 @[simp]
 lemma inv_equivalence {a out : ZMod N} :
-  Gates.inv a out ↔ a ≠ 0 ∧ out = 1 / a := by
-  unfold Gates.inv
+  GatesDef.inv a out ↔ a ≠ 0 ∧ out = 1 / a := by
+  unfold GatesDef.inv
   rw [one_div, and_congr_right_iff]
   intro h
   conv => rhs; rw [<-mul_one (a := a⁻¹)]; rw [mul_comm]
@@ -84,12 +84,12 @@ lemma inv_equivalence {a out : ZMod N} :
 
 @[simp]
 lemma xor_equivalence {a b out : ZMod N} :
-  Gates.xor a b out ↔
+  GatesDef.xor a b out ↔
   (a = 0 ∧ b = 0 ∧ out = 0) ∨
   (a = 0 ∧ b = 1 ∧ out = 1) ∨
   (a = 1 ∧ b = 0 ∧ out = 1) ∨
   (a = 1 ∧ b = 1 ∧ out = 0) := by
-  unfold Gates.xor
+  unfold GatesDef.xor
   apply Iff.intro
   . intro h
     simp at h
@@ -104,17 +104,17 @@ lemma xor_equivalence {a b out : ZMod N} :
     repeat (
       casesm* (_ ∧ _)
       subst_vars
-      simp [Gates.is_bool]
+      simp [GatesDef.is_bool]
     )
 
 @[simp]
 lemma or_equivalence {a b out : ZMod N} :
-  Gates.or a b out ↔
+  GatesDef.or a b out ↔
   (a = 0 ∧ b = 0 ∧ out = 0) ∨
   (a = 0 ∧ b = 1 ∧ out = 1) ∨
   (a = 1 ∧ b = 0 ∧ out = 1) ∨
   (a = 1 ∧ b = 1 ∧ out = 1) := by
-  unfold Gates.or
+  unfold GatesDef.or
   apply Iff.intro
   . intro h
     simp at h
@@ -129,17 +129,17 @@ lemma or_equivalence {a b out : ZMod N} :
     repeat (
       casesm* (_ ∧ _)
       subst_vars
-      simp [Gates.is_bool]
+      simp [GatesDef.is_bool]
     )
 
 @[simp]
 lemma and_equivalence {a b out : ZMod N} :
-  Gates.and a b out ↔
+  GatesDef.and a b out ↔
   (a = 0 ∧ b = 0 ∧ out = 0) ∨
   (a = 0 ∧ b = 1 ∧ out = 0) ∨
   (a = 1 ∧ b = 0 ∧ out = 0) ∨
   (a = 1 ∧ b = 1 ∧ out = 1) := by
-  unfold Gates.and
+  unfold GatesDef.and
   rw [is_bool_equivalence]
   rw [is_bool_equivalence]
   apply Iff.intro
@@ -161,8 +161,8 @@ lemma and_equivalence {a b out : ZMod N} :
 
 @[simp]
 lemma select_equivalence {b i1 i2 out : ZMod N} :
-  Gates.select b i1 i2 out ↔ (b = 0 ∨ b = 1) ∧ if b = 1 then out = i1 else out = i2 := by
-  unfold Gates.select
+  GatesDef.select b i1 i2 out ↔ (b = 0 ∨ b = 1) ∧ if b = 1 then out = i1 else out = i2 := by
+  unfold GatesDef.select
   rw [is_bool_equivalence]
   apply Iff.intro
   . intro h
@@ -186,8 +186,8 @@ lemma select_equivalence {b i1 i2 out : ZMod N} :
 
 @[simp]
 lemma select_equivalence' {b i1 i2 out : ZMod N} :
-  Gates.select b i1 i2 out ↔ (b = 1 ∧ out = i1) ∨ (b = 0 ∧ out = i2) := by
-  unfold Gates.select
+  GatesDef.select b i1 i2 out ↔ (b = 1 ∧ out = i1) ∨ (b = 0 ∧ out = i2) := by
+  unfold GatesDef.select
   rw [is_bool_equivalence]
   apply Iff.intro
   . intro h
@@ -208,12 +208,12 @@ lemma select_equivalence' {b i1 i2 out : ZMod N} :
 
 @[simp]
 lemma lookup_equivalence {b0 b1 i0 i1 i2 i3 out : ZMod N} :
-  Gates.lookup b0 b1 i0 i1 i2 i3 out ↔
+  GatesDef.lookup b0 b1 i0 i1 i2 i3 out ↔
   (b0 = 0 ∧ b1 = 0 ∧ out = i0) ∨
   (b0 = 1 ∧ b1 = 0 ∧ out = i1) ∨
   (b0 = 0 ∧ b1 = 1 ∧ out = i2) ∨
   (b0 = 1 ∧ b1 = 1 ∧ out = i3) := by
-  unfold Gates.lookup
+  unfold GatesDef.lookup
   rw [is_bool_equivalence]
   rw [is_bool_equivalence]
   apply Iff.intro
@@ -237,8 +237,8 @@ lemma cmp_equivalence : sorry := by sorry -- TODO
 
 @[simp]
 lemma is_zero_equivalence {a out: ZMod N} :
-  Gates.is_zero a out ↔ if a = 0 then out = 1 else out = 0 := by
-  unfold Gates.is_zero
+  GatesDef.is_zero a out ↔ if a = 0 then out = 1 else out = 0 := by
+  unfold GatesDef.is_zero
   rw [one_div, mul_comm]
   apply Iff.intro
   . intro h
@@ -263,8 +263,8 @@ lemma is_zero_equivalence {a out: ZMod N} :
 
 @[simp]
 lemma is_zero_equivalence' {a out: ZMod N} :
-  Gates.is_zero a out ↔ (a = 0 ∧ out = 1) ∨ (a ≠ 0 ∧ out = 0) := by
-  unfold Gates.is_zero
+  GatesDef.is_zero a out ↔ (a = 0 ∧ out = 1) ∨ (a ≠ 0 ∧ out = 0) := by
+  unfold GatesDef.is_zero
   rw [one_div, mul_comm]
   apply Iff.intro
   . intro h

ProvenZk/Misc.lean

@@ -1,13 +1,14 @@
 import ProvenZk.Gates
+import ProvenZk.GatesEquivalence
 import ProvenZk.Binary
 
 open  GatesEquivalence
 
 variable {N : Nat}
 variable [Fact (Nat.Prime N)]
 
-theorem or_rw (a b out : (ZMod N)) : Gates.or a b out ↔
-  (Gates.is_bool a ∧ Gates.is_bool b ∧
+theorem or_rw (a b out : (ZMod N)) : GatesDef.or a b out ↔
+  (GatesDef.is_bool a ∧ GatesDef.is_bool b ∧
   ( (out = 1 ∧ (a = 1 ∨ b = 1) ∨
     (out = 0 ∧ a = 0 ∧ b = 0)))) := by
   rw [or_equivalence]
@@ -31,7 +32,7 @@ theorem or_rw (a b out : (ZMod N)) : Gates.or a b out ↔
       tauto
     }
 
-lemma select_rw {b i1 i2 out : (ZMod N)} : (Gates.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with
+lemma select_rw {b i1 i2 out : (ZMod N)} : (GatesDef.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with
   | Bit.zero => out = i2
   | Bit.one => out = i1 := by
   rw [select_equivalence]
@@ -59,36 +60,36 @@ lemma select_rw {b i1 i2 out : (ZMod N)} : (Gates.select b i1 i2 out) ↔ is_bit
     )
 
 @[simp]
-theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by
+theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: GatesDef.is_bool a = is_bit a := by
   rw [is_bool_equivalence]
 
 @[simp]
-theorem select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by
-  simp [Gates.select]
+theorem select_zero {a b r : ZMod N}: GatesDef.select 0 a b r = (r = b) := by
+  simp [GatesDef.select]
 
 @[simp]
-theorem select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by
-  simp [Gates.select]
+theorem select_one {a b r : ZMod N}: GatesDef.select 1 a b r = (r = a) := by
+  simp [GatesDef.select]
 
 @[simp]
-theorem or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by
-  simp [Gates.or]
+theorem or_zero { a r : ZMod N}: GatesDef.or a 0 r = (is_bit a ∧ r = a) := by
+  simp [GatesDef.or]
 
 @[simp]
-theorem zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by
-  simp [Gates.or]
+theorem zero_or { a r : ZMod N}: GatesDef.or 0 a r = (is_bit a ∧ r = a) := by
+  simp [GatesDef.or]
 
 @[simp]
-theorem one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by
-  simp [Gates.or]
+theorem one_or { a r : ZMod N}: GatesDef.or 1 a r = (is_bit a ∧ r = 1) := by
+  simp [GatesDef.or]
 
 @[simp]
-theorem or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by
-  simp [Gates.or]
+theorem or_one { a r : ZMod N}: GatesDef.or a 1 r = (is_bit a ∧ r = 1) := by
+  simp [GatesDef.or]
 
 @[simp]
-theorem is_bit_one_sub {a : ZMod N}: is_bit (Gates.sub 1 a) ↔ is_bit a := by
-  simp [Gates.sub, is_bit, sub_eq_zero]
+theorem is_bit_one_sub {a : ZMod N}: is_bit (GatesDef.sub 1 a) ↔ is_bit a := by
+  simp [GatesDef.sub, is_bit, sub_eq_zero]
   tauto
 
 lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by