The contract
Twenty properties, executed
Compiled with solc 0.8.26, optimizer 200 runs and run on a real EVM by every build, through an eth_call state override on Robinhood Chain — no testnet, no key, no funded account. Then the same contract is broken 8 ways and the suite has to notice.
| Property | ||
|---|---|---|
| P1 | the first deposit mints, and redeeming it all returns exactly what went in | held |
| P2 | rounding never favours the holder, at every size | held |
| P3 | a stray transfer moves no price at all until harvest accounts for it | held |
| P4 | the inflation attack is unprofitable: the victim keeps 99.9% after a 100x donation | held |
| P5 | redeem pays exactly what previewRedeem quoted, to the wei | held |
| P6 | deposit mints exactly what previewDeposit quoted | held |
| P7 | totalAssets tracks the accounting rather than the token balance | held |
| P8 | a cut above the cap reverts — from the owner and from the constructor — and one at the cap is accepted | held |
| P9 | a stranger reaches none of the four owner-only functions | held |
| P10 | harvest charges exactly the cut on the income and no more | held |
| P11 | accrued cut sits outside every holder's claim and survives a full exit | held |
| P12 | collect cannot move a wei more than has been accrued, and never touches principal | held |
| P13 | another holder arriving or leaving moves the share price by nothing | held |
| P14 | transferring an Etalon moves the claim and moves no price | held |
| P15 | a zero deposit, a zero redemption and the zero address all revert | held |
| P16 | THE RECORD EXISTS: a reading carries the block, the timestamp and the pair | held |
| P17 | at most one reading per block, however many times it is asked for | held |
| P18 | readings never go backwards in time or in height | held |
| P19 | allowance is respected, and an infinite one does not decay | held |
| P20 | everybody leaving empties the supply and strands no principal | held |
Sabotage
A suite that passes is evidence of nothing until you have watched it bite. Each of these is the same contract with one deliberate defect.
the classic donation vector, and the reason the accounting is tracked at all.
caught by P7, P10, P12
it is the only thing standing between a first depositor and rounding the second one down to almost nothing. ONE rather than ZERO deliberately: at zero the contract divides by zero and every property reverts, which catches it for the wrong reason — a crash is not the failure this defence exists to prevent. At one the contract works perfectly and only the attack finds it.
caught by P4
a ceiling an owner can raise is a floor.
caught by P8(revert)
the one function that moves money to the owner, pointed at the wrong pot.
caught by P12
an access modifier is a claim like any other.
caught by P9
a history anyone can pad is not a history, and the padding is free.
caught by P17
a rounding error that always favours whoever is leaving is a slow drain on everyone who stays.
caught by P2
it breaks no property — every property that exists still holds — and it hands the owner the principal. Only a mechanical read of the ABI surface can see a function that was ADDED.
no property saw it · caught by the ABI surface check
rescue() breaks no property — every property that exists still holds — and it
hands the owner the principal. It is caught by a mechanical read of the compiled ABI against a written-down
surface, which is the only kind of check that can see a function that was added. A hand-written list
of “functions the owner can call” would test the list.And then twenty-four thousand random operations
Twenty specific questions cannot reach the state nobody thought to construct. This drives the same contract with a seeded generator and checks 9 invariants after every single call.
| Invariant, checked after every operation | |
|---|---|
| I1 | every claim together never exceeds what the Bar owes |
| I2 | the token balance always covers principal plus the cut charged |
| I3 | totalSupply is exactly what was minted, tracked outside the contract |
| I4 | a round trip out and back never gains a holder anything |
| I5 | the share price never falls, at any point, for any reason |
| I6 | the cut never exceeds the cap that is a constant in the code |
| I7 | accrued is exactly what harvest charged minus what collect paid |
| I8 | a harvest splits into exactly the cut and the rest, computed independently |
| I9 | collecting more than has been charged always reverts |
| Deliberately broken build | Broke |
|---|---|
| collect can reach the principal | I9 at step 8 |
| the share conversion rounds toward the holder | I5 at step 15 |
| harvest forgets to charge the cut | I8 at step 0 |
Every seed is fixed and published in
data/fuzz.json, because a failing run that cannot be repeated is not a finding. Two of these
invariants were worthless when first written — one compared accrued against an expression
containing accrued, and another tracked fees using the number harvest itself
returned, so a build that charged nothing agreed with it perfectly. The control caught both.
And the page, separately
A property suite proves the contract. It says nothing about whether the front end asks it the right questions, and that gap is where a correct vault meets a broken page.
| Step | ||
|---|---|---|
| A1 | the page's creation payload deploys a Bar | held |
| A2 | and it lands at exactly the address the page predicted | held |
| A3 | the string constructor argument survived encoding (the Etalon has a symbol) | held |
| A4 | the uint16 and both address arguments survived (cut under its cap, asset correct) | held |
| A5 | the page's approve calldata is accepted by the REAL token | held |
| A6 | the page's previewDeposit quotes a non-zero number of shares | held |
| A7 | the page's deposit calldata mints exactly what previewDeposit quoted | held |
| A8 | and the real token actually moved out of the depositor | held |
| A9 | the page's balanceOf calldata reads back the Etalon it just minted | held |
| A10 | the page's previewRedeem quotes the exit | held |
| A11 | the page's redeem calldata pays exactly that, to the wei | held |
| A12 | the page's fringe calldata decodes the record field for field | held |
Run against real
NVDA at 0xd0601ce157db5bdc3162bbac2a2c8af5320d9eec on Robinhood Chain. The balance was
written into the token’s own storage by the same override, at a slot that is discovered rather than
assumed — namespaced openzeppelin.storage.ERC20 — because a wrong slot overrides nothing and the failure then looks
exactly like a contract bug.
What it does not claim
None of this is an audit. It is a set of properties somebody chose, executed honestly, with the suite itself tested against deliberate defects. The list of properties is the limit of what it can tell you, and the eighth sabotage is on this page precisely because it shows where that limit is.
The contract is not deployed by anyone. The app deploys one from your wallet, which makes you its owner and the only person who can set its cut or collect its fees.