Fix cmp/le definitions

reilabs · Mar 12, 2024 · f7bd0d1 · f7bd0d1
1 parent 681155e
commit f7bd0d1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 30 deletions.
diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean
@@ -107,10 +107,6 @@ lemma is_vector_binary_iff_exists_bool_vec {N n : ℕ} {v : Vector (ZMod N) n}:
       simp [Vector.toList, htl]
       rfl
 
-def recover_binary_nat {d} (rep : Vector Bool d): Nat := match d with
-  | 0 => 0
-  | Nat.succ _ => rep.head.toNat + 2 * recover_binary_nat rep.tail
-
 def recover_binary_zmod' {d n} (rep : Vector (ZMod n) d) : ZMod n := match d with
   | 0 => 0
   | Nat.succ _ => rep.head + 2 * recover_binary_zmod' rep.tail
@@ -121,24 +117,6 @@ protected theorem Nat.add_lt_add_of_le_of_lt {a b c d : Nat} (hle : a ≤ b) (hl
 
 def binary_length (n : Nat) : Nat := (Nat.log 2 n).succ
 
-def bit_mod_two (inp : Nat) : Bool := match h:inp%2 with
- | 0 => false
- | 1 => true
- | x + 2 => False.elim (by
-    have := Nat.mod_lt inp (y := 2)
-    rw [h] at this
-    simp at this
-    contradiction
- )
-
-def nat_to_bits_le_full_n (l : Nat): Nat → Vector Bool l := match l with
-  | 0 => fun _ => Vector.nil
-  | Nat.succ l => fun i =>
-    let x := i / 2
-    let y := bit_mod_two i
-    let xs := nat_to_bits_le_full_n l x
-    y ::ᵥ xs
-
 namespace Fin
 
 def msb {d:ℕ} (v : Fin (2^d.succ)): Bool := v.val ≥ 2^d

diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean
@@ -27,16 +27,14 @@ def lookup (b0 b1 i0 i1 i2 i3 out : ZMod N): Prop :=
 -- 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) ∧
+  ∃z w: Fin (binary_length N), z.val % N = a.val ∧ w.val % N = b.val ∧
   ((a = b ∧ out = 0) ∨
   (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) ∧
+  ∃z w: Fin (binary_length N), z.val = a.val ∧ w.val = b.val ∧
   ((a = b ∧ out = 0) ∨
   (a.val < b.val ∧ out = -1) ∨
   (a.val > b.val ∧ out = 1))
@@ -46,13 +44,11 @@ def eq (a b : ZMod N): Prop := a = b
 def ne (a b : ZMod N): Prop := a ≠ b
 
 def le_8 (a b : 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 ∧
+  ∃z w: Fin (binary_length N), z.val % N = a.val ∧ w.val % N = b.val ∧
   a.val <= b.val
 
 def le_9 (a b : 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 ∧
+  ∃z w: Fin (binary_length N), z.val = a.val ∧ w.val = b.val ∧
   a.val <= b.val
 
 def to_binary (a : ZMod N) (d : Nat) (out : Vector (ZMod N) d): Prop :=