Use Unlink memory array helpers

Benchmark/Cases/UnlinkXyz/Pool/Contract.lean

@@ -42,10 +42,8 @@
   These shapes use struct-array parameters whose elements 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: memory-array return
-  helpers for `_realCommitments` / `_realNullifiers`, the source-level
-  memory-array value passed into `_insertLeaves`, and dynamic array event
-  payloads.
+  first-class source equivalents in Verity or this model: dynamic array event
+  payloads and the LazyIMT insertion body behind `_insertLeaves`.
 -/
 import Contracts.Common
 import Compiler.Modules.Hashing
@@ -402,26 +400,69 @@ verity_contract UnlinkPool where
       else
         pure ())
 
-  /- Source shape: `_insertLeaves(_realCommitments(values, excludeIndex))`.
-     Verity does not yet model memory-array-return helpers, so this helper
-     fuses the source filter with the `_insertLeaves` state update while
-     keeping the insertion side-effect factored out of entry points. -/
-  function insertFilteredLeaves
-      (values : Array Uint256, excludeIndex : Uint256, leafCount : Uint256,
-       startIndex : Uint256) : Uint256 := do
-    let mut newRoot := startIndex
-    forEach "m" (arrayLength values) (do
-      let leaf := arrayElement values m
-      if m != excludeIndex then
-        if leaf != 0 then
-          newRoot := add newRoot leaf
+  function realCommitments
+      (newCommitments : Array Uint256, excludeIndex : Uint256)
+      : Array Uint256 := do
+    let len := arrayLength newCommitments
+    let mut count := 0
+    forEach "i" len (do
+      let commitment := arrayElement newCommitments i
+      if i != excludeIndex then
+        if commitment != 0 then
+          count := add count 1
+        else
+          pure ()
+      else
+        pure ())
+    let leaves ← allocArray count
+    let mut j := 0
+    forEach "i" len (do
+      let commitment := arrayElement newCommitments i
+      if i != excludeIndex then
+        if commitment != 0 then
+          setMemoryArrayElement leaves j commitment
+          j := add j 1
         else
           pure ()
       else
         pure ())
+    returnArray leaves
+
+  function realNullifiers (nullifierHashes : Array Uint256) : Array Uint256 := do
+    let len := arrayLength nullifierHashes
+    let mut count := 0
+    forEach "i" len (do
+      let nullifierHash := arrayElement nullifierHashes i
+      if nullifierHash != 0 then
+        count := add count 1
+      else
+        pure ())
+    let real ← allocArray count
+    let mut j := 0
+    forEach "i" len (do
+      let nullifierHash := arrayElement nullifierHashes i
+      if nullifierHash != 0 then
+        setMemoryArrayElement real j nullifierHash
+        j := add j 1
+      else
+        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
+      else
+        pure ())
     setStorage stateMerkleRoot newRoot
     setMappingWord stateRootSeen newRoot 0 1
-    setStorage lazyNumberOfLeaves (add startIndex leafCount)
+    setStorage lazyNumberOfLeaves (add startIndex (arrayLength leafHashes))
     return newRoot
 
   function view computeContextHash (ciphertexts : Array Ciphertext) : Uint256 := do
@@ -503,16 +544,14 @@ verity_contract UnlinkPool where
       requireError proofOk PoolProofVerificationFailed()
       requireError ok PoolProofVerificationFailed()
       spendNullifiers txn.nullifierHashes
-      let startIndex ← nextLeafIndex
-      let newRoot ← insertFilteredLeaves txn.newCommitments
-        0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
-        ciphertextCount
-        startIndex
-      let realNullifierCount ← countNonZero txn.nullifierHashes
+      let leaves ← realCommitments txn.newCommitments
         0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+      let startIndex ← nextLeafIndex
+      let newRoot ← insertLeaves leaves
+      let realNullifierHashes ← realNullifiers txn.nullifierHashes
       emit "Transferred"
-        [newRoot, startIndex, ciphertextCount,
-         realNullifierCount,
+        [newRoot, startIndex, arrayLength leaves,
+         arrayLength realNullifierHashes,
          arrayLength txn.ciphertexts])
 
   /- `_executeWithdrawal(WithdrawalTransaction calldata _txn, bool _emergency)`
@@ -568,28 +607,28 @@ verity_contract UnlinkPool where
     requireError proofOk PoolProofVerificationFailed()
     requireError ok PoolProofVerificationFailed()
     spendNullifiers txn.nullifierHashes
+    let leaves ← realCommitments txn.newCommitments wSlot
     let startIndex ← nextLeafIndex
-    let newRoot ← insertFilteredLeaves txn.newCommitments wSlot ciphertextCount startIndex
+    let newRoot ← insertLeaves leaves
     settleWithdrawalTransfer txn.withdrawal.token recipient txn.withdrawal.amount
-    let realNullifierCount ← countNonZero txn.nullifierHashes
-      0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+    let realNullifierHashes ← realNullifiers txn.nullifierHashes
     if emergency then
       emit "EmergencyWithdrawn"
         [addressToWord recipient,
          txn.withdrawal.npk,
          addressToWord txn.withdrawal.token,
          txn.withdrawal.amount,
-         newRoot, startIndex, ciphertextCount,
-         realNullifierCount,
+         newRoot, startIndex, arrayLength leaves,
+         arrayLength realNullifierHashes,
          arrayLength txn.ciphertexts]
     else
       emit "Withdrawn"
         [addressToWord recipient,
          txn.withdrawal.npk,
          addressToWord txn.withdrawal.token,
          txn.withdrawal.amount,
-         newRoot, startIndex, ciphertextCount,
-         realNullifierCount,
+         newRoot, startIndex, arrayLength leaves,
+         arrayLength realNullifierHashes,
          arrayLength txn.ciphertexts]
 
   /- `function withdraw(WithdrawalTransaction[] calldata _transactions)

cases/unlink_xyz/pool/case.yaml

@@ -32,7 +32,7 @@ selected_functions:
   - acceptOwnership
   - renounceOwnership
 source_language: solidity
-verity_version: 5781a22489c721670f33bc1a74563cacd7d9232b
+verity_version: cd1f92dda5bbf3aed775a744cba1e3da883c739e
 lean_toolchain: leanprover/lean4:v4.22.0
 abstraction_level: protocol_slice
 abstraction_tags:
@@ -64,16 +64,15 @@ abstraction_notes: >
   `emergencyWithdraw`) now build against `Array Transaction` /
   `Array WithdrawalTransaction` parameters using dynamic struct-array
   member projections and projected dynamic-array forwarding to linked
-  externals / internal helpers. Remaining promotion blockers are fidelity
-  gaps rather than basic body expressibility: memory-array-return helper
-  shapes for `_realCommitments` / `_realNullifiers`, source-faithful
-  memory-array values flowing into `_insertLeaves`, and event payloads
-  carrying dynamic arrays. Event ABI metadata is now declared in the
-  macro-generated `CompilationModel.events` table, but the executable
-  `emit` sites still use surrogate scalar counts until first-class dynamic
-  array payload emission lands. `_executeWithdrawal(_transactions[i], bool)` is
-  now routed through an internal helper call; the insertion mutation is also
-  factored into a helper while memory-array construction remains pending.
+  externals / internal helpers. The transfer/withdraw paths now use
+  `_realCommitments` / `_realNullifiers`-shaped memory-array helpers and pass
+  the resulting memory array into an `_insertLeaves`-shaped helper. Remaining
+  promotion blockers are fidelity gaps rather than basic body expressibility:
+  event payloads still use surrogate scalar counts until first-class dynamic
+  array payload emission lands, and the `_insertLeaves` body still uses this
+  scoped model's lightweight LazyIMT accumulator boundary.
+  `_executeWithdrawal(_transactions[i], bool)` is routed through an internal
+  helper call.
 
   Source confirmation (pinned commit 4bc46c1f): there is NO
   `UnlinkAdapter`, no `adapterDeposit`, no `adapterWithdraw` —
@@ -105,9 +104,8 @@ abstraction_notes: >
       into internal helpers that accept `Array Note` / `Array Uint256`
       parameters until that ships.
 unsupported_feature_codes:
-  - memory_array_return_helpers
-  - source_faithful_insert_leaves
   - dynamic_array_event_payloads
+  - lazy_imt_insert_body_assumed
   - uups_proxy_storage_rotation_not_modeled
   - bn254_precompile_probes_via_ecm_assumed
   - poseidon_assumed_axiom

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5781a22489c721670f33bc1a74563cacd7d9232b",
+   "rev": "cd1f92dda5bbf3aed775a744cba1e3da883c739e",
    "name": "verity",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "5781a22489c721670f33bc1a74563cacd7d9232b",
+   "inputRev": "cd1f92dda5bbf3aed775a744cba1e3da883c739e",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/lfglabs-dev/EVMYulLean.git",

lakefile.lean

@@ -5,7 +5,7 @@ package «verity-benchmark» where
   version := v!"0.1.0"
 
 require verity from git
-  "https://github.com/lfglabs-dev/verity.git"@"5781a22489c721670f33bc1a74563cacd7d9232b"
+  "https://github.com/lfglabs-dev/verity.git"@"cd1f92dda5bbf3aed775a744cba1e3da883c739e"
 
 @[default_target]
 lean_lib «Benchmark» where