From 7859c8d0a73a983e7eadd4921dc103e0bbfdc181 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Fri, 15 May 2026 00:30:03 +0200
Subject: [PATCH] Model UnlinkPool hashNote via PoseidonT4 boundary

---
 Benchmark/Cases/UnlinkXyz/Pool/Contract.lean        |  8 ++------
 .../Generated/UnlinkXyz/Pool/Tasks/BuildGreen.lean  |  2 +-
 cases/unlink_xyz/pool/tasks/build_green.yaml        | 13 ++++++++-----
 3 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
index 6ab16d6..f07dcf7 100644
--- a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
+++ b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
@@ -379,6 +379,7 @@ verity_contract UnlinkPool where
       Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256,
       Uint256, Uint256, Uint256, Array Uint256, Array Uint256) -> (Bool)
     external poseidonT3(Uint256, Uint256) -> (Uint256)
+    external poseidonT4(Uint256, Uint256, Uint256) -> (Uint256)
     external permitWitnessTransferFrom(
       Address, Address, Uint256, Uint256, Uint256, Address, Uint256, Address,
       Uint256, Bytes) -> (Bool)
@@ -494,14 +495,9 @@ verity_contract UnlinkPool where
 
   /- `function hashNote(Note calldata _note) public pure returns (uint256)`
       (UnlinkPool.sol:212-215). Pure Poseidon-T4 boundary call. -/
-  -- BLOCKED(verity#1003): qualified Lean helper calls (`PoseidonT4.hash`)
-  -- are not yet supported inside `verity_contract` function bodies. The
-  -- pure spec lives in `Specs.lean` (assumed boundary). Once verity#1003
-  -- lifts, replace with `let h ← PoseidonT4.hash (npk, ...)` (the same
-  -- shape the scratchpad uses).
   function view hashNote (npk : Uint256, _token : Address, amount : Uint256)
       : Uint256 := do
-    return (add npk amount)
+    return externalCall "poseidonT4" [npk, addressToWord _token, amount]
 
   function poseidon2 (lhs : Uint256, rhs : Uint256) : Uint256 := do
     return externalCall "poseidonT3" [lhs, rhs]
diff --git a/Benchmark/Generated/UnlinkXyz/Pool/Tasks/BuildGreen.lean b/Benchmark/Generated/UnlinkXyz/Pool/Tasks/BuildGreen.lean
index 65cffc9..3a23702 100644
--- a/Benchmark/Generated/UnlinkXyz/Pool/Tasks/BuildGreen.lean
+++ b/Benchmark/Generated/UnlinkXyz/Pool/Tasks/BuildGreen.lean
@@ -2,7 +2,7 @@
   Editable task template for `unlink_xyz/pool/build_green`.
 
   The case is currently `stage: scoped` with `translation_status:
-  in_progress`. The promotion path to `build_green` is documented in
+  scoped`. The promotion path to `build_green` is documented in
   `cases/unlink_xyz/pool/review/spec-review.md`. The reference solution
   lives in `Benchmark.Cases.UnlinkXyz.Pool.Proofs`.
 -/
diff --git a/cases/unlink_xyz/pool/tasks/build_green.yaml b/cases/unlink_xyz/pool/tasks/build_green.yaml
index 14d82cb..9fd8d67 100644
--- a/cases/unlink_xyz/pool/tasks/build_green.yaml
+++ b/cases/unlink_xyz/pool/tasks/build_green.yaml
@@ -30,9 +30,12 @@ abstraction_level: protocol_slice
 abstraction_notes: >
   First buildable target for the case: the `verity_contract UnlinkPool`
   declaration in `Contract.lean` must elaborate cleanly through `lake build`
-  on the lakefile-pinned Verity revision. The three nested-dynamic-struct-
-  array entry points (`transfer`, `withdraw`, `adapterWithdraw`) are stubbed
-  with `BLOCKED(#1760-nested-dynamic):` markers until the Verity macro
-  surface gains struct-parameter projection from an ABI-dynamic root.
+  on the lakefile-pinned Verity revision. The pool entry points now elaborate
+  with source-shaped dynamic-array projections, LazyIMT insertion, and
+  PoseidonT3/T4 routed through explicit linked-external cryptographic
+  boundaries. Remaining blockers are tracked in the case manifest.
 unsupported_feature_codes:
-  - nested_dynamic_struct_array_param
+  - uups_proxy_storage_rotation_not_modeled
+  - poseidon_assumed_axiom
+  - permit2_assumed_axiom
+  - groth16_verifier_assumed_axiom