Check UnlinkPool event metadata

[Th0rgal]

Summary

• add a native-decide check that UnlinkPool.spec.events matches the source interface event metadata
• cover dynamic array event params for notes, commitments, nullifiers, and ciphertexts
• lock indexed address/root metadata for relayer, transfer, withdraw, and router events

Checks

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

---

Note

Low Risk
Low risk: adds a native_decide-based compile-time check over event ABI metadata without changing contract/spec behavior. The main risk is test brittleness if event signatures/param ordering changes upstream.

Overview
Adds a Lean-level metadata check in Benchmark/Cases/UnlinkXyz/Pool/Compile.lean that validates UnlinkPool.spec.events contains the expected event definitions (names, param types—including tuple/array shapes—and indexed vs unindexed kinds) for deposit/transfer/withdraw/relayer/router events.

Introduces small helper definitions for common ABI ParamTypes and equality predicates, and enforces the check via example : ... = true := by native_decide.

^{Reviewed by Cursor Bugbot for commit 9c7a39b. 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 9c7a39b. Configure here.}

[cursor]

Missing event count check allows undetected extra events

Medium Severity

unlinkPoolEventMetadataMatchesSource uses hasEvent (which calls .any) to verify each expected event exists in UnlinkPool.spec.events, but never checks that the total number of events in the spec equals 7. This makes it a subset check, not an equality check. If a spurious or duplicate event were added to the spec, this "lock" would still pass silently, contradicting the PR's stated goal of verifying that spec.events matches the source interface metadata.

Additional Locations (1)

• Benchmark/Cases/UnlinkXyz/Pool/Compile.lean#L34-L36

 

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