The contract
28 properties, executed
On Robinhood Chain at block 56,946,135, through an
eth_call with no to.
No testnet, no toolchain, no funded account, no private key.
What each one asserts
| # | Property |
|---|---|
| P1 | Shares are issued against the assets that actually arrived. |
| P2 | Deposit then redeem never returns more than it took. |
| P3 | A bare transfer into the vault cannot move the share price. |
| P4 | A partial redemption settles and leaves the rest. |
| P5 | Below minHarvest, glean() reverts — and reverts with NotRipe, not for some other reason. |
| P6 | At exactly minHarvest it runs. |
| P7 | Gleaning raises the share price. |
| P8 | The caller is paid exactly the bounty rate, to the wei. |
| P9 | booked + cut + bounty equals the pending amount exactly, on an amount divisible by neither rate. |
| P10 | After a glean the tracked counter equals the real balance. |
| P11 | Cadence-independence. Identical income gleaned once and gleaned twenty times leaves depositors with the same assets and gleaners with the same pay. |
| P12 | And it survives rounding: the uneven split drifts, if at all, in the depositors’ favour. |
| P13 | Redeeming before a glean really is worse than after one — the disclosure, executed. |
| P14 | The owner cannot set the protocol cut above its hard cap. |
| P15 | The owner cannot set the gleaner bounty above its hard cap. |
| P16 | A stranger cannot move either rate. |
| P17 | The owner cannot reach the vault asset through rescue(), pending fees included. |
| P18 | rescue() does recover a stray token that is not the asset. |
| P19 | Redeeming somebody else’s shares needs an allowance. |
| P20 | And the allowance is actually decremented. |
| P21 | previewDeposit matches deposit exactly. |
| P22 | previewRedeem matches redeem exactly. |
| P23 | pricePerShare() has real resolution — it quotes a whole share, not one share unit. |
| P24 | A fee-on-transfer token is credited what arrived, not what was requested. |
| P25 | A transfer hook cannot re-enter deposit. The property fails if the hook did not fire. |
| P26 | And cannot re-enter glean. |
| P27 | Zero-value calls are refused rather than silently doing nothing. |
| P28 | The classic inflation attack on an empty vault returns the victim everything. |
All 28 hold. If one did not, the run would stop there rather than continue to the sabotages: a property that is already red appears in every sabotage's caught-by list and makes a suite look as though it bites on everything.
The sabotages
A suite that has never been shown to fail is a suite nobody has tested. The contract is compiled again with one deliberate defect at a time, and each defect must be caught by a named property. Each sabotage's anchor has to match the source exactly once — a drifted anchor would compile the untouched contract, pass everything, and report a hole that was never there.
| Defect | Caught by |
|---|---|
| read assets from balanceOf instead of the tracked counter | P3 |
| let glean() run at any pending amount | P5 |
| pay the gleaner a fixed reimbursement instead of a proportion | P8, P11, P12 |
| let the owner set the gleaner bounty above its hard cap | P15 |
| let the owner set the protocol cut above its hard cap | P14 |
| let the owner rescue the vault asset, pending fees included | P17 |
| let anyone redeem anyone else’s shares | P20 |
| credit the amount requested rather than the amount that arrived | P24 |
| remove the reentrancy guard | P25 |
| pay the gleaner without deducting the bounty from the harvest | P9, P10, P11, P12 |
| quote one share UNIT instead of one whole share | P7, P23 |
| remove the virtual share offset from both conversions | survives — see below |
| add an owner-only function that empties the vault | the ABI surface check |
The two that survive, and why that is the finding
Removing the virtual share offset breaks nothing. The attack it defends
against is already closed by tracked accounting: the attacker's donation never reaches the
counter, so it never touches what the next depositor is quoted. Property 28 runs the classic
inflation attack and the victim recovers everything either way. Two locks on one door, and the
offset is the optional one — it is kept because it costs nothing and because
pricePerShare() needs the extra decimals to have any resolution at all.
Adding an owner-only function that empties the vault is invisible to every
property, because no property enumerates the ABI. It is caught by a mechanical read of
the compiled interface and by nothing else. A hand-written list of owner functions would have
tested the list. The sanctioned set is
rescue, setBounty, setCut, setTreasury, transferOwnership, and the build fails if anything else
appears.
Publishing only the caught ones would look like a suite that bites on everything. These two say where the floor is.
What this is not
It is not an audit. It is an adversarial self-review by the author, with every claim executed rather than asserted, and the difference matters: a review finds what its author thought to look for. Nothing on this site is deployed by us, and /state says which part is which.