From 681155e030f213b29348f411ca2045f41031d0c3 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 7 Mar 2024 18:25:13 +0000
Subject: [PATCH] Updated gates

---
 ProvenZk/Gates.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean
index 0eef002..84a2d9d 100644
--- a/ProvenZk/Gates.lean
+++ b/ProvenZk/Gates.lean
@@ -41,7 +41,6 @@ def cmp_9 (a b out : ZMod N): Prop :=
   (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 = 0) ∨ (a = 0 ∧ out = 1)
 def eq (a b : ZMod N): Prop := a = b
 def ne (a b : ZMod N): Prop := a ≠ b
@@ -56,9 +55,6 @@ def le_9 (a b : ZMod N): Prop :=
   (recover_binary_nat (nat_to_bits_le_full_n (binary_length N) b.val)) = b.val ∧
   a.val <= b.val
 
--- `a(.val)` is always less than `N` because it's `ZMod`.
--- If `a` doesn't fit in `n`, then the result of `recover_binary_zmod'` is `a % 2^n`
--- If `a` fits `n`, the result is exact
 def to_binary (a : ZMod N) (d : Nat) (out : Vector (ZMod N) d): Prop :=
   @recover_binary_zmod' d N out = a ∧ is_vector_binary out
 def from_binary {d} (a : Vector (ZMod N) d) (out : ZMod N) : Prop :=