progress on address tree

reilabs · Feb 15, 2025 · a37c2bc · a37c2bc
1 parent d50fda8
commit a37c2bc
Show file tree

Hide file tree

Showing 10 changed files with 315 additions and 57 deletions.
diff --git 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
@@ -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
@@ -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