diff --git a/light-prover/formal-verification/FormalVerification/Circuit.lean b/light-prover/formal-verification/FormalVerification/Circuit.lean index 2db14617ba..83f80b38d0 100644 --- a/light-prover/formal-verification/FormalVerification/Circuit.lean +++ b/light-prover/formal-verification/FormalVerification/Circuit.lean @@ -315,11 +315,10 @@ def Poseidon3 (In1: F) (In2: F) (In3: F) (k: F -> Prop): Prop := k gate_0[0] def LeafHashGadget (LeafLowerRangeValue: F) (NextIndex: F) (LeafHigherRangeValue: F) (Value: F) (k: F -> Prop): Prop := - Gates.ne LeafLowerRangeValue Value ∧ AssertIsLess_248 LeafLowerRangeValue Value ∧ AssertIsLess_248 Value LeafHigherRangeValue ∧ - Poseidon3 LeafLowerRangeValue NextIndex LeafHigherRangeValue fun gate_3 => - k gate_3 + Poseidon3 LeafLowerRangeValue NextIndex LeafHigherRangeValue fun gate_2 => + k gate_2 def NonInclusionProof_10_10_10_10_10_10_20_10_10_20 (Roots: Vector F 10) (Values: Vector F 10) (LeafLowerRangeValues: Vector F 10) (LeafHigherRangeValues: Vector F 10) (NextIndices: Vector F 10) (InPathIndices: Vector F 10) (InPathElements: Vector (Vector F 20) 10) (k: Vector F 10 -> Prop): Prop := LeafHashGadget LeafLowerRangeValues[0] NextIndices[0] LeafHigherRangeValues[0] Values[0] fun gate_0 => @@ -359,17 +358,7 @@ def InclusionCircuit_10_10_10_20_10_10_20 (Roots: Vector F 10) (Leaves: Vector F True def NonInclusionCircuit_10_10_10_10_10_10_20_10_10_20 (Roots: Vector F 10) (Values: Vector F 10) (LeafLowerRangeValues: Vector F 10) (LeafHigherRangeValues: Vector F 10) (NextIndices: Vector F 10) (InPathIndices: Vector F 10) (InPathElements: Vector (Vector F 20) 10): Prop := - NonInclusionProof_10_10_10_10_10_10_20_10_10_20 Roots Values LeafLowerRangeValues LeafHigherRangeValues NextIndices InPathIndices InPathElements fun gate_0 => - Gates.eq gate_0[0] Roots[0] ∧ - Gates.eq gate_0[1] Roots[1] ∧ - Gates.eq gate_0[2] Roots[2] ∧ - Gates.eq gate_0[3] Roots[3] ∧ - Gates.eq gate_0[4] Roots[4] ∧ - Gates.eq gate_0[5] Roots[5] ∧ - Gates.eq gate_0[6] Roots[6] ∧ - Gates.eq gate_0[7] Roots[7] ∧ - Gates.eq gate_0[8] Roots[8] ∧ - Gates.eq gate_0[9] Roots[9] ∧ + NonInclusionProof_10_10_10_10_10_10_20_10_10_20 Roots Values LeafLowerRangeValues LeafHigherRangeValues NextIndices InPathIndices InPathElements fun _ => True def CombinedCircuit_10_10_10_20_10_10_10_10_10_10_10_20_10 (Inclusion_Roots: Vector F 10) (Inclusion_Leaves: Vector F 10) (Inclusion_InPathIndices: Vector F 10) (Inclusion_InPathElements: Vector (Vector F 20) 10) (NonInclusion_Roots: Vector F 10) (NonInclusion_Values: Vector F 10) (NonInclusion_LeafLowerRangeValues: Vector F 10) (NonInclusion_LeafHigherRangeValues: Vector F 10) (NonInclusion_NextIndices: Vector F 10) (NonInclusion_InPathIndices: Vector F 10) (NonInclusion_InPathElements: Vector (Vector F 20) 10): Prop := diff --git a/light-prover/formal-verification/FormalVerification/Merkle.lean b/light-prover/formal-verification/FormalVerification/Merkle.lean index 250d79494d..d753804bbe 100644 --- a/light-prover/formal-verification/FormalVerification/Merkle.lean +++ b/light-prover/formal-verification/FormalVerification/Merkle.lean @@ -101,7 +101,7 @@ lemma LeafHashGadget_rw {r : Range} {v : F} {k : F → Prop}: unfold LightProver.LeafHashGadget simp only [Poseidon3_iff_uniqueAssignment] apply Iff.intro - . rintro ⟨_, lo, hi, cont⟩ + . rintro ⟨lo, hi, cont⟩ apply And.intro _ cont have lo' := AssertIsLess_range (by rw [ZMod.val_nat_cast, Nat.mod_eq_of_lt] @@ -114,11 +114,7 @@ lemma LeafHashGadget_rw {r : Range} {v : F} {k : F → Prop}: . exact Nat.lt_trans r.hi.prop (by decide) . exact Nat.lt_trans r.lo.prop (by decide) . rintro ⟨⟨lo, hi⟩, cont⟩ - refine ⟨?_, ?_, ?_, cont⟩ - . rintro ⟨_⟩ - rw [ZMod.val_nat_cast, Nat.mod_eq_of_lt] at lo - . linarith - . exact Nat.lt_trans r.lo.prop (by decide) + refine ⟨?_, ?_, cont⟩ . rw [AssertIsLess_248_semantics] zify zify at lo hi diff --git a/light-prover/prover/circuit_utils.go b/light-prover/prover/circuit_utils.go index 7b3c3d8605..c687acf9ba 100644 --- a/light-prover/prover/circuit_utils.go +++ b/light-prover/prover/circuit_utils.go @@ -125,7 +125,6 @@ type LeafHashGadget struct { // Limit the number of bits to 248 + 1, // since we truncate address values to 31 bytes. func (gadget LeafHashGadget) DefineGadget(api frontend.API) interface{} { - api.AssertIsDifferent(gadget.LeafLowerRangeValue, gadget.Value) // Lower bound is less than value abstractor.CallVoid(api, AssertIsLess{A: gadget.LeafLowerRangeValue, B: gadget.Value, N: 248}) // Value is less than upper bound @@ -146,7 +145,8 @@ func (gadget AssertIsLess) DefineGadget(api frontend.API) interface{} { // Add 2^N to B to ensure a positive number oneShifted := new(big.Int).Lsh(big.NewInt(1), uint(gadget.N)) num := api.Add(gadget.A, api.Sub(*oneShifted, gadget.B)) - return api.ToBinary(num, gadget.N) + api.ToBinary(num, gadget.N) + return []frontend.Variable{} } type MerkleRootGadget struct { diff --git a/light-prover/prover/is_less_test.go b/light-prover/prover/is_less_test.go index e497574440..aebc2a221c 100644 --- a/light-prover/prover/is_less_test.go +++ b/light-prover/prover/is_less_test.go @@ -1,6 +1,7 @@ package prover import ( + "github.com/reilabs/gnark-lean-extractor/v2/abstractor" "math/big" "testing" @@ -21,7 +22,7 @@ func (circuit *IsLessCircuit) Define(api frontend.API) error { B: circuit.B, N: 248, } - AssertIsLess(isLess).DefineGadget(api) + abstractor.CallVoid(api, isLess) return nil } diff --git a/light-prover/prover/non_inclusion_circuit.go b/light-prover/prover/non_inclusion_circuit.go index a69af9d063..789bbeb372 100644 --- a/light-prover/prover/non_inclusion_circuit.go +++ b/light-prover/prover/non_inclusion_circuit.go @@ -39,10 +39,7 @@ func (circuit *NonInclusionCircuit) Define(api frontend.API) error { NumberOfCompressedAccounts: circuit.NumberOfCompressedAccounts, Depth: circuit.Depth, } - roots := abstractor.Call1(api, proof) - for i := 0; i < int(circuit.NumberOfCompressedAccounts); i++ { - api.AssertIsEqual(roots[i], circuit.Roots[i]) - } + abstractor.Call1(api, proof) return nil }