Skip to content

Adunka/fraudproof

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

fraudproof

fraudproof — an optimistic rollup dispute, bisected to the fraudulent step

ci python theorems bisection proof

An optimistic rollup with fraud proofs. A sequencer publishes state roots and is believed by default; if it ever lies, anyone can prove it on-chain with a proof the size of two Merkle paths, and the liar loses its bond. Small disputes settle in a single step; large ones settle by a bisection game, so even a batch too big to re-execute on-chain is challengeable one halving at a time. Security comes from making fraud more expensive than honesty - not from trust.

python3 scripts/demo.py     # watch a thief get caught and slashed
make test                   # the two theorems, proven across the matrix

The thesis

An optimistic rollup is a bet on asymmetry. The sequencer publishes a new state root and asserts "I applied these transactions honestly." Nobody verifies by default - that is what makes it cheap. But if the assertion is false, any watcher can prove it in a single step, and the sequencer's bond is slashed. Honesty is not enforced by trust. It is made cheaper than fraud, and the arithmetic does the rest.

Three of my other projects are about one honest machine keeping careful books. This one is different: it is about two parties who do not trust each other, a dispute between them, and a referee - the L1 contract - that decides who is right by re-running exactly one transaction. That is the mechanism at the heart of every optimistic rollup securing billions today, built here small enough to read in an afternoon and rigorous enough to prove.

Watch it work

  now a dishonest sequencer tries to forge a state root
    eve proposes   eeeeeeeeeeeeeeee...   bond 1000

  the watcher recomputes and finds the lie
    fraud at step 1, proof is 516 hashes (not the whole state)

  the L1 re-runs that one transaction and judges
    verdict: FRAUD PROVEN
    eve's bond, slashed to the watcher: 1000

See a dispute unfold

docs/dispute.html is a self-contained, interactive record of one real dispute: eight transfers, a state root after each, and a fraud hidden in the middle. Press Open the dispute and watch the bisection game halve the range round by round until it pins the lie to a single step - then the L1 re-runs that one transaction and the bond is slashed. Every root, transaction and round on the page is real output from the engine, embedded by scripts/build_dispute_viz.py; the picture cannot drift from the protocol because it is generated from it.

The batch lifecycle

A proposed root is optimistically assumed correct. It finalizes only if its challenge window closes unchallenged; a single valid fraud proof rejects it and slashes the bond.

stateDiagram-v2
    [*] --> proposed: sequencer posts a root + bond
    proposed --> finalized: challenge window elapses, unchallenged
    proposed --> rejected: a valid fraud proof lands
    rejected --> [*]: bond slashed to the challenger
    finalized --> [*]: post_root becomes canonical
    note right of proposed
        believed by default -
        no one verifies unless
        they suspect a lie
    end note
Loading

How a fraud proof works

The sequencer commits to a root after every transaction, not just the endpoints. So a dishonest batch has a first step where its claimed root stops following from the rules - and the dispute collapses to that one step.

flowchart LR
    r0["root₀"] -->|tx₀| r1["root₁"]
    r1 -->|tx₁| r2["root₂ ✗ claimed"]
    r2 -->|tx₂| r3["root₃"]
    style r2 fill:#3a1212,stroke:#e25a5a,color:#fff
    classDef ok fill:#12261a,stroke:#3ef07c,color:#fff
    class r0,r1,r3 ok
Loading

The challenger points at step 1 and hands the L1 a witness: the two accounts tx₁ touches, their Merkle proofs against root₁, the transaction, and the claimed root₂. The L1 runs the same state transition function the sequencer was obligated to run, recomputes the honest root₂ from the witness alone, and compares. Different → fraud proven, bond slashed.

The two theorems

The whole design rests on two claims, and both are tests, because a claim about soundness is worth exactly what its counterexample search is worth.

theorem test
completeness an honest batch cannot be disproven - the prover raises HonestBatch and no fraud proof exists test_honest_*
soundness a dishonest batch is always disprovable, wherever the lie is hidden test_corrupting_any_step_is_caught

The bisection game

Single-step proving has a hidden assumption: that the L1 can re-execute the disputed step. For a transfer that is trivially true - but the reason rollups exist is to run computation too large for L1. A batch might be a million steps, and the L1 cannot replay a million steps to find the one that was faked.

So it doesn't. It makes the two parties bisect the batch. The challenger says "we disagree about the state somewhere in this range." The defender reveals the state root at the midpoint - a value it already committed to. The challenger points at the half it still disagrees with. The range halves. Repeat.

flowchart TD
    A["dispute [0, 15]"] -->|"reveal step 7 · disagree in second half"| B["dispute [8, 15]"]
    B -->|"reveal step 11 · disagree in first half"| C["dispute [8, 11]"]
    C -->|"reveal step 9 · disagree in second half"| D["dispute [10, 11]"]
    D -->|"reveal step 10 · disagree in second half"| E["single step 11"]
    E --> F["single-step verifier · slash"]
    style E fill:#12261a,stroke:#3ef07c,color:#fff
    style F fill:#3a1212,stroke:#e25a5a,color:#fff
Loading

After ⌈log₂N⌉ rounds the range is one step: an agreed pre-root, a disputed post-root, one transaction. That is exactly the input the single-step verifier already judges. A million-step batch is disputed in twenty rounds, each round a single hash comparison, and the L1 never re-executes the batch.

  round 1:  reveal step  5  challenger keeps the second half  -> [ 6, 11]
            ···············███████████████··········
  round 2:  reveal step  8  challenger keeps the second half  -> [ 9, 11]
            ·······················███████··········
  round 3:  reveal step 10  challenger keeps the second half  -> [11, 11]
            ····························██··········

  bisected to a single step: 11 — challenger won

The game is built on top of the single-step machinery, not instead of it: bisection narrows, the existing verifier convicts. Two clean layers. Run python3 scripts/bisection_demo.py to watch a range collapse live.

Why bisection needs a monotone dispute range

Binary search finds a boundary, and a lie is a boundary: the challenger agrees with the batch up to some step and disagrees from there on. But that is only true if disagreement, once it starts, persists - and an isolated mid-batch lie that self-heals by the final root breaks the assumption. The sequencer could commit a false root at step 5 while every root from 6 onward is honest again.

The fix is to anchor the game on the challenger's first point of divergence, not on the batch's post-root. Over the range from the shared pre-root to that first bad root, the two sides provably agree at the low end and disagree at the high end - a monotone boundary - and bisection is exact. This is the kind of edge case that separates a protocol from a demo, and test_lie_at_every_position plants a lie at every index precisely to pin it.

Why one shared STF is the linchpin

There is exactly one implementation of the state transition function, and both the sequencer and the L1 run it. The sequencer runs it to build a batch; the L1 runs it to judge a dispute. This is not code reuse for tidiness - it is what makes a fraud proof unanswerable.

If the L1 judged disputes with a reimplementation of the rules, a sequencer could exploit any edge case where the two differ: behave one way, be judged by another. With a single STF there is no gap to exploit. "Correct" is defined by one function, the sequencer is obligated to run that function, and the L1 checks by running the very same one. The sequencer cannot argue about the rules, because the rules are the code that will convict it.

Why the proof is tiny

A fraud proof does not contain the state. It contains one transaction and the two accounts that transaction touches, each with its Merkle path to the root - about 2·log₂(N) hashes for N accounts. For the 256-bit tree here that is a fixed ceiling of a few hundred hashes no matter whether the rollup has ten accounts or ten million.

This is the economic argument made concrete. Because judging a dispute costs the L1 only one STF step and O(log N) hashing - never a full state load - anyone can afford to challenge a liar. Cheap verification is what lets "any watcher" be a real threat, and a real threat is what keeps the sequencer honest. Compactness is not an optimization here; it is the security model.

Proving theft from an empty account

The subtle attack is not a corrupted arithmetic result - it is a sequencer spending coins that never existed. Handling it needs a non-inclusion proof: the ability to prove an account is empty.

When a sequencer claims a transfer out of an account, the fraud proof carries that account's pre-state. If the account is empty, the honest STF rejects the transaction for insufficient balance, so the honest post-root equals the pre-root - and the sequencer's claim that value moved is provably false. The Sparse Merkle Tree proves absence with exactly the same shape of proof it uses for presence, which is why test_steal_from_thin_air_is_caught needs no special machinery. Proving a thing is not there is the load-bearing half of the tree.

Run

make test        # smt, stf, fraud theorems, contract lifecycle
make fuzz        # random batches, half honest half corrupted, across seeds
make demo        # the narrated slashing
	python3 scripts/bisection_demo.py   # watch a 16-step dispute halve to one

The Keccak-256 here is written from scratch (original padding - the Ethereum variant, not NIST SHA3) so the project has no hashing dependency and no chance of the sha3/keccak mix-up that silently corrupts every hash. If a native Keccak backend happens to be installed, keccak.py will use it - but only after checking it agrees with the reference on a vector that tells Keccak and SHA3 apart. Correct everywhere by default, fast where the wheel exists, and never trusting a backend it hasn't verified.

Architecture

optimism/
  state/
    smt.py         sparse merkle tree: inclusion AND non-inclusion proofs
    account.py     balance + nonce, deterministic 32-byte leaf
    keccak.py      the ethereum keccak-256 (original padding), from scratch
  rollup/
    stf.py         THE state transition function - shared by sequencer and L1
    sequencer.py   applies the STF, publishes batches (can be told to cheat)
    batch.py       pre_root, per-step roots, post_root, witnesses
  fraud/
    prover.py      finds the first dishonest step, packages a compact proof
    verifier.py    the L1's judgement: local Merkle root recomputation
    bisection.py   the multi-round dispute game over a whole batch
    players.py     an honest challenger that drives the game to a verdict
  l1/
    contract.py    stores roots, holds the bond, judges, slashes, finalizes

What is deliberately out of scope

The fraud proof here is complete: a single-round settlement wrapped in a multi-round bisection game, so even a batch far too large for the L1 to re-execute is disputable one halving at a time - exactly the design production systems like Arbitrum use. What is left is the surrounding machinery, not the core mechanism:

  • A real EVM. The STF is signed transfers with nonces, which is enough to exhibit every part of the fraud-proof and bisection machinery. A richer STF is more code around the same skeleton: read some accounts, check some rules, write some accounts, deterministically.
  • Real ECDSA. A deterministic mock signature stands in - the mechanism does not depend on how a signature is checked, only that it is, deterministically.
  • A data-availability layer. The batch data is assumed available; DA is an orthogonal problem with its own literature.

The one thing this project does, it proves: a fraud proof that an honest sequencer cannot fear and a dishonest one cannot escape, that scales to computations nobody can afford to recompute.

License

MIT.

About

An optimistic rollup with fraud proofs and a bisection dispute game — a sparse Merkle state, one shared state transition function, and an L1 that convicts a lying sequencer by re-running a single transaction. Includes an interactive dispute visualization.

Topics

Resources

License

Stars

0 stars

Watchers

0 watching

Forks

Releases

No releases published

Packages

 
 
 

Contributors