Cupel.sol · block 58,831,199
Broken on purpose.
A test suite that only ever runs the correct contract tells you the tests pass. It does not tell you they would notice. So the contract is compiled again 20 times, each time with one guard removed or one formula replaced by the easy version, and every defect has to be caught by a specific, related property.
Two rules make that mean something. A property that is red on the correct contract is excluded from the sabotage runs, because it would appear in every caught-by list and prove nothing. And a sabotage anchor that no longer matches throws — otherwise it compiles the untouched contract, every property passes, and the run reports a hole whose real cause is that nothing was broken.
The survivors are published too
zero-deposit-guard-removed — the explicit `assets == 0` check is removed from deposit.
Survives because: genuinely redundant: a zero deposit pulls nothing, converts to zero shares, and is refused two lines later by the `shares == 0` guard — which the next sabotage removes instead
Publishing only the caught ones hides where the floor is.
Properties
26 of 26 hold. Each runs in its own
eth_call with no to: one property per call, so a revert can only have come from the property in that call.
| # | Result | What it executed |
|---|---|---|
| P1 | ok | deposit minted the previewed 100000000000 shares |
| P2 | ok | mint charged 2333334, at or above the floor conversion |
| P3 | ok | donation moved nothing; settle booked 50 and the price then rose |
| P4 | ok | victim kept 100000000 of 100000000; attacker recovered 1 of 1000000001 staked |
| P5 | ok | credited 99000000, which is what arrived, not the 100000000 asked for |
| P6 | ok | the hook re-entered and deposited; the vault holds 600000000 and its books say 600000000 |
| P7 | ok | withdrew the quoted 137000001 and was paid exactly that |
| P8 | ok | previewWithdraw(137000001) fits and (m+1) does not |
| P9 | ok | refused above the quote, with ExceedsQuote |
| P10 | ok | the naive quote says 137000001, the vault honours 136315000, and the naive one reverts |
| P11 | ok | under a 50bp exit fee the quote is 136315000, tight, and paid in full |
| P12 | ok | maxRedeem 100250626004 is inside the liquid bound, redeemable, and r+1 is refused |
| P13 | ok | quote fell from 500000000 to 50000000 when the assets left, and was paid |
| P14 | ok | liquid 99999993 split 66666662 / 33333330 - the two quotes together never exceed what the vault holds |
| P15 | ok | after a full exit of 66666662 the other holder still drew their whole quote of 12820511 |
| P16 | ok | a stranger cannot deploy, the steward cannot deploy more than is liquid, and the assets went to the berth |
| P17 | ok | liquid rose from 100000000 to 500000000 and nothing is outstanding |
| P18 | ok | an empty vault quotes zero, in every one of the four functions |
| P19 | ok | price per share rose from 1000000 to 1009999 for the holder who stayed |
| P20 | ok | 101 bps is refused at construction, 100 is allowed |
| P21 | ok | a steward without a berth, and a berth without a steward, are both refused |
| P22 | ok | a stranger booked the income and the price rose for the holders |
| P23 | ok | refused without an allowance, allowed with one, and the allowance was spent |
| P24 | ok | a quote of 1000000000 split into 500000000 and 500000000 when half the shares moved |
| P25 | ok | a zero deposit, withdrawal and redemption are all refused |
| P26 | ok | the berth holds 99000000 and the vault books exactly that as deployed, not the 100000000 asked for |
Sabotages
20 of 20 behave as declared.
| Defect | Result | What was broken | Caught by |
|---|---|---|---|
| maxwithdraw-computed-the-easy-way | as declared | the quote is convertToAssets(balanceOf(o)) — the obvious formula, and the one this whole site is about | P10, P11, P19 |
| quote-ignores-the-liquid-bound | as declared | maxWithdraw reports what the shares are worth and never asks whether the vault is holding it | P13, P14, P15 |
| liquid-served-first-come | as declared | a holder may take the whole of what the vault can pay, rather than their share of it | P14, P15 |
| liquid-share-rounded-up | as declared | each pro-rata claim rounds up, so the claims sum to more than the vault holds and the last one out reverts | P14 |
| withdraw-does-not-enforce-its-quote | as declared | the exit path stops checking the number the quote path published | P9 |
| redeem-does-not-enforce-its-quote | as declared | the same drift, on the share-denominated side | P12 |
| maxredeem-returns-the-whole-balance | as declared | maxRedeem ignores the liquid bound and answers with the whole balance | P12 |
| deposit-credits-what-was-asked-for | as declared | the vault credits the requested amount rather than the amount that arrived | P5 |
| deposit-credits-an-uncapped-delta | as declared | the credit is the measured delta with no cap, so a donation made first is handed back as shares | P6 |
| deposit-prices-itself-after-its-own-pull | as declared | the conversion happens after the assets have landed, so a depositor is diluted by their own deposit | P1, P2, P4 |
| exit-fee-not-charged | as declared | the fee is quoted but never taken, so the holders who stayed are not paid | P11, P19 |
| anybody-may-deploy | as declared | the steward check comes off the one function that moves assets out | P16 |
| deploy-sends-to-the-caller | as declared | the berth is quoted in the interface and ignored in the transfer | P13, P16, P17 |
| settle-is-permissioned | as declared | income can only be recognised by the steward, so holders wait for it | P3, P22 |
| exit-fee-cap-removed | as declared | the fee stops being bounded by code | P20 |
| virtual-offset-removed | as declared | the conversion loses its virtual share and asset | P2 |
| steward-without-a-berth-allowed | as declared | a steward may be set with no destination, which is the same as having no bound | P21 |
| deploy-books-the-amount-it-asked-to-send | as declared | the berth is credited with the requested amount rather than what reached it, inflating totalAssets by the fee | P26 |
| zero-deposit-guard-removed | as declared | the explicit `assets == 0` check is removed from deposit Survivor: genuinely redundant: a zero deposit pulls nothing, converts to zero shares, and is refused two lines later by the `shares == 0` guard — which the next sabotage removes instead |
survives |
| zero-share-mint-allowed | as declared | the guard the previous survivor was leaning on is removed as well, so a deposit can mint nothing and keep the assets | P25 |