Verity feature parity for Unlink (privacy pool + atomic-DeFi adapter)

[Th0rgal]

Goal

Make verity_contract capable of expressing the Unlink privacy pool and atomic-DeFi adapter end-to-end at the compilation level (proofs out of scope for this issue, but no choice made here should make a future proof effort harder).

Context

Unlink is a UTXO-based privacy pool for EVM (Tornado / RAILGUN family) with an explicit DeFi adapter for atomic withdraw → DeFi → re-deposit. Two core contracts:

• UnlinkPool — UUPS-upgradeable, Permit2 deposits, ZK transfers, ERC20 withdrawals, Lazy-IMT state, Poseidon commitments, Groth16 proof verification.
• UnlinkAdapter — non-upgradeable, balance-neutral DeFi router; arbitrary Call[] execution between an adapterWithdraw and re-deposit.

We want to ship a Verity model of these contracts to grow verity-benchmark and to give Unlink users meaningful safety guarantees (per-token conservation, no double-spend, balance-neutrality of the adapter, withdrawal recipient/amount/token binding to the proof, etc.).

Scope

This issue is about what Verity itself needs. Assumed-status ECMs for Poseidon, Permit2, Lazy-IMT, and the Groth16 verifier are expected to ship in a separate unlink-verity package and are not part of this issue.

Required Verity-core changes

P0 — new (no existing issue)

• Nested-dynamic struct ABI decoding for calldata array params.
  Transaction[] calldata, WithdrawalTransaction[] calldata, AdapterTransaction[] calldata, where each element contains nested dynamic fields (uint256[], Ciphertext[]).
  Today the macro only accepts arrays whose element is a static tuple of ABI words (the case landed for Morpho's CurveCut[]). Without this, the function signatures of transfer, withdraw, adapterWithdraw cannot be written.
• SELFBALANCE / address(this).balance first-class expression.
  Needed for UnlinkAdapter._assertZeroBalance's ETH residual check. Listed under Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 P6 as missing; no standalone issue yet.
• ETH-aware generic external call ECM (call{value: v}(data) with arbitrary calldata + bubble-revert).
  Calls.withReturn only handles single-uint256 returns. Needed for UnlinkAdapter._executeCalls's arbitrary Call[].

P1 — already filed (push priority, link from this issue)

• verity_contract cannot call functions from another Solidity library #1748 — verity_contract cannot call functions from another Solidity library. Highest leverage of the filed issues; covers Poseidon, Lazy-IMT, and (with a Permit2 wrapper) Permit2.
• verity_contract has no named struct types for function parameters #1750 — Named struct types for function parameters. Companion to the nested-dynamic ABI work above. Alone, unblocks Note / Ciphertext (single-element static-tuple cases).
• verity_contract function bodies cannot call user-defined Lean def helpers #1749 — verity_contract bodies cannot call user-defined Lean def helpers. Currently the cleanest way to wrap an assumed Poseidon / verifier interface; without it every assumed dependency has to ride through an ECM.

P2 — nice-to-have, not unlink-critical

• Macro shorthand for "trusted external library import" — one-line declaration of a stateless library function as an assumed-status ECM, instead of ~30 lines of Lean per function.

Out of scope for this issue

• UUPS upgrade-path proof modeling (Verification: proxy and upgradeability semantics on top of native delegatecall support #1420) — UnlinkPool is a UUPS implementation; the implementation compiles fine without it. Only matters when/if we want to reason about post-upgrade state.
• Full linear-memory / mload/mstore proof coverage — covered by the EVMYulLean transition (Target native EVMYulLean runtime for generated Yul #1737).
• Helper-call compositional proof reuse (Layer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image #1630, Proof: model IR internal helper composition for the generic Layer 2 theorem #1638) — only relevant once we move from "compiles" to "proves".

Definition of done

This issue is closed when all of the following hold:

1. P0 features land in lfglabs-dev/verity main

• Nested-dynamic ABI decoding
  • The macro accepts Array (Tuple [...]) element types that themselves contain Array Uint256 / Bytes / nested tuples (at least the shapes of Note, Ciphertext, Proof, Transaction, WithdrawalTransaction, AdapterTransaction from unlink-xyz/monorepo protocol/contracts/src/lib/Models.sol).
  • Round-trip property test (Contracts/MacroTranslateRoundTripFuzz.lean analog) covers at least one such shape end-to-end (calldata in → field access → returndata).
  • Foundry differential test added that exercises the new decoder against solc-emitted ABI for the exact Transaction struct.
  • docs/INTERPRETER_FEATURE_MATRIX.md updated.
• SELFBALANCE expression
  • New Expr.selfBalance constructor (or equivalent) with Yul lowering to selfbalance().
  • Source-side semantics added to Verity/Core.lean ContractState (a selfBalance : Uint256 field) and threaded through Contract.run.
  • One smoke contract under Contracts/ and one Foundry differential test.
  • Listed in the interpreter feature matrix.
• ETH-aware generic call ECM
  • New ECM in Compiler/Modules/ (e.g. Calls.callWithValue) accepting (target, value, data) with bubble-revert; proofStatus := .assumed; documented axiom name.
  • One smoke contract using it for an arbitrary (to, value, data) triple.
  • Listed in docs/EXTERNAL_CALL_MODULES.md.

2. P1 issues closed

• verity_contract cannot call functions from another Solidity library #1748, verity_contract has no named struct types for function parameters #1750, verity_contract function bodies cannot call user-defined Lean def helpers #1749 are merged and closed in a way that satisfies their original repro cases (TermMax in verity_contract cannot call functions from another Solidity library #1748/verity_contract function bodies cannot call user-defined Lean def helpers #1749/verity_contract has no named struct types for function parameters #1750), and is sufficient for the unlink model below.

3. End-to-end Unlink model builds

• A new verity-benchmark case cases/unlink/pool/ exists with:
  • A verity_contract UnlinkPool declaration that compiles via lake build, exposing at minimum the public methods deposit, transfer, withdraw, adapterDeposit, adapterWithdraw, addRelayer, removeRelayer, setAdapter, initialize, plus the public views.
  • A verity_contract UnlinkAdapter declaration that compiles via lake build, exposing execute, addRelayer, removeRelayer, computeAdapterDataHash, plus public views.
  • Poseidon, Permit2, Lazy-IMT, and the Groth16 verifier router routed through assumed-status ECMs (or library-call surface from verity_contract cannot call functions from another Solidity library #1748). Their axiom names are listed in the case's README.
• verity-compiler --trust-report on the case emits a manifest whose only assumed/unchecked entries are the four ECMs above plus the documented EVMYulLean / linear-memory / proxy-upgradeability boundaries.

4. Documentation

• docs/ROADMAP.md "Solidity Interop Profile" status table reflects the landed features.
• docs/INTERPRETER_FEATURE_MATRIX.md updated.
• A short "Lessons from Unlink" section added to docs/ROADMAP.md (mirroring the existing "Lessons from UnlinkPool ([Meta] Roadmap for compiling real-world contracts: lessons from UnlinkPool #185)" pattern), capturing what changed in Verity vs what was punted to assumed ECMs.

5. No regressions

• make check green.
• All existing Foundry differential tests still pass.
• Theorem count in the README stats block has not regressed (no new sorry, no new axioms beyond the four documented ECMs).

Related

• Umbrella: Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 (Solidity feature parity)
• Subsumed (kept open, repro-specific): verity_contract cannot call functions from another Solidity library #1748, verity_contract has no named struct types for function parameters #1750, verity_contract function bodies cannot call user-defined Lean def helpers #1749
• Adjacent (proofs, not on this issue's path): Target native EVMYulLean runtime for generated Yul #1737, Layer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image #1630, Proof: model IR internal helper composition for the generic Layer 2 theorem #1638, Verification: proxy and upgradeability semantics on top of native delegatecall support #1420