Blanc/implementations/études
FMINT.
An étude, not a port: an ERC-20 token with the ERC-3156 flash-mint extension, pared down to the one hard thing flash minting adds — during a loan, supply is deliberately unbacked, and the books must still balance when the dust settles. Its headline: totalSupply = Σ balances at every observable point, under arbitrary executions and arbitrary reentrant borrower code.
It models no deployed contract. Its behavior is referenced against OpenZeppelin’s ERC20FlashMint at a pinned release, so every difference has an address — the same registry discipline the ports carry, applied to a contract composed from scratch to be the cleanest possible exhibit of one capability.
Fig. 1 — the FMINT gates, verbatim (fixtures 2026-08-12, coverage 2026-08-15). Note the honest budget: three selectors appear in branching borrower code but lack a callsite-execution witness, so the gate credits nine, not twelve — and the budget is shrink-only from here.
What the étude proves
Settlement against an arbitrary borrower.
Flash minting hands control to untrusted code in the middle of its own invariant’s violation — that is the capability, and the étude’s two headline families quantify over exactly that adversary: the books balance at every observable point, and a funded flashLoan frame settles cleanly, with no premise about the borrower at all.
A funded, non-static flashLoan frame over the exact compiled bytes ends in success, a deliberate revert, or the non-consensus fault channel — never a consensus exceptional halt — with the borrower’s code universally quantified: no hypothesis below mentions it.
theorem fmint_flashLoan_settles {sevm : Sevm} {pre : Devm} (hfork : CoveredFork sevm.benvStat.fork) {receiver token amount : B256} {data : Bytes} (h_code : some sevm.code.toList = Prog.compile fmint) (h_sel : Sevm.selector sevm = flashLoanSelector) (h_static : sevm.isStatic = false) (h_dec : Sevm.DecodesCallWithTail sevm flashLoanSelector [receiver, token, amount] data) (h_size : 196 + ceil32 data.length < 2 ^ 256) (h_token : token = sevm.currentTarget.toB256) (h_addr : ValidAdr receiver) (h_nof : B256.Nof ((Devm.getStor pre sevm.currentTarget).get supplySlot) amount) (h_stack : pre.stack = []) (h_mem : pre.memory = Mem.empty) (h_gas : flashLoanGas data.length ≤ pre.gasLeft) : (∃ post, exec ⟨0, sevm, pre⟩ = .ok post) ∨ (∃ post, exec ⟨0, sevm, pre⟩ = .error (.revert, post)) ∨ (∃ e post, exec ⟨0, sevm, pre⟩ = .error (e, post) ∧ NonConsensus e)
Read the premises — every one is about the caller’s frame and the calldata, never the borrower: a covered fork (Prague, Osaka, BPO1, or BPO2 — never Amsterdam), the exact bytes, canonical ERC-3156 argument encoding, the guards’ facts, a clean entry frame, and flashLoanGas data.length of gas — 4,429,379 at empty data, EIP-150’s retained sixty-fourths inside the figure. Even h_static is about the caller: a static caller halts at the mint’s first SSTORE by its own doing. NonConsensus names the channel outside every settleable halt — crypto and internal — so a consensus exceptional halt, outOfGas included, is unreachable however the callback burns. What makes a borrower-free statement possible is that Jaune’s interpreter is total: the hostile callee’s execution is supplied by totality, never assumed.
fmint_preserves_conserved -- one message frame, reentrancy included stateTransition_preserves_conserved -- one transaction addBlockToChain_preserves_conserved -- one block, from raw RLP chain_preserves_conserved -- every reachable state stateTransitionUsing_preserves_conserved -- …and the same three again on a addBlockToChainUsing_preserves_conserved *configured* chain, across scheduled chainUsing_preserves_conserved activations of the covered forks Stor.Conserved.of_empty -- the base case: all-zero storage conserved
A trichotomy is not a success theorem. Does flashLoan ever succeed?
pushbackDeliberately unclaimed. The whole flash surface is partial correctness, never liveness — nothing in the repository says a flashLoan call ever succeeds, and no page of prose may imply one does. That is the honest shape, not a gap: a success theorem for an entrypoint that calls out would carry the callee’s execution inside its own witness — arbitrary code, and for a flash loan, adversarial by design. Where no call leaves the frame the repository does construct success: fmint_totalSupply_succeeds, at exactly 2,218 gas — the first statement in the repository that a contract call succeeds.
Conserved — while the supply is deliberately unbacked?
pushbackYes, and the two facts do not compete. Stor.Conserved is an equality internal to storage — the supply word equals the sum of balances over all 2160 address-shaped keys, with supplySlot excluding itself by not being address-shaped — and it holds at every observable point, including mid-callback, with the mint landed and the settlement burn still to come. It is not solvency and not a stronger claim than WETH’s: during a loan the minted supply is unbacked by construction — that is the design, not a gap. One corollary is worth naming: every booked balance is bounded by the supply word, always.
Where does the invariant start? There is no constructor.
pushbackStor.Conserved.of_empty closes the genesis-installed case: all-zero storage is conserved because both sides are zero. It closes exactly that gap and leaves the other one open, in so many words: no initcode/CREATE deployment theorem exists, and nothing says an FMINT deployed by a transaction starts conserved — a declared non-claim, with a runnable source check in the README. The port that closed this class of gap end to end is WETH10, whose invariants stand on a derived deployment root.
Claim class, stated: the flash families live at message-call altitude, one frame — never the transaction; the constructed-revert rows pin this error and no data, while the settles_with_error family names an error channel, deliberately not a kind; and every statement is tied to the exact 1,257 bytes by fmintCode_compile — kernel evaluation, nothing added to the trusted base. The module docstrings are the authority on which claim is which.
How we know it does what it claims
The étude’s burden: prove the adversarial part.
For a contract whose defining move is handing control to untrusted code mid-flight, the evidence has to be strongest exactly where the adversary lives. The differential layer runs hostile borrowers on chosen inputs; the theorem layer quantifies over all of them.
▸Differential evidence — the sanity layer11 fixtures · 188 assertions · pinned EELS oracle
check-fmint.sh runs eleven committed fixtures through Jaune’s runner with the committed fmintCode as the lender’s code, every expectation filled by the pinned frozen EELS oracle. The scenarios lean adversarial: the full flashLoan success path, a wrong magic word, a reverting borrower, spectra over returndata shape, data length, and allowance arm, a depth-2 reentrant loan, a borrower that moves its minted balance away before answering, nine guard-and-dispatcher probes in one case, the ERC-20 view and transferFrom surface, and a Solidity-compiled borrower.
The harness hardens four ways beyond the WETH suite. A scenario manifest is cross-checked against the directory, so a deleted case fails the gate instead of shrinking the “all PASS” count. Every fixture’s lender account must be byte-identical to the committed 1,257-byte literal. Each of the twelve rejected probes asserts a discriminating clean-failure triple — success flag 0, RETURNDATASIZE + 1 = 1, and an in-EVM gas floor — and a committed falsifier table shows each of the three failure shapes the old bare revert produced breaks at least one leg. And every case declares its expected log sequence at generation time — generation aborts if the declaration disagrees with what the oracle executed, moving the question from “do two implementations of our bytecode agree” to “does our bytecode match the specification we wrote down.”
One deliberate diversity exercise: every borrower is a real Blanc program compiled by Blanc’s own compiler, except one — a pinned, digest-verified solc-compiled borrower whose independent ABI decoder recovers, word for word, the five callback arguments the suite claims are sent. It is one borrower on chosen inputs; it widens no theorem, and the suite says so.
▸Proven functional specifications — the quantified layerflashLoan spec · rollback · error genre
The conservation ladder and the settlement trichotomy — the étude’s substantive apex — are stated in full in the results section above. This layer is the endpoint specification beneath them: how a flashLoan execution is shaped when it succeeds, and how it is shaped when it does not.
fmint_flashLoan_spec -- the headline: factors a given successful execution through the canonical callback window no_success_of_* -- 7 corollaries ruling executions out rollback_of_no_success (+10) -- frame-level state restoration, 11 rows settles_with_error_of_* (+6) -- error genre, 13 rows: 7 name the error channel, 6 construct .revert with no data, exactly
The scope notes are part of the claim, and the module docstrings are their authority. The headline takes four premises — canonical calldata, a size bound, frame freshness, and the selector — beside the covered-fork premise every frame theorem now carries, so non-canonical encodings are out of scope, and the registry says so. Two corollaries (no_success_of_callback_never_magic, no_success_of_callback_never_returns_word) quantify over the callback boundaries the headline could produce, not over the receiver’s code — the weaker, honest form, chosen because the boundary is pinned by equations rather than proved unique. Every rollback claim names a frame, never a transaction. And the compile witness fmintCode_compile (kernel evaluation, nothing added to the trusted base) ties all of it to the exact 1,257 bytes.
Deviations
Twenty-six rows against a pinned reference.
An étude has no deployed original, so the registry pins the prevailing implementation instead: OpenZeppelin’s ERC20FlashMint at release v5.7.0, tag commit and reference files locked. FMINT_DEVIATIONS.md holds twenty-six rows spanning the flash surface, events, the ERC-20 surface, storage and collision handling, failure encoding, value handling, metadata, and the reentrancy window — each with a stance and a fixture-evidence citation, including an honest “no case in this suite” where the suite does not exercise a row. Three rows are representative of how the arguments run; the registry is the authority on all twenty-six.
Revert data: no error machinery, anywhere
deviation — row 20OpenZeppelin raises typed custom errors with arguments. FMINT reverts with empty returndata on every failure path — every revert site in the runtime is PUSH0 PUSH0 REVERT.
The argument: deliberate. Blanc carries no reasons, selectors, or messages on any failure path; what the discipline buys is a single, provable failure shape — the clean-failure triple the fixtures discriminate — and the registry row records the whole history of the normalisation that achieved it, including the three divergent failure shapes it replaced.
Storage layout and collision handling
deviations — rows 17–18Balances live at raw address words and allowances at keccak256(src ‖ dst), with the same fail-on-collision guard as WETH: in the exceptional case where an allowance key collides with a balance key, the operation refuses rather than writing through a third party’s balance.
The argument: the layout is proof-oriented and claims no compatibility with Solidity’s mapping scheme; refusal-on-collision converts an inexpressible corner into a clean revert. The design is shared with the WETH port — one decision, recorded in both registries, implemented once in the shared modules.
The comparison is behavior, not implementation
standing scopeThe registry compares observable behavior only — it never claims shared storage, source, or bytecode with the reference, and rows cite Blanc’s side by declaration name rather than line number, because names do not rot.
The argument: the reference exists so that every difference has an address and a defence. Rows the suite cannot exercise say so in their evidence column rather than borrowing credibility from neighbouring rows.
Deltas
What is measured, and what has no counterpart.
| quantity | value | status |
|---|---|---|
| runtime size | 1,257 B | committed literal, byte-checked by every fixture |
| totalSupply gas | 2,218 | proved equation, with a constructed successful run |
| revert-site normalisation | 1,217 → 1,257 B | exactly two bytes per revert site |
Closed forms and maxima for the remaining paths ship as lemmas in FmintGas.lean. No reference-side gas comparison has been run for FMINT, and none is claimed.
There is no deployed original, so there is no size or per-path gas delta to report — that is the étude trade, taken knowingly: the reference pins behavior for the registry, not an artifact to race.
One boundary is load-bearing enough to restate wherever sizes are stated: FMINT compiles one runtime and has no constructor, so no deployment theorem exists — conservation is proved to hold from a genesis installation (all-zero storage is conserved because both sides are zero), and nothing says an FMINT deployed by a transaction starts conserved. A declared non-claim, with a runnable source check in the README.
Notes
What the étude taught.
Flash minting is the hardest small thing a token can do: it hands control to an adversary in the middle of its own invariant’s violation. Porting a production flash minter would have buried that capability under a production surface; composing a minimal one made the adversarial theorems the whole contract. The étude then paid forward: the callback-crossing machinery and the settlement method built here are what made WETH10’s 27-selector surface a day’s work rather than a season’s.
The clean-failure discipline was discovered here — the old bare revert produced three observably different failure shapes, one of them burning the frame’s whole gas — and the fix landed in the one shared definition, normalising every revert site in both FMINT and WETH at once. The sibling-module rule (no contract imports another’s modules; shared things move upstream) is what made a two-contract fix a one-line diff radius.
Honesty budget, restated: three selectors lack callsite-execution witnesses and the coverage gate says so; the flashLoan corollaries are not one kind of theorem and their docstrings say which is which; no liveness is claimed for flashLoan; and the solc borrower is decoder diversity, not a second proof.