Add UnlinkPool event metadata

Benchmark/Cases/UnlinkXyz/Pool/Contract.lean

@@ -196,6 +196,21 @@ verity_contract UnlinkPool where
     error PoolWithdrawalSlotZero ()
     error CallerNotPendingOwner ()
 
+  event_defs
+    event Deposited(@indexed depositor : Address, newRoot : Uint256, startIndex : Uint256,
+      notes : Array Note, ciphertexts : Array Ciphertext)
+    event Transferred(@indexed newRoot : Uint256, startIndex : Uint256,
+      commitments : Array Uint256, nullifierHashes : Array Uint256, ciphertexts : Array Ciphertext)
+    event Withdrawn(@indexed «to» : Address, note : Note, @indexed newRoot : Uint256,
+      startIndex : Uint256, commitments : Array Uint256, nullifierHashes : Array Uint256,
+      ciphertexts : Array Ciphertext)
+    event EmergencyWithdrawn(@indexed «to» : Address, note : Note, @indexed newRoot : Uint256,
+      startIndex : Uint256, commitments : Array Uint256, nullifierHashes : Array Uint256,
+      ciphertexts : Array Ciphertext)
+    event RelayerAdded(@indexed relayer : Address)
+    event RelayerRemoved(@indexed relayer : Address)
+    event VerifierRouterUpdated(@indexed previousRouter : Address, @indexed newRouter : Address)
+
   -- ERC-7201 namespace base slot for the relayer set:
   -- `keccak256("unlink.storage.UnlinkPoolRelayers")`. Derived at
   -- elaboration time through `keccak256_lit` (verity#1827) so the

cases/unlink_xyz/pool/case.yaml

@@ -32,7 +32,7 @@ selected_functions:
   - acceptOwnership
   - renounceOwnership
 source_language: solidity
-verity_version: f917a7c9e2becafbcbabe7df8c8ba7a697a35afc
+verity_version: bd211c574f45cda31d66feab1bbc7e9d08dc5486
 lean_toolchain: leanprover/lean4:v4.22.0
 abstraction_level: protocol_slice
 abstraction_tags:
@@ -47,6 +47,7 @@ abstraction_tags:
   - initializer_modeled
   - nonreentrant_modeled
   - keccak256_literal_typehash
+  - macro_event_declarations
 abstraction_notes: >
   Verity model of `UnlinkPool` (Unlink privacy pool implementation). Protocol-
   specific cryptographic primitives (Poseidon, Permit2, Lazy-IMT, Groth16
@@ -67,7 +68,10 @@ abstraction_notes: >
   gaps rather than basic body expressibility: memory-array-return helper
   shapes for `_realCommitments` / `_realNullifiers`, source-faithful
   memory-array values flowing into `_insertLeaves`, and event payloads
-  carrying dynamic arrays. `_executeWithdrawal(_transactions[i], bool)` is
+  carrying dynamic arrays. Event ABI metadata is now declared in the
+  macro-generated `CompilationModel.events` table, but the executable
+  `emit` sites still use surrogate scalar counts until first-class dynamic
+  array payload emission lands. `_executeWithdrawal(_transactions[i], bool)` is
   now routed through an internal helper call; the insertion mutation is also
   factored into a helper while memory-array construction remains pending.
 

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f917a7c9e2becafbcbabe7df8c8ba7a697a35afc",
+   "rev": "bd211c574f45cda31d66feab1bbc7e9d08dc5486",
    "name": "verity",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f917a7c9e2becafbcbabe7df8c8ba7a697a35afc",
+   "inputRev": "bd211c574f45cda31d66feab1bbc7e9d08dc5486",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/lfglabs-dev/EVMYulLean.git",

lakefile.lean

@@ -5,7 +5,7 @@ package «verity-benchmark» where
   version := v!"0.1.0"
 
 require verity from git
-  "https://github.com/lfglabs-dev/verity.git"@"f917a7c9e2becafbcbabe7df8c8ba7a697a35afc"
+  "https://github.com/lfglabs-dev/verity.git"@"bd211c574f45cda31d66feab1bbc7e9d08dc5486"
 
 @[default_target]
 lean_lib «Benchmark» where