From ae9327ec14d84b20f1c17f336ed7698e5b0fbae1 Mon Sep 17 00:00:00 2001 From: Marcin Kostrzewa Date: Sun, 28 Jan 2024 17:59:20 +0100 Subject: [PATCH] Clean up binary representations and merkle trees (#22) --- ProvenZk.lean | 5 +- ProvenZk/Binary.lean | 825 ++++++++++----------------------- ProvenZk/Ext/GetElem.lean | 52 +++ ProvenZk/Ext/Vector/Basic.lean | 220 ++++----- ProvenZk/Gates.lean | 11 +- ProvenZk/Lemmas.lean | 175 +++++++ ProvenZk/Merkle.lean | 722 ++++------------------------- ProvenZk/Misc.lean | 96 ---- ProvenZk/Subvector.lean | 61 --- ProvenZk/UniqueAssignment.lean | 18 + 10 files changed, 688 insertions(+), 1497 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 068eaef..f267cef 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -1,68 +1,13 @@ 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 @@ -73,578 +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 => - simp - 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 [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] - -@[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/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 71a9022..949fe98 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -1,4 +1,5 @@ import Mathlib.Data.Vector.Snoc +import Mathlib.Data.Vector.Mem import Mathlib.Data.Matrix.Basic import Mathlib.Data.List.Defs @@ -108,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 @@ -124,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 @@ -167,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 @@ -190,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 => @@ -228,16 +224,16 @@ lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = v | 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 +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 @@ -251,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 → α) : @@ -333,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 - . 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] + . 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 + . 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/Gates.lean b/ProvenZk/Gates.lean index c1181a6..e944ac4 100644 --- a/ProvenZk/Gates.lean +++ b/ProvenZk/Gates.lean @@ -2,18 +2,19 @@ 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/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 3b73cd4..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 (CollisionResistant 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 (CollisionResistant 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 (CollisionResistant 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 (CollisionResistant 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 : CollisionResistant H := (inferInstance : Fact (CollisionResistant 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 (CollisionResistant 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 (CollisionResistant 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 (CollisionResistant 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 (CollisionResistant 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 522f59d..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 - | 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 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