From 0e12d806b49c00f81388a11b861ac0ea3cf1fcae Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Sat, 21 Oct 2023 13:29:51 +0100 Subject: [PATCH 01/18] Added theorems for delete circuit --- ProvenZk/Ext/Vector/Basic.lean | 5 ++++- ProvenZk/Merkle.lean | 38 ++++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 1d18f97..9ce376e 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -186,7 +186,10 @@ theorem vector_map_inj {a b : Vector α d} {f_inj : ∀ a b, f a = f b → a = b def dropLast { n : Nat } (v : Vector α n) : Vector α (n-1) := ⟨List.dropLast v.toList, by simp⟩ -theorem toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toList.dropLast := by +lemma toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toList.dropLast := by + rfl + +lemma vector_list_vector {d} {x₁ x₂ : α} {xs : Vector α d} : (x₁ ::ᵥ x₂ ::ᵥ xs).dropLast = x₁ ::ᵥ (x₂ ::ᵥ xs).dropLast := by rfl end Vector diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index e35a393..6e0cc33 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -114,6 +114,20 @@ theorem nat_to_dir_vec_unique {ix₁ ix₂ : Nat} {r₁ r₂ : Vector Dir d}: rfl . intro a b; cases a <;> { cases b <;> tauto } +lemma dropLastOrder {d n : Nat} {out : Vector (ZMod n) d} : Dir.create_dir_vec (Vector.dropLast out) = (Dir.create_dir_vec out).dropLast := by + induction out using Vector.inductionOn with + | h_nil => + simp [Dir.create_dir_vec, Vector.dropLast, Dir.nat_to_dir, Vector.map] + | h_cons ih₁ => + rename_i x₁ xs + induction xs using Vector.inductionOn with + | h_nil => + simp [Dir.create_dir_vec, Vector.dropLast, Dir.nat_to_dir, Vector.map] + | h_cons _ => + rename_i x₂ xs + simp [Vector.vector_list_vector] + simp [ih₁] + end Dir inductive MerkleTree (F: Type) (H : Hash F 2) : Nat -> Type @@ -403,4 +417,28 @@ theorem recover_proof_reversible {H : Hash α 2} [Fact (perfect_hash H)] {Tree : assumption } +theorem recover_equivalence + {F depth} + (H : Hash F 2) + [Fact (perfect_hash H)] + (tree : MerkleTree F H depth) + (Path : Vector Dir depth) + (Proof : Vector F depth) + (Item : F) : + (item_at tree Path = Item ∧ proof tree Path = Proof) ↔ + recover H Path Proof Item = tree.root := by + apply Iff.intro + . intros + casesm* (_ ∧ _) + rename_i hitem_at hproof + rw [<-hitem_at] + rw [<-hproof] + apply recover_proof_is_root + . intros + apply And.intro + . apply proof_ceritfies_item (proof := Proof) + assumption + . apply recover_proof_reversible (Item := Item) + assumption + end MerkleTree \ No newline at end of file From e682985d44b5db59fad19da09b4bc03381d4eee6 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Sat, 21 Oct 2023 18:07:38 +0100 Subject: [PATCH 02/18] Refactoring zmod_to_bit --- ProvenZk/Binary.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 0e9963c..4e4ef3f 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -97,7 +97,7 @@ theorem is_vector_binary_dropLast {d n : Nat} {gate_0 : Vector (ZMod n) d} : is_ tauto def vector_zmod_to_bit {n d : Nat} (a : Vector (ZMod n) d) : Vector Bit d := - Vector.map nat_to_bit (Vector.map ZMod.val a) + Vector.map zmod_to_bit a @[simp] theorem vector_zmod_to_bit_cons : vector_zmod_to_bit (x ::ᵥ xs) = (nat_to_bit x.val) ::ᵥ vector_zmod_to_bit xs := by @@ -323,7 +323,6 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : vector_zmo apply absurd this simp | succ => - rw [ZMod.val] simp rfl } From d1ac1762aba5cb9a892de075d29139a35a446f3a Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Sat, 21 Oct 2023 18:20:39 +0100 Subject: [PATCH 03/18] New binary theorems --- ProvenZk/Binary.lean | 70 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 4e4ef3f..be2c5b3 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -96,9 +96,79 @@ theorem is_vector_binary_dropLast {d n : Nat} {gate_0 : Vector (ZMod n) d} : is_ cases h tauto +lemma dropLast_symm {n} {xs : Vector Bit d} : + Vector.map (fun i => @Bit.toZMod n i) (Vector.dropLast xs) = (Vector.map (fun i => @Bit.toZMod n i) xs).dropLast := by + induction xs using Vector.inductionOn with + | h_nil => + simp [Vector.dropLast, Vector.map] + | h_cons ih₁ => + rename_i x₁ xs + induction xs using Vector.inductionOn with + | h_nil => + simp [Vector.dropLast, Vector.map] + | h_cons _ => + rename_i x₂ xs + simp [Vector.vector_list_vector] + simp [ih₁] + +lemma zmod_to_bit_to_zmod {n : Nat} [Fact (n > 1)] {x : (ZMod n)} (h : is_bit x): + Bit.toZMod (zmod_to_bit x) = x := by + simp [is_bit] at h + cases h with + | inl => + subst_vars + simp [zmod_to_bit, Bit.toZMod] + | inr => + subst_vars + simp [zmod_to_bit, ZMod.val_one, Bit.toZMod] + +lemma bit_to_zmod_to_bit {n : Nat} [Fact (n > 1)] {x : Bit}: + zmod_to_bit (@Bit.toZMod n x) = x := by + cases x with + | zero => + simp [zmod_to_bit, Bit.toZMod] + | one => + simp [zmod_to_bit, Bit.toZMod] + simp [zmod_to_bit, ZMod.val_one, Bit.toZMod] + def vector_zmod_to_bit {n d : Nat} (a : Vector (ZMod n) d) : Vector Bit d := Vector.map zmod_to_bit a +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] + +lemma vector_zmod_to_bit_to_zmod {n d : Nat} [Fact (n > 1)] {xs : Vector (ZMod n) d} (h : is_vector_binary xs) : + Vector.map Bit.toZMod (vector_zmod_to_bit xs) = xs := by + induction xs using Vector.inductionOn with + | h_nil => simp + | h_cons ih => + simp [is_vector_binary_cons] at h + cases h + simp [vector_zmod_to_bit] + simp [vector_zmod_to_bit] at ih + rw [zmod_to_bit_to_zmod] + rw [ih] + assumption + assumption + +lemma vector_bit_to_zmod_to_bit {d n : Nat} [Fact (n > 1)] {xs : Vector Bit d} : + vector_zmod_to_bit (Vector.map (fun i => @Bit.toZMod n i) xs) = xs := by + induction xs using Vector.inductionOn with + | h_nil => simp + | h_cons ih => + rename_i x xs + simp [vector_zmod_to_bit] + simp [vector_zmod_to_bit] at ih + simp [ih] + rw [bit_to_zmod_to_bit] + +lemma vector_zmod_to_bit_dropLast {n d : Nat} [Fact (n > 1)] {xs : Vector (ZMod n) (d+1)} (h : is_vector_binary xs) : + Vector.map Bit.toZMod (Vector.dropLast (vector_zmod_to_bit xs)) = (Vector.dropLast xs) := by + simp [dropLast_symm] + rw [vector_zmod_to_bit_to_zmod] + assumption + @[simp] theorem vector_zmod_to_bit_cons : vector_zmod_to_bit (x ::ᵥ xs) = (nat_to_bit x.val) ::ᵥ vector_zmod_to_bit xs := by rfl From 58037374a3be5d6bedacd3f491de8eb8fa956aeb Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 25 Oct 2023 20:17:27 +0100 Subject: [PATCH 04/18] Merkle theorem --- ProvenZk/Merkle.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 6e0cc33..9b98d59 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -338,6 +338,12 @@ theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} (tree : Me simp [set] split <;> simp [item_at, tree_for, left, right, *] +lemma set_implies_item_at { depth : Nat } {F: Type} {H : Hash F 2} {t₁ t₂ : MerkleTree F H depth} {ix : Vector Dir depth} {item : F} : + set t₁ ix item = t₂ → item_at t₂ ix = item := by + intro h + rw [<-h] + apply read_after_insert_sound + -- Related to recover_proof_is_root theorem proof_ceritfies_item {depth : Nat} @@ -441,4 +447,4 @@ theorem recover_equivalence . apply recover_proof_reversible (Item := Item) assumption -end MerkleTree \ No newline at end of file +end MerkleTree From 4d6558d5b0032f243257a93759fb7ed73aa63f2c Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Fri, 27 Oct 2023 23:07:04 +0100 Subject: [PATCH 05/18] New theorems for deletion circuit and updated mathlib --- ProvenZk/Binary.lean | 87 +++++++++++++++++++++++++++++++++++++++----- ProvenZk/Merkle.lean | 81 +++++++++++++++++++++++++++++++++++++++++ lake-manifest.json | 4 +- lakefile.lean | 2 +- 4 files changed, 162 insertions(+), 12 deletions(-) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index be2c5b3..3b4f82e 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -82,7 +82,8 @@ theorem is_vector_binary_cons {a : ZMod n} {vec : Vector (ZMod n) d}: unfold is_vector_binary conv => lhs; unfold List.foldr; simp -theorem is_vector_binary_dropLast {d n : Nat} {gate_0 : Vector (ZMod n) d} : is_vector_binary gate_0 → is_vector_binary (Vector.dropLast gate_0) := by +theorem is_vector_binary_dropLast {d n : Nat} {gate_0 : Vector (ZMod n) d} : + is_vector_binary gate_0 → is_vector_binary (Vector.dropLast gate_0) := by simp [is_vector_binary, Vector.toList_dropLast] intro h induction gate_0 using Vector.inductionOn with @@ -191,7 +192,8 @@ theorem recover_binary_nat_zero {n : Nat} : recover_binary_nat (Vector.replicate | zero => rfl | succ n ih => simp [recover_binary_nat, ih] -theorem recover_binary_zmod_bit {d n} [Fact (n > 1)] {w : Vector (ZMod n) d}: is_vector_binary w → recover_binary_zmod' w = recover_binary_zmod (vector_zmod_to_bit w) := by +theorem recover_binary_zmod_bit {d n} [Fact (n > 1)] {w : Vector (ZMod n) d}: + is_vector_binary w → recover_binary_zmod' w = recover_binary_zmod (vector_zmod_to_bit w) := by intro h induction w using Vector.inductionOn with | h_nil => rfl @@ -210,7 +212,7 @@ theorem recover_binary_zmod_bit {d n} [Fact (n > 1)] {w : Vector (ZMod n) d}: i | zero => simp | succ n => induction n with - | zero => + | zero => simp | succ => rw [ZMod.val] @@ -248,7 +250,8 @@ lemma parity_bit_unique (a b : Bit) (c d : Nat) : a + 2 * c = b + 2 * d -> a = b . rw [add_comm, eq_comm] at h; apply even_ne_odd _ _ h . assumption -theorem binary_nat_unique {d} (rep1 rep2 : Vector Bit d): recover_binary_nat rep1 = recover_binary_nat rep2 -> rep1 = rep2 := by +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; @@ -373,7 +376,8 @@ theorem recover_binary_zmod'_to_bits_le {n : Nat} [Fact (n > 1)] {v : ZMod n} {w assumption . assumption -theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : vector_zmod_to_bit (Vector.map (Bit.toZMod (n := n)) w) = w := by +theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : + vector_zmod_to_bit (Vector.map (Bit.toZMod (n := n)) w) = w := by induction w using Vector.inductionOn with | h_nil => rfl | h_cons ih => @@ -389,7 +393,7 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : vector_zmo simp | succ n => induction n with - | zero => + | zero => apply absurd this simp | succ => @@ -397,7 +401,8 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : vector_zmo rfl } -theorem vector_binary_of_bit_to_zmod {n : Nat} [Fact (n > 1)] {w : Vector Bit d }: is_vector_binary (w.map (Bit.toZMod (n := n))) := by +theorem vector_binary_of_bit_to_zmod {n : Nat} [Fact (n > 1)] {w : Vector Bit d }: + is_vector_binary (w.map (Bit.toZMod (n := n))) := by induction w using Vector.inductionOn with | h_nil => trivial | h_cons ih => @@ -412,7 +417,7 @@ theorem vector_binary_of_bit_to_zmod {n : Nat} [Fact (n > 1)] {w : Vector Bit d simp | succ n => induction n with - | zero => + | zero => apply absurd this simp | succ => @@ -428,4 +433,68 @@ theorem recover_binary_of_to_bits {n : Nat} [Fact (n > 1)] {w : Vector Bit d} {v rw [←binary_nat_zmod_equiv] rw [h] simp [ZMod.val_cast_of_lt] - apply vector_binary_of_bit_to_zmod \ No newline at end of file + apply vector_binary_of_bit_to_zmod + +theorem nat_to_bits_le_some_of_lt : n < 2 ^ d → ∃p, nat_to_bits_le d n = some p := by + induction d generalizing n with + | zero => intro h; simp at h; rw [h]; exists Vector.nil + | succ d ih => + intro h + have := ih (n := n / 2) (by + have : 2 ^ d = (2 ^ d.succ) / 2 := by + simp [Nat.pow_succ] + rw [this] + apply Nat.div_lt_div_of_lt_of_dvd + simp [Nat.pow_succ] + assumption + ) + rcases this with ⟨_, h⟩ + apply Exists.intro + unfold nat_to_bits_le + simp [h, Bind.bind] + rfl + +def fin_to_bits_le {d : Nat} (n : Fin (2 ^ d)): Vector Bit d := match h: nat_to_bits_le d n.val with +| some r => r +| none => False.elim (by + have := nat_to_bits_le_some_of_lt n.prop + cases this + simp [*] at h + ) + +theorem fin_to_bits_le_to_recover_binary_zmod' {n d : Nat} [Fact (n > 1)] {v : ZMod n} {w : Vector (ZMod n) d} {h : v.val < 2^d }: + n > 2^d → + is_vector_binary w → + recover_binary_zmod' w = v → + fin_to_bits_le ⟨v.val, by simp[h]⟩ = vector_zmod_to_bit w := by + intros + have : some (fin_to_bits_le ⟨v.val, by simp[h]⟩) = some (vector_zmod_to_bit w) := by + rw [<-recover_binary_zmod'_to_bits_le] + rotate_left + linarith + assumption + assumption + simp [recover_binary_nat_to_bits_le] + simp [fin_to_bits_le] + split + rename_i h + simp [h] + contradiction + simp at this + rw [this] + +lemma vector_bit_to_zmod_last {d n : Nat} [Fact (n > 1)] {xs : Vector Bit (d+1)} : + (zmod_to_bit (Vector.last (Vector.map (fun i => @Bit.toZMod n i) xs))) = Vector.last xs := by + cases xs using Vector.casesOn + simp + rename_i x xs + rw [<-vector_zmod_to_bit_last] + simp + have hx : nat_to_bit (ZMod.val (@Bit.toZMod n x)) = x := by + simp [Bit.toZMod, is_bit, nat_to_bit] + cases x + . simp + . simp [ZMod.val_one] + have hxs : vector_zmod_to_bit (Vector.map (fun i => @Bit.toZMod n i) xs) = xs := by + simp [vector_bit_to_zmod_to_bit] + rw [hx, hxs] diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 9b98d59..593c606 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -1,3 +1,5 @@ +import Mathlib.Data.Vector.MapLemmas + import ProvenZk.Ext.Vector import ProvenZk.Hash import ProvenZk.Binary @@ -128,6 +130,79 @@ lemma dropLastOrder {d n : Nat} {out : Vector (ZMod n) d} : Dir.create_dir_vec ( simp [Vector.vector_list_vector] simp [ih₁] +def fin_to_dir_vec {depth : Nat} (idx : Fin (2 ^ depth)): Vector Dir depth := + (Vector.map Dir.bit_to_dir (fin_to_bits_le idx)) + +lemma zmod_to_bit_and_dir {n : Nat} [Fact (n > 1)] {x : ZMod n} {h : is_bit x}: + Dir.bit_to_dir (zmod_to_bit x) = Dir.nat_to_dir (ZMod.val x) := by + simp only [zmod_to_bit] + simp only [Dir.bit_to_dir] + simp only [Dir.nat_to_dir] + cases h with + | inl => + rename_i h + simp [h] + | inr => + rename_i h + simp [h] + rw [ZMod.val_one] + +lemma vector_zmod_to_bit_and_dir {n : Nat} [Fact (n > 1)] {w : Vector (ZMod n) d} : + is_vector_binary w → + Vector.map (fun x => Dir.bit_to_dir (zmod_to_bit x)) w = Vector.map (fun x => Dir.nat_to_dir (ZMod.val x)) w := by + induction w using Vector.inductionOn with + | h_nil => + simp + | h_cons ih => + intro h + simp [is_vector_binary_cons] at h + cases h + rename_i y ys + simp + rw [zmod_to_bit_and_dir] + rw [ih] + assumption + assumption + +theorem recover_binary_zmod'_to_dir {n d : Nat} [Fact (n > 1)] {v : ZMod n} {w : Vector (ZMod n) d}: + v.val < 2^d → + n > 2^d → + is_vector_binary w → + recover_binary_zmod' w = v → + fin_to_dir_vec v.val = (Dir.create_dir_vec w) := by + intros + simp [fin_to_dir_vec] + simp [fin_to_bits_le] + split + . simp [Dir.create_dir_vec] + rename_i r _ + have : some r = some (vector_zmod_to_bit w) := by + rw [<-@recover_binary_zmod'_to_bits_le (v:= v)] + apply Eq.symm + rename_i h + rw [ZMod.cast_eq_val] at h + rw [Fin.val_cast_of_lt] at h + assumption + assumption + assumption + linarith + assumption + assumption + simp at this + rw [this] + simp [vector_zmod_to_bit] + rw [vector_zmod_to_bit_and_dir] + assumption + . rename_i hfin _ _ _ h + rw [ZMod.cast_eq_val] at h + rw [Fin.val_cast_of_lt] at h + apply False.elim (by + have := nat_to_bits_le_some_of_lt hfin + cases this + simp [*] at h + ) + assumption + end Dir inductive MerkleTree (F: Type) (H : Hash F 2) : Nat -> Type @@ -164,6 +239,9 @@ def item_at {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p def item_at_nat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do t.item_at <$> Dir.nat_to_dir_vec idx depth +def tree_item_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): F := + MerkleTree.item_at Tree (Dir.fin_to_dir_vec i).dropLast.reverse + -- Walk the tree using path Vector and return list of Hashes along the path def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Dir depth) : Vector F depth := match depth with | Nat.zero => Vector.nil @@ -172,6 +250,9 @@ def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : def proof_at_nat (t : MerkleTree F H depth) (idx: Nat): Option (Vector F depth) := t.proof <$> Dir.nat_to_dir_vec idx depth +def tree_proof_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): Vector F d := + MerkleTree.proof Tree (Dir.fin_to_dir_vec i).dropLast.reverse + -- Recover the Merkle tree from partial hashes. From bottom to top. It returns the item at the top (i.e. root) def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item diff --git a/lake-manifest.json b/lake-manifest.json index ad49671..a7b16c2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -16,9 +16,9 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "ea67efc21e4e1496f0a1d954cd0c0a952523133a", + "rev": "26d0eab43f05db777d1cf31abd31d3a57954b2a9", "name": "mathlib", - "inputRev?": "ea67efc21e4e1496f0a1d954cd0c0a952523133a"}}, + "inputRev?": "26d0eab43f05db777d1cf31abd31d3a57954b2a9"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 9ae629e..ac7ac19 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ package «proven-zk» { } require mathlib from git - "https://github.com/leanprover-community/mathlib4.git"@"ea67efc21e4e1496f0a1d954cd0c0a952523133a" + "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9" @[default_target] lean_lib «ProvenZk» { From b12b886978a8f433178b08e213788081bd880876 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Fri, 3 Nov 2023 15:46:46 +0000 Subject: [PATCH 06/18] New merkletree proof --- ProvenZk/Merkle.lean | 19 +++++++++++++++++++ ProvenZk/Misc.lean | 2 +- 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 593c606..bfc7566 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -528,4 +528,23 @@ theorem recover_equivalence . apply recover_proof_reversible (Item := Item) assumption +theorem eq_root_eq_tree {H} [ph: Fact (perfect_hash H)] {t₁ t₂ : MerkleTree α H d}: + t₁.root = t₂.root ↔ t₁ = t₂ := by + induction d with + | zero => cases t₁; cases t₂; tauto + | succ _ ih => + cases t₁ + cases t₂ + apply Iff.intro + . intro h + have h := Fact.elim ph h + injection h with h + injection h with _ h + injection h + congr <;> {rw [←ih]; assumption} + . intro h + injection h + subst_vars + rfl + end MerkleTree diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean index 870ec71..e206567 100644 --- a/ProvenZk/Misc.lean +++ b/ProvenZk/Misc.lean @@ -44,4 +44,4 @@ lemma select_rw [Fact (Nat.Prime N)] {b i1 i2 out : (ZMod N)} : (Gates.select b lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by simp - tauto \ No newline at end of file + tauto From 25ab09ae7d83ab6f34db1f8af289f1f738497dc9 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Fri, 3 Nov 2023 15:51:16 +0000 Subject: [PATCH 07/18] Removed unused comments --- ProvenZk/Merkle.lean | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index bfc7566..11606a2 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -230,7 +230,6 @@ def root {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) : F := | leaf f => f | bin l r => H vec![root l, root r] --- Walk the tree using path Vector and return leaf def item_at {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Dir depth) : F := match depth with | Nat.zero => match t with | leaf f => f @@ -242,7 +241,6 @@ def item_at_nat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) def tree_item_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): F := MerkleTree.item_at Tree (Dir.fin_to_dir_vec i).dropLast.reverse --- Walk the tree using path Vector and return list of Hashes along the path def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Dir depth) : Vector F depth := match depth with | Nat.zero => Vector.nil | Nat.succ _ => Vector.cons (t.tree_for p.head.swap).root ((t.tree_for p.head).proof p.tail) @@ -253,7 +251,6 @@ def proof_at_nat (t : MerkleTree F H depth) (idx: Nat): Option (Vector F depth) def tree_proof_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): Vector F d := MerkleTree.proof Tree (Dir.fin_to_dir_vec i).dropLast.reverse --- Recover the Merkle tree from partial hashes. From bottom to top. It returns the item at the top (i.e. root) def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item | Nat.succ _ => @@ -263,7 +260,6 @@ def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proo | Dir.left => H vec![recover', pitem] | Dir.right => H vec![pitem, recover'] --- Same proof and path imply same item theorem equal_recover_equal_tree {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item₁ : F) (item₂ : F) [Fact (perfect_hash H)] @@ -290,7 +286,6 @@ theorem equal_recover_equal_tree {depth : Nat} {F: Type} (H : Hash F 2) intro h rw [h] --- Recover the Merkle tree from partial hashes. From top to bottom. It returns the item at the bottom (i.e. leaf) def recover_tail {depth : Nat} {F: Type} (H: Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item | Nat.succ _ => @@ -318,7 +313,6 @@ lemma recover_tail_snoc lhs rw [recover_tail, Vector.head_snoc, Vector.head_snoc, Vector.tail_snoc, Vector.tail_snoc, ih] --- recover_tail on reverse Vectors is equal to recover theorem recover_tail_reverse_equals_recover {F depth} (H : Hash F 2) @@ -351,7 +345,6 @@ theorem recover_tail_equals_recover_reverse rw [recover_tail_reverse_equals_recover] simp --- recover on Merke Tree returns root theorem recover_proof_is_root {F depth} (H : Hash F 2) @@ -370,7 +363,6 @@ theorem recover_proof_is_root congr <;> simp [*, proof, tree_for, left, right, Dir.swap, item_at, ih] ) --- Set item in the tree at position ix def set { depth : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Dir depth) (item : F) : MerkleTree F H depth := match depth with | Nat.zero => leaf item | Nat.succ _ => match ix.head with @@ -409,7 +401,6 @@ theorem item_at_nat_invariant {H : Hash α 2} {tree tree': MerkleTree α H depth refine (neq ?_) apply Dir.nat_to_dir_vec_unique <;> assumption --- Check set function changes the tree theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Dir depth) (new : F) : (tree.set ix new).item_at ix = new := by induction depth with @@ -425,7 +416,6 @@ lemma set_implies_item_at { depth : Nat } {F: Type} {H : Hash F 2} {t₁ t₂ : rw [<-h] apply read_after_insert_sound --- Related to recover_proof_is_root theorem proof_ceritfies_item {depth : Nat} {F: Type} From a1e766abaf4dc33ed7714b2f025ad09f8308ad93 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Thu, 9 Nov 2023 17:51:21 +0000 Subject: [PATCH 08/18] Added theorems --- ProvenZk/Merkle.lean | 68 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 66 insertions(+), 2 deletions(-) diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 11606a2..e55f2c4 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -238,9 +238,12 @@ def item_at {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p def item_at_nat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do t.item_at <$> Dir.nat_to_dir_vec idx depth -def tree_item_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): F := +def tree_item_at_fin_dropLast {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): F := MerkleTree.item_at Tree (Dir.fin_to_dir_vec i).dropLast.reverse +def tree_item_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): F := + MerkleTree.item_at Tree (Dir.fin_to_dir_vec i).reverse + def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Dir depth) : Vector F depth := match depth with | Nat.zero => Vector.nil | Nat.succ _ => Vector.cons (t.tree_for p.head.swap).root ((t.tree_for p.head).proof p.tail) @@ -248,9 +251,12 @@ def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : def proof_at_nat (t : MerkleTree F H depth) (idx: Nat): Option (Vector F depth) := t.proof <$> Dir.nat_to_dir_vec idx depth -def tree_proof_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): Vector F d := +def tree_proof_at_fin_dropLast {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): Vector F d := MerkleTree.proof Tree (Dir.fin_to_dir_vec i).dropLast.reverse +def tree_proof_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): Vector F d := + MerkleTree.proof Tree (Dir.fin_to_dir_vec i).reverse + def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item | Nat.succ _ => @@ -372,6 +378,9 @@ def set { depth : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) ( def set_at_nat(t : MerkleTree F H depth) (idx: Nat) (newVal: F): Option (MerkleTree F H depth) := (t.set · newVal) <$> Dir.nat_to_dir_vec idx depth +def tree_set_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)) (Item : F): MerkleTree F H d := + MerkleTree.set Tree (Dir.fin_to_dir_vec i).reverse Item + theorem item_at_invariant { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix₁ ix₂ : Vector Dir depth} {item₁ : F} {neq : ix₁ ≠ ix₂}: item_at (set tree ix₁ item₁) ix₂ = item_at tree ix₂ := by induction depth with @@ -537,4 +546,59 @@ theorem eq_root_eq_tree {H} [ph: Fact (perfect_hash H)] {t₁ t₂ : MerkleTree subst_vars rfl +lemma proof_of_set_is_proof + {F d} + (H : Hash F 2) + [Fact (perfect_hash H)] + (Tree : MerkleTree F H d) + (ix : Vector Dir d) + (item : F): + (MerkleTree.proof (MerkleTree.set Tree ix item) ix) = MerkleTree.proof Tree ix := by + induction d with + | zero => + simp [MerkleTree.set, MerkleTree.proof] + | succ d ih => + cases Tree + simp [MerkleTree.set, MerkleTree.proof, MerkleTree.tree_for] + split + . rename_i hdir + have : Dir.swap (Dir.swap (Vector.head ix)) = Dir.right := by + rw [hdir] + simp [Dir.swap] + have : Vector.head ix = Dir.right := by + rw [<-this] + simp [Dir.swap] + cases ix.head + . simp + . simp + rw [this] + simp [MerkleTree.set, MerkleTree.left, MerkleTree.right] + simp [Vector.vector_eq_cons] + rw [ih] + . rename_i hdir + have : Dir.swap (Dir.swap (Vector.head ix)) = Dir.left := by + rw [hdir] + simp [Dir.swap] + have : Vector.head ix = Dir.left := by + rw [<-this] + simp [Dir.swap] + cases ix.head + . simp + . simp + rw [this] + simp [MerkleTree.set, MerkleTree.left, MerkleTree.right] + simp [Vector.vector_eq_cons] + rw [ih] + +lemma proof_of_set_fin + {F d} + (H : Hash F 2) + [Fact (perfect_hash H)] + (Tree : MerkleTree F H d) + (ix : Fin (2^d)) + (item : F): + (tree_proof_at_fin (tree_set_at_fin Tree ix item) ix) = tree_proof_at_fin Tree ix := by + simp [tree_proof_at_fin, tree_set_at_fin] + simp [proof_of_set_is_proof] + end MerkleTree From b2be7e092d3a195090cfe896dd0a8d66c40af39d Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Thu, 9 Nov 2023 23:25:49 +0000 Subject: [PATCH 09/18] New merkle tree theorems --- ProvenZk/Binary.lean | 18 ++++++++++++++++++ ProvenZk/Merkle.lean | 45 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 63 insertions(+) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 3b4f82e..11b4042 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -462,6 +462,24 @@ def fin_to_bits_le {d : Nat} (n : Fin (2 ^ d)): Vector Bit d := match h: nat_to_ simp [*] at h ) +lemma fin_to_bits_recover_binary {D n : Nat } [Fact (n > 1)] (Index : (ZMod n)) (ix_small : Index.val < 2^D) : + recover_binary_zmod' (Vector.map Bit.toZMod (fin_to_bits_le { val := ZMod.val Index, isLt := ix_small })) = Index := by + rw [recover_binary_of_to_bits] + simp [fin_to_bits_le] + split + . assumption + . contradiction + +lemma fin_to_bits_le_is_some {depth : Nat} {idx : Nat} (h : idx < 2 ^ depth) : + nat_to_bits_le depth idx = some (fin_to_bits_le idx) := by + simp [fin_to_bits_le] + split + . rename_i hnats + rw [Nat.mod_eq_of_lt] at hnats + . simp [hnats] + . simp [h] + . contradiction + theorem fin_to_bits_le_to_recover_binary_zmod' {n d : Nat} [Fact (n > 1)] {v : ZMod n} {w : Vector (ZMod n) d} {h : v.val < 2^d }: n > 2^d → is_vector_binary w → diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index e55f2c4..2f5fc37 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -257,6 +257,18 @@ def tree_proof_at_fin_dropLast {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) def tree_proof_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): Vector F d := MerkleTree.proof Tree (Dir.fin_to_dir_vec i).reverse +lemma proof_at_nat_to_fin {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): + MerkleTree.proof_at_nat t idx = some (MerkleTree.tree_proof_at_fin t idx) := by + simp [MerkleTree.proof_at_nat, MerkleTree.tree_proof_at_fin] + simp [Dir.nat_to_dir_vec, Dir.fin_to_dir_vec] + simp [fin_to_bits_le_is_some h] + +lemma proof_at_nat_to_fin_some {depth : Nat} {F: Type} {H: Hash F 2} {a : Vector F depth} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): + MerkleTree.proof_at_nat t idx = some a ↔ + MerkleTree.tree_proof_at_fin t idx = a := by + rw [proof_at_nat_to_fin (h := h)] + . simp + def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item | Nat.succ _ => @@ -381,6 +393,31 @@ def set_at_nat(t : MerkleTree F H depth) (idx: Nat) (newVal: F): Option (MerkleT def tree_set_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)) (Item : F): MerkleTree F H d := MerkleTree.set Tree (Dir.fin_to_dir_vec i).reverse Item +lemma set_at_nat_to_fin {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) (item : F) (h : idx < 2 ^ depth): + MerkleTree.set_at_nat t idx item = some (MerkleTree.tree_set_at_fin t idx item) := by + simp [MerkleTree.set_at_nat, MerkleTree.tree_set_at_fin] + simp [Dir.nat_to_dir_vec] + simp [Dir.fin_to_dir_vec] + simp [fin_to_bits_le_is_some h] + +lemma set_at_nat_to_fin_some {depth : Nat} {F: Type} {H: Hash F 2} {a : MerkleTree F H depth} (t : MerkleTree F H depth) (idx : Nat) (item : F) (h : idx < 2 ^ depth): + MerkleTree.set_at_nat t idx item = some a ↔ + MerkleTree.tree_set_at_fin t idx item = a := by + rw [set_at_nat_to_fin (h := h)] + . simp + +lemma item_at_nat_to_fin {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): + MerkleTree.item_at_nat t idx = some (MerkleTree.tree_item_at_fin t idx) := by + simp [MerkleTree.item_at_nat, MerkleTree.tree_item_at_fin] + simp [Dir.nat_to_dir_vec, Dir.fin_to_dir_vec] + simp [fin_to_bits_le_is_some h] + +lemma item_at_nat_to_fin_some {depth : Nat} {F: Type} {H: Hash F 2} {a : F} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): + MerkleTree.item_at_nat t idx = some a ↔ + MerkleTree.tree_item_at_fin t idx = a := by + rw [item_at_nat_to_fin (h := h)] + . simp + theorem item_at_invariant { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix₁ ix₂ : Vector Dir depth} {item₁ : F} {neq : ix₁ ≠ ix₂}: item_at (set tree ix₁ item₁) ix₂ = item_at tree ix₂ := by induction depth with @@ -410,6 +447,14 @@ theorem item_at_nat_invariant {H : Hash α 2} {tree tree': MerkleTree α H depth refine (neq ?_) apply Dir.nat_to_dir_vec_unique <;> assumption +theorem item_at_fin_invariant {H : Hash α 2} {tree tree': MerkleTree α H depth} { neq : ix₁ ≠ ix₂ } {h₁ : ix₁ < 2 ^ depth} {h₂ : ix₂ < 2 ^ depth}: + MerkleTree.tree_set_at_fin tree ix₁ item₁ = tree' → + MerkleTree.tree_item_at_fin tree' ix₂ = MerkleTree.tree_item_at_fin tree ix₂ := by + rw [<-set_at_nat_to_fin_some (h := h₁)] + rw [<-item_at_nat_to_fin_some (h := h₂)] + rw [<-item_at_nat_to_fin (h := h₂)] + apply MerkleTree.item_at_nat_invariant (neq := neq) + theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Dir depth) (new : F) : (tree.set ix new).item_at ix = new := by induction depth with From cb1288dfa2b80340cbf19ba1ab6a3eee26dc1533 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 00:43:13 +0000 Subject: [PATCH 10/18] New theorems --- ProvenZk/Ext/Vector/Basic.lean | 4 +++ ProvenZk/Merkle.lean | 62 ++++++++++++++++++++++++++++++++++ 2 files changed, 66 insertions(+) diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 9ce376e..d3b3b7f 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -192,4 +192,8 @@ lemma toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toLi lemma vector_list_vector {d} {x₁ x₂ : α} {xs : Vector α d} : (x₁ ::ᵥ x₂ ::ᵥ xs).dropLast = x₁ ::ᵥ (x₂ ::ᵥ xs).dropLast := by rfl +lemma cons_zero {d : Nat } {y : α} {v : Vector α d} : + (y ::ᵥ v)[0] = y := by + rfl + end Vector diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 2f5fc37..884f7fd 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -646,4 +646,66 @@ lemma proof_of_set_fin simp [tree_proof_at_fin, tree_set_at_fin] simp [proof_of_set_is_proof] +def multi_set { depth b : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (path : Vector (Vector Dir depth) b) (item : F) : MerkleTree F H depth := + match b with + | Nat.zero => tree + | Nat.succ _ => multi_set (tree.set path.head item) path.tail item + +lemma tree_set_comm { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p₁ p₂ : Vector Dir depth} {item : F}: + MerkleTree.set (MerkleTree.set tree p₁ item) p₂ item = MerkleTree.set (MerkleTree.set tree p₂ item) p₁ item := by + induction depth with + | zero => rfl + | succ d ih => cases tree with | bin l r => + cases p₁ using Vector.casesOn with | cons p₁h p₁t => + cases p₂ using Vector.casesOn with | cons p₂h p₂t => + cases p₁h <;> { + cases p₂h <;> { simp [MerkleTree.set, MerkleTree.left, MerkleTree.right]; try rw [ih] } + } + +lemma multi_set_set { depth b : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p : Vector Dir depth} {path : Vector (Vector Dir depth) b} {item : F}: + multi_set (MerkleTree.set tree p item) path item = MerkleTree.set (multi_set tree path item) p item := by + induction path using Vector.inductionOn generalizing tree p with + | h_nil => rfl + | h_cons ih => simp [multi_set, ih, tree_set_comm] + +def multi_item_at { depth b : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (path : Vector (Vector Dir depth) b) (item : F) : Prop := + match b with + | Nat.zero => true + | Nat.succ _ => tree.item_at path.head = item ∧ multi_item_at tree path.tail item + +theorem multi_set_is_item_at { depth b : Nat } {F: Type} {H : Hash F 2} {initialTree finalTree: MerkleTree F H depth} {path : Vector (Vector Dir depth) b} {item : F} : + (multi_set initialTree path item = finalTree → + multi_item_at finalTree path item) := by + induction path using Vector.inductionOn generalizing initialTree finalTree with + | h_nil => + simp [multi_set, multi_item_at] + | @h_cons b' x xs ih => + unfold multi_set + unfold multi_item_at + simp only [Vector.tail_cons, Vector.head_cons] + intro h + refine ⟨?_, ?_⟩ + . rw [←h, multi_set_set, MerkleTree.read_after_insert_sound] + . apply ih h + +theorem multi_set_is_item_at_all_item { depth b i : Nat } {range : i ∈ [0:b]} {F: Type} {H : Hash F 2} + {initialTree finalTree: MerkleTree F H depth} {path : Vector (Vector Dir depth) b} {item : F} : + multi_set initialTree path item = finalTree → + MerkleTree.item_at finalTree (path[i]'(by rcases range; tauto)) = item := by + intro hp + induction path using Vector.inductionOn generalizing i initialTree finalTree with + | h_nil => + rcases range with ⟨lo, hi⟩ + have := Nat.ne_of_lt (Nat.lt_of_le_of_lt lo hi) + contradiction + | @h_cons b' x xs ih => + rcases range with ⟨lo, hi⟩ + cases lo with + | refl => + have hitem_at : multi_item_at finalTree (x ::ᵥ xs) item := multi_set_is_item_at hp + unfold multi_item_at at hitem_at + tauto + | @step i h => + exact ih (by assumption) (range := ⟨zero_le _, Nat.lt_of_succ_lt_succ hi⟩) + end MerkleTree From c612b943c8431e69031dfd54a7256a3e8c5c2b92 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 01:46:56 +0000 Subject: [PATCH 11/18] Added keccak utils --- ProvenZk/Binary.lean | 84 +++++++++++++++++++++++++++ ProvenZk/Ext/Fin.lean | 26 +++++++++ ProvenZk/Ext/Vector/Basic.lean | 100 ++++++++++++++++++++++++++++++++- ProvenZk/Misc.lean | 40 ++++++++++++- ProvenZk/Subvector.lean | 61 ++++++++++++++++++++ 5 files changed, 306 insertions(+), 5 deletions(-) create mode 100644 ProvenZk/Ext/Fin.lean create mode 100644 ProvenZk/Subvector.lean diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 11b4042..f07e241 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -66,6 +66,16 @@ def zmod_to_bit {n} (x : ZMod n) : Bit := match ZMod.val x with @[reducible] def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1 +@[simp] +theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto + +@[simp] +theorem is_bit_one : is_bit (1 : ZMod n) := by tauto + +abbrev bOne : {v : ZMod n // is_bit v} := ⟨1, by simp⟩ + +abbrev bZero : {v : ZMod n // is_bit v} := ⟨0, by simp⟩ + def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop := (List.foldr (fun a r => is_bit a ∧ r) True (Vector.toList x)) @@ -516,3 +526,77 @@ lemma vector_bit_to_zmod_last {d n : Nat} [Fact (n > 1)] {xs : Vector Bit (d+1)} have hxs : vector_zmod_to_bit (Vector.map (fun i => @Bit.toZMod n i) xs) = xs := by simp [vector_bit_to_zmod_to_bit] rw [hx, hxs] + +@[elab_as_elim] +def bitCases' {n : Nat} {C : Subtype (α := ZMod n.succ.succ) is_bit → Sort _} (v : Subtype (α := ZMod n.succ.succ) is_bit) + (zero : C bZero) + (one : C bOne): C v := by + rcases v with ⟨v, h⟩ + rcases v with ⟨v, _⟩ + cases v with + | zero => exact zero + | succ v => cases v with + | zero => exact one + | succ v => + apply False.elim + rcases h with h | h <;> { + injection h with h + simp at h + } + +theorem isBitCases (b : Subtype (α := ZMod n) is_bit): b = bZero ∨ b = bOne := by + cases b with | mk _ prop => + cases prop <;> {subst_vars ; tauto } + + +def bitCases : { v : ZMod (Nat.succ (Nat.succ n)) // is_bit v} → Bit + | ⟨0, _⟩ => Bit.zero + | ⟨1, _⟩ => Bit.one + | ⟨⟨Nat.succ (Nat.succ i), _⟩, h⟩ => False.elim (by + cases h <;> { + rename_i h + injection h with h; + rw [Nat.mod_eq_of_lt] at h + . injection h; try (rename_i h; injection h) + . simp + } + ) + +@[simp] lemma ne_1_0 {n:Nat}: ¬(1 : ZMod (n.succ.succ)) = (0 : ZMod (n.succ.succ)) := by + intro h; + conv at h => lhs; whnf + conv at h => rhs; whnf + injection h with h + injection h + +@[simp] lemma ne_0_1 {n:Nat}: ¬(0 : ZMod (n.succ.succ)) = (1 : ZMod (n.succ.succ)) := by + intro h; + conv at h => lhs; whnf + conv at h => rhs; whnf + injection h with h + injection h + + +@[simp] +lemma bitCases_eq_0 : bitCases b = Bit.zero ↔ b = bZero := by + cases b with | mk val prop => + cases prop <;> { + subst_vars + conv => lhs; lhs; whnf + simp + } + +@[simp] +lemma bitCases_eq_1 : bitCases b = Bit.one ↔ b = bOne := by + cases b with | mk val prop => + cases prop <;> { + subst_vars + conv => lhs; lhs; whnf + simp + } + +@[simp] +lemma bitCases_bZero {n:Nat}: bitCases (@bZero (n + 2)) = Bit.zero := by rfl + +@[simp] +lemma bitCases_bOne {n:Nat}: bitCases (@bOne (n+2)) = Bit.one := by rfl diff --git a/ProvenZk/Ext/Fin.lean b/ProvenZk/Ext/Fin.lean new file mode 100644 index 0000000..920e8fc --- /dev/null +++ b/ProvenZk/Ext/Fin.lean @@ -0,0 +1,26 @@ +import Std.Data.Fin.Basic +import Std.Classes.Cast +import Mathlib.Data.Fin.Basic +import Mathlib.Tactic.Linarith.Frontend + +namespace Fin + +theorem castSucc_succ_eq_succ_castSucc : Fin.castSucc (Fin.succ i) = Fin.succ (Fin.castSucc i) := by + rfl + +theorem last_succ_eq_succ_last : Fin.last (Nat.succ n) = Fin.succ (Fin.last n) := by + rfl + +theorem last_def : Fin.mk (n := Nat.succ n) n (by simp) = Fin.last n := by + rfl + +theorem castSucc_def {i : Fin n} : + Fin.mk (n := Nat.succ n) (i.val) (by cases i; linarith) = i.castSucc := by + rfl + +theorem cast_last {n : Nat} : ↑n = Fin.last n := by + conv => lhs; whnf + conv => rhs; whnf + simp + +end Fin diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index d3b3b7f..09cbaa6 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -2,6 +2,7 @@ import Mathlib.Data.Vector.Snoc import Mathlib.Data.Matrix.Basic import Mathlib.Data.List.Defs +import ProvenZk.Ext.Fin import ProvenZk.Ext.Range import ProvenZk.Ext.List @@ -192,8 +193,101 @@ lemma toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toLi lemma vector_list_vector {d} {x₁ x₂ : α} {xs : Vector α d} : (x₁ ::ᵥ x₂ ::ᵥ xs).dropLast = x₁ ::ᵥ (x₂ ::ᵥ xs).dropLast := by rfl -lemma cons_zero {d : Nat } {y : α} {v : Vector α d} : - (y ::ᵥ v)[0] = y := by - rfl +@[simp] +theorem vector_get_zero {vs : Vector i n} : (v ::ᵥ vs)[0] = v := by rfl + +@[simp] +theorem vector_get_succ_fin {vs : Vector i n} {i : Fin n} : (v ::ᵥ vs)[i.succ] = vs[i] := by rfl + +@[simp] +theorem vector_get_succ_nat {vs : Vector i n} {i : Nat} {h : i.succ < n.succ } : (v ::ᵥ vs)[i.succ]'h = vs[i]'(by linarith) := by rfl + +@[simp] +theorem vector_get_snoc_last { vs : Vector α n }: + (vs.snoc v).get (Fin.last n) = v := by + induction n with + | zero => + cases vs using Vector.casesOn; rfl + | succ n ih => + cases vs using Vector.casesOn + rw [Fin.last_succ_eq_succ_last, Vector.snoc_cons, Vector.get_cons_succ, ih] + +@[simp] +lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = vs.get i := by + cases n + case zero => cases i using finZeroElim + case succ n => + induction n with + | zero => + cases i using Fin.cases with + | H0 => cases vs using Vector.casesOn with | cons hd tl => simp + | Hs i => cases i using finZeroElim + | succ n ih => + cases vs using Vector.casesOn with | cons hd tl => + cases i using Fin.cases with + | H0 => simp + | Hs i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih] + +theorem vector_get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by + rfl + +theorem getElem_def {v : Vector α n} {i : Nat} {prop}: v[i]'prop = v.get ⟨i, prop⟩ := by + rfl + +@[simp] +lemma vector_get_snoc_fin_prev {vs : Vector α n} {v : α} {i : Fin n}: + (vs.snoc v)[i.val]'(by (have := i.prop); linarith) = vs[i.val]'(i.prop) := by + simp [vector_get_val_getElem, getElem_def, Fin.castSucc_def] + +theorem ofFn_snoc' { fn : Fin (Nat.succ n) → α }: + Vector.ofFn fn = Vector.snoc (Vector.ofFn (fun (x : Fin n) => fn (Fin.castSucc x))) (fn n) := by + induction n with + | zero => rfl + | succ n ih => + conv => lhs; rw [Vector.ofFn, ih] + simp [Vector.ofFn] + congr + simp [Fin.succ] + congr + simp [Nat.mod_eq_of_lt] + +def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i] + +@[simp] +theorem allIxes_cons : allIxes f (v ::ᵥ vs) ↔ f v ∧ allIxes f vs := by + simp [allIxes, GetElem.getElem] + apply Iff.intro + . intro h + exact ⟨h 0, fun i => h i.succ⟩ + . intro h i + cases i using Fin.cases + . simp [h.1] + . simp [h.2] + +@[simp] +theorem allIxes_nil : allIxes f Vector.nil := by + simp [allIxes] + +theorem getElem_allIxes {v : { v: Vector α n // allIxes prop v }} {i : Nat} { i_small : i < n}: + v.val[i]'i_small = ↑(Subtype.mk (v.val.get ⟨i, i_small⟩) (v.prop ⟨i, i_small⟩)) := by rfl + +theorem getElem_allIxes₂ {v : { v: Vector (Vector α m) n // allIxes (allIxes prop) v }} {i j: Nat} { i_small : i < n} { j_small : j < m}: + (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (v.prop ⟨i, i_small⟩ ⟨j, j_small⟩)) := by rfl + +theorem allIxes_indexed {v : {v : Vector α n // allIxes prop v}} {i : Nat} {i_small : i < n}: + prop (v.val[i]'i_small) := v.prop ⟨i, i_small⟩ + +theorem allIxes_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes prop) v}} + {i : Nat} {i_small : i < c} + {j : Nat} {j_small : j < b}: + prop ((v.val[i]'i_small)[j]'j_small) := + v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ + +theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes (allIxes prop)) v}} + {i : Nat} {i_small : i < c} + {j : Nat} {j_small : j < b} + {k : Nat} {k_small : k < a}: + prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) := + v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ ⟨k, k_small⟩ end Vector diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean index e206567..edee748 100644 --- a/ProvenZk/Misc.lean +++ b/ProvenZk/Misc.lean @@ -1,6 +1,10 @@ import ProvenZk.Gates +import ProvenZk.Binary -theorem or_rw [Fact (Nat.Prime N)] (a b out : (ZMod N)) : Gates.or a b out ↔ +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 ∧ ( (out = 1 ∧ (a = 1 ∨ b = 1) ∨ (out = 0 ∧ a = 0 ∧ b = 0)))) := by @@ -10,7 +14,7 @@ theorem or_rw [Fact (Nat.Prime N)] (a b out : (ZMod N)) : Gates.or a b out ↔ intro ha hb cases ha <;> cases hb <;> { subst_vars; simp } -lemma select_rw [Fact (Nat.Prime N)] {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)} : (Gates.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with | Bit.zero => out = i2 | Bit.one => out = i1 := by unfold Gates.select @@ -42,6 +46,38 @@ lemma select_rw [Fact (Nat.Prime N)] {b i1 i2 out : (ZMod N)} : (Gates.select b } } +@[simp] +theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by rfl + +@[simp] +theorem select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by + simp [Gates.select] + +@[simp] +theorem select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by + simp [Gates.select] + +@[simp] +theorem or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by + simp [Gates.or] + +@[simp] +theorem zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by + simp [Gates.or] + +@[simp] +theorem one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by + simp [Gates.or] + +@[simp] +theorem or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by + simp [Gates.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] + tauto + lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by simp tauto diff --git a/ProvenZk/Subvector.lean b/ProvenZk/Subvector.lean new file mode 100644 index 0000000..522f59d --- /dev/null +++ b/ProvenZk/Subvector.lean @@ -0,0 +1,61 @@ +import ProvenZk.Ext.Vector + +abbrev SubVector α n prop := Subtype (α := Vector α n) (Vector.allIxes prop) + +namespace SubVector + +def nil : SubVector α 0 prop := ⟨Vector.nil, by simp⟩ + +def snoc (vs: SubVector α n prop) (v : Subtype prop): SubVector α n.succ prop := + ⟨vs.val.snoc v.val, by + intro i + cases i using Fin.lastCases with + | hlast => simp [GetElem.getElem, Fin.last_def, Subtype.property] + | hcast i => + have := vs.prop i + simp at this + simp [*] + ⟩ + +@[elab_as_elim] +def revCases {C : ∀ {n:Nat}, SubVector α n prop → Sort _} (v : SubVector α n prop) + (nil : C nil) + (snoc : ∀ {n : Nat} (vs : SubVector α n prop) (v : Subtype prop), C (vs.snoc v)): C v := by + rcases v with ⟨v, h⟩ + cases v using Vector.revCasesOn with + | nil => exact nil + | snoc vs v => + refine snoc ⟨vs, ?vsp⟩ ⟨v, ?vp⟩ + case vsp => + intro i + have := h i.castSucc + simp at this + simp [this] + case vp => + have := h (Fin.last _) + simp [GetElem.getElem, Fin.last_def] at this + exact this + +instance : GetElem (SubVector α n prop) (Fin n) (Subtype prop) (fun _ _ => True) where + getElem v i _ := ⟨v.val.get i, v.prop i⟩ + +def lower (v: SubVector α n prop): Vector {v : α // prop v} n := + Vector.ofFn fun i => v[i] + +def lift {prop : α → Prop} (v : Vector (Subtype prop) n): SubVector α n prop := + ⟨v.map Subtype.val, by + intro i + simp [GetElem.getElem, Subtype.property]⟩ + +theorem snoc_lower {vs : SubVector α n prop} {v : Subtype prop}: + (vs.snoc v).lower = vs.lower.snoc v := by + unfold lower + rw [Vector.ofFn_snoc'] + congr + . funext i + cases n with + | zero => cases i using finZeroElim + | _ => simp [GetElem.getElem, snoc] + . simp [GetElem.getElem, snoc, Fin.cast_last] + +end SubVector From c47129dc435e49a1fda01408ec1b615bd7384b48 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 01:48:20 +0000 Subject: [PATCH 12/18] Added import --- ProvenZk.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ProvenZk.lean b/ProvenZk.lean index 974901a..74549f9 100644 --- a/ProvenZk.lean +++ b/ProvenZk.lean @@ -6,3 +6,5 @@ import ProvenZk.Ext.Vector import ProvenZk.Ext.Range import ProvenZk.Ext.Matrix import ProvenZk.Ext.List +import ProvenZk.Ext.Fin +import ProvenZk.Subvector From 87915b495463baaffaf9675a9daebf40753ff83d Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 02:05:34 +0000 Subject: [PATCH 13/18] Added bit theorems --- ProvenZk/Binary.lean | 48 ++++++++++++++++++++++++++++++++++ ProvenZk/Ext/Vector/Basic.lean | 12 +++++++++ ProvenZk/Misc.lean | 13 +++++++++ 3 files changed, 73 insertions(+) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index f07e241..068eaef 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -3,6 +3,7 @@ import Mathlib.Data.Bitvec.Defs import ProvenZk.Ext.List import ProvenZk.Ext.Vector +import ProvenZk.Subvector inductive Bit : Type where | zero : Bit @@ -76,6 +77,10 @@ abbrev bOne : {v : ZMod n // is_bit v} := ⟨1, by simp⟩ abbrev bZero : {v : ZMod n // is_bit v} := ⟨0, by simp⟩ +def embedBit {n : Nat} : Bit → {x : (ZMod n) // is_bit x} +| Bit.zero => bZero +| Bit.one => bOne + def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop := (List.foldr (fun a r => is_bit a ∧ r) True (Vector.toList x)) @@ -600,3 +605,46 @@ lemma bitCases_bZero {n:Nat}: bitCases (@bZero (n + 2)) = Bit.zero := by rfl @[simp] lemma bitCases_bOne {n:Nat}: bitCases (@bOne (n+2)) = Bit.one := by rfl + +theorem is_vector_binary_iff_allIxes_is_bit {n : Nat} {v : Vector (ZMod n) d}: Vector.allIxes is_bit v ↔ is_vector_binary v := by + induction v using Vector.inductionOn with + | h_nil => simp [is_vector_binary] + | h_cons ih => conv => lhs; simp [ih] + +theorem fin_to_bits_le_recover_binary_nat {v : Vector Bit d}: + fin_to_bits_le ⟨recover_binary_nat v, binary_nat_lt _⟩ = v := by + unfold fin_to_bits_le + split + . rename_i h + rw [←recover_binary_nat_to_bits_le] at h + exact binary_nat_unique _ _ h + . contradiction + +theorem SubVector_map_cast_lower {v : SubVector α n prop} {f : α → β }: + (v.val.map f) = v.lower.map fun (x : Subtype prop) => f x.val := by + rw [←Vector.ofFn_get v.val] + simp only [SubVector.lower, GetElem.getElem, Vector.map_ofFn] + +@[simp] +theorem recover_binary_nat_fin_to_bits_le {v : Fin (2^d)}: + recover_binary_nat (fin_to_bits_le v) = v.val := by + unfold fin_to_bits_le + split + . rename_i h + rw [←recover_binary_nat_to_bits_le] at h + assumption + . contradiction + +@[simp] +theorem SubVector_lower_lift : SubVector.lift (SubVector.lower v) = v := by + unfold SubVector.lift + unfold SubVector.lower + apply Subtype.eq + simp [GetElem.getElem] + +@[simp] +theorem SubVector_lift_lower : SubVector.lower (SubVector.lift v) = v := by + unfold SubVector.lift + unfold SubVector.lower + apply Subtype.eq + simp [GetElem.getElem] diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 09cbaa6..440d511 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -290,4 +290,16 @@ theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxe prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) := v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ ⟨k, k_small⟩ +@[simp] +theorem map_ofFn {f : α → β} (g : Fin n → α) : + Vector.map f (Vector.ofFn g) = Vector.ofFn (fun x => f (g x)) := by + apply Vector.eq + simp + rfl + +@[simp] +theorem map_id': Vector.map (fun x => x) v = v := by + have : ∀α, (fun (x:α) => x) = id := by intro _; funext _; rfl + rw [this, Vector.map_id] + end Vector diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean index edee748..52eea7f 100644 --- a/ProvenZk/Misc.lean +++ b/ProvenZk/Misc.lean @@ -81,3 +81,16 @@ theorem is_bit_one_sub {a : ZMod N}: is_bit (Gates.sub 1 a) ↔ is_bit a := by lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by simp tauto + +lemma and_iff (P Q R : Prop): (Q ↔ R) → (P ∧ Q ↔ P ∧ R) := by + tauto + +lemma ex_iff {P Q : α → Prop}: (∀x, P x ↔ Q x) → ((∃x, P x) ↔ ∃x, Q x) := by + intro h; + apply Iff.intro <;> { + intro h1 + cases h1; rename_i witness prop + exists witness + try { rw [h witness]; assumption } + try { rw [←h witness]; assumption } + } From 89c96ee15da7d7a4e1f6c5946e0429fcce1f6976 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 02:46:47 +0000 Subject: [PATCH 14/18] Fixed imports --- ProvenZk.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/ProvenZk.lean b/ProvenZk.lean index 74549f9..ac31cd2 100644 --- a/ProvenZk.lean +++ b/ProvenZk.lean @@ -8,3 +8,4 @@ import ProvenZk.Ext.Matrix import ProvenZk.Ext.List import ProvenZk.Ext.Fin import ProvenZk.Subvector +import ProvenZk.Misc From 67ed8a5df2c5ddbf6cdaf0a4ba3f67d3340575c8 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 03:17:12 +0000 Subject: [PATCH 15/18] Updated vector --- ProvenZk/Ext/Vector/Basic.lean | 86 ++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 440d511..e5f66a9 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -302,4 +302,90 @@ theorem map_id': Vector.map (fun x => x) v = v := by have : ∀α, (fun (x:α) => x) = id := by intro _; funext _; rfl rw [this, Vector.map_id] +def ofFnGet (v : Vector F d) : Vector F d := Vector.ofFn fun i => v[i.val]'i.prop +instance : HAppend (Vector α d₁) (Vector α d₂) (Vector α (d₁ + d₂)) := ⟨Vector.append⟩ + +@[simp] +theorem ofFnGet_id : ofFnGet v = v := by simp [ofFnGet, GetElem.getElem] + +@[simp] +theorem Vector.hAppend_toList {v₁ : Vector α d₁} {v₂ : Vector α d₂}: + (v₁ ++ v₂).toList = v₁.toList ++ v₂.toList := by rfl + +theorem Vector.append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: + v₁ ++ v₂ = w₁ ++ w₂ → v₁ = w₁ ∧ v₂ = w₂ := by + intro h + induction v₁, w₁ using Vector.inductionOn₂ with + | nil => + apply And.intro rfl + apply Vector.eq + have := congrArg toList h + simp at this + assumption + | cons ih => + have := congrArg toList h + simp at this + rcases this with ⟨h₁, h₂⟩ + rw [←hAppend_toList, ←hAppend_toList] at h₂ + have := Vector.eq _ _ h₂ + have := ih this + cases this + subst_vars + apply And.intro <;> rfl + +theorem allIxes_toList : Vector.allIxes prop v ↔ ∀ i, prop (v.toList.get i) := by + unfold Vector.allIxes + apply Iff.intro + . intro h i + rcases i with ⟨i, p⟩ + simp at p + simp [GetElem.getElem, Vector.get] at h + have := h ⟨i, p⟩ + conv at this => arg 1; whnf + exact this + . intro h i + simp [GetElem.getElem, Vector.get] + rcases i with ⟨i, p⟩ + have := h ⟨i, by simpa⟩ + conv at this => arg 1; whnf + exact this + +theorem allIxes_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allIxes prop (v₁ ++ v₂) ↔ Vector.allIxes prop v₁ ∧ Vector.allIxes prop v₂ := by + simp [allIxes_toList] + apply Iff.intro + . intro h + apply And.intro + . intro i + rcases i with ⟨i, hp⟩ + simp at hp + rw [←List.get_append] + exact h ⟨i, (by simp; apply Nat.lt_add_right; assumption)⟩ + . intro i + rcases i with ⟨i, hp⟩ + simp at hp + have := h ⟨n₁ + i, (by simpa)⟩ + rw [List.get_append_right] at this + simp at this + exact this + . simp + . simpa + . intro ⟨l, r⟩ + intro ⟨i, hi⟩ + simp at hi + cases lt_or_ge i n₁ with + | inl hp => + rw [List.get_append _ (by simpa)] + exact l ⟨i, (by simpa)⟩ + | inr hp => + rw [List.get_append_right] + have := r ⟨i - n₁, (by simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption )⟩ + simp at this + simpa + . simp; exact LE.le.ge hp + . simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption + +theorem SubVector_append {v₁ : Vector α d₁} {prop₁ : Vector.allIxes prop v₁ } {v₂ : Vector α d₂} {prop₂ : Vector.allIxes prop v₂}: + (Subtype.mk v₁ prop₁).val ++ (Subtype.mk v₂ prop₂).val = + (Subtype.mk (v₁ ++ v₂) (allIxes_append.mpr ⟨prop₁, prop₂⟩)).val := by eq_refl + end Vector From 9fc2a8d51ff79d2efa64a72d997686e3726aa91c Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Wed, 15 Nov 2023 03:26:57 +0000 Subject: [PATCH 16/18] Fixed names --- ProvenZk/Ext/Vector/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index e5f66a9..71a9022 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -309,10 +309,10 @@ instance : HAppend (Vector α d₁) (Vector α d₂) (Vector α (d₁ + d₂)) : theorem ofFnGet_id : ofFnGet v = v := by simp [ofFnGet, GetElem.getElem] @[simp] -theorem Vector.hAppend_toList {v₁ : Vector α d₁} {v₂ : Vector α d₂}: +theorem hAppend_toList {v₁ : Vector α d₁} {v₂ : Vector α d₂}: (v₁ ++ v₂).toList = v₁.toList ++ v₂.toList := by rfl -theorem Vector.append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: +theorem append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: v₁ ++ v₂ = w₁ ++ w₂ → v₁ = w₁ ∧ v₂ = w₂ := by intro h induction v₁, w₁ using Vector.inductionOn₂ with From 80c7e686c5ff7580b3e0340b5cbba4c3a6e7fee6 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Fri, 17 Nov 2023 20:26:45 +0000 Subject: [PATCH 17/18] Updated to lean 4.2.0 --- .gitignore | 1 + ProvenZk/Binary.lean | 3 +- ProvenZk/Ext/Fin.lean | 2 +- ProvenZk/Ext/List.lean | 5 ++- ProvenZk/Ext/Vector/Basic.lean | 15 +++++--- ProvenZk/Ext/Vector/SetLoop.lean | 3 +- ProvenZk/Gates.lean | 2 +- ProvenZk/Subvector.lean | 6 ++-- lake-manifest.json | 61 +++++++++++++++++++------------- lakefile.lean | 2 +- lean-toolchain | 2 +- 11 files changed, 61 insertions(+), 41 deletions(-) diff --git a/.gitignore b/.gitignore index 40da894..74b281e 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /build /lake-packages/* /.cache +*.olean \ No newline at end of file diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 068eaef..bd1874a 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.ZMod.Defs import Mathlib.Data.ZMod.Basic import Mathlib.Data.Bitvec.Defs @@ -412,7 +413,6 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : apply absurd this simp | succ => - simp rfl } @@ -507,7 +507,6 @@ theorem fin_to_bits_le_to_recover_binary_zmod' {n d : Nat} [Fact (n > 1)] {v : Z linarith assumption assumption - simp [recover_binary_nat_to_bits_le] simp [fin_to_bits_le] split rename_i h diff --git a/ProvenZk/Ext/Fin.lean b/ProvenZk/Ext/Fin.lean index 920e8fc..7239d64 100644 --- a/ProvenZk/Ext/Fin.lean +++ b/ProvenZk/Ext/Fin.lean @@ -18,7 +18,7 @@ theorem castSucc_def {i : Fin n} : Fin.mk (n := Nat.succ n) (i.val) (by cases i; linarith) = i.castSucc := by rfl -theorem cast_last {n : Nat} : ↑n = Fin.last n := by +theorem nat_cast_last {n : Nat} : ↑n = Fin.last n := by conv => lhs; whnf conv => rhs; whnf simp diff --git a/ProvenZk/Ext/List.lean b/ProvenZk/Ext/List.lean index 3081c20..cc5b9f6 100644 --- a/ProvenZk/Ext/List.lean +++ b/ProvenZk/Ext/List.lean @@ -1,3 +1,6 @@ +-- import Mathlib.Data.List.Basic +-- import Mathlib.Data.List.Indexes +import Std.Data.List.Basic import Mathlib.Data.List.Basic import Mathlib.Data.List.Indexes @@ -39,4 +42,4 @@ theorem dropLast_cons {head₁ head₂ : α} {tail : List α} : List.dropLast (h | nil => simp | cons _ _ _ => simp [List.dropLast] -end List \ No newline at end of file +end List diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 71a9022..2d50776 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -1,6 +1,11 @@ +--import Mathlib.Data.Vector.Snoc +--import Mathlib.Data.Matrix.Basic +--import Mathlib.Data.List.Defs +import Mathlib.Data.Vector +import Mathlib.Data.Vector.Basic import Mathlib.Data.Vector.Snoc import Mathlib.Data.Matrix.Basic -import Mathlib.Data.List.Defs +import Std.Data.Fin.Lemmas import ProvenZk.Ext.Fin import ProvenZk.Ext.Range @@ -220,13 +225,13 @@ lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = v induction n with | zero => cases i using Fin.cases with - | H0 => cases vs using Vector.casesOn with | cons hd tl => simp - | Hs i => cases i using finZeroElim + | zero => cases vs using Vector.casesOn with | cons hd tl => simp + | succ i => cases i using finZeroElim | succ n ih => cases vs using Vector.casesOn with | cons hd tl => cases i using Fin.cases with - | H0 => simp - | Hs i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih] + | zero => simp + | succ i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih] theorem vector_get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by rfl diff --git a/ProvenZk/Ext/Vector/SetLoop.lean b/ProvenZk/Ext/Vector/SetLoop.lean index a4084de..fea130c 100644 --- a/ProvenZk/Ext/Vector/SetLoop.lean +++ b/ProvenZk/Ext/Vector/SetLoop.lean @@ -1,6 +1,5 @@ import ProvenZk.Ext.Vector.Basic - namespace Vector private lemma set_at_len (l1 l2 : List α) (it new : α): @@ -133,4 +132,4 @@ theorem setLoop_mapIdx {v : Vector α n} {f : ℕ -> α -> α }: apply Vector.eq simp [listMapIdx_setLoop, toList_setLoop] -end Vector \ No newline at end of file +end Vector diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean index c1181a6..7e03076 100644 --- a/ProvenZk/Gates.lean +++ b/ProvenZk/Gates.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.ZMod.Basic +import Mathlib.Data.ZMod.Defs import ProvenZk.Binary diff --git a/ProvenZk/Subvector.lean b/ProvenZk/Subvector.lean index 522f59d..dbe73b4 100644 --- a/ProvenZk/Subvector.lean +++ b/ProvenZk/Subvector.lean @@ -10,8 +10,8 @@ def snoc (vs: SubVector α n prop) (v : Subtype prop): SubVector α n.succ prop ⟨vs.val.snoc v.val, by intro i cases i using Fin.lastCases with - | hlast => simp [GetElem.getElem, Fin.last_def, Subtype.property] - | hcast i => + | last => simp [GetElem.getElem, Fin.last_def, Subtype.property] + | cast i => have := vs.prop i simp at this simp [*] @@ -56,6 +56,6 @@ theorem snoc_lower {vs : SubVector α n prop} {v : Subtype prop}: cases n with | zero => cases i using finZeroElim | _ => simp [GetElem.getElem, snoc] - . simp [GetElem.getElem, snoc, Fin.cast_last] + . simp [GetElem.getElem, snoc, Fin.nat_cast_last] end SubVector diff --git a/lake-manifest.json b/lake-manifest.json index a7b16c2..4b7cb34 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,39 +1,52 @@ -{"version": 4, +{"version": 6, "packagesDir": "lake-packages", "packages": [{"git": - {"url": "https://github.com/EdAyers/ProofWidgets4", - "subDir?": null, - "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8", - "name": "proofwidgets", - "inputRev?": "v0.0.11"}}, - {"git": - {"url": "https://github.com/mhuisi/lean4-cli.git", - "subDir?": null, - "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e", - "name": "Cli", - "inputRev?": "nightly"}}, - {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "26d0eab43f05db777d1cf31abd31d3a57954b2a9", + "rev": "753159252c585df6b6aa7c48d2b8828d58388b79", + "opts": {}, "name": "mathlib", - "inputRev?": "26d0eab43f05db777d1cf31abd31d3a57954b2a9"}}, + "inputRev?": "v4.2.0", + "inherited": false}}, {"git": - {"url": "https://github.com/gebner/quote4", + {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, - "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55", + "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", + "opts": {}, "name": "Qq", - "inputRev?": "master"}}, + "inputRev?": "master", + "inherited": true}}, {"git": - {"url": "https://github.com/JLimperg/aesop", + {"url": "https://github.com/leanprover/lean4-cli", "subDir?": null, - "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee", - "name": "aesop", - "inputRev?": "master"}}, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "opts": {}, + "name": "Cli", + "inputRev?": "nightly", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "subDir?": null, + "rev": "f1a5c7808b001305ba07d8626f45ee054282f589", + "opts": {}, + "name": "proofwidgets", + "inputRev?": "v0.0.21", + "inherited": true}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb", + "rev": "6747f41f28627bed83e6d5891683538211caa2c1", + "opts": {}, "name": "std", - "inputRev?": "main"}}]} + "inputRev?": "main", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover-community/aesop", + "subDir?": null, + "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7", + "opts": {}, + "name": "aesop", + "inputRev?": "master", + "inherited": true}}], + "name": "«proven-zk»"} diff --git a/lakefile.lean b/lakefile.lean index ac7ac19..b641c26 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ package «proven-zk» { } require mathlib from git - "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9" + "https://github.com/leanprover-community/mathlib4.git"@"v4.2.0" @[default_target] lean_lib «ProvenZk» { diff --git a/lean-toolchain b/lean-toolchain index 7e1c30c..2f868c6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-07-12 +leanprover/lean4:v4.2.0 From 30434f582d6b44a7f6b21fd4043eddb5b1605b20 Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Thu, 29 Feb 2024 22:24:42 +0000 Subject: [PATCH 18/18] Updated for merge --- ProvenZk.lean | 5 +- ProvenZk/Binary.lean | 824 +++++++++---------------------- ProvenZk/Ext/GetElem.lean | 52 ++ ProvenZk/Ext/List.lean | 5 +- ProvenZk/Ext/Vector/Basic.lean | 227 +++++---- ProvenZk/Ext/Vector/SetLoop.lean | 3 +- ProvenZk/Gates.lean | 13 +- ProvenZk/Hash.lean | 10 +- ProvenZk/Lemmas.lean | 175 +++++++ ProvenZk/Merkle.lean | 722 ++++----------------------- ProvenZk/Misc.lean | 96 ---- ProvenZk/Subvector.lean | 61 --- ProvenZk/UniqueAssignment.lean | 18 + 13 files changed, 698 insertions(+), 1513 deletions(-) create mode 100644 ProvenZk/Ext/GetElem.lean create mode 100644 ProvenZk/Lemmas.lean delete mode 100644 ProvenZk/Misc.lean delete mode 100644 ProvenZk/Subvector.lean create mode 100644 ProvenZk/UniqueAssignment.lean diff --git a/ProvenZk.lean b/ProvenZk.lean index ac31cd2..64dad76 100644 --- a/ProvenZk.lean +++ b/ProvenZk.lean @@ -2,10 +2,11 @@ import ProvenZk.Binary import ProvenZk.Gates import ProvenZk.Hash import ProvenZk.Merkle +import ProvenZk.Ext.GetElem import ProvenZk.Ext.Vector import ProvenZk.Ext.Range import ProvenZk.Ext.Matrix import ProvenZk.Ext.List import ProvenZk.Ext.Fin -import ProvenZk.Subvector -import ProvenZk.Misc +import ProvenZk.Lemmas +import ProvenZk.UniqueAssignment diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index bd1874a..f267cef 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -1,69 +1,13 @@ -import Mathlib.Data.ZMod.Defs import Mathlib.Data.ZMod.Basic import Mathlib.Data.Bitvec.Defs +import Mathlib.Data.Vector.Mem +import Mathlib.Data.Vector.MapLemmas +import Mathlib import ProvenZk.Ext.List import ProvenZk.Ext.Vector -import ProvenZk.Subvector - -inductive Bit : Type where - | zero : Bit - | one : Bit - deriving Repr, BEq - -namespace Bit -def toNat : Bit -> Nat := fun b => match b with - | Bit.zero => 0 - | Bit.one => 1 - -def toZMod {n} : Bit -> ZMod n := fun b => match b with - | Bit.zero => 0 - | Bit.one => 1 - -instance : Coe Bit Nat where - coe := toNat - -instance {n} : Coe Bit (ZMod n) where - coe := toZMod - -instance : OfNat Bit 0 where - ofNat := zero - -instance : OfNat Bit 1 where - ofNat := one - -instance : Inhabited Bit where - default := zero - -end Bit - -def bit_mod_two (inp : Nat) : Bit := match h:inp%2 with - | 0 => Bit.zero - | 1 => Bit.one - | 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 (l : Nat): Nat → Option (Vector Bit l) := match l with - | 0 => fun i => if i = 0 then some Vector.nil else none - | Nat.succ l => fun i => do - let x := i / 2 - let y := bit_mod_two i - let xs ← nat_to_bits_le l x - some (y ::ᵥ xs) - -def nat_to_bit (x : Nat) : Bit := match x with - | 0 => Bit.zero - | 1 => Bit.one - | Nat.succ (Nat.succ _) => panic "Bit can only be 0 or 1" - -def zmod_to_bit {n} (x : ZMod n) : Bit := match ZMod.val x with - | 0 => Bit.zero - | 1 => Bit.one - | Nat.succ (Nat.succ _) => panic "Bit can only be 0 or 1" + +open BigOperators @[reducible] def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1 @@ -74,576 +18,274 @@ theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto @[simp] theorem is_bit_one : is_bit (1 : ZMod n) := by tauto -abbrev bOne : {v : ZMod n // is_bit v} := ⟨1, by simp⟩ +def Bool.toZMod {N} (b : Bool) : ZMod N := b.toNat + +def Bool.ofZMod {N} (b : ZMod N) : Bool := Bool.ofNat b.val + +@[simp] +lemma Bool.toZMod_zero {N} : Bool.toZMod false = (0 : ZMod N) := by + simp [Bool.toZMod, Bool.toNat] + +@[simp] +lemma Bool.toZMod_one {N} : Bool.toZMod true = (1 : ZMod N) := by + simp [Bool.toZMod, Bool.toNat] + +@[simp] +lemma Bool.toZMod_is_bit {N} : is_bit (toZMod (N:=N) b) := by + cases b <;> simp [is_bit, toZMod, toNat] -abbrev bZero : {v : ZMod n // is_bit v} := ⟨0, by simp⟩ -def embedBit {n : Nat} : Bit → {x : (ZMod n) // is_bit x} -| Bit.zero => bZero -| Bit.one => bOne +@[simp] +theorem Bool.toZMod_eq_one_iff_eq_true {n:ℕ} [Fact (n > 1)] : (Bool.toZMod a : ZMod n) = 1 ↔ a = true := by + cases a <;> simp + +@[simp] +theorem Bool.toZMod_eq_one_iff_eq_false {n:ℕ} [Fact (n > 1)] : (Bool.toZMod a : ZMod n) = 0 ↔ a = false := by + cases a <;> simp + +@[simp] +lemma Bool.ofZMod_toZMod_eq_self {b} [Fact (N > 1)]: Bool.ofZMod (Bool.toZMod (N:=N) b) = b := by + cases b <;> simp [toZMod, ofZMod, ofNat, toNat] + +@[simp] +lemma Bool.toZMod_ofZMod_eq_self_of_is_bit {N} [Fact (N > 1)] {i : ZMod N} (h : is_bit i): + Bool.toZMod (Bool.ofZMod i) = i := by + cases h <;> {simp [*, ofZMod, toZMod, ofNat, toNat]} -def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop := - (List.foldr (fun a r => is_bit a ∧ r) True (Vector.toList x)) +def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop := ∀ a ∈ x, is_bit a @[simp] lemma is_vector_binary_reverse {depth} (ix : Vector (ZMod n) depth): is_vector_binary ix.reverse ↔ is_vector_binary ix := by - simp only [is_vector_binary, Vector.toList_reverse] - rw [List.foldr_reverse_assoc] - { simp } - { intros; simp; tauto } + simp [is_vector_binary ,Vector.toList_reverse] theorem is_vector_binary_cons {a : ZMod n} {vec : Vector (ZMod n) d}: is_vector_binary (a ::ᵥ vec) ↔ is_bit a ∧ is_vector_binary vec := by - unfold is_vector_binary - conv => lhs; unfold List.foldr; simp - -theorem is_vector_binary_dropLast {d n : Nat} {gate_0 : Vector (ZMod n) d} : - is_vector_binary gate_0 → is_vector_binary (Vector.dropLast gate_0) := by - simp [is_vector_binary, Vector.toList_dropLast] - intro h - induction gate_0 using Vector.inductionOn with - | h_nil => simp [List.dropLast] - | h_cons ih => - rename_i x xs - cases xs using Vector.casesOn - simp - rw [Vector.toList_cons, Vector.toList_cons, List.dropLast_cons] - simp [h] - cases h - tauto - -lemma dropLast_symm {n} {xs : Vector Bit d} : - Vector.map (fun i => @Bit.toZMod n i) (Vector.dropLast xs) = (Vector.map (fun i => @Bit.toZMod n i) xs).dropLast := by - induction xs using Vector.inductionOn with - | h_nil => - simp [Vector.dropLast, Vector.map] - | h_cons ih₁ => - rename_i x₁ xs - induction xs using Vector.inductionOn with - | h_nil => - simp [Vector.dropLast, Vector.map] - | h_cons _ => - rename_i x₂ xs - simp [Vector.vector_list_vector] - simp [ih₁] - -lemma zmod_to_bit_to_zmod {n : Nat} [Fact (n > 1)] {x : (ZMod n)} (h : is_bit x): - Bit.toZMod (zmod_to_bit x) = x := by - simp [is_bit] at h - cases h with - | inl => - subst_vars - simp [zmod_to_bit, Bit.toZMod] - | inr => - subst_vars - simp [zmod_to_bit, ZMod.val_one, Bit.toZMod] - -lemma bit_to_zmod_to_bit {n : Nat} [Fact (n > 1)] {x : Bit}: - zmod_to_bit (@Bit.toZMod n x) = x := by - cases x with - | zero => - simp [zmod_to_bit, Bit.toZMod] - | one => - simp [zmod_to_bit, Bit.toZMod] - simp [zmod_to_bit, ZMod.val_one, Bit.toZMod] - -def vector_zmod_to_bit {n d : Nat} (a : Vector (ZMod n) d) : Vector Bit d := - Vector.map zmod_to_bit a - -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] - -lemma vector_zmod_to_bit_to_zmod {n d : Nat} [Fact (n > 1)] {xs : Vector (ZMod n) d} (h : is_vector_binary xs) : - Vector.map Bit.toZMod (vector_zmod_to_bit xs) = xs := by - induction xs using Vector.inductionOn with - | h_nil => simp - | h_cons ih => - simp [is_vector_binary_cons] at h - cases h - simp [vector_zmod_to_bit] - simp [vector_zmod_to_bit] at ih - rw [zmod_to_bit_to_zmod] - rw [ih] - assumption - assumption - -lemma vector_bit_to_zmod_to_bit {d n : Nat} [Fact (n > 1)] {xs : Vector Bit d} : - vector_zmod_to_bit (Vector.map (fun i => @Bit.toZMod n i) xs) = xs := by - induction xs using Vector.inductionOn with - | h_nil => simp - | h_cons ih => - rename_i x xs - simp [vector_zmod_to_bit] - simp [vector_zmod_to_bit] at ih - simp [ih] - rw [bit_to_zmod_to_bit] + simp [is_vector_binary] -lemma vector_zmod_to_bit_dropLast {n d : Nat} [Fact (n > 1)] {xs : Vector (ZMod n) (d+1)} (h : is_vector_binary xs) : - Vector.map Bit.toZMod (Vector.dropLast (vector_zmod_to_bit xs)) = (Vector.dropLast xs) := by - simp [dropLast_symm] - rw [vector_zmod_to_bit_to_zmod] - assumption +lemma is_vector_binary_snoc {N : ℕ} {vs : Vector (ZMod N) n} {v}: is_vector_binary (vs.snoc v) ↔ is_vector_binary vs ∧ is_bit v := by + simp [is_vector_binary] + apply Iff.intro + . intro h + exact ⟨(fun a ha => h a (Or.inl ha)), h v (Or.inr rfl)⟩ + . intro h + rcases h with ⟨hl, hr⟩ + intro a ha + cases ha + . apply hl; assumption + . subst_vars; assumption @[simp] -theorem vector_zmod_to_bit_cons : vector_zmod_to_bit (x ::ᵥ xs) = (nat_to_bit x.val) ::ᵥ vector_zmod_to_bit xs := by - rfl +lemma is_vector_binary_map_toZMod {N n : ℕ} {v : Vector Bool n}: is_vector_binary (Vector.map (Bool.toZMod (N := N)) v) := by + simp [is_vector_binary] + tauto -def recover_binary_nat {d} (rep : Vector Bit 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 Bit d) : ZMod n := match d with - | 0 => 0 - | Nat.succ _ => rep.head.toZMod + 2 * recover_binary_zmod rep.tail +lemma is_vector_binary_iff_exists_bool_vec {N n : ℕ} {v : Vector (ZMod N) n}: + is_vector_binary v ↔ ∃x : Vector Bool n, v = x.map Bool.toZMod := by + induction n with + | zero => simp [is_vector_binary] + | succ n ih => + cases v using Vector.casesOn with | cons hd tl => + simp only [is_vector_binary_cons, ih] + apply Iff.intro + . intro ⟨bhd, ⟨tl, btl⟩⟩ + cases bhd with + | inl hz => + exists (false ::ᵥ tl) + simp [*] + | inr ho => + exists true ::ᵥ tl + simp [*] + . intro ⟨x, hx⟩ + cases x using Vector.casesOn with | cons hd' tl' => + simp at hx + injection hx with hx + injection hx with hx htl + simp [hx] + exists tl' + apply Vector.eq + simp [Vector.toList, htl] + rfl 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 +protected theorem Nat.add_lt_add_of_le_of_lt {a b c d : Nat} (hle : a ≤ b) (hlt : c < d) : + a + c < b + d := + Nat.lt_of_le_of_lt (Nat.add_le_add_right hle _) (Nat.add_lt_add_left hlt _) + +namespace Fin + +def msb {d:ℕ} (v : Fin (2^d.succ)): Bool := v.val ≥ 2^d + @[simp] -theorem recover_binary_nat_zero {n : Nat} : recover_binary_nat (Vector.replicate n Bit.zero) = 0 := by - induction n with - | zero => rfl - | succ n ih => simp [recover_binary_nat, ih] - -theorem recover_binary_zmod_bit {d n} [Fact (n > 1)] {w : Vector (ZMod n) d}: - is_vector_binary w → recover_binary_zmod' w = recover_binary_zmod (vector_zmod_to_bit w) := by - intro h - induction w using Vector.inductionOn with - | h_nil => rfl - | h_cons ih => - simp [recover_binary_zmod', recover_binary_zmod] - rw [is_vector_binary_cons] at h - cases h - rw [ih] - rotate_left - . assumption - rename (is_bit _) => isb - cases isb <;> { - subst_vars - have : n > 1 := (inferInstance : Fact (n > 1)).elim - induction n with - | zero => simp - | succ n => - induction n with - | zero => - simp - | succ => - rw [ZMod.val] - simp - rfl - } +theorem msb_false_of_lt {d:ℕ} {v : Fin (2^d.succ)} (h : v.val < 2^d): msb v = false := by + simpa [msb] -theorem mod_two_bit_back : (Bit.toNat $ bit_mod_two n) = n % 2 := by - simp [bit_mod_two] - split - . simp [*] - . simp [*] - . contradiction - -def is_binary_of {n d} (inp : ZMod n) (rep : Vector Bit d): Prop := inp = recover_binary_zmod rep - -def nat_n_bits (a : Nat) (digits : Nat) : Nat := - Bitvec.bitsToNat (List.reverse (List.take digits (List.reverse (Nat.bits a)))) - -lemma even_ne_odd (a b : Nat): 2 * a ≠ 2 * b + 1 := by - intro h - induction a generalizing b with - | zero => cases h - | succ a1 ih => - rw [Nat.mul_succ] at h - cases b - . cases h - . simp_arith at h - apply ih _ h - -lemma parity_bit_unique (a b : Bit) (c d : Nat) : a + 2 * c = b + 2 * d -> a = b ∧ c = d := by - intro h; cases a <;> cases b <;> simp [Bit.toNat, *] at * - . assumption - . rw [add_comm] at h; apply even_ne_odd _ _ h - . rw [add_comm, eq_comm] at h; apply even_ne_odd _ _ h - . 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 - -theorem binary_nat_lt {d} (rep : Vector Bit d): recover_binary_nat rep < 2 ^ d := by - induction d with - | zero => simp [recover_binary_nat] - | succ _ ih => - simp [recover_binary_nat] - cases rep.head <;> ( - simp [*, Bit.toNat] - simp_arith - let h := ih rep.tail - let h := Nat.le.dest h - cases h; rename_i w h - simp_arith at h - rw [Nat.pow_succ] - ) - . apply @Nat.le.intro _ _ (w + w + 1) - linarith - . apply @Nat.le.intro _ _ (w + w) - linarith - -theorem binary_nat_zmod_equiv {n d} (rep : Vector Bit d): - (recover_binary_nat rep : ZMod n) = (recover_binary_zmod rep) := by - induction d with - | zero => simp [recover_binary_nat, recover_binary_zmod] - | succ d' ih => - simp [recover_binary_nat, recover_binary_zmod] - cases rep.head <;> simp [Bit.toNat, Bit.toZMod, *] - -theorem binary_nat_zmod_equiv_mod_p {n d} (rep : Vector Bit d): - (recover_binary_zmod rep : ZMod n).val = recover_binary_nat rep % n := by - rw [←binary_nat_zmod_equiv] - apply ZMod.val_nat_cast - -theorem binary_zmod_same_as_nat {n d} (rep : Vector Bit d): - 2 ^ d < n -> - (recover_binary_zmod rep : ZMod n).val = recover_binary_nat rep := by - intro d_small - rw [binary_nat_zmod_equiv_mod_p] - apply Nat.mod_eq_of_lt - apply @lt_trans _ _ _ (2^d) - . apply binary_nat_lt - . assumption - -theorem binary_zmod_unique {n d} (rep1 rep2 : Vector Bit d): - 2 ^ d < n -> - (recover_binary_zmod rep1 : ZMod n) = (recover_binary_zmod rep2 : ZMod n) -> - rep1 = rep2 := by - intro d_small - intro same_recs - have same_vals : (recover_binary_zmod rep1 : ZMod n).val = (recover_binary_zmod rep2 : ZMod n).val := by - 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 - -theorem recover_binary_nat_to_bits_le {w : Vector Bit d}: - recover_binary_nat w = v ↔ - nat_to_bits_le d v = some w := by +@[simp] +theorem msb_true_of_ge {d:ℕ} {v : Fin (2^d.succ)} (h : v.val ≥ 2^d): msb v = true := by + simpa [msb] + +def lsbs {d:ℕ} (v : Fin (2^d.succ)): Fin (2^d) := ⟨v.val - (msb v).toNat * 2^d, prop⟩ where + prop := by + cases Nat.lt_or_ge v.val (2^d) with + | inl lt => + simp [lt, Bool.toNat] + | inr ge => + apply Nat.sub_lt_left_of_lt_add + . simp [msb, ge, Bool.toNat] + . have : 2^d + 2^d = 2^d.succ := by simp_arith [pow_succ] + simp [msb, ge, Bool.toNat, v.prop, this] + +private lemma snoc_step_helper {d : ℕ} {b : Bool} {v : Fin (2^d)}: + b.toNat + 2 * v.val < 2^d.succ := by + have : b.toNat ≤ 1 := by cases b <;> simp + simp_arith + calc + b.toNat + 2 * v.val + 1 ≤ 2 * v.val + 2 := by cases b <;> { simp_arith } + _ = 2 * (v.val + 1) := by simp_arith + _ ≤ 2 * 2^d := by + have := Fin.prop v + simp_arith [-Fin.is_lt] at this + simp_arith [this] + _ = 2^(d+1) := by simp [pow_succ] + +private lemma cons_step_helper {d : ℕ} {b : Bool} {v : Fin (2^d)}: + b.toNat * 2^d + v.val < 2^d.succ := by + have : 2 ^ d.succ = 2^d + 2^d := by simp_arith [pow_succ] + apply Nat.add_lt_add_of_le_of_lt + . cases b <;> simp + . apply Fin.is_lt + +theorem msbs_lsbs_decomposition {d} {v : Fin (2^d.succ)}: + v = ⟨(msb v).toNat * 2^d + (lsbs v).val, cons_step_helper⟩ := by + cases Decidable.em (v.val ≥ 2^d) <;> simp [msb, lsbs, *, Bool.toNat] + +theorem msb_lsbs_decomposition_unique {d} {v : Fin (2^d.succ)} {msb' : Bool} {lsbs' : Fin (2^d)} {h}: + v = ⟨(msb'.toNat * 2^d) + lsbs'.val, h⟩ ↔ msb' = msb v ∧ lsbs' = lsbs v := by apply Iff.intro - . induction d generalizing v with - | zero => - cases w using Vector.casesOn - intro h; cases h; rfl - | succ d ih => - cases w using Vector.casesOn; rename_i hd tl; - simp [recover_binary_nat, nat_to_bits_le] - intro h - rw [ih (v := v/2) (w := tl)] - . conv => lhs; whnf - congr - rw [←Nat.mod_add_div (m := v) (k := 2), ←mod_two_bit_back] at h - have := And.left (parity_bit_unique _ _ _ _ h) - apply Eq.symm - assumption - . subst_vars - unfold Bit.toNat - rw [Nat.add_div] - cases hd - . simp - . simp - . simp_arith - . induction d generalizing v with - | zero => - cases w using Vector.casesOn - simp [recover_binary_nat, nat_to_bits_le] - tauto - | succ d ih => - cases w using Vector.casesOn - simp [recover_binary_nat, nat_to_bits_le, Bind.bind] - intro tl htl veq - rw [Vector.vector_eq_cons] at veq - cases veq - subst_vars - rw [ih (v := v/2)] - . rw [mod_two_bit_back] - simp [Nat.mod_add_div] - . assumption - -theorem recover_binary_zmod'_to_bits_le {n : Nat} [Fact (n > 1)] {v : ZMod n} {w : Vector (ZMod n) d}: - 2 ^ d < n → - is_vector_binary w → - recover_binary_zmod' w = v → - nat_to_bits_le d v.val = some (vector_zmod_to_bit w) := by - intros - rw [←recover_binary_nat_to_bits_le] - subst_vars - rw [recover_binary_zmod_bit] - . apply Eq.symm - apply binary_zmod_same_as_nat - assumption - . assumption - -theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : - vector_zmod_to_bit (Vector.map (Bit.toZMod (n := n)) w) = w := by - induction w using Vector.inductionOn with - | h_nil => rfl - | h_cons ih => - simp [vector_zmod_to_bit] at ih - simp [vector_zmod_to_bit, ih] - congr - unfold Bit.toZMod - split <;> { - have : n > 1 := (inferInstance : Fact (n > 1)).elim - induction n with - | zero => - apply absurd this - simp - | succ n => - induction n with - | zero => - apply absurd this - simp - | succ => - rfl - } - -theorem vector_binary_of_bit_to_zmod {n : Nat} [Fact (n > 1)] {w : Vector Bit d }: - is_vector_binary (w.map (Bit.toZMod (n := n))) := by - induction w using Vector.inductionOn with - | h_nil => trivial - | h_cons ih => - simp [is_vector_binary_cons] + . rintro ⟨_⟩ apply And.intro - . unfold Bit.toZMod - split <;> { - have : n > 1 := (inferInstance : Fact (n > 1)).elim - induction n with - | zero => - apply absurd this - simp - | succ n => - induction n with - | zero => - apply absurd this - simp - | succ => - simp [is_bit] + . cases msb' <;> { + simp [msb, Bool.toNat] } - . apply ih - -theorem recover_binary_of_to_bits {n : Nat} [Fact (n > 1)] {w : Vector Bit d} {v : ZMod n}: - nat_to_bits_le d v.val = some w → - recover_binary_zmod' (w.map Bit.toZMod) = v := by - rw [←recover_binary_nat_to_bits_le, recover_binary_zmod_bit, zmod_to_bit_coe] - intro h - rw [←binary_nat_zmod_equiv] - rw [h] - simp [ZMod.val_cast_of_lt] - apply vector_binary_of_bit_to_zmod - -theorem nat_to_bits_le_some_of_lt : n < 2 ^ d → ∃p, nat_to_bits_le d n = some p := by - induction d generalizing n with - | zero => intro h; simp at h; rw [h]; exists Vector.nil - | succ d ih => - intro h - have := ih (n := n / 2) (by - have : 2 ^ d = (2 ^ d.succ) / 2 := by - simp [Nat.pow_succ] - rw [this] - apply Nat.div_lt_div_of_lt_of_dvd - simp [Nat.pow_succ] - assumption - ) - rcases this with ⟨_, h⟩ - apply Exists.intro - unfold nat_to_bits_le - simp [h, Bind.bind] - rfl + . cases msb' <;> { + have : ¬ 2^d ≤ lsbs'.val := not_le_of_lt (Fin.is_lt lsbs') + simp [lsbs, Bool.toNat, msb, this] + } + . rintro ⟨⟨_⟩, ⟨_⟩⟩ + apply Fin.eq_of_veq + cases Decidable.em (2^d ≤ v.val) <;> simp [msb, lsbs, *, Bool.toNat] -def fin_to_bits_le {d : Nat} (n : Fin (2 ^ d)): Vector Bit d := match h: nat_to_bits_le d n.val with -| some r => r -| none => False.elim (by - have := nat_to_bits_le_some_of_lt n.prop - cases this - simp [*] at h - ) - -lemma fin_to_bits_recover_binary {D n : Nat } [Fact (n > 1)] (Index : (ZMod n)) (ix_small : Index.val < 2^D) : - recover_binary_zmod' (Vector.map Bit.toZMod (fin_to_bits_le { val := ZMod.val Index, isLt := ix_small })) = Index := by - rw [recover_binary_of_to_bits] - simp [fin_to_bits_le] - split - . assumption - . contradiction - -lemma fin_to_bits_le_is_some {depth : Nat} {idx : Nat} (h : idx < 2 ^ depth) : - nat_to_bits_le depth idx = some (fin_to_bits_le idx) := by - simp [fin_to_bits_le] - split - . rename_i hnats - rw [Nat.mod_eq_of_lt] at hnats - . simp [hnats] - . simp [h] - . contradiction - -theorem fin_to_bits_le_to_recover_binary_zmod' {n d : Nat} [Fact (n > 1)] {v : ZMod n} {w : Vector (ZMod n) d} {h : v.val < 2^d }: - n > 2^d → - is_vector_binary w → - recover_binary_zmod' w = v → - fin_to_bits_le ⟨v.val, by simp[h]⟩ = vector_zmod_to_bit w := by - intros - have : some (fin_to_bits_le ⟨v.val, by simp[h]⟩) = some (vector_zmod_to_bit w) := by - rw [<-recover_binary_zmod'_to_bits_le] - rotate_left - linarith - assumption - assumption - simp [fin_to_bits_le] - split - rename_i h - simp [h] - contradiction - simp at this - rw [this] - -lemma vector_bit_to_zmod_last {d n : Nat} [Fact (n > 1)] {xs : Vector Bit (d+1)} : - (zmod_to_bit (Vector.last (Vector.map (fun i => @Bit.toZMod n i) xs))) = Vector.last xs := by - cases xs using Vector.casesOn - simp - rename_i x xs - rw [<-vector_zmod_to_bit_last] - simp - have hx : nat_to_bit (ZMod.val (@Bit.toZMod n x)) = x := by - simp [Bit.toZMod, is_bit, nat_to_bit] - cases x - . simp - . simp [ZMod.val_one] - have hxs : vector_zmod_to_bit (Vector.map (fun i => @Bit.toZMod n i) xs) = xs := by - simp [vector_bit_to_zmod_to_bit] - rw [hx, hxs] - -@[elab_as_elim] -def bitCases' {n : Nat} {C : Subtype (α := ZMod n.succ.succ) is_bit → Sort _} (v : Subtype (α := ZMod n.succ.succ) is_bit) - (zero : C bZero) - (one : C bOne): C v := by - rcases v with ⟨v, h⟩ - rcases v with ⟨v, _⟩ - cases v with - | zero => exact zero - | succ v => cases v with - | zero => exact one - | succ v => - apply False.elim - rcases h with h | h <;> { - injection h with h - simp at h - } +@[simp] +theorem lsbs_of_msb_lsbs_decomposition {d} {msb' : Bool} {lsbs' : Fin (2^d)} {h}: + lsbs ⟨(msb'.toNat * 2^d) + lsbs'.val, h⟩ = lsbs' := by + apply eq_comm.mp + refine (msb_lsbs_decomposition_unique.mp (Eq.refl _)).2 -theorem isBitCases (b : Subtype (α := ZMod n) is_bit): b = bZero ∨ b = bOne := by - cases b with | mk _ prop => - cases prop <;> {subst_vars ; tauto } - - -def bitCases : { v : ZMod (Nat.succ (Nat.succ n)) // is_bit v} → Bit - | ⟨0, _⟩ => Bit.zero - | ⟨1, _⟩ => Bit.one - | ⟨⟨Nat.succ (Nat.succ i), _⟩, h⟩ => False.elim (by - cases h <;> { - rename_i h - injection h with h; - rw [Nat.mod_eq_of_lt] at h - . injection h; try (rename_i h; injection h) - . simp - } - ) +@[simp] +theorem msb_of_msb_lsbs_decomposition {d} {msb' : Bool} {lsbs' : Fin (2^d)} {h}: + msb (⟨(msb'.toNat * 2^d) + lsbs'.val, h⟩: Fin (2^d.succ)) = msb' := by + apply eq_comm.mp + refine (msb_lsbs_decomposition_unique.mp (Eq.refl _)).1 -@[simp] lemma ne_1_0 {n:Nat}: ¬(1 : ZMod (n.succ.succ)) = (0 : ZMod (n.succ.succ)) := by - intro h; - conv at h => lhs; whnf - conv at h => rhs; whnf - injection h with h - injection h +def toBitsBE {d : ℕ} (v : Fin (2^d)): Vector Bool d := match d with + | 0 => Vector.nil + | Nat.succ _ => msb v ::ᵥ (lsbs v).toBitsBE -@[simp] lemma ne_0_1 {n:Nat}: ¬(0 : ZMod (n.succ.succ)) = (1 : ZMod (n.succ.succ)) := by - intro h; - conv at h => lhs; whnf - conv at h => rhs; whnf - injection h with h - injection h +def toBitsLE {d : ℕ} (v : Fin (2^d)): Vector Bool d := v.toBitsBE.reverse +@[simp] +theorem lsbs_eq_val_of_lt {d:ℕ} {v : Fin (2^d.succ)} (h : v.val < 2^d): lsbs v = ⟨v, h⟩ := by + simp [lsbs, *, Bool.toNat] + +def ofBitsBE {d : ℕ} (v : Vector Bool d): Fin (2^d) := match d with + | 0 => ⟨0, by decide⟩ + | d + 1 => + let proof := by + have : 2^d.succ = 2^d + 2^d := by simp_arith [pow_succ] + rw [this] + apply Nat.add_lt_add_of_le_of_lt + . cases v.head <;> simp + . apply Fin.prop + ⟨(v.head.toNat * 2^d + (ofBitsBE v.tail).val), proof⟩ + +theorem ofBitsBE_snoc {d : ℕ} {v : Bool} {vs : Vector Bool d}: + ofBitsBE (vs.snoc v) = ⟨v.toNat + 2 * (ofBitsBE vs).val, snoc_step_helper⟩ := by + induction d with + | zero => + cases vs using Vector.casesOn + simp [ofBitsBE] + | succ d ih => + unfold ofBitsBE + simp_arith [Vector.tail_snoc, Vector.head_snoc, ih, Nat.pow_succ] + cases vs.head <;> simp_arith [Bool.toNat] + +def ofBitsLE {d : ℕ} (v : Vector Bool d): Fin (2^d) := ofBitsBE v.reverse + +@[simp] +lemma lsbs_ofBitsBE_eq_ofBitsBE_tail {d : ℕ} {v : Vector Bool d.succ}: + lsbs (ofBitsBE v) = ofBitsBE v.tail := by + induction d with + | zero => simp [ofBitsBE, lsbs] + | succ d ih => + cases v using Vector.casesOn with | cons hd tl => + rw [ofBitsBE] + simp [ih] @[simp] -lemma bitCases_eq_0 : bitCases b = Bit.zero ↔ b = bZero := by - cases b with | mk val prop => - cases prop <;> { - subst_vars - conv => lhs; lhs; whnf - simp - } +lemma msb_ofBitsBE_eq_head {d : ℕ} {v : Vector Bool d.succ}: + msb (ofBitsBE v) = v.head := by + cases v using Vector.casesOn with | cons hd tl => + rw [ofBitsBE] + simp @[simp] -lemma bitCases_eq_1 : bitCases b = Bit.one ↔ b = bOne := by - cases b with | mk val prop => - cases prop <;> { - subst_vars - conv => lhs; lhs; whnf - simp - } +lemma toBitsBE_ofBitsBE_eq_self {d : ℕ} {v : Vector Bool d}: + toBitsBE (ofBitsBE v) = v := by + induction d with + | zero => simp + | succ d ih => simp [toBitsBE, ih] @[simp] -lemma bitCases_bZero {n:Nat}: bitCases (@bZero (n + 2)) = Bit.zero := by rfl +lemma toBitsLE_ofBitsLE_eq_self {d : ℕ} {v : Vector Bool d}: + toBitsLE (ofBitsLE v) = v := by + simp [toBitsLE, ofBitsLE] @[simp] -lemma bitCases_bOne {n:Nat}: bitCases (@bOne (n+2)) = Bit.one := by rfl - -theorem is_vector_binary_iff_allIxes_is_bit {n : Nat} {v : Vector (ZMod n) d}: Vector.allIxes is_bit v ↔ is_vector_binary v := by - induction v using Vector.inductionOn with - | h_nil => simp [is_vector_binary] - | h_cons ih => conv => lhs; simp [ih] - -theorem fin_to_bits_le_recover_binary_nat {v : Vector Bit d}: - fin_to_bits_le ⟨recover_binary_nat v, binary_nat_lt _⟩ = v := by - unfold fin_to_bits_le - split - . rename_i h - rw [←recover_binary_nat_to_bits_le] at h - exact binary_nat_unique _ _ h - . contradiction - -theorem SubVector_map_cast_lower {v : SubVector α n prop} {f : α → β }: - (v.val.map f) = v.lower.map fun (x : Subtype prop) => f x.val := by - rw [←Vector.ofFn_get v.val] - simp only [SubVector.lower, GetElem.getElem, Vector.map_ofFn] +lemma ofBitsBE_toBitsBE_eq_self {d : ℕ} {v : Fin (2^d)}: + ofBitsBE (toBitsBE v) = v := by + induction d with + | zero => simp + | succ d ih => + rw [msbs_lsbs_decomposition (v := v)] + simp [toBitsBE, ofBitsBE, ih] @[simp] -theorem recover_binary_nat_fin_to_bits_le {v : Fin (2^d)}: - recover_binary_nat (fin_to_bits_le v) = v.val := by - unfold fin_to_bits_le - split - . rename_i h - rw [←recover_binary_nat_to_bits_le] at h - assumption - . contradiction +lemma ofBitsLE_toBitsLE_eq_self {d : ℕ} {v : Fin (2^d)}: + ofBitsLE (toBitsLE v) = v := by + simp [toBitsLE, ofBitsLE] @[simp] -theorem SubVector_lower_lift : SubVector.lift (SubVector.lower v) = v := by - unfold SubVector.lift - unfold SubVector.lower - apply Subtype.eq - simp [GetElem.getElem] +lemma toBitsBE_injective : toBitsBE a = toBitsBE b ↔ a = b := by + apply Iff.intro + . intro h + have := congrArg ofBitsBE h + simpa [this] + . intro; simp [*] @[simp] -theorem SubVector_lift_lower : SubVector.lower (SubVector.lift v) = v := by - unfold SubVector.lift - unfold SubVector.lower - apply Subtype.eq - simp [GetElem.getElem] +lemma toBitsLE_injective : toBitsLE a = toBitsLE b ↔ a = b := by + simp [toBitsLE] + +end Fin + +theorem recover_binary_zmod'_map_toZMod_eq_Fin_ofBitsLE {N l : ℕ} {v : Vector Bool l}: + recover_binary_zmod' (Vector.map (Bool.toZMod (N := N)) v) = (Fin.ofBitsLE v).val := by + induction l with + | zero => simp [recover_binary_zmod'] + | succ l ih => + cases v using Vector.casesOn with | cons hd tl => + simp [recover_binary_zmod', Fin.ofBitsLE, Fin.ofBitsBE_snoc, ih] + rfl diff --git a/ProvenZk/Ext/GetElem.lean b/ProvenZk/Ext/GetElem.lean new file mode 100644 index 0000000..9b93963 --- /dev/null +++ b/ProvenZk/Ext/GetElem.lean @@ -0,0 +1,52 @@ +import Mathlib + +theorem getElem?_eq_some_getElem_of_valid_index [GetElem cont idx elem domain] [Decidable (domain container index)] (h : domain container index): + container[index]? = some container[index] := by + unfold getElem? + split + . rfl + . contradiction + +theorem getElem!_eq_getElem_of_valid_index [GetElem cont idx elem domain] [Decidable (domain container index)] [Inhabited elem] (h : domain container index): + container[index]! = container[index] := by + simp [getElem!, h] + +theorem getElem_of_getElem! [GetElem cont idx elem domain] [Decidable (domain container index)] [Inhabited elem] (ix_ok : domain container index) (h : container[index]! = element): + container[index] = element := by + simp [getElem!, ix_ok] at h + assumption + +theorem getElem?_none_of_invalid_index [GetElem cont idx elem domain] [Decidable (domain container index)] (h : ¬ domain container index): + container[index]? = none := by + unfold getElem? + split + . tauto + . rfl + +theorem valid_index_of_getElem?_some [GetElem cont idx elem domain] [Decidable (domain container index)] (h : container[index]? = some element): + domain container index := by + unfold getElem? at h + split at h + . assumption + . contradiction + +theorem getElem_of_getElem?_some [GetElem cont idx elem domain] [Decidable (domain container index)] (h : container[index]? = some element): + container[index]'(valid_index_of_getElem?_some h) = element := by + unfold getElem? at h + split at h + . injection h + . contradiction + +theorem getElem?_some_of_getElem [GetElem cont idx elem domain] [Decidable (domain container index)] {ix_valid : domain container index} (h : container[index]'ix_valid = element): + container[index]? = some element := by + unfold getElem? + split + . congr + . contradiction + +theorem getElem!_eq_getElem?_get! [GetElem cont idx elem domain] [Decidable (domain container index)] [Inhabited elem]: + container[index]! = container[index]?.get! := by + simp [getElem!, getElem?] + split + . rfl + . unfold Option.get!; rfl diff --git a/ProvenZk/Ext/List.lean b/ProvenZk/Ext/List.lean index cc5b9f6..3081c20 100644 --- a/ProvenZk/Ext/List.lean +++ b/ProvenZk/Ext/List.lean @@ -1,6 +1,3 @@ --- import Mathlib.Data.List.Basic --- import Mathlib.Data.List.Indexes -import Std.Data.List.Basic import Mathlib.Data.List.Basic import Mathlib.Data.List.Indexes @@ -42,4 +39,4 @@ theorem dropLast_cons {head₁ head₂ : α} {tail : List α} : List.dropLast (h | nil => simp | cons _ _ _ => simp [List.dropLast] -end List +end List \ No newline at end of file diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 2d50776..3aabd2d 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -1,11 +1,7 @@ ---import Mathlib.Data.Vector.Snoc ---import Mathlib.Data.Matrix.Basic ---import Mathlib.Data.List.Defs -import Mathlib.Data.Vector -import Mathlib.Data.Vector.Basic import Mathlib.Data.Vector.Snoc +import Mathlib.Data.Vector.Mem import Mathlib.Data.Matrix.Basic -import Std.Data.Fin.Lemmas +import Mathlib.Data.List.Defs import ProvenZk.Ext.Fin import ProvenZk.Ext.Range @@ -113,10 +109,10 @@ macro_rules def to_column (v : Vector α n) : Matrix (Fin n) Unit α := Matrix.of (fun i _ => v.get i) -theorem vector_eq_cons : (x ::ᵥ xs) = (y ::ᵥ ys) ↔ x = y ∧ xs = ys := by +theorem eq_cons : (x ::ᵥ xs) = (y ::ᵥ ys) ↔ x = y ∧ xs = ys := by simp [Vector.eq_cons_iff] -theorem vector_reverse_eq {x y : Vector α n} : (x.reverse = y) ↔ (x = y.reverse) := by +theorem reverse_eq {x y : Vector α n} : (x.reverse = y) ↔ (x = y.reverse) := by apply Iff.intro case mp => { intro @@ -129,31 +125,28 @@ theorem vector_reverse_eq {x y : Vector α n} : (x.reverse = y) ↔ (x = y.rever simp } -@[simp] -theorem vector_replicate_succ : Vector.replicate (Nat.succ n) a = a ::ᵥ Vector.replicate n a := by - rfl - -theorem vector_replicate_succ_snoc : Vector.replicate (Nat.succ n) a = (Vector.replicate n a).snoc a := by +theorem replicate_succ_snoc : Vector.replicate (Nat.succ n) a = (Vector.replicate n a).snoc a := by induction n with | zero => rfl | succ n ih => conv => rhs; simp [←ih] @[simp] -theorem vector_replicate_reverse : Vector.reverse (Vector.replicate n a) = Vector.replicate n a := by +theorem replicate_reverse : Vector.reverse (Vector.replicate n a) = Vector.replicate n a := by induction n with | zero => rfl | succ n ih => - simp [ih, ←vector_replicate_succ_snoc] + simp [ih, ←replicate_succ_snoc] @[simp] -theorem vector_map_replicate : Vector.map f (Vector.replicate n a) = Vector.replicate n (f a) := by +theorem map_replicate : Vector.map f (Vector.replicate n a) = Vector.replicate n (f a) := by induction n with | zero => rfl | succ n ih => simp [ih] -theorem vector_reverse_inj {a b : Vector α d} : Vector.reverse a = Vector.reverse b ↔ a = b := by +@[simp] +theorem reverse_inj {a b : Vector α d} : Vector.reverse a = Vector.reverse b ↔ a = b := by apply Iff.intro . intro h induction d with @@ -172,7 +165,8 @@ theorem vector_reverse_inj {a b : Vector α d} : Vector.reverse a = Vector.rever assumption . intro h; congr -theorem vector_map_inj {a b : Vector α d} {f_inj : ∀ a b, f a = f b → a = b}: a.map f = b.map f ↔ a = b := by +@[simp] +theorem map_inj {a b : Vector α d} {f_inj : ∀ a b, f a = f b → a = b}: a.map f = b.map f ↔ a = b := by apply Iff.intro . intro h induction d with @@ -195,20 +189,17 @@ def dropLast { n : Nat } (v : Vector α n) : Vector α (n-1) := ⟨List.dropLast lemma toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toList.dropLast := by rfl -lemma vector_list_vector {d} {x₁ x₂ : α} {xs : Vector α d} : (x₁ ::ᵥ x₂ ::ᵥ xs).dropLast = x₁ ::ᵥ (x₂ ::ᵥ xs).dropLast := by - rfl - @[simp] -theorem vector_get_zero {vs : Vector i n} : (v ::ᵥ vs)[0] = v := by rfl +theorem getElem_zero {vs : Vector i n} : (v ::ᵥ vs)[0] = v := by rfl @[simp] -theorem vector_get_succ_fin {vs : Vector i n} {i : Fin n} : (v ::ᵥ vs)[i.succ] = vs[i] := by rfl +theorem get_succ_fin {vs : Vector i n} {i : Fin n} : (v ::ᵥ vs)[i.succ] = vs[i] := by rfl @[simp] -theorem vector_get_succ_nat {vs : Vector i n} {i : Nat} {h : i.succ < n.succ } : (v ::ᵥ vs)[i.succ]'h = vs[i]'(by linarith) := by rfl +theorem get_succ_nat {vs : Vector i n} {i : Nat} {h : i.succ < n.succ } : (v ::ᵥ vs)[i.succ]'h = vs[i]'(by linarith) := by rfl @[simp] -theorem vector_get_snoc_last { vs : Vector α n }: +theorem get_snoc_last { vs : Vector α n }: (vs.snoc v).get (Fin.last n) = v := by induction n with | zero => @@ -233,16 +224,16 @@ lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = v | zero => simp | succ i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih] -theorem vector_get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by +theorem get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by rfl theorem getElem_def {v : Vector α n} {i : Nat} {prop}: v[i]'prop = v.get ⟨i, prop⟩ := by rfl @[simp] -lemma vector_get_snoc_fin_prev {vs : Vector α n} {v : α} {i : Fin n}: +lemma get_snoc_fin_prev {vs : Vector α n} {v : α} {i : Fin n}: (vs.snoc v)[i.val]'(by (have := i.prop); linarith) = vs[i.val]'(i.prop) := by - simp [vector_get_val_getElem, getElem_def, Fin.castSucc_def] + simp [get_val_getElem, getElem_def, Fin.castSucc_def] theorem ofFn_snoc' { fn : Fin (Nat.succ n) → α }: Vector.ofFn fn = Vector.snoc (Vector.ofFn (fun (x : Fin n) => fn (Fin.castSucc x))) (fn n) := by @@ -256,44 +247,10 @@ theorem ofFn_snoc' { fn : Fin (Nat.succ n) → α }: congr simp [Nat.mod_eq_of_lt] -def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i] +instance : Membership α (Vector α n) := ⟨fun x xs => x ∈ xs.toList⟩ @[simp] -theorem allIxes_cons : allIxes f (v ::ᵥ vs) ↔ f v ∧ allIxes f vs := by - simp [allIxes, GetElem.getElem] - apply Iff.intro - . intro h - exact ⟨h 0, fun i => h i.succ⟩ - . intro h i - cases i using Fin.cases - . simp [h.1] - . simp [h.2] - -@[simp] -theorem allIxes_nil : allIxes f Vector.nil := by - simp [allIxes] - -theorem getElem_allIxes {v : { v: Vector α n // allIxes prop v }} {i : Nat} { i_small : i < n}: - v.val[i]'i_small = ↑(Subtype.mk (v.val.get ⟨i, i_small⟩) (v.prop ⟨i, i_small⟩)) := by rfl - -theorem getElem_allIxes₂ {v : { v: Vector (Vector α m) n // allIxes (allIxes prop) v }} {i j: Nat} { i_small : i < n} { j_small : j < m}: - (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (v.prop ⟨i, i_small⟩ ⟨j, j_small⟩)) := by rfl - -theorem allIxes_indexed {v : {v : Vector α n // allIxes prop v}} {i : Nat} {i_small : i < n}: - prop (v.val[i]'i_small) := v.prop ⟨i, i_small⟩ - -theorem allIxes_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes prop) v}} - {i : Nat} {i_small : i < c} - {j : Nat} {j_small : j < b}: - prop ((v.val[i]'i_small)[j]'j_small) := - v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ - -theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes (allIxes prop)) v}} - {i : Nat} {i_small : i < c} - {j : Nat} {j_small : j < b} - {k : Nat} {k_small : k < a}: - prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) := - v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ ⟨k, k_small⟩ +theorem mem_def {xs : Vector α n} {x} : x ∈ xs ↔ x ∈ xs.toList := by rfl @[simp] theorem map_ofFn {f : α → β} (g : Fin n → α) : @@ -338,59 +295,99 @@ theorem append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: subst_vars apply And.intro <;> rfl -theorem allIxes_toList : Vector.allIxes prop v ↔ ∀ i, prop (v.toList.get i) := by - unfold Vector.allIxes +lemma eq_iff {n} {v w : Vector α n} : v = w ↔ v.toList = w.toList := by + apply Iff.intro + . intro h + subst h + rfl + . intro h + apply Vector.eq + simp at h + assumption + +theorem append_inj_iff {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: + v₁ ++ v₂ = w₁ ++ w₂ ↔ v₁ = w₁ ∧ v₂ = w₂ := by + apply Iff.intro + . exact append_inj + . intro ⟨_, _⟩ + simp [*] + + +@[simp] +theorem getElem_map {i n : ℕ} {h : i < n} {v : Vector α n} : (Vector.map f v)[i]'h = f (v[i]'h) := by + simp [getElem] + +theorem map_singleton {a : α} {f : α → β} : Vector.map f (a ::ᵥ Vector.nil) = (f a ::ᵥ Vector.nil) := by + rfl + +@[simp] +lemma getElem_snoc_at_length {vs : Vector α n}: (vs.snoc v)[n]'(by simp_arith) = v := by + induction n with + | zero => cases vs using Vector.casesOn; rfl + | succ n ih => cases vs using Vector.casesOn; simp [ih] + +@[simp] +lemma getElem_snoc_before_length {vs : Vector α n} {i : ℕ} (hp : i < n): (vs.snoc v)[i]'(by linarith) = vs[i]'hp := by + induction n generalizing i with + | zero => cases vs using Vector.casesOn; contradiction + | succ n ih => + cases vs using Vector.casesOn; + cases i with + | zero => simp + | succ i => simp [ih (Nat.lt_of_succ_lt_succ hp)] + + +def permute (fn : Fin m → Fin n) (v : Vector α n): Vector α m := + Vector.ofFn (fun i => v[fn i]) + +theorem permute_inj {n : Nat} {fn : Fin m → Fin n} (perm_surj : Function.Surjective fn): Function.Injective (permute (α := α) fn) := by + intro v₁ v₂ h + ext i + rcases perm_surj i with ⟨j, i_inv⟩ + have : (permute fn v₁).get j = (permute fn v₂).get j := by rw [h] + simp [permute, GetElem.getElem] at this + subst_vars + assumption + +theorem map_permute {p : Fin m → Fin n} {f : α → β} {v : Vector α n}: + Vector.map f (permute p v) = permute p (v.map f) := by + simp [permute] + +theorem exists_succ_iff_exists_snoc {α d} {pred : Vector α (Nat.succ d) → Prop}: + (∃v, pred v) ↔ ∃vs v, pred (Vector.snoc vs v) := by + apply Iff.intro + . rintro ⟨v, hp⟩ + cases v using Vector.revCasesOn + apply Exists.intro + apply Exists.intro + assumption + . rintro ⟨vs, v, hp⟩ + exists vs.snoc v + +theorem exists_succ_iff_exists_cons {α d} {pred : Vector α (Nat.succ d) → Prop}: + (∃v, pred v) ↔ ∃v vs, pred (v ::ᵥ vs) := by apply Iff.intro - . intro h i - rcases i with ⟨i, p⟩ - simp at p - simp [GetElem.getElem, Vector.get] at h - have := h ⟨i, p⟩ - conv at this => arg 1; whnf - exact this - . intro h i - simp [GetElem.getElem, Vector.get] - rcases i with ⟨i, p⟩ - have := h ⟨i, by simpa⟩ - conv at this => arg 1; whnf - exact this - -theorem allIxes_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allIxes prop (v₁ ++ v₂) ↔ Vector.allIxes prop v₁ ∧ Vector.allIxes prop v₂ := by - simp [allIxes_toList] + . rintro ⟨v, hp⟩ + cases v using Vector.casesOn + apply Exists.intro + apply Exists.intro + assumption + . rintro ⟨v, vs, hp⟩ + exists (v ::ᵥ vs) + +@[simp] +theorem snoc_eq : Vector.snoc xs x = Vector.snoc ys y ↔ xs = ys ∧ x = y := by apply Iff.intro . intro h - apply And.intro - . intro i - rcases i with ⟨i, hp⟩ - simp at hp - rw [←List.get_append] - exact h ⟨i, (by simp; apply Nat.lt_add_right; assumption)⟩ - . intro i - rcases i with ⟨i, hp⟩ - simp at hp - have := h ⟨n₁ + i, (by simpa)⟩ - rw [List.get_append_right] at this - simp at this - exact this - . simp - . simpa - . intro ⟨l, r⟩ - intro ⟨i, hi⟩ - simp at hi - cases lt_or_ge i n₁ with - | inl hp => - rw [List.get_append _ (by simpa)] - exact l ⟨i, (by simpa)⟩ - | inr hp => - rw [List.get_append_right] - have := r ⟨i - n₁, (by simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption )⟩ - simp at this - simpa - . simp; exact LE.le.ge hp - . simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption - -theorem SubVector_append {v₁ : Vector α d₁} {prop₁ : Vector.allIxes prop v₁ } {v₂ : Vector α d₂} {prop₂ : Vector.allIxes prop v₂}: - (Subtype.mk v₁ prop₁).val ++ (Subtype.mk v₂ prop₂).val = - (Subtype.mk (v₁ ++ v₂) (allIxes_append.mpr ⟨prop₁, prop₂⟩)).val := by eq_refl + have := congrArg Vector.reverse h + simp at this + injection this with this + injection this with h t + simp [*] + apply Vector.eq + have := congrArg List.reverse t + simpa [this] + . intro ⟨_, _⟩ + simp [*] end Vector diff --git a/ProvenZk/Ext/Vector/SetLoop.lean b/ProvenZk/Ext/Vector/SetLoop.lean index fea130c..a4084de 100644 --- a/ProvenZk/Ext/Vector/SetLoop.lean +++ b/ProvenZk/Ext/Vector/SetLoop.lean @@ -1,5 +1,6 @@ import ProvenZk.Ext.Vector.Basic + namespace Vector private lemma set_at_len (l1 l2 : List α) (it new : α): @@ -132,4 +133,4 @@ theorem setLoop_mapIdx {v : Vector α n} {f : ℕ -> α -> α }: apply Vector.eq simp [listMapIdx_setLoop, toList_setLoop] -end Vector +end Vector \ No newline at end of file diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean index 7e03076..e944ac4 100644 --- a/ProvenZk/Gates.lean +++ b/ProvenZk/Gates.lean @@ -1,19 +1,20 @@ -import Mathlib.Data.ZMod.Defs +import Mathlib.Data.ZMod.Basic import ProvenZk.Binary +open BigOperators + namespace Gates variable {N : Nat} -variable [Fact (Nat.Prime N)] def is_bool (a : ZMod N): Prop := a = 0 ∨ a = 1 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 = a * (1 / b)) ∨ (a = 0 ∧ b = 0 ∧ out = 0) -def div (a b out : ZMod N): Prop := b ≠ 0 ∧ out = a * (1 / b) -def inv (a out : ZMod N): Prop := a ≠ 0 ∧ out = 1 / a +def div_unchecked [Fact (Nat.Prime N)] (a b out : ZMod N): Prop := (b ≠ 0 ∧ out = a * (1 / b)) ∨ (a = 0 ∧ b = 0 ∧ out = 0) +def div [Fact (Nat.Prime N)] (a b out : ZMod N): Prop := b ≠ 0 ∧ out = a * (1 / b) +def inv [Fact (Nat.Prime N)] (a out : ZMod N): Prop := a ≠ 0 ∧ out = 1 / a def xor (a b out : ZMod N): Prop := is_bool a ∧ is_bool b ∧ out = a*(1-2*b)+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 @@ -31,6 +32,6 @@ def is_zero (a out: ZMod N): Prop := (a = 0 ∧ out = 1) ∨ (a != 0 ∧ out = 0 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 := ZMod.val a <= ZMod.val b -def to_binary (a : ZMod N) (n : Nat) (out : Vector (ZMod N) n): Prop := (recover_binary_zmod' out : ZMod N) = a ∧ is_vector_binary out +def to_binary (a : ZMod N) (n : Nat) (out : Vector (ZMod N) n): Prop := recover_binary_zmod' out = a ∧ is_vector_binary out def from_binary {d} (a : Vector (ZMod N) d) (out : ZMod N): Prop := (recover_binary_zmod' a : ZMod N) = out end Gates diff --git a/ProvenZk/Hash.lean b/ProvenZk/Hash.lean index be914d1..a6572b8 100644 --- a/ProvenZk/Hash.lean +++ b/ProvenZk/Hash.lean @@ -2,10 +2,10 @@ import ProvenZk.Ext.Vector def Hash (F: Type) (n: Nat) : Type := Vector F n -> F -def perfect_hash {F n} (h: Hash F n): Prop := ∀{i1 i2}, h i1 = h i2 → i1 = i2 +def CollisionResistant {F n} (h: Hash F n): Prop := ∀{i1 i2}, h i1 = h i2 → i1 = i2 -@[simp] theorem simp_hash {h : Hash F n} [Fact (perfect_hash h)] {a b : Vector F n}: h a = h b ↔ a = b := by - have : perfect_hash h := (inferInstance : Fact (perfect_hash h)).elim +@[simp] theorem CollisionResistant_def {h : Hash F n} [Fact (CollisionResistant h)] {a b : Vector F n}: h a = h b ↔ a = b := by + have : CollisionResistant h := (inferInstance : Fact (CollisionResistant h)).elim apply Iff.intro - { apply (inferInstance : Fact (perfect_hash h)).elim } - { tauto } \ No newline at end of file + { apply (inferInstance : Fact (CollisionResistant h)).elim } + { tauto } diff --git a/ProvenZk/Lemmas.lean b/ProvenZk/Lemmas.lean new file mode 100644 index 0000000..c94adfa --- /dev/null +++ b/ProvenZk/Lemmas.lean @@ -0,0 +1,175 @@ +import ProvenZk.Gates +import ProvenZk.Binary + +import Mathlib.Data.Vector.MapLemmas +import Mathlib + +variable {N : Nat} +variable [Fact (Nat.Prime N)] + +instance : Fact (N > 1) := ⟨Nat.Prime.one_lt Fact.out⟩ + +theorem ZMod.eq_of_veq {a b : ZMod N} (h : a.val = b.val) : a = b := by + have : N ≠ 0 := by apply Nat.Prime.ne_zero Fact.out + have : ∃n, N = Nat.succ n := by exists N.pred; simp [Nat.succ_pred this] + rcases this with ⟨_, ⟨_⟩⟩ + simp [val] at h + exact Fin.eq_of_veq h + + +theorem ZMod.val_fin {n : ℕ} {i : ZMod (Nat.succ n)} : i.val = Fin.val i := by + simp [ZMod.val] + +@[simp] +theorem exists_eq_left₂ {pred : α → β → Prop}: + (∃a b, (a = c ∧ b = d) ∧ pred a b) ↔ pred c d := by + simp [and_assoc] + +@[simp] +theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by rfl + +@[simp] +theorem Gates.eq_def : Gates.eq a b ↔ a = b := by simp [Gates.eq] + +@[simp] +theorem Gates.sub_def {N} {a b : ZMod N} : Gates.sub a b = a - b := by simp [Gates.sub] + +@[simp] +theorem Gates.is_zero_def {N} {a out : ZMod N} : Gates.is_zero a out ↔ out = Bool.toZMod (a = 0) := by + simp [Gates.is_zero] + apply Iff.intro + . rintro (_ | _) <;> simp [*] + . rintro ⟨_⟩ + simp [Bool.toZMod, Bool.toNat] + tauto + +@[simp] +theorem Gates.select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by + simp [Gates.select] + +@[simp] +theorem Gates.select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by + simp [Gates.select] + +@[simp] +theorem Gates.or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by + simp [Gates.or] + +@[simp] +theorem Gates.zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by + simp [Gates.or] + +@[simp] +theorem Gates.one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by + simp [Gates.or] + +@[simp] +theorem Gates.or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by + simp [Gates.or] + +@[simp] +theorem Gates.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] + tauto + +@[simp] +theorem Gates.xor_bool {N} [Fact (N>1)] {a b : Bool} {c : ZMod N} : Gates.xor a.toZMod b.toZMod c ↔ c = (a != b).toZMod := by + unfold xor + cases a <;> cases b <;> { + simp [is_bool, Bool.toZMod, Bool.toNat, bne] + try ring_nf + } + +@[simp] +theorem Gates.and_bool {N} [Fact (N>1)] {a b : Bool} {c : ZMod N} : Gates.and a.toZMod b.toZMod c ↔ c = (a && b).toZMod := by + unfold and + cases a <;> cases b <;> { + simp [is_bool, Bool.toZMod, Bool.toNat] + } + +@[simp] +theorem Gates.or_bool {N} [Fact (N>1)] {a b : Bool} {c : ZMod N} : Gates.or a.toZMod b.toZMod c ↔ c = (a || b).toZMod := by + unfold or + cases a <;> cases b <;> { + simp [is_bool, Bool.toZMod, Bool.toNat] + } + +@[simp] +theorem Gates.not_bool {N} [Fact (N>1)] {a : Bool} : (1 : ZMod N) - a.toZMod = (!a).toZMod := by + cases a <;> simp [sub] + +@[simp] +lemma Gates.select_bool {N} [Fact (N > 1)] {c : Bool} {t f r : ZMod N}: Gates.select (c.toZMod (N:=N)) t f r ↔ r = if c then t else f := by + cases c <;> simp [select, is_bool] + +@[simp] +lemma Gates.eq_1_toZMod {N} [Fact (N>1)] {b : Bool}: Gates.eq (b.toZMod (N:=N)) 1 ↔ b := by + cases b <;> simp [eq, is_bool] + +@[simp] +lemma Gates.ite_0_toZMod {N} [Fact (N>1)] {b f: Bool}: (if b then (0:ZMod N) else f.toZMod (N:=N)) = (if b then false else f).toZMod := by + cases b <;> simp + +theorem Gates.to_binary_rangecheck {a : ZMod N} {n out} (h: to_binary a n out): a.val < 2^n := by + rcases h with ⟨hrec, hbin⟩ + replace hbin := is_vector_binary_iff_exists_bool_vec.mp hbin + rcases hbin with ⟨x, ⟨_⟩⟩ + rw [recover_binary_zmod'_map_toZMod_eq_Fin_ofBitsLE] at hrec + cases Nat.lt_or_ge (2^n) N with + | inl hp => + cases hrec + have : (Fin.ofBitsLE x).val < N := Nat.lt_trans (Fin.is_lt _) hp + rw [ZMod.val_nat_cast, Nat.mod_eq_of_lt this] + exact Fin.is_lt _ + | inr hp => + apply Nat.lt_of_lt_of_le + . apply ZMod.val_lt + . simp [*] + +lemma Gates.to_binary_iff_eq_Fin_ofBitsLE {l : ℕ} {a : ZMod N} {v : Vector (ZMod N) l}: + Gates.to_binary a l v ↔ ∃v', v = v'.map Bool.toZMod ∧ a = (Fin.ofBitsLE v').val := by + unfold to_binary + rw [is_vector_binary_iff_exists_bool_vec] + apply Iff.intro + . rintro ⟨⟨_⟩, ⟨x, ⟨_⟩⟩⟩ + exists x + cases x using Vector.casesOn + . simp [recover_binary_zmod'] + . rename_i xhd xtl + simp [recover_binary_zmod', recover_binary_zmod'_map_toZMod_eq_Fin_ofBitsLE, Fin.ofBitsLE, Fin.ofBitsBE_snoc] + rfl + . rintro ⟨v', ⟨_⟩, ⟨_⟩⟩ + simp [recover_binary_zmod'_map_toZMod_eq_Fin_ofBitsLE] + +@[simp] +lemma map_toZMod_ofZMod_eq_self_of_is_vector_binary {n : ℕ} {v : Vector (ZMod N) n} (h : is_vector_binary v) : + v.map (fun x => Bool.toZMod (Bool.ofZMod x)) = v := by + induction n with + | zero => simp [Vector.map] + | succ n ih => + cases v using Vector.casesOn + simp only [is_vector_binary_cons] at h + simp [*] + +lemma Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt {l : ℕ} {a : ZMod N} {v : Vector (ZMod N) l} (pow_lt : 2 ^ l < N): + Gates.to_binary a l v ↔ ∃(ha : a.val < 2^l), v = (Fin.toBitsLE ⟨a.val, ha⟩).map Bool.toZMod := by + apply Iff.intro + . intro to_bin + have := Gates.to_binary_rangecheck to_bin + exists this + rw [Gates.to_binary_iff_eq_Fin_ofBitsLE] at to_bin + rcases to_bin with ⟨v, ⟨_⟩, ⟨_⟩⟩ + have : Fin.mk (ZMod.val ((Fin.ofBitsLE v) : ZMod N)) this = Fin.ofBitsLE v := by + apply Fin.eq_of_veq + simp + rw [ZMod.val_cast_of_lt] + apply Nat.lt_trans (Fin.is_lt _) pow_lt + rw [this] + simp [Fin.toBitsLE, Fin.ofBitsLE] + . intro ⟨ha, hv⟩ + rw [Gates.to_binary_iff_eq_Fin_ofBitsLE] + simp [*] + +lemma Gates.from_binary_iff_eq_ofBitsLE_mod_order {l : ℕ} {a : Vector Bool l} {out : ZMod N}: + Gates.from_binary (a.map Bool.toZMod) out ↔ out = (Fin.ofBitsLE a).val := by + simp [from_binary, recover_binary_zmod'_map_toZMod_eq_Fin_ofBitsLE, eq_comm] diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 884f7fd..23e291a 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -4,207 +4,6 @@ import ProvenZk.Ext.Vector import ProvenZk.Hash import ProvenZk.Binary -inductive Dir : Type -| left : Dir -| right : Dir -deriving Repr - -namespace Dir - -def swap : Dir -> Dir -| left => right -| right => left - -instance : Inhabited Dir where - default := left - -def toNat : Dir -> Nat := fun b => match b with - | Dir.left => 0 - | Dir.right => 1 - -def toZMod {n} : Dir -> ZMod n := fun b => match b with - | Dir.left => 0 - | Dir.right => 1 - -def nat_to_dir : Nat -> Dir - | 0 => Dir.left - | 1 => Dir.right - | Nat.succ (Nat.succ _) => panic "Dir can be 0 or 1" - -def dir_mod_two (inp : Nat) : Dir := match h:inp%2 with - | 0 => Dir.left - | 1 => Dir.right - | x + 2 => False.elim (by - have := Nat.mod_lt inp (y := 2) - rw [h] at this - simp at this - contradiction - ) - -def nat_to_list_le : Nat → List Dir - | 0 => [Dir.left] - | 1 => [Dir.right] - | x+2 => dir_mod_two x :: nat_to_list_le ((x + 2) / 2) -termination_by nat_to_list_le x => x -decreasing_by simp_wf; simp_arith; apply Nat.div_le_self - -def nat_to_list_be (d: Nat) (ix: Nat): Vector Dir d := match d with -| 0 => Vector.nil -| Nat.succ d' => if ix ≥ 2^d' - then Dir.right ::ᵥ nat_to_list_be d' (ix - 2^d') - else Dir.left ::ᵥ nat_to_list_be d' ix - -def dir_to_bit : Dir → Bit - | Dir.left => Bit.zero - | Dir.right => Bit.one - -def bit_to_dir : Bit → Dir - | Bit.zero => Dir.left - | Bit.one => Dir.right - -theorem bit_to_dir_to_bit : Dir.bit_to_dir (Dir.dir_to_bit x) = x := by cases x <;> rfl - -def nat_to_dir_vec (idx : Nat) (depth : Nat ): Option <| Vector Dir depth := - (Vector.reverse ∘ Vector.map bit_to_dir) <$> nat_to_bits_le depth idx - -def create_dir_vec {n} {depth} (ix: Vector (ZMod n) depth) : Vector Dir depth := - Vector.map Dir.nat_to_dir (Vector.map ZMod.val ix) - -def list_to_vec_n (L : List Dir) (n : Nat) : Vector Dir n := ⟨List.takeI n L, List.takeI_length n L⟩ - -@[simp] -theorem list_to_vec_cons_succ : list_to_vec_n (x :: xs) (Nat.succ n) = x ::ᵥ list_to_vec_n xs n := by - rfl - -@[simp] -theorem list_to_vec_nil: list_to_vec_n [] n = Vector.replicate n Dir.left := by - apply Vector.eq - simp [list_to_vec_n, Vector.replicate, default] - -@[simp] -lemma create_dir_vec_reverse {n} {depth} (ix : Vector (ZMod n) depth) : - create_dir_vec ix.reverse = (create_dir_vec ix).reverse := by - simp [create_dir_vec] - apply Vector.eq - simp [Vector.toList_reverse, List.map_reverse] - -@[simp] -lemma create_dir_vec_cons {n} {ix : ZMod n} {ixes: Vector (ZMod n) d} : - create_dir_vec (ix ::ᵥ ixes) = Dir.nat_to_dir ix.val ::ᵥ create_dir_vec ixes := by - simp [create_dir_vec] - -theorem dir_bit_dir : Dir.nat_to_dir x = Dir.bit_to_dir (nat_to_bit x) := by - cases x - . rfl - . rename_i x; cases x <;> rfl - -theorem create_dir_vec_bit : Dir.create_dir_vec w = Vector.map Dir.bit_to_dir (vector_zmod_to_bit w) := by - induction w using Vector.inductionOn with - | h_nil => rfl - | h_cons ih => - simp [ih] - congr - rw [dir_bit_dir] - -theorem nat_to_dir_vec_unique {ix₁ ix₂ : Nat} {r₁ r₂ : Vector Dir d}: - Dir.nat_to_dir_vec ix₁ d = some r₁ → Dir.nat_to_dir_vec ix₂ d = some r₂ → r₁ = r₂ → ix₁ = ix₂ := by - simp [Dir.nat_to_dir_vec] - intros - subst_vars - rw [←recover_binary_nat_to_bits_le, Vector.vector_reverse_inj, Vector.vector_map_inj] at * - subst_vars - rfl - . intro a b; cases a <;> { cases b <;> tauto } - -lemma dropLastOrder {d n : Nat} {out : Vector (ZMod n) d} : Dir.create_dir_vec (Vector.dropLast out) = (Dir.create_dir_vec out).dropLast := by - induction out using Vector.inductionOn with - | h_nil => - simp [Dir.create_dir_vec, Vector.dropLast, Dir.nat_to_dir, Vector.map] - | h_cons ih₁ => - rename_i x₁ xs - induction xs using Vector.inductionOn with - | h_nil => - simp [Dir.create_dir_vec, Vector.dropLast, Dir.nat_to_dir, Vector.map] - | h_cons _ => - rename_i x₂ xs - simp [Vector.vector_list_vector] - simp [ih₁] - -def fin_to_dir_vec {depth : Nat} (idx : Fin (2 ^ depth)): Vector Dir depth := - (Vector.map Dir.bit_to_dir (fin_to_bits_le idx)) - -lemma zmod_to_bit_and_dir {n : Nat} [Fact (n > 1)] {x : ZMod n} {h : is_bit x}: - Dir.bit_to_dir (zmod_to_bit x) = Dir.nat_to_dir (ZMod.val x) := by - simp only [zmod_to_bit] - simp only [Dir.bit_to_dir] - simp only [Dir.nat_to_dir] - cases h with - | inl => - rename_i h - simp [h] - | inr => - rename_i h - simp [h] - rw [ZMod.val_one] - -lemma vector_zmod_to_bit_and_dir {n : Nat} [Fact (n > 1)] {w : Vector (ZMod n) d} : - is_vector_binary w → - Vector.map (fun x => Dir.bit_to_dir (zmod_to_bit x)) w = Vector.map (fun x => Dir.nat_to_dir (ZMod.val x)) w := by - induction w using Vector.inductionOn with - | h_nil => - simp - | h_cons ih => - intro h - simp [is_vector_binary_cons] at h - cases h - rename_i y ys - simp - rw [zmod_to_bit_and_dir] - rw [ih] - assumption - assumption - -theorem recover_binary_zmod'_to_dir {n d : Nat} [Fact (n > 1)] {v : ZMod n} {w : Vector (ZMod n) d}: - v.val < 2^d → - n > 2^d → - is_vector_binary w → - recover_binary_zmod' w = v → - fin_to_dir_vec v.val = (Dir.create_dir_vec w) := by - intros - simp [fin_to_dir_vec] - simp [fin_to_bits_le] - split - . simp [Dir.create_dir_vec] - rename_i r _ - have : some r = some (vector_zmod_to_bit w) := by - rw [<-@recover_binary_zmod'_to_bits_le (v:= v)] - apply Eq.symm - rename_i h - rw [ZMod.cast_eq_val] at h - rw [Fin.val_cast_of_lt] at h - assumption - assumption - assumption - linarith - assumption - assumption - simp at this - rw [this] - simp [vector_zmod_to_bit] - rw [vector_zmod_to_bit_and_dir] - assumption - . rename_i hfin _ _ _ h - rw [ZMod.cast_eq_val] at h - rw [Fin.val_cast_of_lt] at h - apply False.elim (by - have := nat_to_bits_le_some_of_lt hfin - cases this - simp [*] at h - ) - assumption - -end Dir - inductive MerkleTree (F: Type) (H : Hash F 2) : Nat -> Type | leaf : F -> MerkleTree F H 0 | bin : MerkleTree F H depth -> MerkleTree F H depth -> MerkleTree F H (depth+1) @@ -212,214 +11,73 @@ deriving Repr namespace MerkleTree -def eq (a b : Nat) := a == b - def left {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H (Nat.succ depth)) : MerkleTree F H depth := match t with | bin l _ => l def right {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H (Nat.succ depth)) : MerkleTree F H depth := match t with | bin _ r => r --- Return left/right subtree -def tree_for {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H (Nat.succ depth)) (dir : Dir) : MerkleTree F H depth := match dir with -| Dir.left => t.left -| Dir.right => t.right +def treeFor {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H (Nat.succ depth)) (dir : Bool) : MerkleTree F H depth := match dir with +| false => t.left +| true => t.right --- Recursively walk the tree and return the root def root {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) : F := match t with | leaf f => f | bin l r => H vec![root l, root r] -def item_at {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Dir depth) : F := match depth with +def itemAt {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Bool depth) : F := match depth with | Nat.zero => match t with | leaf f => f - | Nat.succ _ => (t.tree_for p.head).item_at p.tail - -def item_at_nat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do - t.item_at <$> Dir.nat_to_dir_vec idx depth + | Nat.succ _ => (t.treeFor p.head).itemAt p.tail -def tree_item_at_fin_dropLast {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): F := - MerkleTree.item_at Tree (Dir.fin_to_dir_vec i).dropLast.reverse +def itemAtFin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): F := + MerkleTree.itemAt Tree i.toBitsBE -def tree_item_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): F := - MerkleTree.item_at Tree (Dir.fin_to_dir_vec i).reverse +instance : GetElem (MerkleTree α H d) Nat α (fun _ i => i < 2^d) where + getElem tree ix inb := tree.itemAtFin ⟨ix, inb⟩ -def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Dir depth) : Vector F depth := match depth with +def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : Vector Bool depth) : Vector F depth := match depth with | Nat.zero => Vector.nil - | Nat.succ _ => Vector.cons (t.tree_for p.head.swap).root ((t.tree_for p.head).proof p.tail) - -def proof_at_nat (t : MerkleTree F H depth) (idx: Nat): Option (Vector F depth) := - t.proof <$> Dir.nat_to_dir_vec idx depth - -def tree_proof_at_fin_dropLast {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^(d+1))): Vector F d := - MerkleTree.proof Tree (Dir.fin_to_dir_vec i).dropLast.reverse - -def tree_proof_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): Vector F d := - MerkleTree.proof Tree (Dir.fin_to_dir_vec i).reverse + | Nat.succ _ => Vector.cons (t.treeFor !p.head).root ((t.treeFor p.head).proof p.tail) -lemma proof_at_nat_to_fin {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): - MerkleTree.proof_at_nat t idx = some (MerkleTree.tree_proof_at_fin t idx) := by - simp [MerkleTree.proof_at_nat, MerkleTree.tree_proof_at_fin] - simp [Dir.nat_to_dir_vec, Dir.fin_to_dir_vec] - simp [fin_to_bits_le_is_some h] +def proofAtFin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): Vector F d := + MerkleTree.proof Tree i.toBitsBE -lemma proof_at_nat_to_fin_some {depth : Nat} {F: Type} {H: Hash F 2} {a : Vector F depth} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): - MerkleTree.proof_at_nat t idx = some a ↔ - MerkleTree.tree_proof_at_fin t idx = a := by - rw [proof_at_nat_to_fin (h := h)] - . simp - -def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with +def recover {depth : Nat} {F: Type} (H : Hash F 2) (ix : Vector Bool depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item | Nat.succ _ => let pitem := proof.head let recover' := recover H ix.tail proof.tail item match ix.head with - | Dir.left => H vec![recover', pitem] - | Dir.right => H vec![pitem, recover'] - -theorem equal_recover_equal_tree {depth : Nat} {F: Type} (H : Hash F 2) - (ix : Vector Dir depth) (proof : Vector F depth) (item₁ : F) (item₂ : F) - [Fact (perfect_hash H)] - : - (recover H ix proof item₁ = recover H ix proof item₂) ↔ (item₁ = item₂) := by - apply Iff.intro - case mp => - induction depth with - | zero => - intro h - unfold recover at h - assumption - | succ _ ih => - intro h - unfold recover at h - split at h <;> { - simp at h - have := congrArg Vector.head h - have := congrArg (Vector.head ∘ Vector.tail) h - apply ih - assumption - } - case mpr => - intro h - rw [h] - -def recover_tail {depth : Nat} {F: Type} (H: Hash F 2) (ix : Vector Dir depth) (proof : Vector F depth) (item : F) : F := match depth with - | Nat.zero => item - | Nat.succ _ => - let pitem := proof.head - let next := match ix.head with - | Dir.left => H vec![item, pitem] - | Dir.right => H vec![pitem, item] - recover_tail H ix.tail proof.tail next - -lemma recover_tail_snoc - {depth F} - (H: Hash F 2) - (ix : Vector Dir depth) - (dir : Dir) - (proof : Vector F depth) - (pitem : F) - (item : F): - recover_tail H (ix.snoc dir) (proof.snoc pitem) item = match dir with - | Dir.left => H vec![recover_tail H ix proof item, pitem] - | Dir.right => H vec![pitem, recover_tail H ix proof item] := by - induction depth generalizing dir pitem item with - | zero => simp [Vector.eq_nil, recover_tail] - | succ _ ih => - conv => - lhs - rw [recover_tail, Vector.head_snoc, Vector.head_snoc, Vector.tail_snoc, Vector.tail_snoc, ih] - -theorem recover_tail_reverse_equals_recover - {F depth} - (H : Hash F 2) - (ix : Vector Dir depth) - (proof : Vector F depth) - (item : F) : - recover_tail H ix.reverse proof.reverse item = recover H ix proof item := by - induction depth with - | zero => rfl - | succ _ ih => - rw [←ix.cons_head_tail, - ←proof.cons_head_tail, - Vector.reverse_cons, - Vector.reverse_cons, - recover_tail_snoc] + | false => H vec![recover', pitem] + | true => H vec![pitem, recover'] + +lemma recover_snoc {H : Hash α 2} {item : α} {ps : Vector Bool n} {p : Bool} {ss : Vector α n} {s : α}: + recover H (ps.snoc p) (ss.snoc s) item = recover H ps ss ( + match p with + | false => H vec![item, s] + | true => H vec![s, item] + ) := by + induction ps, ss using Vector.inductionOn₂ generalizing item s with + | nil => rfl + | @cons n p s ps ss ih => unfold recover - split <;> simp [*] + cases p <;> simp [*] -theorem recover_tail_equals_recover_reverse - {F depth} - (H : Hash F 2) - (ix : Vector Dir depth) - (proof : Vector F depth) - (item : F) : - recover_tail H ix proof item = recover H ix.reverse proof.reverse item := by - have : ix = ix.reverse.reverse:= by simp - rw [this] - have : proof = proof.reverse.reverse := by simp - rw [this] - rw [recover_tail_reverse_equals_recover] - simp +def recoverAtFin {depth : Nat} {F: Type} (H : Hash F 2) (ix : Fin (2^depth)) (proof : Vector F depth) (item : F) : F := + recover H ix.toBitsBE proof item -theorem recover_proof_is_root - {F depth} - (H : Hash F 2) - (ix : Vector Dir depth) - (tree : MerkleTree F H depth): - recover H ix (tree.proof ix) (tree.item_at ix) = tree.root := by - induction depth with - | zero => - cases tree - simp [recover, proof, item_at, root] - | succ _ ih => - cases tree; rename_i l r - simp [recover] - split <;> ( - unfold root - congr <;> simp [*, proof, tree_for, left, right, Dir.swap, item_at, ih] - ) - -def set { depth : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Dir depth) (item : F) : MerkleTree F H depth := match depth with +def set { depth : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Bool depth) (item : F) : MerkleTree F H depth := match depth with | Nat.zero => leaf item | Nat.succ _ => match ix.head with - | Dir.left => bin (set tree.left ix.tail item) tree.right - | Dir.right => bin tree.left (set tree.right ix.tail item) - -def set_at_nat(t : MerkleTree F H depth) (idx: Nat) (newVal: F): Option (MerkleTree F H depth) := - (t.set · newVal) <$> Dir.nat_to_dir_vec idx depth - -def tree_set_at_fin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)) (Item : F): MerkleTree F H d := - MerkleTree.set Tree (Dir.fin_to_dir_vec i).reverse Item + | false => bin (set tree.left ix.tail item) tree.right + | true => bin tree.left (set tree.right ix.tail item) -lemma set_at_nat_to_fin {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) (item : F) (h : idx < 2 ^ depth): - MerkleTree.set_at_nat t idx item = some (MerkleTree.tree_set_at_fin t idx item) := by - simp [MerkleTree.set_at_nat, MerkleTree.tree_set_at_fin] - simp [Dir.nat_to_dir_vec] - simp [Dir.fin_to_dir_vec] - simp [fin_to_bits_le_is_some h] +def setAtFin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)) (Item : F): MerkleTree F H d := + MerkleTree.set Tree i.toBitsBE Item -lemma set_at_nat_to_fin_some {depth : Nat} {F: Type} {H: Hash F 2} {a : MerkleTree F H depth} (t : MerkleTree F H depth) (idx : Nat) (item : F) (h : idx < 2 ^ depth): - MerkleTree.set_at_nat t idx item = some a ↔ - MerkleTree.tree_set_at_fin t idx item = a := by - rw [set_at_nat_to_fin (h := h)] - . simp - -lemma item_at_nat_to_fin {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): - MerkleTree.item_at_nat t idx = some (MerkleTree.tree_item_at_fin t idx) := by - simp [MerkleTree.item_at_nat, MerkleTree.tree_item_at_fin] - simp [Dir.nat_to_dir_vec, Dir.fin_to_dir_vec] - simp [fin_to_bits_le_is_some h] - -lemma item_at_nat_to_fin_some {depth : Nat} {F: Type} {H: Hash F 2} {a : F} (t : MerkleTree F H depth) (idx : Nat) (h : idx < 2 ^ depth): - MerkleTree.item_at_nat t idx = some a ↔ - MerkleTree.tree_item_at_fin t idx = a := by - rw [item_at_nat_to_fin (h := h)] - . simp - -theorem item_at_invariant { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix₁ ix₂ : Vector Dir depth} {item₁ : F} {neq : ix₁ ≠ ix₂}: - item_at (set tree ix₁ item₁) ix₂ = item_at tree ix₂ := by +theorem itemAt_set_invariant_of_neq { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix₁ ix₂ : Vector Bool depth} {item₁ : F} {neq : ix₁ ≠ ix₂}: + itemAt (set tree ix₁ item₁) ix₂ = itemAt tree ix₂ := by induction depth with | zero => cases ix₁ using Vector.casesOn @@ -429,283 +87,83 @@ theorem item_at_invariant { depth : Nat } {F: Type} {H : Hash F 2} {tree : Merkl cases ix₁ using Vector.casesOn; rename_i ix₁_hd ix₁_tl cases ix₂ using Vector.casesOn; rename_i ix₂_hd ix₂_tl cases tree; rename_i tree_l tree_r - simp [item_at, set, tree_for, set, left, right] - simp [Vector.vector_eq_cons] at neq + simp [itemAt, set, treeFor, set, left, right] + simp [Vector.eq_cons] at neq cases ix₁_hd <;> { cases ix₂_hd <;> { simp [ih, neq] } } -theorem item_at_nat_invariant {H : Hash α 2} {tree tree': MerkleTree α H depth} { neq : ix₁ ≠ ix₂ }: - set_at_nat tree ix₁ item₁ = some tree' → - item_at_nat tree' ix₂ = item_at_nat tree ix₂ := by - simp [set_at_nat, item_at_nat] - intros; subst_vars - cases h : Dir.nat_to_dir_vec ix₂ depth with - | none => rfl - | some ix => - simp - rw [item_at_invariant] - intro hp - refine (neq ?_) - apply Dir.nat_to_dir_vec_unique <;> assumption - -theorem item_at_fin_invariant {H : Hash α 2} {tree tree': MerkleTree α H depth} { neq : ix₁ ≠ ix₂ } {h₁ : ix₁ < 2 ^ depth} {h₂ : ix₂ < 2 ^ depth}: - MerkleTree.tree_set_at_fin tree ix₁ item₁ = tree' → - MerkleTree.tree_item_at_fin tree' ix₂ = MerkleTree.tree_item_at_fin tree ix₂ := by - rw [<-set_at_nat_to_fin_some (h := h₁)] - rw [<-item_at_nat_to_fin_some (h := h₂)] - rw [<-item_at_nat_to_fin (h := h₂)] - apply MerkleTree.item_at_nat_invariant (neq := neq) +theorem itemAtFin_setAtFin_invariant_of_neq {tree : MerkleTree α H depth} {ix₁ ix₂ : Fin (2 ^ depth)} (hneq : ix₁ ≠ ix₂): + (tree.setAtFin ix₂ item).itemAtFin ix₁ = tree.itemAtFin ix₁ := by + apply itemAt_set_invariant_of_neq + intro h + rw [Fin.toBitsBE_injective, eq_comm] at h + contradiction -theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Dir depth) (new : F) : - (tree.set ix new).item_at ix = new := by +@[simp] +theorem itemAt_set_eq_self { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix : Vector Bool depth} {item : F}: + itemAt (set tree ix item) ix = item := by induction depth with | zero => rfl | succ depth ih => + cases ix using Vector.casesOn cases tree - simp [set] - split <;> simp [item_at, tree_for, left, right, *] + simp [set, itemAt, treeFor, left, right, *] + split <;> simp [ih] -lemma set_implies_item_at { depth : Nat } {F: Type} {H : Hash F 2} {t₁ t₂ : MerkleTree F H depth} {ix : Vector Dir depth} {item : F} : - set t₁ ix item = t₂ → item_at t₂ ix = item := by - intro h - rw [<-h] - apply read_after_insert_sound +@[simp] +theorem itemAtFin_setAtFin_eq_self {F: Type} {H : Hash F 2} {tree : MerkleTree F H d} {ix : Fin (2^d)} {item : F}: + (tree.setAtFin ix item).itemAtFin ix = item := itemAt_set_eq_self -theorem proof_ceritfies_item - {depth : Nat} - {F: Type} - {H: Hash F 2} - [Fact (perfect_hash H)] - (ix : Vector Dir depth) - (tree : MerkleTree F H depth) - (proof : Vector F depth) - (item : F) - : - recover H ix proof item = tree.root → tree.item_at ix = item := by - intro h +@[simp] +theorem recover_eq_root_iff_proof_and_item_correct { depth : Nat } {F: Type} {H : Hash F 2} [Fact (CollisionResistant H)] {tree : MerkleTree F H depth} {ix : Vector Bool depth} {proof : Vector F depth} {item : F}: + recover H ix proof item = tree.root ↔ proof = tree.proof ix ∧ item = tree.itemAt ix := by induction depth with | zero => cases tree - simp [recover, root] at h - simp [item_at] - rw [h] - | succ depth ih => + cases ix using Vector.casesOn + cases proof using Vector.casesOn + simp [recover, root, itemAt] + | succ n ih => cases tree - simp [item_at, tree_for, left, right] - split <;> { - simp [recover, root, *, Vector.eq_cons_iff] at h - cases h - apply ih (proof := proof.tail) - assumption + cases proof using Vector.casesOn + cases ix using Vector.casesOn; rename_i hix _ + cases hix <;> { + simp [recover, proof, root, treeFor, left, right, ih, Vector.eq_cons_iff] + tauto } -theorem proof_insert_invariant - {depth : Nat} - {F: Type} - {H: Hash F 2} - [Fact (perfect_hash H)] - (ix : Vector Dir depth) - (tree : MerkleTree F H depth) - (old new : F) - (proof : Vector F depth) - : - recover H ix proof old = tree.root → recover H ix proof new = (tree.set ix new).root := by - intro h +@[simp] +theorem recoverAtFin_eq_root_iff_proof_and_item_correct {F: Type} {H : Hash F 2} [Fact (CollisionResistant H)] {tree : MerkleTree F H d} {ix : Fin (2^d)} {proof : Vector F d} {item : F}: + recoverAtFin H ix proof item = tree.root ↔ proof = tree.proofAtFin ix ∧ item = tree.itemAtFin ix := by + simp [recoverAtFin, proofAtFin, itemAtFin] + +@[simp] +theorem proof_set_eq_proof { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix : Vector Bool depth} {item : F}: + (set tree ix item).proof ix = tree.proof ix := by induction depth with | zero => rfl - | succ _ ih => - cases tree - simp [set] - split <;> { - simp [root, recover, *, Vector.eq_cons_iff] at h - simp [left, right, root, recover, *] - congr - apply ih - simp [*] - } - -theorem recover_proof_reversible {H : Hash α 2} [Fact (perfect_hash H)] {Tree : MerkleTree α H d} {Proof : Vector α d}: - recover H Index Proof Item = Tree.root → - Tree.proof Index = Proof := by - induction d with - | zero => - cases Proof using Vector.casesOn - simp [proof] - | succ d ih => - cases Proof using Vector.casesOn - cases Index using Vector.casesOn - cases Tree - simp [root, recover, proof] - intro h - split at h <;> { - have : perfect_hash H := (inferInstance : Fact (perfect_hash H)).out - have := this h - rw [Vector.vector_eq_cons, Vector.vector_eq_cons] at this - casesm* (_ ∧ _) - subst_vars - simp [tree_for, Dir.swap, left, right] - congr - apply ih - assumption + | succ depth ih => + cases ix using Vector.casesOn; rename_i hix _ + cases hix <;> { + simp [set, proof, treeFor, left, right, root, ih] } -theorem recover_equivalence - {F depth} - (H : Hash F 2) - [Fact (perfect_hash H)] - (tree : MerkleTree F H depth) - (Path : Vector Dir depth) - (Proof : Vector F depth) - (Item : F) : - (item_at tree Path = Item ∧ proof tree Path = Proof) ↔ - recover H Path Proof Item = tree.root := by - apply Iff.intro - . intros - casesm* (_ ∧ _) - rename_i hitem_at hproof - rw [<-hitem_at] - rw [<-hproof] - apply recover_proof_is_root - . intros - apply And.intro - . apply proof_ceritfies_item (proof := Proof) - assumption - . apply recover_proof_reversible (Item := Item) - assumption - -theorem eq_root_eq_tree {H} [ph: Fact (perfect_hash H)] {t₁ t₂ : MerkleTree α H d}: - t₁.root = t₂.root ↔ t₁ = t₂ := by - induction d with - | zero => cases t₁; cases t₂; tauto - | succ _ ih => - cases t₁ - cases t₂ - apply Iff.intro - . intro h - have h := Fact.elim ph h - injection h with h - injection h with _ h - injection h - congr <;> {rw [←ih]; assumption} - . intro h - injection h - subst_vars - rfl - -lemma proof_of_set_is_proof - {F d} - (H : Hash F 2) - [Fact (perfect_hash H)] - (Tree : MerkleTree F H d) - (ix : Vector Dir d) - (item : F): - (MerkleTree.proof (MerkleTree.set Tree ix item) ix) = MerkleTree.proof Tree ix := by - induction d with - | zero => - simp [MerkleTree.set, MerkleTree.proof] - | succ d ih => - cases Tree - simp [MerkleTree.set, MerkleTree.proof, MerkleTree.tree_for] - split - . rename_i hdir - have : Dir.swap (Dir.swap (Vector.head ix)) = Dir.right := by - rw [hdir] - simp [Dir.swap] - have : Vector.head ix = Dir.right := by - rw [<-this] - simp [Dir.swap] - cases ix.head - . simp - . simp - rw [this] - simp [MerkleTree.set, MerkleTree.left, MerkleTree.right] - simp [Vector.vector_eq_cons] - rw [ih] - . rename_i hdir - have : Dir.swap (Dir.swap (Vector.head ix)) = Dir.left := by - rw [hdir] - simp [Dir.swap] - have : Vector.head ix = Dir.left := by - rw [<-this] - simp [Dir.swap] - cases ix.head - . simp - . simp - rw [this] - simp [MerkleTree.set, MerkleTree.left, MerkleTree.right] - simp [Vector.vector_eq_cons] - rw [ih] - -lemma proof_of_set_fin - {F d} - (H : Hash F 2) - [Fact (perfect_hash H)] - (Tree : MerkleTree F H d) - (ix : Fin (2^d)) - (item : F): - (tree_proof_at_fin (tree_set_at_fin Tree ix item) ix) = tree_proof_at_fin Tree ix := by - simp [tree_proof_at_fin, tree_set_at_fin] - simp [proof_of_set_is_proof] - -def multi_set { depth b : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (path : Vector (Vector Dir depth) b) (item : F) : MerkleTree F H depth := - match b with - | Nat.zero => tree - | Nat.succ _ => multi_set (tree.set path.head item) path.tail item +@[simp] +theorem proofAtFin_setAtFin_eq_proof {F: Type} {H : Hash F 2} {tree : MerkleTree F H d} {ix : Fin (2^d)} {item : F}: + (tree.setAtFin ix item).proofAtFin ix = tree.proofAtFin ix := proof_set_eq_proof -lemma tree_set_comm { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p₁ p₂ : Vector Dir depth} {item : F}: - MerkleTree.set (MerkleTree.set tree p₁ item) p₂ item = MerkleTree.set (MerkleTree.set tree p₂ item) p₁ item := by +theorem root_set_eq_recover { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix : Vector Bool depth} {item : F}: + (set tree ix item).root = recover H ix (tree.proof ix) item := by induction depth with | zero => rfl - | succ d ih => cases tree with | bin l r => - cases p₁ using Vector.casesOn with | cons p₁h p₁t => - cases p₂ using Vector.casesOn with | cons p₂h p₂t => - cases p₁h <;> { - cases p₂h <;> { simp [MerkleTree.set, MerkleTree.left, MerkleTree.right]; try rw [ih] } + | succ depth ih => + cases tree + cases ix using Vector.casesOn; rename_i hix _ + cases hix <;> { + simp [set, proof, treeFor, left, right, root, ih, recover] } -lemma multi_set_set { depth b : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p : Vector Dir depth} {path : Vector (Vector Dir depth) b} {item : F}: - multi_set (MerkleTree.set tree p item) path item = MerkleTree.set (multi_set tree path item) p item := by - induction path using Vector.inductionOn generalizing tree p with - | h_nil => rfl - | h_cons ih => simp [multi_set, ih, tree_set_comm] - -def multi_item_at { depth b : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (path : Vector (Vector Dir depth) b) (item : F) : Prop := - match b with - | Nat.zero => true - | Nat.succ _ => tree.item_at path.head = item ∧ multi_item_at tree path.tail item - -theorem multi_set_is_item_at { depth b : Nat } {F: Type} {H : Hash F 2} {initialTree finalTree: MerkleTree F H depth} {path : Vector (Vector Dir depth) b} {item : F} : - (multi_set initialTree path item = finalTree → - multi_item_at finalTree path item) := by - induction path using Vector.inductionOn generalizing initialTree finalTree with - | h_nil => - simp [multi_set, multi_item_at] - | @h_cons b' x xs ih => - unfold multi_set - unfold multi_item_at - simp only [Vector.tail_cons, Vector.head_cons] - intro h - refine ⟨?_, ?_⟩ - . rw [←h, multi_set_set, MerkleTree.read_after_insert_sound] - . apply ih h - -theorem multi_set_is_item_at_all_item { depth b i : Nat } {range : i ∈ [0:b]} {F: Type} {H : Hash F 2} - {initialTree finalTree: MerkleTree F H depth} {path : Vector (Vector Dir depth) b} {item : F} : - multi_set initialTree path item = finalTree → - MerkleTree.item_at finalTree (path[i]'(by rcases range; tauto)) = item := by - intro hp - induction path using Vector.inductionOn generalizing i initialTree finalTree with - | h_nil => - rcases range with ⟨lo, hi⟩ - have := Nat.ne_of_lt (Nat.lt_of_le_of_lt lo hi) - contradiction - | @h_cons b' x xs ih => - rcases range with ⟨lo, hi⟩ - cases lo with - | refl => - have hitem_at : multi_item_at finalTree (x ::ᵥ xs) item := multi_set_is_item_at hp - unfold multi_item_at at hitem_at - tauto - | @step i h => - exact ih (by assumption) (range := ⟨zero_le _, Nat.lt_of_succ_lt_succ hi⟩) +theorem root_setAtFin_eq_recoverAtFin {F: Type} {H : Hash F 2} {tree : MerkleTree F H d} {ix : Fin (2^d)} {item : F}: + (tree.setAtFin ix item).root = recoverAtFin H ix (tree.proofAtFin ix) item := by + simp [root_set_eq_recover, recoverAtFin, proofAtFin, setAtFin] end MerkleTree diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean deleted file mode 100644 index 52eea7f..0000000 --- a/ProvenZk/Misc.lean +++ /dev/null @@ -1,96 +0,0 @@ -import ProvenZk.Gates -import ProvenZk.Binary - -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 ∧ - ( (out = 1 ∧ (a = 1 ∨ b = 1) ∨ - (out = 0 ∧ a = 0 ∧ b = 0)))) := by - unfold Gates.or - unfold Gates.is_bool - simp - intro ha hb - cases ha <;> cases hb <;> { subst_vars; simp } - -lemma select_rw {b i1 i2 out : (ZMod N)} : (Gates.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with - | Bit.zero => out = i2 - | Bit.one => out = i1 := by - unfold Gates.select - unfold Gates.is_bool - apply Iff.intro <;> { - intro h; rcases h with ⟨is_b, _⟩ - refine ⟨is_b, ?_⟩ - cases is_b - case inl => { - simp [*, zmod_to_bit] at * - assumption - } - case inr => { - simp [*, zmod_to_bit] at * - have : Nat.Prime N := (inferInstance : Fact (Nat.Prime N)).elim - have : N > 1 := by - apply Nat.Prime.one_lt - assumption - cases N - case zero => simp [ZMod.val] at * - case succ n _ _ _ _=> { - cases n - case zero => simp [ZMod.val] at * - case succ => { - simp [ZMod.val] at * - assumption - } - } - } - } - -@[simp] -theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by rfl - -@[simp] -theorem select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by - simp [Gates.select] - -@[simp] -theorem select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by - simp [Gates.select] - -@[simp] -theorem or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by - simp [Gates.or] - -@[simp] -theorem zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by - simp [Gates.or] - -@[simp] -theorem one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by - simp [Gates.or] - -@[simp] -theorem or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by - simp [Gates.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] - tauto - -lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by - simp - tauto - -lemma and_iff (P Q R : Prop): (Q ↔ R) → (P ∧ Q ↔ P ∧ R) := by - tauto - -lemma ex_iff {P Q : α → Prop}: (∀x, P x ↔ Q x) → ((∃x, P x) ↔ ∃x, Q x) := by - intro h; - apply Iff.intro <;> { - intro h1 - cases h1; rename_i witness prop - exists witness - try { rw [h witness]; assumption } - try { rw [←h witness]; assumption } - } diff --git a/ProvenZk/Subvector.lean b/ProvenZk/Subvector.lean deleted file mode 100644 index dbe73b4..0000000 --- a/ProvenZk/Subvector.lean +++ /dev/null @@ -1,61 +0,0 @@ -import ProvenZk.Ext.Vector - -abbrev SubVector α n prop := Subtype (α := Vector α n) (Vector.allIxes prop) - -namespace SubVector - -def nil : SubVector α 0 prop := ⟨Vector.nil, by simp⟩ - -def snoc (vs: SubVector α n prop) (v : Subtype prop): SubVector α n.succ prop := - ⟨vs.val.snoc v.val, by - intro i - cases i using Fin.lastCases with - | last => simp [GetElem.getElem, Fin.last_def, Subtype.property] - | cast i => - have := vs.prop i - simp at this - simp [*] - ⟩ - -@[elab_as_elim] -def revCases {C : ∀ {n:Nat}, SubVector α n prop → Sort _} (v : SubVector α n prop) - (nil : C nil) - (snoc : ∀ {n : Nat} (vs : SubVector α n prop) (v : Subtype prop), C (vs.snoc v)): C v := by - rcases v with ⟨v, h⟩ - cases v using Vector.revCasesOn with - | nil => exact nil - | snoc vs v => - refine snoc ⟨vs, ?vsp⟩ ⟨v, ?vp⟩ - case vsp => - intro i - have := h i.castSucc - simp at this - simp [this] - case vp => - have := h (Fin.last _) - simp [GetElem.getElem, Fin.last_def] at this - exact this - -instance : GetElem (SubVector α n prop) (Fin n) (Subtype prop) (fun _ _ => True) where - getElem v i _ := ⟨v.val.get i, v.prop i⟩ - -def lower (v: SubVector α n prop): Vector {v : α // prop v} n := - Vector.ofFn fun i => v[i] - -def lift {prop : α → Prop} (v : Vector (Subtype prop) n): SubVector α n prop := - ⟨v.map Subtype.val, by - intro i - simp [GetElem.getElem, Subtype.property]⟩ - -theorem snoc_lower {vs : SubVector α n prop} {v : Subtype prop}: - (vs.snoc v).lower = vs.lower.snoc v := by - unfold lower - rw [Vector.ofFn_snoc'] - congr - . funext i - cases n with - | zero => cases i using finZeroElim - | _ => simp [GetElem.getElem, snoc] - . simp [GetElem.getElem, snoc, Fin.nat_cast_last] - -end SubVector diff --git a/ProvenZk/UniqueAssignment.lean b/ProvenZk/UniqueAssignment.lean new file mode 100644 index 0000000..5ddcf41 --- /dev/null +++ b/ProvenZk/UniqueAssignment.lean @@ -0,0 +1,18 @@ + +structure UniqueAssignment (f : (β → Prop) → Prop) (emb : α → β) where + val : α + equiv : ∀k, f k = k (emb val) + +namespace UniqueAssignment + +def constant (x : α) (emb : α → β): UniqueAssignment (fun k => k (emb x)) emb := ⟨x, fun _ => rfl⟩ + +def constant' (x : α) (y : β) (emb : α → β) (hp : y = emb x): UniqueAssignment (fun k => k y) emb := ⟨x, fun k => congrArg k hp⟩ + +def compose { f: (β → Prop) → Prop } {g : β → (γ → Prop) → Prop} + (f_constant : UniqueAssignment f embf) (g_constant : ∀c, UniqueAssignment (g (embf c)) embg): + UniqueAssignment (fun k => f (λx ↦ g x k)) embg := UniqueAssignment.mk + (g_constant f_constant.val).val + (fun _ => Eq.trans (f_constant.equiv _) ((g_constant _).equiv _)) + +end UniqueAssignment