Use generic Verity ergonomics in UnlinkPool

[Th0rgal]

Summary

• update UnlinkPool to use typed Circuit external-call returns
• replace proof abiHeadWord slices with abiEncode txn.proof
• use inline realNullifiers ... in event arguments
• replace inlined relayer checks with generic with onlyRelayer modifier syntax
• pin benchmark to the Verity feature commit from Add generic Solidity ergonomics to Verity macro verity#1883

Validation

• lake build Benchmark.Cases.UnlinkXyz.Pool.Compile
• lake build

---

Note

Medium Risk
Touches core deposit/transfer/withdraw flows and proof/circuit external-call wiring; behavior should be equivalent but mismatched ABI encoding or circuit shape handling could break verification at runtime.

Overview
Modernizes the UnlinkPool Verity model to use a typed Circuit struct for getCircuit results (plus *_try variants), and updates transfer/executeWithdrawal to validate input/output shapes and circuit status via circuit.* fields.

Refactors ZK proof verification calls to pass abiEncode txn.proof instead of manual abiHeadWord slicing, and simplifies event emission by inlining realNullifiers computation.

Replaces per-call-site relayer checks with a shared modifier onlyRelayer and applies it via with onlyRelayer on relayer-gated entrypoints. Updates the pinned verity dependency revision in lakefile.lean/lake-manifest.json.

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