diff --git a/formal-verification/FormalVerification/BinaryDecompositions.lean b/formal-verification/FormalVerification/BinaryDecompositions.lean new file mode 100644 index 0000000..ad73b04 --- /dev/null +++ b/formal-verification/FormalVerification/BinaryDecompositions.lean @@ -0,0 +1,72 @@ +import FormalVerification +import FormalVerification.Common +import FormalVerification.ReducednessCheck +import ProvenZk + +open SemaphoreMTB (F Order) + +lemma ReducedToBinary_256_iff_Fin_toBitsLE {f : F} {v : Vector F 256}: + Gates.to_binary f 256 v ∧ SemaphoreMTB.ReducedModRCheck_256 v ↔ + v = (Fin.toBitsLE ⟨f.val, Nat.lt_trans (Fin.is_lt f) (by decide)⟩).map Bool.toZMod := by + rw [Gates.to_binary_iff_eq_Fin_ofBitsLE] + apply Iff.intro + . intro ⟨bin, red⟩ + rcases bin with ⟨v, a, b⟩ + subst_vars + rw [ReducedModRCheck_256_semantics] at red + have {h} : Fin.mk (ZMod.val ((Fin.ofBitsLE v).val : F)) h = Fin.ofBitsLE v := by + simp [ZMod.val_cast_of_lt, red] + simp [this] + . rintro ⟨_⟩ + simp [ReducedModRCheck_256_semantics, ZMod.val_lt] + +def rev_ix_256 (i : Fin 256): Fin 256 := 248 - (i / 8) * 8 + i % 8 +def rev_ix_32 (i : Fin 32): Fin 32 := 24 - (i / 8) * 8 + i % 8 + +theorem rev_ix_256_surj : Function.Surjective rev_ix_256 := by + intro i + exists rev_ix_256 i + revert i + decide + +theorem rev_ix_32_surj : Function.Surjective rev_ix_32 := by + intro i + exists rev_ix_32 i + revert i + decide + +theorem ToReducedBigEndian_256_uncps {f k}: + SemaphoreMTB.ToReducedBigEndian_256 f k ↔ k (Vector.permute rev_ix_256 ((Fin.toBitsLE ⟨f.val, Nat.lt_trans (Fin.is_lt f) (by decide)⟩).map Bool.toZMod)) := by + unfold SemaphoreMTB.ToReducedBigEndian_256 + conv => + pattern _ ::ᵥ _ + change Vector.permute rev_ix_256 gate_0 + apply Iff.intro + . intro ⟨g, a, b, c⟩ + rw [ReducedToBinary_256_iff_Fin_toBitsLE.mp ⟨a, b⟩] at c + assumption + . intro _ + simp_rw [←and_assoc, ReducedToBinary_256_iff_Fin_toBitsLE] + simp [*] + +theorem ToReducedBigEndian_32_uncps {f k}: + SemaphoreMTB.ToReducedBigEndian_32 f k ↔ ∃(h : f.val < 2^32), k (Vector.permute rev_ix_32 ((Fin.toBitsLE ⟨f.val, h⟩).map Bool.toZMod)) := by + unfold SemaphoreMTB.ToReducedBigEndian_32 + unfold SemaphoreMTB.ReducedModRCheck_32 + conv => + pattern _ ::ᵥ _ + change Vector.permute rev_ix_32 gate_0 + simp_rw [Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt] + apply Iff.intro + . rintro ⟨_, ⟨_, ⟨_⟩⟩, _, cont⟩ + simp [*] + . rintro ⟨_, _⟩ + simp [*] + +theorem FromBinaryBigEndian_256_uncps {f k}: + SemaphoreMTB.FromBinaryBigEndian_256 (Vector.map Bool.toZMod f) k ↔ k (Fin.ofBitsLE (Vector.permute rev_ix_256 f)).val := by + unfold SemaphoreMTB.FromBinaryBigEndian_256 + conv => + pattern _ ::ᵥ _ + change Vector.permute rev_ix_256 (f.map Bool.toZMod) + simp [←Vector.map_permute, Gates.from_binary_iff_eq_ofBitsLE_mod_order] diff --git a/formal-verification/FormalVerification/Common.lean b/formal-verification/FormalVerification/Common.lean new file mode 100644 index 0000000..a881703 --- /dev/null +++ b/formal-verification/FormalVerification/Common.lean @@ -0,0 +1,12 @@ +import FormalVerification +import ProvenZk.Binary +import ProvenZk.Hash +import ProvenZk.Merkle +import ProvenZk.Ext.Vector + +def Bn256_Fr : Nat := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 +axiom bn256_Fr_prime : Nat.Prime Bn256_Fr +instance : Fact (Nat.Prime SemaphoreMTB.Order) := Fact.mk (by apply bn256_Fr_prime) + +abbrev D := 30 +abbrev B := 4 diff --git a/formal-verification/FormalVerification/Deletion.lean b/formal-verification/FormalVerification/Deletion.lean new file mode 100644 index 0000000..740a829 --- /dev/null +++ b/formal-verification/FormalVerification/Deletion.lean @@ -0,0 +1,206 @@ +import ProvenZk + +import FormalVerification +import FormalVerification.Common +import FormalVerification.Poseidon + +import FormalVerification.MerkleProofs + +open SemaphoreMTB (F Order) + +open SemaphoreMTB renaming DeletionRound_30_30 → gDeletionRound +open SemaphoreMTB renaming DeletionProof_4_4_30_4_4_30 → gDeletionProof +open SemaphoreMTB renaming VerifyProof_31_30 → gVerifyProof + +namespace Deletion + +def deletionRoundSemantics (Index Item : F) (Tree : MerkleTree F poseidon₂ D) (Proof : Vector F D) (k : MerkleTree F poseidon₂ D → Prop): Prop := + if Index.val < 2 ^ (D + 1) + then if h : Index.val < 2 ^ D + then Tree.itemAtFin ⟨Index.val, h⟩ = Item ∧ + Tree.proofAtFin ⟨Index.val, h⟩ = Proof.reverse ∧ + k (Tree.setAtFin ⟨Index.val, h⟩ 0) + else k Tree + else False + +theorem deletionRoundCircuit_eq_deletionRoundSemantics [Fact (CollisionResistant poseidon₂)]: + gDeletionRound tree.root index item proof k ↔ deletionRoundSemantics index item tree proof (fun t => k t.root) := by + unfold gDeletionRound + unfold deletionRoundSemantics + rw [Vector.exists_succ_iff_exists_snoc] + simp only [Vector.getElem_snoc_before_length, Vector.getElem_snoc_at_length] + conv => + pattern (occs := *) _ ::ᵥ _ + . change item ::ᵥ Vector.ofFn proof.get + . change Vector.ofFn vs.get + . change 0 ::ᵥ Vector.ofFn proof.get + simp_rw [Vector.ofFn_get, Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt] + unfold Fin.toBitsLE + unfold Fin.toBitsBE + cases Decidable.em (index.val < 2^(D+1)) with + | inl hlt => + cases Nat.lt_or_ge index.val (2^D) with + | inl hlt => + simp [*, VerifyProof_uncps', sub_eq_zero, MerkleTree.root_setAtFin_eq_recoverAtFin] + apply Iff.intro <;> { + intros; casesm* _ ∧ _; simp [*] at *; assumption + } + | inr hge => + have : ¬index.val < 2 ^ D := by linarith + simp [*, VerifyProof_uncps, sub_eq_zero] + | inr hge => simp [*] + +def deletionRoundsSemantics {b : Nat} + (indices : Vector F b) + (items : Vector F b) + (proofs : Vector (Vector F D) b) + (tree : MerkleTree F poseidon₂ D) + (k : F → Prop): Prop := match b with + | Nat.zero => k tree.root + | Nat.succ _ => + deletionRoundSemantics (indices.head) (items.head) tree (proofs.head) (fun t => deletionRoundsSemantics indices.tail items.tail proofs.tail t k) + +theorem deletionProofCircuit_eq_deletionRoundsSemantics [Fact (CollisionResistant poseidon₂)]: + gDeletionProof indices tree.root idComms proofs k ↔ deletionRoundsSemantics indices idComms proofs tree k := by + unfold gDeletionProof + repeat unfold deletionRoundsSemantics + repeat ( + cases indices using Vector.casesOn; rename_i _ indices + cases idComms using Vector.casesOn; rename_i _ idComms + cases proofs using Vector.casesOn; rename_i _ proofs + ) + simp_rw [deletionRoundCircuit_eq_deletionRoundSemantics] + rfl + +def treeTransformationSemantics {B : ℕ} + (tree : MerkleTree F poseidon₂ D) + (indices : Vector F B): Option (MerkleTree F poseidon₂ D) := match B with + | 0 => some tree + | _ + 1 => if h : indices.head.val < 2 ^ D + then treeTransformationSemantics (tree.setAtFin ⟨indices.head.val, h⟩ 0) indices.tail + else if indices.head.val < 2 ^ (D + 1) + then treeTransformationSemantics tree indices.tail + else none + +theorem deletionRounds_rootTransformation {B : ℕ} {indices idComms : Vector F B} {proofs : Vector (Vector F D) B} {tree : MerkleTree F poseidon₂ D} {k : F → Prop}: + deletionRoundsSemantics indices idComms proofs tree k → + ∃postTree, treeTransformationSemantics tree indices = some postTree ∧ k postTree.root := by + intro hp + induction B generalizing tree with + | zero => exists tree + | succ B ih => + unfold deletionRoundsSemantics at hp + unfold deletionRoundSemantics at hp + split at hp + . split at hp + . rcases hp with ⟨-, -, hp⟩ + replace hp := ih hp + unfold treeTransformationSemantics + simp [*] + . unfold treeTransformationSemantics + replace hp := ih hp + simp [*] + . contradiction + +theorem treeTransform_get_absent {B : ℕ} {i : F} {indices : Vector F B} {tree tree' : MerkleTree F poseidon₂ D}: + treeTransformationSemantics tree indices = some tree' → i ∉ indices → tree'[i.val]? = tree[i.val]? := by + intro hp hn + induction B generalizing tree tree' with + | zero => unfold treeTransformationSemantics at hp; injection hp; simp [*] + | succ B ih => + unfold treeTransformationSemantics at hp + have i_tail : i ∉ indices.tail := by + intro h + apply hn + apply Vector.mem_of_mem_tail + assumption + split at hp + . replace hp := ih hp i_tail + rw [hp]; clear hp + cases Nat.lt_or_ge i.val (2^D) with + | inl _ => + repeat rw [getElem?_eq_some_getElem_of_valid_index] <;> try assumption + apply congrArg + apply MerkleTree.itemAtFin_setAtFin_invariant_of_neq + intro hp + apply hn + injection hp with hp + cases (Fin.eq_of_veq hp) + apply Vector.head_mem + | inr _ => + repeat rw [getElem?_none_of_invalid_index] + all_goals (apply not_lt_of_ge; assumption) + . split at hp + . exact ih hp i_tail + . contradiction + +theorem treeTranform_get_present {B : ℕ} {i : F} {indices : Vector F B} {tree tree' : MerkleTree F poseidon₂ D}: + treeTransformationSemantics tree indices = some tree' → i ∈ indices → tree'[i.val]! = 0 := by + intro hp hi + induction B generalizing tree tree' with + | zero => cases indices using Vector.casesOn; cases hi + | succ B ih => + unfold treeTransformationSemantics at hp + cases indices using Vector.casesOn; rename_i hix tix + split at hp + . rename_i range + cases Decidable.em (i ∈ tix.toList) with + | inl h => exact ih hp h + | inr h => + rw [getElem!_eq_getElem?_get!] + rw [treeTransform_get_absent hp h] + cases eq_or_ne i hix with + | inl heq => + cases heq + rw [getElem?_eq_some_getElem_of_valid_index] <;> try exact range + simp [getElem] + | inr hne => cases hi <;> contradiction + . rename_i invalid + cases List.eq_or_ne_mem_of_mem hi with + | inl heq => + rw [getElem!_eq_getElem?_get!, getElem?_none_of_invalid_index] + . rfl + . rw [heq]; exact invalid + | inr h => + rcases h with ⟨-, range⟩ + split at hp + . exact ih hp range + . contradiction + +theorem exists_assignment {B : ℕ} {indices : Vector F B} {tree : MerkleTree F poseidon₂ D} (ixesOk : ∀i ∈ indices, i.val < 2 ^ (D+1)): + ∃items proofs postRoot, deletionRoundsSemantics indices items proofs tree (fun t => t = postRoot):= by + induction B generalizing tree with + | zero => simp [deletionRoundsSemantics] + | succ B ih => + cases indices using Vector.casesOn with | cons i indices => + simp [deletionRoundsSemantics, deletionRoundSemantics, ixesOk] + split + . have := ih (indices := indices) (tree := tree.setAtFin ⟨i.val, by assumption⟩ 0) (by + intro i hi + apply ixesOk + apply Vector.mem_of_mem_tail + simp + exact hi + ) + rcases this with ⟨items, proofs, postRoot, h⟩ + rw [Vector.exists_succ_iff_exists_cons] + apply Exists.intro + exists items + rw [Vector.exists_succ_iff_exists_cons] + apply Exists.intro + exists proofs + exists postRoot + simp [←Vector.reverse_eq] + exact ⟨by rfl, by rfl, h⟩ + . have := ih (indices := indices) (tree := tree) (by + intro i hi + apply ixesOk + apply Vector.mem_of_mem_tail + simp + exact hi + ) + rcases this with ⟨items, proofs, h⟩ + exists (0 ::ᵥ items) + exists (Vector.replicate D 0 ::ᵥ proofs) + +end Deletion diff --git a/formal-verification/FormalVerification/InputHashing.lean b/formal-verification/FormalVerification/InputHashing.lean new file mode 100644 index 0000000..19c4e89 --- /dev/null +++ b/formal-verification/FormalVerification/InputHashing.lean @@ -0,0 +1,239 @@ +import FormalVerification +import FormalVerification.Common +import FormalVerification.ReducednessCheck +import FormalVerification.BinaryDecompositions +import FormalVerification.Keccak +import ProvenZk +import Mathlib.Data.Vector.MapLemmas +open SemaphoreMTB (F Order) + +lemma ZMod.eq_iff_veq {N : ℕ} {a b : ZMod (N.succ)} : a = b ↔ a.val = b.val := by + apply Iff.intro + . intro h; subst h; rfl + . intro hp + simp [ZMod.val] at hp + apply Fin.eq_of_veq hp + +def RC : Vector (Fin (2 ^ 64)) 24 := vec![0x0000000000000001, 0x0000000000008082, 0x800000000000808A, 0x8000000080008000, 0x000000000000808B, 0x0000000080000001, 0x8000000080008081, 0x8000000000008009, 0x000000000000008A, 0x0000000000000088, 0x0000000080008009, 0x000000008000000A, 0x000000008000808B, 0x800000000000008B, 0x8000000000008089, 0x8000000000008003, 0x8000000000008002, 0x8000000000000080, 0x000000000000800A, 0x800000008000000A, 0x8000000080008081, 0x8000000000008080, 0x0000000080000001, 0x8000000080008008] + +def RCBits : Vector (Vector Bool 64) 24 := RC.map Fin.toBitsLE + +def RCBitsField : Vector (Vector F 64) 24 := vec![vec![(1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(0:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(1:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(1:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(0:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(1:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(0:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(1:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(1:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(1:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(1:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(0:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(0:F), (1:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)], vec![(1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F)], vec![(0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (0:F), (1:F)]] + +theorem RCBitsField_def : RCBitsField = RCBits.map (Vector.map Bool.toZMod) := by native_decide + +def DeletionMbuCircuit_4_4_30_4_4_30_Fold (InputHash: F) (DeletionIndices: Vector F 4) (PreRoot: F) (PostRoot: F) (IdComms: Vector F 4) (MerkleProofs: Vector (Vector F 30) 4): Prop := + SemaphoreMTB.ToReducedBigEndian_32 DeletionIndices[0] fun gate_0 => + SemaphoreMTB.ToReducedBigEndian_32 DeletionIndices[1] fun gate_1 => + SemaphoreMTB.ToReducedBigEndian_32 DeletionIndices[2] fun gate_2 => + SemaphoreMTB.ToReducedBigEndian_32 DeletionIndices[3] fun gate_3 => + SemaphoreMTB.ToReducedBigEndian_256 PreRoot fun gate_4 => + SemaphoreMTB.ToReducedBigEndian_256 PostRoot fun gate_5 => + SemaphoreMTB.KeccakGadget_640_64_24_640_256_24_1088_1 + (Vector.ofFnGet gate_0 ++ Vector.ofFnGet gate_1 ++ Vector.ofFnGet gate_2 ++ Vector.ofFnGet gate_3 ++ Vector.ofFnGet gate_4 ++ Vector.ofFnGet gate_5) RCBitsField fun gate_6 => + SemaphoreMTB.FromBinaryBigEndian_256 gate_6 fun gate_7 => + Gates.eq InputHash gate_7 ∧ + SemaphoreMTB.DeletionProof_4_4_30_4_4_30 DeletionIndices PreRoot IdComms MerkleProofs fun gate_9 => + Gates.eq gate_9 PostRoot ∧ + True + +theorem DeletionCircuit_folded {InputHash PreRoot PostRoot : F} {DeletionIndices IdComms : Vector F 4} {MerkleProofs: Vector (Vector F 30) 4}: + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash DeletionIndices PreRoot PostRoot IdComms MerkleProofs = + DeletionMbuCircuit_4_4_30_4_4_30_Fold InputHash DeletionIndices PreRoot PostRoot IdComms MerkleProofs := by rfl + +lemma Vector.map_hAppend {n₁ n₂ α β} {v₁ : Vector α n₁} {v₂ : Vector α n₂} {f : α → β}: Vector.map f v₁ ++ Vector.map f v₂ = Vector.map f (v₁ ++ v₂) := by + apply Vector.eq + simp + +theorem Deletion_InputHash_deterministic : + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash₁ DeletionIndices PreRoot PostRoot IdComms₁ MerkleProofs₁ ∧ + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash₂ DeletionIndices PreRoot PostRoot IdComms₂ MerkleProofs₂ → + InputHash₁ = InputHash₂ := by + intro ⟨h₁, h₂⟩ + rw [DeletionCircuit_folded] at h₁ h₂ + unfold DeletionMbuCircuit_4_4_30_4_4_30_Fold at h₁ h₂ + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_640_64_24_640_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] at h₁ h₂ + rcases h₁ with ⟨_, _, _, _, h₁, _⟩ + rcases h₂ with ⟨_, _, _, _, h₂, _⟩ + simp [h₁, h₂] + +theorem Deletion_skipHashing : + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash DeletionIndices PreRoot PostRoot IdComms MerkleProofs → + SemaphoreMTB.DeletionProof_4_4_30_4_4_30 DeletionIndices PreRoot IdComms MerkleProofs fun res => res = PostRoot := by + repeat rw [DeletionCircuit_folded] + unfold DeletionMbuCircuit_4_4_30_4_4_30_Fold + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_640_64_24_640_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] + simp + +def reducedKeccak640 (v : Vector Bool 640) : F := + (Fin.ofBitsLE (Vector.permute rev_ix_256 (KeccakGadget_640_64_24_640_256_24_1088_1_uniqueAssignment v RCBits).val)).val + +theorem reducedKeccak640_zeros : + reducedKeccak640 (Vector.replicate 640 false) = 4544803827027086362579185658884299814463816764684804205918064517636252260498 := by + native_decide + +theorem reducedKeccak640_ones : + reducedKeccak640 (Vector.replicate 640 true) = 1953461151768174703550518710286555794214949287664819893310466469381641334512 := by + native_decide + +theorem Deletion_InputHash_injective : + Function.Injective reducedKeccak640 → + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash DeletionIndices₁ PreRoot₁ PostRoot₁ IdComms₁ MerkleProofs₁ ∧ + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash DeletionIndices₂ PreRoot₂ PostRoot₂ IdComms₂ MerkleProofs₂ → + DeletionIndices₁ = DeletionIndices₂ ∧ PreRoot₁ = PreRoot₂ ∧ PostRoot₁ = PostRoot₂ := by + intro kr ⟨h₁, h₂⟩ + rw [DeletionCircuit_folded] at h₁ h₂ + unfold DeletionMbuCircuit_4_4_30_4_4_30_Fold at h₁ h₂ + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_640_64_24_640_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] at h₁ h₂ + rcases h₁ with ⟨_, _, _, _, h₁, _⟩ + rcases h₂ with ⟨_, _, _, _, h₂, _⟩ + rw [h₁] at h₂ + replace h₂ := kr h₂ + repeat rw [Vector.append_inj_iff] at h₂ + repeat rw [Function.Injective.eq_iff (Vector.permute_inj rev_ix_256_surj)] at h₂ + repeat rw [Function.Injective.eq_iff (Vector.permute_inj rev_ix_32_surj)] at h₂ + repeat rw [Fin.toBitsLE_injective] at h₂ + repeat rw [Fin.eq_iff_veq] at h₂ + simp [←ZMod.eq_iff_veq, getElem] at h₂ + casesm* _ ∧ _ + refine ⟨?_, by assumption, by assumption⟩ + ext i + fin_cases i <;> simp [*] + +def InsertionMbuCircuit_4_30_4_4_30_Fold (InputHash: F) (StartIndex: F) (PreRoot: F) (PostRoot: F) (IdComms: Vector F 4) (MerkleProofs: Vector (Vector F 30) 4): Prop := + SemaphoreMTB.ToReducedBigEndian_32 StartIndex fun gate_0 => + SemaphoreMTB.ToReducedBigEndian_256 PreRoot fun gate_1 => + SemaphoreMTB.ToReducedBigEndian_256 PostRoot fun gate_2 => + SemaphoreMTB.ToReducedBigEndian_256 IdComms[0] fun gate_3 => + SemaphoreMTB.ToReducedBigEndian_256 IdComms[1] fun gate_4 => + SemaphoreMTB.ToReducedBigEndian_256 IdComms[2] fun gate_5 => + SemaphoreMTB.ToReducedBigEndian_256 IdComms[3] fun gate_6 => + SemaphoreMTB.KeccakGadget_1568_64_24_1568_256_24_1088_1 + (Vector.ofFnGet gate_0 ++ Vector.ofFnGet gate_1 ++ Vector.ofFnGet gate_2 ++ Vector.ofFnGet gate_3 ++ Vector.ofFnGet gate_4 ++ Vector.ofFnGet gate_5 ++ Vector.ofFnGet gate_6) RCBitsField fun gate_7 => + SemaphoreMTB.FromBinaryBigEndian_256 gate_7 fun gate_8 => + Gates.eq InputHash gate_8 ∧ + SemaphoreMTB.InsertionProof_4_30_4_4_30 StartIndex PreRoot IdComms MerkleProofs fun gate_10 => + Gates.eq gate_10 PostRoot ∧ + True + +theorem InsertionMbuCircuit_4_30_4_4_30_folded: + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex PreRoot PostRoot IdComms MerkleProofs = + InsertionMbuCircuit_4_30_4_4_30_Fold InputHash StartIndex PreRoot PostRoot IdComms MerkleProofs := by rfl + +theorem Insertion_InputHash_deterministic : + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash₁ StartIndex PreRoot PostRoot IdComms MerkleProofs₁ ∧ + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash₂ StartIndex PreRoot PostRoot IdComms MerkleProofs₂ → + InputHash₁ = InputHash₂ := by + intro ⟨h₁, h₂⟩ + rw [InsertionMbuCircuit_4_30_4_4_30_folded] at h₁ h₂ + unfold InsertionMbuCircuit_4_30_4_4_30_Fold at h₁ h₂ + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_1568_64_24_1568_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] at h₁ h₂ + rcases h₁ with ⟨_, h₁, _⟩ + rcases h₂ with ⟨_, h₂, _⟩ + simp [h₁, h₂] + +def reducedKeccak1568 (v : Vector Bool 1568) : F := + (Fin.ofBitsLE (Vector.permute rev_ix_256 (KeccakGadget_1568_64_24_1568_256_24_1088_1_uniqueAssignment v RCBits).val)).val + +theorem reducedKeccak1568_zeros : + reducedKeccak1568 (Vector.replicate 1568 false) = 0x2872693cd1edb903471cf4a03c1e436f32dccf7ffa2218a4e0354c2514004511 := by + native_decide + +theorem reducedKeccak1568_ones : + reducedKeccak1568 (Vector.replicate 1568 true) = 0x1d7add23b253ac47705200179f6ea5df39ba965ccda0a213c2afc112bc842a5 := by + native_decide + +theorem Insertion_InputHash_injective : + Function.Injective reducedKeccak1568 → + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex₁ PreRoot₁ PostRoot₁ IdComms₁ MerkleProofs₁ ∧ + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex₂ PreRoot₂ PostRoot₂ IdComms₂ MerkleProofs₂ → + StartIndex₁ = StartIndex₂ ∧ PreRoot₁ = PreRoot₂ ∧ PostRoot₁ = PostRoot₂ ∧ IdComms₁ = IdComms₂ := by + intro kr ⟨h₁, h₂⟩ + rw [InsertionMbuCircuit_4_30_4_4_30_folded] at h₁ h₂ + unfold InsertionMbuCircuit_4_30_4_4_30_Fold at h₁ h₂ + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_1568_64_24_1568_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] at h₁ h₂ + rcases h₁ with ⟨_, h₁, _⟩ + rcases h₂ with ⟨_, h₂, _⟩ + rw [h₁] at h₂ + replace h₂ := kr h₂ + repeat rw [Vector.append_inj_iff] at h₂ + repeat rw [Function.Injective.eq_iff (Vector.permute_inj rev_ix_256_surj)] at h₂ + repeat rw [Function.Injective.eq_iff (Vector.permute_inj rev_ix_32_surj)] at h₂ + repeat rw [Fin.toBitsLE_injective] at h₂ + repeat rw [Fin.eq_iff_veq] at h₂ + simp [←ZMod.eq_iff_veq, and_assoc, getElem] at h₂ + casesm* _ ∧ _ + refine ⟨by assumption, by assumption, by assumption, ?_⟩ + ext i + fin_cases i <;> simp [*] + +theorem Insertion_skipHashing : + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex PreRoot PostRoot IdComms MerkleProofs → + SemaphoreMTB.InsertionProof_4_30_4_4_30 StartIndex PreRoot IdComms MerkleProofs fun res => res = PostRoot := by + intro h + rw [InsertionMbuCircuit_4_30_4_4_30_folded] at h + unfold InsertionMbuCircuit_4_30_4_4_30_Fold at h + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_1568_64_24_1568_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] at h + rcases h with ⟨_, _, h⟩ + simp at h + exact h diff --git a/formal-verification/FormalVerification/Insertion.lean b/formal-verification/FormalVerification/Insertion.lean new file mode 100644 index 0000000..e0c7b97 --- /dev/null +++ b/formal-verification/FormalVerification/Insertion.lean @@ -0,0 +1,324 @@ +import ProvenZk + +import FormalVerification +import FormalVerification.Common +import FormalVerification.Poseidon + +import FormalVerification.MerkleProofs + +open SemaphoreMTB (F Order) + +open SemaphoreMTB renaming InsertionRound_30_30 → gInsertionRound +open SemaphoreMTB renaming InsertionProof_4_30_4_4_30 → gInsertionProof + +namespace Insertion + +def insertionRoundSemantics (Index Item : F) (Tree : MerkleTree F poseidon₂ D) (Proof : Vector F D) (k : MerkleTree F poseidon₂ D → Prop): Prop := + if h : Index.val < 2 ^ D then + Tree.itemAtFin ⟨Index.val, h⟩ = 0 ∧ + Tree.proofAtFin ⟨Index.val, h⟩ = Proof.reverse ∧ + k (Tree.setAtFin ⟨Index.val, h⟩ Item) + else False + +theorem insertionRoundCircuit_eq_insertionRoundSemantics [Fact (CollisionResistant poseidon₂)] {Tree : MerkleTree F poseidon₂ D} : + gInsertionRound Index Item Tree.root Proof k ↔ + insertionRoundSemantics Index Item Tree Proof (fun t => k t.root) := by + unfold insertionRoundSemantics + unfold gInsertionRound + conv => + pattern (occs := *) _ ::ᵥ _ + . change 0 ::ᵥ Vector.ofFn Proof.get; + . change Item ::ᵥ Vector.ofFn Proof.get; + cases Decidable.em (Index.val < 2 ^ D) with + | inl h => + simp [h, Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt, Fin.toBitsLE, VerifyProof_uncps', MerkleTree.root_setAtFin_eq_recoverAtFin] + apply Iff.intro <;> { intros; casesm* _∧_; simp [*] at *; assumption } + | inr h => + simp [h] + intro _ h + replace h := Gates.to_binary_rangecheck h + contradiction + +def insertionRoundsSemantics {b : Nat} + (startIndex : F) + (tree : MerkleTree F poseidon₂ D) + (identities : Vector F b) + (proofs : Vector (Vector F D) b) + (k : F → Prop): Prop := match b with + | 0 => k tree.root + | Nat.succ _ => insertionRoundSemantics + startIndex + identities.head + tree + proofs.head + fun t => insertionRoundsSemantics (startIndex + 1) t identities.tail proofs.tail k + +theorem insertionRoundsCircuit_eq_insertionRoundsSemantics [Fact (CollisionResistant poseidon₂)] {Tree : MerkleTree F poseidon₂ D}: + gInsertionProof startIndex Tree.root idComms proofs k ↔ + insertionRoundsSemantics startIndex Tree idComms proofs k := by + repeat ( + cases idComms using Vector.casesOn; rename_i _ idComms + cases proofs using Vector.casesOn; rename_i _ proofs + ) + simp [gInsertionProof, insertionRoundsSemantics, insertionRoundCircuit_eq_insertionRoundSemantics, Gates.add] + ring_nf + +def treeTransformationSemantics {B : ℕ} + (tree : MerkleTree F poseidon₂ D) + (identities : Vector F B) + (startIndex : Nat): Option (MerkleTree F poseidon₂ D) := match B with + | 0 => some tree + | _ + 1 => if h : startIndex < 2 ^ D + then treeTransformationSemantics (tree.setAtFin ⟨startIndex, h⟩ identities.head) identities.tail (startIndex + 1) + else none + +lemma treeTransformationSemantics_some_index_bound {B : ℕ} {identities : Vector F B.succ}: + treeTransformationSemantics tree identities startIndex = some tree' → + startIndex < 2 ^ D := by + intro hp + unfold treeTransformationSemantics at hp + split at hp + . assumption + . contradiction + +lemma treeTransformationSemantics_next {B : ℕ} {identities : Vector F B.succ} + (hp : treeTransformationSemantics tree identities startIndex = some tree'): + treeTransformationSemantics + (tree.setAtFin ⟨startIndex, treeTransformationSemantics_some_index_bound hp⟩ identities.head) + identities.tail + (startIndex + 1) = some tree' := by + have bound : startIndex < 2 ^ D := treeTransformationSemantics_some_index_bound hp + unfold treeTransformationSemantics at hp + split at hp + . rename_i h + assumption + . contradiction + +theorem insertionRoundsRootTransformation + {B : ℕ} {startIndex : F} {identities : Vector F B} {proofs : Vector (Vector F D) B}: + insertionRoundsSemantics startIndex tree identities proofs k → + ∃postTree, treeTransformationSemantics tree identities startIndex.val = some postTree ∧ k postTree.root := by + intro hp + induction B generalizing startIndex tree with + | zero => exists tree + | succ B ih => + unfold insertionRoundsSemantics at hp + unfold insertionRoundSemantics at hp + split at hp <;> try contradiction + rename_i h + unfold treeTransformationSemantics + have : (startIndex + 1).val = startIndex.val + 1 := by + have : 2 ^ D < Order := by decide + rw [ZMod.val_add, Nat.mod_eq_of_lt (Nat.lt_trans (Nat.add_lt_add_right h (ZMod.val 1)) (by decide))] + rfl + simp [h, ←this, ih hp.2.2] + +theorem before_insertion_all_zero + {B: ℕ} {startIndex : F} {proofs : Vector (Vector F D) B} {identities : Vector F B}: + insertionRoundsSemantics (b := B) startIndex tree identities proofs k → + ∀i ∈ [startIndex.val : (startIndex + B).val], tree[i]? = some 0 := by + intro hp i hi + induction B generalizing i startIndex tree with + | zero => + cases hi; rename_i hl hu + simp at hu + simp at hl + have := Nat.lt_of_le_of_lt hl hu + have := lt_irrefl _ this + contradiction + | succ B ih => + cases identities using Vector.casesOn with | cons id ids => + cases proofs using Vector.casesOn with | cons proof proofs => + unfold insertionRoundsSemantics at hp + unfold insertionRoundSemantics at hp + rcases hi with ⟨hil, hiu⟩ + split at hp + . cases hil + . rcases hp with ⟨hp, -, -⟩ + rename_i h + rw [getElem?_eq_some_getElem_of_valid_index] + . simp [getElem, hp] + . exact h + . rename_i i hil + rcases hp with ⟨-, -, hp⟩ + have := ih hp (i.succ) (by + apply And.intro + . apply Nat.le_trans (m := startIndex.val + 1) + simp [ZMod.val_fin] + rw [Fin.val_add_one] + split <;> simp + simp_arith + assumption + . apply Nat.lt_of_lt_of_eq hiu + simp [add_assoc] + rw [add_comm (b:=1)] + ) + have := getElem_of_getElem?_some this + simp only [getElem] at this + rw [MerkleTree.itemAtFin_setAtFin_invariant_of_neq] at this + exact getElem?_some_of_getElem this + simp + rw [eq_comm] + apply Nat.ne_of_lt + apply Nat.lt_succ_of_le + assumption + . contradiction + +theorem ix_bound {B : ℕ} {startIndex : F} {identities : Vector F B.succ} {proofs : Vector (Vector F D) B.succ}: + insertionRoundsSemantics startIndex tree identities proofs k → + startIndex.val + B < 2 ^ D := by + induction B generalizing startIndex tree with + | zero => + intro hp + unfold insertionRoundsSemantics at hp + unfold insertionRoundSemantics at hp + split at hp + . simpa + . contradiction + | succ B ih => + intro hp + unfold insertionRoundsSemantics at hp + unfold insertionRoundSemantics at hp + split at hp + . rename_i hi + rcases hp with ⟨-, -, hp⟩ + have := ih hp + rw [ZMod.val_fin] at this hi + cases identities using Vector.casesOn with | cons id ids => + cases proofs using Vector.casesOn with | cons proof proofs => + rw [Fin.val_add_one_of_lt _] at this + . rw [ZMod.val_fin] + linarith + . rw [Fin.lt_iff_val_lt_val] + exact LT.lt.trans hi (by decide) + . contradiction + +lemma treeTransform_get_lt {i : Nat} {B : ℕ} {startIndex : Nat} + {identities : Vector F B}: + treeTransformationSemantics tree identities startIndex = some tree' → + i < startIndex → tree[i]? = tree'[i]? := by + induction B generalizing startIndex tree tree' with + | zero => + intro h _ + cases identities using Vector.casesOn + injection h with h + rw [h] + | succ B ih => + intro h hu + cases identities using Vector.casesOn + unfold treeTransformationSemantics at h + split at h + . rename_i hp' + have := ih h (by linarith) + rw [←this] + have ibound : i < 2^D := lt_trans hu hp' + repeat rw [getElem?_eq_some_getElem_of_valid_index (cont := MerkleTree _ _ _) ibound] + apply congrArg + rw [eq_comm] + apply MerkleTree.itemAtFin_setAtFin_invariant_of_neq + intro hp; injection hp with hp + apply Nat.ne_of_lt hu hp + . contradiction + +lemma treeTransform_get_gt {i B startIndex : ℕ} + {identities : Vector F B}: + treeTransformationSemantics tree identities startIndex = some tree' → + i ≥ startIndex + B → tree[i]? = tree'[i]? := by + induction B generalizing startIndex tree tree' with + | zero => + intro h _ + cases identities using Vector.casesOn + injection h with h + rw [h] + | succ B ih => + intro h hl + cases identities using Vector.casesOn + unfold treeTransformationSemantics at h + split at h + . cases Nat.lt_or_ge i (2^D) with + | inl ibound => + rename_i sibound + have := ih h (by linarith) + rw [←ih h (by linarith)] + repeat rw [getElem?_eq_some_getElem_of_valid_index (cont := MerkleTree _ _ _) ibound] + apply congrArg + rw [eq_comm] + apply MerkleTree.itemAtFin_setAtFin_invariant_of_neq + intro hp; injection hp with hp + cases hp + linarith + | inr h => + repeat rw [getElem?_none_of_invalid_index] + all_goals exact not_lt_of_ge h + . contradiction + +lemma treeTransform_get_inrange {i B startIndex : ℕ} {identities : Vector F B} + (hp : treeTransformationSemantics tree identities startIndex = some tree') + (inrange : i ∈ [0 : B]): + tree'[startIndex + i]? = identities[i]'inrange.2 := by + induction B generalizing startIndex i tree tree' with + | zero => cases inrange; exfalso; linarith + | succ B ih => + have := treeTransformationSemantics_next hp + have bound := treeTransformationSemantics_some_index_bound hp + cases identities using Vector.casesOn with | cons id ids => + cases i with + | zero => + have := treeTransform_get_lt this (by linarith) + rw [getElem?_eq_some_getElem_of_valid_index (cont := MerkleTree _ _ _) bound] at this + simp + rw [←this] + simp [getElem] + | succ i => + have inrange : i ∈ [0 : B] := by + cases inrange + apply And.intro <;> linarith + have := ih this inrange + simp + simp at this + rw [←this] + rw [Nat.succ_eq_one_add, add_assoc] + +theorem exists_assignment {B} {identities : Vector F B} {tree : MerkleTree F poseidon₂ D} {startIndex : Nat} (indexOk : startIndex + B < 2 ^ D) + (h : ∀i, (h: i ∈ [startIndex : startIndex + B]) → tree[i]'(Nat.lt_trans h.2 indexOk) = 0): + ∃proofs postRoot, insertionRoundsSemantics startIndex tree identities proofs (fun t => t = postRoot) := by + induction B generalizing startIndex tree with + | zero => + simp [insertionRoundsSemantics] + | succ B ih => + cases identities using Vector.casesOn with | cons id ids => + have fstIxOk : startIndex < 2 ^ D := by linarith + have fstIxMod: startIndex < Order := Nat.lt_trans fstIxOk (by decide) + simp [insertionRoundsSemantics, insertionRoundSemantics, ZMod.val_cast_of_lt fstIxMod, fstIxOk] + apply And.intro + . apply h + apply And.intro <;> simp + . rw [Vector.exists_succ_iff_exists_cons] + simp + apply And.intro + . apply Exists.intro + simp [←Vector.reverse_eq] + rfl + . apply ih + intro i h' + have gt : i > startIndex := by + have := h'.1 + simp [Order] at fstIxMod + simp [Nat.mod_eq_of_lt fstIxMod] at this + linarith + have ne: i ≠ startIndex := Nat.ne_of_gt gt + have lt : i < startIndex + Nat.succ B := by + have := h'.2 + simp [Order] at fstIxMod + simp [Nat.mod_eq_of_lt fstIxMod] at this + linarith + simp [getElem] + rw [MerkleTree.itemAtFin_setAtFin_invariant_of_neq (by intro h; injection h with h; exact ne h)] + simp [getElem] at h + apply h + apply And.intro <;> linarith + simp [Order] at fstIxMod + simp [Nat.mod_eq_of_lt fstIxMod] + linarith + +end Insertion diff --git a/formal-verification/FormalVerification/Keccak.lean b/formal-verification/FormalVerification/Keccak.lean new file mode 100644 index 0000000..df40daa --- /dev/null +++ b/formal-verification/FormalVerification/Keccak.lean @@ -0,0 +1,189 @@ +import FormalVerification +import FormalVerification.Common +import ProvenZk +import Mathlib + +open SemaphoreMTB (F Order) + +def Xor_64_64_uniqueAssignment (v1 v2 : Vector Bool 64): + UniqueAssignment (SemaphoreMTB.Xor_64_64 (v1.map Bool.toZMod) (v2.map Bool.toZMod)) (Vector.map Bool.toZMod) := by + simp [SemaphoreMTB.Xor_64_64, Vector.getElem_map, Gates.xor_bool] + rw [←Vector.map_nil] + repeat rw [←Vector.map_cons] + apply UniqueAssignment.constant + +def And_64_64_uniqueAssignment (v1 v2 : Vector Bool 64): + UniqueAssignment (SemaphoreMTB.And_64_64 (v1.map Bool.toZMod) (v2.map Bool.toZMod)) (Vector.map Bool.toZMod) := by + simp [SemaphoreMTB.And_64_64, Vector.getElem_map, Gates.and_bool] + rw [←Vector.map_nil] + repeat rw [←Vector.map_cons] + apply UniqueAssignment.constant + +def Not_64_uniqueAssignment (v1 : Vector Bool 64): + UniqueAssignment (SemaphoreMTB.Not_64 (v1.map Bool.toZMod)) (Vector.map Bool.toZMod) := by + simp [SemaphoreMTB.Not_64, Vector.getElem_map, Gates.not_bool] + rw [←Vector.map_nil] + repeat rw [←Vector.map_cons] + apply UniqueAssignment.constant + +def Xor5Round_uniqueAssignment {v1 v2 v3 v4 v5 : Bool}: + UniqueAssignment (SemaphoreMTB.Xor5Round v1.toZMod v2.toZMod v3.toZMod v4.toZMod v5.toZMod) Bool.toZMod := by + simp [SemaphoreMTB.Xor5Round, Gates.xor_bool] + apply UniqueAssignment.constant + +def Xor5_64_64_64_64_64_uniqueAssignment {v1 v2 v3 v4 v5 : Vector Bool 64}: + UniqueAssignment (SemaphoreMTB.Xor5_64_64_64_64_64 (v1.map Bool.toZMod) (v2.map Bool.toZMod) (v3.map Bool.toZMod) (v4.map Bool.toZMod) (v5.map Bool.toZMod)) (Vector.map Bool.toZMod) := by + unfold SemaphoreMTB.Xor5_64_64_64_64_64 + simp only [Vector.getElem_map] + repeat ( + apply UniqueAssignment.compose + apply Xor5Round_uniqueAssignment + intro _ + ) + rw [←Vector.map_nil] + repeat rw [←Vector.map_cons] + apply UniqueAssignment.constant + +def KeccakRound_64_5_5_64_uniqueAssignment + { state : Vector (Vector (Vector Bool 64) 5) 5} + { rc : Vector Bool 64 }: + UniqueAssignment (SemaphoreMTB.KeccakRound_64_5_5_64 (Vector.map (Vector.map (Vector.map Bool.toZMod)) state) (rc.map Bool.toZMod)) (Vector.map (Vector.map (Vector.map Bool.toZMod))) := by + unfold SemaphoreMTB.KeccakRound_64_5_5_64 + simp only [Vector.getElem_map] + + repeat ( + apply UniqueAssignment.compose + apply Xor5_64_64_64_64_64_uniqueAssignment + intro _ + ) + + repeat ( + apply UniqueAssignment.compose (embf := Vector.map Bool.toZMod) + . unfold SemaphoreMTB.Rot_64_1 + simp only [Vector.getElem_map] + rw [←Vector.map_nil] + repeat rw [←Vector.map_cons] + apply UniqueAssignment.constant + intro _ + apply UniqueAssignment.compose + apply Xor_64_64_uniqueAssignment + intro _ + ) + + repeat ( + apply UniqueAssignment.compose + apply Xor_64_64_uniqueAssignment + intro _ + ) + + ( + apply UniqueAssignment.compose (embf := Vector.map Bool.toZMod) + . apply UniqueAssignment.constant + intro _ + ) + + repeat ( + apply UniqueAssignment.compose (embf := Vector.map Bool.toZMod) + . apply UniqueAssignment.constant' + simp only [Vector.getElem_map] + rw [←Vector.map_nil] + repeat rw [←Vector.map_cons] + intro _ + ) + + repeat ( + apply UniqueAssignment.compose + apply Not_64_uniqueAssignment + intro _ + apply UniqueAssignment.compose + apply And_64_64_uniqueAssignment + intro _ + apply UniqueAssignment.compose + apply Xor_64_64_uniqueAssignment + intro _ + ) + + apply UniqueAssignment.compose + apply Xor_64_64_uniqueAssignment + intro _ + + apply UniqueAssignment.constant' + repeat rw [←Vector.map_singleton (f := Vector.map Bool.toZMod)] + repeat rw [←Vector.map_cons] + rw [←Vector.map_singleton] + repeat rw [←Vector.map_cons] + +def KeccakF_64_5_5_64_24_24_uniqueAssignment + { state : Vector (Vector (Vector Bool 64) 5) 5} + { rc : Vector (Vector Bool 64) 24 }: + UniqueAssignment (SemaphoreMTB.KeccakF_64_5_5_64_24_24 (Vector.map (Vector.map (Vector.map Bool.toZMod)) state) (rc.map (Vector.map Bool.toZMod))) (Vector.map (Vector.map (Vector.map Bool.toZMod))) := by + unfold SemaphoreMTB.KeccakF_64_5_5_64_24_24 + repeat ( + apply UniqueAssignment.compose + . simp only [Vector.getElem_map] + apply KeccakRound_64_5_5_64_uniqueAssignment + intro _ + ) + apply UniqueAssignment.constant + +def KeccakGadget_640_64_24_640_256_24_1088_1_uniqueAssignment + (input : Vector Bool 640) + ( rc : Vector (Vector Bool 64) 24): + UniqueAssignment (SemaphoreMTB.KeccakGadget_640_64_24_640_256_24_1088_1 (input.map Bool.toZMod) (rc.map (Vector.map Bool.toZMod))) (Vector.map Bool.toZMod) := by + unfold SemaphoreMTB.KeccakGadget_640_64_24_640_256_24_1088_1 + simp only [ ←Bool.toZMod_zero + , ←Bool.toZMod_one + , Vector.getElem_map + ] + simp only [Gates.xor_bool, exists_eq_left] + simp only [ ←Vector.map_singleton (f:=Bool.toZMod) + , ←Vector.map_singleton (f:=Vector.map Bool.toZMod) + , ←Vector.map_singleton (f:=Vector.map (Vector.map Bool.toZMod)) + , ←Vector.map_cons + ] + apply UniqueAssignment.compose + apply KeccakF_64_5_5_64_24_24_uniqueAssignment + intro _ + simp only [Vector.getElem_map] + simp only [ ←Vector.map_singleton (f:=Bool.toZMod) + , ←Vector.map_cons + ] + apply UniqueAssignment.constant + +def KeccakGadget_1568_64_24_1568_256_24_1088_1_uniqueAssignment + (input : Vector Bool 1568) + ( rc : Vector (Vector Bool 64) 24): + UniqueAssignment (SemaphoreMTB.KeccakGadget_1568_64_24_1568_256_24_1088_1 (input.map Bool.toZMod) (rc.map (Vector.map Bool.toZMod))) (Vector.map Bool.toZMod) := by + unfold SemaphoreMTB.KeccakGadget_1568_64_24_1568_256_24_1088_1 + simp only [ ←Bool.toZMod_zero + , ←Bool.toZMod_one + , Vector.getElem_map + ] + simp only [Gates.xor_bool, exists_eq_left] + simp only [ ←Vector.map_singleton (f:=Bool.toZMod) + , ←Vector.map_singleton (f:=Vector.map Bool.toZMod) + , ←Vector.map_singleton (f:=Vector.map (Vector.map Bool.toZMod)) + , ←Vector.map_cons + ] + apply UniqueAssignment.compose + apply KeccakF_64_5_5_64_24_24_uniqueAssignment + intro _ + simp only [Vector.getElem_map] + repeat ( + apply UniqueAssignment.compose + . apply Xor_64_64_uniqueAssignment + intro _ + ) + simp only [ ←Vector.map_singleton (f:=Vector.map (Vector.map Bool.toZMod)) + , ←Vector.map_singleton (f:=Vector.map Bool.toZMod) + , ←Vector.map_cons + ] + apply UniqueAssignment.compose + apply KeccakF_64_5_5_64_24_24_uniqueAssignment + intro _ + + simp only [Vector.getElem_map] + simp only [ ←Vector.map_singleton (f:=Bool.toZMod) + , ←Vector.map_cons + ] + apply UniqueAssignment.constant diff --git a/formal-verification/FormalVerification/MerkleProofs.lean b/formal-verification/FormalVerification/MerkleProofs.lean new file mode 100644 index 0000000..c73edda --- /dev/null +++ b/formal-verification/FormalVerification/MerkleProofs.lean @@ -0,0 +1,37 @@ +import ProvenZk + +import FormalVerification +import FormalVerification.Common +import FormalVerification.Poseidon + +open SemaphoreMTB (F Order) +open SemaphoreMTB renaming VerifyProof_31_30 → gVerifyProof + +def hashLevel (d : Bool) (h s : F): F := match d with + | true => poseidon₂ (vec![h, s]) + | false => poseidon₂ (vec![s, h]) + +lemma ProofRound_uncps {direction: Bool} {hash: F} {sibling: F} {k: F -> Prop} : + SemaphoreMTB.ProofRound direction.toZMod hash sibling k ↔ k (hashLevel direction hash sibling) := by + cases direction <;> + simp [SemaphoreMTB.ProofRound, Gates.is_bool, Gates.select, Gates.is_bool, Poseidon2_uncps, hashLevel] + +lemma MerkleTree.recover_snoc': + MerkleTree.recover poseidon₂ (ps.snoc p) (ss.snoc s) item = recover poseidon₂ ps ss (hashLevel p s item) := by + cases p <;> simp [MerkleTree.recover_snoc, hashLevel] + +lemma VerifyProof_uncps {PathIndices: Vector Bool D} {Siblings: Vector F D} {Item : F} {k : F -> Prop}: + gVerifyProof (Item ::ᵥ Siblings) (Vector.map Bool.toZMod PathIndices) k ↔ + k (MerkleTree.recover poseidon₂ PathIndices.reverse Siblings.reverse Item) := by + repeat ( + cases PathIndices using Vector.casesOn; rename_i _ PathIndices + cases Siblings using Vector.casesOn; rename_i _ Siblings + ) + unfold gVerifyProof + simp [ProofRound_uncps, MerkleTree.recover_snoc'] + simp [MerkleTree.recover] + +lemma VerifyProof_uncps' {Index: Fin (2^D)} {Siblings: Vector F D} {Item : F} {k : F -> Prop}: + gVerifyProof (Item ::ᵥ Siblings) (Index.toBitsBE.reverse.map Bool.toZMod) k ↔ + k (MerkleTree.recoverAtFin poseidon₂ Index Siblings.reverse Item) := by + simp [VerifyProof_uncps, MerkleTree.recoverAtFin] diff --git a/formal-verification/FormalVerification/Poseidon.lean b/formal-verification/FormalVerification/Poseidon.lean new file mode 100644 index 0000000..29fd2e8 --- /dev/null +++ b/formal-verification/FormalVerification/Poseidon.lean @@ -0,0 +1,40 @@ +import FormalVerification +import FormalVerification.Common +import Mathlib +import ProvenZk + +open SemaphoreMTB (F Order) + +instance : Fact (Nat.Prime SemaphoreMTB.Order) := Fact.mk (by apply bn256_Fr_prime) + +def sbox_uniqueAssignment (Inp : F): UniqueAssignment (SemaphoreMTB.sbox Inp) id := UniqueAssignment.mk _ $ by + simp [SemaphoreMTB.sbox]; tauto + +def mds_3_uniqueAssignment (S : Vector F 3): UniqueAssignment (SemaphoreMTB.mds_3 S) id := UniqueAssignment.mk _ $ by + simp [SemaphoreMTB.mds_3]; tauto + +def fullRound_3_3_uniqueAssignment (S C : Vector F 3): UniqueAssignment (SemaphoreMTB.fullRound_3_3 S C) id := UniqueAssignment.mk _ $ by + simp [SemaphoreMTB.fullRound_3_3, (sbox_uniqueAssignment _).equiv, (mds_3_uniqueAssignment _).equiv]; tauto + +def halfRound_3_3_uniqueAssignment (S C : Vector F 3): UniqueAssignment (SemaphoreMTB.halfRound_3_3 S C) id := UniqueAssignment.mk _ $ by + simp [SemaphoreMTB.halfRound_3_3, (sbox_uniqueAssignment _).equiv, (mds_3_uniqueAssignment _).equiv]; tauto + +def poseidon_3_uniqueAssignment (inp : Vector F 3): UniqueAssignment (SemaphoreMTB.poseidon_3 inp) id := by + unfold SemaphoreMTB.poseidon_3 + repeat ( + apply UniqueAssignment.compose + . (first | apply fullRound_3_3_uniqueAssignment | apply halfRound_3_3_uniqueAssignment) + intro _ + ) + apply UniqueAssignment.constant + +theorem poseidon_3_testVector : (poseidon_3_uniqueAssignment (vec![0,1,2])).val = vec![0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a, 0x0fca49b798923ab0239de1c9e7a4a9a2210312b6a2f616d18b5a87f9b628ae29, 0x0e7ae82e40091e63cbd4f16a6d16310b3729d4b6e138fcf54110e2867045a30c] := + by native_decide + +def poseidon₂ : Hash F 2 := fun a => (poseidon_3_uniqueAssignment vec![0, a.get 0, a.get 1]).val.get 0 + +lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : SemaphoreMTB.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by + unfold SemaphoreMTB.Poseidon2 poseidon₂ + apply Iff.of_eq + rw [(poseidon_3_uniqueAssignment _).equiv] + congr diff --git a/formal-verification/FormalVerification/Poseidon/Constants.lean b/formal-verification/FormalVerification/Poseidon/Constants.lean deleted file mode 100644 index 1a94d3e..0000000 --- a/formal-verification/FormalVerification/Poseidon/Constants.lean +++ /dev/null @@ -1,46 +0,0 @@ -import Mathlib - -structure Constants where - prime : Nat - t : Nat - t_ne_zero : t ≠ 0 - R_F : Nat - R_P : Nat - round_constants : List (ZMod prime) - MDS_matrix : Matrix (Fin t) (Fin t) (ZMod prime) - -namespace Constants - -abbrev F (cfg : Constants) : Type := ZMod cfg.prime - -instance {cfg : Constants} : NeZero cfg.t := ⟨cfg.t_ne_zero⟩ - -def bn254_prime : Nat := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 - -def x5_254_2_constants : List (ZMod bn254_prime) := [0x09c46e9ec68e9bd4fe1faaba294cba38a71aa177534cdd1b6c7dc0dbd0abd7a7, 0x0c0356530896eec42a97ed937f3135cfc5142b3ae405b8343c1d83ffa604cb81, 0x1e28a1d935698ad1142e51182bb54cf4a00ea5aabd6268bd317ea977cc154a30, 0x27af2d831a9d2748080965db30e298e40e5757c3e008db964cf9e2b12b91251f, 0x1e6f11ce60fc8f513a6a3cfe16ae175a41291462f214cd0879aaf43545b74e03, 0x2a67384d3bbd5e438541819cb681f0be04462ed14c3613d8f719206268d142d3, 0x0b66fdf356093a611609f8e12fbfecf0b985e381f025188936408f5d5c9f45d0, 0x012ee3ec1e78d470830c61093c2ade370b26c83cc5cebeeddaa6852dbdb09e21, 0x0252ba5f6760bfbdfd88f67f8175e3fd6cd1c431b099b6bb2d108e7b445bb1b9, 0x179474cceca5ff676c6bec3cef54296354391a8935ff71d6ef5aeaad7ca932f1, 0x2c24261379a51bfa9228ff4a503fd4ed9c1f974a264969b37e1a2589bbed2b91, 0x1cc1d7b62692e63eac2f288bd0695b43c2f63f5001fc0fc553e66c0551801b05, 0x255059301aada98bb2ed55f852979e9600784dbf17fbacd05d9eff5fd9c91b56, 0x28437be3ac1cb2e479e1f5c0eccd32b3aea24234970a8193b11c29ce7e59efd9, 0x28216a442f2e1f711ca4fa6b53766eb118548da8fb4f78d4338762c37f5f2043, 0x2c1f47cd17fa5adf1f39f4e7056dd03feee1efce03094581131f2377323482c9, 0x07abad02b7a5ebc48632bcc9356ceb7dd9dafca276638a63646b8566a621afc9, 0x0230264601ffdf29275b33ffaab51dfe9429f90880a69cd137da0c4d15f96c3c, 0x1bc973054e51d905a0f168656497ca40a864414557ee289e717e5d66899aa0a9, 0x2e1c22f964435008206c3157e86341edd249aff5c2d8421f2a6b22288f0a67fc, 0x1224f38df67c5378121c1d5f461bbc509e8ea1598e46c9f7a70452bc2bba86b8, 0x02e4e69d8ba59e519280b4bd9ed0068fd7bfe8cd9dfeda1969d2989186cde20e, 0x1f1eccc34aaba0137f5df81fc04ff3ee4f19ee364e653f076d47e9735d98018e, 0x1672ad3d709a353974266c3039a9a7311424448032cd1819eacb8a4d4284f582, 0x283e3fdc2c6e420c56f44af5192b4ae9cda6961f284d24991d2ed602df8c8fc7, 0x1c2a3d120c550ecfd0db0957170fa013683751f8fdff59d6614fbd69ff394bcc, 0x216f84877aac6172f7897a7323456efe143a9a43773ea6f296cb6b8177653fbd, 0x2c0d272becf2a75764ba7e8e3e28d12bceaa47ea61ca59a411a1f51552f94788, 0x16e34299865c0e28484ee7a74c454e9f170a5480abe0508fcb4a6c3d89546f43, 0x175ceba599e96f5b375a232a6fb9cc71772047765802290f48cd939755488fc5, 0x0c7594440dc48c16fead9e1758b028066aa410bfbc354f54d8c5ffbb44a1ee32, 0x1a3c29bc39f21bb5c466db7d7eb6fd8f760e20013ccf912c92479882d919fd8d, 0x0ccfdd906f3426e5c0986ea049b253400855d349074f5a6695c8eeabcd22e68f, 0x14f6bc81d9f186f62bdb475ce6c9411866a7a8a3fd065b3ce0e699b67dd9e796, 0x0962b82789fb3d129702ca70b2f6c5aacc099810c9c495c888edeb7386b97052, 0x1a880af7074d18b3bf20c79de25127bc13284ab01ef02575afef0c8f6a31a86d, 0x10cba18419a6a332cd5e77f0211c154b20af2924fc20ff3f4c3012bb7ae9311b, 0x057e62a9a8f89b3ebdc76ba63a9eaca8fa27b7319cae3406756a2849f302f10d, 0x287c971de91dc0abd44adf5384b4988cb961303bbf65cff5afa0413b44280cee, 0x21df3388af1687bbb3bca9da0cca908f1e562bc46d4aba4e6f7f7960e306891d, 0x1be5c887d25bce703e25cc974d0934cd789df8f70b498fd83eff8b560e1682b3, 0x268da36f76e568fb68117175cea2cd0dd2cb5d42fda5acea48d59c2706a0d5c1, 0x0e17ab091f6eae50c609beaf5510ececc5d8bb74135ebd05bd06460cc26a5ed6, 0x04d727e728ffa0a67aee535ab074a43091ef62d8cf83d270040f5caa1f62af40, 0x0ddbd7bf9c29341581b549762bc022ed33702ac10f1bfd862b15417d7e39ca6e, 0x2790eb3351621752768162e82989c6c234f5b0d1d3af9b588a29c49c8789654b, 0x1e457c601a63b73e4471950193d8a570395f3d9ab8b2fd0984b764206142f9e9, 0x21ae64301dca9625638d6ab2bbe7135ffa90ecd0c43ff91fc4c686fc46e091b0, 0x0379f63c8ce3468d4da293166f494928854be9e3432e09555858534eed8d350b, 0x002d56420359d0266a744a080809e054ca0e4921a46686ac8c9f58a324c35049, 0x123158e5965b5d9b1d68b3cd32e10bbeda8d62459e21f4090fc2c5af963515a6, 0x0be29fc40847a941661d14bbf6cbe0420fbb2b6f52836d4e60c80eb49cad9ec1, 0x1ac96991dec2bb0557716142015a453c36db9d859cad5f9a233802f24fdf4c1a, 0x1596443f763dbcc25f4964fc61d23b3e5e12c9fa97f18a9251ca3355bcb0627e, 0x12e0bcd3654bdfa76b2861d4ec3aeae0f1857d9f17e715aed6d049eae3ba3212, 0x0fc92b4f1bbea82b9ea73d4af9af2a50ceabac7f37154b1904e6c76c7cf964ba, 0x1f9c0b1610446442d6f2e592a8013f40b14f7c7722236f4f9c7e965233872762, 0x0ebd74244ae72675f8cde06157a782f4050d914da38b4c058d159f643dbbf4d3, 0x2cb7f0ed39e16e9f69a9fafd4ab951c03b0671e97346ee397a839839dccfc6d1, 0x1a9d6e2ecff022cc5605443ee41bab20ce761d0514ce526690c72bca7352d9bf, 0x2a115439607f335a5ea83c3bc44a9331d0c13326a9a7ba3087da182d648ec72f, 0x23f9b6529b5d040d15b8fa7aee3e3410e738b56305cd44f29535c115c5a4c060, 0x05872c16db0f72a2249ac6ba484bb9c3a3ce97c16d58b68b260eb939f0e6e8a7, 0x1300bdee08bb7824ca20fb80118075f40219b6151d55b5c52b624a7cdeddf6a7, 0x19b9b63d2f108e17e63817863a8f6c288d7ad29916d98cb1072e4e7b7d52b376, 0x015bee1357e3c015b5bda237668522f613d1c88726b5ec4224a20128481b4f7f, 0x2953736e94bb6b9f1b9707a4f1615e4efe1e1ce4bab218cbea92c785b128ffd1, 0x0b069353ba091618862f806180c0385f851b98d372b45f544ce7266ed6608dfc, 0x304f74d461ccc13115e4e0bcfb93817e55aeb7eb9306b64e4f588ac97d81f429, 0x15bbf146ce9bca09e8a33f5e77dfe4f5aad2a164a4617a4cb8ee5415cde913fc, 0x0ab4dfe0c2742cde44901031487964ed9b8f4b850405c10ca9ff23859572c8c6, 0x0e32db320a044e3197f45f7649a19675ef5eedfea546dea9251de39f9639779a, 0x0a1756aa1f378ca4b27635a78b6888e66797733a82774896a3078efa516da016, 0x044c4a33b10f693447fd17177f952ef895e61d328f85efa94254d6a2a25d93ef, 0x2ed3611b725b8a70be655b537f66f700fe0879d79a496891d37b07b5466c4b8b, 0x1f9ba4e8bab7ce42c8ecc3d722aa2e0eadfdeb9cfdd347b5d8339ea7120858aa, 0x1b233043052e8c288f7ee907a84e518aa38e82ac4502066db74056f865c5d3da, 0x2431e1cc164bb8d074031ab72bd55b4c902053bfc0f14db0ca2f97b020875954, 0x082f934c91f5aac330cd6953a0a7db45a13e322097583319a791f273965801fd, 0x2b9a0a223e7538b0a34be074315542a3c77245e2ae7cbe999ad6bb930c48997c, 0x0e1cd91edd2cfa2cceb85483b887a9be8164163e75a8a00eb0b589cc70214e7d, 0x2e1eac0f2bfdfd63c951f61477e3698999774f19854d00f588d324601cebe2f9, 0x0cbfa95f37fb74060c76158e769d6d157345784d8efdb33c23d748115b500b83, 0x08f05b3be923ed44d65ad49d8a61e9a676d991e3a77513d9980c232dfa4a4f84, 0x22719e2a070bcd0852bf8e21984d0443e7284925dc0758a325a2dd510c047ef6, 0x041f596a9ee1cb2bc060f7fcc3a1ab4c7bdbf036119982c0f41f62b2f26830c0, 0x233fd35de1be520a87628eb06f6b1d4c021be1c2d0dc464a19fcdd0986b10f89, 0x0524b46d1aa87a5e4325e0a423ebc810d31e078aa1b4707eefcb453c61c9c267, 0x2c34f424c81e5716ce47fcac894b85824227bb954b0f3199cc4486237c515211, 0x0b5f2a4b63387819207effc2b5541fb72dd2025b5457cc97f33010327de4915e, 0x22207856082ccc54c5b72fe439d2cfd6c17435d2f57af6ceaefac41fe05c659f, 0x24d57a8bf5da63fe4e24159b7f8950b5cdfb210194caf79f27854048ce2c8171, 0x0afab181fdd5e0583b371d75bd693f98374ad7097bb01a8573919bb23b79396e, 0x2dba9b108f208772998a52efac7cbd5676c0057194c16c0bf16290d62b1128ee, 0x26349b66edb8b16f56f881c788f53f83cbb83de0bd592b255aff13e6bce420b3, 0x25af7ce0e5e10357685e95f92339753ad81a56d28ecc193b235288a3e6f137db, 0x25b4ce7bd2294390c094d6a55edd68b970eed7aae88b2bff1f7c0187fe35011f, 0x22c543f10f6c89ec387e53f1908a88e5de9cef28ebdf30b18cb9d54c1e02b631, 0x0236f93e7789c4724fc7908a9f191e1e425e906a919d7a34df668e74882f87a9, 0x29350b401166ca010e7d27e37d05da99652bdae114eb01659cb497af980c4b52, 0x0eed787d65820d3f6bd31bbab547f75a65edb75d844ebb89ee1260916652363f, 0x07cc1170f13b46f2036a753f520b3291fdcd0e99bd94297d1906f656f4de6fad, 0x22b939233b1d7205f49bcf613a3d30b1908786d7f9f5d10c2059435689e8acea, 0x01451762a0aab81c8aad1dc8bc33e870740f083a5aa85438add650ace60ae5a6, 0x23506bb5d8727d4461fabf1025d46d1fe32eaa61dec7da57e704fec0892fce89, 0x2e484c44e838aea0bac06ae3f71bdd092a3709531e1efea97f8bd68907355522, 0x0f4bc7d07ebafd64379e78c50bd2e42baf4a594545cedc2545418da26835b54c, 0x1f4d3c8f6583e9e5fa76637862faaee851582388725df460e620996d50d8e74e, 0x093514e0c70711f82660d07be0e4a988fae02abc7b681d9153eb9bcb48fe7389, 0x1adab0c8e2b3bad346699a2b5f3bc03643ee83ece47228f24a58e0a347e153d8, 0x1672b1726057d99dd14709ebb474641a378c1b94b8072bac1a22dbef9e80dad2, 0x1dfd53d4576af2e38f44f53fdcab468cc5d8e2fae0acc4ee30d47b239b479c14, 0x0c6888a10b75b0f3a70a36263a37e17fe6d77d640f6fc3debc7f207753205c60, 0x1addb933a65be77092b34a7e77d12fe8611a61e00ee6848b85091ecca9d1e508, 0x00d7540dcd268a845c10ae18d1de933cf638ff5425f0afff7935628e299d1791, 0x140c0e42687e9ead01b2827a5664ca9c26fedde4acd99db1d316939d20b82c0e, 0x2f0c3a115d4317d191ba89b8d13d1806c20a0f9b24f8c5edc091e2ae56565984, 0x0c4ee778ff7c14553006ed220cf9c81008a0cff670b22b82d8c538a1dc958c61, 0x1704f2766d46f82c3693f00440ccc3609424ed26c0acc66227c3d7485de74c69, 0x2f2d19cc3ea5d78ea7a02c1b51d244abf0769c9f8544e40239b66fe9009c3cfa, 0x1ae03853b75fcaba5053f112e2a8e8dcdd7ee6cb9cfed9c7d6c766a806fc6629, 0x0971aabf795241df51d131d0fa61aa5f3556921b2d6f014e4e41a86ddaf056d5, 0x1408c316e6014e1a91d4cf6b6e0de73eda624f8380df1c875f5c29f7bfe2f646, 0x1667f3fe2edbe850248abe42b543093b6c89f1f773ef285341691f39822ef5bd, 0x13bf7c5d0d2c4376a48b0a03557cdf915b81718409e5c133424c69576500fe37, 0x07620a6dfb0b6cec3016adf3d3533c24024b95347856b79719bc0ba743a62c2c, 0x1574c7ef0c43545f36a8ca08bdbdd8b075d2959e2f322b731675de3e1982b4d0, 0x269e4b5b7a2eb21afd567970a717ceec5bd4184571c254fdc06e03a7ff8378f0] -def x5_254_2_MDS_matrix : Matrix (Fin 2) (Fin 2) (ZMod bn254_prime) := ![![0x066f6f85d6f68a85ec10345351a23a3aaf07f38af8c952a7bceca70bd2af7ad5, 0x2b9d4b4110c9ae997782e1509b1d0fdb20a7c02bbd8bea7305462b9f8125b1e8],![0x0cc57cdbb08507d62bf67a4493cc262fb6c09d557013fff1f573f431221f8ff9, 0x1274e649a32ed355a31a6ed69724e1adade857e86eb5c3a121bcd147943203c8]] - -def x5_254_3_constants : List (ZMod bn254_prime) := [0x0ee9a592ba9a9518d05986d656f40c2114c4993c11bb29938d21d47304cd8e6e, 0x00f1445235f2148c5986587169fc1bcd887b08d4d00868df5696fff40956e864, 0x08dff3487e8ac99e1f29a058d0fa80b930c728730b7ab36ce879f3890ecf73f5, 0x2f27be690fdaee46c3ce28f7532b13c856c35342c84bda6e20966310fadc01d0, 0x2b2ae1acf68b7b8d2416bebf3d4f6234b763fe04b8043ee48b8327bebca16cf2, 0x0319d062072bef7ecca5eac06f97d4d55952c175ab6b03eae64b44c7dbf11cfa, 0x28813dcaebaeaa828a376df87af4a63bc8b7bf27ad49c6298ef7b387bf28526d, 0x2727673b2ccbc903f181bf38e1c1d40d2033865200c352bc150928adddf9cb78, 0x234ec45ca27727c2e74abd2b2a1494cd6efbd43e340587d6b8fb9e31e65cc632, 0x15b52534031ae18f7f862cb2cf7cf760ab10a8150a337b1ccd99ff6e8797d428, 0x0dc8fad6d9e4b35f5ed9a3d186b79ce38e0e8a8d1b58b132d701d4eecf68d1f6, 0x1bcd95ffc211fbca600f705fad3fb567ea4eb378f62e1fec97805518a47e4d9c, 0x10520b0ab721cadfe9eff81b016fc34dc76da36c2578937817cb978d069de559, 0x1f6d48149b8e7f7d9b257d8ed5fbbaf42932498075fed0ace88a9eb81f5627f6, 0x1d9655f652309014d29e00ef35a2089bfff8dc1c816f0dc9ca34bdb5460c8705, 0x04df5a56ff95bcafb051f7b1cd43a99ba731ff67e47032058fe3d4185697cc7d, 0x0672d995f8fff640151b3d290cedaf148690a10a8c8424a7f6ec282b6e4be828, 0x099952b414884454b21200d7ffafdd5f0c9a9dcc06f2708e9fc1d8209b5c75b9, 0x052cba2255dfd00c7c483143ba8d469448e43586a9b4cd9183fd0e843a6b9fa6, 0x0b8badee690adb8eb0bd74712b7999af82de55707251ad7716077cb93c464ddc, 0x119b1590f13307af5a1ee651020c07c749c15d60683a8050b963d0a8e4b2bdd1, 0x03150b7cd6d5d17b2529d36be0f67b832c4acfc884ef4ee5ce15be0bfb4a8d09, 0x2cc6182c5e14546e3cf1951f173912355374efb83d80898abe69cb317c9ea565, 0x005032551e6378c450cfe129a404b3764218cadedac14e2b92d2cd73111bf0f9, 0x233237e3289baa34bb147e972ebcb9516469c399fcc069fb88f9da2cc28276b5, 0x05c8f4f4ebd4a6e3c980d31674bfbe6323037f21b34ae5a4e80c2d4c24d60280, 0x0a7b1db13042d396ba05d818a319f25252bcf35ef3aeed91ee1f09b2590fc65b, 0x2a73b71f9b210cf5b14296572c9d32dbf156e2b086ff47dc5df542365a404ec0, 0x1ac9b0417abcc9a1935107e9ffc91dc3ec18f2c4dbe7f22976a760bb5c50c460, 0x12c0339ae08374823fabb076707ef479269f3e4d6cb104349015ee046dc93fc0, 0x0b7475b102a165ad7f5b18db4e1e704f52900aa3253baac68246682e56e9a28e, 0x037c2849e191ca3edb1c5e49f6e8b8917c843e379366f2ea32ab3aa88d7f8448, 0x05a6811f8556f014e92674661e217e9bd5206c5c93a07dc145fdb176a716346f, 0x29a795e7d98028946e947b75d54e9f044076e87a7b2883b47b675ef5f38bd66e, 0x20439a0c84b322eb45a3857afc18f5826e8c7382c8a1585c507be199981fd22f, 0x2e0ba8d94d9ecf4a94ec2050c7371ff1bb50f27799a84b6d4a2a6f2a0982c887, 0x143fd115ce08fb27ca38eb7cce822b4517822cd2109048d2e6d0ddcca17d71c8, 0x0c64cbecb1c734b857968dbbdcf813cdf8611659323dbcbfc84323623be9caf1, 0x028a305847c683f646fca925c163ff5ae74f348d62c2b670f1426cef9403da53, 0x2e4ef510ff0b6fda5fa940ab4c4380f26a6bcb64d89427b824d6755b5db9e30c, 0x0081c95bc43384e663d79270c956ce3b8925b4f6d033b078b96384f50579400e, 0x2ed5f0c91cbd9749187e2fade687e05ee2491b349c039a0bba8a9f4023a0bb38, 0x30509991f88da3504bbf374ed5aae2f03448a22c76234c8c990f01f33a735206, 0x1c3f20fd55409a53221b7c4d49a356b9f0a1119fb2067b41a7529094424ec6ad, 0x10b4e7f3ab5df003049514459b6e18eec46bb2213e8e131e170887b47ddcb96c, 0x2a1982979c3ff7f43ddd543d891c2abddd80f804c077d775039aa3502e43adef, 0x1c74ee64f15e1db6feddbead56d6d55dba431ebc396c9af95cad0f1315bd5c91, 0x07533ec850ba7f98eab9303cace01b4b9e4f2e8b82708cfa9c2fe45a0ae146a0, 0x21576b438e500449a151e4eeaf17b154285c68f42d42c1808a11abf3764c0750, 0x2f17c0559b8fe79608ad5ca193d62f10bce8384c815f0906743d6930836d4a9e, 0x2d477e3862d07708a79e8aae946170bc9775a4201318474ae665b0b1b7e2730e, 0x162f5243967064c390e095577984f291afba2266c38f5abcd89be0f5b2747eab, 0x2b4cb233ede9ba48264ecd2c8ae50d1ad7a8596a87f29f8a7777a70092393311, 0x2c8fbcb2dd8573dc1dbaf8f4622854776db2eece6d85c4cf4254e7c35e03b07a, 0x1d6f347725e4816af2ff453f0cd56b199e1b61e9f601e9ade5e88db870949da9, 0x204b0c397f4ebe71ebc2d8b3df5b913df9e6ac02b68d31324cd49af5c4565529, 0x0c4cb9dc3c4fd8174f1149b3c63c3c2f9ecb827cd7dc25534ff8fb75bc79c502, 0x174ad61a1448c899a25416474f4930301e5c49475279e0639a616ddc45bc7b54, 0x1a96177bcf4d8d89f759df4ec2f3cde2eaaa28c177cc0fa13a9816d49a38d2ef, 0x066d04b24331d71cd0ef8054bc60c4ff05202c126a233c1a8242ace360b8a30a, 0x2a4c4fc6ec0b0cf52195782871c6dd3b381cc65f72e02ad527037a62aa1bd804, 0x13ab2d136ccf37d447e9f2e14a7cedc95e727f8446f6d9d7e55afc01219fd649, 0x1121552fca26061619d24d843dc82769c1b04fcec26f55194c2e3e869acc6a9a, 0x00ef653322b13d6c889bc81715c37d77a6cd267d595c4a8909a5546c7c97cff1, 0x0e25483e45a665208b261d8ba74051e6400c776d652595d9845aca35d8a397d3, 0x29f536dcb9dd7682245264659e15d88e395ac3d4dde92d8c46448db979eeba89, 0x2a56ef9f2c53febadfda33575dbdbd885a124e2780bbea170e456baace0fa5be, 0x1c8361c78eb5cf5decfb7a2d17b5c409f2ae2999a46762e8ee416240a8cb9af1, 0x151aff5f38b20a0fc0473089aaf0206b83e8e68a764507bfd3d0ab4be74319c5, 0x04c6187e41ed881dc1b239c88f7f9d43a9f52fc8c8b6cdd1e76e47615b51f100, 0x13b37bd80f4d27fb10d84331f6fb6d534b81c61ed15776449e801b7ddc9c2967, 0x01a5c536273c2d9df578bfbd32c17b7a2ce3664c2a52032c9321ceb1c4e8a8e4, 0x2ab3561834ca73835ad05f5d7acb950b4a9a2c666b9726da832239065b7c3b02, 0x1d4d8ec291e720db200fe6d686c0d613acaf6af4e95d3bf69f7ed516a597b646, 0x041294d2cc484d228f5784fe7919fd2bb925351240a04b711514c9c80b65af1d, 0x154ac98e01708c611c4fa715991f004898f57939d126e392042971dd90e81fc6, 0x0b339d8acca7d4f83eedd84093aef51050b3684c88f8b0b04524563bc6ea4da4, 0x0955e49e6610c94254a4f84cfbab344598f0e71eaff4a7dd81ed95b50839c82e, 0x06746a6156eba54426b9e22206f15abca9a6f41e6f535c6f3525401ea0654626, 0x0f18f5a0ecd1423c496f3820c549c27838e5790e2bd0a196ac917c7ff32077fb, 0x04f6eeca1751f7308ac59eff5beb261e4bb563583ede7bc92a738223d6f76e13, 0x2b56973364c4c4f5c1a3ec4da3cdce038811eb116fb3e45bc1768d26fc0b3758, 0x123769dd49d5b054dcd76b89804b1bcb8e1392b385716a5d83feb65d437f29ef, 0x2147b424fc48c80a88ee52b91169aacea989f6446471150994257b2fb01c63e9, 0x0fdc1f58548b85701a6c5505ea332a29647e6f34ad4243c2ea54ad897cebe54d, 0x12373a8251fea004df68abcf0f7786d4bceff28c5dbbe0c3944f685cc0a0b1f2, 0x21e4f4ea5f35f85bad7ea52ff742c9e8a642756b6af44203dd8a1f35c1a90035, 0x16243916d69d2ca3dfb4722224d4c462b57366492f45e90d8a81934f1bc3b147, 0x1efbe46dd7a578b4f66f9adbc88b4378abc21566e1a0453ca13a4159cac04ac2, 0x07ea5e8537cf5dd08886020e23a7f387d468d5525be66f853b672cc96a88969a, 0x05a8c4f9968b8aa3b7b478a30f9a5b63650f19a75e7ce11ca9fe16c0b76c00bc, 0x20f057712cc21654fbfe59bd345e8dac3f7818c701b9c7882d9d57b72a32e83f, 0x04a12ededa9dfd689672f8c67fee31636dcd8e88d01d49019bd90b33eb33db69, 0x27e88d8c15f37dcee44f1e5425a51decbd136ce5091a6767e49ec9544ccd101a, 0x2feed17b84285ed9b8a5c8c5e95a41f66e096619a7703223176c41ee433de4d1, 0x1ed7cc76edf45c7c404241420f729cf394e5942911312a0d6972b8bd53aff2b8, 0x15742e99b9bfa323157ff8c586f5660eac6783476144cdcadf2874be45466b1a, 0x1aac285387f65e82c895fc6887ddf40577107454c6ec0317284f033f27d0c785, 0x25851c3c845d4790f9ddadbdb6057357832e2e7a49775f71ec75a96554d67c77, 0x15a5821565cc2ec2ce78457db197edf353b7ebba2c5523370ddccc3d9f146a67, 0x2411d57a4813b9980efa7e31a1db5966dcf64f36044277502f15485f28c71727, 0x002e6f8d6520cd4713e335b8c0b6d2e647e9a98e12f4cd2558828b5ef6cb4c9b, 0x2ff7bc8f4380cde997da00b616b0fcd1af8f0e91e2fe1ed7398834609e0315d2, 0x00b9831b948525595ee02724471bcd182e9521f6b7bb68f1e93be4febb0d3cbe, 0x0a2f53768b8ebf6a86913b0e57c04e011ca408648a4743a87d77adbf0c9c3512, 0x00248156142fd0373a479f91ff239e960f599ff7e94be69b7f2a290305e1198d, 0x171d5620b87bfb1328cf8c02ab3f0c9a397196aa6a542c2350eb512a2b2bcda9, 0x170a4f55536f7dc970087c7c10d6fad760c952172dd54dd99d1045e4ec34a808, 0x29aba33f799fe66c2ef3134aea04336ecc37e38c1cd211ba482eca17e2dbfae1, 0x1e9bc179a4fdd758fdd1bb1945088d47e70d114a03f6a0e8b5ba650369e64973, 0x1dd269799b660fad58f7f4892dfb0b5afeaad869a9c4b44f9c9e1c43bdaf8f09, 0x22cdbc8b70117ad1401181d02e15459e7ccd426fe869c7c95d1dd2cb0f24af38, 0x0ef042e454771c533a9f57a55c503fcefd3150f52ed94a7cd5ba93b9c7dacefd, 0x11609e06ad6c8fe2f287f3036037e8851318e8b08a0359a03b304ffca62e8284, 0x1166d9e554616dba9e753eea427c17b7fecd58c076dfe42708b08f5b783aa9af, 0x2de52989431a859593413026354413db177fbf4cd2ac0b56f855a888357ee466, 0x3006eb4ffc7a85819a6da492f3a8ac1df51aee5b17b8e89d74bf01cf5f71e9ad, 0x2af41fbb61ba8a80fdcf6fff9e3f6f422993fe8f0a4639f962344c8225145086, 0x119e684de476155fe5a6b41a8ebc85db8718ab27889e85e781b214bace4827c3, 0x1835b786e2e8925e188bea59ae363537b51248c23828f047cff784b97b3fd800, 0x28201a34c594dfa34d794996c6433a20d152bac2a7905c926c40e285ab32eeb6, 0x083efd7a27d1751094e80fefaf78b000864c82eb571187724a761f88c22cc4e7, 0x0b6f88a3577199526158e61ceea27be811c16df7774dd8519e079564f61fd13b, 0x0ec868e6d15e51d9644f66e1d6471a94589511ca00d29e1014390e6ee4254f5b, 0x2af33e3f866771271ac0c9b3ed2e1142ecd3e74b939cd40d00d937ab84c98591, 0x0b520211f904b5e7d09b5d961c6ace7734568c547dd6858b364ce5e47951f178, 0x0b2d722d0919a1aad8db58f10062a92ea0c56ac4270e822cca228620188a1d40, 0x1f790d4d7f8cf094d980ceb37c2453e957b54a9991ca38bbe0061d1ed6e562d4, 0x0171eb95dfbf7d1eaea97cd385f780150885c16235a2a6a8da92ceb01e504233, 0x0c2d0e3b5fd57549329bf6885da66b9b790b40defd2c8650762305381b168873, 0x1162fb28689c27154e5a8228b4e72b377cbcafa589e283c35d3803054407a18d, 0x2f1459b65dee441b64ad386a91e8310f282c5a92a89e19921623ef8249711bc0, 0x1e6ff3216b688c3d996d74367d5cd4c1bc489d46754eb712c243f70d1b53cfbb, 0x01ca8be73832b8d0681487d27d157802d741a6f36cdc2a0576881f9326478875, 0x1f7735706ffe9fc586f976d5bdf223dc680286080b10cea00b9b5de315f9650e, 0x2522b60f4ea3307640a0c2dce041fba921ac10a3d5f096ef4745ca838285f019, 0x23f0bee001b1029d5255075ddc957f833418cad4f52b6c3f8ce16c235572575b, 0x2bc1ae8b8ddbb81fcaac2d44555ed5685d142633e9df905f66d9401093082d59, 0x0f9406b8296564a37304507b8dba3ed162371273a07b1fc98011fcd6ad72205f, 0x2360a8eb0cc7defa67b72998de90714e17e75b174a52ee4acb126c8cd995f0a8, 0x15871a5cddead976804c803cbaef255eb4815a5e96df8b006dcbbc2767f88948, 0x193a56766998ee9e0a8652dd2f3b1da0362f4f54f72379544f957ccdeefb420f, 0x2a394a43934f86982f9be56ff4fab1703b2e63c8ad334834e4309805e777ae0f, 0x1859954cfeb8695f3e8b635dcb345192892cd11223443ba7b4166e8876c0d142, 0x04e1181763050e58013444dbcb99f1902b11bc25d90bbdca408d3819f4fed32b, 0x0fdb253dee83869d40c335ea64de8c5bb10eb82db08b5e8b1f5e5552bfd05f23, 0x058cbe8a9a5027bdaa4efb623adead6275f08686f1c08984a9d7c5bae9b4f1c0, 0x1382edce9971e186497eadb1aeb1f52b23b4b83bef023ab0d15228b4cceca59a, 0x03464990f045c6ee0819ca51fd11b0be7f61b8eb99f14b77e1e6634601d9e8b5, 0x23f7bfc8720dc296fff33b41f98ff83c6fcab4605db2eb5aaa5bc137aeb70a58, 0x0a59a158e3eec2117e6e94e7f0e9decf18c3ffd5e1531a9219636158bbaf62f2, 0x06ec54c80381c052b58bf23b312ffd3ce2c4eba065420af8f4c23ed0075fd07b, 0x118872dc832e0eb5476b56648e867ec8b09340f7a7bcb1b4962f0ff9ed1f9d01, 0x13d69fa127d834165ad5c7cba7ad59ed52e0b0f0e42d7fea95e1906b520921b1, 0x169a177f63ea681270b1c6877a73d21bde143942fb71dc55fd8a49f19f10c77b, 0x04ef51591c6ead97ef42f287adce40d93abeb032b922f66ffb7e9a5a7450544d, 0x256e175a1dc079390ecd7ca703fb2e3b19ec61805d4f03ced5f45ee6dd0f69ec, 0x30102d28636abd5fe5f2af412ff6004f75cc360d3205dd2da002813d3e2ceeb2, 0x10998e42dfcd3bbf1c0714bc73eb1bf40443a3fa99bef4a31fd31be182fcc792, 0x193edd8e9fcf3d7625fa7d24b598a1d89f3362eaf4d582efecad76f879e36860, 0x18168afd34f2d915d0368ce80b7b3347d1c7a561ce611425f2664d7aa51f0b5d, 0x29383c01ebd3b6ab0c017656ebe658b6a328ec77bc33626e29e2e95b33ea6111, 0x10646d2f2603de39a1f4ae5e7771a64a702db6e86fb76ab600bf573f9010c711, 0x0beb5e07d1b27145f575f1395a55bf132f90c25b40da7b3864d0242dcb1117fb, 0x16d685252078c133dc0d3ecad62b5c8830f95bb2e54b59abdffbf018d96fa336, 0x0a6abd1d833938f33c74154e0404b4b40a555bbbec21ddfafd672dd62047f01a, 0x1a679f5d36eb7b5c8ea12a4c2dedc8feb12dffeec450317270a6f19b34cf1860, 0x0980fb233bd456c23974d50e0ebfde4726a423eada4e8f6ffbc7592e3f1b93d6, 0x161b42232e61b84cbf1810af93a38fc0cece3d5628c9282003ebacb5c312c72b, 0x0ada10a90c7f0520950f7d47a60d5e6a493f09787f1564e5d09203db47de1a0b, 0x1a730d372310ba82320345a29ac4238ed3f07a8a2b4e121bb50ddb9af407f451, 0x2c8120f268ef054f817064c369dda7ea908377feaba5c4dffbda10ef58e8c556, 0x1c7c8824f758753fa57c00789c684217b930e95313bcb73e6e7b8649a4968f70, 0x2cd9ed31f5f8691c8e39e4077a74faa0f400ad8b491eb3f7b47b27fa3fd1cf77, 0x23ff4f9d46813457cf60d92f57618399a5e022ac321ca550854ae23918a22eea, 0x09945a5d147a4f66ceece6405dddd9d0af5a2c5103529407dff1ea58f180426d, 0x188d9c528025d4c2b67660c6b771b90f7c7da6eaa29d3f268a6dd223ec6fc630, 0x3050e37996596b7f81f68311431d8734dba7d926d3633595e0c0d8ddf4f0f47f, 0x15af1169396830a91600ca8102c35c426ceae5461e3f95d89d829518d30afd78, 0x1da6d09885432ea9a06d9f37f873d985dae933e351466b2904284da3320d8acc, 0x2796ea90d269af29f5f8acf33921124e4e4fad3dbe658945e546ee411ddaa9cb, 0x202d7dd1da0f6b4b0325c8b3307742f01e15612ec8e9304a7cb0319e01d32d60, 0x096d6790d05bb759156a952ba263d672a2d7f9c788f4c831a29dace4c0f8be5f, 0x054efa1f65b0fce283808965275d877b438da23ce5b13e1963798cb1447d25a4, 0x1b162f83d917e93edb3308c29802deb9d8aa690113b2e14864ccf6e18e4165f1, 0x21e5241e12564dd6fd9f1cdd2a0de39eedfefc1466cc568ec5ceb745a0506edc, 0x1cfb5662e8cf5ac9226a80ee17b36abecb73ab5f87e161927b4349e10e4bdf08, 0x0f21177e302a771bbae6d8d1ecb373b62c99af346220ac0129c53f666eb24100, 0x1671522374606992affb0dd7f71b12bec4236aede6290546bcef7e1f515c2320, 0x0fa3ec5b9488259c2eb4cf24501bfad9be2ec9e42c5cc8ccd419d2a692cad870, 0x193c0e04e0bd298357cb266c1506080ed36edce85c648cc085e8c57b1ab54bba, 0x102adf8ef74735a27e9128306dcbc3c99f6f7291cd406578ce14ea2adaba68f8, 0x0fe0af7858e49859e2a54d6f1ad945b1316aa24bfbdd23ae40a6d0cb70c3eab1, 0x216f6717bbc7dedb08536a2220843f4e2da5f1daa9ebdefde8a5ea7344798d22, 0x1da55cc900f0d21f4a3e694391918a1b3c23b2ac773c6b3ef88e2e4228325161] -def x5_254_3_MDS_matrix : Matrix (Fin 3) (Fin 3) (ZMod bn254_prime) := ![![0x109b7f411ba0e4c9b2b70caf5c36a7b194be7c11ad24378bfedb68592ba8118b, 0x16ed41e13bb9c0c66ae119424fddbcbc9314dc9fdbdeea55d6c64543dc4903e0, 0x2b90bba00fca0589f617e7dcbfe82e0df706ab640ceb247b791a93b74e36736d], ![0x2969f27eed31a480b9c36c764379dbca2cc8fdd1415c3dded62940bcde0bd771, 0x2e2419f9ec02ec394c9871c832963dc1b89d743c8c7b964029b2311687b1fe23, 0x101071f0032379b697315876690f053d148d4e109f5fb065c8aacc55a0f89bfa], ![0x143021ec686a3f330d5f9e654638065ce6cd79e28c5b3753326244ee65a1b1a7, 0x176cc029695ad02582a70eff08a6fd99d057e12e58e7d7b6b16cdfabc8ee2911, 0x19a3fc0a56702bf417ba7fee3802593fa644470307043f7773279cd71d25d5e0]] - -def x5_254_3 : Constants := { - prime := bn254_prime, - t := 3, - t_ne_zero := by decide, - R_F := 8, - R_P := 57, - round_constants := x5_254_3_constants, - MDS_matrix := x5_254_3_MDS_matrix -} - -def x5_254_2 : Constants := { - prime := bn254_prime - t := 2, - t_ne_zero := by decide, - R_F := 8, - R_P := 56, - round_constants := x5_254_2_constants, - MDS_matrix := x5_254_2_MDS_matrix -} - -end Constants \ No newline at end of file diff --git a/formal-verification/FormalVerification/Poseidon/Correctness.lean b/formal-verification/FormalVerification/Poseidon/Correctness.lean deleted file mode 100644 index eabffea..0000000 --- a/formal-verification/FormalVerification/Poseidon/Correctness.lean +++ /dev/null @@ -1,293 +0,0 @@ -import FormalVerification -import FormalVerification.Poseidon.Constants -import FormalVerification.Poseidon.Spec -import Mathlib -import ProvenZk - -open Matrix -open SemaphoreMTB (F Order) - -variable [Fact (Nat.Prime Order)] - -private lemma iff_to_eq {α} {a b: α} {k : α -> Prop }: a = b -> (k a ↔ k b) := by intro eq; rw [eq] - -def mds_matmul (cfg : Constants) (S : Vector cfg.F cfg.t) : Vector cfg.F cfg.t := (cfg.MDS_matrix ⬝ S.to_column).to_vector - -def full_round (cfg : Constants) (S C: Vector cfg.F cfg.t) : Vector cfg.F cfg.t := - mds_matmul cfg (S.mapIdx fun i s => (s + C.get i) ^ 5) - -def partial_round (cfg : Constants) (S C: Vector cfg.F cfg.t) : Vector cfg.F cfg.t := - let with_const := S.mapIdx fun i s => s + C.get i - mds_matmul cfg (with_const.set 0 (with_const.get 0 ^ 5)) - -def full_rounds (cfg : Constants) (state_words : Vector cfg.F cfg.t) (round_constants_counter rounds : ℕ) : Vector cfg.F cfg.t := Id.run do - let mut round_constants_counter := round_constants_counter - let mut state_words := state_words - - for _ in [0:rounds] do - let consts := Vector.ofFn (fun i => cfg.round_constants[round_constants_counter + i]!) - state_words := full_round cfg state_words consts - round_constants_counter := round_constants_counter + cfg.t - state_words - -def partial_rounds (cfg : Constants) (state_words : Vector cfg.F cfg.t) (round_constants_counter rounds : ℕ) : Vector cfg.F cfg.t := Id.run do - let mut round_constants_counter := round_constants_counter - let mut state_words := state_words - - for _ in [0:rounds] do - let consts := Vector.ofFn (fun i => cfg.round_constants[round_constants_counter + i]!) - state_words := partial_round cfg state_words consts - round_constants_counter := round_constants_counter + cfg.t - state_words - -def full_rounds_cps - (cfg : Constants) - (full_round : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop) - (state: Vector cfg.F cfg.t) - (init_const: Nat) - (round_count: Nat) - (k : Vector cfg.F cfg.t -> Prop): Prop := match round_count with -| Nat.zero => k state -| Nat.succ round_count => - full_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' => - full_rounds_cps cfg full_round state' (init_const + cfg.t) round_count k - -def half_rounds_cps - (cfg : Constants) - (half_round : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop) - (state: Vector cfg.F cfg.t) - (init_const: Nat) - (round_count: Nat) - (k : Vector cfg.F cfg.t -> Prop): Prop := match round_count with -| Nat.zero => k state -| Nat.succ round_count => - half_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' => - half_rounds_cps cfg half_round state' (init_const + cfg.t) round_count k - -lemma sbox_uncps (A : F) (k : F -> Prop): SemaphoreMTB.sbox A k = k (A ^ 5) := by - unfold SemaphoreMTB.sbox - simp [Gates.mul] - apply iff_to_eq - repeat (rw [pow_succ]) - rw [pow_zero, mul_one, mul_assoc] - -lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop): - SemaphoreMTB.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by - simp [SemaphoreMTB.mds_3, Gates.add, Gates.mul] - apply iff_to_eq - simp [mds_matmul, Constants.x5_254_3, Constants.x5_254_3_MDS_matrix] - simp [Vector.to_column, Matrix.to_vector, Vector.ofFn] - repeat ( - apply congrArg₂ - { - simp [getElem, Matrix.of, Matrix.mul, Matrix.dotProduct] - simp [Finset.sum, Finset.univ, Fintype.elems] - rw [←add_assoc] - conv => lhs; simp [mul_comm] - } - ) - rfl - -lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop): - SemaphoreMTB.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by - unfold SemaphoreMTB.fullRound_3_3 - unfold Gates.add - simp [mds_3_uncps, sbox_uncps, full_round] - rw [←Vector.ofFn_get S] - rfl - - -lemma half_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop): - SemaphoreMTB.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by - unfold SemaphoreMTB.halfRound_3_3 - unfold Gates.add - simp [sbox_uncps, mds_3_uncps, partial_round] - rw [←Vector.ofFn_get S] - rfl - -lemma partial_rounds_uncps - {cfg : Constants} - {S : Vector cfg.F cfg.t} - {start count : Nat} - {k : Vector cfg.F cfg.t -> Prop} - {half_round_cps : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop} - {half_round_uncps : ∀ S C k, half_round_cps S C k = k (partial_round cfg S C)} - : - half_rounds_cps cfg half_round_cps S start count k = k (partial_rounds cfg S start count) := by - induction count generalizing start S with - | zero => - simp [half_rounds_cps, partial_rounds, forIn, Std.Range.forIn, Std.Range.forIn.loop, Id.run] - | succ count ih => - unfold half_rounds_cps - rw [half_round_uncps, ih] - unfold partial_rounds - simp [Id.run, forIn] - apply iff_to_eq - simp [Std.Range.counter_elide_fst] - rw [←zero_add (Nat.succ count), Std.Range.forIn_startSucc] - have : Nat.succ 0 = 0 + 1 := by rfl - rw [this] - have : 0 + Nat.succ count = count + 1 := by simp_arith - rw [this] - rw [←Std.Range.forIn_ixShift] - apply congrArg₂ - { simp } - funext i r - congr - funext i' - have : start + cfg.t + i * cfg.t + ↑i' = start + (i + 1) * cfg.t + ↑i' := by linarith - rw [this] - -lemma partial_rounds_3_uncps - {S : Vector F 3} - {start count : Nat} - {k : Vector F 3 -> Prop}: - half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by - apply partial_rounds_uncps - apply half_round_3_uncps - -lemma full_rounds_uncps - {cfg : Constants} - {S : Vector cfg.F cfg.t} - {start count : Nat} - {k : Vector cfg.F cfg.t -> Prop} - {full_round_cps : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop} - {full_round_uncps : ∀ S C k, full_round_cps S C k = k (full_round cfg S C)} - : - full_rounds_cps cfg full_round_cps S start count k = k (full_rounds cfg S start count) := by - induction count generalizing start S with - | zero => - simp [full_rounds_cps, full_rounds, forIn, Std.Range.forIn, Std.Range.forIn.loop, Id.run] - | succ count ih => - unfold full_rounds_cps - rw [full_round_uncps, ih] - unfold full_rounds - simp [Id.run, forIn] - apply iff_to_eq - simp [Std.Range.counter_elide_fst] - rw [←zero_add (Nat.succ count), Std.Range.forIn_startSucc] - have : Nat.succ 0 = 0 + 1 := by rfl - rw [this] - have : 0 + Nat.succ count = count + 1 := by simp_arith - rw [this] - rw [←Std.Range.forIn_ixShift] - apply congrArg₂ - { simp } - funext i r - congr - funext i' - have : start + cfg.t + i * cfg.t + ↑i' = start + (i + 1) * cfg.t + ↑i' := by linarith - rw [this] - -lemma full_rounds_3_uncps - {S : Vector F 3} - {start count : Nat} - {k : Vector F 3 -> Prop}: - full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by - apply full_rounds_uncps - apply full_round_3_uncps - -def looped_poseidon_3 (inp : Vector F 3) (k: Vector F 3 -> Prop): Prop := - full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 inp 0 4 fun state => - half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 state 12 57 fun state' => - full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 state' 183 4 k - -set_option maxRecDepth 2048 - -theorem looped_poseidon_3_go (inp : Vector F 3) (k : Vector F 3 -> Prop): - SemaphoreMTB.poseidon_3 inp k = looped_poseidon_3 inp k := by - unfold looped_poseidon_3 - unfold SemaphoreMTB.poseidon_3 - simp [full_rounds_cps, half_rounds_cps, getElem!, Vector.ofFn] - rfl - -set_option maxRecDepth 512 - -def perm_folded (cfg : Constants) (input_words : Vector cfg.F cfg.t): Vector cfg.F cfg.t := Id.run do - let R_f := cfg.R_F / 2 - let mut round_constants_counter := 0 - let mut state_words := input_words - - state_words := full_rounds cfg state_words round_constants_counter R_f - round_constants_counter := R_f * cfg.t - - state_words := partial_rounds cfg state_words round_constants_counter cfg.R_P - round_constants_counter := R_f * cfg.t + cfg.R_P * cfg.t - - state_words := full_rounds cfg state_words round_constants_counter R_f - - state_words - -theorem perm_folded_go (cfg : Constants) (input_words : Vector cfg.F cfg.t): - Poseidon.perm cfg input_words = perm_folded cfg input_words := by - unfold Poseidon.perm - unfold perm_folded - unfold full_rounds - unfold partial_rounds - simp [Id.run, forIn] - simp [Std.Range.counter_elide_fst] - cases cfg; rename_i prime t t_ne_zero R_F R_P round_constants MDS_matrix - cases t - { contradiction } - rename_i t' - simp at * - apply congrArg₂ - { - apply congrArg₂ - { - apply congrArg - funext i r - unfold full_round - unfold mds_matmul - simp - apply congrArg - apply congrArg - apply congrArg - apply congrArg - rw [Vector.setLoop_def (f := fun _ r => r ^ 5)] - rw [Vector.setLoop_def (f := fun i' r => r + round_constants[i * Nat.succ t' + i']!)] - simp [Vector.setLoop_mapIdx, Vector.mapIdx_compose] - rw [Vector.mapIdx_mod] - } - { - funext i r - rw [Vector.setLoop_def (f := fun i' r => r + round_constants[R_F / 2 * Nat.succ t' + i * Nat.succ t' + i']!)] - rw [Vector.setLoop_mapIdx] - apply congrArg - unfold partial_round - simp - unfold mds_matmul - simp - apply congrArg - apply congrArg - apply congrArg - rw [Vector.mapIdx_mod] - } - } - { - funext i r - apply congrArg - unfold full_round - unfold mds_matmul - simp - apply congrArg - apply congrArg - apply congrArg - rw [Vector.setLoop_def (f := fun _ r => r ^ 5)] - rw [Vector.setLoop_def (f := fun i' r => r + round_constants[R_F / 2 * Nat.succ t' + R_P * Nat.succ t' + i * Nat.succ t' + i']!)] - simp [Vector.setLoop_mapIdx, Vector.mapIdx_compose] - rw [Vector.mapIdx_mod] - } - -theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop): - SemaphoreMTB.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by - simp [ - looped_poseidon_3_go, - looped_poseidon_3, - full_rounds_uncps, - partial_rounds_3_uncps, - full_rounds_3_uncps, - perm_folded_go, - perm_folded - ] - rfl diff --git a/formal-verification/FormalVerification/Poseidon/Spec.lean b/formal-verification/FormalVerification/Poseidon/Spec.lean deleted file mode 100644 index b823399..0000000 --- a/formal-verification/FormalVerification/Poseidon/Spec.lean +++ /dev/null @@ -1,42 +0,0 @@ -import Mathlib -import ProvenZk -import FormalVerification.Poseidon.Constants - -open Matrix - -namespace Poseidon - -def perm (cfg : Constants) (input_words : Vector cfg.F cfg.t): Vector cfg.F cfg.t := Id.run do - let R_f := cfg.R_F / 2 - let mut round_constants_counter := 0 - let mut state_words := input_words - for _ in [0:R_f] do - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i + cfg.round_constants[round_constants_counter]!) - round_constants_counter := round_constants_counter + 1 - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i ^ 5) - state_words := (cfg.MDS_matrix ⬝ state_words.to_column).to_vector - - for _ in [0:cfg.R_P] do - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i + cfg.round_constants[round_constants_counter]!) - round_constants_counter := round_constants_counter + 1 - state_words := state_words.set 0 (state_words.get 0 ^ 5) - state_words := (cfg.MDS_matrix ⬝ state_words.to_column).to_vector - - for _ in [0:R_f] do - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i + cfg.round_constants[round_constants_counter]!) - round_constants_counter := round_constants_counter + 1 - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i ^ 5) - state_words := (cfg.MDS_matrix ⬝ state_words.to_column).to_vector - - state_words - -theorem test_vector_correct_x5_254_3: - perm Constants.x5_254_3 vec![0,1,2] = vec![0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a, 0x0fca49b798923ab0239de1c9e7a4a9a2210312b6a2f616d18b5a87f9b628ae29, 0x0e7ae82e40091e63cbd4f16a6d16310b3729d4b6e138fcf54110e2867045a30c] := - by eq_refl - -end Poseidon \ No newline at end of file diff --git a/formal-verification/FormalVerification/ReducednessCheck.lean b/formal-verification/FormalVerification/ReducednessCheck.lean new file mode 100644 index 0000000..ea97dc0 --- /dev/null +++ b/formal-verification/FormalVerification/ReducednessCheck.lean @@ -0,0 +1,130 @@ +import ProvenZk +import FormalVerification +import FormalVerification.Common + +open SemaphoreMTB (F Order) + +abbrev orderBinaryLE : Vector Bool 256 := vec![true,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,false,true,true,true,true,true,true,false,false,true,false,false,true,true,false,true,false,true,true,true,true,true,false,false,false,false,true,true,true,true,true,false,false,false,false,true,false,true,false,false,false,true,false,false,true,false,false,false,false,true,true,true,false,true,false,false,true,true,true,false,true,true,false,false,true,true,true,true,false,false,false,false,true,false,false,true,false,false,false,false,true,false,true,true,true,true,true,false,false,true,true,false,false,false,false,false,true,false,true,false,false,true,false,true,true,true,false,true,false,false,false,false,true,true,false,true,false,true,false,false,false,false,false,false,true,true,false,false,false,false,false,false,true,false,true,true,false,true,true,false,true,true,false,true,false,false,false,true,false,false,false,false,false,true,false,true,false,false,false,false,true,true,true,false,true,true,false,false,true,false,true,false,false,false,false,false,false,false,true,false,true,true,false,false,false,true,true,false,false,true,false,false,false,false,true,true,true,false,true,false,false,true,true,true,false,false,true,true,true,false,false,true,false,false,false,true,false,false,true,true,false,false,false,false,false,true,true,false,false] + +def binaryComparisonCircuit + (base : Vector Bool n) + (arg : Vector F n) + (start_ix : ℕ) + (ix_ok : start_ix < n) + (succeeded : F) + (failed : F): Prop := + Gates.is_bool arg[start_ix] ∧ + match base[start_ix] with + | false => + ∃or, Gates.or arg[start_ix] failed or ∧ + ∃failed, Gates.select succeeded 0 or failed ∧ + match start_ix with + | 0 => Gates.eq succeeded 1 + | Nat.succ ix => binaryComparisonCircuit base arg ix (Nat.lt_of_succ_lt ix_ok) succeeded failed + | true => + ∃bit_neg, bit_neg = Gates.sub 1 arg[start_ix] ∧ + ∃or, Gates.or bit_neg succeeded or ∧ + ∃succeeded, Gates.select failed 0 or succeeded ∧ + match start_ix with + | 0 => Gates.eq succeeded 1 + | Nat.succ start_ix => binaryComparisonCircuit base arg start_ix (Nat.lt_of_succ_lt ix_ok) succeeded failed + +theorem ReducedModRCheck_256_Fold {v : Vector F 256} : + binaryComparisonCircuit orderBinaryLE v 255 (by decide) 0 0 ↔ SemaphoreMTB.ReducedModRCheck_256 v := by + repeat (first | intro _ | apply and_congr_right' | apply exists_congr) + tauto + +def binaryComparison (base arg : Vector Bool n) (start_ix : Fin n) (succeeded failed : Bool): Prop := + let (succeeded, failed) := match base[start_ix] with + | false => + let or := arg[start_ix] || failed + let failed := if succeeded then false else or + (succeeded, failed) + | true => + let bit_neg := !arg[start_ix] + let or := bit_neg || succeeded + let succeeded := if failed then false else or + (succeeded, failed) + match start_ix with + | ⟨0, _⟩ => succeeded = true + | ⟨Nat.succ ix, p⟩ => binaryComparison base arg ⟨ix, by linarith⟩ succeeded failed + +theorem binaryComparison_iff_binaryComparisonCircuit {base arg : Vector Bool n} {ix : Nat} {ix_ok : ix < n} {succeeded failed : Bool}: + binaryComparisonCircuit base (arg.map Bool.toZMod) ix ix_ok succeeded.toZMod failed.toZMod ↔ + binaryComparison base arg ⟨ix, by linarith⟩ succeeded failed := by + induction ix generalizing succeeded failed with + | zero => + simp [binaryComparison, binaryComparisonCircuit, getElem] + split <;> simp [*] + | succ n ih => + unfold binaryComparison binaryComparisonCircuit + simp [getElem, ←ih] + split <;> simp [*] + +lemma binaryComparison_failed_always_fails {base arg : Vector Bool n} {i : Fin n}: + ¬binaryComparison base arg i false true := by + rcases i with ⟨i, p⟩ + induction i <;> { + unfold binaryComparison + simp + split <;> { simp [*] } + } + +lemma binaryComparison_succeeded_always_succeeds {base arg : Vector Bool n} {i : Fin n}: + binaryComparison base arg i true false := by + rcases i with ⟨i, p⟩ + induction i <;> { + unfold binaryComparison + simp + split <;> simp [*] + } + +lemma binaryComparison_unused_snoc {a b s f : Bool} { base arg : Vector Bool (Nat.succ n) } {i : ℕ} (hp : i < Nat.succ n): + binaryComparison (base.snoc b) (arg.snoc a) ⟨i, by linarith⟩ s f ↔ + binaryComparison base arg ⟨i, hp⟩ s f := by + induction i generalizing s f with + | zero => + unfold binaryComparison + simp [Vector.getElem_snoc_before_length] + | succ i ih => + unfold binaryComparison + have : i < n.succ := by linarith + simp [Vector.getElem_snoc_before_length hp, Vector.getElem_snoc_at_length, ih (hp := this)] + +theorem binaryComparison_is_comparison {base arg : Vector Bool (Nat.succ n)}: + binaryComparison base arg ⟨n, by simp⟩ false false ↔ + (Fin.ofBitsLE base).val > (Fin.ofBitsLE arg).val := by + induction n with + | zero => + simp only [←Bool.toZMod_zero] + cases base using Vector.casesOn; rename_i bhd btl; cases btl using Vector.casesOn + cases arg using Vector.casesOn; rename_i ahd atl; cases atl using Vector.casesOn + unfold binaryComparison + cases ahd <;> cases bhd <;> simp + | succ n ih => + cases base using Vector.revCasesOn with | snoc binit blast => + cases arg using Vector.revCasesOn with | snoc ainit alast => + simp only [←Bool.toZMod_zero] + unfold Fin.ofBitsLE Fin.ofBitsBE binaryComparison + simp [Vector.getElem_snoc_at_length, binaryComparison_unused_snoc] + cases alast <;> cases blast + . simp [ih, Fin.ofBitsLE] + . simp [binaryComparison_succeeded_always_succeeds, Bool.toNat] + apply Nat.lt_of_lt_of_le (Fin.is_lt _) + simp + . simp [binaryComparison_failed_always_fails, Bool.toNat] + apply Nat.le_trans (Nat.le_of_lt (Fin.is_lt _)) + simp + . simp [ih, Fin.ofBitsLE] + +theorem fin_ofBitsLE_orderBinaryLE_eq_order : + Fin.ofBitsLE orderBinaryLE = Order := by rfl + +theorem ReducedModRCheck_256_semantics {v : Vector Bool 256}: + SemaphoreMTB.ReducedModRCheck_256 (v.map Bool.toZMod) ↔ (Fin.ofBitsLE v).val < Order := by + rw [ ←ReducedModRCheck_256_Fold + , ←Bool.toZMod_zero + , binaryComparison_iff_binaryComparisonCircuit + , binaryComparison_is_comparison + , fin_ofBitsLE_orderBinaryLE_eq_order] + simp [Nat.mod_eq_of_lt] diff --git a/formal-verification/FormalVerification/SemanticEquivalence.lean b/formal-verification/FormalVerification/SemanticEquivalence.lean deleted file mode 100644 index de88125..0000000 --- a/formal-verification/FormalVerification/SemanticEquivalence.lean +++ /dev/null @@ -1,317 +0,0 @@ -import ProvenZk.Binary -import ProvenZk.Hash -import ProvenZk.Merkle -import ProvenZk.Misc - -import FormalVerification -import FormalVerification.Poseidon.Spec -import FormalVerification.Poseidon.Correctness - -open SemaphoreMTB (F Order) - -variable [Fact (Nat.Prime Order)] - -abbrev D := 30 -- Tree depth -abbrev B := 4 -- Batch sizes -open SemaphoreMTB renaming VerifyProof_31_30 → gVerifyProof -open SemaphoreMTB renaming DeletionRound_30_30 → gDeletionRound -open SemaphoreMTB renaming DeletionProof_4_4_30_4_4_30 → gDeletionProof -open SemaphoreMTB renaming InsertionRound_30_30 → gInsertionRound -open SemaphoreMTB renaming InsertionProof_4_30_4_4_30 → gInsertionProof - --- Poseidon semantic equivalence - -def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0 - -lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : SemaphoreMTB.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by - simp [SemaphoreMTB.Poseidon2, poseidon₂, poseidon_3_correct, getElem] - rfl - --- Verify Proof semantic equivalence - -/-! -`ProofRound_uncps` proves that `SemaphoreMTB.ProofRound` is equivalent to a -single iteration of `MerkleTree.recover_tail` --/ -lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} : - SemaphoreMTB.ProofRound direction hash sibling k ↔ - is_bit direction ∧ k (match Dir.nat_to_dir direction.val with - | Dir.left => poseidon₂ vec![sibling, hash] - | Dir.right => poseidon₂ vec![hash, sibling]) := by - simp [SemaphoreMTB.ProofRound, Gates.is_bool, Gates.select, Gates.is_bool] - intro hb - cases hb <;> { - simp [*] - simp [Dir.nat_to_dir, ZMod.val, Order] - rw [Poseidon2_uncps] - } - -/-! -`proof_rounds` rewrites `SemaphoreMTB.VerifyProof_31_30` with recursion using `proof_rounds` --/ -def proof_rounds (Siblings : Vector F (n+1)) (PathIndices : Vector F n) (k : F -> Prop) : Prop := - match n with - | Nat.zero => k Siblings.head - | Nat.succ _ => SemaphoreMTB.ProofRound PathIndices.head Siblings.tail.head Siblings.head fun next => - proof_rounds (next ::ᵥ Siblings.tail.tail) PathIndices.tail k - -/-! -`proof_rounds_uncps` rewrites `proof_rounds` using the corresponding operations of `MerkleTree` library --/ -lemma proof_rounds_uncps - {Leaf : F} - {Siblings : Vector F n} - {PathIndices : Vector F n} - {k : F -> Prop}: - proof_rounds (Leaf ::ᵥ Siblings) PathIndices k ↔ - is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings Leaf) := by - induction PathIndices, Siblings using Vector.inductionOn₂ generalizing Leaf with - | nil => - simp [is_vector_binary] - rfl - | @cons n ix sib ixes sibs ih => - simp [MerkleTree.recover_tail_reverse_equals_recover, MerkleTree.recover_tail, proof_rounds] - simp [ProofRound_uncps, is_vector_binary_cons, and_assoc, ih] - intros - rfl - -/-! -`VerifyProof_looped` proves that `SemaphoreMTB.VerifyProof_31_30` is identical to `proof_rounds` --/ -lemma VerifyProof_looped (PathIndices: Vector F D) (Siblings: Vector F (D+1)) (k: F -> Prop): - gVerifyProof Siblings PathIndices k = - proof_rounds Siblings PathIndices k := by - unfold gVerifyProof - simp [proof_rounds] - rw [←Vector.ofFn_get (v := PathIndices)] - rw [←Vector.ofFn_get (v := Siblings)] - rfl - -/-! -`VerifyProof_uncps` proves that `SemaphoreMTB.VerifyProof_31_30` is identical to `MerkleTree.recover_tail` --/ -lemma VerifyProof_uncps {PathIndices: Vector F D} {Siblings: Vector F (D+1)} {k : F -> Prop}: - gVerifyProof (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔ - is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings.tail Siblings.head) := by - simp only [VerifyProof_looped, proof_rounds_uncps] - --- Deletion round semantic equivalence - -/-! -We need to prove that `DeletionRound_30` checks that `MerkleTree.recover_tail` = `root` and returns `MerkleTree.recover_tail` with empty Leaf: -this is shown in `DeletionRound_uncps`. -Then we need to show that `DeletionProof_4_4_30_4` is continuous application of `DeletionLoop` --/ - -lemma sub_zero_is_eq {a b cond : F} {k: F -> Prop}: - (fun gate_2 => - ∃gate_3, gate_3 = Gates.sub a b ∧ -- gate_3 = a - b - ∃gate_4, Gates.is_zero gate_3 gate_4 ∧ -- gate_4 = (a - b) == 0 = a == b - ∃gate_5, Gates.or gate_4 cond gate_5 ∧ -- gate_5 = (a == b) ∨ cond - Gates.eq gate_5 (1:F) ∧ -- gate_5 == 1 - ∃gate_7, Gates.select cond b gate_2 gate_7 ∧ -- return $ if cond then b else gate_2 - k gate_7) = (fun gate_2 => is_bit cond ∧ match zmod_to_bit cond with - | Bit.zero => (a = b) ∧ k gate_2 -- Update the root - | Bit.one => k b -- Skip flag set, don't update the root - ) := by - funext g2 - simp - unfold Gates.select - simp [or_rw] - unfold Gates.sub - unfold Gates.is_zero - unfold Gates.is_bool - unfold Gates.eq - apply Iff.intro - . intros; casesm* (∃ _, _), (_∧ _) - rename (cond = 0 ∨ cond = 1) => hp - cases hp - . simp at *; subst_vars; simp at *; subst_vars; simp at * - apply And.intro - . tauto - . apply And.intro - . apply eq_of_sub_eq_zero; assumption - . assumption - . subst_vars - apply And.intro - . tauto - . simp at *; subst_vars; assumption - . rintro ⟨is_b, rest⟩ - cases is_b <;> ( - subst_vars - conv at rest => whnf - ) - . cases rest; subst_vars; simp; assumption - . simp - cases h: decide (a - b = 0) with - | false => - simp at h; - exists 0 - apply And.intro - . tauto - . exists 1; tauto - | true => - simp at h; - exists 1; - apply And.intro - . tauto - . exists 1; tauto - -/-! -`DeletionRound_uncps` proves that a single round of the deletion loop corresponds to checking that -the result of `MerkleTree.recover_tail` matches `Root` and returns the hash of the merkle tree with empty Leaf --/ -lemma DeletionRound_uncps {Root: F} {Index: F} {Item: F} {Proof: Vector F D} {k: F -> Prop} : - gDeletionRound Root Index Item Proof k ↔ - ∃out: Vector F (D+1), recover_binary_zmod' out = Index ∧ is_vector_binary out ∧ - (is_bit out.last ∧ match zmod_to_bit out.last with - | Bit.zero => (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out).dropLast Proof Item = Root) ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out).dropLast Proof 0) -- Update the root - | Bit.one => k Root -- Skip flag set, don't update the root - ) := by - unfold gDeletionRound - simp only [sub_zero_is_eq] - simp [VerifyProof_looped, proof_rounds_uncps] - simp [Gates.to_binary, and_assoc] - apply exists_congr - simp - intros - subst_vars - rename_i gate_0 h - rw [←Vector.ofFn_get (v := gate_0)] - rw [←Vector.ofFn_get (v := gate_0)] at h - rw [←Vector.ofFn_get (v := Proof)] - rw [and_iff_right] - tauto - have : is_vector_binary (gate_0.dropLast) := by - simp at h - apply is_vector_binary_dropLast - assumption - rw [←Vector.ofFn_get (v := gate_0)] - rw [←Vector.ofFn_get (v := gate_0)] at this - assumption - -/-! -`deletion_rounds` rewrites `DeletionProof_4_4_30_4` using pattern matching and recursion on the batch size --/ -def deletion_rounds {n} (DeletionIndices: Vector F n) (PreRoot: F) (IdComms: Vector F n) (MerkleProofs: Vector (Vector F D) n) (k : F -> Prop) : Prop := - match n with - | Nat.zero => k PreRoot - | Nat.succ _ => gDeletionRound PreRoot DeletionIndices.head IdComms.head MerkleProofs.head fun next => - deletion_rounds DeletionIndices.tail next IdComms.tail MerkleProofs.tail k - -/-! -`DeletionLoop` rewrites `DeletionProof_4_4_30_4` using pattern matching and recursion on the batch size through by chaining -calls to `MerkleTree.recover_tail`. Ultimately we show that `DeletionLoop` is formally identical to `DeletionProof_4_4_30_4` --/ -def DeletionLoop {n} (DeletionIndices: Vector F n) (PreRoot: F) (IdComms: Vector F n) (MerkleProofs: Vector (Vector F D) n) (k : F -> Prop) : Prop := - match n with - | Nat.zero => k PreRoot - | Nat.succ _ => - ∃out: Vector F (D+1), recover_binary_zmod' out = DeletionIndices.head ∧ is_vector_binary out ∧ - is_bit out.last ∧ match zmod_to_bit out.last with - | Bit.zero => MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out).dropLast MerkleProofs.head IdComms.head = PreRoot ∧ - DeletionLoop DeletionIndices.tail (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out).dropLast MerkleProofs.head 0) IdComms.tail MerkleProofs.tail k -- Update the root - | Bit.one => DeletionLoop DeletionIndices.tail PreRoot IdComms.tail MerkleProofs.tail k -- Skip flag set, don't update the root - -lemma deletion_rounds_uncps {n} {DeletionIndices: Vector F n} {PreRoot: F} {IdComms: Vector F n} {MerkleProofs: Vector (Vector F D) n} {k : F -> Prop}: - deletion_rounds DeletionIndices PreRoot IdComms MerkleProofs k ↔ - DeletionLoop DeletionIndices PreRoot IdComms MerkleProofs k := by - induction DeletionIndices, IdComms, MerkleProofs using Vector.inductionOn₃ generalizing PreRoot with - | nil => - unfold deletion_rounds - unfold DeletionLoop - rfl - | cons => - unfold deletion_rounds - unfold DeletionLoop - simp [DeletionRound_uncps] - rename_i ih - simp [ih] - -lemma DeletionProof_looped (DeletionIndices: Vector F B) (PreRoot: F) (IdComms: Vector F B) (MerkleProofs: Vector (Vector F D) B) (k: F -> Prop) : - gDeletionProof DeletionIndices PreRoot IdComms MerkleProofs k = - deletion_rounds DeletionIndices PreRoot IdComms MerkleProofs k := by - unfold gDeletionProof - simp [deletion_rounds] - rw [←Vector.ofFn_get (v := DeletionIndices)] - rw [←Vector.ofFn_get (v := IdComms)] - rw [←Vector.ofFn_get (v := MerkleProofs)] - rfl - -/-! -`DeletionProof_uncps` is the key lemma which shows that `DeletionProof_4_4_30_4` and `DeletionLoop` are equivalent --/ -lemma DeletionProof_uncps {DeletionIndices: Vector F B} {PreRoot: F} {IdComms: Vector F B} {MerkleProofs: Vector (Vector F D) B} {k: F -> Prop}: - gDeletionProof DeletionIndices PreRoot IdComms MerkleProofs k ↔ - DeletionLoop DeletionIndices PreRoot IdComms MerkleProofs k := by - simp only [DeletionProof_looped, deletion_rounds_uncps] - --- Insertion round semantic equivalence - -def insertion_round (Index: F) (Item: F) (PrevRoot: F) (Proof: Vector F D) (k: F -> Prop) : Prop := - ∃out: Vector F D, recover_binary_zmod' out = Index ∧ is_vector_binary out ∧ - (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out) Proof 0 = PrevRoot) ∧ - k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out) Proof Item) - -lemma InsertionRound_uncps {Index: F} {Item: F} {PrevRoot: F} {Proof: Vector F D} {k: F -> Prop} : - gInsertionRound Index Item PrevRoot Proof k ↔ - insertion_round Index Item PrevRoot Proof k := by - simp [insertion_round] - simp [gInsertionRound] - simp [Gates.to_binary, Gates.eq] - simp [VerifyProof_looped, proof_rounds_uncps] - simp [and_assoc] - apply exists_congr - intros - simp [double_prop] - rename_i gate - rw [←Vector.ofFn_get (v := gate)] - rw [←Vector.ofFn_get (v := Proof)] - tauto - -def insertion_rounds {n} (StartIndex: F) (PreRoot: F) (IdComms: Vector F n) (MerkleProofs: Vector (Vector F D) n) (k : F -> Prop) : Prop := - match n with - | Nat.zero => k PreRoot - | Nat.succ _ => gInsertionRound StartIndex IdComms.head PreRoot MerkleProofs.head fun next => - insertion_rounds (StartIndex + 1) next IdComms.tail MerkleProofs.tail k - -def InsertionLoop {n} (StartIndex: F) (PreRoot: F) (IdComms: Vector F n) (MerkleProofs: Vector (Vector F D) n) (k : F -> Prop) : Prop := - match n with - | Nat.zero => k PreRoot - | Nat.succ _ => - ∃out: Vector F D, recover_binary_zmod' out = StartIndex ∧ is_vector_binary out ∧ - MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out) MerkleProofs.head 0 = PreRoot ∧ - InsertionLoop (StartIndex + 1) (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec out) MerkleProofs.head IdComms.head) IdComms.tail MerkleProofs.tail k - -lemma insertion_rounds_uncps {n} {StartIndex: F} {PreRoot: F} {IdComms: Vector F n} {MerkleProofs: Vector (Vector F D) n} {k : F -> Prop}: - insertion_rounds StartIndex PreRoot IdComms MerkleProofs k ↔ - InsertionLoop StartIndex PreRoot IdComms MerkleProofs k := by - induction IdComms, MerkleProofs using Vector.inductionOn₂ generalizing StartIndex PreRoot with - | nil => - unfold insertion_rounds - unfold InsertionLoop - rfl - | cons => - unfold insertion_rounds - unfold InsertionLoop - simp [InsertionRound_uncps, insertion_round] - rename_i ih - simp [ih] - -lemma InsertionProof_looped (StartIndex: F) (PreRoot: F) (IdComms: Vector F B) (MerkleProofs: Vector (Vector F D) B) (k: F -> Prop) : - gInsertionProof StartIndex PreRoot IdComms MerkleProofs k = - insertion_rounds StartIndex PreRoot IdComms MerkleProofs k := by - unfold gInsertionProof - simp [insertion_rounds] - simp [InsertionRound_uncps] - simp [Gates.add] - rw [add_assoc] - rw [add_assoc] - rw [←Vector.ofFn_get (v := IdComms)] - rw [←Vector.ofFn_get (v := MerkleProofs)] - rfl - -lemma InsertionProof_uncps {StartIndex: F} {PreRoot: F} {IdComms: Vector F B} {MerkleProofs: Vector (Vector F D) B} {k: F -> Prop}: - gInsertionProof StartIndex PreRoot IdComms MerkleProofs k ↔ - InsertionLoop StartIndex PreRoot IdComms MerkleProofs k := by - simp only [InsertionProof_looped, insertion_rounds_uncps] \ No newline at end of file diff --git a/formal-verification/Main.lean b/formal-verification/Main.lean index 9060d7c..a8b51ce 100644 --- a/formal-verification/Main.lean +++ b/formal-verification/Main.lean @@ -1,140 +1,360 @@ -import ProvenZk.Binary -import ProvenZk.Hash -import ProvenZk.Merkle -import ProvenZk.Ext.Vector - +import ProvenZk import FormalVerification -import FormalVerification.Poseidon.Spec -import FormalVerification.Poseidon.Correctness -import FormalVerification.SemanticEquivalence +import FormalVerification.Insertion +import FormalVerification.Deletion +import FormalVerification.Common +import FormalVerification.Poseidon +import FormalVerification.InputHashing +import FormalVerification.ReducednessCheck +import FormalVerification.BinaryDecompositions open SemaphoreMTB (F Order) -variable [Fact (Nat.Prime Order)] - -open SemaphoreMTB renaming VerifyProof_31_30 → gVerifyProof -open SemaphoreMTB renaming DeletionRound_30_30 → gDeletionRound -open SemaphoreMTB renaming DeletionProof_4_4_30_4_4_30 → gDeletionProof -open SemaphoreMTB renaming InsertionRound_30_30 → gInsertionRound -open SemaphoreMTB renaming InsertionProof_4_30_4_4_30 → gInsertionProof - -def TreeInsert [Fact (perfect_hash poseidon₂)] (Tree : MerkleTree F poseidon₂ D) (Index Item : F) (Proof : Vector F D) (k : F → Prop): Prop := - MerkleTree.item_at_nat Tree Index.val = some 0 ∧ - MerkleTree.proof_at_nat Tree Index.val = some Proof.reverse ∧ - ∃postTree, MerkleTree.set_at_nat Tree Index.val Item = some postTree ∧ - k postTree.root - -theorem insertion_round_uncps [Fact (perfect_hash poseidon₂)] (Tree : MerkleTree F poseidon₂ D) (Index Item : F) (Proof : Vector F D) (k : F → Prop): - insertion_round Index Item Tree.root Proof k ↔ - TreeInsert Tree Index Item Proof k := by - unfold insertion_round - unfold TreeInsert - apply Iff.intro - . rintro ⟨ixbin, _⟩ - casesm* (_ ∧ _) - have : nat_to_bits_le D Index.val = some (vector_zmod_to_bit ixbin) := by - apply recover_binary_zmod'_to_bits_le - . simp - . assumption - . rename_i h _ _ _; simp[h] - unfold MerkleTree.item_at_nat - unfold MerkleTree.proof_at_nat - unfold MerkleTree.set_at_nat - unfold Dir.nat_to_dir_vec - rw [this] - simp [←Dir.create_dir_vec_bit] - rename_i h₀ h₁ h₂ h₃ - refine ⟨?_, ⟨?_, ?_⟩⟩ - . apply MerkleTree.proof_ceritfies_item (proof := Proof.reverse) - rw [←MerkleTree.recover_tail_reverse_equals_recover] - simp [h₂] - . apply MerkleTree.recover_proof_reversible - rw [←MerkleTree.recover_tail_reverse_equals_recover (item := (0:F))] - simp [h₂] - . rw [←MerkleTree.proof_insert_invariant (proof := Proof.reverse) (old := 0)] - . rw [←MerkleTree.recover_tail_reverse_equals_recover] - simp [h₃] - . rw [←MerkleTree.recover_tail_reverse_equals_recover] - simp [h₂] - . rintro ⟨hitem, ⟨hproof, ⟨ftree, ⟨hftree, hresult⟩⟩⟩⟩ - simp [MerkleTree.item_at_nat, Dir.nat_to_dir_vec] at hitem - rcases hitem with ⟨bits, ⟨hbits, hitem_at⟩⟩ - simp [MerkleTree.proof_at_nat, Dir.nat_to_dir_vec] at hproof - rcases hproof with ⟨bits', ⟨hbits', hproof_at⟩⟩ - simp [hbits] at hbits' - simp [hbits'] at * - simp [MerkleTree.set_at_nat, Dir.nat_to_dir_vec] at hftree - rcases hftree with ⟨bits'', ⟨hbits'', hftree_at⟩⟩ - simp [hbits''] at hbits - rw [←Vector.vector_reverse_eq] at hproof_at - simp [hbits] at * - simp [<-hproof_at] - let t : Vector F D := (Vector.map Bit.toZMod bits') - refine ⟨t, ?_⟩ - refine ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩ - . apply recover_binary_of_to_bits - simp [hbits''] - . apply vector_binary_of_bit_to_zmod - . rw [MerkleTree.recover_tail_equals_recover_reverse, Dir.create_dir_vec_bit, zmod_to_bit_coe, ←hitem_at] - simp [MerkleTree.recover_proof_is_root] - . rw [<-hftree_at] at hresult - rw [MerkleTree.recover_tail_equals_recover_reverse, Dir.create_dir_vec_bit, zmod_to_bit_coe] - rw [MerkleTree.proof_insert_invariant _] - . apply hresult - . exact 0 - . rw [← hitem_at] - simp [MerkleTree.recover_proof_is_root] - -theorem before_insertion_all_items_zero_loop - [Fact (perfect_hash poseidon₂)] - {Tree: MerkleTree F poseidon₂ D} - {StartIndex B: Nat} - {ixBound: StartIndex + B < Order} - {IdComms: Vector F B} {MerkleProofs: Vector (Vector F D) B} {k: F -> Prop}: - insertion_rounds ↑StartIndex Tree.root IdComms MerkleProofs k → - (∀ i ∈ [StartIndex:StartIndex + B], MerkleTree.item_at_nat Tree i = some 0) := by - induction B generalizing StartIndex Tree with - | zero => - intro _ i range - rcases range with ⟨lo, hi⟩ - have := Nat.ne_of_lt (Nat.lt_of_le_of_lt lo hi) - contradiction - | succ B ih => - intro hp i range - rcases range with ⟨lo, hi⟩; simp at lo hi - have hStartIndexCast : ZMod.val (StartIndex : F) = StartIndex := by - apply ZMod.val_cast_of_lt + +namespace Poseidon + +/-- +Tests the Poseidon implementation automatically derived from the circuit, by +comparing its output on an arbitrary value to a reference value. + +The reference value is taken from + +-/ +theorem poseidon₂_test: + poseidon₂ vec![1,2] = 0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a + := by native_decide + +end Poseidon + +namespace Deletion + +/-- +States the exact semantics of the deletion circuit. +Whenever the circuit is satisfied, there exists a Merkle tree, such that: +1. its root is equal to the one given as the `postRoot` input; +2. for every index `i` in `deletionIndices`, the value at index `i` is zero; +3. for every index `i` not in `deletionIndices`, the value at index `i` is + unchanged. +-/ +theorem root_transformation_correct + [Fact (CollisionResistant poseidon₂)] + {tree : MerkleTree F poseidon₂ D}: + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 inputHash deletionIndices tree.root postRoot identities merkleProofs → + ∃(postTree : MerkleTree F poseidon₂ D), + postTree.root = postRoot ∧ + (∀ i ∈ deletionIndices, postTree[i.val]! = 0) ∧ + (∀ i, i ∉ deletionIndices → postTree[i.val]! = tree[i.val]!) + := by + intro hp + replace hp := Deletion_skipHashing hp + rw [deletionProofCircuit_eq_deletionRoundsSemantics] at hp + replace hp := deletionRounds_rootTransformation hp + rcases hp with ⟨postTree, treeTrans, rootTrans⟩ + exists postTree + refine ⟨rootTrans, ?inrange, ?outrange⟩ + . intro i hi + apply treeTranform_get_present treeTrans hi + . intro i hi + simp [getElem!_eq_getElem?_get!] + apply congrArg + apply treeTransform_get_absent treeTrans hi + +/-- +States that for any given tree and list of valid indices, there exists a choice +of other parameters, such that the deletion circuit is satisfied. As a corollary, +we can be certain that the system will always be able to remove any identity from +the tree. +NB indices are consider valid if they are less than 2ᴰ⁺¹, where D is the merkle +tree depth. This allows the circuit to use indices larger than the tree size to +pad batches. +-/ +theorem assignment_exists + [Fact (CollisionResistant poseidon₂)] + {tree : MerkleTree F poseidon₂ D} + {indices : Vector F B}: + (∀i ∈ indices, i.val < 2^(D+1)) → + ∃inputHash identities proofs postRoot, SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 inputHash indices tree.root postRoot identities proofs + := by + intro h; + simp only [DeletionCircuit_folded, DeletionMbuCircuit_4_4_30_4_4_30_Fold] + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_640_64_24_640_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq, + deletionProofCircuit_eq_deletionRoundsSemantics + ] + have := exists_assignment (tree := tree) h + rcases this with ⟨_, _, _, hp⟩ + repeat apply Exists.intro + apply And.intro (Eq.refl _) + simp + apply hp + simp only [D] at h + all_goals { + apply Nat.lt_trans _ ((by decide) : 2 ^ 31 < 2 ^ 32) + apply h + simp [getElem] + } + +/-- +Establishes that the deletion circuit's InputHash parameter is uniquely +determined by DeletionIndices, PreRoot and PostRoot. That is done by showing +that any two valid assigments that agree on those parameters, must also agree +on InputHash. +-/ +theorem inputHash_deterministic: + (SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash₁ DeletionIndices PreRoot PostRoot IdComms₁ MerkleProofs₁ ∧ + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash₂ DeletionIndices PreRoot PostRoot IdComms₂ MerkleProofs₂) + → InputHash₁ = InputHash₂ + := Deletion_InputHash_deterministic + +/-- +Arbitrary string used for testing the 640-bit keccak hash implementation. +-/ +def testString80 : String := + "This string is exactly 80 bytes long, which is unbelievably lucky for this test." + +/-- +An embedding of the test string into a vector of bits, by taking the little-endian +bit decomposition of the ASCII value of each character. +-/ +def testVector640 : Vector Bool 640 := + Subtype.mk (testString80.toUTF8.toList.map (fun b => Vector.toList $ Fin.toBitsLE (d := 8) b.val)).join (by native_decide) + +/-- +Tests the Keccak implementation automatically derived from the circuit, by +comparing its output on an arbitrary value to a reference value computed using +solidity. + +The reference number is obtained by hashing the test string using the following Solidity code: +```solidity +string memory data = "This string is exactly 80 bytes long, which is unbelievably lucky for this test."; +uint256 result; +assembly { + result := mod(keccak256(add(data, 0x20), mload(data)), 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001) +} +``` +-/ +theorem reducedKeccak640_test : + reducedKeccak640 testVector640 = 0x799e635101207dc20689c342be25dc6f5a2f25b51d2a5ac3c9fee51694b3609 := by native_decide + +/-- +This axiom is necessary for the proof of the injectivity of the input hash +parameter. It is obviously not true (e.g. by the pigeonhole principle), but it +captures the usual intuition behind hash functions. +-/ +axiom reducedKeccak640_collision_resistant : + ∀x y, reducedKeccak640 x = reducedKeccak640 y → x = y + +/-- +States that the input hash parameter is injective. That is, if two valid +assignments share the same input hash, then they must agree on all other public +parameters. +-/ +theorem inputHash_injective: + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash DeletionIndices₁ PreRoot₁ PostRoot₁ IdComms₁ MerkleProofs₁ ∧ + SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash DeletionIndices₂ PreRoot₂ PostRoot₂ IdComms₂ MerkleProofs₂ → + DeletionIndices₁ = DeletionIndices₂ ∧ PreRoot₁ = PreRoot₂ ∧ PostRoot₁ = PostRoot₂ + := Deletion_InputHash_injective reducedKeccak640_collision_resistant + +end Deletion + +namespace Insertion + +/-- +Checks input validation on the insertion circuit. The circuit being satisfied +implies that all items at modified indices are zero, therefore it is impossible +to use this circuit to, either accidentally or malicious, overwrite existing +data. +-/ +theorem before_insertion_all_items_zero + [Fact (CollisionResistant poseidon₂)] + {tree: MerkleTree F poseidon₂ D} + {startIndex : F}: + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash startIndex tree.root PostRoot IdComms MerkleProofs → + ∀ i ∈ [startIndex.val:startIndex.val + B], tree[i]! = 0 + := by + intro hp i hir + have hp := Insertion_skipHashing hp + rw [Insertion.insertionRoundsCircuit_eq_insertionRoundsSemantics] at hp + have hp'' := ix_bound hp + rw [getElem!_eq_getElem?_get!] + rw [before_insertion_all_zero hp]; rfl + apply And.intro + . exact hir.1 + . apply Nat.lt_of_lt_of_eq hir.2 + rw [ZMod.val_add, Nat.mod_eq_of_lt] + rfl + calc + startIndex.val + 4 = (startIndex.val + 3) + 1 := by ring + _ < 2^D + 1 := Nat.add_lt_add_right hp'' (k := 1) + _ < Order := by decide + +/-- +States the exact semantics of the insertion circuit. +Whenever the circuit is satisfied, there exists a Merkle tree, such that: +1. its root is equal to the one given as the `postRoot` input; +2. for every index `i` such that `startIndex ≤ i < startIndex + B`, the value + at index `i` is equal to `idComms[i-startIndex]`; +3. for every index `i` outside the specified range, the value at index `i` + remains unchanged. +-/ +theorem root_transformation_correct + [Fact (CollisionResistant poseidon₂)] + {Tree : MerkleTree F poseidon₂ D}: + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex Tree.root PostRoot IdComms MerkleProofs → + ∃(postTree : MerkleTree F poseidon₂ D), + postTree.root = PostRoot ∧ + (∀ i, i ∈ [StartIndex.val:StartIndex.val + B] → postTree[i]! = IdComms[i-StartIndex.val]!) ∧ + (∀ i, i ∉ [StartIndex.val:StartIndex.val + B] → postTree[i]! = Tree[i]!) + := by + intro hp + have hp := Insertion_skipHashing hp + rw [insertionRoundsCircuit_eq_insertionRoundsSemantics] at hp + have hp := insertionRoundsRootTransformation hp + rcases hp with ⟨postTree, treeTrans, rootTrans⟩ + exists postTree + simp_rw [getElem!_eq_getElem?_get!] + refine ⟨rootTrans, ?inrange, ?outrange⟩ + case inrange => + intro i hi + have : i = StartIndex.val + (i - StartIndex.val) := by + rw [add_comm, Nat.sub_add_cancel hi.1] + have i_off_inrange : i - StartIndex.val ∈ [0:B] := by + refine ⟨Nat.zero_le _, ?_⟩ + cases hi linarith - cases lo with - | refl => - simp [insertion_rounds, InsertionRound_uncps, insertion_round_uncps, TreeInsert, hStartIndexCast] at hp - cases hp - rename_i l r - simp [l] - | @step StartIndex' h => - have : (StartIndex : F) + 1 = ((StartIndex + 1 : Nat) : F) := by - simp [Fin.ext] - rw [insertion_rounds, InsertionRound_uncps, insertion_round_uncps, TreeInsert, this] at hp - rcases hp with ⟨_, ⟨_, ⟨postTree, ⟨hinsert, hnext⟩⟩⟩⟩ - rw [←MerkleTree.item_at_nat_invariant hinsert] - apply ih hnext StartIndex'.succ - . apply And.intro - . simp_arith; simp [Nat.le] at h; simp [h] - . simp; linarith + rw [this, treeTransform_get_inrange treeTrans i_off_inrange, ←this] + apply congrArg + apply eq_comm.mp + apply getElem?_eq_some_getElem_of_valid_index + case outrange => + intro i hi + cases Nat.lt_or_ge i StartIndex.val with + | inl h => + apply congrArg + apply eq_comm.mp + apply treeTransform_get_lt treeTrans h + | inr h => + cases Nat.lt_or_ge i (StartIndex.val + B) with + | inl h' => + exfalso + exact hi ⟨h, h'⟩ + | inr h => + apply congrArg + apply eq_comm.mp + apply treeTransform_get_gt treeTrans h + +/-- +States that for any given tree, a valid start index, and a list of identities, +there exists a choice of the other parameters such that the insertion circuit +is satisfied. As a corollary, we can be certain that the system will always be +able to progress, as long as there is enough free space in the tree. + +NB a start index is considered valid if it denotes the beginning of a length-B +block of empty leaves. +-/ +theorem assignment_exists [Fact (CollisionResistant poseidon₂)] {tree : MerkleTree F poseidon₂ D}: + startIndex + B < 2 ^ D ∧ + (∀i ∈ [startIndex : startIndex + B], tree[i]! = 0) → + ∃proofs postRoot inputHash, SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 inputHash startIndex tree.root postRoot idComms proofs + := by + rintro ⟨ix_ok, items_zero⟩ + simp only [InsertionMbuCircuit_4_30_4_4_30_folded] + unfold InsertionMbuCircuit_4_30_4_4_30_Fold + simp only [ + Vector.ofFnGet_id, + ToReducedBigEndian_32_uncps, + ToReducedBigEndian_256_uncps, + RCBitsField_def, + ←Vector.map_permute, + Vector.map_hAppend, + (KeccakGadget_1568_64_24_1568_256_24_1088_1_uniqueAssignment _ _).equiv, + FromBinaryBigEndian_256_uncps, + Gates.eq + ] + simp [insertionRoundsCircuit_eq_insertionRoundsSemantics] + have := exists_assignment (identities := idComms) ix_ok (by + intro i h + apply getElem_of_getElem! + apply items_zero + assumption + ) + rcases this with ⟨proofs, postRoot, h⟩ + exists proofs, postRoot + apply And.intro + . apply Exists.intro + apply Exists.intro + . rfl + . simp only [D, B] at ix_ok + rw [ZMod.val_cast_of_lt] . linarith - . rw [hStartIndexCast] - apply Nat.ne_of_lt - simp_arith; simp [Nat.le] at h; simp [h] + . simp only [Order]; linarith + . exact h -theorem before_insertion_all_items_zero - [Fact (perfect_hash poseidon₂)] - {Tree: MerkleTree F poseidon₂ D} - (StartIndex: Nat) (IdComms: Vector F B) (MerkleProofs: Vector (Vector F D) B) (k: F -> Prop) - {ixBound: StartIndex + B < Order}: - gInsertionProof ↑StartIndex Tree.root IdComms MerkleProofs k → - (∀ i ∈ [StartIndex:StartIndex + B], MerkleTree.item_at_nat Tree i = some 0) := by - rw [InsertionProof_looped] - apply before_insertion_all_items_zero_loop - simp [ixBound] - -def main : IO Unit := pure () \ No newline at end of file +/-- +Establishes that the insertion circuit's InputHash parameter is uniquely +determined by StartIndex, PreRoot, PostRoot and the identity commitments. That +is done by showing that any two valid assigments that agree on those +parameters, must also agree on InputHash. +-/ +theorem inputHash_deterministic: + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash₁ StartIndex PreRoot PostRoot IdComms MerkleProofs₁ ∧ + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash₂ StartIndex PreRoot PostRoot IdComms MerkleProofs₂ → + InputHash₁ = InputHash₂ + := Insertion_InputHash_deterministic + +/-- +Arbitrary string used for testing the 1568-bit keccak hash implementation. +-/ +def testString196 : String := + "This is string is exactly 196 bytes long, which happens to be exactly the length we need to test the 1568-bit keccak hash implementation, that can be found in the SemaphoreMTB Insertion Circuit..." + +/-- +An embedding of the test string into a vector of bits, by taking the little-endian +bit decomposition of the ASCII value of each character. +-/ +def testVector1568 : Vector Bool 1568 := + Subtype.mk (testString196.toUTF8.toList.map (fun b => Vector.toList $ Fin.toBitsLE (d := 8) b.val)).join (by native_decide) + +/-- +The reference number is obtained by hashing the test string using the following Solidity code: +```solidity +string memory data = "This is string is exactly 196 bytes long, which happens to be exactly the length we need to test the 1568-bit keccak hash implementation, that can be found in the SemaphoreMTB Insertion Circuit..."; +uint256 result; +assembly { + result := mod(keccak256(add(data, 0x20), mload(data)), 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001) +} +``` +-/ +theorem reducedKeccak1568_test : + reducedKeccak1568 testVector1568 = 0x204e42742e70b563e147bca3aac705534bfae2e7d17691127dd6425b23f5ba43 := by native_decide + +/-- +This axiom is necessary for the proof of the injectivity of the input hash +parameter. It is obviously not true (e.g. by the pigeonhole principle), but it +captures the usual intuition behind hash functions. +-/ +axiom reducedKeccak1568_collision_resistant : + ∀x y, reducedKeccak1568 x = reducedKeccak1568 y → x = y + +/-- +States that the input hash parameter is injective. That is, if two valid +assignments share the same input hash, then they must agree on all other public +parameters. +-/ +theorem inputHash_injective: + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex₁ PreRoot₁ PostRoot₁ IdComms₁ MerkleProofs₁ ∧ + SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30 InputHash StartIndex₂ PreRoot₂ PostRoot₂ IdComms₂ MerkleProofs₂ → + StartIndex₁ = StartIndex₂ ∧ PreRoot₁ = PreRoot₂ ∧ PostRoot₁ = PostRoot₂ ∧ IdComms₁ = IdComms₂ := + Insertion_InputHash_injective reducedKeccak1568_collision_resistant + +end Insertion + +def main (_ : List String): IO UInt32 := pure 0 diff --git a/formal-verification/lake-manifest.json b/formal-verification/lake-manifest.json index e00d3fa..e2c9d69 100644 --- a/formal-verification/lake-manifest.json +++ b/formal-verification/lake-manifest.json @@ -16,9 +16,9 @@ {"git": {"url": "https://github.com/reilabs/proven-zk.git", "subDir?": null, - "rev": "18e62cc54899ee6e3c06cbeb42c94c8773b48e98", + "rev": "ae9327ec14d84b20f1c17f336ed7698e5b0fbae1", "name": "ProvenZK", - "inputRev?": "v1.1.0"}}, + "inputRev?": "v1.3.0"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, diff --git a/formal-verification/lakefile.lean b/formal-verification/lakefile.lean index e2540b1..f6209ef 100644 --- a/formal-verification/lakefile.lean +++ b/formal-verification/lakefile.lean @@ -9,7 +9,7 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9" require ProvenZK from git - "https://github.com/reilabs/proven-zk.git"@"v1.1.0" + "https://github.com/reilabs/proven-zk.git"@"v1.3.0" lean_lib FormalVerification { moreLeanArgs := #["--tstack=65520", "-DmaxRecDepth=10000", "-DmaxHeartbeats=200000000"]