zkSync Era IMT Linked-List Order
Following successor links from the zero sentinel visits every occupied leaf exactly once, in strictly increasing value order.
zkSync Era records atomic interop commitments in an indexed Merkle tree. Cheap non-inclusion arguments later walk a sorted linked list of leaf values. The physical array is append order, not sorted order.
We modeled IndexedMerkleTree setup and insert at Matter Labs commit e5f6e004a09f667c6109e44c4fe1f81658127631. The wrapper L2InteropCommitmentTree gates the appender, delegates list mutation to the engine, then reports the leaf as an L2-to-L1 log and emits RootUpdated. This proof models only the engine list-state fragment.
Why It Matters
Each zkSync chain uses this tree as the record of atomic-flow commitments. Finality needs to show that a commitment is present. A timeout needs to show that it was absent before the deadline so the flow can be refunded. The indexed links make that absence argument cheap: they identify the two neighboring values between which the missing commitment would have appeared.
This only works if every insert preserves the sorted successor list. Physical indices still follow append order: inserting 10, then 20, then 15 stores them at indices 1, 2, and 3, while nextIndex traversal remains 0 to 10 to 15 to 20. A wrong link could make the list skip a stored commitment and undermine the list-level basis for a later absence argument.
The proof shows that setup from fresh-zero storage establishes the ordered list and its value-to-index relation, and that every successful insert preserves both. This is not a claim that the Merkle root authenticates the list.
How This Was Modeled and Proven
We recreated the list-state fragment of IndexedMerkleTree in Lean: sentinel setup, the fuelled predecessor walk, and the insert write order. Specs define IMTOrder as sentinel value 0 together with one covering ordered chain: head 0, length equal to leafNumber, no duplicate indices, coherent nextIndex and nextValue hops, occupancy coverage, strictly increasing leaf values, and a tail with next index and next value 0. Specs combine this with agreement between occupied leaves and valueToIndex as IMTValidState.
Lean checks that setup on fresh-zero storage establishes that valid state. For insert, map consistency turns the modeled duplicate guard into genuine value absence. Lean then checks that every successful insert preserves both the ordered chain and map consistency. No separate value-absence premise is needed.
Reproduce with lake build Benchmark.Cases.ZkSync.InteropCommitmentTreeOrder.Proofs. The proofs contain no sorry and no case-specific axioms.
Scope
Included: setup and insert list writes, Solidity require names, the predecessor walk, addPanic on leafNumber, and the valueToIndex map as storage. The valid-state theorem proves that every occupied non-sentinel leaf agrees with that map, alongside the IMTOrder chain.
Excluded: After the list splice, Solidity also updates the FullMerkle hash tree. That branch is triggered by every successful insert and would authenticate roots and paths. It is absent from the theorem, so the public claim is list-state only. hashLeaf, _nodes, _zeros, verifyInclusion, Merkle paths, events, and gas are not modeled. verifyNonInclusion is a separate read that exhibits a low-nullifier bracket plus a Merkle path. Those branches need their own model. They are not assumed correct here.
Timeout settlement: Atomic-interop timeout is triggered when a committed flow leg must be refunded because its commitValue was never present in this chain's IMT at a later batch snapshot. The extra behavior is a non-membership proof against the bootloader-snapshotted root, which lets the refund proceed without an L1 coordinator. This theorem does not model that settlement path, the snapshots, or the Merkle check they use.
Physical append order: Array indices record insertion order. Linked-list value order is the successor walk from sentinel 0. The theorem never claims leaves[i].value < leaves[i+1].value.
Storage model: Abstract semantic channels, not EVM slots or packed structs. There is no mechanized source-to-model storage relation and no bytecode refinement.
Walk helper: The Solidity while is a fuelled recursive helper. Fuel is the current leaf count. Under IMTOrder the chain is finite and values strictly increase, so the walk terminates before fuel runs out.
Proof artifacts
- Contract.lean is the list-state model.
- Specs.lean defines
IMTOrderandIMTValidState. - Proofs.lean contains the setup and insert preservation proofs. The supporting
insert_leaf_frametheorem is in the same file. - Case directory and pull request 176.
| Function | Theorem | Status |
|---|---|---|
| setup | setup_establishes_valid_state | Proven |
| insert | insert_preserves_order | Proven |
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout 36d334beb69c8baa182dd3ff91bee39427cc2ac1 lake build Benchmark.Cases.ZkSync.InteropCommitmentTreeOrder.Proofs
Hypotheses
The proof applies under the conditions below.
fresh deployment storagesetup starts from zeroed leaf records and valueToIndex cellsInitialization theorem premise. EVM deployment storage defaults to zero
Setup establishes the valid state from fresh-zero storage. The theorem does not claim to repair arbitrary dirty pre-setup storage.
valid pre-statethe ordered covering chain agrees with valueToIndexPreservation theorem premise. IMTValidState in Specs.lean
This is the usual inductive invariant: setup establishes it, and every successful modeled insert preserves it.
successful insertionthe modeled Solidity insert returns successfullyRuntime precondition. IndexedMerkleTree.insert guards
The call passes the source guards, including initialization, nonzero value, duplicate-map, low-leaf, and arithmetic checks. Reverting calls produce no post-state for this theorem.