Lido’s CircuitBreaker.

What is stored

The registry, and why it needs hash premises.

The registry is a Solidity array of protected contracts with three mappings: from a contract to its pauser, from a contract to its index in the array, and from a pauser to the number of contracts it guards. Mappings live at Keccak-hashed storage slots, so a proof that they stay consistent must know their slots do not collide — with each other, with the array, or with the fixed slots. Blanc adds no axiom about Keccak-256; it states the separation it uses, and the two tiers state it in two different ways.

Safety, after any history

The history tier: consistency, under universal premises.

After any configured history from a checkpoint holding the code and an empty registry, there is a registry witness of the final storage: assignment and index slots are nonzero exactly for registered contracts and agree with the array; every pauser’s count equals its number of assignments; the zero pauser’s count is zero; and the live pausers’ counts sum to the array’s length (lido_history_l1_l3). And every committed, non-static registerPauser(t, 0) — including one re-entered from inside pause’s external call — removes t with the correct swap-and-pop repair of the array (lido_history_l2_committed).

This tier assumes, at every frame, separation conditions on the registry’s hashed slots that quantify over all 2¹⁶⁰ addresses. It is the one family in the corpus whose headline history results still need them. Under a random-function model of Keccak, the chance that such a premise fails is about q·2⁻⁹⁴ per frame for q written slots — four key families, each ranging over 2¹⁶⁰ addresses or indices, among 2²⁵⁶ slots — but that estimate is a heuristic: no reduction or bound is proved.

Premises the kernel decides

The finite tier: a universal premise traded for a computation.

Its observation, RegistryOn storage entries probes, says that an explicit list of entries is valid and that the array and, for each address in a caller-supplied list of probes, the assignment, index and count words agree with it. A decision procedure, checkRegistryOn, decides it. A successful execution of registerPauser(target, p) for an existing target and a nonzero new pauser takes storage on which the check holds to storage on which it holds for the updated entries — and every separation premise it takes is itself a decidable check on concrete key lists.

theorem registerPauser_nonzero_finite {sevm : Sevm} {pre post : Devm}
    {entries : List LidoCircuitBreaker.Entry} {probes : List B256}
    {index : Nat} {oldPauser : B256}
    (hfork : CoveredFork sevm.benvStat.fork)
    (hinstalled : Devm.getCode pre sevm.currentTarget = code)
    (hcode : sevm.code = Devm.getCode pre sevm.currentTarget)
    (hfresh : Exec.FreshEntry sevm pre)
    (hsig : Sevm.dataWord sevm 0 >>> 224 = selector "registerPauser" [.address, .address])
    (hpre : checkRegistryOn (solRegistryStorage (Devm.getStor pre sevm.currentTarget))
      entries probes = true)
    (hcover : checkLiveCovered entries probes = true)
    (hclosure : Sevm.dataWord sevm 4 ∈ probes ∧ oldPauser ∈ probes ∧
      Sevm.dataWord sevm 36 ∈ probes)
    (hnew : Sevm.dataWord sevm 36 ≠ 0)
    (hfind : findEntry entries (Sevm.dataWord sevm 4) = some (index, oldPauser))
    (hfaithful : SlotFootprint.checkFaithfulOn solKey (registryQueries probes entries.length)
      ((nonzeroWrites entries (Sevm.dataWord sevm 4) (Sevm.dataWord sevm 36) oldPauser).map
        Prod.fst) = true)
    (hapart : SlotFootprint.checkApartOn solKey (registryQueries probes entries.length)
      [mapSlot oldPauser 2, mapSlot (Sevm.dataWord sevm 36) 2] = true)
    (execution : Exec 0 sevm pre (.ok post)) :
    checkRegistryOn (solRegistryStorage (Devm.getStor post sevm.currentTarget))
      (setEntryAt index (Sevm.dataWord sevm 4, Sevm.dataWord sevm 36) entries) probes = true ∧
    checkLiveCovered
      (setEntryAt index (Sevm.dataWord sevm 4, Sevm.dataWord sevm 36) entries) probes = true

Every hypothesis after the call shape is decidable — the separation premises are literally Boolean checks on finite key lists — so for a concrete state the kernel closes them by evaluation, Keccak included. The premises are not idle: a constructed state with one entry and four probes satisfies all of them at once (exampleApplicable). The price is scope: the finite tier says nothing about addresses outside the probes, about inserting or removing targets, or about histories.

The seventh question

The live registry passes the check.

All of the CircuitBreaker’s use lies in forks Jaune covers. At block 26,141,229, 29 explicit probes over 107 storage slots, on which three providers agree, satisfy every field of the decidable RegistryOn check for the 19 live entries — which replaying all 23 PauserSet events since deployment reproduces. The probes cover finitely many addresses, no state root authenticates the reads, and the check was computed outside the kernel; a kernel-checked version of it has not been built.

Where a history can start

Deployment.

Under every covered fork, the recorded creation input, run as a CREATE from the recorded deployer at nonce 0 with 1,000,000 gas, installs the certified runtime at the mainnet address and leaves exactly the constructor’s storage: a pause duration of 1,814,400 seconds (21 days) and a heartbeat interval of 31,536,000 (365 days) (lido_deploy_covered). The finite deployment theorem shows that this storage satisfies RegistryOn [] probes for every probe list passing one decidable check (lido_create_finite_init); the history tier’s empty-registry checkpoint is established under two bounded hash premises. Because the contract was created after BPO2 activated, the historical deployment ran under a covered fork — though, like every deployment here, the theorem is a modeled execution, not a proof of inclusion.

Stated, so it is not inferred

Not claimed.

• That any target is actually paused, or that pausing succeeds: there is no liveness result at any level, in either tier.
• That authorization is complete, or anything about setter effects and events.
• At the history tier, static committed frames and frames under a rolled-back ancestor.
• At the finite tier, any address outside the probe list, target insertion or removal, and any history.

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

Context

Earlier work, and Blanc’s own CircuitBreaker.

Before deployment, Cyfrin checked 41 properties of a pre-deployment revision of the source with the Certora Prover 8.8.1, verifying 38 and reporting three cases of registerPauser as known limitations correct by manual analysis, and matched a local build of the deployed revision to the deployed bytecode. We found no machine-checked verification of the deployed bytecode.

Blanc also contains a reimplementation of the CircuitBreaker in its own language, whose registry integrity is proved for every state reachable along a configured chain, with no premise about the code at any other address. More on Blanc’s CircuitBreaker.