From 0a6b31636c29155ff639617fe956eb189249b6ea Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Thu, 14 May 2026 21:17:36 +0200
Subject: [PATCH] Pin Unlink case to dynamic event source support

---
 cases/unlink_xyz/pool/case.yaml | 5 +++--
 lake-manifest.json              | 4 ++--
 lakefile.lean                   | 2 +-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/cases/unlink_xyz/pool/case.yaml b/cases/unlink_xyz/pool/case.yaml
index 1442dc0..502e306 100644
--- a/cases/unlink_xyz/pool/case.yaml
+++ b/cases/unlink_xyz/pool/case.yaml
@@ -32,7 +32,7 @@ selected_functions:
   - acceptOwnership
   - renounceOwnership
 source_language: solidity
-verity_version: cd1f92dda5bbf3aed775a744cba1e3da883c739e
+verity_version: 3b7e69bf819356c64c567f84dd686739befab334
 lean_toolchain: leanprover/lean4:v4.22.0
 abstraction_level: protocol_slice
 abstraction_tags:
@@ -58,7 +58,8 @@ abstraction_notes: >
   and tracked under verity#1420). The model uses every Solidity-feature-parity
   primitive that landed in verity through PRs #1782 (selfbalance), #1795
   (Unlink-audit helpers), #1810 (callWithValue ECM), and #1827 (BN254
-  precompile ECMs + `keccak256_lit` literal sugar).
+  precompile ECMs + `keccak256_lit` literal sugar), plus #1870
+  (memory-array helper lowering) and #1871 (dynamic-array event sources).
 
   The three public ZK entry points (`transfer`, `withdraw`, and
   `emergencyWithdraw`) now build against `Array Transaction` /
diff --git a/lake-manifest.json b/lake-manifest.json
index 49b9cf1..d1e47b0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cd1f92dda5bbf3aed775a744cba1e3da883c739e",
+   "rev": "3b7e69bf819356c64c567f84dd686739befab334",
    "name": "verity",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "cd1f92dda5bbf3aed775a744cba1e3da883c739e",
+   "inputRev": "3b7e69bf819356c64c567f84dd686739befab334",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/lfglabs-dev/EVMYulLean.git",
diff --git a/lakefile.lean b/lakefile.lean
index bdb3abd..94245dd 100644
--- a/lakefile.lean
+++ b/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"@"cd1f92dda5bbf3aed775a744cba1e3da883c739e"
+  "https://github.com/lfglabs-dev/verity.git"@"3b7e69bf819356c64c567f84dd686739befab334"
 
 @[default_target]
 lean_lib «Benchmark» where