Skip to content

Use generic Verity ergonomics in UnlinkPool #69

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Th0rgal merged 2 commits into from
May 16, 2026
Merged

Use generic Verity ergonomics in UnlinkPool #69

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d26d7e5
Use generic Verity ergonomics in UnlinkPool
Th0rgal May 15, 2026
d94775d
Update UnlinkPool ergonomics Verity pin
Th0rgal May 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
101 changes: 42 additions & 59 deletions Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,12 @@ verity_contract UnlinkPool where
nonce : Uint256,
deadline : Uint256

struct Circuit where
verifier : Uint256,
inputCount : Uint256,
outputCount : Uint256,
active : Uint256

struct Transaction where
proof : Proof,
circuitId : Uint256,
Expand Down Expand Up @@ -374,15 +380,22 @@ verity_contract UnlinkPool where
-- `(verifier, inputCount, outputCount, active)`. The first argument is the
-- stored router address that Solidity obtains through `_getVerifierRouter()`.
linked_externals
external getCircuit(Address, Uint256) -> (Uint256, Uint256, Uint256, Uint256)
external getCircuit(Address, Uint256) -> (Circuit)
external getCircuit_try(Address, Uint256) -> (Bool, Circuit)
external verifySpend(
Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256,
Uint256, Uint256, Uint256, Array Uint256, Array Uint256) -> (Bool)
external verifySpend_try(
Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256,
Uint256, Uint256, Uint256, Array Uint256, Array Uint256) -> (Bool, 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)
external permitWitnessTransferFrom_try(
Address, Address, Uint256, Uint256, Uint256, Address, Uint256, Address,
Uint256, Bytes) -> (Bool, Bool)

/- `constructor(address _permit2)` (UnlinkPool.sol:147-160).

Expand All @@ -397,6 +410,13 @@ verity_contract UnlinkPool where
-- binding automatically. `_disableInitializers` sets the marker.
setStorage initializedSlot 0xff

/- Solidity's `onlyRelayer` modifier delegates to `_checkRelayer()`
(UnlinkPool.sol:266-270). -/
modifier onlyRelayer := do
let sender ← msgSender
let isR ← getMapping relayersSlot sender
requireError (isR != 0) PoolUnauthorizedRelayer()

/- `function initialize(address _verifierRouter, address _owner,
address _relayer) external initializer`
(UnlinkPool.sol:166-184).
Expand Down Expand Up @@ -578,14 +598,6 @@ verity_contract UnlinkPool where
setStorageAddr ownerSlot pending
setStorageAddr pendingOwnerSlot zeroAddress

/- ### Relayer modifier (inlined per call site) -/

/- `function _checkRelayer() internal view` (UnlinkPool.sol:266-270). -/
function _checkRelayer () : Unit := do
let sender ← msgSender
let isR ← getMapping relayersSlot sender
requireError (isR != 0) PoolUnauthorizedRelayer()

function countNonZero (values : Array Uint256, excludeIndex : Uint256) : Uint256 := do
let mut count := 0
forEach "j" (arrayLength values) (do
Expand Down Expand Up @@ -807,10 +819,7 @@ verity_contract UnlinkPool where
(UnlinkPool.sol:306-324). -/
function nonreentrant(reentrancyLockSlot) deposit
(depositor : Address, notes : Array Note, ciphertexts : Array Ciphertext,
permit : PermitTransferFrom, signature : Bytes) : Unit := do
let sender ← msgSender
let isR ← getMapping relayersSlot sender
requireError (isR != 0) PoolUnauthorizedRelayer()
permit : PermitTransferFrom, signature : Bytes) with onlyRelayer : Unit := do
let notesLen := arrayLength notes
requireError (notesLen != 0) PoolEmptyNotes()
requireError ((arrayLength ciphertexts) == notesLen)
Expand Down Expand Up @@ -851,26 +860,21 @@ verity_contract UnlinkPool where
/- `function transfer(Transaction[] calldata _transactions) external
onlyRelayer nonReentrant` (UnlinkPool.sol:328-363). -/
function nonreentrant(reentrancyLockSlot) transfer (transactions : Array Transaction)
: Unit := do
let sender ← msgSender
let isR ← getMapping relayersSlot sender
requireError (isR != 0) PoolUnauthorizedRelayer()
with onlyRelayer : Unit := do
let txLen := arrayLength transactions
requireError (txLen != 0) PoolEmptyTransactions()
forEach "i" txLen (do
let txn := arrayElement transactions i
let verifierRouter ← getStorageAddr stateVerifierRouter
let (success, verifier, inputCount, outputCount, active) ←
let (success, circuit) ←
tryExternalCall "getCircuit"
[verifierRouter, txn.circuitId]
let verifierWord := add verifier 0
let activeWord := add active 0
requireError success PoolCircuitNotRegistered()
requireError (verifierWord != 0) PoolCircuitNotRegistered()
requireError (activeWord != 0) PoolCircuitInactive()
requireError ((arrayLength txn.nullifierHashes) == inputCount)
requireError (circuit.verifier != 0) PoolCircuitNotRegistered()
requireError (circuit.active != 0) PoolCircuitInactive()
requireError ((arrayLength txn.nullifierHashes) == circuit.inputCount)
PoolInvalidInputShape()
requireError ((arrayLength txn.newCommitments) == outputCount)
requireError ((arrayLength txn.newCommitments) == circuit.outputCount)
PoolInvalidOutputShape()
let ciphertextCount ← countNonZero txn.newCommitments
0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
Expand All @@ -879,15 +883,8 @@ verity_contract UnlinkPool where
let computedContext ← computeContextHash txn.ciphertexts
validateContext txn.merkleRoot txn.contextHash computedContext
let (proofOk, ok) ← tryExternalCall "verifySpend"
[verifierWord,
abiHeadWord txn 0,
abiHeadWord txn 1,
abiHeadWord txn 2,
abiHeadWord txn 3,
abiHeadWord txn 4,
abiHeadWord txn 5,
abiHeadWord txn 6,
abiHeadWord txn 7,
[circuit.verifier,
abiEncode txn.proof,
txn.merkleRoot,
txn.contextHash,
txn.nullifierHashes,
Expand All @@ -899,9 +896,8 @@ verity_contract UnlinkPool where
0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
let startIndex ← nextLeafIndex
let newRoot ← insertLeaves leaves
let realNullifierHashes ← realNullifiers txn.nullifierHashes
emit "Transferred"
[newRoot, startIndex, leaves, realNullifierHashes, txn.ciphertexts])
[newRoot, startIndex, leaves, realNullifiers txn.nullifierHashes, txn.ciphertexts])

/- `_executeWithdrawal(WithdrawalTransaction calldata _txn, bool _emergency)`
(UnlinkPool.sol:614-666). -/
Expand All @@ -918,18 +914,16 @@ verity_contract UnlinkPool where
let selfAddr ← Verity.contractAddress
requireError (recipient != selfAddr) PoolInvalidWithdrawalRecipient()
let verifierRouter ← getStorageAddr stateVerifierRouter
let (success, verifier, inputCount, outputCount, active) ←
let (success, circuit) ←
tryExternalCall "getCircuit" [verifierRouter, txn.circuitId]
let verifierWord := add verifier 0
let activeWord := add active 0
requireError success PoolCircuitNotRegistered()
requireError (verifierWord != 0) PoolCircuitNotRegistered()
requireError (activeWord != 0) PoolCircuitInactive()
requireError ((arrayLength txn.nullifierHashes) == inputCount)
requireError (circuit.verifier != 0) PoolCircuitNotRegistered()
requireError (circuit.active != 0) PoolCircuitInactive()
requireError ((arrayLength txn.nullifierHashes) == circuit.inputCount)
PoolInvalidInputShape()
requireError ((arrayLength txn.newCommitments) == outputCount)
requireError ((arrayLength txn.newCommitments) == circuit.outputCount)
PoolInvalidOutputShape()
let wSlot := sub outputCount 1
let wSlot := sub circuit.outputCount 1
let withdrawalCommitment := arrayElement txn.newCommitments wSlot
requireError (withdrawalCommitment != 0) PoolWithdrawalSlotZero()
let noteHash ← hashNote txn.withdrawal.npk txn.withdrawal.token txn.withdrawal.amount
Expand All @@ -940,15 +934,8 @@ verity_contract UnlinkPool where
let computedContext ← computeContextHash txn.ciphertexts
validateContext txn.merkleRoot txn.contextHash computedContext
let (proofOk, ok) ← tryExternalCall "verifySpend"
[verifierWord,
abiHeadWord txn 0,
abiHeadWord txn 1,
abiHeadWord txn 2,
abiHeadWord txn 3,
abiHeadWord txn 4,
abiHeadWord txn 5,
abiHeadWord txn 6,
abiHeadWord txn 7,
[circuit.verifier,
abiEncode txn.proof,
txn.merkleRoot,
txn.contextHash,
txn.nullifierHashes,
Expand All @@ -960,23 +947,19 @@ verity_contract UnlinkPool where
let startIndex ← nextLeafIndex
let newRoot ← insertLeaves leaves
settleWithdrawalTransfer txn.withdrawal.token recipient txn.withdrawal.amount
let realNullifierHashes ← realNullifiers txn.nullifierHashes
if emergency then
emit "EmergencyWithdrawn"
[addressToWord recipient, txn.withdrawal, newRoot, startIndex, leaves,
realNullifierHashes, txn.ciphertexts]
realNullifiers txn.nullifierHashes, txn.ciphertexts]
else
emit "Withdrawn"
[addressToWord recipient, txn.withdrawal, newRoot, startIndex, leaves,
realNullifierHashes, txn.ciphertexts]
realNullifiers txn.nullifierHashes, txn.ciphertexts]

/- `function withdraw(WithdrawalTransaction[] calldata _transactions)
external onlyRelayer nonReentrant` (UnlinkPool.sol:365-372). -/
function nonreentrant(reentrancyLockSlot) withdraw (transactions : Array WithdrawalTransaction)
: Unit := do
let sender ← msgSender
let isR ← getMapping relayersSlot sender
requireError (isR != 0) PoolUnauthorizedRelayer()
with onlyRelayer : Unit := do
let txLen := arrayLength transactions
requireError (txLen != 0) PoolEmptyTransactions()
forEach "i" txLen (do
Expand Down
4 changes: 2 additions & 2 deletions lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "56b831a53113d1df3a0dc78209a6b25fe6794ba2",
"rev": "551ab45c7c2fefcdac385946d22758ff3854c00c",
"name": "verity",
"manifestFile": "lake-manifest.json",
"inputRev": "56b831a53113d1df3a0dc78209a6b25fe6794ba2",
"inputRev": "551ab45c7c2fefcdac385946d22758ff3854c00c",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/lfglabs-dev/EVMYulLean.git",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ package «verity-benchmark» where
version := v!"0.1.0"

require verity from git
"https://github.com/lfglabs-dev/verity.git"@"56b831a53113d1df3a0dc78209a6b25fe6794ba2"
"https://github.com/lfglabs-dev/verity.git"@"551ab45c7c2fefcdac385946d22758ff3854c00c"

@[default_target]
lean_lib «Benchmark» where
Expand Down
Loading