From ce8f85456ff5f09f5c1d57edc53caac363872573 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Fri, 15 May 2026 00:34:41 +0200 Subject: [PATCH] Remove UnlinkPool Lean axioms from specs --- .../Cases/UnlinkXyz/Pool/InternalLazyIMT.lean | 3 +- Benchmark/Cases/UnlinkXyz/Pool/Proofs.lean | 8 ++- Benchmark/Cases/UnlinkXyz/Pool/Specs.lean | 19 ++----- cases/unlink_xyz/pool/case.yaml | 6 +-- cases/unlink_xyz/pool/review/spec-review.md | 50 +++++++------------ .../pool/upstream/source-metadata.md | 18 +++---- 6 files changed, 38 insertions(+), 66 deletions(-) diff --git a/Benchmark/Cases/UnlinkXyz/Pool/InternalLazyIMT.lean b/Benchmark/Cases/UnlinkXyz/Pool/InternalLazyIMT.lean index aec5974..4c42cd8 100644 --- a/Benchmark/Cases/UnlinkXyz/Pool/InternalLazyIMT.lean +++ b/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 diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Proofs.lean b/Benchmark/Cases/UnlinkXyz/Pool/Proofs.lean index 32c03ad..cfc816d 100644 --- a/Benchmark/Cases/UnlinkXyz/Pool/Proofs.lean +++ b/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 diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Specs.lean b/Benchmark/Cases/UnlinkXyz/Pool/Specs.lean index 2b5813c..56a39c0 100644 --- a/Benchmark/Cases/UnlinkXyz/Pool/Specs.lean +++ b/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) diff --git a/cases/unlink_xyz/pool/case.yaml b/cases/unlink_xyz/pool/case.yaml index 76d25f0..fa9503a 100644 --- a/cases/unlink_xyz/pool/case.yaml +++ b/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. diff --git a/cases/unlink_xyz/pool/review/spec-review.md b/cases/unlink_xyz/pool/review/spec-review.md index a15cae2..3f08da5 100644 --- a/cases/unlink_xyz/pool/review/spec-review.md +++ b/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). diff --git a/cases/unlink_xyz/pool/upstream/source-metadata.md b/cases/unlink_xyz/pool/upstream/source-metadata.md index 2e48b53..805a2d6 100644 --- a/cases/unlink_xyz/pool/upstream/source-metadata.md +++ b/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` |