diff --git a/prover/server/formal-verification/FormalVerification/Circuit.lean b/prover/server/formal-verification/FormalVerification/Circuit.lean index 5ad42ae5a..1f9c7c253 100644 --- a/prover/server/formal-verification/FormalVerification/Circuit.lean +++ b/prover/server/formal-verification/FormalVerification/Circuit.lean @@ -375,13 +375,37 @@ def NonInclusionProof_8_8_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Values: List Gates.eq gate_30 Roots[7] ∧ k vec![gate_2, gate_6, gate_10, gate_14, gate_18, gate_22, gate_26, gate_30] +def HashChain_3 (Hashes: List.Vector F 3) (k: F -> Prop): Prop := + Poseidon2 Hashes[0] Hashes[2] fun gate_0 => + k gate_0 + +def HashChain_8 (Hashes: List.Vector F 8) (k: F -> Prop): Prop := + Poseidon2 Hashes[0] Hashes[2] fun gate_0 => + Poseidon2 gate_0 Hashes[3] fun gate_1 => + Poseidon2 gate_1 Hashes[4] fun gate_2 => + Poseidon2 gate_2 Hashes[5] fun gate_3 => + Poseidon2 gate_3 Hashes[6] fun gate_4 => + Poseidon2 gate_4 Hashes[7] fun gate_5 => + k gate_5 + +def MerkleRootUpdateGadget_26_26_26 (OldRoot: F) (OldLeaf: F) (NewLeaf: F) (PathIndex: List.Vector F 26) (MerkleProof: List.Vector F 26) (k: F -> Prop): Prop := + MerkleRootGadget_26_26_26 OldLeaf PathIndex MerkleProof fun gate_0 => + Gates.eq gate_0 OldRoot ∧ + MerkleRootGadget_26_26_26 NewLeaf PathIndex MerkleProof fun gate_2 => + k gate_2 + +def HashChain_4 (Hashes: List.Vector F 4) (k: F -> Prop): Prop := + Poseidon2 Hashes[0] Hashes[2] fun gate_0 => + Poseidon2 gate_0 Hashes[3] fun gate_1 => + k gate_1 + def InclusionCircuit_8_8_8_26_8_8_26 (PublicInputHash: F) (Roots: List.Vector F 8) (Leaves: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8): Prop := TwoInputsHashChain_8_8 Roots Leaves fun gate_0 => Gates.eq PublicInputHash gate_0 ∧ InclusionProof_8_8_8_26_8_8_26 Roots Leaves InPathIndices InPathElements fun _ => True -def NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 (PublicInputHash: F) (Roots: List.Vector F 8) (Values: List.Vector F 8) (LeafLowerRangeValues: List.Vector F 8) (LeafHigherRangeValues: List.Vector F 8) (NextIndices: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8): Prop := +def NonInclusionCircuit_8_8_8_8_8_26_8_8_26 (PublicInputHash: F) (Roots: List.Vector F 8) (Values: List.Vector F 8) (LeafLowerRangeValues: List.Vector F 8) (LeafHigherRangeValues: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8): Prop := TwoInputsHashChain_8_8 Roots Values fun gate_0 => Gates.eq PublicInputHash gate_0 ∧ NonInclusionProof_8_8_8_8_8_26_8_8_26 Roots Values LeafLowerRangeValues LeafHigherRangeValues InPathIndices InPathElements fun _ => @@ -396,4 +420,108 @@ def CombinedCircuit_8_8_8_26_8_8_8_8_8_8_26_8 (PublicInputHash: F) (Inclusion_Ro NonInclusionProof_8_8_8_8_8_26_8_8_26 NonInclusion_Roots NonInclusion_Values NonInclusion_LeafLowerRangeValues NonInclusion_LeafHigherRangeValues NonInclusion_InPathIndices NonInclusion_InPathElements fun _ => True +def BatchUpdateCircuit_8_8_8_26_8_8_26_8 (PublicInputHash: F) (OldRoot: F) (NewRoot: F) (LeavesHashchainHash: F) (TxHashes: List.Vector F 8) (Leaves: List.Vector F 8) (OldLeaves: List.Vector F 8) (MerkleProofs: List.Vector (List.Vector F 26) 8) (PathIndices: List.Vector F 8): Prop := + HashChain_3 vec![OldRoot, NewRoot, LeavesHashchainHash] fun gate_0 => + Gates.eq gate_0 PublicInputHash ∧ + Poseidon3 Leaves[0] PathIndices[0] TxHashes[0] fun gate_2 => + Poseidon3 Leaves[1] PathIndices[1] TxHashes[1] fun gate_3 => + Poseidon3 Leaves[2] PathIndices[2] TxHashes[2] fun gate_4 => + Poseidon3 Leaves[3] PathIndices[3] TxHashes[3] fun gate_5 => + Poseidon3 Leaves[4] PathIndices[4] TxHashes[4] fun gate_6 => + Poseidon3 Leaves[5] PathIndices[5] TxHashes[5] fun gate_7 => + Poseidon3 Leaves[6] PathIndices[6] TxHashes[6] fun gate_8 => + Poseidon3 Leaves[7] PathIndices[7] TxHashes[7] fun gate_9 => + HashChain_8 vec![gate_2, gate_3, gate_4, gate_5, gate_6, gate_7, gate_8, gate_9] fun gate_10 => + Gates.eq gate_10 LeavesHashchainHash ∧ + ∃gate_12, Gates.to_binary PathIndices[0] 26 gate_12 ∧ + MerkleRootUpdateGadget_26_26_26 OldRoot OldLeaves[0] gate_2 gate_12 MerkleProofs[0] fun gate_13 => + ∃gate_14, Gates.to_binary PathIndices[1] 26 gate_14 ∧ + MerkleRootUpdateGadget_26_26_26 gate_13 OldLeaves[1] gate_3 gate_14 MerkleProofs[1] fun gate_15 => + ∃gate_16, Gates.to_binary PathIndices[2] 26 gate_16 ∧ + MerkleRootUpdateGadget_26_26_26 gate_15 OldLeaves[2] gate_4 gate_16 MerkleProofs[2] fun gate_17 => + ∃gate_18, Gates.to_binary PathIndices[3] 26 gate_18 ∧ + MerkleRootUpdateGadget_26_26_26 gate_17 OldLeaves[3] gate_5 gate_18 MerkleProofs[3] fun gate_19 => + ∃gate_20, Gates.to_binary PathIndices[4] 26 gate_20 ∧ + MerkleRootUpdateGadget_26_26_26 gate_19 OldLeaves[4] gate_6 gate_20 MerkleProofs[4] fun gate_21 => + ∃gate_22, Gates.to_binary PathIndices[5] 26 gate_22 ∧ + MerkleRootUpdateGadget_26_26_26 gate_21 OldLeaves[5] gate_7 gate_22 MerkleProofs[5] fun gate_23 => + ∃gate_24, Gates.to_binary PathIndices[6] 26 gate_24 ∧ + MerkleRootUpdateGadget_26_26_26 gate_23 OldLeaves[6] gate_8 gate_24 MerkleProofs[6] fun gate_25 => + ∃gate_26, Gates.to_binary PathIndices[7] 26 gate_26 ∧ + MerkleRootUpdateGadget_26_26_26 gate_25 OldLeaves[7] gate_9 gate_26 MerkleProofs[7] fun gate_27 => + Gates.eq gate_27 NewRoot ∧ + True + +def BatchAddressTreeAppendCircuit_8_8_8_26_8_8_26_8_8_26 (PublicInputHash: F) (OldRoot: F) (NewRoot: F) (HashchainHash: F) (StartIndex: F) (LowElementValues: List.Vector F 8) (LowElementNextValues: List.Vector F 8) (LowElementIndices: List.Vector F 8) (LowElementProofs: List.Vector (List.Vector F 26) 8) (NewElementValues: List.Vector F 8) (NewElementProofs: List.Vector (List.Vector F 26) 8): Prop := + LeafHashGadget LowElementValues[0] LowElementNextValues[0] NewElementValues[0] fun gate_0 => + Poseidon2 LowElementValues[0] NewElementValues[0] fun gate_1 => + ∃gate_2, Gates.to_binary LowElementIndices[0] 26 gate_2 ∧ + MerkleRootUpdateGadget_26_26_26 OldRoot gate_0 gate_1 gate_2 LowElementProofs[0] fun gate_3 => + Poseidon2 NewElementValues[0] LowElementNextValues[0] fun gate_4 => + ∃gate_5, gate_5 = Gates.add StartIndex (0:F) ∧ + ∃gate_6, Gates.to_binary gate_5 26 gate_6 ∧ + MerkleRootUpdateGadget_26_26_26 gate_3 (0:F) gate_4 gate_6 NewElementProofs[0] fun gate_7 => + LeafHashGadget LowElementValues[1] LowElementNextValues[1] NewElementValues[1] fun gate_8 => + Poseidon2 LowElementValues[1] NewElementValues[1] fun gate_9 => + ∃gate_10, Gates.to_binary LowElementIndices[1] 26 gate_10 ∧ + MerkleRootUpdateGadget_26_26_26 gate_7 gate_8 gate_9 gate_10 LowElementProofs[1] fun gate_11 => + Poseidon2 NewElementValues[1] LowElementNextValues[1] fun gate_12 => + ∃gate_13, gate_13 = Gates.add StartIndex (1:F) ∧ + ∃gate_14, Gates.to_binary gate_13 26 gate_14 ∧ + MerkleRootUpdateGadget_26_26_26 gate_11 (0:F) gate_12 gate_14 NewElementProofs[1] fun gate_15 => + LeafHashGadget LowElementValues[2] LowElementNextValues[2] NewElementValues[2] fun gate_16 => + Poseidon2 LowElementValues[2] NewElementValues[2] fun gate_17 => + ∃gate_18, Gates.to_binary LowElementIndices[2] 26 gate_18 ∧ + MerkleRootUpdateGadget_26_26_26 gate_15 gate_16 gate_17 gate_18 LowElementProofs[2] fun gate_19 => + Poseidon2 NewElementValues[2] LowElementNextValues[2] fun gate_20 => + ∃gate_21, gate_21 = Gates.add StartIndex (2:F) ∧ + ∃gate_22, Gates.to_binary gate_21 26 gate_22 ∧ + MerkleRootUpdateGadget_26_26_26 gate_19 (0:F) gate_20 gate_22 NewElementProofs[2] fun gate_23 => + LeafHashGadget LowElementValues[3] LowElementNextValues[3] NewElementValues[3] fun gate_24 => + Poseidon2 LowElementValues[3] NewElementValues[3] fun gate_25 => + ∃gate_26, Gates.to_binary LowElementIndices[3] 26 gate_26 ∧ + MerkleRootUpdateGadget_26_26_26 gate_23 gate_24 gate_25 gate_26 LowElementProofs[3] fun gate_27 => + Poseidon2 NewElementValues[3] LowElementNextValues[3] fun gate_28 => + ∃gate_29, gate_29 = Gates.add StartIndex (3:F) ∧ + ∃gate_30, Gates.to_binary gate_29 26 gate_30 ∧ + MerkleRootUpdateGadget_26_26_26 gate_27 (0:F) gate_28 gate_30 NewElementProofs[3] fun gate_31 => + LeafHashGadget LowElementValues[4] LowElementNextValues[4] NewElementValues[4] fun gate_32 => + Poseidon2 LowElementValues[4] NewElementValues[4] fun gate_33 => + ∃gate_34, Gates.to_binary LowElementIndices[4] 26 gate_34 ∧ + MerkleRootUpdateGadget_26_26_26 gate_31 gate_32 gate_33 gate_34 LowElementProofs[4] fun gate_35 => + Poseidon2 NewElementValues[4] LowElementNextValues[4] fun gate_36 => + ∃gate_37, gate_37 = Gates.add StartIndex (4:F) ∧ + ∃gate_38, Gates.to_binary gate_37 26 gate_38 ∧ + MerkleRootUpdateGadget_26_26_26 gate_35 (0:F) gate_36 gate_38 NewElementProofs[4] fun gate_39 => + LeafHashGadget LowElementValues[5] LowElementNextValues[5] NewElementValues[5] fun gate_40 => + Poseidon2 LowElementValues[5] NewElementValues[5] fun gate_41 => + ∃gate_42, Gates.to_binary LowElementIndices[5] 26 gate_42 ∧ + MerkleRootUpdateGadget_26_26_26 gate_39 gate_40 gate_41 gate_42 LowElementProofs[5] fun gate_43 => + Poseidon2 NewElementValues[5] LowElementNextValues[5] fun gate_44 => + ∃gate_45, gate_45 = Gates.add StartIndex (5:F) ∧ + ∃gate_46, Gates.to_binary gate_45 26 gate_46 ∧ + MerkleRootUpdateGadget_26_26_26 gate_43 (0:F) gate_44 gate_46 NewElementProofs[5] fun gate_47 => + LeafHashGadget LowElementValues[6] LowElementNextValues[6] NewElementValues[6] fun gate_48 => + Poseidon2 LowElementValues[6] NewElementValues[6] fun gate_49 => + ∃gate_50, Gates.to_binary LowElementIndices[6] 26 gate_50 ∧ + MerkleRootUpdateGadget_26_26_26 gate_47 gate_48 gate_49 gate_50 LowElementProofs[6] fun gate_51 => + Poseidon2 NewElementValues[6] LowElementNextValues[6] fun gate_52 => + ∃gate_53, gate_53 = Gates.add StartIndex (6:F) ∧ + ∃gate_54, Gates.to_binary gate_53 26 gate_54 ∧ + MerkleRootUpdateGadget_26_26_26 gate_51 (0:F) gate_52 gate_54 NewElementProofs[6] fun gate_55 => + LeafHashGadget LowElementValues[7] LowElementNextValues[7] NewElementValues[7] fun gate_56 => + Poseidon2 LowElementValues[7] NewElementValues[7] fun gate_57 => + ∃gate_58, Gates.to_binary LowElementIndices[7] 26 gate_58 ∧ + MerkleRootUpdateGadget_26_26_26 gate_55 gate_56 gate_57 gate_58 LowElementProofs[7] fun gate_59 => + Poseidon2 NewElementValues[7] LowElementNextValues[7] fun gate_60 => + ∃gate_61, gate_61 = Gates.add StartIndex (7:F) ∧ + ∃gate_62, Gates.to_binary gate_61 26 gate_62 ∧ + MerkleRootUpdateGadget_26_26_26 gate_59 (0:F) gate_60 gate_62 NewElementProofs[7] fun gate_63 => + Gates.eq NewRoot gate_63 ∧ + HashChain_8 NewElementValues fun gate_65 => + Gates.eq HashchainHash gate_65 ∧ + HashChain_4 vec![OldRoot, NewRoot, HashchainHash, StartIndex] fun gate_67 => + Gates.eq PublicInputHash gate_67 ∧ + True + end LightProver diff --git a/prover/server/formal-verification/FormalVerification/Merkle.lean b/prover/server/formal-verification/FormalVerification/Merkle.lean index 6d34a8d30..4863388f2 100644 --- a/prover/server/formal-verification/FormalVerification/Merkle.lean +++ b/prover/server/formal-verification/FormalVerification/Merkle.lean @@ -439,9 +439,9 @@ theorem NonInclusionCircuit_rec_correct [Fact poseidon₂_no_zero_preimage] [Fac . decide theorem NonInclusionCircuit_correct [Fact poseidon₂_no_zero_preimage] [Fact (CollisionResistant poseidon₂)] {trees : List.Vector (RangeVector (2^26)) 8} {leaves : List.Vector F 8}: - (∃lo hi inds proofs, LightProver.NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 h (trees.map (·.root)) leaves lo hi nxt inds proofs) ↔ + (∃lo hi inds proofs, LightProver.NonInclusionCircuit_8_8_8_8_8_26_8_8_26 h (trees.map (·.root)) leaves lo hi inds proofs) ↔ h = inputHash poseidon₂ poseidon₃ (trees.map (·.root)) leaves ∧ ∀i (_: i∈[0:8]), leaves[i].val ∈ trees[i] := by - unfold LightProver.NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 + unfold LightProver.NonInclusionCircuit_8_8_8_8_8_26_8_8_26 simp only [←NonInclusionProof_rec_equiv] simp only [TwoInputsHashChain_rw] simp [Gates, GatesGnark8, GatesDef.eq] @@ -481,3 +481,113 @@ theorem CombinedCircuit_correct [Fact poseidon₂_no_zero_preimage] [Fact (Colli . apply NonInclusionCircuit_rec_correct.mpr simp_all . exact fun i ir => (hp i ir).1 + +theorem MerkleRootUpdateGadget_rw [Fact (CollisionResistant poseidon₂)] {tree : MerkleTree F poseidon₂ 26}: + (∃bin, Gates.to_binary ix 26 bin ∧ + LightProver.MerkleRootUpdateGadget_26_26_26 tree.root oldleaf newleaf bin proof k) ↔ + ∃(hi: ix.val < 2^26), proof.reverse = tree.proofAtFin ⟨ix.val, hi⟩ ∧ oldleaf = tree.itemAtFin ⟨ix.val, hi⟩ ∧ k (tree.setAtFin ⟨ix.val, hi⟩ newleaf).root := by + unfold LightProver.MerkleRootUpdateGadget_26_26_26 + have : 2^26 < Order := by decide + simp only [Gates, GatesGnark8, GatesDef.eq, Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt this] + apply Iff.intro + · rintro ⟨_, ⟨hi, rfl⟩, h⟩ + simp only [MerkleRootGadget_rw] at h + simp only [MerkleTree.recover_eq_root_iff_proof_and_item_correct, Fin.toBitsLE, List.Vector.reverse_reverse] at h + simp only [MerkleTree.proofAtFin, MerkleTree.root_setAtFin_eq_recoverAtFin, MerkleTree.recoverAtFin, MerkleTree.itemAtFin] + rcases h with ⟨⟨h₁, h₂⟩, h₃⟩ + apply Exists.intro hi + apply And.intro h₁ + apply And.intro h₂ + rw [←h₁] + exact h₃ + · rintro ⟨hi, hpr, hol, hk⟩ + apply Exists.intro + apply And.intro + · exists hi + simp only [MerkleRootGadget_rw, MerkleTree.recover_eq_root_iff_proof_and_item_correct, Fin.toBitsLE, List.Vector.reverse_reverse] + simp only [MerkleTree.proofAtFin] at hpr + simp only [MerkleTree.itemAtFin] at hol + simp only [MerkleTree.root_setAtFin_eq_recoverAtFin, MerkleTree.recoverAtFin, MerkleTree.proofAtFin] at hk + simp_all + +lemma Range.none_of_hashOpt_zero {r: Option Range} [Fact poseidon₂_no_zero_preimage]: 0 = Range.hashOpt r ↔ r = none := by + apply Iff.intro + · intro h + cases r + · trivial + · simp [Range.hashOpt, Option.map, Option.getD, hash] at h + have : poseidon₂_no_zero_preimage := Fact.elim inferInstance + unfold poseidon₂_no_zero_preimage at this + have := this _ _ (Eq.symm h) + cases this + · rintro rfl; rfl + +lemma MerkleTree.setAtFin_comm_of_ne {t : MerkleTree H α d} (hp : i₁ ≠ i₂) : + (t.setAtFin i₁ v₁ |>.setAtFin i₂ v₂) = (t.setAtFin i₂ v₂ |>.setAtFin i₁ v₁) := by + sorry + +theorem BatchAddressAppend_step_rw [Fact (CollisionResistant poseidon₂)] [Fact poseidon₂_no_zero_preimage] {rv : RangeVector (2^26)}: + (LightProver.LeafHashGadget LowElementValue LowElementNextValue NewElementValue fun gate_0 => + LightProver.Poseidon2 LowElementValue NewElementValue fun gate_1 => + ∃gate_2, Gates.to_binary LowElementIndices 26 gate_2 ∧ + LightProver.MerkleRootUpdateGadget_26_26_26 rv.root gate_0 gate_1 gate_2 LowElementProof fun gate_3 => + LightProver.Poseidon2 NewElementValue LowElementNextValue fun gate_4 => + ∃gate_5, gate_5 = Gates.add StartIndex offset ∧ + ∃gate_6, Gates.to_binary gate_5 26 gate_6 ∧ + LightProver.MerkleRootUpdateGadget_26_26_26 gate_3 (0:F) gate_4 gate_6 NewElementProof k) → + ∃(hei : (StartIndex+offset).val < 2^26) + (hli : LowElementIndices.val < 2^26) + (currentIndex_valid : NewElementValue.val ∈ rv.ranges ⟨LowElementIndices.val, hli⟩) + (emptyIndex_valid : rv.ranges ⟨(StartIndex+offset).val, hei⟩ = none), + k (rv.remove NewElementValue.val ⟨LowElementIndices.val, hli⟩ ⟨(StartIndex+offset).val, hei⟩ currentIndex_valid emptyIndex_valid).root := by + simp only [LightProver.LeafHashGadget, Poseidon2_iff_uniqueAssignment, RangeVector.root, MerkleRootUpdateGadget_rw] + have := @Range.hashOpt_eq_poseidon_iff_is_some + conv at this => enter [x,x,x,x,x,1]; rw [eq_comm] + simp only [rangeTree, MerkleTree.ofFn_itemAtFin, this, Gates, GatesGnark8, GatesDef.add] + -- apply Iff.intro + · rintro ⟨hlo, hhi, hli, hlep, ⟨hrsome, hlodef, hhidef⟩, _, rfl, hemp, hnep, heltZ, hk⟩ + apply Exists.intro hemp + apply Exists.intro hli + have := AssertIsLess_range (by rw [hlodef]; apply Fin.prop) ⟨hlo, hhi⟩ + rw [hlodef, hhidef] at this + apply Exists.intro (by + rw [Option.eq_some_of_isSome hrsome] + exact this + ) + have : Fin.mk LowElementIndices.val hli ≠ Fin.mk (StartIndex+offset).val hemp := by + intro h + rw [h, MerkleTree.itemAtFin_setAtFin_eq_self] at heltZ + have : poseidon₂_no_zero_preimage := Fact.elim inferInstance + exact this _ _ (Eq.symm heltZ) + rw [MerkleTree.itemAtFin_setAtFin_invariant_of_neq (ne_comm.mp this), MerkleTree.ofFn_itemAtFin] at heltZ + simp [Range.none_of_hashOpt_zero] at heltZ + apply Exists.intro heltZ + convert hk + simp only [RangeVector.remove, Range.remove, Range.remove.rlo, Range.remove.rhi] + + simp only [MerkleTree.ofFn_cond] + rw [MerkleTree.setAtFin_comm_of_ne this] + simp only [Range.hashOpt, Range.hash, Option.map, Option.getD, ←hlodef, ←hhidef] + simp + -- · sorry + + + + + + -- Range.hashOpt_eq_poseidon_iff_is_some + +-- theorem BatchAddressAppend_step_rw {rv : RangeVector (2^26)}: +-- (LightProver.LeafHashGadget LowElementValue LowElementNextValue NewElementValue fun gate_2 => +-- LightProver.Poseidon2 LowElementValue NewElementValue fun gate_3 => +-- ∃gate_4, Gates.to_binary LowElementIndex 26 gate_4 ∧ +-- LightProver.MerkleRootUpdateGadget_26_26_26 rv.root gate_2 gate_3 gate_4 LowElementProof fun gate_5 => +-- LightProver.Poseidon2 NewElementValue LowElementNextValue fun gate_6 => +-- ∃gate_1, Gates.to_binary StartIndex 26 gate_1 ∧ +-- LightProver.MerkleRootUpdateGadget_26_26_26 gate_5 (0:F) gate_6 gate_1 NewElementProof k) ↔ +-- ∃(hei : StartIndex.val < 2^26) +-- (hli : LowElementIndex.val < 2^26) +-- (currentIndex_valid : NewElementValue.val ∈ rv.ranges ⟨LowElementIndex.val, hli⟩) +-- (emptyIndex_valid : rv.ranges ⟨StartIndex.val, hei⟩ = none), +-- k (rv.remove NewElementValue.val ⟨LowElementIndex.val, hli⟩ ⟨StartIndex.val, hei⟩ currentIndex_valid emptyIndex_valid).root := by +-- simp only [LightProver.LeafHashGadget, Poseidon2_iff_uniqueAssignment] diff --git a/prover/server/formal-verification/FormalVerification/RangeTree.lean b/prover/server/formal-verification/FormalVerification/RangeTree.lean index ee47411bb..52b20f5e7 100644 --- a/prover/server/formal-verification/FormalVerification/RangeTree.lean +++ b/prover/server/formal-verification/FormalVerification/RangeTree.lean @@ -302,12 +302,9 @@ lemma Fin.lt_of_msb_zero {x : Fin (2^(d+1))} (h : Fin.msb x = false): x.val < 2^ rw [Fin.msbs_lsbs_decomposition (v:=x)] simp_all --- lemma x : Fin.val (n := n+1) (2^d) = (2^d % (n+1)) := by --- induction d with --- | zero => rfl --- | succ d ih => --- simp [pow_succ, Fin.val_mul, ih] - +lemma MerkleTree.ofFn_cond {fn : Fin (2^d) → α} {v k} : + MerkleTree.ofFn H emb (fun i => if i = k then v else fn i) = (MerkleTree.ofFn H emb fn |>.setAtFin k (emb v)) := by + sorry lemma MerkleTree.ofFn_itemAtFin {fn : Fin (2^d) → α} : (ofFn H emb fn |>.itemAtFin idx) = emb (fn idx) := by induction d with diff --git a/prover/server/prover/batch_address_append_circuit.go b/prover/server/prover/batch_address_append_circuit.go index c7f6c6d9a..438a254d9 100644 --- a/prover/server/prover/batch_address_append_circuit.go +++ b/prover/server/prover/batch_address_append_circuit.go @@ -19,25 +19,24 @@ import ( type BatchAddressTreeAppendCircuit struct { PublicInputHash frontend.Variable `gnark:",public"` - OldRoot frontend.Variable `gnark:",private"` - NewRoot frontend.Variable `gnark:",private"` - HashchainHash frontend.Variable `gnark:",private"` - StartIndex frontend.Variable `gnark:",private"` - - LowElementValues []frontend.Variable `gnark:",private"` - LowElementNextValues []frontend.Variable `gnark:",private"` - LowElementIndices []frontend.Variable `gnark:",private"` - LowElementProofs [][]frontend.Variable `gnark:",private"` - - NewElementValues []frontend.Variable `gnark:",private"` - NewElementProofs [][]frontend.Variable `gnark:",private"` + OldRoot frontend.Variable `gnark:",secret"` + NewRoot frontend.Variable `gnark:",secret"` + HashchainHash frontend.Variable `gnark:",secret"` + StartIndex frontend.Variable `gnark:",secret"` + + LowElementValues []frontend.Variable `gnark:",secret"` + LowElementNextValues []frontend.Variable `gnark:",secret"` + LowElementIndices []frontend.Variable `gnark:",secret"` + LowElementProofs [][]frontend.Variable `gnark:",secret"` + + NewElementValues []frontend.Variable `gnark:",secret"` + NewElementProofs [][]frontend.Variable `gnark:",secret"` BatchSize uint32 TreeHeight uint32 } func (circuit *BatchAddressTreeAppendCircuit) Define(api frontend.API) error { currentRoot := circuit.OldRoot - indexBits := api.ToBinary(circuit.StartIndex, int(circuit.TreeHeight)) for i := uint32(0); i < circuit.BatchSize; i++ { oldLowLeafHash := abstractor.Call(api, LeafHashGadget{ @@ -69,6 +68,7 @@ func (circuit *BatchAddressTreeAppendCircuit) Define(api frontend.API) error { In2: circuit.LowElementNextValues[i], }) + indexBits := api.ToBinary(api.Add(circuit.StartIndex, i), int(circuit.TreeHeight)) currentRoot = abstractor.Call(api, MerkleRootUpdateGadget{ OldRoot: currentRoot, OldLeaf: getZeroValue(0), @@ -77,11 +77,6 @@ func (circuit *BatchAddressTreeAppendCircuit) Define(api frontend.API) error { MerkleProof: circuit.NewElementProofs[i], Height: int(circuit.TreeHeight), }) - - indexBits = incrementBits( - api, - indexBits, - ) } api.AssertIsEqual(circuit.NewRoot, currentRoot) diff --git a/prover/server/prover/batch_append_with_proofs_circuit.go b/prover/server/prover/batch_append_with_proofs_circuit.go index fbc8496b2..d6081b3c3 100644 --- a/prover/server/prover/batch_append_with_proofs_circuit.go +++ b/prover/server/prover/batch_append_with_proofs_circuit.go @@ -15,14 +15,14 @@ import ( type BatchAppendWithProofsCircuit struct { PublicInputHash frontend.Variable `gnark:",public"` - OldRoot frontend.Variable `gnark:",private"` - NewRoot frontend.Variable `gnark:",private"` - LeavesHashchainHash frontend.Variable `gnark:",private"` - StartIndex frontend.Variable `gnark:",private"` - - OldLeaves []frontend.Variable `gnark:",private"` - Leaves []frontend.Variable `gnark:",private"` - MerkleProofs [][]frontend.Variable `gnark:",private"` + OldRoot frontend.Variable `gnark:",secret"` + NewRoot frontend.Variable `gnark:",secret"` + LeavesHashchainHash frontend.Variable `gnark:",secret"` + StartIndex frontend.Variable `gnark:",secret"` + + OldLeaves []frontend.Variable `gnark:",secret"` + Leaves []frontend.Variable `gnark:",secret"` + MerkleProofs [][]frontend.Variable `gnark:",secret"` Height uint32 BatchSize uint32 diff --git a/prover/server/prover/batch_circuit_helpers.go b/prover/server/prover/batch_circuit_helpers.go index e2d52b64c..3e21d079a 100644 --- a/prover/server/prover/batch_circuit_helpers.go +++ b/prover/server/prover/batch_circuit_helpers.go @@ -10,13 +10,21 @@ import ( "github.com/consensys/gnark/frontend" ) -func createHashChain(api frontend.API, hashes []frontend.Variable) frontend.Variable { - if len(hashes) == 0 { +type HashChain struct { + Hashes []frontend.Variable +} + +func (gadget HashChain) DefineGadget(api frontend.API) interface{} { + if len(gadget.Hashes) == 0 { return frontend.Variable(0) } - initialHash := hashes[0] - return computeHashChain(api, initialHash, hashes) + initialHash := gadget.Hashes[0] + return computeHashChain(api, initialHash, gadget.Hashes[1:]) +} + +func createHashChain(api frontend.API, hashes []frontend.Variable) frontend.Variable { + return abstractor.Call(api, HashChain{hashes}) } type TwoInputsHashChain struct { @@ -52,5 +60,5 @@ func computeHashChain(api frontend.API, initialHash frontend.Variable, hashes [] // getZeroValue returns the zero value for a given tree level func getZeroValue(level int) frontend.Variable { - return frontend.Variable(new(big.Int).SetBytes(merkletree.ZERO_BYTES[level][:])) + return frontend.Variable(*new(big.Int).SetBytes(merkletree.ZERO_BYTES[level][:])) } diff --git a/prover/server/prover/batch_update_circuit.go b/prover/server/prover/batch_update_circuit.go index 576af56ba..6c1266fa5 100644 --- a/prover/server/prover/batch_update_circuit.go +++ b/prover/server/prover/batch_update_circuit.go @@ -16,15 +16,15 @@ import ( type BatchUpdateCircuit struct { PublicInputHash frontend.Variable `gnark:",public"` - OldRoot frontend.Variable `gnark:",private"` - NewRoot frontend.Variable `gnark:",private"` - LeavesHashchainHash frontend.Variable `gnark:",private"` - - TxHashes []frontend.Variable `gnark:"private"` - Leaves []frontend.Variable `gnark:"private"` - OldLeaves []frontend.Variable `gnark:"private"` - MerkleProofs [][]frontend.Variable `gnark:"private"` - PathIndices []frontend.Variable `gnark:"private"` + OldRoot frontend.Variable `gnark:",secret"` + NewRoot frontend.Variable `gnark:",secret"` + LeavesHashchainHash frontend.Variable `gnark:",secret"` + + TxHashes []frontend.Variable `gnark:",secret"` + Leaves []frontend.Variable `gnark:",secret"` + OldLeaves []frontend.Variable `gnark:",secret"` + MerkleProofs [][]frontend.Variable `gnark:",secret"` + PathIndices []frontend.Variable `gnark:",secret"` Height uint32 BatchSize uint32 diff --git a/prover/server/prover/extractor.go b/prover/server/prover/extractor.go index 8248a3759..df922cb41 100644 --- a/prover/server/prover/extractor.go +++ b/prover/server/prover/extractor.go @@ -12,10 +12,16 @@ func ExtractLean(treeHeight uint32, numberOfCompressedAccounts uint32) (string, // Initialising MerkleProofs slice with correct dimensions inclusionInPathElements := make([][]frontend.Variable, numberOfCompressedAccounts) nonInclusionInPathElements := make([][]frontend.Variable, numberOfCompressedAccounts) + addressAppendLowProofs := make([][]frontend.Variable, numberOfCompressedAccounts) + addressAppendEmptyProofs := make([][]frontend.Variable, numberOfCompressedAccounts) + batchUpdateProofs := make([][]frontend.Variable, numberOfCompressedAccounts) for i := 0; i < int(numberOfCompressedAccounts); i++ { inclusionInPathElements[i] = make([]frontend.Variable, treeHeight) nonInclusionInPathElements[i] = make([]frontend.Variable, treeHeight) + addressAppendLowProofs[i] = make([]frontend.Variable, treeHeight) + addressAppendEmptyProofs[i] = make([]frontend.Variable, treeHeight) + batchUpdateProofs[i] = make([]frontend.Variable, treeHeight) } inclusionCircuit := InclusionCircuit{ @@ -34,7 +40,6 @@ func ExtractLean(treeHeight uint32, numberOfCompressedAccounts uint32) (string, Values: make([]frontend.Variable, numberOfCompressedAccounts), LeafLowerRangeValues: make([]frontend.Variable, numberOfCompressedAccounts), LeafHigherRangeValues: make([]frontend.Variable, numberOfCompressedAccounts), - NextIndices: make([]frontend.Variable, numberOfCompressedAccounts), InPathIndices: make([]frontend.Variable, numberOfCompressedAccounts), InPathElements: nonInclusionInPathElements, } @@ -63,5 +68,26 @@ func ExtractLean(treeHeight uint32, numberOfCompressedAccounts uint32) (string, NonInclusion: nonInclusionProof, } - return extractor.ExtractCircuits("LightProver", ecc.BN254, &inclusionCircuit, &nonInclusionCircuit, &combinedCircuit) + indexedUpdateCircuit := BatchAddressTreeAppendCircuit{ + LowElementValues: make([]frontend.Variable, numberOfCompressedAccounts), + LowElementNextValues: make([]frontend.Variable, numberOfCompressedAccounts), + LowElementIndices: make([]frontend.Variable, numberOfCompressedAccounts), + LowElementProofs: addressAppendLowProofs, + NewElementValues: make([]frontend.Variable, numberOfCompressedAccounts), + NewElementProofs: addressAppendEmptyProofs, + BatchSize: numberOfCompressedAccounts, + TreeHeight: treeHeight, + } + + batchUpdateCircuit := BatchUpdateCircuit{ + TxHashes: make([]frontend.Variable, numberOfCompressedAccounts), + Leaves: make([]frontend.Variable, numberOfCompressedAccounts), + OldLeaves: make([]frontend.Variable, numberOfCompressedAccounts), + MerkleProofs: batchUpdateProofs, + PathIndices: make([]frontend.Variable, numberOfCompressedAccounts), + Height: treeHeight, + BatchSize: numberOfCompressedAccounts, + } + + return extractor.ExtractCircuits("LightProver", ecc.BN254, &inclusionCircuit, &nonInclusionCircuit, &combinedCircuit, &batchUpdateCircuit, &indexedUpdateCircuit) } diff --git a/prover/server/prover/non_inclusion_circuit.go b/prover/server/prover/non_inclusion_circuit.go index 2362c5237..9c2a0a334 100644 --- a/prover/server/prover/non_inclusion_circuit.go +++ b/prover/server/prover/non_inclusion_circuit.go @@ -17,7 +17,6 @@ type NonInclusionCircuit struct { // private inputs LeafLowerRangeValues []frontend.Variable `gnark:"input"` LeafHigherRangeValues []frontend.Variable `gnark:"input"` - NextIndices []frontend.Variable `gnark:"input"` InPathIndices []frontend.Variable `gnark:"input"` InPathElements [][]frontend.Variable `gnark:"input"` @@ -53,7 +52,6 @@ func ImportNonInclusionSetup(treeHeight uint32, numberOfCompressedAccounts uint3 leafLowerRangeValues := make([]frontend.Variable, numberOfCompressedAccounts) leafHigherRangeValues := make([]frontend.Variable, numberOfCompressedAccounts) - leafIndices := make([]frontend.Variable, numberOfCompressedAccounts) inPathIndices := make([]frontend.Variable, numberOfCompressedAccounts) inPathElements := make([][]frontend.Variable, numberOfCompressedAccounts) @@ -69,7 +67,6 @@ func ImportNonInclusionSetup(treeHeight uint32, numberOfCompressedAccounts uint3 Values: values, LeafLowerRangeValues: leafLowerRangeValues, LeafHigherRangeValues: leafHigherRangeValues, - NextIndices: leafIndices, InPathIndices: inPathIndices, InPathElements: inPathElements, } diff --git a/prover/server/prover/non_inclusion_proving_system.go b/prover/server/prover/non_inclusion_proving_system.go index 66d4fbdb0..0556957c4 100644 --- a/prover/server/prover/non_inclusion_proving_system.go +++ b/prover/server/prover/non_inclusion_proving_system.go @@ -56,7 +56,6 @@ func R1CSNonInclusion(treeHeight uint32, numberOfCompressedAccounts uint32) (con leafLowerRangeValues := make([]frontend.Variable, numberOfCompressedAccounts) leafHigherRangeValues := make([]frontend.Variable, numberOfCompressedAccounts) - nextIndices := make([]frontend.Variable, numberOfCompressedAccounts) inPathIndices := make([]frontend.Variable, numberOfCompressedAccounts) inPathElements := make([][]frontend.Variable, numberOfCompressedAccounts) @@ -73,7 +72,6 @@ func R1CSNonInclusion(treeHeight uint32, numberOfCompressedAccounts uint32) (con Values: values, LeafLowerRangeValues: leafLowerRangeValues, LeafHigherRangeValues: leafHigherRangeValues, - NextIndices: nextIndices, InPathIndices: inPathIndices, InPathElements: inPathElements, } @@ -131,7 +129,6 @@ func (ps *ProvingSystemV1) ProveNonInclusion(params *NonInclusionParameters) (*P Values: values, LeafLowerRangeValues: leafLowerRangeValues, LeafHigherRangeValues: leafHigherRangeValues, - NextIndices: nextIndices, InPathIndices: inPathIndices, InPathElements: inPathElements, }