Blanc/implementations/études

PRORATA.

The second étude, and the first of the arithmetic série: an ETH-native, non-transferable share ledger pared down to the one hard thing ratio pricing adds. The price is a ratio, so every deposit and every withdrawal rounds — and both the rounding and the ratio itself are attacker-influenceable, because anyone can move the numerator by sending ether. Its headline: with the virtual offset in place, no coalition of attackers can take out more than it put in, at any reachable state, with no honesty premise on any callee.

It models no deployed contract and claims no token standard — no events, no transferability, no ERC-4626 conformance. Four endpoints — deposit, withdraw, and the two conversion views — plus plain ether receipt, which mints nothing: the donation lever. Its arithmetic was brute-forced by an independent exact-integer oracle before it was proved, and a control shows the offset is load-bearing.

$ scripts/check-prorata.sh --no-build OK — prorata fixtures: 14/14 PASS, manifest/vector/runtime checks clean $ scripts/check-prorata-current-mainnet.sh --composed-prerequisites OK — prorata current-mainnet: 14 fixtures and 10-case three-runtime benchmark reproduce

Fig. 1 — the PRORATA gates, verbatim: the committed BPO2 fixture replay through Jaune’s runner, with every fixture’s pre-state code byte-checked against the committed literal (exact-candidate run 2026-09-03 UTC), and the current-mainnet lane that regenerates those fixtures and the three-runtime gas benchmark against the pinned BPO2 target, byte for byte (last green run 2026-09-02, credited by content identity).

343 B runtime no profit vs any coalition 14 fixtures / 131 assertions

What the étude proves

Rounding as an adversarial surface, closed.

Every deployed contract that prices anything computes a·b/d, every such computation rounds, and rounding is where value leaks. The étude proves the exact, zero-tolerance, adversary-quantified versions of the properties the industrial tier approximates — a four-rung ladder in ascending order of what nobody else states: rounding direction; preview/actual consistency with no tolerance parameter anywhere; cumulative dust conservation along arbitrary operation sequences; and the étude’s burden, the strategy-quantified impossibility of the inflation attack.

machine-checked

Theorem (attacker_no_profit, Blanc/ProrataAttackTrace.lean).

Over any closed attack trace realized along a configured chain from PRORATA’s deployment root — a coalition’s deposits, withdrawals, and donations interleaved around a victim’s deposit, with arbitrary callee code inside the quantifier — the coalition’s settled take is bounded by its own settled input.

theorem attacker_no_profit {cfg : ChainConfig} {deployed future : BlockChain}
    {ca : Adr} {root : DeploymentRoot cfg deployed ca}
    {coalition : Finset Adr} {victim : Adr}
    {steps : List (ProrataAccountingStep offset.toNat)}
    (trace : ProrataAttackTrace root coalition victim steps future) :
    outA victim coalitionCharge steps ≤ inA victim coalitionCharge steps

Read what is absent — no honesty, cooperation, or no-donation premise on any callee, and no premise on callee code of any kind: reentrancy after the pre-CALL settlement, receive-path donations, forced and native credit, and every ordering the realized carrier admits all sit inside the quantifier. The 2 ≤ O the pure result needs is discharged from the compiled offset O = 1000, not carried as a side condition. Beside it stand attacker_open_context — the same bound with an explicit outsideSubsidy term, for diagnosis over an open trace — and victim_loss_bound: a victim who deposited v against pre-credit state (S, B) and later exits its unchanged shares for p loses at most (B + 1) / (S + O) + 1 — one virtual-asset quantum above the price ratio, a bound the oracle found tight.

Blanc/Prorata*.leanthe ladder

mintN_never_overmints · payN_never_overpays        -- P1: every conversion rounds in the ledger's favour
deposit_price_nondecreasing · withdraw_price_…    -- P1: the share price never falls
prorata_convertToShares_eq_deposit_mint            -- P2: preview = actual, exactly, on the compiled bytes
prorata_convertToAssets_eq_withdraw_pay            -- P2: …and on the withdraw side
prorata_realized_dust_trace_exact                  -- P3: the rounding residue telescopes exactly along
                                                      real configured histories
DeploymentRoot.reachable_accountingInvariant       -- P3: Σ ledger = supply, supply ≤ cap, S ≤ O·B,
                                                      at every reachable state from the root
attacker_no_profit · attacker_open_context         -- P4: the theorem above, and its open-context form
victim_loss_bound                                  -- P4: one quantum above the price ratio

the virtual offset, priced

Mint and burn price at (B + 1) / (S + O): one virtual asset beside O virtual shares, in the OpenZeppelin decimal-offset shape. The price starts at 1/O and — the ledger’s core invariant — never decreases. The oracle found the edge before any proof did: at O = 1 a five-step transcript skims one wei of a victim’s rounded-away value, so 2 ≤ O is load-bearing and is the theorem’s hypothesis, discharged by the compiled 1000.

checks, effects, then the adversary

withdraw burns, updates the supply, and only then sends ether to the caller with all remaining gas — FMINT’s mid-flight hand-off to untrusted code, reused. The payout satisfies p ≤ B structurally, so the send cannot fail for want of balance; a rejected payout reverts the whole call, and a reentrant receiver is both a committed fixture and a case inside the theorems’ quantifier.

eleven rungs to the chain

The pure accounting is carried to real executions by a realized-execution ladder: one message call, a transaction, a transaction list, system messages, request calls, direct withdrawals, a block body, a configured block, a configured history, the frozen interface, and the realized P3 endpoint. Nine of the eleven rungs added no contract hypothesis; the two that did are discharged by the block carrier itself, so the endpoint rests on the deployment root, the chain reach, and the schedule premise every Blanc chain theorem now carries — that each fork it selects is Prague, Osaka, BPO1, or BPO2.

“No attacker profit” — proved over executions?

pushback

Over classifications consistent with real storage movement, and the distinction is stated rather than smoothed over. The realized carrier does not restate intra-block order in its type: every trace the construction produces is in that order, and every step is pinned to actual storage movement, but the honest reading of P4’s domain is “classifications consistent with the chain” rather than “executions”. P3 is untouched by this — strengthened, in fact, since it is universally quantified over realizing step lists and prorataTraceRealizes_exists_of_reachUsing guarantees every real reach over the covered forks has one. And there is no existence theorem for the attack trace: anti-vacuity for P4 rests on the committed fixture controls, as the frozen statement assigns.

Where do third-party donations go in the books?

pushback

To the coalition, in the closed form — which is why the open form exists. Forced and native credits — direct block withdrawals, coinbase and fee credits, foreign frames — record no actor, and the closed trace charges all of them to coalition input by frozen designation. That means attacker_no_profit can count third-party principal as coalition input; attacker_open_context charges it to outsideSubsidy instead, with a reference trace on record showing the subsidy term is necessary: a third-party donation of 1,000,000 wei lets a one-wei coalition take out 500,125.

Is this a vault?

pushback

No, and the étude says so at every altitude: no ERC-4626 claim — that needs an ERC-20 asset — no transferability, no economic viability, and no liveness. A donation that pushes the balance above 2¹²⁶ − 1 wei halts withdrawals until the balance falls, and the source comment says so rather than promising an exit. The claim class is the étude’s: composed from scratch, with the adversarial part proved. The port that buys the 4626 claim back — the same ledger over Blanc’s exact WETH, with a joint two-contract invariant — has since landed as its own contract: the ERC-4626 vault, with its own page and its own boundary.

Claim class, stated: P1 through P4 each hold within propext, Classical.choice, and Quot.sound; P2 and P3 are exact, with no tolerance parameter anywhere; every statement is tied to the exact 343 bytes by the compile witness; and the étude’s 51 audited theorems sit in the repository-wide axiom audit, with the P3 and P4 headline statements pinned character for character. The statement-freeze memo and the module docstrings are the authority on which claim is which.

How we know it does what it claims

An oracle, a control, and a compiler shadow.

An étude has no deployed original to run beside, so the evidence had to be built to falsify the statements themselves: an exact-integer oracle that searched for counterexamples before a proof was attempted, fixtures replayed through Jaune, and — for the efficiency question — an exact-surface shadow written twice in Solidity, so that “smaller and cheaper” has a referent that is fair.

▸The oracle — brute force before proof290 s battery · 230 million P4 search nodes · zero P1–P3 violations

An independent Python model with exact integers and no floats re-implements the ledger and checks every property at every transition: exhaustive reachable-state sweeps at offsets 1, 2, 3, and 10 to depth five and six — up to 151,631 unique states and 3.3 million transitions per configuration — and 320,000 randomized operations at 2⁹⁶ magnitudes. P1, P2, and P3 recorded zero violations. For P4 an exhaustive search over every interleaving of coalition deposits, withdrawals, and donations around a victim’s deposit explored 230,010,464 nodes and returned the theorem-deciding answer: profit is exactly zero for every offset of two or more, and positive — one wei — at offset one, with a fidelity-confirmed witness.

Two controls bracket the result. With the offset disabled, the classic first-depositor attack drains the victim entirely — one wei in, zero shares minted, the whole deposit lost — so the vulnerability is real when the defense is removed. On the real contract at O = 1000 the same shape costs the attacker 499,876 wei and the victim 249 of 1,000,000, inside every candidate bound; that transcript is now fixture 09-g6-real-offset-attack. The victim bound the theorems carry was the tightest of three candidates and is achieved with zero slack, so its + 1 is necessary.

The oracle also flagged, rather than smoothed, a margin: the withdraw product MAXS · (MAXB + 1) is a 252-bit value against a 256-bit word. Safe at the compiled caps, with four bits to spare and no room to widen either.

▸Fixture evidence — the sanity layer14 BPO2 blocks · 131 assertions · byte-checked runtime

check-prorata.sh replays fourteen committed blocks through Jaune’s runner at BPO2, each generated through the pinned current-mainnet target with its outer receipt status, scenario-specific post-state facts, and absence of logs asserted before writing: a genesis deposit, a donation that shifts the price, full and partial exits, the views, every arithmetic guard, all three nonpayable wrappers, an unknown selector, a reentrant receiver after checks-and-effects, a rejected payout with full rollback, and the frozen offset-attack transcript. The harness checks the manifest in both directions, byte-compares every pre-state PRORATA runtime against the committed prorataCode literal, regenerates the canonical arithmetic vectors, and carries two self-test falsifiers that must fail in isolated copies.

▸Proven functional specifications — the quantified layerP1–P4 · eleven rungs · twelve shared modules

The four rungs are stated in full in the results section. Beneath them, each endpoint has an effect theorem at body altitude and again at compiled-bytes altitude — prorata_deposit_exec_effect, prorata_withdraw_exec_effect, and their view counterparts — and the completion report audits every clause of the frozen statement against a named declaration, saying plainly where a clause is a composition of three theorems rather than one, and where one clause is not separately stated because it is arithmetic rearrangement of another.

What the étude left behind is as large as what it proved: twelve contract-neutral Execution* modules — retained trace carriers from messages through configured histories, ordered state replays, and effect transports — built to carry PRORATA’s accounting and hoisted to the shared layer, where the later contracts consume them whole. The arithmetic itself rests on Jaune’s MulDiv layer, landed additively for this étude, and the one generic fact the étude had to prove privately was queued as a hoist and has since landed upstream.

Deviations

No reference, so no registry — and a frozen statement instead.

PRORATA is referenced against nothing deployed and nothing vendored; its authority is its own statement-freeze memo, approved before implementation, and the arithmetic série map. What stands where a registry would: the completion report’s ledger of deviations from that frozen statement, and its list of what is not pinned down — published so that a reader citing P4 knows exactly what P4 quantifies over.

A hypothesis dropped, not added

deviation from the freeze — a strengthening

The frozen statement carried 2 ≤ O on the no-profit headline. The theorem as landed carries none: the compiled offset discharges it, and the parametric premise survives only on the pure attacker_no_profit_of_attackPath.

One carrier became two

deviation from the freeze — arity

The freeze named a single attack carrier. Stating the open-context bound needs something to carry the coalition/outside split, so the general carrier is the open trace with a per-step charge, and the closed trace is its abbreviation at the coalition charge — the frozen arity exactly, with outsideSubsidy definitionally zero.

Indexed by storage and balance, not by state

deviation from the freeze — representation

The realized carrier cannot be indexed by a world state, because a deposit’s pricing sees the balance immediately before its own incoming credit — a boundary that is no world state’s balance. That is the freeze’s own rule for which (S, B) a deposit observes, and the carrier follows it rather than the memo’s spelling.

Deltas

Against a shadow, not an original.

measured — committed benchmark, pinned compiler and target

quantity	value	status
runtime size, selected	343 B	committed literal, byte-checked by every fixture
exact-surface shadow, strict Yul	356 B	solc 0.8.36 via-IR, pinned; +13 B / +2,600 code-deposit gas
exact-surface shadow, Solidity legacy	440 B	same compiler, legacy pipeline; +97 B / +19,400
BPO2 receipt gas vs the Yul shadow	9 / 10	cases where Blanc is cheaper; net 162 gas over the suite; Yul wins the unknown-selector revert by 15
BPO2 receipt gas vs the legacy shadow	10 / 10	aggregate 502 gas over ten one-transaction blocks

Each benchmark row is one signed transaction in an independent BPO2 block through the pinned current-mainnet target, with identical envelopes across the three runtimes and zero semantic mismatch in receipts and projected state.

what an étude forgoes, and what it declines

There is no deployed original, so there is no delta against one. The shadows exist as compiler baselines — the same four endpoints, ledger, guards, and rounding, once in legacy Solidity and once in strict Yul — never as specifications; PRORATA’s frozen statement, proofs, oracle, and fixtures remain the authority.

Global optimality is not claimed: a 333-byte variant was assembled and tested, and rejected because its ten bytes would have made the recognized nonpayable routes dearer and every affected body proof longer. Aggregate gas totals are descriptive, not workload weights. And these are Jaune and pinned-target costs, not deployed gas.

Notes

What the étude taught.

falsify the statement before you spend the proof

The étude’s decisive finding cost 290 seconds of Python and no Lean at all. “Attacker profit is never positive” was the expected airtight headline; exhaustive search showed it false at offset one and true from two upward, stable across depth. The hypothesis went into the theorem before the first proof line was written, and the compiled offset later discharged it. The série makes this the standing order: every quantitative statement is brute-forced independently, with attained-tightness witnesses recorded, before proof trust is extended to it.

what the étude paid forward

The étude’s burden was arithmetic; its dividend was machinery. The realized-execution ladder and the twelve shared carrier, chronology, and effect modules were built here because nothing carried an accounting invariant from a message call to a configured history, and every contract since — the deposit contract’s open history among them — inherits them whole. The étude also priced its own upstream: the one generic floor-division fact it had to prove privately was recorded as a hoist candidate and landed in Jaune with the série’s next arithmetic layer.

Honesty budget, restated: P4 quantifies over classifications consistent with the chain, and no existence theorem for the attack trace is claimed; two rounding-direction clauses are three-theorem compositions and one is not separately stated; forced and native credits are charged to the coalition in the closed form; no liveness, token standard, transferability, or economic claim is made; and the compiler shadows are baselines, not specifications. The completion report’s evidence table, not this page, is the authority on each.