Blanc/implementations/études
DRIP.
The third étude: an ETH-native savings ledger pared down to the one hard thing a savings rate adds — compounding. A per-second accrual index chi grows by a fixed rate raised to the elapsed seconds, computed in 27-decimal fixed point by a Maker-shaped rpow, so every update rounds, and the rounding compounds. Its headlines: the rounding is certified to a two-sided band, a successful update never leaves a stale index, and the books of every configured history balance exactly, term by term, over the history’s own calls.
It models no deployed contract and claims no token standard and no Maker equivalence. Five endpoints — join, the one payable entry, mints units against the ether sent; exit burns units and pays out after its books are written; drip advances the index; and two conversion views — no events, no owner, no rate setter. The fixed rate compounds to 5% over a 365-day year, less rounding in the twentieth decimal — a figure the kernel checks rather than the prose asserting it.
Fig. 1 — the stack-certificate provenance gate, verbatim (run 2026-09-25 UTC): the finite 735-row table over the exact runtime, regenerated and byte-compared, whose soundness is a kernel-checked theorem rather than this script; and the repository-wide statement-pin gate, shown in its verdict wording at the current pin count, which pins DRIP’s twelve headline statements among the 460.
What the étude proves
Compounding, with the books closed.
Every contract that pays a rate over time multiplies an index by a fixed-point power, and every such power rounds — per multiplication, compounding with the exponent. The étude proves four rungs, each stated over the exact compiled bytes or the configured histories that run them: the one-call update and its certified rounding band; exact accounting over the history’s actual calls; no stale index and a bounded entitlement; and a clock-paired invariant with a monotone index.
From DRIP’s deployment root, along any configured history over the covered forks, any coalition’s actual cumulative exit receipts never exceed its actual principal plus the floor of its actual realized accrual — every term a fold of the history’s own DRIP calls, not of a reconstructed or idealized trace.
theorem history_transcript_entitlement (root : DeploymentRoot cfg base deployed ca) (coalition : Finset Adr) (history : ExecutionTrace.ConfiguredHistoryTrace cfg deployed future) (hcov : ∀ timestamp fork, cfg.forkAt timestamp = .ok fork → CoveredFork fork) : (transcriptTally scale.toNat freshNat scale.toNat 0 (history.dripCalls coalition ca)).paid ≤ (transcriptTally scale.toNat freshNat scale.toNat 0 (history.dripCalls coalition ca)).joined + (transcriptTally scale.toNat freshNat scale.toNat 0 (history.dripCalls coalition ca)).accrual / scale.toNat
Read the quantifiers — the coalition is any finite set of accounts, and the history is every configured chain history from the deployment root: arbitrary blocks, arbitrary other contracts, arbitrary interleavings of joins, drips, and exits. history.dripCalls projects the history’s own calls to DRIP, and dripTraceRealizes_transcript proves a realization exists whose call steps are exactly that projection — so the tally is of what the chain did. The deployment root is derived from a canonical creation step, not assumed, and it records that the deployment ran at a covered fork. cfg, base, deployed, ca, and future are the module’s section variables.
drip_compiled_drip -- R1: one compiled drip() sets chi to chi·rpow(elapsed)/S and stamps the clock to the block time drip_rpow_certified_band -- R1: the deployed rpow tree's two-sided error band drip_rpow_exact_telescope -- R1: the exact rounding identity behind it dripTraceRealizes_transcript -- R2: every history realized by its own DRIP calls history_transcript_accounting_exact -- R2: units·chi + residues + S·paid = accrual + S·joined history_transcript_balance_exact -- R2: balance + all paid = all joined + outside credit no_stale_index_success_callback_free -- R3: a successful drip() or join() leaves no stale index no_stale_index_settlement_exit -- R3: …and exit() at its settlement boundary history_transcript_entitlement -- R3: the theorem above realized_segment_certified -- R3: same total elapsed time, certified drift apart history_clockInv -- R4: the clock-paired invariant at the head timestamp history_chi_rho_mono -- R4: index and clock never fall
rpow squares and multiplies by the rate, rounding half-up at every step. The étude does not bound that error by a guess: an exact additive telescope accounts for every rounding at every node of the deployed computation tree, and the certified band follows from it — deliberately not a minimality statement. The runtime performs at most 62 rounded multiplications, and one year’s factor is a kernel-decided equation.
exit refreshes the index, writes the caller’s row and the total, and only then sends ether to the caller with all remaining gas — reverting the whole call if the send fails. The payout the call accepts is stated exactly, and a reentrant receiver is inside the history theorems’ quantifier rather than excluded by a premise.
A finite 735-row table records the stack height at every node of the exact runtime’s same-frame paths. table_checked shows the runtime and the table agree, and actual_entry_safe that every node reachable from entry stays within eight stack slots and steps safely — so stack depth becomes a checked fact about the bytes rather than a proof obligation at every endpoint.
Is this the Maker savings rate, verified?
pushbackNo. The rpow and the chi/Pie vocabulary are Maker-shaped, but nothing here claims equivalence with Maker’s contracts or any deployed bytes. DRIP is composed from scratch, ETH-native, with no rate governance at all: the claim class is the étude’s — the adversarial arithmetic proved, the rest declined.
Does the entitlement bound mean every holder can exit?
pushbackNo, and it is stated the other way round: it bounds what a coalition can take out, not what it can get. There is no solvency, liveness, or gas-sufficiency claim — accrual is paid from whatever ether the contract holds, so an underfunded exit may revert. The history theorems describe successful calls; the realization carrier is not claimed to reject every fictitious ledger, and no ledger uniqueness is claimed.
Claim class, stated: the étude’s 63 audited theorems sit in the repository-wide axiom audit — 54 within propext, Classical.choice, and Quot.sound, nine within smaller sets — and its twelve R1–R4 headlines are pinned character for character. Chain-level headlines take a schedule of covered forks — Prague, Osaka, BPO1, BPO2 — and the exit settlement theorem a covered frame fork; no Amsterdam frame or block is covered.
How we know it does what it claims
An oracle, the real arithmetic, and a replay.
An étude has no deployed original to run beside, so the evidence was built to falsify the frozen statement itself: an exact-integer oracle, the compiled arithmetic checked against it row by row, and a fixture population replayed through Jaune — each finite, none a theorem, and none asked to stand in for one.
▸The oracle — the frozen statement, executable38 frozen obligations · regenerated vectors · 6 corruptions caught
An independent Python model, with exact integers for the mathematics and explicit helpers reproducing every 256-bit multiplication and addition guard of the frozen runtime, carries the statement’s 38 scenario obligations — checks-effects-interactions and rollback included. Its committed vectors are regenerated byte for byte on every run, and its own boundary record says what it is: a falsifier and fixture oracle, not proof evidence.
▸The arithmetic, and the replay — the sanity layer39 arithmetic rows · 91 BPO2 fixtures · 137 transactions
check-drip.sh compares 39 rows of the real Lean arithmetic with independently computed Python integers, then replays every committed fixture through the pinned Jaune at BPO2: 91 fixtures and 137 transactions spanning deployment, first and later joins, drips from the same second to the maximum elapsed window, full and partial exits, and every guard — each block’s receipts, blooms, and trie roots derived and bound to its decoded header before replay. Finite arithmetic comparison is not the deployed-loop theorem, and the gate says so.
▸Proven functional specifications — the quantified layerR1–R4 · a derived deployment root · a concrete history
The four rungs are listed in the results section. Beneath them, canonicalDeploymentStep_establishes_root derives the deployment root from a canonical creation step, and configuredHistory_has_head_timestamp shows every configured history from a root has a head block, so the clock invariant’s antecedent is never vacuous.
The carrier is also inhabited by an actual chain: concreteHistory_realizes exhibits a concrete history — a join, a three-second drip, and an exit — through real blocks, and the kernel proves, among its facts, the join transaction’s receipt at 76,144 gas.
Deviations
No reference, so no registry — and what the freeze did not get.
DRIP is referenced against nothing deployed; its authority is its own frozen statement. Where the tree answers that statement differently, the source says so in its docstrings, and two of the answers are theorems.
Exit freshness, at the settlement boundary
deviation from the freeze — scopeThe freeze asked for one no-stale-index statement over all three mutating selectors. exit writes its books before the payout call, so its post-state is the resumed child’s, and carrying the clock equation through that child needs a block-indexed frame ladder the shared layer does not yet have. So drip and join get the post-state statement, and exit gets the same two equations at its settlement boundary, with the accepted payout the only remaining distance.
A drafted witness that no chain can realize
deviation from the freeze — provedThe design drafted its concrete history’s call kinds with one second of elapsed time in total, while the witness chain moves the clock by five. Rather than bend the carrier, concreteHistory_not_draftedKinds proves no realization has the drafted kinds, and the realized history carries the true ones.
A band, not an optimum
not claimedThe certified band bounds the deployed tree’s rounding in both directions; it is not a claim that no tighter band exists, rpow’s monotonicity in the exponent is not claimed, and the segmentation drift bound is certified, not minimal.
Deltas
No original, so no delta — only the measured costs.
| quantity | value | status |
|---|---|---|
| runtime size | 1,762 B | committed literal; kernel-checked length |
| creation code | 2,001 B | committed literal; kernel-checked length |
| deployment | 479,909 | receipt gas, genesis deployment fixture |
| join, first | 70,465 | receipt gas |
| drip, same second | 26,076 | receipt gas |
| drip, one year | 37,880 | receipt gas; the rpow loop at 31,536,000 s |
| exit, full | 34,591 | receipt gas |
Each row is one committed fixture’s receipt through the pinned current-mainnet target at BPO2, intrinsic gas included.
There is no deployed original and no committed compiler shadow, so there is no delta to publish; the figures are costs, not wins. They are Jaune and pinned-target costs, not deployed gas, and no aggregate or workload weighting is offered.
Notes
What the étude taught.
PRORATA’s attack theorems quantify over classifications consistent with the chain. DRIP went one step further: its accounting identities are folds of the history’s own DRIP calls, and a separate theorem proves those calls are exactly a realization’s steps. What is tallied is what the chain executed — with the honest residue that the carrier may still accept ledgers no chain produced.
The finite stack certificate — an abstract checker, its soundness theorem, and a reusable table producer — was built for DRIP and first reused by the proxy pair. Settled-frame, observed-accounting, and frame-time carriers, a prefix-transport spine, and five generic execution-identification lemmas were hoisted from its proofs into the shared layer, and Jaune’s rpow layer is the arithmetic it stands on.
Honesty budget, restated: exit freshness is proved at the settlement boundary, not the post-state; the band is certified, not minimal; the realization carrier is not claimed to reject fictitious ledgers; no solvency, liveness, gas-sufficiency, token-standard, or Maker equivalence claim is made; and no Amsterdam frame or block is covered. The module docstrings are the authority on each.