From f036bc342a9fbc74aa0ded45ed8fd7f027da512f Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Thu, 14 May 2026 20:30:29 +0200 Subject: [PATCH] Use Unlink memory array helpers --- Benchmark/Cases/UnlinkXyz/Pool/Contract.lean | 105 +++++++++++++------ cases/unlink_xyz/pool/case.yaml | 24 ++--- lake-manifest.json | 4 +- lakefile.lean | 2 +- 4 files changed, 86 insertions(+), 49 deletions(-) diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean index 514212a..796db48 100644 --- a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean +++ b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean @@ -42,10 +42,8 @@ These shapes use struct-array parameters whose elements carry nested dynamic members (`uint256[] nullifierHashes`, `Ciphertext[] ciphertexts`, etc.). The remaining fidelity gaps are the parts that still need - first-class source equivalents in Verity or this model: memory-array return - helpers for `_realCommitments` / `_realNullifiers`, the source-level - memory-array value passed into `_insertLeaves`, and dynamic array event - payloads. + first-class source equivalents in Verity or this model: dynamic array event + payloads and the LazyIMT insertion body behind `_insertLeaves`. -/ import Contracts.Common import Compiler.Modules.Hashing @@ -402,26 +400,69 @@ verity_contract UnlinkPool where else pure ()) - /- Source shape: `_insertLeaves(_realCommitments(values, excludeIndex))`. - Verity does not yet model memory-array-return helpers, so this helper - fuses the source filter with the `_insertLeaves` state update while - keeping the insertion side-effect factored out of entry points. -/ - function insertFilteredLeaves - (values : Array Uint256, excludeIndex : Uint256, leafCount : Uint256, - startIndex : Uint256) : Uint256 := do - let mut newRoot := startIndex - forEach "m" (arrayLength values) (do - let leaf := arrayElement values m - if m != excludeIndex then - if leaf != 0 then - newRoot := add newRoot leaf + function realCommitments + (newCommitments : Array Uint256, excludeIndex : Uint256) + : Array Uint256 := do + let len := arrayLength newCommitments + let mut count := 0 + forEach "i" len (do + let commitment := arrayElement newCommitments i + if i != excludeIndex then + if commitment != 0 then + count := add count 1 + else + pure () + else + pure ()) + let leaves ← allocArray count + let mut j := 0 + forEach "i" len (do + let commitment := arrayElement newCommitments i + if i != excludeIndex then + if commitment != 0 then + setMemoryArrayElement leaves j commitment + j := add j 1 else pure () else pure ()) + returnArray leaves + + function realNullifiers (nullifierHashes : Array Uint256) : Array Uint256 := do + let len := arrayLength nullifierHashes + let mut count := 0 + forEach "i" len (do + let nullifierHash := arrayElement nullifierHashes i + if nullifierHash != 0 then + count := add count 1 + else + pure ()) + let real ← allocArray count + let mut j := 0 + forEach "i" len (do + let nullifierHash := arrayElement nullifierHashes i + if nullifierHash != 0 then + setMemoryArrayElement real j nullifierHash + j := add j 1 + else + pure ()) + returnArray real + + /- Source shape: `_insertLeaves(uint256[] memory _leafHashes)`. + The LazyIMT update is still represented by the existing lightweight + accumulator used by this scoped benchmark model. -/ + function insertLeaves (leafHashes : Array Uint256) : Uint256 := do + let startIndex ← nextLeafIndex + let mut newRoot := startIndex + forEach "m" (arrayLength leafHashes) (do + let leaf := arrayElement leafHashes m + if leaf != 0 then + newRoot := add newRoot leaf + else + pure ()) setStorage stateMerkleRoot newRoot setMappingWord stateRootSeen newRoot 0 1 - setStorage lazyNumberOfLeaves (add startIndex leafCount) + setStorage lazyNumberOfLeaves (add startIndex (arrayLength leafHashes)) return newRoot function view computeContextHash (ciphertexts : Array Ciphertext) : Uint256 := do @@ -503,16 +544,14 @@ verity_contract UnlinkPool where requireError proofOk PoolProofVerificationFailed() requireError ok PoolProofVerificationFailed() spendNullifiers txn.nullifierHashes - let startIndex ← nextLeafIndex - let newRoot ← insertFilteredLeaves txn.newCommitments - 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff - ciphertextCount - startIndex - let realNullifierCount ← countNonZero txn.nullifierHashes + let leaves ← realCommitments txn.newCommitments 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff + let startIndex ← nextLeafIndex + let newRoot ← insertLeaves leaves + let realNullifierHashes ← realNullifiers txn.nullifierHashes emit "Transferred" - [newRoot, startIndex, ciphertextCount, - realNullifierCount, + [newRoot, startIndex, arrayLength leaves, + arrayLength realNullifierHashes, arrayLength txn.ciphertexts]) /- `_executeWithdrawal(WithdrawalTransaction calldata _txn, bool _emergency)` @@ -568,19 +607,19 @@ verity_contract UnlinkPool where requireError proofOk PoolProofVerificationFailed() requireError ok PoolProofVerificationFailed() spendNullifiers txn.nullifierHashes + let leaves ← realCommitments txn.newCommitments wSlot let startIndex ← nextLeafIndex - let newRoot ← insertFilteredLeaves txn.newCommitments wSlot ciphertextCount startIndex + let newRoot ← insertLeaves leaves settleWithdrawalTransfer txn.withdrawal.token recipient txn.withdrawal.amount - let realNullifierCount ← countNonZero txn.nullifierHashes - 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff + let realNullifierHashes ← realNullifiers txn.nullifierHashes if emergency then emit "EmergencyWithdrawn" [addressToWord recipient, txn.withdrawal.npk, addressToWord txn.withdrawal.token, txn.withdrawal.amount, - newRoot, startIndex, ciphertextCount, - realNullifierCount, + newRoot, startIndex, arrayLength leaves, + arrayLength realNullifierHashes, arrayLength txn.ciphertexts] else emit "Withdrawn" @@ -588,8 +627,8 @@ verity_contract UnlinkPool where txn.withdrawal.npk, addressToWord txn.withdrawal.token, txn.withdrawal.amount, - newRoot, startIndex, ciphertextCount, - realNullifierCount, + newRoot, startIndex, arrayLength leaves, + arrayLength realNullifierHashes, arrayLength txn.ciphertexts] /- `function withdraw(WithdrawalTransaction[] calldata _transactions) diff --git a/cases/unlink_xyz/pool/case.yaml b/cases/unlink_xyz/pool/case.yaml index 1cc25e3..1442dc0 100644 --- a/cases/unlink_xyz/pool/case.yaml +++ b/cases/unlink_xyz/pool/case.yaml @@ -32,7 +32,7 @@ selected_functions: - acceptOwnership - renounceOwnership source_language: solidity -verity_version: 5781a22489c721670f33bc1a74563cacd7d9232b +verity_version: cd1f92dda5bbf3aed775a744cba1e3da883c739e lean_toolchain: leanprover/lean4:v4.22.0 abstraction_level: protocol_slice abstraction_tags: @@ -64,16 +64,15 @@ abstraction_notes: > `emergencyWithdraw`) now build against `Array Transaction` / `Array WithdrawalTransaction` parameters using dynamic struct-array member projections and projected dynamic-array forwarding to linked - externals / internal helpers. Remaining promotion blockers are fidelity - gaps rather than basic body expressibility: memory-array-return helper - shapes for `_realCommitments` / `_realNullifiers`, source-faithful - memory-array values flowing into `_insertLeaves`, and event payloads - carrying dynamic arrays. Event ABI metadata is now declared in the - macro-generated `CompilationModel.events` table, but the executable - `emit` sites still use surrogate scalar counts until first-class dynamic - array payload emission lands. `_executeWithdrawal(_transactions[i], bool)` is - now routed through an internal helper call; the insertion mutation is also - factored into a helper while memory-array construction remains pending. + externals / internal helpers. The transfer/withdraw paths now use + `_realCommitments` / `_realNullifiers`-shaped memory-array helpers and pass + the resulting memory array into an `_insertLeaves`-shaped helper. Remaining + promotion blockers are fidelity gaps rather than basic body expressibility: + event payloads still use surrogate scalar counts until first-class dynamic + array payload emission lands, and the `_insertLeaves` body still uses this + scoped model's lightweight LazyIMT accumulator boundary. + `_executeWithdrawal(_transactions[i], bool)` is routed through an internal + helper call. Source confirmation (pinned commit 4bc46c1f): there is NO `UnlinkAdapter`, no `adapterDeposit`, no `adapterWithdraw` — @@ -105,9 +104,8 @@ abstraction_notes: > into internal helpers that accept `Array Note` / `Array Uint256` parameters until that ships. unsupported_feature_codes: - - memory_array_return_helpers - - source_faithful_insert_leaves - dynamic_array_event_payloads + - lazy_imt_insert_body_assumed - uups_proxy_storage_rotation_not_modeled - bn254_precompile_probes_via_ecm_assumed - poseidon_assumed_axiom diff --git a/lake-manifest.json b/lake-manifest.json index efc2351..49b9cf1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5781a22489c721670f33bc1a74563cacd7d9232b", + "rev": "cd1f92dda5bbf3aed775a744cba1e3da883c739e", "name": "verity", "manifestFile": "lake-manifest.json", - "inputRev": "5781a22489c721670f33bc1a74563cacd7d9232b", + "inputRev": "cd1f92dda5bbf3aed775a744cba1e3da883c739e", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/lfglabs-dev/EVMYulLean.git", diff --git a/lakefile.lean b/lakefile.lean index 4466587..bdb3abd 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,7 +5,7 @@ package «verity-benchmark» where version := v!"0.1.0" require verity from git - "https://github.com/lfglabs-dev/verity.git"@"5781a22489c721670f33bc1a74563cacd7d9232b" + "https://github.com/lfglabs-dev/verity.git"@"cd1f92dda5bbf3aed775a744cba1e3da883c739e" @[default_target] lean_lib «Benchmark» where