Executed, not asserted
Every claim, run on the real EVM
No testnet, no fork, no toolchain, no funded account and no private key. eth_call with no to executes creation code on Robinhood Chain’s own evaluator against real state and returns whatever the constructor returns.
The properties
One per eth_call, because this node caps call gas server-side and because a revert can then only have come from the property in that call.
| # | What it holds | Result |
|---|---|---|
| P1 | Share decimals are the asset’s plus the offset, and an empty vault starts at startPrice | holds |
| P2 | deposit mints exactly what previewDeposit quoted | holds |
| P3 | redeem pays exactly previewRedeemFor and burns exactly the shares asked for | holds |
| P4 | transfer moves exactly the amount asked, in both fee modes | holds |
| P5 | An infinite allowance is not decremented; a finite one is | holds |
| P6 | A same-block round trip never profits the depositor | holds |
| P7 | previewRedeem never over-quotes, for any owner | holds |
| P8 | Withdrawing exactly maxWithdraw does not revert | holds |
| P9 | A donation moves neither the price nor totalAssets | holds |
| P10 | The first depositor cannot round the second to zero | holds |
| P11 | The identity: what the ratchet took is f times (crest − startPrice) | holds |
| P12 | A path that ends where it started is still charged, and the charge is the peak | holds |
| P13 | Crystallising more often never charges less | holds |
| P14 | A vault that only ever falls is charged nothing | holds |
| P15 | Crystallise is permissionless and pays its caller nothing | holds |
| P16 | The fee is dilution, so it moves no assets out of the vault | holds |
| P17 | giveUp equals the price the vault actually lost, measured by the harness | holds |
| P18 | The basis fee is path-independent: same endpoints, same fee | holds |
| P19 | A holder who is flat pays nothing, however far the vault travelled | holds |
| P20 | The fee cannot be shed by moving the shares to a fresh address | holds |
| P21 | The weighted-average basis is exactly the weighted average | holds |
| P22 | previewRedeem is a floor and previewRedeemFor is the answer | holds |
| P23 | withdraw delivers exactly the assets asked for | holds |
| P24 | A basis vault has no ratchet to crystallise, and says so | holds |
| P25 | A transfer hook cannot re-enter deposit, and the exploit fires | holds |
| P26 | sweep moves donations and only donations | holds |
| P27 | A rebalance changes what the vault is worth by nothing, and a stranger cannot call it | holds |
| P28 | Recovering the fee’s own drag is a new record and is charged | holds |
| P29 | The fee is capped in code and there is no function that can set it | holds |
| P30 | holds | |
| P31 | holds |
The sabotages
The contract is compiled again with one deliberate defect at a time. A suite that bites on everything is a suite nobody has found the floor of, so the ones expected to survive are kept and say why.
| Defect | What it breaks | Caught by | |
|---|---|---|---|
| giveup-restates-intent | giveUp records the drop it MEANT to take instead of the price the vault actually lost | P17 | caught |
| fee-cap-removed | the constructor stops capping the fee | P29 | caught |
| high-water-is-the-crest | highWater() returns the crest rather than the price the last record left | P28 | caught |
| no-record-test | the ratchet charges on every crystallisation, not only on records | P11, P12, P14 | caught |
| crest-net-not-gross | the crest is recorded against the net price, so fees already taken hide later records | P28 | caught |
| basis-reset-on-transfer | a receiver's basis is set to the current mark, so a sender sheds the fee by moving shares | P20 | caught |
| basis-ignored | the exit fee is charged on the whole value rather than on the gain | P8, P19, P22, P23 | caught |
| preview-overquotes | previewRedeem returns the gross amount on a basis vault, which over-quotes every holder | P7, P22 | caught |
| donation-priced | totalAssets reads balanceOf instead of the tracked counters | P9, P10 | caught |
| no-mutex | deposit drops its reentrancy guard | P25 | caught |
| sweep-takes-principal | sweep moves the whole balance rather than only what was donated | P26 | caught |
| rebalance-free | a rebalance does not charge the manager for what it takes | P11, P14, P18, P19, P27, P31 | caught |
| rebalance-rounds-down | the manager's payment for the position is floored instead of rounded up | P30 | caught |
| stranger-rebalances | the manager check is dropped from rebalance | P27 | caught |
| fee-on-transfer-credited | deposit credits what was requested rather than what arrived | P25 | caught |
| no-offset | the virtual share offset is removed | P1, P12, P19 | control |
| added-rescue | an owner-only rescue() that can take anything is added to the surface | ABI surface | expected to survive |
giveup-restates-intent
giveUp records the drop it MEANT to take instead of the price the vault actually lost
The one that makes identityResidual() a tautology. P11 cannot see it; only the harness measuring the price itself can.
no-offset
the virtual share offset is removed
The inflation attack is closed by tracked accounting, not by the offset. P10 must still pass without it, or the site is crediting the wrong defence.
added-rescue
an owner-only rescue() that can take anything is added to the surface
It changes no property, because no property calls it. It is seen ONLY by the mechanical read of the compiled ABI below — which is why that check exists, and why a hand-written list of owner functions would have tested the list.
Four things this suite got wrong before the contract did
Every one of these was found by the sabotage pass rather than by writing more tests, and each is why the pass exists.
Six properties were red on the correct contract
They then appeared in every sabotage’s caught-by list, which looks exactly like a suite biting hard. The runner now fails the build if any property is caught by every real sabotage.
A guard was “working” because something else also said no
The stranger who was supposed to be refused a rebalance held no tokens and no approval, so the call died on an allowance and the property passed against a vault with its manager check removed entirely. The stranger is armed now: it must be able to succeed but for the guard.
A state variable was written and never read
highWater was stored, and a sabotage that changed it survived because nothing could see it. It is a view derived from crest and giveUp now, which is exactly what it always was.
One sabotage needed a vault sized by measurement
The defect that makes giveUp restate its own intent rather than measure the loss only shows when the fee mint cannot land on the price it aims at. A ten-dollar vault rounds on none of twelve steps, a one-dollar vault on two, and a quarter-dollar vault on eleven. The property uses a quarter of a dollar, and it says so.