From f0d5e1b4718386c4db41f59582e94d3a1e229b01 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Thu, 14 May 2026 14:45:46 +0200
Subject: [PATCH] Factor Unlink filtered leaf insertion

---
 Benchmark/Cases/UnlinkXyz/Pool/Contract.lean | 52 +++++++++++---------
 cases/unlink_xyz/pool/case.yaml              |  6 ++-
 2 files changed, 34 insertions(+), 24 deletions(-)

diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
index 8a61fd5..81a4d53 100644
--- a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
+++ b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
@@ -43,8 +43,9 @@
   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`, `_insertLeaves`, and
-  dynamic array event payloads.
+  helpers for `_realCommitments` / `_realNullifiers`, the source-level
+  memory-array value passed into `_insertLeaves`, and dynamic array event
+  payloads.
 -/
 import Contracts.Common
 import Compiler.Modules.Hashing
@@ -386,6 +387,28 @@ 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
+        else
+          pure ()
+      else
+        pure ())
+    setStorage stateMerkleRoot newRoot
+    setMappingWord stateRootSeen newRoot 0 1
+    setStorage lazyNumberOfLeaves (add startIndex leafCount)
+    return newRoot
+
   function view computeContextHash (ciphertexts : Array Ciphertext) : Uint256 := do
     let cid ← Verity.chainid
     let selfAddr ← Verity.contractAddress
@@ -466,16 +489,10 @@ verity_contract UnlinkPool where
       requireError ok PoolProofVerificationFailed()
       spendNullifiers txn.nullifierHashes
       let startIndex ← nextLeafIndex
-      let mut newRoot := startIndex
-      forEach "m" (arrayLength txn.newCommitments) (do
-        let leaf := arrayElement txn.newCommitments m
-        if leaf != 0 then
-          newRoot := add newRoot leaf
-        else
-          pure ())
-      setStorage stateMerkleRoot newRoot
-      setMappingWord stateRootSeen newRoot 0 1
-      setStorage lazyNumberOfLeaves (add startIndex ciphertextCount)
+      let newRoot ← insertFilteredLeaves txn.newCommitments
+        0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+        ciphertextCount
+        startIndex
       emit "Transferred"
         [newRoot, startIndex, ciphertextCount,
          arrayLength txn.nullifierHashes,
@@ -535,16 +552,7 @@ verity_contract UnlinkPool where
     requireError ok PoolProofVerificationFailed()
     spendNullifiers txn.nullifierHashes
     let startIndex ← nextLeafIndex
-    let mut newRoot := startIndex
-    forEach "m" wSlot (do
-      let leaf := arrayElement txn.newCommitments m
-      if leaf != 0 then
-        newRoot := add newRoot leaf
-      else
-        pure ())
-    setStorage stateMerkleRoot newRoot
-    setMappingWord stateRootSeen newRoot 0 1
-    setStorage lazyNumberOfLeaves (add startIndex ciphertextCount)
+    let newRoot ← insertFilteredLeaves txn.newCommitments wSlot ciphertextCount startIndex
     settleWithdrawalTransfer txn.withdrawal.token recipient txn.withdrawal.amount
     if emergency then
       emit "EmergencyWithdrawn"
diff --git a/cases/unlink_xyz/pool/case.yaml b/cases/unlink_xyz/pool/case.yaml
index 6c746dc..97f13a1 100644
--- a/cases/unlink_xyz/pool/case.yaml
+++ b/cases/unlink_xyz/pool/case.yaml
@@ -66,8 +66,10 @@ abstraction_notes: >
   externals / internal helpers. Remaining promotion blockers are fidelity
   gaps rather than basic body expressibility: memory-array-return helper
   shapes for `_realCommitments` / `_realNullifiers`, source-faithful
-  `_insertLeaves`, first-class `_executeWithdrawal(_transactions[i], bool)`
-  helper arguments, and event payloads carrying dynamic arrays.
+  memory-array values flowing into `_insertLeaves`, and event payloads
+  carrying dynamic arrays. `_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.
 
   Source confirmation (pinned commit 4bc46c1f): there is NO
   `UnlinkAdapter`, no `adapterDeposit`, no `adapterWithdraw` —