Blanc/implementations/ports
WETH10.
The port of the deployed WETH10 at 0xf4BB…8A9F — all 27 selectors plus receive, flash loans, ERC-677-style callbacks, EIP-2612 permit — taken from zero contract code to a closed verification charter. On top of the endpoint families sits the headline theorem: future redeemability, at every reachable future, after arbitrary other actors have done their worst.
A port never claims byte identity — PORTING.md governs what is claimed and what never is. What makes this port distinctive is that its behavior contract was frozen first, endpoint by endpoint, and every layer of evidence answers to that document.
Fig. 1 — the WETH10 differential suite beside the deployed runtime, and the repository-wide statement-pinning gate that makes a silently weakened theorem statement fail as loudly as a broken proof. The statement-pin count spans every protected family, not WETH10 alone. The differential line continues “… 7 state-mutating reentrancy rows, 26 STATICCALL-context rows, 69 oracle calls traced, 8 channel falsifiers live.”
What the port proves
Redeemability, at every reachable future.
Behaving like WETH10 is the entry fee. The reason to rebuild a wrapper in a proof language is the promise no test suite can state: whatever happens after deployment — flash loans, reentrancy, hostile callbacks, arbitrary contracts doing arbitrary things — every holder can still get the ether out. The redeemability theorem states that promise at any reachable future of a proved deployment, and proves it constructively, execution by execution.
From a proved deployment of the exact compiled WETH10 runtime, any leg of valid blocks selected by Jaune’s configured mainnet schedule to a checkpoint, and any further configured leg to an arbitrary future snapshot, there is an accounted history of the window carrying the dual-selector redemption guarantee below for an arbitrary holder u. The unsuffixed theorem has the same shape for any cfg whose schedule selects only covered forks.
theorem deployment_reachable_future_dualSelector_redeemable_mainnet {dp : DeployParams} {ca u : Adr} {base deployed checkpoint future : BlockChain} (hroot : MainnetDeploymentRoot base deployed dp ca) (hcheckpoint : BlockChain.ReachUsing mainnetChainConfig deployed checkpoint) (hfuture : BlockChain.ReachUsing mainnetChainConfig checkpoint future) : ∃ history, FutureDualSelectorRedemptionGuarantee mainnetChainConfig dp ca u checkpoint future history
Read the quantifiers — u is every holder, not a specially chosen one. ReachUsing is Jaune’s configured-chain reachability: whole valid blocks, every transaction anyone sent, under the model’s one global side condition, that total ETH plus pending withdrawals stays below 2256 wei. The history is obtained from the reachability derivation, not reconstructed from the endpoints — a logical guarantee about the window, never a trace extractor. And the all-holders sibling, deployment_reachable_future_redeemable_allHolders, concludes ∃ history, ∀ u — one history carrying the guarantee for every holder at once — not the weaker ∀ u, ∃ history.
The gross ledger identity retains every flow — B₀ + ordinaryIn + selfTransfer + flashCredit = Bₜ + redeemed + externalTransferredOut + selfTransfer + flashRepayment — and flash credits and repayments are proved to pair and cancel exactly, leaving B₀ + ordinaryIn = Bₜ + redeemed + externalTransferredOut in ℕ: committed credits proved not to wrap, no hidden modular slack. Hence the floor B₀ ≤ Bₜ + redeemed + externalTransferredOut — whatever the window did, it cannot dilute a holder below their residual.
For every amount within the residual, every admissible canonical withdraw or withdrawTo at the future snapshot succeeds — a constructed ∃ post, … = .ok … with the exact effect, not the absence of a counterexample — and so does the complete signed type-2 transaction, intrinsic gas, validity checks, and settlement included. Rebased corollaries deliver the same at the full booked balance.
deployment_reachable_dormant_holder_balance_monotone: a holder who performed no effectful authorizing act — no debit as actual caller, no approve write, no permit recovering to it — cannot have lost a wei, and inert reads do not void the premise. deployment_reachable_redeemClaims_anyOrder: the bank-run shape — for any duplicate-free supplied holder list, every permutation of full-balance claims succeeds, one canonical message at a time, with the aggregate effect on balances and ETH exact. Overbooking is impossible by the shape of admissibility, not by a side condition.
“Redeemable” for whom, exactly? Holders are not all EOAs.
pushbackAt transaction altitude the admissible senders are exactly the senders Ethereum’s modeled rules admit: code-free accounts and valid EIP-7702-delegated ones. For a funded code-free external holder with canonical nonce, fees, gas, and payload, the envelope discharges every admission obligation except one — recovery of the holder’s own signature — and no theorem forges it. A holder with non-delegation contract code that cannot call WETH10 keeps a conserved balance but has no transaction-altitude exit of its own; WETH10 itself is an example, since it can legally receive its own token. Direct withdraw pays the sender and so retains the code-free-recipient restriction; withdrawTo permits any nonzero, non-precompile, code-free recipient.
Doesn’t attribution smuggle a hash assumption into redeemability?
pushbackThe hypothesis exists, and it is quarantined. Unconditionally, hardenedOutflow ≤ permanentOutflow. The equality — every nonzero permanent outflow in the deployment window traces exactly to the holder’s own call, its in-window approve, or its in-window permit — takes exactly one hypothesis, NoAllowanceKeyCollision: a decidable, trace-local property of the finitely many (owner, spender) word pairs the history actually touched, never a global injectivity assumption. It is consumed solely for attribution — the conservation equation, the floor, and both enabledness families never depend on it. And attribution names the account whose recorded act the runtime accepted, not consent, intent, or awareness: a phished approve and a relayed permit both attribute to the signing account.
The deployment root — an axiom wearing a record type?
pushbackDerived, not axiomatized. The public inputs are deliberately pre-execution — a valid configured base, strict canonical-block evidence, the closed type-2 envelope — plus one actual stateTransitionUsing success. From those, canonicalDeploymentStep_establishes_root reconstructs the prepared post-system message rather than assuming it, and proves the collision branch, receipt success, the exact installed runtime, empty storage, and the deployed valid context, with the creation message’s 1,264,071-gas cost as a closed form. The result is deliberately specific in shape: one strict singleton anchor — no factory, CREATE2, or co-block shapes. The theorem itself is schedule-parametric over the covered forks — Prague, Osaka, BPO1, BPO2; the public mainnet constructor selects BPO2, and the finite BPO2 deployment fixture witnesses that specialization without becoming a proof premise.
And the everyone-out run — is that a real bank run?
pushbackIt is a message-altitude theorem about a supplied list: every permutation of one full-balance claim per listed holder succeeds, each envelope constructed by canonicalRedemptionMessage from that step’s own state — nothing about success is assumed along the way. What it is not: the list is input, not a state enumeration; no block step, no transaction inclusion, no claim that any of these messages was mined. Inclusion, propagation, key custody, and fee markets are out of frame here and everywhere on this page.
Boundary, stated early: every theorem above is about the exact compiled Blanc runtime on a configured chain, from its proved deployment root — never the Solidity artifact at 0xf4BB…8A9F, which nothing here verifies. The public mainnet instances use Jaune’s Prague (1746612311) → Osaka (1764798551) → BPO1 (1765290071) → BPO2 (1767747671) activation schedule; BPO2 has been live on mainnet since 2026-01-07, while Prague remains an audited compatibility corollary and the historical executable lane. The statements in Weth10*.lean are the authority on their own premises, and the full non-claim register — no semantic equivalence, no malformed-calldata closure, no key custody or inclusion, no gas, storage, or codehash parity — lives in PORTING.md and the WETH10 registries, in the honest register.
How we know it is WETH10
A frozen boundary, and evidence that answers to it.
“Right” was written down before it was argued: WETH10_COMPATIBILITY.md freezes the reference’s ordinary-call public boundary for all 27 selectors and receive — outputs, state and ETH effects, logs, guard order, rollback, what a callback may observe mid-flight — and names the evidence owning every row. Two layers discharge that contract — open the one you want to audit.
▸Differential evidence — the sanity layer147 rows vs the deployed runtime · deployment & redemption replays
check-weth10-differential.sh executes 147 generated canonical-call rows against both the literal deployed 9,975-byte runtime and the exact named Blanc family members, in a pinned oracle, across two identity worlds — zero mismatches. The rows are not gentle: 69 live CALL/STATICCALL traces, seven state-mutating or hostile reentrancy rows, 26 static-context rows, and eight channel falsifiers that must keep failing. They include a callback that catches a failed nested WETH10 transfer while its parent commits without child flow, and a successful flash callback whose ordinary transfer commits between the paired mint and settlement burn.
The current-mainnet witness is check-weth10-current-mainnet.sh: one fresh BPO2 creation block at the Lean-pinned timestamp, the type-2 redemption sequence, the type-4 authorization mutation, and 28 ordinary selector-plus-receive rows. It compares status, logs, projected storage, and fee-normalized ETH, records both receipt-gas values without claiming equality, and replays all three committed blocks through Jaune at BPO2. Prague remains the historical evidence lane. In that preserved lane, check-weth10-deployment.sh generates a fresh strict singleton type-2 creation block in memory, checks sixteen semantic assertions — successful receipt, exact installed runtime among them — and replays it through Jaune at Prague, with six falsifiers. check-weth10-redemption.sh replays two committed Prague fixtures: a zero/nonzero/failed-redemption sequence with receipt statuses [true, true, false], and a valid type-4 authorization that changes the recipient’s code and nonce.
The register stays modest on purpose: finite rows and fixtures on chosen inputs — never semantic equivalence, never called a proof. This layer’s job is to keep the theorems honest about which contract they are theorems about.
▸Proven functional specifications — the quantified layer28/28 entry families · proved deployment · compile witness
Where the corpus samples, the theorems quantify — over states, arguments, callbacks, and valid chain histories, always about the exact compiled bytes. weth10_compiles kernel-checks compiler success for every DeployParams, and weth10Code_compile exposes the exact-bytes equation each comparison world instantiates.
public compiled-effect families -- 28/28 runtime entries: reads, state transitions, 3 typed callbacks, permit, flash mint/repay/log order, exact rollback, error genres processCreateMessage_weth10_success -- creation through Jaune's real pipeline canonicalDeploymentStep_…_root -- the tx/block crossing → DeploymentRoot
These families stop where conformance stops: they say the artifact deploys, dispatches, reads, writes, calls back, rolls back, and errs exactly as the frozen boundary says it must. The conservation, attribution, dormant-holder, and redeemability stack that stands on them — the port’s reason to exist — is stated in full in the results section at the top of this page.
Exact cold and warm gas for the required views — flashFee, balanceOf, totalSupply, maxFlashLoan — is proved uniformly over deployment parameters in Weth10Live.lean. Every audited theorem sits in the repository-wide axiom audit, pinned to its exact axiom set in CI, and check-claims.sh additionally pins the redeemability family’s exact statements.
Deviations
Zero accepted — and what that does and doesn’t mean.
WETH10_DEVIATIONS.md currently accepts no behavioral deviations in its stated scope: no in-scope mismatch is known from the finite differential suite, and agreement on chosen inputs is recorded as evidence, not inflated into a proof that no mismatch exists. The registry’s standing rule does the real work: a future mismatch in the frozen surface is a defect or a new explicit conformance decision — it may not be silently moved into an “accepted” section. Silence is the one prohibited move.
The registry distinguishes behavior from implementation. Blanc keeps its freedom in: program structure, control flow, instruction selection, and runtime bytes; raw storage slots and storage proofs; code and codehash identity; exact gas consumption and access-list warming, under the adequate-gas boundary; initcode, deployment gas, CREATE2 address, and the parameter-embedding mechanism; and cheaper or more proof-reliable internals — so long as endpoint outcomes, returndata, logical state and ETH, calls, logs, guard precedence, and reentrancy snapshots remain compatible.
The README’s assurance boundary keeps “not established” beside “proved” and “tested,” and the third register is load-bearing: no verification of the deployed runtime, no semantic-equivalence claim, no malformed-calldata closure, no key custody or inclusion, no gas, storage, or codehash parity. The normative target is locked by scripts/weth10-reference.json — deployment input at a pinned parent source revision, the installed 9,975-byte runtime as the oracle anchor — so “compared against what, exactly” always has a one-line answer.
Deltas
Size, and gas — proved, not raced.
| quantity | value | status |
|---|---|---|
| runtime size | 6,313 B | committed template, parameterized by chain ID + cached domain separator |
| deployed WETH10 runtime | 9,975 B | pinned reference lock — the oracle anchor |
| constructor | 6,490 B | a 177-byte prefix copies and patches the template |
| init-execution gas | 1,471 | closed form |
| code-deposit gas | 1,262,600 | closed form |
| direct creation message | 1,264,071 | closed form, concluded by the deployment proof |
| view gas, required views | exact | cold/warm, uniform over deployment parameters |
No per-path gas comparison against the deployed original has been run for WETH10, and exact deployed-gas parity is a declared freedom, not a claim — the deployed contract’s gas profile is simply not this port’s subject. The committed figures above are Blanc/Jaune modeled costs; where the WETH page carries an informal measured comparison, this page carries none rather than a hasty one.
One floor is a fact about the bytes: both runtime and initcode contain PUSH0, so Shanghai is the minimum execution fork, and the executable specialization is BPO2 on Jaune’s current-mainnet lane, with the pinned Prague EELS retained as historical evidence. Neither fact implies deployability on earlier forks, and the page will not imply it either.
Fork boundary: a future fork that changes only rule data Jaune already models — blob parameters, the precompile set, transaction/block/code limits, or opcode activation — is a Jaune pin bump and re-verification, with any new facts stated as explicit premises. A fork that changes execution semantics changes Jaune itself — and that has now happened: the pinned Jaune models Amsterdam’s gas metering and block-level access lists, while every theorem on this page is confined to the covered forks Prague, Osaka, BPO1, and BPO2. No WETH10 result covers an Amsterdam frame or block.
Notes
What the build taught.
The 21-hour charter closed 13 of its 14 requirement rows. The fourteenth — a settlement theorem carried over from FMINT — turned out to be false of WETH10’s design, and was struck by explicit amendment: no replacement installed, nothing nearby relabeled to fill the row. The redeemability theorem was a successor program, landed over the following days by the same method. A project that never records a lost bet is not reporting, it is advertising.
The deployment execution proof is deliberately compositional — copy, chain-word patches, prehash writes, hash, separator patches, and return, proved separately and joined — replacing an all-at-once elaboration that ran past 1,000 seconds with anomalous memory use. Historical snapshots of the split modules elaborate in tens of seconds. The lesson generalises: at production surface area, the shape of a proof is an engineering artifact with its own budget, and the repository gates elaboration cost the way it gates everything else.
Boundary, restated: nothing on this page verifies the Solidity artifact deployed at 0xf4BB…8A9F — it is the reference, never the subject. The redeemability theorem’s own non-claims — attribution is not consent, signatures are inputs, inclusion and fee markets are out of frame — are listed beside it in the results section and in the registries, in the honest register.