From eafa2cb91bf425ac2fac258271d6a0bb08f18a87 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Sat, 16 Dec 2023 00:17:45 +0000 Subject: [PATCH] Added to_binary and from_binary --- ProvenZk/Binary.lean | 78 +++++++++++++++++---- ProvenZk/Gates.lean | 37 ++++++++++ ProvenZk/GatesEquivalence.lean | 124 +++++++++++++++++++++++++++++++-- 3 files changed, 220 insertions(+), 19 deletions(-) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index b5f1fc8..fb2e7c0 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -178,6 +178,50 @@ def vector_zmod_to_bit {n d : Nat} (a : Vector (ZMod n) d) : Vector Bit d := def vector_bit_to_zmod {n d : Nat} (a : Vector Bit d) : Vector (ZMod n) d := Vector.map (fun x => Bit.toZMod x) a +lemma bit_to_zmod_equiv {d} [Fact (n > 1)] (x : Vector Bit d) (y : Vector (ZMod n) d) (h : is_vector_binary y): + vector_bit_to_zmod x = y ↔ x = vector_zmod_to_bit y := by + apply Iff.intro + . intro hv + rename_i d + rw [<-hv] + induction x, y using Vector.inductionOn₂ with + | nil => simp + | cons ih=> + rename_i x y xs ys + simp [vector_bit_to_zmod, vector_zmod_to_bit] + simp [Vector.vector_eq_cons] + refine ⟨?_, ?_⟩ + . simp [bit_to_zmod_to_bit] + . rw [<-vector_bit_to_zmod, <-vector_zmod_to_bit] + apply ih + . simp [is_vector_binary_cons] at h + tauto + . simp [vector_bit_to_zmod] at hv + simp [Vector.vector_eq_cons] at hv + rw [<-vector_bit_to_zmod] at hv + tauto + . intro hv + rename_i d + rw [hv] + induction x, y using Vector.inductionOn₂ with + | nil => simp + | cons ih=> + rename_i x y xs ys + simp [vector_bit_to_zmod, vector_zmod_to_bit] + simp [Vector.vector_eq_cons] + refine ⟨?_, ?_⟩ + . rw [zmod_to_bit_to_zmod] + . simp [is_vector_binary_cons] at h + tauto + . rw [<-vector_bit_to_zmod, <-vector_zmod_to_bit] + apply ih + . simp [is_vector_binary_cons] at h + tauto + . simp [vector_zmod_to_bit] at hv + simp [Vector.vector_eq_cons] at hv + rw [<-vector_zmod_to_bit] at hv + tauto + lemma vector_zmod_to_bit_last {n d : Nat} {xs : Vector (ZMod n) (d+1)} : (vector_zmod_to_bit xs).last = (zmod_to_bit xs.last) := by simp [vector_zmod_to_bit, Vector.last] @@ -297,19 +341,21 @@ lemma parity_bit_unique (a b : Bit) (c d : Nat) : a + 2 * c = b + 2 * d -> a = b . assumption theorem binary_nat_unique {d} (rep1 rep2 : Vector Bit d): - recover_binary_nat rep1 = recover_binary_nat rep2 -> rep1 = rep2 := by - intro h - induction d with - | zero => apply Vector.zero_subsingleton.allEq; - | succ d1 ih => - simp [recover_binary_nat] at h - rw [←Vector.cons_head_tail rep1] - rw [←Vector.cons_head_tail rep2] - have h := parity_bit_unique _ _ _ _ h - cases h - apply congr - . apply congrArg; assumption - . apply ih; assumption + recover_binary_nat rep1 = recover_binary_nat rep2 ↔ rep1 = rep2 := by + apply Iff.intro + . intro h + induction d with + | zero => apply Vector.zero_subsingleton.allEq; + | succ d1 ih => + simp [recover_binary_nat] at h + rw [←Vector.cons_head_tail rep1] + rw [←Vector.cons_head_tail rep2] + have h := parity_bit_unique _ _ _ _ h + cases h + apply congr + . apply congrArg; assumption + . apply ih; assumption + . tauto theorem binary_nat_lt {d} (rep : Vector Bit d): recover_binary_nat rep < 2 ^ d := by induction d with @@ -363,7 +409,8 @@ theorem binary_zmod_unique {n d} (rep1 rep2 : Vector Bit d): rw [same_recs] rw [binary_zmod_same_as_nat rep1 d_small] at same_vals rw [binary_zmod_same_as_nat rep2 d_small] at same_vals - exact binary_nat_unique _ _ same_vals + simp [binary_nat_unique] at same_vals + tauto theorem recover_binary_nat_to_bits_le {w : Vector Bit d}: recover_binary_nat w = v ↔ @@ -646,7 +693,8 @@ theorem fin_to_bits_le_recover_binary_nat {v : Vector Bit d}: split . rename_i h rw [←recover_binary_nat_to_bits_le] at h - exact binary_nat_unique _ _ h + simp [binary_nat_unique] at h + tauto . contradiction theorem SubVector_map_cast_lower {v : SubVector α n prop} {f : α → β }: diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean index d4ede6e..7997b89 100644 --- a/ProvenZk/Gates.lean +++ b/ProvenZk/Gates.lean @@ -117,3 +117,40 @@ def GatesGnark_9 (N : Nat) [Fact (Nat.Prime N)] : Gates_base (ZMod N) := { cmp := GatesDef.cmp_9 le := GatesDef.le_9 } + +lemma recover_nat_unique (N : Nat) [Fact (Nat.Prime N)] (i1 i2 : Vector Bit (binary_length N)) : + i1 = i2 ↔ recover_binary_nat i1 = recover_binary_nat i2 := by + apply Iff.intro + . apply congr_arg + . simp [binary_nat_unique] + +lemma recover_nat_different (N : Nat) [Fact (Nat.Prime N)] (i1 i2 : Vector Bit (binary_length N)) : + i1 ≠ i2 ↔ recover_binary_nat i1 ≠ recover_binary_nat i2 := by + simp [recover_nat_unique] + +-- Given a Vector of size `binary_length N`, there are at least two numbers with length `binary_length N` +-- whose `mod N` returns the same value. +lemma recover_mod_not_unique (N : Nat) [Fact (Nat.Prime N)] (i1 i2 : Vector Bit (binary_length N)) : + (recover_binary_nat i2) % N = (recover_binary_nat i1) % N → + ((recover_binary_nat i2) + N) % N = (recover_binary_nat i1) % N:= by + intros + simp [Nat.mod_eq_sub_mod] + tauto + +lemma recover_unique (N : Nat) [Fact (Nat.Prime N)] (i1 : Vector Bit (binary_length N)) : + ∃i2 : Vector Bit (binary_length N), + (recover_binary_nat i2) = (recover_binary_nat i1) → + i2 = i1 := by + apply Exists.intro + rotate_left + . assumption + . tauto + +/- +Given three numbers +`i1` `i2` and `i3 = i2 + N` +→ +le i1 i2 = le i1 i3 +although +i1 < i2 ≠ i1 < i3 +-/ diff --git a/ProvenZk/GatesEquivalence.lean b/ProvenZk/GatesEquivalence.lean index bc5a034..456a99e 100644 --- a/ProvenZk/GatesEquivalence.lean +++ b/ProvenZk/GatesEquivalence.lean @@ -35,6 +35,18 @@ theorem eq_mul_sides (a b out: ZMod N) : b ≠ 0 → ((out = a * b⁻¹) ↔ (ou . tauto . contradiction +lemma split_vector_eq_cons {x : α} {xs : Vector α d} {y : Vector α d.succ} : + x ::ᵥ xs = y ↔ x = y.head ∧ xs = y.tail := by + apply Iff.intro + . intro h + rw [<-h] + simp + . intro h + casesm* (_ ∧ _) + rename_i hx hxs + rw [hx, hxs] + simp + @[simp] lemma is_bool_equivalence {a : ZMod N} : GatesDef.is_bool a ↔ a = 0 ∨ a = 1 := by @@ -233,7 +245,9 @@ lemma lookup_equivalence {b0 b1 i0 i1 i2 i3 out : ZMod N} : ) @[simp] -lemma cmp_equivalence : sorry := by sorry -- TODO +lemma cmp_equivalence {a b out : ZMod N} : + GatesDef.cmp_9 a b out ↔ if a = b then out = 0 else (if a.val < b.val then out = -1 else out = 1) := by + sorry -- TODO @[simp] lemma is_zero_equivalence {a out: ZMod N} : @@ -289,12 +303,114 @@ lemma is_zero_equivalence' {a out: ZMod N} : . tauto @[simp] -lemma le_equivalence : sorry := by sorry -- TODO +lemma le_equivalence {a b : ZMod N} : + GatesDef.le_9 a b ↔ a.val < b.val := by + sorry -- TODO +def nat_to_binary_self {d : Nat} {h : d >= 1} : + recover_binary_nat (nat_to_bits_le_full_n d x) = x % 2^d := by + induction d generalizing x with + | zero => + contradiction + | succ d' ih => + simp [recover_binary_nat, nat_to_bits_le_full_n] + have : recover_binary_nat (nat_to_bits_le_full_n d' (x / 2)) = (x/2) % 2^d' := by + if 1 <= d' then + rw [ih (x := x/2)] + rw [Nat.succ_eq_add_one] at h + rw [ge_iff_le, le_add_iff_nonneg_left] at h + linarith + else + have : d' = 0 := by + linarith + subst_vars + simp [nat_to_bits_le_full_n, recover_binary_nat, Nat.mod_one] + rw [this] + rw [<-Nat.div2_val] + simp [bit_mod_two] + split + . rename_i h + simp only [Bit.toNat] + rw [Nat.mod_pow_succ] + rw [<-Nat.div2_val] + rw [h] + simp_arith + . rename_i h + simp only [Bit.toNat] + rw [Nat.mod_pow_succ] + rw [<-Nat.div2_val] + rw [h] + simp_arith + . rename_i h + apply False.elim (by + have := Nat.mod_lt x (y := 2) + rw [h] at this + simp at this + contradiction + ) + +-- Should `hd : 2^d < N` be a hypothesis? @[simp] -lemma to_binary_equivalence : sorry := by sorry -- TODO +lemma to_binary_equivalence {a : ZMod N} {d : Nat} {out : Vector (ZMod N) d} (hd : 2^d < N) : + GatesDef.to_binary a d out ↔ vector_bit_to_zmod (nat_to_bits_le_full_n d a.val) = out := by + apply Iff.intro + . intro h + unfold GatesDef.to_binary at h + casesm* (_ ∧ _) + rename_i h hbin + rw [recover_binary_zmod_bit] at h + rw [binary_nat_zmod_equiv_mod_p] at h + rw [<-ZMod.val_nat_cast] at h + rw [ZMod.val_nat_cast_of_lt] at h + . induction d generalizing a with + | zero => simp + | succ d' _ => + rw [<-nat_to_binary_self] at h + . simp [binary_nat_unique] at h + rw [bit_to_zmod_equiv] + rw [h] + simp [hbin] + . rw [<-Nat.add_one] + linarith + . rw [<-@binary_zmod_same_as_nat (n := N) (d := d) (rep := vector_zmod_to_bit out)] + . apply ZMod.val_lt + . simp [hd] + . simp [hbin] + . unfold GatesDef.to_binary + intro h + have hbin : is_vector_binary out := by + rw [<-h] + rw [vector_bit_to_zmod] + simp [vector_binary_of_bit_to_zmod] + rw [recover_binary_zmod_bit] + rw [binary_nat_zmod_equiv_mod_p] + rw [<-ZMod.val_nat_cast] + rw [ZMod.val_nat_cast_of_lt] + refine ⟨?_, ?_⟩ + . induction d generalizing a with + | zero => + simp [Nat.mod_one] + simp [vector_zmod_to_bit, recover_binary_nat] + | succ d' _ => + rw [<-nat_to_binary_self] + . simp [binary_nat_unique] + apply Eq.symm + rw [<-bit_to_zmod_equiv] + . rw [h] + . simp [hbin] + . rw [<-Nat.add_one] + linarith + . simp [hbin] + . rw [<-@binary_zmod_same_as_nat (n := N) (d := d) (rep := vector_zmod_to_bit out)] + . apply ZMod.val_lt + . simp [hd] + . simp [hbin] @[simp] -lemma from_binary_equivalence : sorry := by sorry -- TODO +lemma from_binary_equivalence {d} {a : Vector (ZMod N) d} {out : ZMod N} (hd : 2^d < N) : + GatesDef.from_binary a out ↔ vector_bit_to_zmod (nat_to_bits_le_full_n d out.val) = a := by + unfold GatesDef.from_binary + rw [<-GatesDef.to_binary] + apply to_binary_equivalence (hd := hd) end GatesEquivalence