From 89c7fd165328a58bbf365d14cd274b623bd2f31e Mon Sep 17 00:00:00 2001 From: Marcin Kostrzewa Date: Thu, 11 Jan 2024 17:55:30 +0100 Subject: [PATCH 1/5] progress --- ProvenZk.lean | 1 + ProvenZk/Ext/GetElem.lean | 43 +++++++++++ ProvenZk/Merkle.lean | 153 ++++++++++++++++++++++---------------- 3 files changed, 131 insertions(+), 66 deletions(-) create mode 100644 ProvenZk/Ext/GetElem.lean diff --git a/ProvenZk.lean b/ProvenZk.lean index ac31cd2..e8c7bc1 100644 --- a/ProvenZk.lean +++ b/ProvenZk.lean @@ -2,6 +2,7 @@ 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 diff --git a/ProvenZk/Ext/GetElem.lean b/ProvenZk/Ext/GetElem.lean new file mode 100644 index 0000000..56a0fac --- /dev/null +++ b/ProvenZk/Ext/GetElem.lean @@ -0,0 +1,43 @@ +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?_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/Merkle.lean b/ProvenZk/Merkle.lean index 3b73cd4..5a447fe 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -133,6 +133,22 @@ lemma dropLastOrder {d n : Nat} {out : Vector (ZMod n) d} : Dir.create_dir_vec ( 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 contra_of_eq_false : x = False.elim h → False := fun _ => h + +lemma fin_to_dir_vec_injective {depth : ℕ} : Function.Injective (fin_to_dir_vec (depth := depth)) := by + intro a b h + rw [fin_to_dir_vec, fin_to_dir_vec, Vector.vector_map_inj (f_inj := by intro a b; cases a <;> {cases b <;> tauto}), fin_to_bits_le, fin_to_bits_le] at h + split at h + . split at h + . rw [←recover_binary_nat_to_bits_le] at * + apply Fin.eq_of_veq + apply eq_comm.mp + simp [*] at * + assumption + . exfalso; apply contra_of_eq_false h + . exfalso; rw [eq_comm] at h; apply contra_of_eq_false h + + 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] @@ -212,41 +228,37 @@ 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 +def treeFor {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 --- 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 Dir depth) : F := match depth with | Nat.zero => match t with | leaf f => f - | Nat.succ _ => (t.tree_for p.head).item_at p.tail + | Nat.succ _ => (t.treeFor p.head).itemAt 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 +def itemAtNat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do + t.itemAt <$> Dir.nat_to_dir_vec idx depth -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 (Dir.fin_to_dir_vec i).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 +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 | Nat.zero => Vector.nil - | Nat.succ _ => Vector.cons (t.tree_for p.head.swap).root ((t.tree_for p.head).proof p.tail) + | Nat.succ _ => Vector.cons (t.treeFor p.head.swap).root ((t.treeFor 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 @@ -254,18 +266,18 @@ def proof_at_nat (t : MerkleTree F H depth) (idx: Nat): Option (Vector F 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 := +def proofAtFin {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] + MerkleTree.proof_at_nat t idx = some (MerkleTree.proofAtFin t idx) := by + simp [MerkleTree.proof_at_nat, MerkleTree.proofAtFin] 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 + MerkleTree.proofAtFin t idx = a := by rw [proof_at_nat_to_fin (h := h)] . simp @@ -368,17 +380,17 @@ theorem recover_proof_is_root (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 + recover H ix (tree.proof ix) (tree.itemAt ix) = tree.root := by induction depth with | zero => cases tree - simp [recover, proof, item_at, root] + simp [recover, proof, itemAt, 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] + congr <;> simp [*, proof, treeFor, left, right, Dir.swap, itemAt, 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 @@ -390,36 +402,36 @@ 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 := +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 (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] + MerkleTree.set_at_nat t idx item = some (MerkleTree.setAtFin t idx item) := by + simp [MerkleTree.set_at_nat, MerkleTree.setAtFin] 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 + MerkleTree.setAtFin 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] + MerkleTree.itemAtNat t idx = some (MerkleTree.itemAtFin t idx) := by + simp [MerkleTree.itemAtNat, MerkleTree.itemAtFin] 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 + MerkleTree.itemAtNat t idx = some a ↔ + MerkleTree.itemAtFin 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 Dir 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,43 +441,52 @@ 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 [itemAt, set, treeFor, set, left, right] simp [Vector.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 item_at_nat_invariant {H : Hash α 2} {tree tree': MerkleTree α H depth} { neq : ix₁ ≠ ix₂ }: +-- set_at_nat tree ix₁ item₁ = some tree' → +-- itemAtNat tree' ix₂ = itemAtNat tree ix₂ := by +-- simp [set_at_nat, itemAtNat] +-- 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.setAtFin tree ix₁ item₁ = tree' → +-- MerkleTree.itemAtFin tree' ix₂ = MerkleTree.itemAtFin 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 getElem_setAtFin_invariant_of_neq {tree : MerkleTree α H depth} {ix₁ : Nat} {hix₁ : ix₁ < 2 ^ depth} {ix₂ : Fin (2 ^ depth)} (hneq : ix₁ ≠ ix₂.val): + (tree.setAtFin ix₂ item)[ix₁]'hix₁ = tree[ix₁]'hix₁ := by + unfold setAtFin + simp [setAtFin, getElem, itemAtFin] + apply itemAt_set_invariant_of_neq + intro h + rw [Vector.vector_reverse_inj, Dir.fin_to_dir_vec_injective.eq_iff, eq_comm] at h + exact hneq (congrArg Fin.val h) 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 + (tree.set ix new).itemAt ix = new := by induction depth with | zero => rfl | succ depth ih => cases tree simp [set] - split <;> simp [item_at, tree_for, left, right, *] + split <;> simp [itemAt, treeFor, 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 + set t₁ ix item = t₂ → itemAt t₂ ix = item := by intro h rw [<-h] apply read_after_insert_sound @@ -480,17 +501,17 @@ theorem proof_ceritfies_item (proof : Vector F depth) (item : F) : - recover H ix proof item = tree.root → tree.item_at ix = item := by + recover H ix proof item = tree.root → tree.itemAt ix = item := by intro h induction depth with | zero => cases tree simp [recover, root] at h - simp [item_at] + simp [itemAt] rw [h] | succ depth ih => cases tree - simp [item_at, tree_for, left, right] + simp [itemAt, treeFor, left, right] split <;> { simp [recover, root, *, Vector.eq_cons_iff] at h cases h @@ -542,7 +563,7 @@ theorem recover_proof_reversible {H : Hash α 2} [Fact (CollisionResistant H)] { rw [Vector.vector_eq_cons, Vector.vector_eq_cons] at this casesm* (_ ∧ _) subst_vars - simp [tree_for, Dir.swap, left, right] + simp [treeFor, Dir.swap, left, right] congr apply ih assumption @@ -556,7 +577,7 @@ theorem recover_equivalence (Path : Vector Dir depth) (Proof : Vector F depth) (Item : F) : - (item_at tree Path = Item ∧ proof tree Path = Proof) ↔ + (itemAt tree Path = Item ∧ proof tree Path = Proof) ↔ recover H Path Proof Item = tree.root := by apply Iff.intro . intros @@ -604,7 +625,7 @@ lemma proof_of_set_is_proof simp [MerkleTree.set, MerkleTree.proof] | succ d ih => cases Tree - simp [MerkleTree.set, MerkleTree.proof, MerkleTree.tree_for] + simp [MerkleTree.set, MerkleTree.proof, MerkleTree.treeFor] split . rename_i hdir have : Dir.swap (Dir.swap (Vector.head ix)) = Dir.right := by @@ -642,8 +663,8 @@ lemma proof_of_set_fin (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] + (proofAtFin (setAtFin Tree ix item) ix) = proofAtFin Tree ix := by + simp [proofAtFin, setAtFin] 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 := @@ -671,7 +692,7 @@ lemma multi_set_set { depth b : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTre 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 + | Nat.succ _ => tree.itemAt 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 → @@ -691,7 +712,7 @@ theorem multi_set_is_item_at { depth b : Nat } {F: Type} {H : Hash F 2} {initial 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 + MerkleTree.itemAt finalTree (path[i]'(by rcases range; tauto)) = item := by intro hp induction path using Vector.inductionOn generalizing i initialTree finalTree with | h_nil => From b523809f30a324d60b1ae8f115bea1c27b94eba3 Mon Sep 17 00:00:00 2001 From: Marcin Kostrzewa Date: Thu, 18 Jan 2024 14:09:38 +0100 Subject: [PATCH 2/5] progress --- ProvenZk/Binary.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 068eaef..04de915 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -648,3 +648,22 @@ theorem SubVector_lift_lower : SubVector.lower (SubVector.lift v) = v := by unfold SubVector.lower apply Subtype.eq simp [GetElem.getElem] + +lemma recover_binary_nat_snoc {n : Nat} {v : Vector Bit n} {b : Bit}: + recover_binary_nat (v.snoc b) = recover_binary_nat v + 2^n * b.toNat := by + induction n with + | zero => + cases v using Vector.casesOn + simp [recover_binary_nat] + | succ n ih => + cases v using Vector.casesOn with | cons hd tl => + unfold recover_binary_nat + simp [ih] + rw [Nat.add_assoc, + Nat.add_left_cancel_iff, + Nat.mul_add, + Nat.add_left_cancel_iff, + Nat.mul_left_comm, + ← Nat.mul_assoc, + Nat.pow_succ + ] From 94ae1c5017fcaaa907bbcdbb2680548453487e10 Mon Sep 17 00:00:00 2001 From: Marcin Kostrzewa Date: Sat, 20 Jan 2024 00:13:34 +0100 Subject: [PATCH 3/5] x --- ProvenZk/Binary.lean | 99 ++++++++--------- ProvenZk/Ext/Vector/Basic.lean | 190 +++++++++++++++++++-------------- ProvenZk/Subvector.lean | 36 +++---- 3 files changed, 172 insertions(+), 153 deletions(-) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 04de915..53f2c22 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -1,10 +1,16 @@ import Mathlib.Data.ZMod.Basic import Mathlib.Data.Bitvec.Defs +import Mathlib.Data.Vector.Mem import ProvenZk.Ext.List import ProvenZk.Ext.Vector import ProvenZk.Subvector +open BigOperators + +@[reducible] +def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1 + inductive Bit : Type where | zero : Bit | one : Bit @@ -19,11 +25,11 @@ 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 : Coe Bit Nat where +-- coe := toNat -instance {n} : Coe Bit (ZMod n) where - coe := toZMod +-- instance {n} : Coe Bit (ZMod n) where +-- coe := toZMod instance : OfNat Bit 0 where ofNat := zero @@ -34,6 +40,15 @@ instance : OfNat Bit 1 where instance : Inhabited Bit where default := zero +instance [semiring : Semiring α] : Coe Bit α where + coe b := match b with + | Bit.zero => semiring.zero + | Bit.one => semiring.one + +@[simp] +lemma is_bit_toZMod {N} {b:Bit} : is_bit (toZMod b : ZMod N) := by + cases b <;> simp [is_bit, toZMod] + end Bit def bit_mod_two (inp : Nat) : Bit := match h:inp%2 with @@ -64,9 +79,6 @@ def zmod_to_bit {n} (x : ZMod n) : Bit := match ZMod.val x with | 1 => Bit.one | Nat.succ (Nat.succ _) => panic "Bit can only be 0 or 1" -@[reducible] -def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1 - @[simp] theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto @@ -81,36 +93,35 @@ 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)) +def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop := ∀ a ∈ x, is_bit a + +def recoverBinary [Semiring α] {n} (x : Vector Bit n): α := + ∑i, 2^i.val * ↑(x.get i) + +-- @[simp] +-- theorem is_vector_binary_def : is_vector_binary v ↔ ∀ a ∈ v.toList, is_bit a := by +-- simp [is_vector_binary, Vector.instMembershipVector] @[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 + simp [is_vector_binary] -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 is_vector_binary_snoc {vs : Vector (ZMod (Nat.succ p)) 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 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 @@ -417,28 +428,7 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} : } 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] - 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] - } - . apply ih + is_vector_binary (w.map (Bit.toZMod (n := n))) := by simp [is_vector_binary] 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 → @@ -606,10 +596,9 @@ 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 is_vector_binary_iff_allIxes_is_bit {n : Nat} {v : Vector (ZMod n) d}: Vector.allIxes is_bit v ↔ is_vector_binary v := by +-- rw [Vector.allIxes_iff_allElems] +-- rfl 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 diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 71a9022..59eed0b 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 @@ -251,44 +252,65 @@ 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] +theorem mem_def {xs : Vector α n} {x} : x ∈ xs ↔ x ∈ xs.toList := by rfl + +def allElems (f : α → Prop) : Vector α n → Prop := fun v => ∀(a : α), a ∈ v → f a @[simp] -theorem allIxes_nil : allIxes f Vector.nil := by - simp [allIxes] +theorem allElems_cons : Vector.allElems prop (v ::ᵥ vs) ↔ prop v ∧ allElems prop vs := by + simp [allElems] + +@[simp] +theorem allElems_nil : Vector.allElems prop Vector.nil := by simp [allElems] + +-- def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i] -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 +-- @[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] -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 +-- @[simp] +-- theorem allIxes_nil : allIxes f Vector.nil := by +-- simp [allIxes] -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 getElem_allElems {v : { v: Vector α n // allElems prop v }} {i : Nat} { i_small : i < n}: + v.val[i]'i_small = ↑(Subtype.mk (p := prop) (v.val.get ⟨i, i_small⟩) (by apply v.prop; simp)) := by rfl -theorem allIxes_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes prop) v}} +theorem getElem_allElems₂ {v : { v: Vector (Vector α m) n // allElems (allElems prop) v }} {i j: Nat} { i_small : i < n} { j_small : j < m}: + (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk (p := prop) ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (by apply v.prop; rotate_right; exact v.val.get ⟨i, i_small⟩; all_goals simp)) := by rfl + +theorem allElems_indexed {v : {v : Vector α n // allElems prop v}} {i : Nat} {i_small : i < n}: + prop (v.val[i]'i_small) := by + apply v.prop + simp [getElem] + +theorem allElems_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems 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⟩ + prop ((v.val[i]'i_small)[j]'j_small) := by + apply v.prop (v.val[i]'i_small) <;> simp [getElem] -theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes (allIxes prop)) v}} +theorem allElems_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems (allElems 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⟩ + prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) := by + apply v.prop + rotate_right + . exact (v.val[i]'i_small)[j]'j_small + rotate_right + . exact (v.val[i]'i_small) + all_goals simp [getElem] @[simp] theorem map_ofFn {f : α → β} (g : Fin n → α) : @@ -333,59 +355,71 @@ 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 - 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 +-- 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 + + +-- theorem allIxes_iff_allElems : allIxes prop v ↔ ∀ a ∈ v, prop a := by +-- apply Iff.intro +-- . intro hp a ain +-- have := (Vector.mem_iff_get a v).mp ain +-- rcases this with ⟨i, h⟩ +-- cases h +-- apply hp +-- . intro hp i +-- apply hp +-- apply Vector.get_mem end Vector diff --git a/ProvenZk/Subvector.lean b/ProvenZk/Subvector.lean index 522f59d..d116c01 100644 --- a/ProvenZk/Subvector.lean +++ b/ProvenZk/Subvector.lean @@ -1,20 +1,18 @@ import ProvenZk.Ext.Vector -abbrev SubVector α n prop := Subtype (α := Vector α n) (Vector.allIxes prop) +abbrev SubVector α n prop := Subtype (α := Vector α n) (Vector.allElems prop) namespace SubVector -def nil : SubVector α 0 prop := ⟨Vector.nil, by simp⟩ +def nil : SubVector α 0 prop := ⟨Vector.nil, by simp [Vector.allElems]⟩ 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 [*] + intro a ha + simp at ha + rcases ha with ha | ha + . exact vs.prop a ha + . cases ha; exact v.prop ⟩ @[elab_as_elim] @@ -25,27 +23,25 @@ def revCases {C : ∀ {n:Nat}, SubVector α n prop → Sort _} (v : SubVector α cases v using Vector.revCasesOn with | nil => exact nil | snoc vs v => + simp [Vector.allElems] at h 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 + intro a ha + exact h a (Or.inl ha) + case vp => exact h v (Or.inr rfl) + instance : GetElem (SubVector α n prop) (Fin n) (Subtype prop) (fun _ _ => True) where - getElem v i _ := ⟨v.val.get i, v.prop i⟩ + getElem v i _ := ⟨v.val.get i, by apply v.prop; simp⟩ 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]⟩ + intro a ha + simp at ha + tauto⟩ theorem snoc_lower {vs : SubVector α n prop} {v : Subtype prop}: (vs.snoc v).lower = vs.lower.snoc v := by From 0431a2d711af626f35e2e1d279b8db647d495661 Mon Sep 17 00:00:00 2001 From: Marcin Kostrzewa Date: Fri, 26 Jan 2024 11:34:37 +0100 Subject: [PATCH 4/5] . --- ProvenZk.lean | 4 +- ProvenZk/Binary.lean | 784 +++++++++------------------------ ProvenZk/Ext/Vector/Basic.lean | 199 +++++---- ProvenZk/Gates.lean | 12 +- ProvenZk/Lemmas.lean | 144 ++++++ ProvenZk/Merkle.lean | 662 +++++++++------------------- ProvenZk/Misc.lean | 96 ---- ProvenZk/Subvector.lean | 57 --- ProvenZk/UniqueAssignment.lean | 18 + 9 files changed, 705 insertions(+), 1271 deletions(-) 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 e8c7bc1..64dad76 100644 --- a/ProvenZk.lean +++ b/ProvenZk.lean @@ -8,5 +8,5 @@ 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 53f2c22..8e23293 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -1,107 +1,50 @@ 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 open BigOperators @[reducible] def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1 -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 +@[simp] +theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto -instance : OfNat Bit 1 where - ofNat := one +@[simp] +theorem is_bit_one : is_bit (1 : ZMod n) := by tauto -instance : Inhabited Bit where - default := zero +def Bool.toZMod {N} (b : Bool) : ZMod N := b.toNat -instance [semiring : Semiring α] : Coe Bit α where - coe b := match b with - | Bit.zero => semiring.zero - | Bit.one => semiring.one +def Bool.ofZMod {N} (b : ZMod N) : Bool := Bool.ofNat b.val @[simp] -lemma is_bit_toZMod {N} {b:Bit} : is_bit (toZMod b : ZMod N) := by - cases b <;> simp [is_bit, toZMod] - -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" +lemma Bool.toZMod_zero {N} : Bool.toZMod false = (0 : ZMod N) := by + simp [Bool.toZMod, Bool.toNat] @[simp] -theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto +lemma Bool.toZMod_one {N} : Bool.toZMod true = (1 : ZMod N) := by + simp [Bool.toZMod, Bool.toNat] @[simp] -theorem is_bit_one : is_bit (1 : ZMod n) := by tauto +lemma Bool.toZMod_is_bit {N} : is_bit (toZMod (N:=N) b) := by + cases b <;> simp [is_bit, toZMod, toNat] -abbrev bOne : {v : ZMod n // is_bit v} := ⟨1, by simp⟩ - -abbrev bZero : {v : ZMod n // is_bit v} := ⟨0, by 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] -def embedBit {n : Nat} : Bit → {x : (ZMod n) // is_bit x} -| Bit.zero => bZero -| Bit.one => bOne +@[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 := ∀ a ∈ x, is_bit a -def recoverBinary [Semiring α] {n} (x : Vector Bit n): α := - ∑i, 2^i.val * ↑(x.get i) - --- @[simp] --- theorem is_vector_binary_def : is_vector_binary v ↔ ∀ a ∈ v.toList, is_bit a := by --- simp [is_vector_binary, Vector.instMembershipVector] - @[simp] lemma is_vector_binary_reverse {depth} (ix : Vector (ZMod n) depth): is_vector_binary ix.reverse ↔ is_vector_binary ix := by @@ -111,7 +54,7 @@ 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 simp [is_vector_binary] -lemma is_vector_binary_snoc {vs : Vector (ZMod (Nat.succ p)) n} {v}: is_vector_binary (vs.snoc v) ↔ is_vector_binary vs ∧ is_bit v := by +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 @@ -123,536 +66,217 @@ lemma is_vector_binary_snoc {vs : Vector (ZMod (Nat.succ p)) n} {v}: is_vector_b . apply hl; assumption . subst_vars; assumption -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 - -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 +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_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 + . rintro ⟨_⟩ + apply And.intro + . cases msb' <;> { + simp [msb, Bool.toNat] + } + . 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] -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 simp [is_vector_binary] - -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 +@[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 -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 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 -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 - } - ) +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_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 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] -@[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 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 --- rw [Vector.allIxes_iff_allElems] --- rfl - -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 recover_binary_nat_snoc {n : Nat} {v : Vector Bit n} {b : Bit}: - recover_binary_nat (v.snoc b) = recover_binary_nat v + 2^n * b.toNat := by - induction n with - | zero => - cases v using Vector.casesOn - simp [recover_binary_nat] - | succ n ih => +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 => - unfold recover_binary_nat - simp [ih] - rw [Nat.add_assoc, - Nat.add_left_cancel_iff, - Nat.mul_add, - Nat.add_left_cancel_iff, - Nat.mul_left_comm, - ← Nat.mul_assoc, - Nat.pow_succ - ] + simp [recover_binary_zmod', Fin.ofBitsLE, Fin.ofBitsBE_snoc, ih] + rfl diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index 59eed0b..c43de7c 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -109,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 @@ -125,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 @@ -168,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 @@ -191,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 => @@ -229,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 @@ -257,14 +252,14 @@ instance : Membership α (Vector α n) := ⟨fun x xs => x ∈ xs.toList⟩ @[simp] theorem mem_def {xs : Vector α n} {x} : x ∈ xs ↔ x ∈ xs.toList := by rfl -def allElems (f : α → Prop) : Vector α n → Prop := fun v => ∀(a : α), a ∈ v → f a +-- def allElems (f : α → Prop) : Vector α n → Prop := fun v => ∀(a : α), a ∈ v → f a -@[simp] -theorem allElems_cons : Vector.allElems prop (v ::ᵥ vs) ↔ prop v ∧ allElems prop vs := by - simp [allElems] +-- @[simp] +-- theorem allElems_cons : Vector.allElems prop (v ::ᵥ vs) ↔ prop v ∧ allElems prop vs := by +-- simp [allElems] -@[simp] -theorem allElems_nil : Vector.allElems prop Vector.nil := by simp [allElems] +-- @[simp] +-- theorem allElems_nil : Vector.allElems prop Vector.nil := by simp [allElems] -- def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i] @@ -283,34 +278,34 @@ theorem allElems_nil : Vector.allElems prop Vector.nil := by simp [allElems] -- theorem allIxes_nil : allIxes f Vector.nil := by -- simp [allIxes] -theorem getElem_allElems {v : { v: Vector α n // allElems prop v }} {i : Nat} { i_small : i < n}: - v.val[i]'i_small = ↑(Subtype.mk (p := prop) (v.val.get ⟨i, i_small⟩) (by apply v.prop; simp)) := by rfl - -theorem getElem_allElems₂ {v : { v: Vector (Vector α m) n // allElems (allElems prop) v }} {i j: Nat} { i_small : i < n} { j_small : j < m}: - (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk (p := prop) ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (by apply v.prop; rotate_right; exact v.val.get ⟨i, i_small⟩; all_goals simp)) := by rfl - -theorem allElems_indexed {v : {v : Vector α n // allElems prop v}} {i : Nat} {i_small : i < n}: - prop (v.val[i]'i_small) := by - apply v.prop - simp [getElem] - -theorem allElems_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems prop) v}} - {i : Nat} {i_small : i < c} - {j : Nat} {j_small : j < b}: - prop ((v.val[i]'i_small)[j]'j_small) := by - apply v.prop (v.val[i]'i_small) <;> simp [getElem] - -theorem allElems_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems (allElems 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) := by - apply v.prop - rotate_right - . exact (v.val[i]'i_small)[j]'j_small - rotate_right - . exact (v.val[i]'i_small) - all_goals simp [getElem] +-- theorem getElem_allElems {v : { v: Vector α n // allElems prop v }} {i : Nat} { i_small : i < n}: +-- v.val[i]'i_small = ↑(Subtype.mk (p := prop) (v.val.get ⟨i, i_small⟩) (by apply v.prop; simp)) := by rfl + +-- theorem getElem_allElems₂ {v : { v: Vector (Vector α m) n // allElems (allElems prop) v }} {i j: Nat} { i_small : i < n} { j_small : j < m}: +-- (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk (p := prop) ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (by apply v.prop; rotate_right; exact v.val.get ⟨i, i_small⟩; all_goals simp)) := by rfl + +-- theorem allElems_indexed {v : {v : Vector α n // allElems prop v}} {i : Nat} {i_small : i < n}: +-- prop (v.val[i]'i_small) := by +-- apply v.prop +-- simp [getElem] + +-- theorem allElems_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems prop) v}} +-- {i : Nat} {i_small : i < c} +-- {j : Nat} {j_small : j < b}: +-- prop ((v.val[i]'i_small)[j]'j_small) := by +-- apply v.prop (v.val[i]'i_small) <;> simp [getElem] + +-- theorem allElems_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems (allElems 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) := by +-- apply v.prop +-- rotate_right +-- . exact (v.val[i]'i_small)[j]'j_small +-- rotate_right +-- . exact (v.val[i]'i_small) +-- all_goals simp [getElem] @[simp] theorem map_ofFn {f : α → β} (g : Fin n → α) : @@ -355,6 +350,23 @@ theorem append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: subst_vars apply And.intro <;> rfl +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 [*] + -- theorem allIxes_toList : Vector.allIxes prop v ↔ ∀ i, prop (v.toList.get i) := by -- unfold Vector.allIxes -- apply Iff.intro @@ -372,39 +384,14 @@ theorem append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: -- 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] +-- theorem allElems_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allElems prop (v₁ ++ v₂) ↔ Vector.allElems prop v₁ ∧ Vector.allElems prop v₂ := by +-- simp [allElems] -- 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 +-- . exact fun a hp => h a (Or.inl hp) +-- . exact fun a hp => h a (Or.inr hp) +-- . rintro ⟨_,_⟩ _ _ ; tauto -- 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 = @@ -422,4 +409,44 @@ theorem append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}: -- apply hp -- apply Vector.get_mem +@[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] + end Vector diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean index c1181a6..5a8cb5f 100644 --- a/ProvenZk/Gates.lean +++ b/ProvenZk/Gates.lean @@ -2,18 +2,20 @@ import Mathlib.Data.ZMod.Basic import ProvenZk.Binary +open BigOperators + namespace Gates variable {N : Nat} -variable [Fact (Nat.Prime N)] +-- 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 +33,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..ea9a15e --- /dev/null +++ b/ProvenZk/Lemmas.lean @@ -0,0 +1,144 @@ +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⟩ + +@[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 + +@[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} : Gates.sub (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 5a447fe..533d7b0 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -4,223 +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 contra_of_eq_false : x = False.elim h → False := fun _ => h - -lemma fin_to_dir_vec_injective {depth : ℕ} : Function.Injective (fin_to_dir_vec (depth := depth)) := by - intro a b h - rw [fin_to_dir_vec, fin_to_dir_vec, Vector.vector_map_inj (f_inj := by intro a b; cases a <;> {cases b <;> tauto}), fin_to_bits_le, fin_to_bits_le] at h - split at h - . split at h - . rw [←recover_binary_nat_to_bits_le] at * - apply Fin.eq_of_veq - apply eq_comm.mp - simp [*] at * - assumption - . exfalso; apply contra_of_eq_false h - . exfalso; rw [eq_comm] at h; apply contra_of_eq_false h - - -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) @@ -234,74 +17,82 @@ def left {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H (Nat.succ dep 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 -def treeFor {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 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 itemAt {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.treeFor p.head).itemAt p.tail -def itemAtNat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do - t.itemAt <$> Dir.nat_to_dir_vec idx depth +-- def itemAtNat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do +-- t.itemAt <$> Dir.nat_to_dir_vec idx depth def itemAtFin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): F := - MerkleTree.itemAt Tree (Dir.fin_to_dir_vec i).reverse + MerkleTree.itemAt Tree i.toBitsBE 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.treeFor p.head.swap).root ((t.treeFor p.head).proof p.tail) + | Nat.succ _ => Vector.cons (t.treeFor !p.head).root ((t.treeFor 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 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_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 proofAtFin {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 + MerkleTree.proof Tree i.toBitsBE -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.proofAtFin t idx) := by - simp [MerkleTree.proof_at_nat, MerkleTree.proofAtFin] - 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 {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.proofAtFin t idx) := by +-- simp [MerkleTree.proof_at_nat, MerkleTree.proofAtFin] +-- 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.proofAtFin t idx = a := by - rw [proof_at_nat_to_fin (h := h)] - . simp +-- 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.proofAtFin 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'] + | 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 + cases p <;> simp [*] -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 +theorem eq_recover_iff_eq_item {depth : Nat} {F: Type} {H : Hash F 2} + {ix : Vector Bool 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 + | zero => simp [recover] | succ _ ih => intro h unfold recover at h @@ -316,69 +107,69 @@ theorem equal_recover_equal_tree {depth : Nat} {F: Type} (H : Hash F 2) 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] - unfold recover - split <;> 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 recover_tail {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 next := match ix.head with +-- | false => H vec![item, pitem] +-- | true => H vec![pitem, item] +-- recover_tail H ix.tail proof.tail next + +-- lemma recover_tail_snoc +-- {depth F} +-- (H: Hash F 2) +-- (ix : Vector Bool depth) +-- (dir : Bool) +-- (proof : Vector F depth) +-- (pitem : F) +-- (item : F): +-- recover_tail H (ix.snoc dir) (proof.snoc pitem) item = match dir with +-- | false => H vec![recover_tail H ix proof item, pitem] +-- | true => 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 Bool 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] +-- unfold recover +-- split <;> simp [*] + +-- theorem recover_tail_equals_recover_reverse +-- {F depth} +-- (H : Hash F 2) +-- (ix : Vector Bool 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 theorem recover_proof_is_root {F depth} (H : Hash F 2) - (ix : Vector Dir depth) + (ix : Vector Bool depth) (tree : MerkleTree F H depth): recover H ix (tree.proof ix) (tree.itemAt ix) = tree.root := by induction depth with @@ -390,47 +181,47 @@ theorem recover_proof_is_root simp [recover] split <;> ( unfold root - congr <;> simp [*, proof, treeFor, left, right, Dir.swap, itemAt, ih] + congr <;> simp [*, proof, treeFor, left, right, itemAt, 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) + | false => bin (set tree.left ix.tail item) tree.right + | true => 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 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 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 (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.setAtFin t idx item) := by - simp [MerkleTree.set_at_nat, MerkleTree.setAtFin] - 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.setAtFin 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.itemAtNat t idx = some (MerkleTree.itemAtFin t idx) := by - simp [MerkleTree.itemAtNat, MerkleTree.itemAtFin] - 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.itemAtNat t idx = some a ↔ - MerkleTree.itemAtFin t idx = a := by - rw [item_at_nat_to_fin (h := h)] - . simp - -theorem itemAt_set_invariant_of_neq { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {ix₁ ix₂ : Vector Dir depth} {item₁ : F} {neq : ix₁ ≠ ix₂}: + MerkleTree.set Tree i.toBitsBE 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.setAtFin t idx item) := by +-- simp [MerkleTree.set_at_nat, MerkleTree.setAtFin] +-- 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.setAtFin 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.itemAtNat t idx = some (MerkleTree.itemAtFin t idx) := by +-- simp [MerkleTree.itemAtNat, MerkleTree.itemAtFin] +-- 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.itemAtNat t idx = some a ↔ +-- MerkleTree.itemAtFin t idx = a := by +-- rw [item_at_nat_to_fin (h := h)] +-- . simp + +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 => @@ -442,7 +233,7 @@ theorem itemAt_set_invariant_of_neq { depth : Nat } {F: Type} {H : Hash F 2} {tr cases ix₂ using Vector.casesOn; rename_i ix₂_hd ix₂_tl cases tree; rename_i tree_l tree_r simp [itemAt, set, treeFor, set, left, right] - simp [Vector.vector_eq_cons] at neq + 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₂ }: @@ -472,11 +263,10 @@ theorem getElem_setAtFin_invariant_of_neq {tree : MerkleTree α H depth} {ix₁ unfold setAtFin simp [setAtFin, getElem, itemAtFin] apply itemAt_set_invariant_of_neq - intro h - rw [Vector.vector_reverse_inj, Dir.fin_to_dir_vec_injective.eq_iff, eq_comm] at h - exact hneq (congrArg Fin.val h) + simp [ne_comm, Fin.eq_iff_veq, *] -theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} (tree : MerkleTree F H depth) (ix : Vector Dir depth) (new : F) : +@[simp] +theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} {tree : MerkleTree F H depth} {ix : Vector Bool depth} {new : F} : (tree.set ix new).itemAt ix = new := by induction depth with | zero => rfl @@ -485,22 +275,21 @@ theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} (tree : Me simp [set] split <;> simp [itemAt, treeFor, 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₂ → itemAt t₂ ix = item := by - intro h - rw [<-h] - apply read_after_insert_sound +-- lemma set_implies_item_at { depth : Nat } {F: Type} {H : Hash F 2} {t₁ t₂ : MerkleTree F H depth} {ix : Vector Bool depth} {item : F} : +-- set t₁ ix item = t₂ → itemAt t₂ ix = item := by +-- intro h +-- rw [<-h] +-- apply read_after_insert_sound 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) - : + {ix : Vector Bool depth} + {tree : MerkleTree F H depth} + {proof : Vector F depth} + {item : F}: recover H ix proof item = tree.root → tree.itemAt ix = item := by intro h induction depth with @@ -524,7 +313,7 @@ theorem proof_insert_invariant {F: Type} {H: Hash F 2} [Fact (CollisionResistant H)] - (ix : Vector Dir depth) + (ix : Vector Bool depth) (tree : MerkleTree F H depth) (old new : F) (proof : Vector F depth) @@ -560,10 +349,10 @@ theorem recover_proof_reversible {H : Hash α 2} [Fact (CollisionResistant 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 + rw [Vector.eq_cons, Vector.eq_cons] at this casesm* (_ ∧ _) subst_vars - simp [treeFor, Dir.swap, left, right] + simp [treeFor, left, right] congr apply ih assumption @@ -574,7 +363,7 @@ theorem recover_equivalence (H : Hash F 2) [Fact (CollisionResistant H)] (tree : MerkleTree F H depth) - (Path : Vector Dir depth) + (Path : Vector Bool depth) (Proof : Vector F depth) (Item : F) : (itemAt tree Path = Item ∧ proof tree Path = Proof) ↔ @@ -612,12 +401,20 @@ theorem eq_root_eq_tree {H} [ph: Fact (CollisionResistant H)] {t₁ t₂ : Merkl subst_vars rfl +@[simp] +theorem Bool.eq_true_of_neg_eq_false {b}: !b = false ↔ b = true := by + cases b <;> simp + +@[simp] +theorem Bool.eq_false_of_neg_eq_true {b}: !b = true ↔ b = false := by + cases b <;> simp + lemma proof_of_set_is_proof {F d} (H : Hash F 2) [Fact (CollisionResistant H)] (Tree : MerkleTree F H d) - (ix : Vector Dir d) + (ix : Vector Bool d) (item : F): (MerkleTree.proof (MerkleTree.set Tree ix item) ix) = MerkleTree.proof Tree ix := by induction d with @@ -626,35 +423,10 @@ lemma proof_of_set_is_proof | succ d ih => cases Tree simp [MerkleTree.set, MerkleTree.proof, MerkleTree.treeFor] - 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] + split <;> { + simp [*, MerkleTree.set, MerkleTree.left, MerkleTree.right, Vector.eq_cons] at * + simp [*] + } lemma proof_of_set_fin {F d} @@ -667,12 +439,12 @@ lemma proof_of_set_fin simp [proofAtFin, setAtFin] 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 +-- 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}: +lemma tree_set_comm { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p₁ p₂ : Vector Bool 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 @@ -683,50 +455,50 @@ lemma tree_set_comm { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree 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.itemAt 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.itemAt 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⟩) +-- lemma multi_set_set { depth b : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p : Vector Bool depth} {path : Vector (Vector Bool 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.itemAt 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.itemAt 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 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 d116c01..0000000 --- a/ProvenZk/Subvector.lean +++ /dev/null @@ -1,57 +0,0 @@ -import ProvenZk.Ext.Vector - -abbrev SubVector α n prop := Subtype (α := Vector α n) (Vector.allElems prop) - -namespace SubVector - -def nil : SubVector α 0 prop := ⟨Vector.nil, by simp [Vector.allElems]⟩ - -def snoc (vs: SubVector α n prop) (v : Subtype prop): SubVector α n.succ prop := - ⟨vs.val.snoc v.val, by - intro a ha - simp at ha - rcases ha with ha | ha - . exact vs.prop a ha - . cases ha; exact v.prop - ⟩ - -@[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 => - simp [Vector.allElems] at h - refine snoc ⟨vs, ?vsp⟩ ⟨v, ?vp⟩ - case vsp => - intro a ha - exact h a (Or.inl ha) - case vp => exact h v (Or.inr rfl) - - -instance : GetElem (SubVector α n prop) (Fin n) (Subtype prop) (fun _ _ => True) where - getElem v i _ := ⟨v.val.get i, by apply v.prop; simp⟩ - -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 a ha - simp at ha - tauto⟩ - -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 From 0b88b09f259082fdb3fefea09138dda5f2f2ebe8 Mon Sep 17 00:00:00 2001 From: Marcin Kostrzewa Date: Sun, 28 Jan 2024 16:02:23 +0100 Subject: [PATCH 5/5] cleanup --- ProvenZk/Binary.lean | 9 + ProvenZk/Ext/GetElem.lean | 9 + ProvenZk/Ext/Vector/Basic.lean | 133 +++------- ProvenZk/Gates.lean | 1 - ProvenZk/Lemmas.lean | 47 +++- ProvenZk/Merkle.lean | 437 ++++----------------------------- 6 files changed, 145 insertions(+), 491 deletions(-) diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean index 8e23293..f267cef 100644 --- a/ProvenZk/Binary.lean +++ b/ProvenZk/Binary.lean @@ -34,6 +34,15 @@ lemma Bool.toZMod_one {N} : Bool.toZMod true = (1 : ZMod N) := by lemma Bool.toZMod_is_bit {N} : is_bit (toZMod (N:=N) b) := by cases b <;> simp [is_bit, toZMod, toNat] + +@[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] diff --git a/ProvenZk/Ext/GetElem.lean b/ProvenZk/Ext/GetElem.lean index 56a0fac..9b93963 100644 --- a/ProvenZk/Ext/GetElem.lean +++ b/ProvenZk/Ext/GetElem.lean @@ -7,6 +7,15 @@ theorem getElem?_eq_some_getElem_of_valid_index [GetElem cont idx elem domain] [ . 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? diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean index c43de7c..949fe98 100644 --- a/ProvenZk/Ext/Vector/Basic.lean +++ b/ProvenZk/Ext/Vector/Basic.lean @@ -252,61 +252,6 @@ instance : Membership α (Vector α n) := ⟨fun x xs => x ∈ xs.toList⟩ @[simp] theorem mem_def {xs : Vector α n} {x} : x ∈ xs ↔ x ∈ xs.toList := by rfl --- def allElems (f : α → Prop) : Vector α n → Prop := fun v => ∀(a : α), a ∈ v → f a - --- @[simp] --- theorem allElems_cons : Vector.allElems prop (v ::ᵥ vs) ↔ prop v ∧ allElems prop vs := by --- simp [allElems] - --- @[simp] --- theorem allElems_nil : Vector.allElems prop Vector.nil := by simp [allElems] - --- 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_allElems {v : { v: Vector α n // allElems prop v }} {i : Nat} { i_small : i < n}: --- v.val[i]'i_small = ↑(Subtype.mk (p := prop) (v.val.get ⟨i, i_small⟩) (by apply v.prop; simp)) := by rfl - --- theorem getElem_allElems₂ {v : { v: Vector (Vector α m) n // allElems (allElems prop) v }} {i j: Nat} { i_small : i < n} { j_small : j < m}: --- (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk (p := prop) ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (by apply v.prop; rotate_right; exact v.val.get ⟨i, i_small⟩; all_goals simp)) := by rfl - --- theorem allElems_indexed {v : {v : Vector α n // allElems prop v}} {i : Nat} {i_small : i < n}: --- prop (v.val[i]'i_small) := by --- apply v.prop --- simp [getElem] - --- theorem allElems_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems prop) v}} --- {i : Nat} {i_small : i < c} --- {j : Nat} {j_small : j < b}: --- prop ((v.val[i]'i_small)[j]'j_small) := by --- apply v.prop (v.val[i]'i_small) <;> simp [getElem] - --- theorem allElems_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems (allElems 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) := by --- apply v.prop --- rotate_right --- . exact (v.val[i]'i_small)[j]'j_small --- rotate_right --- . exact (v.val[i]'i_small) --- all_goals simp [getElem] - @[simp] theorem map_ofFn {f : α → β} (g : Fin n → α) : Vector.map f (Vector.ofFn g) = Vector.ofFn (fun x => f (g x)) := by @@ -367,47 +312,6 @@ theorem append_inj_iff {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂} . intro ⟨_, _⟩ simp [*] --- 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 allElems_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allElems prop (v₁ ++ v₂) ↔ Vector.allElems prop v₁ ∧ Vector.allElems prop v₂ := by --- simp [allElems] --- apply Iff.intro --- . intro h --- apply And.intro --- . exact fun a hp => h a (Or.inl hp) --- . exact fun a hp => h a (Or.inr hp) --- . rintro ⟨_,_⟩ _ _ ; tauto - --- 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 - - --- theorem allIxes_iff_allElems : allIxes prop v ↔ ∀ a ∈ v, prop a := by --- apply Iff.intro --- . intro hp a ain --- have := (Vector.mem_iff_get a v).mp ain --- rcases this with ⟨i, h⟩ --- cases h --- apply hp --- . intro hp i --- apply hp --- apply Vector.get_mem @[simp] theorem getElem_map {i n : ℕ} {h : i < n} {v : Vector α n} : (Vector.map f v)[i]'h = f (v[i]'h) := by @@ -449,4 +353,41 @@ 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 + 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 5a8cb5f..e944ac4 100644 --- a/ProvenZk/Gates.lean +++ b/ProvenZk/Gates.lean @@ -6,7 +6,6 @@ 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) diff --git a/ProvenZk/Lemmas.lean b/ProvenZk/Lemmas.lean index ea9a15e..c94adfa 100644 --- a/ProvenZk/Lemmas.lean +++ b/ProvenZk/Lemmas.lean @@ -9,35 +9,66 @@ 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 select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by +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 select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by +theorem Gates.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 +theorem Gates.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 +theorem Gates.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 +theorem Gates.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 +theorem Gates.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 +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 @@ -64,7 +95,7 @@ theorem Gates.or_bool {N} [Fact (N>1)] {a b : Bool} {c : ZMod N} : Gates.or a.to } @[simp] -theorem Gates.not_bool {N} [Fact (N>1)] {a : Bool} : Gates.sub (1 : ZMod N) a.toZMod = (!a).toZMod := by +theorem Gates.not_bool {N} [Fact (N>1)] {a : Bool} : (1 : ZMod N) - a.toZMod = (!a).toZMod := by cases a <;> simp [sub] @[simp] diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean index 533d7b0..23e291a 100644 --- a/ProvenZk/Merkle.lean +++ b/ProvenZk/Merkle.lean @@ -30,9 +30,6 @@ def itemAt {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : | leaf f => f | Nat.succ _ => (t.treeFor p.head).itemAt p.tail --- def itemAtNat {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (idx : Nat) : Option F := do --- t.itemAt <$> Dir.nat_to_dir_vec idx depth - def itemAtFin {F: Type} {H: Hash F 2} (Tree : MerkleTree F H d) (i : Fin (2^d)): F := MerkleTree.itemAt Tree i.toBitsBE @@ -43,27 +40,9 @@ def proof {depth : Nat} {F: Type} {H: Hash F 2} (t : MerkleTree F H depth) (p : | Nat.zero => Vector.nil | Nat.succ _ => Vector.cons (t.treeFor !p.head).root ((t.treeFor 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 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 {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.proofAtFin t idx) := by --- simp [MerkleTree.proof_at_nat, MerkleTree.proofAtFin] --- 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.proofAtFin 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 Bool depth) (proof : Vector F depth) (item : F) : F := match depth with | Nat.zero => item | Nat.succ _ => @@ -85,104 +64,8 @@ lemma recover_snoc {H : Hash α 2} {item : α} {ps : Vector Bool n} {p : Bool} { unfold recover cases p <;> simp [*] -theorem eq_recover_iff_eq_item {depth : Nat} {F: Type} {H : Hash F 2} - {ix : Vector Bool 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 => simp [recover] - | 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 Bool 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 --- | false => H vec![item, pitem] --- | true => H vec![pitem, item] --- recover_tail H ix.tail proof.tail next - --- lemma recover_tail_snoc --- {depth F} --- (H: Hash F 2) --- (ix : Vector Bool depth) --- (dir : Bool) --- (proof : Vector F depth) --- (pitem : F) --- (item : F): --- recover_tail H (ix.snoc dir) (proof.snoc pitem) item = match dir with --- | false => H vec![recover_tail H ix proof item, pitem] --- | true => 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 Bool 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] --- unfold recover --- split <;> simp [*] - --- theorem recover_tail_equals_recover_reverse --- {F depth} --- (H : Hash F 2) --- (ix : Vector Bool 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 - -theorem recover_proof_is_root - {F depth} - (H : Hash F 2) - (ix : Vector Bool depth) - (tree : MerkleTree F H depth): - recover H ix (tree.proof ix) (tree.itemAt ix) = tree.root := by - induction depth with - | zero => - cases tree - simp [recover, proof, itemAt, root] - | succ _ ih => - cases tree; rename_i l r - simp [recover] - split <;> ( - unfold root - congr <;> simp [*, proof, treeFor, left, right, itemAt, ih] - ) +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 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 @@ -190,37 +73,9 @@ def set { depth : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) ( | false => bin (set tree.left ix.tail item) tree.right | true => 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 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 {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.setAtFin t idx item) := by --- simp [MerkleTree.set_at_nat, MerkleTree.setAtFin] --- 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.setAtFin 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.itemAtNat t idx = some (MerkleTree.itemAtFin t idx) := by --- simp [MerkleTree.itemAtNat, MerkleTree.itemAtFin] --- 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.itemAtNat t idx = some a ↔ --- MerkleTree.itemAtFin t idx = a := by --- rw [item_at_nat_to_fin (h := h)] --- . simp - 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 @@ -236,269 +91,79 @@ theorem itemAt_set_invariant_of_neq { depth : Nat } {F: Type} {H : Hash F 2} {tr 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' → --- itemAtNat tree' ix₂ = itemAtNat tree ix₂ := by --- simp [set_at_nat, itemAtNat] --- 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.setAtFin tree ix₁ item₁ = tree' → --- MerkleTree.itemAtFin tree' ix₂ = MerkleTree.itemAtFin 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 getElem_setAtFin_invariant_of_neq {tree : MerkleTree α H depth} {ix₁ : Nat} {hix₁ : ix₁ < 2 ^ depth} {ix₂ : Fin (2 ^ depth)} (hneq : ix₁ ≠ ix₂.val): - (tree.setAtFin ix₂ item)[ix₁]'hix₁ = tree[ix₁]'hix₁ := by - unfold setAtFin - simp [setAtFin, getElem, itemAtFin] +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 - simp [ne_comm, Fin.eq_iff_veq, *] + intro h + rw [Fin.toBitsBE_injective, eq_comm] at h + contradiction @[simp] -theorem read_after_insert_sound {depth : Nat} {F: Type} {H: Hash F 2} {tree : MerkleTree F H depth} {ix : Vector Bool depth} {new : F} : - (tree.set ix new).itemAt ix = new := by +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 [itemAt, treeFor, 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 Bool depth} {item : F} : --- set t₁ ix item = t₂ → itemAt 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 Bool depth} - {tree : MerkleTree F H depth} - {proof : Vector F depth} - {item : F}: - recover H ix proof item = tree.root → tree.itemAt 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 [itemAt] - rw [h] - | succ depth ih => - cases tree - simp [itemAt, treeFor, left, right] - split <;> { - simp [recover, root, *, Vector.eq_cons_iff] at h - cases h - apply ih (proof := proof.tail) - assumption - } - -theorem proof_insert_invariant - {depth : Nat} - {F: Type} - {H: Hash F 2} - [Fact (CollisionResistant H)] - (ix : Vector Bool 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 - induction depth with - | zero => rfl - | succ _ ih => + cases ix using Vector.casesOn + cases proof using Vector.casesOn + simp [recover, root, itemAt] + | succ n 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.eq_cons, Vector.eq_cons] at this - casesm* (_ ∧ _) - subst_vars - simp [treeFor, left, right] - congr - apply ih - 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 recover_equivalence - {F depth} - (H : Hash F 2) - [Fact (CollisionResistant H)] - (tree : MerkleTree F H depth) - (Path : Vector Bool depth) - (Proof : Vector F depth) - (Item : F) : - (itemAt 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 - @[simp] -theorem Bool.eq_true_of_neg_eq_false {b}: !b = false ↔ b = true := by - cases b <;> 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 Bool.eq_false_of_neg_eq_true {b}: !b = true ↔ b = false := by - cases b <;> simp - -lemma proof_of_set_is_proof - {F d} - (H : Hash F 2) - [Fact (CollisionResistant H)] - (Tree : MerkleTree F H d) - (ix : Vector Bool 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.treeFor] - split <;> { - simp [*, MerkleTree.set, MerkleTree.left, MerkleTree.right, Vector.eq_cons] at * - 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 depth ih => + cases ix using Vector.casesOn; rename_i hix _ + cases hix <;> { + simp [set, proof, treeFor, left, right, root, 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): - (proofAtFin (setAtFin Tree ix item) ix) = proofAtFin Tree ix := by - simp [proofAtFin, setAtFin] - 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 Bool 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 Bool depth} {path : Vector (Vector Bool 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.itemAt 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.itemAt 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