From f7bd0d1761064feaa5b9f33776bd2cc9a941fb78 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Tue, 12 Mar 2024 22:55:22 +0000
Subject: [PATCH] Fix cmp/le definitions

---
 ProvenZk/Binary.lean | 22 ----------------------
 ProvenZk/Gates.lean  | 12 ++++--------
 2 files changed, 4 insertions(+), 30 deletions(-)

diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean
index f6a77a5..94f91ce 100644
--- 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
index 84a2d9d..3eeebed 100644
--- 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 :=