From e4ce8cdbec8e3fcc9913ba13ae0c61296f773ed6 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Thu, 14 May 2026 15:02:11 +0200
Subject: [PATCH] Use real nullifier count in Unlink event model

---
 Benchmark/Cases/UnlinkXyz/Pool/Contract.lean | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
index 81a4d53..fac0c76 100644
--- a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
+++ b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
@@ -493,9 +493,11 @@ verity_contract UnlinkPool where
         0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
         ciphertextCount
         startIndex
+      let realNullifierCount ← countNonZero txn.nullifierHashes
+        0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
       emit "Transferred"
         [newRoot, startIndex, ciphertextCount,
-         arrayLength txn.nullifierHashes,
+         realNullifierCount,
          arrayLength txn.ciphertexts])
 
   /- `_executeWithdrawal(WithdrawalTransaction calldata _txn, bool _emergency)`
@@ -554,6 +556,8 @@ verity_contract UnlinkPool where
     let startIndex ← nextLeafIndex
     let newRoot ← insertFilteredLeaves txn.newCommitments wSlot ciphertextCount startIndex
     settleWithdrawalTransfer txn.withdrawal.token recipient txn.withdrawal.amount
+    let realNullifierCount ← countNonZero txn.nullifierHashes
+      0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
     if emergency then
       emit "EmergencyWithdrawn"
         [addressToWord recipient,
@@ -561,7 +565,7 @@ verity_contract UnlinkPool where
          addressToWord txn.withdrawal.token,
          txn.withdrawal.amount,
          newRoot, startIndex, ciphertextCount,
-         arrayLength txn.nullifierHashes,
+         realNullifierCount,
          arrayLength txn.ciphertexts]
     else
       emit "Withdrawn"
@@ -570,7 +574,7 @@ verity_contract UnlinkPool where
          addressToWord txn.withdrawal.token,
          txn.withdrawal.amount,
          newRoot, startIndex, ciphertextCount,
-         arrayLength txn.nullifierHashes,
+         realNullifierCount,
          arrayLength txn.ciphertexts]
 
   /- `function withdraw(WithdrawalTransaction[] calldata _transactions)