From f4dd9225ff6bd796da40633f0751acf08e9c8096 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Fri, 15 May 2026 00:26:15 +0200 Subject: [PATCH] Wire UnlinkPool LazyIMT insertion body --- Benchmark/Cases/UnlinkXyz/Pool/Contract.lean | 172 +++++++++++++++++-- cases/unlink_xyz/pool/case.yaml | 7 +- 2 files changed, 155 insertions(+), 24 deletions(-) diff --git a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean index 8cfe2d3..6ab16d6 100644 --- a/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean +++ b/Benchmark/Cases/UnlinkXyz/Pool/Contract.lean @@ -44,8 +44,7 @@ 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: the - LazyIMT insertion body behind `_insertLeaves` and the external cryptographic - / Permit2 boundaries tracked in the case manifest. + external cryptographic / Permit2 boundaries tracked in the case manifest. -/ import Contracts.Common import Compiler.ECM @@ -327,6 +326,44 @@ verity_contract UnlinkPool where -- "DepositWitness(address pool,bytes32 notesHash)"). DEPOSIT_WITNESS_TYPEHASH : Uint256 := 0xbc5a735b1283bedbbb26bd202f39770544802f342490e830972aacc15681b130 + SNARK_SCALAR_FIELD : Uint256 := + 21888242871839275222246405745257275088548364400416034343698204186575808495617 + MAX_LAZY_INDEX : Uint256 := 0xffffffff + MAX_NOTE_VALUE : Uint256 := + 100000000000000000000000000000000000000000000000000000000000000000000 + Z_0 : Uint256 := 0 + Z_1 : Uint256 := 14744269619966411208579211824598458697587494354926760081771325075741142829156 + Z_2 : Uint256 := 7423237065226347324353380772367382631490014989348495481811164164159255474657 + Z_3 : Uint256 := 11286972368698509976183087595462810875513684078608517520839298933882497716792 + Z_4 : Uint256 := 3607627140608796879659380071776844901612302623152076817094415224584923813162 + Z_5 : Uint256 := 19712377064642672829441595136074946683621277828620209496774504837737984048981 + Z_6 : Uint256 := 20775607673010627194014556968476266066927294572720319469184847051418138353016 + Z_7 : Uint256 := 3396914609616007258851405644437304192396347162513310381425243293 + Z_8 : Uint256 := 21551820661461729022865262380882070649935529853313286572328683688269863701601 + Z_9 : Uint256 := 6573136701248752079028194407151022595060682063033565181951145966236778420039 + Z_10 : Uint256 := 12413880268183407374852357075976609371175688755676981206018884971008854919922 + Z_11 : Uint256 := 14271763308400718165336499097156975241954733520325982997864342600795471836726 + Z_12 : Uint256 := 20066985985293572387227381049700832219069292839614107140851619262827735677018 + Z_13 : Uint256 := 9394776414966240069580838672673694685292165040808226440647796406499139370960 + Z_14 : Uint256 := 11331146992410411304059858900317123658895005918277453009197229807340014528524 + Z_15 : Uint256 := 15819538789928229930262697811477882737253464456578333862691129291651619515538 + Z_16 : Uint256 := 19217088683336594659449020493828377907203207941212636669271704950158751593251 + Z_17 : Uint256 := 21035245323335827719745544373081896983162834604456827698288649288827293579666 + Z_18 : Uint256 := 6939770416153240137322503476966641397417391950902474480970945462551409848591 + Z_19 : Uint256 := 10941962436777715901943463195175331263348098796018438960955633645115732864202 + Z_20 : Uint256 := 15019797232609675441998260052101280400536945603062888308240081994073687793470 + Z_21 : Uint256 := 11702828337982203149177882813338547876343922920234831094975924378932809409969 + Z_22 : Uint256 := 11217067736778784455593535811108456786943573747466706329920902520905755780395 + Z_23 : Uint256 := 16072238744996205792852194127671441602062027943016727953216607508365787157389 + Z_24 : Uint256 := 17681057402012993898104192736393849603097507831571622013521167331642182653248 + Z_25 : Uint256 := 21694045479371014653083846597424257852691458318143380497809004364947786214945 + Z_26 : Uint256 := 8163447297445169709687354538480474434591144168767135863541048304198280615192 + Z_27 : Uint256 := 14081762237856300239452543304351251708585712948734528663957353575674639038357 + Z_28 : Uint256 := 16619959921569409661790279042024627172199214148318086837362003702249041851090 + Z_29 : Uint256 := 7022159125197495734384997711896547675021391130223237843255817587255104160365 + Z_30 : Uint256 := 4114686047564160449611603615418567457008101555090703535405891656262658644463 + Z_31 : Uint256 := 12549363297364877722388257367377629555213421373705596078299904496781819142130 + Z_32 : Uint256 := 21443572485391568159800782191812935835534334817699172242223315142338162256601 -- `ISignatureTransfer public immutable PERMIT2` (UnlinkPool.sol:55). -- Bound at construction time to a constructor-supplied address. @@ -341,6 +378,7 @@ verity_contract UnlinkPool where external verifySpend( Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Array Uint256, Array Uint256) -> (Bool) + external poseidonT3(Uint256, Uint256) -> (Uint256) external permitWitnessTransferFrom( Address, Address, Uint256, Uint256, Uint256, Address, Uint256, Address, Uint256, Bytes) -> (Bool) @@ -465,15 +503,14 @@ verity_contract UnlinkPool where : Uint256 := do return (add npk amount) + function poseidon2 (lhs : Uint256, rhs : Uint256) : Uint256 := do + return externalCall "poseidonT3" [lhs, rhs] + function validateNoteFields (npk : Uint256, token : Address, amount : Uint256) : Unit := do requireError (token != zeroAddress) PoolInvalidNoteToken() - requireError ((amount != 0) && - (amount <= - 100000000000000000000000000000000000000000000000000000000000000000000)) + requireError ((amount != 0) && (amount <= MAX_NOTE_VALUE)) PoolInvalidNoteAmount() - requireError ((npk != 0) && - (npk < - 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + requireError ((npk != 0) && (npk < SNARK_SCALAR_FIELD)) PoolInvalidNoteNPK() function sumNoteAmounts (notes : Array Note) : Uint256 := do @@ -622,21 +659,118 @@ verity_contract UnlinkPool where 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 + function lazyDefaultZero (index : Uint256) : Uint256 := do + let mut zero := Z_0 + if index == 1 then zero := Z_1 else pure () + if index == 2 then zero := Z_2 else pure () + if index == 3 then zero := Z_3 else pure () + if index == 4 then zero := Z_4 else pure () + if index == 5 then zero := Z_5 else pure () + if index == 6 then zero := Z_6 else pure () + if index == 7 then zero := Z_7 else pure () + if index == 8 then zero := Z_8 else pure () + if index == 9 then zero := Z_9 else pure () + if index == 10 then zero := Z_10 else pure () + if index == 11 then zero := Z_11 else pure () + if index == 12 then zero := Z_12 else pure () + if index == 13 then zero := Z_13 else pure () + if index == 14 then zero := Z_14 else pure () + if index == 15 then zero := Z_15 else pure () + if index == 16 then zero := Z_16 else pure () + if index == 17 then zero := Z_17 else pure () + if index == 18 then zero := Z_18 else pure () + if index == 19 then zero := Z_19 else pure () + if index == 20 then zero := Z_20 else pure () + if index == 21 then zero := Z_21 else pure () + if index == 22 then zero := Z_22 else pure () + if index == 23 then zero := Z_23 else pure () + if index == 24 then zero := Z_24 else pure () + if index == 25 then zero := Z_25 else pure () + if index == 26 then zero := Z_26 else pure () + if index == 27 then zero := Z_27 else pure () + if index == 28 then zero := Z_28 else pure () + if index == 29 then zero := Z_29 else pure () + if index == 30 then zero := Z_30 else pure () + if index == 31 then zero := Z_31 else pure () + if index == 32 then zero := Z_32 else pure () + return zero + + function lazyIndexForElement (level : Uint256, index : Uint256) : Uint256 := do + return (add (mul MAX_LAZY_INDEX level) index) + + function lazyInsert (leaf : Uint256) : Unit := do + let startIndex ← getStorage lazyNumberOfLeaves + let maxIndex ← getStorage lazyMaxIndex + requireError (leaf < SNARK_SCALAR_FIELD) PoolInvalidOutputShape() + requireError (startIndex < maxIndex) PoolInvalidOutputShape() + setStorage lazyNumberOfLeaves (add startIndex 1) + let mut index := startIndex + let mut hash := leaf + let mut active := 1 + forEach "level" 32 (do + if active != 0 then + let elementKey ← lazyIndexForElement level index + setMappingWord lazyElements elementKey 0 hash + if bitAnd index 1 == 0 then + active := 0 + else + let siblingKey ← lazyIndexForElement level (sub index 1) + let sibling ← getMappingWord lazyElements siblingKey 0 + let parent ← poseidon2 sibling hash + hash := parent + index := shr 1 index else pure ()) + + function lazyRootWithDepth32 () : Uint256 := do + let numberOfLeaves ← getStorage lazyNumberOfLeaves + if numberOfLeaves == 0 then + return Z_32 + else + let levels ← allocArray 33 + let mut index := sub numberOfLeaves 1 + if bitAnd index 1 == 0 then + let elementKey ← lazyIndexForElement 0 index + let element ← getMappingWord lazyElements elementKey 0 + setMemoryArrayElement levels 0 element + else + setMemoryArrayElement levels 0 Z_0 + forEach "level" 32 (do + let current := arrayElement levels level + if bitAnd index 1 == 0 then + let z ← lazyDefaultZero level + let parent ← poseidon2 current z + setMemoryArrayElement levels (add level 1) parent + else + let levelCount := shr (add level 1) numberOfLeaves + let parentIndex := shr 1 index + if levelCount > parentIndex then + let parentKey ← lazyIndexForElement (add level 1) parentIndex + let parent ← getMappingWord lazyElements parentKey 0 + setMemoryArrayElement levels (add level 1) parent + else + let siblingKey ← lazyIndexForElement level (sub index 1) + let sibling ← getMappingWord lazyElements siblingKey 0 + let parent ← poseidon2 sibling current + setMemoryArrayElement levels (add level 1) parent + index := shr 1 index) + return (arrayElement levels 32) + + /- Source shape: `_insertLeaves(uint256[] memory _leafHashes)`. + Appends each leaf through the flattened LazyIMT spine and recomputes the + depth-32 root, matching `InternalLazyIMT._insert` / `_root(self, 32)`. -/ + function insertLeaves (leafHashes : Array Uint256) : Uint256 := do + let count := arrayLength leafHashes + if count == 0 then + let currentRoot ← getStorage stateMerkleRoot + return currentRoot + else + forEach "m" count (do + let leaf := arrayElement leafHashes m + lazyInsert leaf) + let newRoot ← lazyRootWithDepth32 setStorage stateMerkleRoot newRoot setMappingWord stateRootSeen newRoot 0 1 - setStorage lazyNumberOfLeaves (add startIndex (arrayLength leafHashes)) return newRoot function view computeContextHash (ciphertexts : Array Ciphertext) : Uint256 := do diff --git a/cases/unlink_xyz/pool/case.yaml b/cases/unlink_xyz/pool/case.yaml index 9acd572..76d25f0 100644 --- a/cases/unlink_xyz/pool/case.yaml +++ b/cases/unlink_xyz/pool/case.yaml @@ -39,7 +39,6 @@ abstraction_tags: - uups_proxy_modeled_as_implementation - permit2_assumed_boundary - poseidon_assumed_boundary - - lazy_imt_assumed_boundary - groth16_assumed_boundary - bn254_precompile_ecm - erc7201_storage_namespace @@ -75,8 +74,8 @@ abstraction_notes: > elements, computes the source-shaped deposit witness hash, routes the Permit2 transfer through the assumed external boundary, inserts leaves, and emits the source-shaped `Deposited` payload. Remaining promotion blockers are fidelity - gaps rather than basic body expressibility: the `_insertLeaves` body still - uses this scoped model's lightweight LazyIMT accumulator boundary. + gaps rather than basic body expressibility: Poseidon, Permit2, Groth16, and + host-level UUPS proxy behavior remain as explicit boundaries. `_executeWithdrawal(_transactions[i], bool)` is routed through an internal helper call. The deploy-time BN254 precompile probe in `initialize` is wired through the 0x06/0x07/0x08 precompile ECMs and the multi-result ECM binder. @@ -106,11 +105,9 @@ abstraction_notes: > - `deposit`, `transfer`, `withdraw`, and `emergencyWithdraw` bodies are wired, but still carry the fidelity gaps listed above. unsupported_feature_codes: - - lazy_imt_insert_body_assumed - uups_proxy_storage_rotation_not_modeled - poseidon_assumed_axiom - permit2_assumed_axiom - - lazy_imt_assumed_axiom - groth16_verifier_assumed_axiom notes: > This case replaces the previous `backlog/unlink_xyz/placeholder` entry, which