Executed, not asserted
23 properties, 16 sabotages
All of it on Robinhood Chain's own EVM, through eth_call with no to —
which runs creation code against real chain state and returns whatever the constructor returns. No testnet, no
fork, no funded account, no key, nothing installed.
A property that cannot fail is worse than no property
Three rules this suite enforces on itself, each of which was learned by having got it wrong:
A red property proves nothing. One that fails on the correct contract appears in every sabotage's caught-by list, and the run reports coverage it does not have. Red properties are excluded from the sabotage runs, and the whole run fails if any property is caught by every sabotage.
A stale anchor breaks nothing. If a sabotage's search text no longer matches, it compiles the untouched contract, every property passes, and the result reads as a hole — when the real cause is that nothing was broken. A missing anchor throws.
A guard is not tested by watching something else refuse. With a guard removed, the call very often still reverts, one line further down, for an unrelated reason. Every negative property here checks the error selector, not merely that something threw.
Two the suite caught in itself
P6 tested nothing, and reported a bare revert. Deposit to an address with no code was supposed
to fail with NotAToken; it failed with an empty buffer instead, because balanceOf on an
empty address makes solc's own decode revert with no data — before the contract's check was ever reached. The check
moved ahead of the first balance read.
The reentrancy sabotage was uncatchable, and the property was green. Armed to re-enter
deposit directly, the token itself became msg.sender — an address with no balance and no
allowance — so the inner call reverted on the allowance whether the latch was there or not. Removing the latch
changed nothing and the property passed, testing the token's empty wallet. The re-entrant caller is funded now.
The ABI surface
Every external function is read out of the compiled ABI and checked against what this contract is allowed to expose. Nothing outside the declared interface — no owner, no upgrade path, no pause, no fee.
The properties
| # | result | what was executed |
|---|---|---|
| P1 | holds | deposited 100.000000 and booked exactly 100.000000 |
| P2 | holds | asked 100.000000, 97.000000 arrived, 97.000000 booked |
| P3 | holds | a token that reports success and moves nothing is refused |
| P4 | holds | an empty return buffer is accepted, and the arrival is still weighed |
| P5 | holds | `false` is a refusal, and it is read |
| P6 | holds | an address with no code is not a token, whatever it returns |
| P7 | holds | a half-word return is malformed, not `true` |
| P8 | holds | 40.000000 left, 40.000000 arrived, 60.000000 still booked |
| P9 | holds | 50.000000 left the contract and 48.500000 arrived; both are returned |
| P10 | holds | a contract may deliver less than asked; it may never lose more |
| P11 | holds | the callback ran, was refused, and 50.000000 was credited once |
| P12 | holds | 30.000000 taken from outside: the deficit is named and the quote follows the balance |
| P13 | holds | exactly 70000000 is payable and 70000001 is not |
| P14 | holds | an unattributed 25.000000 is claimable once, and only once |
| P15 | holds | booking takes the 25.000000 nobody was credited with, and not the 60.000000 that was |
| P16 | holds | the contract is not a valid payee, and neither is address zero |
| P17 | holds | the first exit leaves the second holder whole, and the second is paid in full |
| P18 | holds | the token said `frozen`, and that is what the caller is told |
| P19 | holds | booked never exceeded held across 12 operations on a fee token |
| P20 | holds | zero is not a settlement |
| P21 | holds | the whole 97000000 came back out and nothing was stranded |
| P22 | holds | the balance runs out first-come, and the quote says so instead of promising 40.000000 |
| P23 | holds | asked for 50.000000, 20.000000 left, and exactly 20.000000 was debited |
The sabotages
The shipping contract, compiled again with one deliberate defect at a time. Each must be caught by a specific, related property, or be declared a survivor with its reason.
| the defect | what it does | result |
|---|---|---|
| credit-the-request-not-the-arrival | a deposit credits the number in the call instead of the difference between two balances — the exact bug this whole site is about | caught by P2, P9, P19, P21 |
| nothing-arrived-guard-removed | a token that returns true and moves nothing is credited with zero instead of being refused | caught by P3 |
| no-code-check-removed | the address is no longer required to hold code, so a call to an empty address is taken for a transfer | caught by P6 |
| false-return-accepted | the bool is no longer read, so a token that declines by returning false is treated as having paid | caught by P5 |
| short-return-decoded-anyway | a return value shorter than a word is passed to abi.decode rather than refused | caught by P7 |
| revert-reason-swallowed | the token's own revert reason is replaced by this contract's error, so every caller debugs the wrapper | caught by P18 |
| reentrancy-latch-removed | the latch is gone, so a token with a transfer hook can re-enter between the two balance readings and be credited twice | caught by P11 |
| quote-ignores-the-balance | available() reports the credit and never asks whether the contract is still holding it | caught by P12, P13, P22 |
| debit-the-request-not-the-departure | a withdrawal debits the number in the call rather than the measured departure, so a token that moves less strands the difference | caught by P23 |
| overdraw-guard-removed | the contract may end up lighter than the holder authorised, which is the one shortfall it must never accept | caught by P10 |
| zero-withdrawal-allowed | a withdrawal of nothing settles and emits, recording a movement that did not happen | caught by P20 |
| book-claims-the-whole-balance | booking an unattributed surplus takes the entire balance, including units already credited to somebody else | caught by P14, P15 |
| deposit-may-credit-the-contract | the contract can be credited to itself, which makes its own balance both the measurement and the subject | caught by P16 |
| withdrawal-may-pay-the-contract | a payout to this contract or to address zero is allowed, so the payee delta is measured against the wrong account | caught by P16 |
| deficit-reported-as-zero | the shortfall a token created from outside is rounded away to nothing rather than named | caught by P12, P22 |
| deposit-event-forgets-the-request | the Deposited log emits the arrival twice instead of the request and the arrival | survives every property runs through eth_call, which returns no receipt and no logs — this suite structurally cannot see an event, and a defect it cannot see is declared rather than counted as covered |