Why it cannot fall.

The claim

The algebra

A redemption.

Let V be the ETH held by THE COUNTER, S the circulating supply, f = V/S the floor, t the exit toll, and q < S a redemption.

The holder is paid p = (V/S)·q·(1−t), and q tokens leave circulation for the dead address:

V′ = V − (V/S)·q·(1−t)
S′ = S − q

f′     V′     V[S − q(1−t)]     S(S − q)        S − q + qt         q·t
── =  ──  =  ───────────── · ──────────  =  ───────────  =  1 + ─────  ≥  1
f      S′     S(S − q)             V            S − q            S − q

Equality holds only at q = 0 or t = 0. The toll is the entire reason an exit is accretive rather than merely neutral. At a zero toll a pro-rata redemption leaves the floor exactly where it was. That is asserted directly in test_zeroToll_isNeutralNotAccretive, because a design whose headline claim is only true for a parameter it happens to ship with should say so out loud.

A harvest, a donation, a transfer.

A harvest or a donation raises V and leaves S alone, so f′ = (V+h)/S ≥ f. A plain transfer between holders moves neither, so f′ = f. That one is asserted every time the invariant handler trades.

Rounding.

The payout is computed as weiOut = (V · q · (BPS − toll)) / (S · BPS) in integer arithmetic, which rounds down. A smaller payout leaves a larger V′, so the realised floor lands at or above the real-valued one. The algebra above is a lower bound, not the claim.

The dependency list

What the floor needs in order to be true.

The reading floor() is a single division over two values that anyone can pull from the chain in one call, so there is no oracle to be wrong, no keeper to stop running, no lender to default and nobody on the other side of it. There is also no owner, no admin key and no upgrade path, which is a property of the deployed bytecode rather than an undertaking anyone has given.

Two claims are easy to blur together here, so they are worth separating. The floor arithmetic needs none of the above. The inflow does ride pons, since it is their curve, their fee policy and their token. What it stopped riding is pons's sweep operator, because THE COUNTER is the curve's own deployer and now calls sweepFees for itself.

The proof

74 tests, five suites.

Coverage: 100% of lines and 100% of functions in src/PawnCounter.sol.

The control on the control

A property that cannot fail is not evidence of anything.

A property that passes for a broken contract as readily as a correct one is not evidence. test/mutants/LeakyCounter.sol is the same contract carrying the single most plausible bug in the design: it reads the supply after the burn, so a holder is paid at the higher floor their own exit creates. It looks generous and survives a casual review.

Run against identical input, 200 redemptions each:

The same sequence drives the two contracts in opposite directions, which is what makes the property load-bearing rather than decorative.

A note on the control's own construction. The two counters were first given a shared token, and because they share 0xdEaD each contract read the other's burns as its own supply reduction, which made the mutant's floor appear to rise. Each mutant now gets its own token. A negative control that has not itself been falsified is just another assertion.

What is not proved here

• That pons behaves as its source saysEvery address and rate was read off mainnet with cast and the whole launch was rehearsed against the live factory on a fork. That is strong evidence, not a guarantee about future pons behaviour.
• That the market price stays near the floorIt need not. The floor is a bid, not a peg, and arbitrage is what connects them.
• That anyone will trade it at allIf volume is zero the floor stays at zero, and the front page will say zero.
• That this is auditedIt is not. The tests are public and so is the source. That is a different thing and it is not going to be called an audit.