Skip to content

Check UnlinkPool event metadata #55

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Th0rgal merged 1 commit into from
May 14, 2026
Merged

Check UnlinkPool event metadata #55

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 74 additions & 0 deletions Benchmark/Cases/UnlinkXyz/Pool/Compile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,80 @@ import Benchmark.Cases.UnlinkXyz.Pool.Proofs

namespace Benchmark.Cases.UnlinkXyz.Pool

open Compiler.CompilationModel

private def uintArray : ParamType :=
ParamType.array ParamType.uint256

private def noteParam : ParamType :=
ParamType.tuple [ParamType.uint256, ParamType.address, ParamType.uint256]

private def ciphertextParam : ParamType :=
ParamType.tuple [
ParamType.uint256,
ParamType.fixedArray ParamType.uint256 3
]

private def ciphertextArray : ParamType :=
ParamType.array ciphertextParam

private def eventParamEq (a b : EventParam) : Bool :=
a.name == b.name && a.ty == b.ty && a.kind == b.kind

private def eventDefEq (name : String) (params : List EventParam) (eventDef : EventDef) : Bool :=
eventDef.name == name &&
eventDef.params.length == params.length &&
(eventDef.params.zip params).all (fun (actual, expected) => eventParamEq actual expected)

private def hasEvent (name : String) (params : List EventParam) : Bool :=
UnlinkPool.spec.events.any (eventDefEq name params)

def unlinkPoolEventMetadataMatchesSource : Bool :=
hasEvent "Deposited" [
{ name := "depositor", ty := ParamType.address, kind := EventParamKind.indexed },
{ name := "newRoot", ty := ParamType.uint256, kind := EventParamKind.unindexed },
{ name := "startIndex", ty := ParamType.uint256, kind := EventParamKind.unindexed },
{ name := "notes", ty := ParamType.array noteParam, kind := EventParamKind.unindexed },
{ name := "ciphertexts", ty := ciphertextArray, kind := EventParamKind.unindexed }
] &&
hasEvent "Transferred" [
{ name := "newRoot", ty := ParamType.uint256, kind := EventParamKind.indexed },
{ name := "startIndex", ty := ParamType.uint256, kind := EventParamKind.unindexed },
{ name := "commitments", ty := uintArray, kind := EventParamKind.unindexed },
{ name := "nullifierHashes", ty := uintArray, kind := EventParamKind.unindexed },
{ name := "ciphertexts", ty := ciphertextArray, kind := EventParamKind.unindexed }
] &&
hasEvent "Withdrawn" [
{ name := "to", ty := ParamType.address, kind := EventParamKind.indexed },
{ name := "note", ty := noteParam, kind := EventParamKind.unindexed },
{ name := "newRoot", ty := ParamType.uint256, kind := EventParamKind.indexed },
{ name := "startIndex", ty := ParamType.uint256, kind := EventParamKind.unindexed },
{ name := "commitments", ty := uintArray, kind := EventParamKind.unindexed },
{ name := "nullifierHashes", ty := uintArray, kind := EventParamKind.unindexed },
{ name := "ciphertexts", ty := ciphertextArray, kind := EventParamKind.unindexed }
] &&
hasEvent "EmergencyWithdrawn" [
{ name := "to", ty := ParamType.address, kind := EventParamKind.indexed },
{ name := "note", ty := noteParam, kind := EventParamKind.unindexed },
{ name := "newRoot", ty := ParamType.uint256, kind := EventParamKind.indexed },
{ name := "startIndex", ty := ParamType.uint256, kind := EventParamKind.unindexed },
{ name := "commitments", ty := uintArray, kind := EventParamKind.unindexed },
{ name := "nullifierHashes", ty := uintArray, kind := EventParamKind.unindexed },
{ name := "ciphertexts", ty := ciphertextArray, kind := EventParamKind.unindexed }
] &&
hasEvent "RelayerAdded" [
{ name := "relayer", ty := ParamType.address, kind := EventParamKind.indexed }
] &&
hasEvent "RelayerRemoved" [
{ name := "relayer", ty := ParamType.address, kind := EventParamKind.indexed }
] &&
hasEvent "VerifierRouterUpdated" [
{ name := "previousRouter", ty := ParamType.address, kind := EventParamKind.indexed },
{ name := "newRouter", ty := ParamType.address, kind := EventParamKind.indexed }
]
Copy link
Copy Markdown

@cursor cursor Bot May 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)
Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit 9c7a39b. Configure here.


example : unlinkPoolEventMetadataMatchesSource = true := by native_decide

def caseReady : Bool := true

end Benchmark.Cases.UnlinkXyz.Pool
Loading