Blanc/implementations/ports
TriggerableWithdrawalsGateway.
The port of the TriggerableWithdrawalsGateway that Lido deployed — directly, not behind a proxy — at 0xDC00…037B: the contract through which validator exits are triggered, rate-limited by a refilling frame quota, and at the pinned block the account the deployed CircuitBreaker holds PAUSE_ROLE on. It was chosen for exactly that reason. The CircuitBreaker port proves that a pause spends its authorization and calls out; this port proves what the callee does with the call — and a new stratum of the repository joins the two.
It was once the portfolio’s honest loss — nearly twice the reference’s size and dearer on 48 of 51 named gas paths, every row published as a priced cost. It no longer is: after re-optimization the runtime is 34 bytes smaller than the reference and every one of the 51 named paths is a strict Blanc win, a ledger the gate now refuses to let regress. A port never claims byte identity — PORTING.md governs what is claimed and what never is — and this one still claims less than most: three accepted behavioral deviations, each with a stance, none defended as an improvement, and two more repaired rather than waived.
Fig. 1 — two gates, ellipses marking elision: the differential matrix beside the locked Solidity reference, whose nine registered-deviation rows are compared as exactly as the sixty-two agreements, shown as the exact verdict line the committed gate registry requires for a pass; and the layering gate, verbatim from a run on 2026-09-25 UTC, classifying a composition stratum strictly downstream of every contract family. The differential line continues “… 46 reference CALL/STATICCALL traces; 10 positive artifact checks; 8 performance control/mutant checks; 9 live channel/identity/semantic falsifiers.”
What the port proves
A pause target that answers for itself.
The gateway family owns three things. The pause face — pauseFor, pauseUntil, resume, with the all-ones sentinel for an infinite pause. The role gate over all of it. And an account-level protocol, PinnedPauseTarget, stated in target-neutral vocabulary and discharged by the exact compiled runtime in four clauses: a successful pauseFor stores the shared projection, sentinel included; the isPaused query is truthful; the pause route writes nothing to the CircuitBreaker’s own cells; and the protected surface reverts while paused. The third clause is the one the CircuitBreaker page keeps loud as an assumption — PauseSuccessNoninterference — and here, for this target, it is a theorem.
For every deployment parameter set, every pair of distinct CircuitBreaker and gateway accounts, and every list of CircuitBreaker cells, the exact compiled gateway runtime satisfies the four-clause pinned-pause-target bundle — assembled only from source-derived walks and actual retained-message inversion, with no structure of assumed witnesses.
structure PinnedPauseTarget (circuitBreaker target : Adr) (program : Prog) (pauseCalldata : B256 → Bytes) (queryCalldata : Bytes) (pausedUntil : Adr → Stor → B256) (circuitBreakerCells : List B256) (protectedSurface : List B256) : Prop where pauseFor_effect : … -- clause (i): the shared projection, sentinel preserved isPaused_truthful : … -- clause (ii): canonical true iff paused at entry … -- clauses (iii), (iv): the CircuitBreaker's cells untouched; the protected surface refuses while paused
Read the shape — the bundle never exposes or unfolds program; its fields say only what the account at target does on exact settled inbound messages, and the paused projection is local to one account’s storage, so no unrelated change can alter its observation. Clause (i) is unconditional on the sentinel: pauseFor(2256 − 1) stores the sentinel and anything else stores timestamp + duration by checked addition — a disjunct, not a premise excluding the input. Clause (ii) is partial correctness for an exact static query: every clean settled answer preserves the projection and accepts canonical true exactly when the account was paused at entry; exceptional outcomes carry no liveness obligation.
pinnedPauseTarget -- the bundle above, over parameters, addresses, cells gateway_lidoPinnedPauseTarget -- …specialized to the CircuitBreaker's two cells: [countSlot pauser, heartbeatIntervalSlot] pauseForCalldata_eq · isPausedCalldata_eq -- exact ABI agreement between two encoders defined on independent evidence — a real check gatewayBoundaryExecutions_of_afterSet_ok -- direct installation supplies both program occurrences; no code-shape fact asked of the caller publicPause_gatewayPinnedTarget -- entry 3, for any successful run (below) gatewayPauseWorld_closedPremises -- every entry-3 premise but the run, discharged for one concrete world gatewayPauseWorld_closedPublicPause -- …and the run itself, constructed: a finite pause sentinelGatewayPauseWorld_closedPublicPause -- the same for the infinite sentinel
A role-gate failure returns the four-byte selector of a no-argument error rather than the reference’s Error(string) with account and role; a wrong-account renounceRole and an out-of-bounds getRoleMember empty-revert where the reference carries a reason or a Panic(0x32). Three accepted deviations, each filed as the declared local cost of one compact, proof-oriented error convention — not as an improvement. The runtime and gas ledger are strictly smaller and cheaper, but those wins do not erase a returndata difference.
Role membership first lived at flat keys with a fail-loud collision refusal, and one global array was filtered for enumeration — two published costs: a colliding state the reference admits could fail, and ordinals after a cross-role removal could differ. Both were public observations, so both were replaced: membership now lives at a nested-keccak slot from the full role and canonical account, with direct per-role length, index, and member slots and the reference’s own within-role swap-pop. The rows stay in the registry as repaired regression boundaries.
triggerFullWithdrawals decodes its request list, checks its role and the resumed state, consumes the frame quota, resolves the withdrawal vault through the immutable locator, forwards the requests with exactly the computed fee, notifies the staking router, and refunds the excess. The locator, vault, and router are mocks in the corpus and arbitrary callees in the theorems; they are not ported, and the claim says so rather than reaching for a system it did not build.
So the port is now simply better?
pushbackSmaller and cheaper on the ledger it names, and no more than that. The 51 cells are one declared boundary — direct EELS Prague message gas, constructor rows with code deposit — and every cell must stay a strict win or the gate fails; there is no disposition left to waive a regression. What the port claims is behavioral agreement on the published corpus, subject to three accepted deviations, plus the proved pause bundle. The earlier larger, dearer runtime was published as a priced cost while it stood; a portfolio that only reported the contracts it beat would be advertising, not reporting.
Does this say anything about Lido’s gateway on mainnet?
pushbackOnly as provenance. The deployed account at 0xDC00…037B was snapshotted through two independent providers at block 25,866,991: its code hash agrees with the official compiled runtime, it is unpaused, and the CircuitBreaker holds PAUSE_ROLE. That fixes which contract was ported. It is not a theorem about deployed Solidity, not a current-state claim, and no dependency contract is covered. Raw storage layout is a declared non-claim: logical pause, limit, membership, count, and locator behavior are compared; slot-for-slot compatibility is not.
The family’s 31 audited theorems sit in the repository-wide axiom audit, with twelve more in the composition stratum below, each pinned to its exact axiom set — all but one to the standard three. The differential manifest freezes the artifact identity and the proof certificate separately, because conformance repairs and a re-optimization moved the runtime after the first proofs landed — and the port’s claim documents keep that split explicit rather than calling either commit the identity of both.
Composition — two verified contracts at once
A pause that leaves its target really paused.
The CircuitBreaker port stops, deliberately, at the boundary of its own frame: a target’s canonical true is evidence the target reported success, never that it is paused. Closing that gap needs a theorem that names two contract families, and under the sibling rule such a theorem has no honest home in either. So the repository grew one place for it — Blanc/Composition/*, a stratum that may import any number of contract families, that no contract or shared module may import, and whose edges the layering gate checks with committed negative controls. Its first inhabitant is this theorem; the ERC-4626 vault’s pair with WETH has since joined it.
At a successful public pause(target) run of the production CircuitBreaker, with the exact compiled gateway runtime directly installed at a distinct, non-precompile target account, the committed-outcome family holds, the actual gateway pauseFor and isPaused executions occur, and the gateway is left paused at exactly pauseForProjection entryTime duration on the same successful final state — with the CircuitBreaker’s pauser-count and heartbeat-interval cells preserved by the gateway’s own proved noninterference.
theorem publicPause_gatewayPinnedTarget {sevm : Sevm} {pre final : Devm} {owner : Adr} (hfork : CoveredFork sevm.benvStat.fork) {target duration idx0 len0 last0 : B256} {img : Bytes} {dp : LidoTriggerableWithdrawalsGateway.DeployParams} {ex : Execution} (premises : PublicPauseEntryPremises sevm pre owner target duration idx0 len0 last0 img (gatewayCode dp)) (targetNe : target.toAdr ≠ sevm.currentTarget) (nonprecompile : sevm.benvStat.rules.isPrecomp target.toAdr = false) (publicRun : Prog.RunCompiledTo sevm pre (runtime officialParams) ex) (success : ex = .ok final) : PublicPausePinnedTargetConclusion sevm pre target duration (gatewayCode dp) (LidoTriggerableWithdrawalsGateway.runtime dp) LidoTriggerableWithdrawalsGateway.pausedUntil ex final
Read what is absent — no bundle premise (the composition supplies it), no program-occurrence premise (both MessageExecutesProgram witnesses and the CALL/STATICCALL linkage are derived from the walk’s own spawns), no accepted-query premise, no callback-noninterference premise, no paused-result premise, and no code-shape premise at all: non-delegation and a nonempty byte list follow from the compiler witness, nonzero installed width from the successful polarity — the CircuitBreaker’s own EXTCODESIZE guard reverts on zero — and nonzero depth from the successful suffix past the CALL. Four hostile review rounds rejected the candidate before the fourth’s bounded follow-ups accepted it, and each round removed a premise: from three low-level code facts, to one, to none, and finally the last implied hypothesis, depth ≠ 0, derived inside the crossing rather than asked of any caller. What remains is the frame’s fork: like every Blanc theorem, it holds for the covered forks Prague, Osaka, BPO1, and BPO2, and says nothing of Amsterdam.
So entry 3 — “a successful pause leaves the target really paused” — is closed?
pushbackFor two concrete worlds, yes, and the register says exactly that much. gatewayPauseWorld_closedPremises discharges every premise but the run for one world — the production CircuitBreaker at its account, the compiler’s own gateway output at the target, and only the explicit role, Registry, time, and storage configuration. gatewayPauseWorld_closedPublicPause then constructs the run: a successful production public pause, its real child CALL and warm query STATICCALL, callback noninterference, and the pinned-target conclusion, all from the walks, with no external run premise. sentinelGatewayPauseWorld_closedPublicPause does the same for an infinite pause, and a sibling shows that world storing the 2256 − 1 sentinel itself. These are two finite configured Prague worlds — not a universal liveness or gas theorem, not a statement about current mainnet code or roles, and not a second transaction after the pause.
Why is the ABI agreement a theorem rather than a definition?
pushbackBecause sharing one definition would have proved nothing. The CircuitBreaker computes its outbound selectors from selector "pauseFor" [.uint256]; the gateway carries census-derived literals frozen from the Solidity source. The two equalities are decided by the kernel between encoders defined on independent evidence, so a wrong literal on either side fails — which is also why, with every code-shape premise gone, the ABI agreement is the one thing left that a mutant can still falsify, and it is controlled.
The stratum is one-way by construction: composition may name several families, the families stay siblings and neither imports the other, and roots aggregate composition without the dependency ever running back. The layering gate’s committed controls include five composition-edge mutations: an unclassified composition module, shared→composition, contract→composition, and composition→root for each of the two roots — each fail at the intended edge in disposable copies and return to green when only the mutation is removed. The CircuitBreaker’s 75-row assurance register carries four composition rows: TWG-3 records the two constructed worlds, and TWG-4 a literal BPO2 replay of the compiler-owned artifacts’ finite and sentinel pause and query — dated finite evidence, never a theorem premise.
How we know it is the gateway
A locked reference, and a corpus that measured the losses.
“Right” was written down before it was argued: LIDO_TRIGGERABLE_WITHDRAWALS_GATEWAY_COMPATIBILITY.md freezes all 24 endpoints, the constructor, six events, and thirteen cross-cutting boundaries, filled from the validated reference lock and the generated differential manifest — a synchronization gate rejects marker drift, an undispositioned deviation, or a mismatch with either source. Two layers discharge the claims.
▸The reference lock — which contract, exactly13-source closure · byte-for-byte recompilation · dual-provider snapshot · 15 falsifiers
check-lido-twg-reference.sh reconstructs the exact source, compiler, deployment, and provider lock offline: the thirteen-file Solidity closure at the pinned lidofinance/core commit recompiled byte for byte with the vendored solc 0.8.9, both parameter worlds derived, the complete ABI, event, error, role, and storage identities checked, and two independent RPC snapshots at block 25,866,991 reconciled — runtime code hash, pause state, and the CircuitBreaker’s role. Fifteen falsifiers cover deletion, type, digest, closure, artifact, provider, and coordinated-input mutations. A separate census gate pins the 24 selectors, six event topics, fourteen custom errors, six role and slot hashes, and the exact whenResumed surface.
▸Differential evidence — the sanity layer62 agreements + 9 registered deviations · 52 causal messages · 186 resource boundaries
check-lido-twg-differential.sh executes the exact compiler-derived Blanc creation and runtime artifacts beside the locked reference in a pinned EELS Prague interpreter, agreeing on status, exact returndata, the logical projection, ETH, ordered logs, and calls — with the nine rows that exercise a registered deviation compared just as exactly, each naming its one stable registry row and its expected channels. No status-only allowlist and no unknown-mismatch allowlist exists. The corpus covers both pause polarities and both sentinel arms, seven role negatives, enumeration and collision histories kept as repaired regression rows, limit configure, consume, and refill behavior, the trigger path over mock worlds with fee, value, router, refund, ETH, log, and call effects, and explicit rollback.
The corpus earned its keep six times over before the port’s claim could be made: supportsInterface(bytes4) had been decoded as if the argument were right-aligned; then, in order, a constructor-argument lifetime, the value returned by role enumeration, the revocation decrement, two non-terminating role loops, and the paused/resumed error polarity. Each is a declared conformance repair that moved the runtime, and the family revalidated every affected proof on the repaired program. The cheapest way to be wrong is to prove the wrong program; tests catch that first. Later, four production-shape controls with paired mutants were added to bind the re-optimized runtime’s packing, nested-keccak role keys, per-role enumeration, and one-read authorization route.
▸Proven functional specifications — the quantified layerpause face · authorization · the bundle · the composition
Where the corpus samples, the theorems quantify — always about the exact compiled bytes: lidoTwgCode_compile exposes the exact-bytes equation for arbitrary deployment parameters, and every statement hypothesises those bytes. The pause-face and authorization families cover pauseUntil, resume, the role-gated negatives, and the protected surface; the bundle and the composition theorem are stated in full above. The composition’s protected statements, both closed worlds included, are pinned by check-claims.sh, and the four composition rows sit in the CircuitBreaker’s assurance register, whose verifier fails if any cited declaration, axiom set, or non-claim phrase drifts.
Deviations
Three accepted, two repaired — none an improvement.
LIDO_TRIGGERABLE_WITHDRAWALS_GATEWAY_DEVIATIONS.md records five behavioral differences: three accepted, two repaired, zero pending, with no unknown-mismatch allowlist; its policy marker and its five row markers encode the same counts, and the family gate rejects drift between them. None of the three accepted rows rests on “better”.
Unauthorized role-gate payload
TWG-D01 — accepted priced costThe reference’s AccessControl base rejects a missing role with dynamic Error(string) data naming account and role. Blanc rejects with the four-byte selector of a no-argument AccessControlUnauthorizedAccount(). Status and rollback agree; returndata differs on seven unauthorized paths.
The argument: one compact, proof-oriented error-table convention, at the declared cost of the reference’s diagnostics. Not defended by the port’s size or gas wins — those do not erase a returndata difference — only as the local cost of the simpler verifiable representation.
Two more empty reverts
TWG-D02, TWG-D03 — accepted priced costsA wrong-account renounceRole and an out-of-bounds getRoleMember empty-revert where the reference returns a reason string and a Panic(0x32) respectively. Both remain gas wins; the cost is returndata only.
The argument: the same compact rejection convention. Proof locality — not size, not gas.
Enumeration order, and collision refusal
TWG-D04, TWG-D05 — repairedThe former runtime could return a different valid member at the same ordinal after a cross-role removal history, and in a constructed colliding state could refuse an operation the reference admits. Both were first filed as orthogonal or priced fail-loud costs; both changed public observations, so both were repaired rather than waived.
The record: the current runtime returns the reference’s order, and both formerly colliding grants succeed independently with hasRole, counts, ordering, and logs matching. The stable IDs stay as regression boundaries, each held by a live causal differential row.
Deltas
Smaller, and cheaper — on every named path.
| quantity | value | status |
|---|---|---|
| runtime size | 8,094 B | vs 8,128 reference — 34 smaller; 16,482 B of EIP-170 headroom |
| full CREATE input | 9,966 B | vs 10,256 — 290 smaller |
| successful construction gas | 1,735,425 | vs 1,744,364, code deposit included, in pinned EELS |
| pauseFor, finite duration | 25,598 | vs 26,352 — cheaper by 754 |
| unauthorized role gate | 2,393 | vs 32,304 — the compact error is 29,911 cheaper |
| named gas rows dearer | 0 / 51 | every cell a strict win; a nonnegative regeneration fails the gate |
No gas superiority beyond the ledger — the numbers are measurements against the locked reference under one declared boundary (direct EELS Prague message gas used; constructor rows include code deposit and exclude intrinsic gas and refunds), over 51 named cells. Arbitrary-world gas and access-list warming remain implementation freedoms, and the unauthorized-gate row is a diagnostic cost the reference pays and Blanc does not, not a defense of anything.
Universal gas behavior is not claimed in either direction. The family’s differential is under the pinned Prague EELS; a separate BPO2 lane replays the compiler-owned CircuitBreaker and gateway artifacts’ finite and sentinel pause and query, with two execution mutants, as dated finite evidence behind a Prague-to-Osaka applicability ledger — not a live-chain attestation.
Notes
What the build taught.
The composition theorem’s first candidate asked the caller for three low-level facts about the target’s code. A hostile review found each implied by something the caller already supplies — the compiler witness, the successful polarity — and a later review found the last one, depth ≠ 0, still implied and still unproved: searching for an existing lemma is not the same as asking whether a fact follows. The inversion now exists, at zero depth a zero-value CALL cannot spawn and the bubble cannot end .ok, and the reviewer’s probe was treated as a blueprint and re-derived against the semantics. The genuinely surviving hypotheses are a non-static enclosing frame, a non-precompile target distinct from the caller, and — since the semantics learned Amsterdam — a covered fork.
The closure contract asked for mutants refuting the non-delegation and nonempty-code premises. Once those premises were derived rather than assumed, the mutants had nothing to refute, and they were deleted rather than kept: an artefact servicing a deleted premise looks like coverage while testing nothing. What remains falsifiable — the ABI agreement between independently defined encoders — remains controlled. The wording is the user’s, recorded because it generalizes: negative controls exist to bite, and a control that can no longer bite is not evidence, it is furniture.
Boundary, restated: nothing on this page verifies the Solidity artifact deployed at 0xDC00…037B — its address and snapshot block are provenance identifiers. The composition theorem’s successful run is constructed in two finite configured Prague worlds, not in general; it does not cover a target behind a proxy, a second transaction, liveness, gas sufficiency, or an Amsterdam frame; and the locator, vault, and router are not ported. The five deviation rows and the raw-storage non-claim are the registry’s, in the honest register.