Wire UnlinkPool LazyIMT insertion body

[Th0rgal]

Summary

• replace the scoped accumulator in UnlinkPool insertLeaves with source-shaped LazyIMT append and depth-32 root recomputation
• add flattened LazyIMT constants/default-zero/index helpers and route Poseidon T3 through the explicit assumed boundary
• remove LazyIMT-specific unsupported feature codes from the case manifest

Verification

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

---

Note

Medium Risk
Medium risk because it replaces the previous simplified accumulator with a full LazyIMT append/root algorithm and adds a new Poseidon external boundary call, affecting Merkle root/state updates used by core ZK flows.

Overview
Implements the previously-assumed _insertLeaves body in Benchmark/Cases/UnlinkXyz/Pool/Contract.lean by adding flattened LazyIMT helpers (lazyInsert, lazyRootWithDepth32, default-zero tower Z_0..Z_32) and switching insertLeaves to append each leaf and recompute the depth-32 root.

Adds a linked external poseidonT3 plus a poseidon2 wrapper, centralizes note validation constants (SNARK_SCALAR_FIELD, MAX_NOTE_VALUE), and updates cases/unlink_xyz/pool/case.yaml to remove LazyIMT-specific abstraction tags/unsupported feature codes now that insertion is modeled.

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

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit f4dd922. Configure here.}

[cursor]

Z_7 constant is truncated, missing 12 digits

High Severity

The Z_7 constant has only 64 digits but the correct value has 76 digits. The value in InternalLazyIMT.lean (line 66) is 3396914609616007258851405644437304192397291162432396347162513310381425243293, but Contract.lean has 3396914609616007258851405644437304192396347162513310381425243293 — 12 digits (729116243239) were dropped from the middle during transcription. This causes incorrect Merkle root computations whenever the tree path traverses level 7 with a left-child (even index), producing a wrong poseidon2(current, Z_7) parent hash.

 

^{Reviewed by Cursor Bugbot for commit f4dd922. Configure here.}