Use Unlink memory array helpers

[Th0rgal]

Summary

• bump Verity to cd1f92dda5bbf3aed775a744cba1e3da883c739e
• replace fused Unlink insertion helper with _realCommitments / _realNullifiers-shaped memory-array helpers
• pass memory-backed leaves into an _insertLeaves-shaped helper
• update case metadata to remove the memory-array helper blockers and keep the remaining event/LazyIMT assumptions explicit

Verification

• git diff --check
• lake build Benchmark.Cases.UnlinkXyz.Pool.Compile

---

Note

Medium Risk
Updates the Unlink pool model’s leaf/nullifier handling and Merkle-root update path, which could affect state transitions and emitted event metadata. Also bumps the verity dependency, so behavior may change due to upstream compiler/runtime updates.

Overview
The Unlink pool Verity model now materializes Solidity-shaped memory arrays via new realCommitments and realNullifiers helpers, replacing the prior fused filtering+insertion helper.

transfer and executeWithdrawal/withdraw are updated to pass the resulting leaves into a new insertLeaves helper (and to derive event scalar fields from these filtered arrays), while keeping LazyIMT insertion as the same lightweight accumulator boundary.

The case metadata is updated to reflect the new assumptions/blockers, and the repo bumps the verity dependency pin (including lakefile.lean/lake-manifest.json).

^{Reviewed by Cursor Bugbot for commit f036bc3. Bugbot is set up for automated code reviews on this repo. Configure here.}