Uniswap V2 pair.

Identity

Why the theorems reach every pair.

The factory’s code — 13,859 bytes, identical from three providers and equal to the published build of the v1.0.0 sources — embeds the pair’s 11,636-byte creation code and has a single CREATE2. That creation code hashes to the init-code hash Uniswap publishes, 0x96e8…845f, and its constructor returns bytes 261 to 11,553, counting from zero, as a literal: exactly the lifted runtime. No executable code of the factory, the creation code or the runtime contains SELFDESTRUCT, CALLCODE or DELEGATECALL.

So every pair the factory creates holds the lifted runtime. This binding is by inspection of the factory’s source and bytes at one block, not a theorem about its executions; as spot checks, eleven pairs from across the factory’s list — the first, second, third and last among them — hold code with the runtime’s hash.

The method’s hard part

Other contracts’ answers, as inputs.

A pair learns its balances only from each token’s balanceOf, and whether a protocol fee is due only from the factory’s feeTo. A token can answer anything, and a callee can revert or consume all the gas it is given, so no contract that calls others is correct, or live, for every callee. The question is where the premises about callees go.

Blanc keeps two layers apart. In the first, answers are inputs. The model the bytes refine is a transcription of the v1.0.1 sources that consumes a transcript of the answers a call received. The refinement theorems say the bytes consume the model’s entry over exactly the answers their own run observed. Every step of a history replay is authenticated: its entry is the one its own frame decoded, and its transcript is consumed positionally — each answer tied to the actual call that returned it, with its reply and the nested calls into the pair beneath it, each admitted the same way in turn. The replay, ledger, oracle and refinement theorems live at this layer and take no premise about any token or the factory.

In the second layer, the economic statements take a named premise about the answers — but only the answers of the steps of the history at hand. That is a checkable property of a concrete history, not an assumption about every token that might ever exist.

Safety, after any history

The history theorem.

After any configured history from a checkpoint at which the bytes are installed and the storage represents a model state, the code is intact and the storage represents the state reached by replaying, in order, exactly the outermost committed non-static calls to the pair, each against the answers its own run observed, at the positions where it observed them. Calls that reach the pair from inside one of these — through a token transfer or the flash-swap callback — are replayed inside the step that contains them. An equation places every committed non-static call to the pair in exactly one step, so no step is invented and none is lost.

Representation includes complete support: every nonzero word of the pair’s storage lies at a fixed slot or at the row of a tracked key. The only hash premise is trace-local. From the deployment checkpoint the statement reads:

theorem pair_history_initialized {pair : Adr} {cfg : ChainConfig} {checkpoint future : BlockChain}
    {factory token0 token1 : Adr} {domain : B256}
    (trace : ConfiguredHistoryTrace cfg checkpoint future)
    (installed : some (checkpoint.state.getCode pair).toList = pairSem.image)
    (initial : InitializedCheckpoint (checkpoint.state.getStor pair) factory domain token0 token1)
    (fresh : WriterFreshKeys (fun _ => False) (pairHistoryTouchedKeys pair trace)) :
    some (future.state.getCode pair).toList = pairSem.image ∧
    ∃ steps : List PairStep,
      steps.flatMap (fun s => pairSubtreeFrames pair s.frame) = committedPairFrames pair trace ∧
      (∀ s ∈ steps, s.AuthenticWith PairEntryAuth pair) ∧
      ∃ (finish : State) (K' : WriterKey → Prop),
        PairObservedReplayWith PairAdmittedConsumes (initializedState factory domain token0 token1) steps finish ∧
        SourceReplay (initializedState factory domain token0 token1)
          (steps.map PairStep.source) finish ∧
        runSourceInvocations (initializedState factory domain token0 token1)
          (steps.map PairStep.source) = some finish ∧
        (∀ k, K' k → k ∈ pairHistoryTouchedKeys pair trace) ∧
        WriterRep K' (future.state.getStor pair) finish

The general form, pair_history_committed, starts from any represented state, so it applies wherever a pair’s storage can be shown to represent its model.

What the replay gives

Ledger, oracle, and the value of a share.

• The LP ledger balances. If the model’s LP balances sum to the total supply at the checkpoint, they still do after any history, every protocol-fee mint included; from the deployment checkpoint this is proved, not assumed. It is a statement about the model’s ledger, whose rows are the tracked keys. pair_history_ledger · pair_history_ledger_from_checkpoint
• The oracle obeys its law. Each price accumulator is its checkpoint value plus the sum, modulo 2²⁵⁶, of every committed update’s increment, ⌊r₁·2¹¹²/r₀⌋·Δt or symmetrically when Δt and both reserves are nonzero, and zero otherwise, with Δt the elapsed time modulo 2³² by the steps’ own block timestamps. Both wrap-arounds are part of the statement. pair_history_oracle
• A share’s value falls only through the protocol fee. If the factory answered feeTo = 0 to the history’s mints and burns, and the token answers satisfy NoShrink, every committed step that starts with positive supply T and reserves r₀, r₁ ends with r₀·r₁·T′² ≤ r₀′·r₁′·T²: the geometric mean of the reserves per LP token, √(r₀·r₁)/T, never decreases. With the fee on, under NoShrink alone, the bound becomes r₀·r₁·T′² ≤ r₀′·r₁′·(T + F)², where F is the step’s exact fee mint, so dilution is bounded by the fee mint alone — the form that matters on mainnet, where the factory has named a fee recipient since 27 December 2025. pair_history_feeOff_product · pair_history_feeOn_product
• The minimum liquidity stays locked. From a checkpoint satisfying the ledger and a supply floor — a supply of zero, or at least 1,000 LP tokens at address 0, which has granted no allowance — for a pair not at address 0, the floor holds after every committed step, provided no step, and no nested call to the pair inside one, has address 0 as its caller; every step that starts with positive supply ends with at least 1,000, and the fee-off bound then holds as a ratio over the rationals. Deployment establishes both premises. pair_history_minimum_liquidity · pair_history_feeOff_ratio

The value measured is not market value. Moving the reserves from (100, 100) to (50, 201) at a supply of 100 raises √(r₀·r₁)/T from 1 to about 1.0025, yet at prices of 4 and 1 the new reserves are worth 401, against 500 for the old ones held outside the pool.

Refinement, frame by frame

Every frame is a step of the model.

From any storage that represents a model state, given trace-local freshness of the rows it touches, a successful frame at each of the runtime’s 27 entry points consumes the model’s entry exactly, over the answers its own run observed, with the model’s storage, logs and return bytes. swap is covered in all six successful shapes — each optimistic transfer present exactly when its amount is nonzero, the callback present exactly when its data is nonempty — and no writer succeeds in a static frame. The model’s laws thereby become laws of the bytes:

• the first mint prices ⌊√(a₀·a₁)⌋ − 1,000, locks 1,000 at address 0 and credits the recipient the rest, and the bytecode’s own Babylonian square-root loop is walked exactly and equals Nat.sqrt on its full domain;
• a later mint issues min(⌊a₀·T/r₀⌋, ⌊a₁·T/r₁⌋), with T the supply after the fee mint;
• a burn pays and returns ⌊L·bᵢ/T⌋ of each token, by exactly two transfer requests;
• a swap succeeds exactly when the canonical conditions hold — some output positive, outputs below the reserves, to neither token, balances within uint112, some input positive, and the fee-adjusted product check — and then stores exactly those balances as reserves.

Because the frame theorems tie every successful call to the model and the liveness theorems tie every accepted state-changing call to a successful execution, no model that departed from the bytes on a successful call could have been proved to match them. Whether the model reads as the sources do is a separate question, which a reader settles by comparing the two; the model register carries a line-by-line correspondence table.

Constructed executions

Every state-changing function, live.

After any configured history, each of the ten state-changing entry points executes from program counter 0 whenever the model accepts the call at the replayed state. The cost is closed: fixed charges, the access charges of the actual slots and accounts, and the gas forwarded to each callee, whose own consumption enters only through the callee premise.

Every row also takes trace-local freshness of the storage rows the new call touches, and skim additionally of the rows the pair’s own frames decode inside its first transfer; that this transfer leaves the lock-guarded fields unchanged is derived, not assumed. The callee premises cannot be dropped: if the first token, or the callback recipient, holds the reverting code PUSH0 PUSH0 REVERT, no run of sync, skim, mint, or a swap that pays out the first token or calls back succeeds, whatever the gas.

An empirical test, outside the proof

Against the chain: 542 receipts.

The frame theorem for approve, with the protocol’s intrinsic gas and refund added, predicts the receipt of a top-level approve transaction to any pair:

Through the 1,444,195 Approval events of the 30,000 blocks ending at block 26,141,229, 542 transactions called approve directly on an account holding the lifted runtime: 476 different pairs, the USDC/WETH exhibit among them five times, from 451 senders, 57 of them accounts with EIP-7702 delegation code, which approve never executes.

The pair has no transaction-level theorem, so this tests the frame theorem’s cost together with the protocol’s transaction rules. With WETH9’s 3,748, it makes 4,290 receipts from the output of two compilers, every one equal to its prediction.

Where a history can start

Deployment and initialization.

Under every covered fork, the factory’s CREATE2 step with the recorded creation code, given an empty target and at least 2,400,000 gas forwarded, installs the certified runtime with the factory recorded as factory and the EIP-712 domain separator over the chain and the new address. Every successful initialize from the factory then leaves exactly the initialized checkpoint of the history theorem — and such a run exists, at a closed cost, so the checkpoint is reached rather than assumed. No hash premise is needed. For the exhibit, the kernel evaluates the CREATE2 address from the factory, the salt keccak(USDC ‖ WETH) and the creation code, and obtains 0xB4e1…C9Dc.

pair_create2_initialize_live · pairAddress_eq. The factory’s own bytecode is not lifted, so that it issues the initialize call is a premise; the run is then constructed.

Statements that can fail

Premises that bite.

A premise never needed, or a statement that would survive a change to the code, says less than it seems. Kernel-checked controls show these do not:

• Without NoShrink, a reachable sync accepts a token answer below the stored reserve and the share-value inequality fails.
• A mint that rounds up breaks the fee-off share-value inequality on a state it reaches; a fee constant other than 997, or a burn that rounds toward the user, gives a different accepted run.
• The oracle law needs the uint32 wrap: a reached update past 2³² seconds refutes the law without it.
• The uint112 guard is load-bearing, and every successful raw swap observes balances below 2¹¹².
• A duplicated key breaks the footprint sum, and an allowance slot aliasing a tracked balance slot breaks raw ledger conservation.
• A salt or init-code hash one bit off gives a different deployment address.

Stated, so it is not inferred

Not claimed.

• That any real token satisfies NoShrink, that a factory answers feeTo = 0, or that the reserves are matched by real token holdings.
• That any price, the time-weighted oracle, or the pool’s economics are fair or safe.
• Any composition of the pair with a token or with the factory; at the exhibit, WETH’s answers are inputs constrained by NoShrink, not discharged from Blanc’s WETH9 results.
• That a live pair’s storage represents its model today: per pair, that needs the fixed slots and every mapping row recovered from its logs and permit calls checked, and a complete enumeration of its storage showing nothing else is stored.
• Transaction-level liveness; unforgeability of permit signatures, whose recovered address is an input; failed calls beyond the controls above.

The claim map’s Uniswap section lists every theorem with its premises, file and line.

Context

Earlier work.

In 2020, dapp.org’s audit proved K reachability claims for each method of the pair and factory, against bytecode built from the v1.0.0 sources whose published build is byte-identical to the deployed runtime, with an exact symbolic gas cost for success; it made no claim about invariants across calls and assumed tokens matching the pair’s own. EquiVM’s repository has since proved refinement for a local build of the same sources, 8,833 bytes that are not the deployed runtime. To our knowledge, no earlier machine-checked result states the pair’s properties across calls of its bytecode.