Wire UnlinkPool LazyIMT insertion body

Benchmark/Cases/UnlinkXyz/Pool/Contract.lean

@@ -44,8 +44,7 @@
   carry nested dynamic members (`uint256[] nullifierHashes`,
   `Ciphertext[] ciphertexts`, etc.). The remaining fidelity gaps are the parts
   that still need first-class source equivalents in Verity or this model: the
-  LazyIMT insertion body behind `_insertLeaves` and the external cryptographic
-  / Permit2 boundaries tracked in the case manifest.
+  external cryptographic / Permit2 boundaries tracked in the case manifest.
 -/
 import Contracts.Common
 import Compiler.ECM
@@ -327,6 +326,44 @@ verity_contract UnlinkPool where
     -- "DepositWitness(address pool,bytes32 notesHash)").
     DEPOSIT_WITNESS_TYPEHASH : Uint256 :=
       0xbc5a735b1283bedbbb26bd202f39770544802f342490e830972aacc15681b130
+    SNARK_SCALAR_FIELD : Uint256 :=
+      21888242871839275222246405745257275088548364400416034343698204186575808495617
+    MAX_LAZY_INDEX : Uint256 := 0xffffffff
+    MAX_NOTE_VALUE : Uint256 :=
+      100000000000000000000000000000000000000000000000000000000000000000000
+    Z_0  : Uint256 := 0
+    Z_1  : Uint256 := 14744269619966411208579211824598458697587494354926760081771325075741142829156
+    Z_2  : Uint256 := 7423237065226347324353380772367382631490014989348495481811164164159255474657
+    Z_3  : Uint256 := 11286972368698509976183087595462810875513684078608517520839298933882497716792
+    Z_4  : Uint256 := 3607627140608796879659380071776844901612302623152076817094415224584923813162
+    Z_5  : Uint256 := 19712377064642672829441595136074946683621277828620209496774504837737984048981
+    Z_6  : Uint256 := 20775607673010627194014556968476266066927294572720319469184847051418138353016
+    Z_7  : Uint256 := 3396914609616007258851405644437304192396347162513310381425243293
+    Z_8  : Uint256 := 21551820661461729022865262380882070649935529853313286572328683688269863701601
+    Z_9  : Uint256 := 6573136701248752079028194407151022595060682063033565181951145966236778420039
+    Z_10 : Uint256 := 12413880268183407374852357075976609371175688755676981206018884971008854919922
+    Z_11 : Uint256 := 14271763308400718165336499097156975241954733520325982997864342600795471836726
+    Z_12 : Uint256 := 20066985985293572387227381049700832219069292839614107140851619262827735677018
+    Z_13 : Uint256 := 9394776414966240069580838672673694685292165040808226440647796406499139370960
+    Z_14 : Uint256 := 11331146992410411304059858900317123658895005918277453009197229807340014528524
+    Z_15 : Uint256 := 15819538789928229930262697811477882737253464456578333862691129291651619515538
+    Z_16 : Uint256 := 19217088683336594659449020493828377907203207941212636669271704950158751593251
+    Z_17 : Uint256 := 21035245323335827719745544373081896983162834604456827698288649288827293579666
+    Z_18 : Uint256 := 6939770416153240137322503476966641397417391950902474480970945462551409848591
+    Z_19 : Uint256 := 10941962436777715901943463195175331263348098796018438960955633645115732864202
+    Z_20 : Uint256 := 15019797232609675441998260052101280400536945603062888308240081994073687793470
+    Z_21 : Uint256 := 11702828337982203149177882813338547876343922920234831094975924378932809409969
+    Z_22 : Uint256 := 11217067736778784455593535811108456786943573747466706329920902520905755780395
+    Z_23 : Uint256 := 16072238744996205792852194127671441602062027943016727953216607508365787157389
+    Z_24 : Uint256 := 17681057402012993898104192736393849603097507831571622013521167331642182653248
+    Z_25 : Uint256 := 21694045479371014653083846597424257852691458318143380497809004364947786214945
+    Z_26 : Uint256 := 8163447297445169709687354538480474434591144168767135863541048304198280615192
+    Z_27 : Uint256 := 14081762237856300239452543304351251708585712948734528663957353575674639038357
+    Z_28 : Uint256 := 16619959921569409661790279042024627172199214148318086837362003702249041851090
+    Z_29 : Uint256 := 7022159125197495734384997711896547675021391130223237843255817587255104160365
+    Z_30 : Uint256 := 4114686047564160449611603615418567457008101555090703535405891656262658644463
+    Z_31 : Uint256 := 12549363297364877722388257367377629555213421373705596078299904496781819142130
+    Z_32 : Uint256 := 21443572485391568159800782191812935835534334817699172242223315142338162256601
 
   -- `ISignatureTransfer public immutable PERMIT2` (UnlinkPool.sol:55).
   -- Bound at construction time to a constructor-supplied address.
@@ -341,6 +378,7 @@ verity_contract UnlinkPool where
     external verifySpend(
       Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256,
       Uint256, Uint256, Uint256, Array Uint256, Array Uint256) -> (Bool)
+    external poseidonT3(Uint256, Uint256) -> (Uint256)
     external permitWitnessTransferFrom(
       Address, Address, Uint256, Uint256, Uint256, Address, Uint256, Address,
       Uint256, Bytes) -> (Bool)
@@ -465,15 +503,14 @@ verity_contract UnlinkPool where
       : Uint256 := do
     return (add npk amount)
 
+  function poseidon2 (lhs : Uint256, rhs : Uint256) : Uint256 := do
+    return externalCall "poseidonT3" [lhs, rhs]
+
   function validateNoteFields (npk : Uint256, token : Address, amount : Uint256) : Unit := do
     requireError (token != zeroAddress) PoolInvalidNoteToken()
-    requireError ((amount != 0) &&
-      (amount <=
-        100000000000000000000000000000000000000000000000000000000000000000000))
+    requireError ((amount != 0) && (amount <= MAX_NOTE_VALUE))
       PoolInvalidNoteAmount()
-    requireError ((npk != 0) &&
-      (npk <
-        21888242871839275222246405745257275088548364400416034343698204186575808495617))
+    requireError ((npk != 0) && (npk < SNARK_SCALAR_FIELD))
       PoolInvalidNoteNPK()
 
   function sumNoteAmounts (notes : Array Note) : Uint256 := do
@@ -622,21 +659,118 @@ verity_contract UnlinkPool where
         pure ())
     returnArray real
 
-  /- Source shape: `_insertLeaves(uint256[] memory _leafHashes)`.
-     The LazyIMT update is still represented by the existing lightweight
-     accumulator used by this scoped benchmark model. -/
-  function insertLeaves (leafHashes : Array Uint256) : Uint256 := do
-    let startIndex ← nextLeafIndex
-    let mut newRoot := startIndex
-    forEach "m" (arrayLength leafHashes) (do
-      let leaf := arrayElement leafHashes m
-      if leaf != 0 then
-        newRoot := add newRoot leaf
+  function lazyDefaultZero (index : Uint256) : Uint256 := do
+    let mut zero := Z_0
+    if index == 1 then zero := Z_1 else pure ()
+    if index == 2 then zero := Z_2 else pure ()
+    if index == 3 then zero := Z_3 else pure ()
+    if index == 4 then zero := Z_4 else pure ()
+    if index == 5 then zero := Z_5 else pure ()
+    if index == 6 then zero := Z_6 else pure ()
+    if index == 7 then zero := Z_7 else pure ()
+    if index == 8 then zero := Z_8 else pure ()
+    if index == 9 then zero := Z_9 else pure ()
+    if index == 10 then zero := Z_10 else pure ()
+    if index == 11 then zero := Z_11 else pure ()
+    if index == 12 then zero := Z_12 else pure ()
+    if index == 13 then zero := Z_13 else pure ()
+    if index == 14 then zero := Z_14 else pure ()
+    if index == 15 then zero := Z_15 else pure ()
+    if index == 16 then zero := Z_16 else pure ()
+    if index == 17 then zero := Z_17 else pure ()
+    if index == 18 then zero := Z_18 else pure ()
+    if index == 19 then zero := Z_19 else pure ()
+    if index == 20 then zero := Z_20 else pure ()
+    if index == 21 then zero := Z_21 else pure ()
+    if index == 22 then zero := Z_22 else pure ()
+    if index == 23 then zero := Z_23 else pure ()
+    if index == 24 then zero := Z_24 else pure ()
+    if index == 25 then zero := Z_25 else pure ()
+    if index == 26 then zero := Z_26 else pure ()
+    if index == 27 then zero := Z_27 else pure ()
+    if index == 28 then zero := Z_28 else pure ()
+    if index == 29 then zero := Z_29 else pure ()
+    if index == 30 then zero := Z_30 else pure ()
+    if index == 31 then zero := Z_31 else pure ()
+    if index == 32 then zero := Z_32 else pure ()
+    return zero
+
+  function lazyIndexForElement (level : Uint256, index : Uint256) : Uint256 := do
+    return (add (mul MAX_LAZY_INDEX level) index)
+
+  function lazyInsert (leaf : Uint256) : Unit := do
+    let startIndex ← getStorage lazyNumberOfLeaves
+    let maxIndex ← getStorage lazyMaxIndex
+    requireError (leaf < SNARK_SCALAR_FIELD) PoolInvalidOutputShape()
+    requireError (startIndex < maxIndex) PoolInvalidOutputShape()
+    setStorage lazyNumberOfLeaves (add startIndex 1)
+    let mut index := startIndex
+    let mut hash := leaf
+    let mut active := 1
+    forEach "level" 32 (do
+      if active != 0 then
+        let elementKey ← lazyIndexForElement level index
+        setMappingWord lazyElements elementKey 0 hash
+        if bitAnd index 1 == 0 then
+          active := 0
+        else
+          let siblingKey ← lazyIndexForElement level (sub index 1)
+          let sibling ← getMappingWord lazyElements siblingKey 0
+          let parent ← poseidon2 sibling hash
+          hash := parent
+          index := shr 1 index
       else
         pure ())
+
+  function lazyRootWithDepth32 () : Uint256 := do
+    let numberOfLeaves ← getStorage lazyNumberOfLeaves
+    if numberOfLeaves == 0 then
+      return Z_32
+    else
+      let levels ← allocArray 33
+      let mut index := sub numberOfLeaves 1
+      if bitAnd index 1 == 0 then
+        let elementKey ← lazyIndexForElement 0 index
+        let element ← getMappingWord lazyElements elementKey 0
+        setMemoryArrayElement levels 0 element
+      else
+        setMemoryArrayElement levels 0 Z_0
+      forEach "level" 32 (do
+        let current := arrayElement levels level
+        if bitAnd index 1 == 0 then
+          let z ← lazyDefaultZero level
+          let parent ← poseidon2 current z
+          setMemoryArrayElement levels (add level 1) parent
+        else
+          let levelCount := shr (add level 1) numberOfLeaves
+          let parentIndex := shr 1 index
+          if levelCount > parentIndex then
+            let parentKey ← lazyIndexForElement (add level 1) parentIndex
+            let parent ← getMappingWord lazyElements parentKey 0
+            setMemoryArrayElement levels (add level 1) parent
+          else
+            let siblingKey ← lazyIndexForElement level (sub index 1)
+            let sibling ← getMappingWord lazyElements siblingKey 0
+            let parent ← poseidon2 sibling current
+            setMemoryArrayElement levels (add level 1) parent
+        index := shr 1 index)
+      return (arrayElement levels 32)
+
+  /- Source shape: `_insertLeaves(uint256[] memory _leafHashes)`.
+     Appends each leaf through the flattened LazyIMT spine and recomputes the
+     depth-32 root, matching `InternalLazyIMT._insert` / `_root(self, 32)`. -/
+  function insertLeaves (leafHashes : Array Uint256) : Uint256 := do
+    let count := arrayLength leafHashes
+    if count == 0 then
+      let currentRoot ← getStorage stateMerkleRoot
+      return currentRoot
+    else
+      forEach "m" count (do
+        let leaf := arrayElement leafHashes m
+        lazyInsert leaf)
+    let newRoot ← lazyRootWithDepth32
     setStorage stateMerkleRoot newRoot
     setMappingWord stateRootSeen newRoot 0 1
-    setStorage lazyNumberOfLeaves (add startIndex (arrayLength leafHashes))
     return newRoot
 
   function view computeContextHash (ciphertexts : Array Ciphertext) : Uint256 := do

cases/unlink_xyz/pool/case.yaml

@@ -39,7 +39,6 @@ abstraction_tags:
   - uups_proxy_modeled_as_implementation
   - permit2_assumed_boundary
   - poseidon_assumed_boundary
-  - lazy_imt_assumed_boundary
   - groth16_assumed_boundary
   - bn254_precompile_ecm
   - erc7201_storage_namespace
@@ -75,8 +74,8 @@ abstraction_notes: >
   elements, computes the source-shaped deposit witness hash, routes the Permit2
   transfer through the assumed external boundary, inserts leaves, and emits the
   source-shaped `Deposited` payload. Remaining promotion blockers are fidelity
-  gaps rather than basic body expressibility: the `_insertLeaves` body still
-  uses this scoped model's lightweight LazyIMT accumulator boundary.
+  gaps rather than basic body expressibility: Poseidon, Permit2, Groth16, and
+  host-level UUPS proxy behavior remain as explicit boundaries.
   `_executeWithdrawal(_transactions[i], bool)` is routed through an internal
   helper call. The deploy-time BN254 precompile probe in `initialize` is wired
   through the 0x06/0x07/0x08 precompile ECMs and the multi-result ECM binder.
@@ -106,11 +105,9 @@ abstraction_notes: >
     - `deposit`, `transfer`, `withdraw`, and `emergencyWithdraw` bodies are wired,
       but still carry the fidelity gaps listed above.
 unsupported_feature_codes:
-  - lazy_imt_insert_body_assumed
   - uups_proxy_storage_rotation_not_modeled
   - poseidon_assumed_axiom
   - permit2_assumed_axiom
-  - lazy_imt_assumed_axiom
   - groth16_verifier_assumed_axiom
 notes: >
   This case replaces the previous `backlog/unlink_xyz/placeholder` entry, which