Blanc/implementations/ports
OssifiableProxy.
The port of Lido’s OssifiableProxy — the ERC-1967 proxy in front of Lido’s withdrawal queue at 0x889e…F9B1, taken from its canonical deployment at block 17,172,547: seven named control entries, a payable fallback and receive that delegate everything else, and an admin that can renounce itself forever. Before this port, every Blanc theorem treated delegation as an exclusion. Delegatecall — code address and storage owner pulled apart — is now a verified capability, and the proxy is the contract that exercises it.
A port never claims byte identity — PORTING.md governs what is claimed and what never is. What makes this port distinctive: its forwarding envelope quantifies over an arbitrary certified child; its efficiency campaign was pre-registered — 25 cells, a 13-win threshold — and won all 25; and on top of the port sits an upgrade theorem: the exact compiled proxy’s upgradeToAndCall proved to realize a named migration, with behavior through the proxy proved to refine before and after.
Fig. 1 — two gates, verbatim (exact-candidate run 2026-09-03 UTC), digests elided: the differential matrix beside the locked Solidity reference in a pinned Prague oracle, and the upgrade gate that pins the headline theorems, their axiom sets, and the twelve executable witness rows byte for byte — and whose self-test now runs 45 disposable controls that must each fail at the intended channel.
What the port proves
Forwarding for any child, and control that ends where it says.
A proxy is two contracts pretending to be one: the code runs at the implementation’s address while the storage stays the proxy’s. The port’s central theorem states the wrapper exactly — for an arbitrary delegated child, supplied as a certificate, the outer message settles to what the child did — and leaves the harder question visible rather than assumed: what a direct call to the implementation has in common with the child a proxy spawns is a separate obligation, DirectTargetTransport, because the two differ in gas, depth, access sets, transfer flag, code address, target, and storage owner.
For the complete runtime, an exact delegated child execution — arbitrary code, supplied as a certificate — determines the wrapper’s settled result: the outer message settles to the child’s status, output, and proxy-owned storage effects, with gas and warm sets deliberately absent from the observation.
theorem processMessage_forwardingEnvelope (outer : Msg) (afterTransfer : Benv) (callPre : Devm) (d : DelegatecallSpawnDescriptor (initSevm (outer.withBenv afterTransfer)) callPre) (route : OssifiableForwardingRoute outer afterTransfer callPre d) (childOut : MessageResult) (tail : match childOut with | .ok child => ForwardingTailBudget d child | .error _ => PUnit) (certificate : DelegatedChildCertificate d.child childOut) : ∃ wrapperOut, processMessage outer = wrapperOut ∧ ChildToWrapperSettledAt outer.currentTarget childOut wrapperOut
Read the shape — the child is an input certificate and the outer result is existential, derived from compiled execution and message settlement rather than asserted. ForwardingTailBudget is the one thing asked of the parent after the child returns — enough gas to run its own return tail — and it is what the registry’s G-5 row is about: Blanc’s shorter schedule before DELEGATECALL can hand a child a different EIP-150 budget than the reference would. The route carries the exact context — current target and storage owner, code address, the gas word and its 63/64 split, depth decrement, warm sets, no value transfer — so that a property of the direct target crosses to the delegated child only through an explicit transport proof.
processMessage_forwardingEnvelope -- the theorem above ossifyMutation_success_irreversible -- after a successful ossify, every control entry is ossified — forever, through the control surface upgradeToAndCall_message_atomicRollback -- a failed setup restores state and transient storage to what the message entered with migration_sound -- the named S1→S2 migration establishes the v2 domain and the relation R2, independent of any transaction upgradeToAndCall_primary_realizes_migration -- the exact compiled proxy performs that migration throughProxy_primary_refinement -- calls through the proxy agree, before and after
getAdmin, getImplementation, getIsOssified, ossify, changeAdmin, upgradeTo, upgradeToAndCall — all seven reject nonzero value in the compiler wrapper before any decoding; an admin of zero yields ProxyIsOssified() before the caller is compared; same-value admin and implementation writes still perform the store and emit their events; and ossification writes zero and emits AdminChanged(previous, 0) then ProxyOssified(). Reference quirks matched on purpose, each proved as the frozen boundary states them.
constructor(address, address, bytes) is decoded strictly, then runs in source order: Upgraded, optional setup, AdminChanged. The setup child owns proxy storage and may alter either ERC-1967 slot — so AdminChanged reads the post-setup admin, and the final write preserves that raw word’s upper 96 bits. Both-slot mutation, the exact returned runtime, direct-CREATE settlement, and whole-CREATE rollback on a failed setup are proved, not sampled.
The proxy sits on a foundation the thread built first: a uniform four-member role separation across the shared call machinery — zero-value call, nonzero call, static call, delegatecall — and a Jaune pin bump that binds the EIP-7702-resolved code address in every call opcode, so the semantics itself keeps code address and storage owner apart. The bump’s measured wave was 44 files and 129 declarations repaired across nine layers, paid once by the goal that wanted the capability.
85/85 — so a GAS-sensitive implementation behaves the same behind the Blanc proxy?
pushbackNo, and that is the one accepted deviation. The rows compare status, exact returndata, projected storage, ETH, ordered logs, target disposition, and the frozen DELEGATECALL projection — caller, code address, input, storage owner, value, and child outcome — but not child gas. Blanc executes a shorter schedule before it reads GAS, so EIP-150 can hand the delegated child a different budget than the reference would, even when both outer calls have ample gas; a child that branches on gasleft() can therefore differ in status, output, logs, or proxy-owned storage. Registry row G-5 prices that: deployers whose implementation depends on exact gas must discharge a budget-sensitive argument or choose a fixed-gas wrapper. Nothing here claims cross-artifact equivalence for such children.
What about CREATE2, beacons, UUPS — or Lido’s actual admin?
pushbackOut of scope, and listed as such in the registry’s exclusions: no arbitrary-block deployment root or historical CREATE address derivation, no current mainnet admin or implementation state, no CREATE2 or factory deployment, no UUPS, beacon, or transparent-proxy behavior, no delegatecall-as-library use of the runtime, and no named control selector beyond the frozen seven — unmatched selectors and calldata of zero to three bytes stay fallback, as the reference’s do. The canonical deployment at block 17,172,547 is an oracle and provenance anchor; nothing verifies the Solidity at 0x889e…F9B1.
The family’s 86 audited theorems sit in the repository-wide axiom audit, and the constructor, direct-CREATE, and closed-fixture boundaries — the nonempty setup chronology, the exact both-slot setup child, and the failed whole-CREATE rollback among them — are pinned by check-claims.sh. Fixed Keccak decisions for the ERC-1967 slot words use the existing kernel route; nothing joins the trusted base.
The upgrade — a proxy and two implementations at once
An upgrade that is proved to be a migration.
Upgrade equivalence is the recurring ask of everyone who runs a proxy, and it is usually answered by inspection. Blanc answers it with five explicit objects — the proxy program, v1, v2, a migration, and a relation — and two conclusions kept deliberately apart: that the migration is sound for the relation, and that later calls through the proxy refine one another. Neither is evidence for the other, and neither contains an opaque certificate that assumes the postcondition it is meant to prove.
One authorized execution of the exact compiled proxy’s upgradeToAndCall(v2, initializeV2(), false), from the named v1 installation, commits v2, runs the initializer child that this very execution spawns over proxy-owned storage, copies the protected word from slot 7 to slot 8, writes the marker at slot 9, emits exactly the Upgraded log — and establishes both the initialized v2 domain and the relation R2.
theorem upgradeToAndCall_primary_realizes_migration (proxyProg : Prog) (hproxy : proxyProg = runtimeBaseline) {sevm : Sevm} {entry post : Devm} {entryImage : Bytes} (houter : Prog.RunCompiledTo sevm entry proxyProg (.ok post)) … -- exact caller, calldata, live admin, v1 installed, v2 code present, … -- the raw implementation commit, a well-formed entry image, and (hchild : PrimaryChildExecution sevm post) : Devm.getStor post upgradeProxy = ((((Devm.getStor entry upgradeProxy).set implementationSlotLit v2Implementation.toB256).set v2ValueSlot (Devm.getStorVal entry upgradeProxy v1ValueSlot)).set migrationMarkerSlot migrationMarkerValue) ∧ … ∧ initializedDomain upgradeProxy post.state ∧ upgradeRelation upgradeProxy entry.state post.state ∧ post.logs = entry.logs ++ [rawUpgradedLog upgradeProxy v2Implementation.toB256]
Read the shape — the proxy program is an explicit argument required equal to the exact runtimeBaseline, never hidden in a constant. PrimaryChildExecution universally consumes the call states the outer boundary selects and supplies only the descriptor-selected child’s compiled run; its output and storage effects are derived from that run, not stored as certificate fields — an independent review blocked an earlier version on exactly that point. The identity routes are proved beside it: exact upgradeTo and the skipped empty upgradeToAndCall change only the implementation word, and they preserve R2 only under an explicit admissibility premise the ordinary witness is proved not to satisfy — so “upgrade without migrating” is a biting control, not a route.
v1 and v2 are goal-local Blanc implementations of 74 and 141 bytes, proved distinct: v1 keeps value() and setValue at slot 7, v2 at slot 8, plus an initializer and a marker getter. The relation is R2 — equality of the protected logical word on the shared selectors — not full-surface R1, since v2’s marker and the stale v1 word are outside the projection, and not invariant-only R3. Through-proxy refinement retains both exact forwarding routes, their context, and the G-5 tail budgets; a closed value() package inhabits the entire premise set, so no premise is satisfiable only in principle.
An evaluator executes the exact artifacts under Prague: the primary upgrade succeeds with implementation v2 and slots 42/42/1 at 4,941,998 gas; upgradeTo and the skipped-empty route succeed while leaving slot 8 and the marker untouched; an unauthorized caller, an ossified proxy, absent v2 code, and a reverting setup each fail and restore v1 and 42/0/0; and four rows re-enter the upgraded proxy to read 42, write 73, read 73, and read the v2-only marker. The relation row confirms the primary poststate is R2-related, the ordinary state is not identity-admissible, and a poststate with slot 8 at 41 violates R2.
What this is not: a theorem about arbitrary proxies, implementations, migrations, or relations; a claim about any Lido upgrade or about deployed Solidity; a forced-empty or redeploy-and-migrate route; a selection of a one-proxy, many-implementations architecture; or a universal liveness or gas claim. Scalar slots are checked against the three named ERC-1967 slots only — no global collision theorem and no hash assumption.
How we know it is the proxy
A locked reference, a corpus, and a bet placed before the race.
“Right” was written down before it was argued: OSSIFIABLE_PROXY_COMPATIBILITY.md freezes the constructor, the seven entries, fallback and receive, and thirteen cross-cutting boundaries — nonpayability, dispatch, ABI edges, authorization precedence, setup reverts, events, errors, the functional ERC-1967 words, constructor order, delegated returndata — and names the proof family and differential rows that own each. Three layers discharge it.
▸The reference lock — which contract, exactly7-source closure · byte-for-byte recompilation · two archival captures · 36 falsifier cases
check-lido-ossifiable-proxy-reference.sh reconstructs Lido core v4.0.0 at its pinned commit with OpenZeppelin 4.4.1 and solc 0.8.9 offline, recompiling the seven-source closure byte for byte and deriving the constructor, seven named entries, fallback and receive, the events and errors, and the exact ERC-1967 words; the source-and-compiler route and the transaction-and-deployed-runtime route reproduce the same 2,497-byte runtime, and two archival RPC captures are reconciled. Thirty-six live falsifier cases — deletion, type, digest, compiler, ABI, provider, coherent-input — keep the evidence-filled compatibility contract synchronized with the lock rather than with anyone’s memory of it.
▸Differential evidence — the sanity layer85 rows · seven falsifier families · a typo the red run caught
check-lido-ossifiable-proxy-differential.sh executes the exact locked Solidity and Blanc complete CREATE inputs in fresh symmetric pinned-EELS Prague worlds: 18 constructor cases, 7 getters, 16 control entries, 20 upgrade-and-call arms, 17 fallback and receive cases, and 7 named-value rejections, compared on status, exact returndata, projected storage, ETH, ordered logs, target disposition, and every ordered DELEGATECALL field, with no skip and no allowlist. Seven independent falsifier families — reference substitution, selector routing, event and error bytes, state projection, rollback, child-call observation, corpus and result mutation — must keep biting.
The first complete run was red, and the red result is preserved: three expected fixtures spelled a revert payload implentation, and both artifacts correctly returned implementation. The successor corpus changed only those expected bytes — a defect in the test, caught by the two things it was testing, and recorded rather than tidied away.
▸The efficiency campaign — pre-registered25 cells · threshold 13 strict wins · 25 won · BPO2 replay 21/21
The immutable campaign contract fixed two size cells, 23 direct Prague gas cells, a denominator of 25, and a threshold of at least 13 strict Blanc wins before any measurement ran, and every cell is scoreable only after semantic agreement. One optimization was admitted, and only after a frozen baseline and a written prediction: ten product-private address reads changed from PUSH0 NOT PUSH1 0xa0 SHL NOT AND to PUSH0 NOT PUSH1 0x60 SHR AND, predicted at −9 and −10 bytes and −1,803 deployment gas, and measured exactly so. Code sharing was rejected because its trigger did not fire. The final ledger is 25 agreements and 25 strict wins, with zero ties, losses, or incomparables.
A report-only replay under the current-mainnet BPO2 target represents 21 transaction scenarios with 21 semantic agreements, 19 lower Blanc receipt-gas rows, and two ties — run 2026-09-02 and credited by content identity. The two size cells are not transactions, and two forwarding cells need pre-warmed message state the singleton transaction interface cannot express; neither alters the primary score.
▸Proven functional specifications — the quantified layerforwarding · control · constructor · the upgrade
Where the corpus samples, the theorems quantify — always about the exact compiled bytes: a generator-owned module ties the 1,249-byte constructor prefix, the 2,188-byte runtime, and the 3,437-byte creation template to explicit byte literals with compiler witnesses and kernel-checked SHA-256 and Keccak-256 identities, and a network-free gate rejects a laundered literal. The forwarding envelope and the upgrade family are stated in full above; between them sit the control effects for all seven entries, the strict constructor decoder and both-slot deployment family, and the whole-CREATE rollback — each a theorem hypothesising those bytes in so many words.
Deviations
One accepted — and four boundaries priced beside it.
OSSIFIABLE_PROXY_DEVIATIONS.md accepts exactly one ordinary-behavior deviation and declares it before anyone asks. Beside it stand three measured semantic-preserving implementation choices whose observability is gas and out-of-gas boundaries, and one boundary clarification that is intrinsic to delegation itself. Any later mismatch must be repaired or dispositioned there before the port claim can move.
The forwarded child budget
G-5 — accepted, pricedBlanc reads GAS after a shorter schedule than the Solidity wrapper — it omits a redundant code check and discards successful setup returndata earlier — so the EIP-150 child budget can differ, and a GAS-sensitive implementation or setup child can branch differently even when both outer calls have ample gas.
The argument: the priced consequence of a measured smaller and cheaper wrapper. The 85 rows agree on their published projection, which excludes child gas; no cross-artifact universal equivalence is claimed, and a deployer whose implementation depends on exact gasleft() owes a budget-sensitive argument.
Three schedules that cost less
G-1, G-2, G-3 — measured, semantic-preservingThe constructor copies its dynamic setup payload incrementally into a fixed scratch region rather than replaying solc’s decoder schedule; the upgrade path checks the new implementation’s code once, where OpenZeppelin checks twice; successful setup returndata is discarded as soon as the child reports success.
The argument: every applicable differential row agrees, and the affected cells are strict wins in the frozen matrix. What can differ is the exact gas point at which a malformed or underfunded creation halts — outside semantic equivalence, and measured separately. No intervening execution can remove code between the reference’s two checks.
Direct target versus delegated child
G-4 — boundary clarificationA direct call to the implementation and the proxy’s delegated child enter with different gas, depth, access sets, transfer flag, code address, current target, and storage owner. Blanc states those differences and does not assert whole-message equivalence for arbitrary code.
The argument: not a port deviation but the nature of delegation, exposed rather than normalized away. A property of the target that is sensitive to any of those seven carries over only through DirectTargetTransport, which the upgrade family discharges for the scalar input word and no more.
Deltas
Twenty-five cells, pre-registered — and all twenty-five won.
| cell | Blanc | reference |
|---|---|---|
| A1 · runtime size | 2,188 B | 2,497 B |
| A2 · creation template | 3,437 B | 4,207 B |
| A3 · deployment, empty setup | 487,814 | 550,980 |
| A4 · deployment, with setup | 510,079 | 573,987 |
| F1 · delegated forward | 4,958 | 5,099 |
| C7 · upgradeToAndCall | 33,705 | 34,973 |
| N5 · setup revert, bubbled | 11,643 | 12,874 |
| all 25 cells | 25 wins | 0 ties · 0 losses |
Seven representative cells of the frozen A1–A4 / F1–F7 / C1–C9 / N1–N5 vector; the committed ledger holds all twenty-five, each scored only after semantic agreement.
Universal gas dominance and global optimality are not claimed: the campaign is a finite, pre-registered vector, and its threshold was a bet the port could have lost. Child gas is not compared anywhere, which is what G-5 records. The direct-versus-delegated gas, depth, and access differences are stated, not equalized.
The primary campaign is under the pinned Prague EELS; the BPO2 replay is report-only and does not alter or double-count that score. These are measurements, and the page labels them as such rather than promoting them into a property.
Notes
What the build taught.
The upgrade family’s first candidate carried the shared child’s output and storage as structure fields and consumed them as certificates; its initializer child was existentially independent of the outer setup boundary; and its complete through-proxy premise set had no inhabitant. An independent reviewer blocked completion on all three. The repairs are the theorems the page now quotes: effects derived from compiled child runs, a child universally bound to the states the outer walk selects, and a closed package that satisfies every premise at once. A certificate that assumes the desired postcondition proves nothing; the gate’s self-test now mutates for exactly that.
The efficiency campaign froze its 25 cells, its 13-win threshold, and its symmetric worlds in an immutable manifest that a static gate validates without running anything, rejecting manifest, result, classification, score, lineage, and threshold corruption in 58 hostile static cases. Only then was one optimization proposed, with its prediction written down, and only after the measurement matched the prediction was it admitted. A number that could not have come out the other way is not a result, and the campaign was built so that it could have.
Boundary, restated: nothing on this page verifies the Solidity deployed at 0x889e…F9B1 — the canonical deployment is an oracle and provenance anchor. The forwarding envelope excludes gas and warm sets from its observation; the upgrade result is R2 on one goal-local witness pair; the direct-versus-delegated boundary is stated, not closed; and the declared destination — Lido’s gateway behind this very proxy — is a successor that must discharge exact transport, G-5 included, and is neither launched nor implied. The full list lives in the deviation registry’s exclusions, in the honest register.