diff --git a/prover/server/formal-verification/.gitignore b/prover/server/formal-verification/.gitignore index 0d3fac651e..79a29fcd08 100644 --- a/prover/server/formal-verification/.gitignore +++ b/prover/server/formal-verification/.gitignore @@ -1 +1,2 @@ lakefile.olean +.lake diff --git a/prover/server/formal-verification/FormalVerification/Circuit.lean b/prover/server/formal-verification/FormalVerification/Circuit.lean index fb5292e336..25d30dfcc6 100644 --- a/prover/server/formal-verification/FormalVerification/Circuit.lean +++ b/prover/server/formal-verification/FormalVerification/Circuit.lean @@ -127,68 +127,6 @@ def Poseidon2 (In1: F) (In2: F) (k: F -> Prop): Prop := poseidon_3 vec![(0:F), In1, In2] fun gate_0 => k gate_0[0] -def ProveParentHash (Bit: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop := - Gates.is_bool Bit ∧ - ∃gate_1, Gates.select Bit Sibling Hash gate_1 ∧ - ∃gate_2, Gates.select Bit Hash Sibling gate_2 ∧ - Poseidon2 gate_1 gate_2 fun gate_3 => - k gate_3 - -def MerkleRootGadget_26_26 (Hash: F) (Index: F) (Path: List.Vector F 26) (k: F -> Prop): Prop := - ∃gate_0, Gates.to_binary Index 26 gate_0 ∧ - ProveParentHash gate_0[0] Hash Path[0] fun gate_1 => - ProveParentHash gate_0[1] gate_1 Path[1] fun gate_2 => - ProveParentHash gate_0[2] gate_2 Path[2] fun gate_3 => - ProveParentHash gate_0[3] gate_3 Path[3] fun gate_4 => - ProveParentHash gate_0[4] gate_4 Path[4] fun gate_5 => - ProveParentHash gate_0[5] gate_5 Path[5] fun gate_6 => - ProveParentHash gate_0[6] gate_6 Path[6] fun gate_7 => - ProveParentHash gate_0[7] gate_7 Path[7] fun gate_8 => - ProveParentHash gate_0[8] gate_8 Path[8] fun gate_9 => - ProveParentHash gate_0[9] gate_9 Path[9] fun gate_10 => - ProveParentHash gate_0[10] gate_10 Path[10] fun gate_11 => - ProveParentHash gate_0[11] gate_11 Path[11] fun gate_12 => - ProveParentHash gate_0[12] gate_12 Path[12] fun gate_13 => - ProveParentHash gate_0[13] gate_13 Path[13] fun gate_14 => - ProveParentHash gate_0[14] gate_14 Path[14] fun gate_15 => - ProveParentHash gate_0[15] gate_15 Path[15] fun gate_16 => - ProveParentHash gate_0[16] gate_16 Path[16] fun gate_17 => - ProveParentHash gate_0[17] gate_17 Path[17] fun gate_18 => - ProveParentHash gate_0[18] gate_18 Path[18] fun gate_19 => - ProveParentHash gate_0[19] gate_19 Path[19] fun gate_20 => - ProveParentHash gate_0[20] gate_20 Path[20] fun gate_21 => - ProveParentHash gate_0[21] gate_21 Path[21] fun gate_22 => - ProveParentHash gate_0[22] gate_22 Path[22] fun gate_23 => - ProveParentHash gate_0[23] gate_23 Path[23] fun gate_24 => - ProveParentHash gate_0[24] gate_24 Path[24] fun gate_25 => - ProveParentHash gate_0[25] gate_25 Path[25] fun gate_26 => - k gate_26 - -def InclusionProof_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Leaves: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8) (k: List.Vector F 8 -> Prop): Prop := - MerkleRootGadget_26_26 Leaves[0] InPathIndices[0] InPathElements[0] fun gate_0 => - Gates.eq gate_0 Roots[0] ∧ - MerkleRootGadget_26_26 Leaves[1] InPathIndices[1] InPathElements[1] fun gate_2 => - Gates.eq gate_2 Roots[1] ∧ - MerkleRootGadget_26_26 Leaves[2] InPathIndices[2] InPathElements[2] fun gate_4 => - Gates.eq gate_4 Roots[2] ∧ - MerkleRootGadget_26_26 Leaves[3] InPathIndices[3] InPathElements[3] fun gate_6 => - Gates.eq gate_6 Roots[3] ∧ - MerkleRootGadget_26_26 Leaves[4] InPathIndices[4] InPathElements[4] fun gate_8 => - Gates.eq gate_8 Roots[4] ∧ - MerkleRootGadget_26_26 Leaves[5] InPathIndices[5] InPathElements[5] fun gate_10 => - Gates.eq gate_10 Roots[5] ∧ - MerkleRootGadget_26_26 Leaves[6] InPathIndices[6] InPathElements[6] fun gate_12 => - Gates.eq gate_12 Roots[6] ∧ - MerkleRootGadget_26_26 Leaves[7] InPathIndices[7] InPathElements[7] fun gate_14 => - Gates.eq gate_14 Roots[7] ∧ - k vec![gate_0, gate_2, gate_4, gate_6, gate_8, gate_10, gate_12, gate_14] - -def AssertIsLess_248 (A: F) (B: F) : Prop := - ∃gate_0, gate_0 = Gates.sub (452312848583266388373324160190187140051835877600158453279131187530910662656:F) B ∧ - ∃gate_1, gate_1 = Gates.add A gate_0 ∧ - ∃_ignored_, Gates.to_binary gate_1 248 _ignored_ ∧ - True - def mds_4 (Inp: List.Vector F 4) (k: List.Vector F 4 -> Prop): Prop := ∃gate_0, gate_0 = Gates.mul Inp[0] (16023668707004248971294664614290028914393192768609916554276071736843535714477:F) ∧ ∃gate_1, gate_1 = Gates.add (0:F) gate_0 ∧ @@ -316,48 +254,144 @@ def Poseidon3 (In1: F) (In2: F) (In3: F) (k: F -> Prop): Prop := poseidon_4 vec![(0:F), In1, In2, In3] fun gate_0 => k gate_0[0] -def LeafHashGadget (LeafLowerRangeValue: F) (NextIndex: F) (LeafHigherRangeValue: F) (Value: F) (k: F -> Prop): Prop := - AssertIsLess_248 LeafLowerRangeValue Value ∧ - AssertIsLess_248 Value LeafHigherRangeValue ∧ - Poseidon3 LeafLowerRangeValue NextIndex LeafHigherRangeValue fun gate_2 => - k gate_2 +def TwoInputsHashChain_8_8 (HashesFirst: List.Vector F 8) (HashesSecond: List.Vector F 8) (k: F -> Prop): Prop := + Poseidon2 HashesFirst[0] HashesSecond[0] fun gate_0 => + Poseidon3 gate_0 HashesFirst[1] HashesSecond[1] fun gate_1 => + Poseidon3 gate_1 HashesFirst[2] HashesSecond[2] fun gate_2 => + Poseidon3 gate_2 HashesFirst[3] HashesSecond[3] fun gate_3 => + Poseidon3 gate_3 HashesFirst[4] HashesSecond[4] fun gate_4 => + Poseidon3 gate_4 HashesFirst[5] HashesSecond[5] fun gate_5 => + Poseidon3 gate_5 HashesFirst[6] HashesSecond[6] fun gate_6 => + Poseidon3 gate_6 HashesFirst[7] HashesSecond[7] fun gate_7 => + k gate_7 -def NonInclusionProof_8_8_8_8_8_8_26_8_8_26 (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) (k: List.Vector F 8 -> Prop): Prop := - LeafHashGadget LeafLowerRangeValues[0] NextIndices[0] LeafHigherRangeValues[0] Values[0] fun gate_0 => - MerkleRootGadget_26_26 gate_0 InPathIndices[0] InPathElements[0] fun gate_1 => +def ProveParentHash (Bit: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop := + Gates.is_bool Bit ∧ + ∃gate_1, Gates.select Bit Sibling Hash gate_1 ∧ + ∃gate_2, Gates.select Bit Hash Sibling gate_2 ∧ + Poseidon2 gate_1 gate_2 fun gate_3 => + k gate_3 + +def MerkleRootGadget_26_26_26 (Hash: F) (Index: List.Vector F 26) (Path: List.Vector F 26) (k: F -> Prop): Prop := + ProveParentHash Index[0] Hash Path[0] fun gate_0 => + ProveParentHash Index[1] gate_0 Path[1] fun gate_1 => + ProveParentHash Index[2] gate_1 Path[2] fun gate_2 => + ProveParentHash Index[3] gate_2 Path[3] fun gate_3 => + ProveParentHash Index[4] gate_3 Path[4] fun gate_4 => + ProveParentHash Index[5] gate_4 Path[5] fun gate_5 => + ProveParentHash Index[6] gate_5 Path[6] fun gate_6 => + ProveParentHash Index[7] gate_6 Path[7] fun gate_7 => + ProveParentHash Index[8] gate_7 Path[8] fun gate_8 => + ProveParentHash Index[9] gate_8 Path[9] fun gate_9 => + ProveParentHash Index[10] gate_9 Path[10] fun gate_10 => + ProveParentHash Index[11] gate_10 Path[11] fun gate_11 => + ProveParentHash Index[12] gate_11 Path[12] fun gate_12 => + ProveParentHash Index[13] gate_12 Path[13] fun gate_13 => + ProveParentHash Index[14] gate_13 Path[14] fun gate_14 => + ProveParentHash Index[15] gate_14 Path[15] fun gate_15 => + ProveParentHash Index[16] gate_15 Path[16] fun gate_16 => + ProveParentHash Index[17] gate_16 Path[17] fun gate_17 => + ProveParentHash Index[18] gate_17 Path[18] fun gate_18 => + ProveParentHash Index[19] gate_18 Path[19] fun gate_19 => + ProveParentHash Index[20] gate_19 Path[20] fun gate_20 => + ProveParentHash Index[21] gate_20 Path[21] fun gate_21 => + ProveParentHash Index[22] gate_21 Path[22] fun gate_22 => + ProveParentHash Index[23] gate_22 Path[23] fun gate_23 => + ProveParentHash Index[24] gate_23 Path[24] fun gate_24 => + ProveParentHash Index[25] gate_24 Path[25] fun gate_25 => + k gate_25 + +def InclusionProof_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Leaves: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8) (k: List.Vector F 8 -> Prop): Prop := + ∃gate_0, Gates.to_binary InPathIndices[0] 26 gate_0 ∧ + MerkleRootGadget_26_26_26 Leaves[0] gate_0 InPathElements[0] fun gate_1 => Gates.eq gate_1 Roots[0] ∧ - LeafHashGadget LeafLowerRangeValues[1] NextIndices[1] LeafHigherRangeValues[1] Values[1] fun gate_3 => - MerkleRootGadget_26_26 gate_3 InPathIndices[1] InPathElements[1] fun gate_4 => + ∃gate_3, Gates.to_binary InPathIndices[1] 26 gate_3 ∧ + MerkleRootGadget_26_26_26 Leaves[1] gate_3 InPathElements[1] fun gate_4 => Gates.eq gate_4 Roots[1] ∧ - LeafHashGadget LeafLowerRangeValues[2] NextIndices[2] LeafHigherRangeValues[2] Values[2] fun gate_6 => - MerkleRootGadget_26_26 gate_6 InPathIndices[2] InPathElements[2] fun gate_7 => + ∃gate_6, Gates.to_binary InPathIndices[2] 26 gate_6 ∧ + MerkleRootGadget_26_26_26 Leaves[2] gate_6 InPathElements[2] fun gate_7 => Gates.eq gate_7 Roots[2] ∧ - LeafHashGadget LeafLowerRangeValues[3] NextIndices[3] LeafHigherRangeValues[3] Values[3] fun gate_9 => - MerkleRootGadget_26_26 gate_9 InPathIndices[3] InPathElements[3] fun gate_10 => + ∃gate_9, Gates.to_binary InPathIndices[3] 26 gate_9 ∧ + MerkleRootGadget_26_26_26 Leaves[3] gate_9 InPathElements[3] fun gate_10 => Gates.eq gate_10 Roots[3] ∧ - LeafHashGadget LeafLowerRangeValues[4] NextIndices[4] LeafHigherRangeValues[4] Values[4] fun gate_12 => - MerkleRootGadget_26_26 gate_12 InPathIndices[4] InPathElements[4] fun gate_13 => + ∃gate_12, Gates.to_binary InPathIndices[4] 26 gate_12 ∧ + MerkleRootGadget_26_26_26 Leaves[4] gate_12 InPathElements[4] fun gate_13 => Gates.eq gate_13 Roots[4] ∧ - LeafHashGadget LeafLowerRangeValues[5] NextIndices[5] LeafHigherRangeValues[5] Values[5] fun gate_15 => - MerkleRootGadget_26_26 gate_15 InPathIndices[5] InPathElements[5] fun gate_16 => + ∃gate_15, Gates.to_binary InPathIndices[5] 26 gate_15 ∧ + MerkleRootGadget_26_26_26 Leaves[5] gate_15 InPathElements[5] fun gate_16 => Gates.eq gate_16 Roots[5] ∧ - LeafHashGadget LeafLowerRangeValues[6] NextIndices[6] LeafHigherRangeValues[6] Values[6] fun gate_18 => - MerkleRootGadget_26_26 gate_18 InPathIndices[6] InPathElements[6] fun gate_19 => + ∃gate_18, Gates.to_binary InPathIndices[6] 26 gate_18 ∧ + MerkleRootGadget_26_26_26 Leaves[6] gate_18 InPathElements[6] fun gate_19 => Gates.eq gate_19 Roots[6] ∧ - LeafHashGadget LeafLowerRangeValues[7] NextIndices[7] LeafHigherRangeValues[7] Values[7] fun gate_21 => - MerkleRootGadget_26_26 gate_21 InPathIndices[7] InPathElements[7] fun gate_22 => + ∃gate_21, Gates.to_binary InPathIndices[7] 26 gate_21 ∧ + MerkleRootGadget_26_26_26 Leaves[7] gate_21 InPathElements[7] fun gate_22 => Gates.eq gate_22 Roots[7] ∧ k vec![gate_1, gate_4, gate_7, gate_10, gate_13, gate_16, gate_19, gate_22] -def InclusionCircuit_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Leaves: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8): Prop := +def AssertIsLess_248 (A: F) (B: F) : Prop := + ∃gate_0, gate_0 = Gates.sub (452312848583266388373324160190187140051835877600158453279131187530910662656:F) B ∧ + ∃gate_1, gate_1 = Gates.add A gate_0 ∧ + ∃_ignored_, Gates.to_binary gate_1 248 _ignored_ ∧ + True + +def LeafHashGadget (LeafLowerRangeValue: F) (NextIndex: F) (LeafHigherRangeValue: F) (Value: F) (k: F -> Prop): Prop := + AssertIsLess_248 LeafLowerRangeValue Value ∧ + AssertIsLess_248 Value LeafHigherRangeValue ∧ + Poseidon3 LeafLowerRangeValue NextIndex LeafHigherRangeValue fun gate_2 => + k gate_2 + +def NonInclusionProof_8_8_8_8_8_8_26_8_8_26 (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) (k: List.Vector F 8 -> Prop): Prop := + LeafHashGadget LeafLowerRangeValues[0] NextIndices[0] LeafHigherRangeValues[0] Values[0] fun gate_0 => + ∃gate_1, Gates.to_binary InPathIndices[0] 26 gate_1 ∧ + MerkleRootGadget_26_26_26 gate_0 gate_1 InPathElements[0] fun gate_2 => + Gates.eq gate_2 Roots[0] ∧ + LeafHashGadget LeafLowerRangeValues[1] NextIndices[1] LeafHigherRangeValues[1] Values[1] fun gate_4 => + ∃gate_5, Gates.to_binary InPathIndices[1] 26 gate_5 ∧ + MerkleRootGadget_26_26_26 gate_4 gate_5 InPathElements[1] fun gate_6 => + Gates.eq gate_6 Roots[1] ∧ + LeafHashGadget LeafLowerRangeValues[2] NextIndices[2] LeafHigherRangeValues[2] Values[2] fun gate_8 => + ∃gate_9, Gates.to_binary InPathIndices[2] 26 gate_9 ∧ + MerkleRootGadget_26_26_26 gate_8 gate_9 InPathElements[2] fun gate_10 => + Gates.eq gate_10 Roots[2] ∧ + LeafHashGadget LeafLowerRangeValues[3] NextIndices[3] LeafHigherRangeValues[3] Values[3] fun gate_12 => + ∃gate_13, Gates.to_binary InPathIndices[3] 26 gate_13 ∧ + MerkleRootGadget_26_26_26 gate_12 gate_13 InPathElements[3] fun gate_14 => + Gates.eq gate_14 Roots[3] ∧ + LeafHashGadget LeafLowerRangeValues[4] NextIndices[4] LeafHigherRangeValues[4] Values[4] fun gate_16 => + ∃gate_17, Gates.to_binary InPathIndices[4] 26 gate_17 ∧ + MerkleRootGadget_26_26_26 gate_16 gate_17 InPathElements[4] fun gate_18 => + Gates.eq gate_18 Roots[4] ∧ + LeafHashGadget LeafLowerRangeValues[5] NextIndices[5] LeafHigherRangeValues[5] Values[5] fun gate_20 => + ∃gate_21, Gates.to_binary InPathIndices[5] 26 gate_21 ∧ + MerkleRootGadget_26_26_26 gate_20 gate_21 InPathElements[5] fun gate_22 => + Gates.eq gate_22 Roots[5] ∧ + LeafHashGadget LeafLowerRangeValues[6] NextIndices[6] LeafHigherRangeValues[6] Values[6] fun gate_24 => + ∃gate_25, Gates.to_binary InPathIndices[6] 26 gate_25 ∧ + MerkleRootGadget_26_26_26 gate_24 gate_25 InPathElements[6] fun gate_26 => + Gates.eq gate_26 Roots[6] ∧ + LeafHashGadget LeafLowerRangeValues[7] NextIndices[7] LeafHigherRangeValues[7] Values[7] fun gate_28 => + ∃gate_29, Gates.to_binary InPathIndices[7] 26 gate_29 ∧ + MerkleRootGadget_26_26_26 gate_28 gate_29 InPathElements[7] fun gate_30 => + 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 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 (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_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 := + TwoInputsHashChain_8_8 Roots Values fun gate_0 => + Gates.eq PublicInputHash gate_0 ∧ NonInclusionProof_8_8_8_8_8_8_26_8_8_26 Roots Values LeafLowerRangeValues LeafHigherRangeValues NextIndices InPathIndices InPathElements fun _ => True -def CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 (Inclusion_Roots: List.Vector F 8) (Inclusion_Leaves: List.Vector F 8) (Inclusion_InPathIndices: List.Vector F 8) (Inclusion_InPathElements: List.Vector (List.Vector F 26) 8) (NonInclusion_Roots: List.Vector F 8) (NonInclusion_Values: List.Vector F 8) (NonInclusion_LeafLowerRangeValues: List.Vector F 8) (NonInclusion_LeafHigherRangeValues: List.Vector F 8) (NonInclusion_NextIndices: List.Vector F 8) (NonInclusion_InPathIndices: List.Vector F 8) (NonInclusion_InPathElements: List.Vector (List.Vector F 26) 8): Prop := +def CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 (PublicInputHash: F) (Inclusion_Roots: List.Vector F 8) (Inclusion_Leaves: List.Vector F 8) (Inclusion_InPathIndices: List.Vector F 8) (Inclusion_InPathElements: List.Vector (List.Vector F 26) 8) (NonInclusion_Roots: List.Vector F 8) (NonInclusion_Values: List.Vector F 8) (NonInclusion_LeafLowerRangeValues: List.Vector F 8) (NonInclusion_LeafHigherRangeValues: List.Vector F 8) (NonInclusion_NextIndices: List.Vector F 8) (NonInclusion_InPathIndices: List.Vector F 8) (NonInclusion_InPathElements: List.Vector (List.Vector F 26) 8): Prop := + TwoInputsHashChain_8_8 Inclusion_Roots Inclusion_Leaves fun gate_0 => + TwoInputsHashChain_8_8 NonInclusion_Roots NonInclusion_Values fun gate_1 => + Poseidon2 gate_0 gate_1 fun gate_2 => + Gates.eq PublicInputHash gate_2 ∧ InclusionProof_8_8_8_26_8_8_26 Inclusion_Roots Inclusion_Leaves Inclusion_InPathIndices Inclusion_InPathElements fun _ => NonInclusionProof_8_8_8_8_8_8_26_8_8_26 NonInclusion_Roots NonInclusion_Values NonInclusion_LeafLowerRangeValues NonInclusion_LeafHigherRangeValues NonInclusion_NextIndices NonInclusion_InPathIndices NonInclusion_InPathElements fun _ => True diff --git a/prover/server/formal-verification/FormalVerification/Merkle.lean b/prover/server/formal-verification/FormalVerification/Merkle.lean index 248040afe8..c67d16e44e 100644 --- a/prover/server/formal-verification/FormalVerification/Merkle.lean +++ b/prover/server/formal-verification/FormalVerification/Merkle.lean @@ -27,25 +27,28 @@ lemma ProveParentHash_rw {d : Bool} {h s : F} {k : F → Prop}: lemma MerkleTree.recover_succ' {ix : List.Vector Bool (Nat.succ N)} {proof : List.Vector F (Nat.succ N)} : MerkleTree.recover poseidon₂ ix proof item = hashLevel ix.head proof.head (MerkleTree.recover poseidon₂ ix.tail proof.tail item) := Eq.refl _ -theorem MerkleRootGadget_rw {h i : F} {p : List.Vector F 26} {k : F → Prop}: - LightProver.MerkleRootGadget_26_26 h i p k ↔ ∃ (hi : i.val < 2^26), k (MerkleTree.recoverAtFin poseidon₂ ⟨i.val, hi⟩ p.reverse h) := by - unfold LightProver.MerkleRootGadget_26_26 - have : 2^26 < Order := by decide - simp_rw [Gates, GatesGnark8, Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt this, ←exists_and_right] - rw [exists_swap] - apply exists_congr - intro - rw [←List.Vector.ofFn_get (v:=p)] - simp [List.Vector.getElem_map, ProveParentHash_rw, MerkleTree.recoverAtFin, MerkleTree.recover_succ', Fin.toBitsLE, Fin.toBitsBE, -List.Vector.ofFn_get] +theorem MerkleRootGadget_rw {h : F} {i : List.Vector Bool 26} {p : List.Vector F 26} {k : F → Prop}: + LightProver.MerkleRootGadget_26_26_26 h (i.map Bool.toZMod) p k ↔ k (MerkleTree.recover poseidon₂ i.reverse p.reverse h) := by + unfold LightProver.MerkleRootGadget_26_26_26 + simp only [List.Vector.getElem_map, ProveParentHash_rw] + rw [←List.Vector.ofFn_get (v:=p), ←List.Vector.ofFn_get (v:=i)] rfl -lemma InclusionProofStep_rw {l i e r} {k : F → Prop}: - (LightProver.MerkleRootGadget_26_26 l i e fun gate_0 => Gates.eq gate_0 r ∧ k gate_0) ↔ +theorem InclusionProofStep_rw {l i e r} {k : F → Prop}: + (∃b, Gates.to_binary i 26 b ∧ LightProver.MerkleRootGadget_26_26_26 l b e fun o => Gates.eq o r ∧ k o) ↔ (∃ (hi : i.val < 2^26), MerkleTree.recoverAtFin poseidon₂ ⟨i.val, hi⟩ e.reverse l = r) ∧ k r := by - simp [MerkleRootGadget_rw] + have : 2^26 < Order := by decide + simp only [Gates, GatesGnark8, Gates.to_binary_iff_eq_fin_to_bits_le_of_pow_length_lt this] + simp only [←exists_and_right] + rw [←exists_comm] + simp only [exists_eq_left, MerkleRootGadget_rw, GatesDef.eq, MerkleTree.recoverAtFin, Fin.toBitsLE] apply Iff.intro - . rintro ⟨_, ⟨_⟩, _⟩; tauto - . rintro ⟨⟨_, ⟨_⟩⟩⟩; tauto + · rintro ⟨_, _, _⟩ + simp_all + tauto + · rintro ⟨_, _⟩ + simp_all + tauto lemma InclusionProof_rw {roots leaves inPathIndices inPathElements k}: LightProver.InclusionProof_8_8_8_26_8_8_26 roots leaves inPathIndices inPathElements k ↔ @@ -92,11 +95,94 @@ theorem InclusionProof_correct [Fact (CollisionResistant poseidon₂)] {trees : rw [←this] congr -theorem InclusionCircuit_correct [Fact (CollisionResistant poseidon₂)] {trees : List.Vector (MerkleTree F poseidon₂ 26) 8} {leaves : List.Vector F 8}: - (∃inPathIndices proofs, LightProver.InclusionCircuit_8_8_8_26_8_8_26 (trees.map (·.root)) leaves inPathIndices proofs) ↔ - ∀i (_: i∈[0:8]), leaves[i] ∈ trees[i] := by +def inputHash (h₂ : Hash F 2) (h₃ : Hash F 3) (l r : List.Vector F (d + 1)) : F := + l.zipWith (·,·) r |>.tail |>.toList |>.foldl (fun h (l, r) => h₃ vec![h, l, r]) (h₂ vec![l.head, r.head]) + +lemma inputHash_next_correct {h₃ d} {l₁ l₂ : List.Vector (F × F) d} {a₁ a₂ : F} [Fact (CollisionResistant h₃)]: + l₁.toList.foldl (fun h (l, r) => h₃ vec![h, l, r]) a₁ = l₂.toList.foldl (fun h (l, r) => h₃ vec![h, l, r]) a₂ ↔ + a₁ = a₂ ∧ l₁ = l₂ := by + induction d generalizing a₁ a₂ with + | zero => + cases l₁ using List.Vector.casesOn + cases l₂ using List.Vector.casesOn + simp + | succ d ih => + cases l₁ using List.Vector.casesOn with | cons h₁ tl₁ => + cases l₂ using List.Vector.casesOn with | cons h₂ tl₂ => + cases h₁ + cases h₂ + simp [ih] + cases tl₁ + cases tl₂ + apply Iff.intro + · intro ⟨l, _⟩ + injections l + simp_all + · intro ⟨_, r⟩ + injections r + simp_all + +lemma List.Vector.zipWith_prod_eq_iff_inputs_eq {l₁ l₂ r₁ r₂ : Vector α d}: l₁.zipWith (·,·) l₂ = r₁.zipWith (·,·) r₂ ↔ l₁ = r₁ ∧ l₂ = r₂ := by + simp only [zipWith] + rw [Subtype.eq_iff] + simp only + induction d with + | zero => + cases l₁ using List.Vector.casesOn + cases l₂ using List.Vector.casesOn + cases r₁ using List.Vector.casesOn + cases r₂ using List.Vector.casesOn + simp + | succ d ih => + cases l₁ using List.Vector.casesOn with | cons h₁ tl₁ => + cases l₂ using List.Vector.casesOn with | cons h₂ tl₂ => + cases r₁ using List.Vector.casesOn with | cons h₃ tl₁ => + cases r₂ using List.Vector.casesOn with | cons h₄ tl₂ => + simp [ih] + apply Iff.intro + . intro ⟨_, h⟩ + simp_all + . intro ⟨h₁, h₂⟩ + injections h₁ + simp_all [Vector, Subtype.eq_iff] + +theorem inputHash_correct {d h₂ h₃} {l₁ r₁ l₂ r₂ : List.Vector F (d + 1)} [Fact (CollisionResistant h₂)] [Fact (CollisionResistant h₃)]: + inputHash h₂ h₃ l₁ r₁ = inputHash h₂ h₃ l₂ r₂ ↔ l₁ = l₂ ∧ r₁ = r₂ := by + cases l₁ using List.Vector.casesOn with | cons _ l₁ => + cases l₂ using List.Vector.casesOn with | cons _ l₂ => + cases r₁ using List.Vector.casesOn with | cons _ r₁ => + cases r₂ using List.Vector.casesOn with | cons _ r₂ => + simp only [inputHash, inputHash_next_correct] + simp [List.Vector.zipWith_prod_eq_iff_inputs_eq] + apply Iff.intro + · intro ⟨h, _⟩ + injections h + simp_all + · intro ⟨h, _⟩ + injections h + simp_all [List.Vector, Subtype.eq_iff] + +lemma TwoInputsHashChain_rw {h₁ h₂: List.Vector F 8} {k : F → Prop}: + LightProver.TwoInputsHashChain_8_8 h₁ h₂ k ↔ k (inputHash poseidon₂ poseidon₃ h₁ h₂) := by + unfold LightProver.TwoInputsHashChain_8_8 + repeat cases h₁ using List.Vector.casesOn; rename_i _ h₁ + repeat cases h₂ using List.Vector.casesOn; rename_i _ h₂ + simp only [Poseidon3_iff_uniqueAssignment, Poseidon2_iff_uniqueAssignment, inputHash] + simp only [List.Vector.zipWith_tail, List.Vector.zipWith_toList, List.Vector.toList_tail, List.Vector.toList_cons, List.tail, List.Vector.toList_nil, List.Vector.head_cons] + apply Iff.of_eq + rfl + +theorem InclusionCircuit_rw: + LightProver.InclusionCircuit_8_8_8_26_8_8_26 h roots leaves inPathIndices inPathElements ↔ + h = inputHash poseidon₂ poseidon₃ roots leaves ∧ + LightProver.InclusionProof_8_8_8_26_8_8_26 roots leaves inPathIndices inPathElements (fun _ => True) := by unfold LightProver.InclusionCircuit_8_8_8_26_8_8_26 - simp [InclusionProof_correct] + simp only [TwoInputsHashChain_rw, Gates, GatesGnark8, GatesDef.eq] + +theorem InclusionCircuit_correct [Fact (CollisionResistant poseidon₂)] {ih : F} {trees : List.Vector (MerkleTree F poseidon₂ 26) 8} {leaves : List.Vector F 8}: + (∃inPathIndices proofs, LightProver.InclusionCircuit_8_8_8_26_8_8_26 ih (trees.map (·.root)) leaves inPathIndices proofs) ↔ + ih = (inputHash poseidon₂ poseidon₃ (trees.map (·.root)) leaves) ∧ ∀i (_: i∈[0:8]), leaves[i] ∈ trees[i] := by + simp [InclusionCircuit_rw, InclusionProof_correct] lemma LeafHashGadget_rw {r : Range} {v : F} {k : F → Prop}: LightProver.LeafHashGadget r.lo r.index r.hi v k ↔ v ∈ r ∧ k r.hash := by @@ -147,23 +233,9 @@ lemma LeafHashGadget_rw {r : Range} {v : F} {k : F → Prop}: . exact Nat.lt_trans r.hi.prop (by decide) theorem MerkleRootGadget_eq_rw [Fact (CollisionResistant poseidon₂)] {h i : F} {p : List.Vector F 26} {tree : MerkleTree F poseidon₂ 26} {k : F → Prop}: - LightProver.MerkleRootGadget_26_26 h i p (fun r => Gates.eq r tree.root ∧ k r) ↔ (∃(hi: i.val < 2^26), h = tree.itemAtFin ⟨i.val, hi⟩ ∧ p.reverse = tree.proofAtFin ⟨i.val, hi⟩) ∧ k tree.root := by - simp [MerkleRootGadget_rw] - rw [←exists_and_right] - apply exists_congr - simp [Gates, GatesGnark8, -MerkleTree.recoverAtFin_eq_root_iff_proof_and_item_correct] - intro i - apply Iff.intro - . intro ⟨l, r⟩ - rw [l] at r - simp at l - rcases l with ⟨_, l⟩ - simp [*] - . intro ⟨l, r⟩ - have l' := l - rw [And.comm, ←MerkleTree.recoverAtFin_eq_root_iff_proof_and_item_correct] at l' - rw [l'] - simp [*] + (∃gate, Gates.to_binary i 26 gate ∧ LightProver.MerkleRootGadget_26_26_26 h gate p (fun r => Gates.eq r tree.root ∧ k r)) ↔ (∃(hi: i.val < 2^26), h = tree.itemAtFin ⟨i.val, hi⟩ ∧ p.reverse = tree.proofAtFin ⟨i.val, hi⟩) ∧ k tree.root := by + rw [InclusionProofStep_rw] + simp [and_comm] lemma LeafHashGadget_hashing {p : F → Prop} : (LightProver.LeafHashGadget lo nxt hi leaf p) → p (poseidon₃ vec![lo, nxt, hi]) := by simp [LightProver.LeafHashGadget] @@ -181,7 +253,8 @@ lemma LeafHashGadget_in_tree [Fact (CollisionResistant poseidon₃)] {p : F → theorem MerkleTreeRoot_LeafHashGadget_rw [Fact (CollisionResistant poseidon₃)] [Fact (CollisionResistant poseidon₂)] {lo hi nxt leaf ind proof} {k : F → Prop } {tree : RangeTree 26}: (LightProver.LeafHashGadget lo nxt hi leaf fun r => - LightProver.MerkleRootGadget_26_26 r ind proof fun root => Gates.eq root tree.val.root ∧ k root) + ∃lv, Gates.to_binary ind 26 lv ∧ + LightProver.MerkleRootGadget_26_26_26 r lv proof fun root => Gates.eq root tree.val.root ∧ k root) ↔ ∃(range : Range) (h: ind.val < 2^26), tree.val.itemAtFin ⟨ind.val, h⟩ = range.hash ∧ lo = range.lo ∧ nxt = range.index ∧ hi = range.hi ∧ proof.reverse = tree.val.proofAtFin ⟨ind.val, h⟩ ∧ leaf ∈ range ∧ k tree.val.root := by apply Iff.intro . intro h @@ -207,7 +280,8 @@ def NonInclusionProof_rec {n : Nat} (lo nxt hi leaf inds roots : List.Vector F n match n with | 0 => k List.Vector.nil | _ + 1 => LightProver.LeafHashGadget lo.head nxt.head hi.head leaf.head fun r => - LightProver.MerkleRootGadget_26_26 r inds.head proofs.head fun root => + ∃lv, Gates.to_binary inds.head 26 lv ∧ + LightProver.MerkleRootGadget_26_26_26 r lv proofs.head fun root => Gates.eq root roots.head ∧ NonInclusionProof_rec lo.tail nxt.tail hi.tail leaf.tail inds.tail roots.tail proofs.tail fun rs => k (root ::ᵥ rs) lemma NonInclusionProof_rec_equiv {lo nxt hi leaf inds roots proofs k}: @@ -294,23 +368,24 @@ theorem NonInclusionCircuit_rec_correct [Fact (CollisionResistant poseidon₃)] . decide theorem NonInclusionCircuit_correct [Fact (CollisionResistant poseidon₃)] [Fact (CollisionResistant poseidon₂)] {trees : List.Vector (RangeTree 26) 8} {leaves : List.Vector F 8}: - (∃lo hi nxt inds proofs, LightProver.NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 (trees.map (·.val.root)) leaves lo hi nxt inds proofs) ↔ - ∀i (_: i∈[0:8]), leaves[i] ∈ trees[i] := by + (∃lo hi nxt inds proofs, LightProver.NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 h (trees.map (·.val.root)) leaves lo hi nxt inds proofs) ↔ + h = inputHash poseidon₂ poseidon₃ (trees.map (·.val.root)) leaves ∧ ∀i (_: i∈[0:8]), leaves[i] ∈ trees[i] := by unfold LightProver.NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 - simp [←NonInclusionProof_rec_equiv, NonInclusionCircuit_rec_correct, Gates, GatesGnark8] + simp [←NonInclusionProof_rec_equiv, NonInclusionCircuit_rec_correct, Gates, GatesGnark8, TwoInputsHashChain_rw] lemma InclusionProof_swap_ex {k : α → List.Vector F 8 → Prop} : (∃ a, LightProver.InclusionProof_8_8_8_26_8_8_26 x y z w fun r => k a r) ↔ LightProver.InclusionProof_8_8_8_26_8_8_26 x y z w fun r => ∃a, k a r := by simp [InclusionProof_rw] - theorem CombinedCircuit_correct [Fact (CollisionResistant poseidon₃)] [Fact (CollisionResistant poseidon₂)] {inclusionTrees : List.Vector (MerkleTree F poseidon₂ 26) 8} { nonInclusionTrees : List.Vector (RangeTree 26) 8} {inclusionLeaves nonInclusionLeaves : List.Vector F 8}: - (∃a b c d e f g, LightProver.CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 (inclusionTrees.map (·.root)) inclusionLeaves a b (nonInclusionTrees.map (·.val.root)) nonInclusionLeaves c d e f g) ↔ + (∃a b c d e f g, LightProver.CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 h (inclusionTrees.map (·.root)) inclusionLeaves a b (nonInclusionTrees.map (·.val.root)) nonInclusionLeaves c d e f g) ↔ + h = poseidon₂ vec![inputHash poseidon₂ poseidon₃ (inclusionTrees.map (·.root)) inclusionLeaves, inputHash poseidon₂ poseidon₃ (nonInclusionTrees.map (·.val.root)) nonInclusionLeaves] ∧ ∀i (_: i∈[0:8]), inclusionLeaves[i] ∈ inclusionTrees[i] ∧ nonInclusionLeaves[i] ∈ nonInclusionTrees[i] := by unfold LightProver.CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 - simp [InclusionProof_swap_ex, InclusionProof_correct, ←NonInclusionProof_rec_equiv, NonInclusionCircuit_rec_correct] + simp [InclusionProof_swap_ex, InclusionProof_correct, ←NonInclusionProof_rec_equiv, NonInclusionCircuit_rec_correct, TwoInputsHashChain_rw, Gates, GatesGnark8, GatesDef.eq] + rintro _ apply Iff.intro . tauto . intro hp diff --git a/prover/server/prover/batch_circuit_helpers.go b/prover/server/prover/batch_circuit_helpers.go index 948f4cc204..e2d52b64ca 100644 --- a/prover/server/prover/batch_circuit_helpers.go +++ b/prover/server/prover/batch_circuit_helpers.go @@ -19,18 +19,27 @@ func createHashChain(api frontend.API, hashes []frontend.Variable) frontend.Vari return computeHashChain(api, initialHash, hashes) } -func createTwoInputsHashChain(api frontend.API, hashesFirst []frontend.Variable, hashesSecond []frontend.Variable) frontend.Variable { - if len(hashesFirst) == 0 { - return abstractor.Call(api, poseidon.Poseidon2{In1: hashesFirst[0], In2: hashesSecond[0]}) +type TwoInputsHashChain struct { + HashesFirst []frontend.Variable + HashesSecond []frontend.Variable +} + +func (gadget TwoInputsHashChain) DefineGadget(api frontend.API) interface{} { + if len(gadget.HashesFirst) == 0 { + panic("HashesFirst must not be empty") } - hashChain := abstractor.Call(api, poseidon.Poseidon2{In1: hashesFirst[0], In2: hashesSecond[0]}) - for i := 1; i < len(hashesFirst); i++ { - hashChain = abstractor.Call(api, poseidon.Poseidon3{In1: hashChain, In2: hashesFirst[i], In3: hashesSecond[i]}) + hashChain := abstractor.Call(api, poseidon.Poseidon2{In1: gadget.HashesFirst[0], In2: gadget.HashesSecond[0]}) + for i := 1; i < len(gadget.HashesFirst); i++ { + hashChain = abstractor.Call(api, poseidon.Poseidon3{In1: hashChain, In2: gadget.HashesFirst[i], In3: gadget.HashesSecond[i]}) } return hashChain } +func createTwoInputsHashChain(api frontend.API, hashesFirst []frontend.Variable, hashesSecond []frontend.Variable) frontend.Variable { + return abstractor.Call(api, TwoInputsHashChain{HashesFirst: hashesFirst, HashesSecond: hashesSecond}) +} + func computeHashChain(api frontend.API, initialHash frontend.Variable, hashes []frontend.Variable) frontend.Variable { hashChain := initialHash diff --git a/prover/server/prover/combined_circuit.go b/prover/server/prover/combined_circuit.go index d264bc9a69..abbc0a37b5 100644 --- a/prover/server/prover/combined_circuit.go +++ b/prover/server/prover/combined_circuit.go @@ -9,8 +9,8 @@ import ( type CombinedCircuit struct { PublicInputHash frontend.Variable `gnark:",public"` - Inclusion InclusionProof `gnark:",input"` - NonInclusion NonInclusionProof `gnark:",input"` + Inclusion InclusionProof `gnark:"input"` + NonInclusion NonInclusionProof `gnark:"input"` } func (circuit *CombinedCircuit) Define(api frontend.API) error { diff --git a/prover/server/prover/inclusion_circuit.go b/prover/server/prover/inclusion_circuit.go index b42f698055..1de07aad05 100644 --- a/prover/server/prover/inclusion_circuit.go +++ b/prover/server/prover/inclusion_circuit.go @@ -11,12 +11,12 @@ type InclusionCircuit struct { PublicInputHash frontend.Variable `gnark:",public"` // hashed public inputs - Roots []frontend.Variable `gnark:",input"` - Leaves []frontend.Variable `gnark:",input"` + Roots []frontend.Variable `gnark:"input"` + Leaves []frontend.Variable `gnark:"input"` // private inputs - InPathIndices []frontend.Variable `gnark:",input"` - InPathElements [][]frontend.Variable `gnark:",input"` + InPathIndices []frontend.Variable `gnark:"input"` + InPathElements [][]frontend.Variable `gnark:"input"` NumberOfCompressedAccounts uint32 Height uint32