Remove UnlinkPool Lean axioms from specs

Benchmark/Cases/UnlinkXyz/Pool/InternalLazyIMT.lean

@@ -15,8 +15,7 @@
 
   This module is pure Lean (not a `verity_contract` declaration); it is
   the trusted-base spec that the pool's `_insertLeaves` /
-  `_validateContext` / `_verifyProof` paths consume. Stored separately
-  so the pool's trust manifest can list the LazyIMT axioms in one place.
+  `_validateContext` / `_verifyProof` paths consume.
 -/
 import Contracts.Common
 import Benchmark.Cases.UnlinkXyz.Pool.Specs

Benchmark/Cases/UnlinkXyz/Pool/Proofs.lean

@@ -2,11 +2,9 @@
   Reference proof file for the `unlink_xyz/pool` case.
 
   Placeholder — promotion to `build_green` only requires the `Contract.lean`
-  declaration to elaborate. Once the three blocked entry points land (see
-  the `BLOCKED(verity#1832):` markers in Contract.lean), the
-  first proof target will be the per-token conservation invariant across
-  `deposit + adapterDeposit` under the assumed Poseidon / Permit2 /
-  Lazy-IMT / Groth16 boundaries declared in `Specs.lean`.
+  declaration to elaborate. The first proof target will likely be the
+  per-token conservation invariant across `deposit + withdraw` under the
+  remaining Poseidon / Permit2 / Groth16 boundaries declared in `Specs.lean`.
 -/
 import Benchmark.Cases.UnlinkXyz.Pool.Contract
 

Benchmark/Cases/UnlinkXyz/Pool/Specs.lean

@@ -1,5 +1,5 @@
 /-
-  Verity model of `UnlinkPool` — assumed boundaries and pure structural specs.
+  Verity model of `UnlinkPool` — opaque boundaries and pure structural specs.
 
   Upstream: unlink-xyz/monorepo@4bc46c1fffbc0e146dccfff5b9fe00167121b27b
   Solidity files:
@@ -11,9 +11,8 @@
   Protocol-specific cryptographic primitives belong in the `unlink-verity`
   package per the package-split policy documented in
   `lfglabs-dev/verity:docs/ROADMAP.md` "Unlink Audit Readiness". This file
-  declares them locally as `opaque` / `axiom` boundaries with the
-  `unlink_verity_*` axiom naming convention so a future trust manifest can
-  list them in one place.
+  declares them locally as opaque boundaries so a future trust manifest can
+  list them in one place without adding Lean axioms to the benchmark target.
 
   BN254 precompile probes are NO LONGER declared here: `_checkBn254Precompile`
   is wired directly to `Compiler.Modules.Precompiles.bn256Add` /
@@ -116,21 +115,14 @@ structure AdapterTransaction where
 /-! ### Assumed boundary: Poseidon T3 / T4 (vendored poseidon-solidity@v0.0.5)
 
 `PoseidonT3.hash(uint[2])` and `PoseidonT4.hash(uint[3])` are the BN254
-scalar-field hashes used inside the ZK circuit. Modeled opaquely; result
-lives in the scalar field. -/
+scalar-field hashes used inside the ZK circuit. Modeled opaquely here. -/
 
 namespace PoseidonT3
   opaque hash : (Uint256 × Uint256) → Uint256
-  /-- Axiom name: `unlink_verity_poseidon_t3_in_field`. -/
-  axiom hash_in_field (xy : Uint256 × Uint256) :
-    (hash xy : Nat) < (PoolConstants.SNARK_SCALAR_FIELD : Nat)
 end PoseidonT3
 
 namespace PoseidonT4
   opaque hash : (Uint256 × Uint256 × Uint256) → Uint256
-  /-- Axiom name: `unlink_verity_poseidon_t4_in_field`. -/
-  axiom hash_in_field (xyz : Uint256 × Uint256 × Uint256) :
-    (hash xyz : Nat) < (PoolConstants.SNARK_SCALAR_FIELD : Nat)
 end PoseidonT4
 
 /-! ### Assumed boundary: Permit2.permitWitnessTransferFrom
@@ -140,7 +132,6 @@ witness checks happen inside Permit2; the pool observes only the post-call
 balance delta (`_transferWithBalanceCheck`). -/
 
 namespace Permit2Spec
-  /-- Axiom name: `unlink_verity_permit2_permit_witness_transfer_from`. -/
   opaque permitWitnessTransferFromEffect
     (permit2 : Address) (token : Address) (depositor : Address)
     (totalAmount : Uint256) (witness : Uint256) : Uint256
@@ -153,7 +144,6 @@ an opaque step function so callers can write the leaf and re-read the
 root through the pool's storage fields. -/
 
 namespace LazyImtSpec
-  /-- Axiom name: `unlink_verity_lazy_imt_root_after_inserts`. -/
   opaque rootAfterInserts (prevRoot prevNumberOfLeaves : Uint256)
     (leaves : Array Uint256) : Uint256
 end LazyImtSpec
@@ -169,7 +159,6 @@ the contract layer `getCircuit` is exposed as a single tuple-returning
 itself runs through Verity's external-call machinery. -/
 
 namespace VerifierRouterSpec
-  /-- Axiom name: `unlink_verity_groth16_verify_proof`. -/
   opaque verifyProof
     (verifier : Address)
     (pA : Uint256 × Uint256)

cases/unlink_xyz/pool/case.yaml

@@ -50,8 +50,8 @@ abstraction_tags:
 abstraction_notes: >
   Verity model of `UnlinkPool` (Unlink privacy pool implementation). Protocol-
   specific cryptographic primitives (Poseidon, Permit2, Lazy-IMT, Groth16
-  verifier router) are routed through assumed-status external boundaries with
-  named axioms, per the `unlink-verity` package split documented in
+  verifier router) are routed through explicit external or opaque boundaries,
+  per the `unlink-verity` package split documented in
   `docs/ROADMAP.md` "Unlink Audit Readiness". UUPS proxy semantics are modeled
   as the implementation contract itself (proxy storage rotation is host-level
   and tracked under verity#1420). The model uses every Solidity-feature-parity
@@ -72,7 +72,7 @@ abstraction_notes: >
   `_insertLeaves`-shaped helper, and emit source-shaped dynamic array and
   withdrawal-note payloads. The deposit path validates static `Note[]`
   elements, computes the source-shaped deposit witness hash, routes the Permit2
-  transfer through the assumed external boundary, inserts leaves, and emits the
+  transfer through the linked external boundary, inserts leaves, and emits the
   source-shaped `Deposited` payload. Remaining promotion blockers are fidelity
   gaps rather than basic body expressibility: Poseidon, Permit2, Groth16, and
   host-level UUPS proxy behavior remain as explicit boundaries.

cases/unlink_xyz/pool/review/spec-review.md

@@ -4,10 +4,10 @@ The Verity model of `UnlinkPool` exposes four classes of declarations.
 
 ## 1. Pure Lean specs
 
-- `Specs.lean` — assumed protocol boundaries (Poseidon T3 / T4, Permit2
+- `Specs.lean` — opaque protocol boundaries (Poseidon T3 / T4, Permit2
   `permitWitnessTransferFrom`, Lazy-IMT root, Groth16 `verifyProof`,
-  three ABI composite hashes) declared via `opaque` + `axiom` with the
-  `unlink_verity_*` axiom-naming convention.
+  three ABI composite hashes). These are trust-boundary declarations, not
+  Lean `axiom` declarations.
 - `InternalLazyIMT.lean` — full LazyIMT spec (Z_0..Z_32 default-zero
   tower, `_init` / `_insert` / `_update` / `_root` / `_rootWithDepth` /
   `_levels` / `_merkleProofElements`). Pure Lean spec consumed by the
@@ -35,22 +35,14 @@ to the router through typed `linked_externals` rather than direct
 references, so the missing sibling is a translation completeness gap,
 not a wire-up gap.
 
-## 4. Blocked surface (`Contract.lean`, `BLOCKED(verity#1832):` markers)
+## 4. Remaining boundary surface
 
 The public ZK entry points carrying `Transaction[] calldata` /
-`WithdrawalTransaction[] calldata` parameters are documented but not
-translated, because their struct elements contain nested dynamic
-members (`uint256[]`, `Ciphertext[]`). The macro rejects struct
-parameter projection from an ABI-dynamic-root at
-`Verity/Macro/Translate.lean:1715`. Tracked dedicated under verity#1832
-(umbrella: verity#1760). Once that lands, the following land 1:1 from
-`UnlinkPool.sol`:
-
-- `transfer(Transaction[] calldata _transactions)`
-  (UnlinkPool.sol:309 ff.)
-- `withdraw(WithdrawalTransaction[] calldata _withdrawals)`
-- `emergencyWithdraw(WithdrawalTransaction[] calldata _transactions)`
-  (UnlinkPool.sol:374-383)
+`WithdrawalTransaction[] calldata` parameters are now translated through
+source-shaped dynamic-array projections. Remaining promotion blockers are
+explicit boundaries rather than basic body expressibility: Poseidon T3/T4,
+Permit2, Groth16 verifier dispatch, and host-level UUPS proxy storage
+rotation.
 
 ### Source confirmation: no UnlinkAdapter at this pin
 
@@ -61,30 +53,24 @@ adapter surface (UE-425)`, which predates our pin
 references the older multi-relayer release that still carried the
 adapter; at the current pin, the case scope is `UnlinkPool` only.
 
-`deposit` translation is gated by verity#1824 (Array-param helper
-lowering), not verity#1832: `Note[]` is a static-tuple-element array
-the macro already accepts, but the natural deposit translation needs
-internal helpers (`_validateAndCollectDeposit`, `_insertLeaves`,
-`_transferWithBalanceCheck`) accepting `Array Note` / `Array Uint256`
-parameters — which verity#1824 documents as unsupported in current
-macro helper lowering.
+`deposit` is translated with source-shaped note validation, Permit2
+witness transfer through the linked boundary, LazyIMT leaf insertion, and
+the source-shaped `Deposited` event payload.
 
 ## Build status
 
 Case stage: `scoped`. `lake build Benchmark.Cases.UnlinkXyz.Pool.Compile`
 green locally. Promotion to `build_green` happens when:
 
-1. verity#1832 lands (struct parameter projection from an ABI-dynamic
-   root).
-2. verity#1824 lands (Array-param helper lowering) — for the
-   helper-factored `deposit` body.
-3. The lakefile in this repo bumps to the resulting verity commit.
-4. The three blocked entry points (`transfer`, `withdraw`,
-   `emergencyWithdraw`) and `deposit` are wired through.
+1. The manifest-level unsupported feature list is cleared.
+2. The remaining cryptographic / Permit2 / Groth16 / UUPS boundaries are
+   either modeled directly or accepted as supported external boundaries.
+3. The lakefile in this repo points at the required Verity revision.
 
 ## Next milestones
 
-- `build_green` once `deposit` + the three blocked entries elaborate.
+- `build_green` once the remaining boundary decisions are resolved and the
+  manifest is promoted.
 - `proof_partial` after a target invariant is selected (likely:
   per-token conservation across `deposit + withdraw` once nullifier
   spend is gated, modeled with the four assumed boundaries).

cases/unlink_xyz/pool/upstream/source-metadata.md

@@ -15,23 +15,23 @@ commit:
 - `protocol/contracts/src/State.sol` — inherited state container (merkle
   root + nullifier-spent set + verifier router).
 - `protocol/contracts/src/lib/InternalLazyIMT.sol` — append-only Lazy-IMT
-  state mutated by `_insertLeaves`. Verity routes this as an assumed-status
-  external library boundary.
+  state mutated by `_insertLeaves`. Verity models this directly in the pool
+  helper path.
 - `protocol/contracts/src/VerifierRouter.sol` — Groth16 verifier circuit
   registry, accessed through `linked_externals`.
 - `protocol/contracts/src/lib/Poseidon.sol` and `PoseidonT4.sol` —
-  Poseidon T4 hash, assumed as a package-local axiom.
+  Poseidon hashes, routed through package-local opaque boundaries.
 
 ## Modeling boundaries
 
-These external dependencies are routed through assumed-status ECMs or
+These external dependencies are routed through opaque helpers, ECMs, or
 linked-external declarations per the `unlink-verity` package-split policy
 documented in `lfglabs-dev/verity:docs/ROADMAP.md` "Unlink Audit Readiness":
 
-| External | Treatment | Axiom / module name |
+| External | Treatment | Boundary / module name |
 |----------|-----------|---------------------|
-| Poseidon T4 | Pure assumed axiom | `unlink_verity_poseidon_t4` |
-| Permit2 `permitWitnessTransferFrom` | Assumed-status ECM with bubble-revert | `unlink_verity_permit2_permit_witness_transfer_from` |
-| Lazy-IMT `_insert` | Assumed-status state-mutating helper | `unlink_verity_lazy_imt_insert` |
-| Groth16 verifier dispatch | `linked_externals` against `VerifierRouter` | `unlink_verity_verifier_router_get_circuit` + `unlink_verity_groth16_verify_proof` |
+| Poseidon T3 / T4 | Opaque hash boundary | `poseidonT3` / `poseidonT4` |
+| Permit2 `permitWitnessTransferFrom` | Linked external with balance-delta checks | `permitWitnessTransferFrom` |
+| Lazy-IMT `_insert` | Source-shaped Lean helper over pool storage | `lazyInsert` / `insertLeaves` |
+| Groth16 verifier dispatch | `linked_externals` against `VerifierRouter` | `getCircuit` + `verifySpend` |
 | BN254 precompiles (0x06 / 0x07 / 0x08) | First-class Verity ECMs | `evm_bn256_add_precompile` / `evm_bn256_scalar_mul_precompile` / `evm_bn256_pairing_precompile` |