Blanc/implementations/ports
ERC-4626 vault.
A share vault over wrapped ether, ported against OpenZeppelin’s ERC4626 (v5.7.0) — all 25 functions of the standard’s surface: deposit, mint, withdraw, redeem, their previews and max* views, the converters, and a transferable share token. Its asset is not an arbitrary ERC-20 but Blanc’s own exact WETH, so the vault’s headline theorems quantify over two verified contracts at once.
It is the port the PRORATA étude declared as its successor — the same offset-priced ledger, now with a real asset, a token standard, and a joint two-contract invariant. A port never claims byte identity — PORTING.md governs — and this one claims no ERC-4626 certification either: the standard is the source of the frozen statement, not a party to the proof.
Fig. 1 — two vault gates, verbatim (run 2026-09-25 UTC), ellipsis marking elision: the independent exact-integer oracle written from the frozen statement, with the control showing the virtual offset is load-bearing, and the offline identity check of the vendored OpenZeppelin closure, its compiler output, and a selector table equal to the vault’s own. The line continues “… native recompile leg: not requested; selected-wasm recompile leg: not requested.”
What the port proves
A vault whose books are its asset’s books.
An ERC-4626 vault makes one promise that matters: the shares are backed by the asset the vault actually holds. Stated about a vault alone, that promise has to assume something about the token. Here the token is a verified contract too, so the promise is stated about both — every configured history of the pair, arbitrary other actors included — and the one premise it cannot discharge is named, finite, and printed in the statement.
From a configured root with the exact compiled vault and the exact Blanc WETH runtime installed at distinct accounts, along any configured history over the covered forks whose visited WETH allowance keys owned by the vault do not collide, the state reached keeps the share ledger conserved, the supply within the offset-weighted WETH row the vault actually holds, and WETH itself solvent.
theorem pair_history_backed {cfg : ChainConfig} {deployed future : BlockChain} {vault : Adr} (root : PairRoot cfg deployed vault) (history : ConfiguredHistoryTrace cfg deployed future) (collision : NoVaultVisitKeyCollision (history.pairVisits vault) vault) (hcov : ∀ timestamp fork, cfg.forkAt timestamp = .ok fork → CoveredFork fork) : PairBacked vault (future.state.getStor vault) (future.state.getStor wethAccount) ∧ State.Inv wethAccount future.state
Read the premises — PairBacked is three facts: the share ledger sums to the supply, the supply stays under its cap, and the supply is at most the offset O = 1000 times the vault’s own WETH balance row. State.Inv is WETH’s solvency invariant from the first port. The collision premise is the one thing assumed: over the WETH allowance pairs the history’s frames actually visit — rolled-back frames included — no pair owned by the vault shares a hashed allowance key with a different written pair. It is finite and trace-local, not a global Keccak injectivity claim, and it is never discharged. Without it, pair_reachable_backed_or_debit still proves every configured continuation is backed or retains a positive, runtime-authorized debit of the vault’s WETH row — the failure the premise rules out is named, not hidden.
deposit_compiled_effect · … -- every successful call to each of the 25 functions: quote, exact WETH child, mint/burn, return, logs vault_message_preserves_conserved -- every vault message keeps shares summing to supply wethFrame_vaultRow_classified -- every foreign WETH frame leaves the vault's row alone, credits it, debits by allowance, or hands off pair_history_backed · pair_history_stable -- the theorem above, and the stable pair state deposit_exec_revert_visits_refused_weth_child -- capacity: within max*, a revert ran a refused WETH child (and three siblings) maxRedeem_exec_never_reverts -- …and maxRedeem, with valid calldata, never reverts deposit_success_within_maxDeposit -- every success stays within max* (four of them) pair_history_realized_dust_trace_exact -- P3: whole-history rounding residue, as an equality pair_history_attacker_open_context -- P4: coalition no-profit with an explicit subsidy term pair_history_victim_loss_bound -- P4: the victim loses at most one quantum
ERC-4626 asks that max* never advertise what the vault would refuse. At a stable pair state, with the call’s own validity conditions, a deposit, mint, withdraw, or redeem within its max* that reverts is proved to have run a refused exact-WETH child — for the caller’s own WETH balance or allowance, gas, depth, or a static context. That is a revert-cause theorem, not liveness: no theorem here says a call within max* succeeds.
The vault reaches WETH only through balanceOf by STATICCALL and transferFrom and transfer by CALL, each to the configured account, each requiring a canonical 32-byte true, each proved to roll back cleanly when the child fails — and a whole-vault inventory shows no other external call exists. A deposit quotes its shares before the WETH transfer.
Each flow is the exact floor or ceiling formula of the frozen statement — deposit never overmints, mint never undercharges, withdraw never underburns, redeem never overpays — with a strict one-quantum residue bound, and each preview returns the same formula of the same state as the successful actual. The accounting model beneath P3 and P4 is PRORATA’s, reused rather than rewritten.
“No attacker profit” — over the executed operations?
pushbackOver some realization faithful to the chain, and the page says so rather than smoothing it. The chain-level P3 and P4 forms conclude that a realized step list exists whose allowance visits are members of the history’s own visits — membership, not order or multiplicity — and state the accounting for that list. Coalition input is attributed by actor, not by the account a credit came from, so a third party’s WETH that a coalition actor moves in is priced as coalition input; the open-context form names outside gifts as an explicit subsidy instead. And the attack carrier’s inhabitant is model-level: a concrete attack path with the frozen transcript’s numbers, not an executed chain history meeting the attack premises — that exhibit is registered as open.
Why not an arbitrary ERC-20?
pushbackBecause a vault’s backing is a fact about its asset, and an arbitrary token’s code is exactly what a theorem cannot vouch for. Pairing the vault with a verified WETH is what lets the backing theorem conclude something about the asset’s real state — WETH’s solvency included — instead of assuming a well-behaved token. The price is scope: no theorem here is about WETH9, a production vault address, the OpenZeppelin source, or any other asset, and both contracts are installed directly at configured accounts — no CREATE transaction is covered.
Claim class, stated: 176 audited theorems — 171 in the vault and pair namespaces and five generic reverting-walk lemmas they introduced — sit in the repository-wide axiom audit, and 63 statements are pinned character for character. Every frame theorem takes a covered fork and every chain headline a schedule of covered forks — Prague, Osaka, BPO1, BPO2; the mainnet schedule is proved to satisfy it, and no Amsterdam frame or block is covered. Compiled-effect theorems are partial correctness: they describe every successful run. The theorem-to-claim map is the authority on which sentence each theorem carries, which only finite evidence carries, and which is not carried at all.
Composition — two verified contracts at once
The vault and its asset, in one stratum.
The vault family proves what its own bytes do; everything that needs WETH’s bytes too lives in the composition stratum — 34 modules strictly downstream of both families, which neither imports. PairRoot installs the compiled vault and the inherited WETH runtime at distinct, non-precompile accounts with empty storage, and every chain-level headline starts there.
wethFrame_vaultRow_classified is the history’s rely condition: every exact WETH frame entered by a caller other than the vault either leaves the vault’s row alone, credits it from another account, debits it through a runtime-authorized allowance, or hands off to a withdraw callback — and the classification is proved sound, complete, and total. A donation is therefore a credit arm, accounted rather than minted against; the whole-history residue equality carries credits as their own term.
WETH’s exact credit is a bare addition modulo 2256. At the one boundary where that matters — a nonzero deposit into a vault with no shares whose assets sit at the word ceiling — the vault executes where the reference reverts, and the deviation registry records it. That world violates WETH’s solvency invariant, which the pair theorem proves at every configured pair state under the collision premise: the row exercises arithmetic, not a reachable history.
How we know it is ERC-4626
A frozen statement, a vendored reference, and an oracle.
The standard (ERC-4626, Final) is the source of the frozen statement; OpenZeppelin v5.7.0 is the differential referent, vendored and compiled, never trusted. Finite evidence carries conformance; the theorems carry the frozen statement. Neither is asked to do the other’s job.
▸The reference — which ERC4626, exactly17 sources + LICENSE · frozen compiler output · 25 selectors · 7 corruptions
check-prorata-weth-vault-reference.sh verifies offline that the vendored closure is exactly the frozen 17-source set, by per-file SHA-256 and Git blob, with the upstream MIT license; that the committed standard-JSON input is built from those bytes; that the committed solc 0.8.36 output carries the frozen creation and runtime identities; and that the reference’s method identifiers are exactly the vault’s 25 signatures, with no permit or ERC-165 on either side. Its self-test corrupts a source byte, the lock, the bytecode, tree membership both ways, the optimizer settings, and the vault’s own selector table; each must fail with its own diagnostic.
▸The oracle — arithmetic, falsified first12 property batteries · 63 boundary states · 8 perturbations caught
An independent exact-integer model written from the frozen statement checks the representability identity, the tightness of both capacity bounds, the four rounding directions, round-trip non-profitability, ledger conservation over randomized transcripts, and donation classification, over 63 boundary states, and regenerates the committed golden vectors byte for byte. With the offset disabled, the control must bite. Its frozen first-depositor transcript is the attack the theorems price: an attacker putting in 1,000,001 wei takes out 500,125, and the victim of a 1,000,000-wei deposit loses 249.
▸Differential evidence — the sanity layer25 selectors × 2 compiled sides · 31 check groups per side · 6 gas rows
check-prorata-weth-vault-differential.sh executes the committed vault runtime and the constructor-patched OpenZeppelin reference — deployed from the locked creation input against Blanc’s WETH — through Jaune’s t8n at BPO2, projects each side’s storage through its own layout, and compares state, status, exact logs, and return data against the oracle over one boundary matrix: empty, nonempty, and donated states; all 25 selectors on both sides; every rounding direction; the guards and malformed calldata; rollback for every mutation; the allowance boundary; max* attainability near the cap; the registered deviations; and the frozen first-depositor transcript.
Where a theorem already covers a family, the differential no longer re-runs it: the gate keeps what only execution can show — fidelity at the boundaries, agreement with the compiled reference, reference identity, and measurements — and its self-test shows its kept controls bite, eleven mutants each failing at its own named diagnostic.
▸The static boundary — what the code may call3 exact child forms · whole-source call closure · 7 optional Lean mutants
Two further gates bind the artifact and its boundary: one pins the routing surface, the constants, the flat storage-key scheme, the auxiliary layout, the exact runtime digest, the EIP-170 bound, and the kernel compile equality; the other pins the exact WETH account and code, every CALL/STATICCALL occurrence, the success and rollback projections, the canonical-true return checks, and the whole-vault exclusion of hidden external calls — with seven Lean mutants available to show the boundary headlines bite.
Deviations
Nine, pre-registered — and nothing else permitted.
PRORATA_WETH_VAULT_DEVIATIONS.md records nine intended differences, each decided when the statement was frozen and each now carrying its evidence. Anything not listed is not a permitted difference: an unexpected mismatch fails the differential rather than becoming a tenth row.
Configured asset, empty reverts, honest zero-receiver capacity
rows 1–3The asset is a configured constant installed with the runtime rather than a constructor-set immutable, so the claim stays about an installed runtime. Every revert carries empty data where the reference returns custom errors. And maxDeposit/maxMint report zero for the zero receiver, matching the call that would revert, where the reference ignores the receiver.
A flat allowance key, guarded; a capped supply; an exact denominator
rows 4–6Allowances live at a flat hashed key with an explicit guard refusing address-shaped or reserved keys — the layout that makes conservation statable, with the guard a proved conclusion of the compiled approve and transferFrom effects. The supply is capped at U − O, keeping S + O a nonzero word. And the converters use an exact 257-bit A + 1 denominator, so they still quote at the word ceiling where the reference’s checked addition reverts.
Canonical returns, no permit, and the size
rows 7–9The vault requires WETH’s canonical 32-byte true where SafeERC20 also accepts empty returndata. It exposes no EIP-2612 or ERC-165, and neither does the reference’s ABI. And the runtime is independently authored at 17,481 bytes against the reference’s 4,347 — four times larger, the priced cost of inlined full-width arithmetic and per-path guards, beside the gas that design saves on every measured call.
Deltas
Four times the bytes, less gas on every call measured.
| quantity | Blanc | reference |
|---|---|---|
| runtime size | 17,481 B | 4,347 B |
| deposit, empty vault | 107,986 | 110,152 |
| deposit, donated vault | 56,662 | 58,828 |
| mint | 56,726 | 58,926 |
| redeem | 52,276 | 54,942 |
| withdraw | 52,337 | 56,969 |
| share transfer | 50,797 | 51,587 |
Each gas row is the receipt’s cumulative gas of one transaction on Jaune’s t8n at BPO2, both sides against the same Blanc WETH; sizes are the installed runtimes. The differential regenerates the file on every run and fails on drift.
Six named transactions, not a workload: no average or aggregate is offered, and nothing here is deployed-chain gas. The size is the registry’s ninth row, published as a cost, and 17,481 bytes remains inside EIP-170 with room to spare.
There is no deployed original to measure against: the reference is OpenZeppelin’s contract compiled by the pinned solc and patched with the same asset, which makes the comparison fair and makes it no claim about any vault on chain.
Notes
What the build taught.
The vault’s public claim was written sentence by sentence against the theorems, and the map that resulted has three tables, not one: sentences a theorem carries, sentences only finite evidence carries — conformance with OpenZeppelin, and max* attainability as an actual successful call — and sentences not carried at all. A capacity sentence that first read as liveness was rewritten into the revert-cause statement the proofs actually give.
PRORATA was built to prove one hard thing about ratio pricing with no token standard in the way. The vault spent that investment: its dust and attack headlines are the étude’s accounting model instantiated over two contracts, with mint and withdraw made accounting steps of the same model. What the vault added in turn — the generic reverting-walk vocabulary its revert-cause theorems are stated in — sits in the shared layer, where the next contract can find it.
Boundary, restated: every theorem is about the exact compiled vault and the exact Blanc WETH installed at configured accounts — never WETH9, a production address, the OpenZeppelin source, or another asset; no CREATE is covered. The chain-level headlines assume the finite allowance-key noncollision premise and never discharge it; P3 and P4 hold for a realization faithful to the chain, not for the executed operations as such; the attack inhabitant is model-level; there is no liveness or gas-sufficiency claim, no Amsterdam coverage, and no ERC-4626 certification. The claim map and the registry are the authority.