Contract
Nothing here is asserted
Every property below is executed on Robinhood Chain on every build. An
eth_call with no to runs creation code against the real EVM of the real chain and returns
whatever the constructor returns, so this needs no testnet, no toolchain, no funded account and no private key —
and leaves nothing behind. executed
Executed
The properties
Each is one eth_call. One per call, because this node caps eth_call gas
server side and raising the number in the request changes nothing at all.
| # | What holds | On chain |
|---|---|---|
| P01 | first deposit mints shares and books the assets | holds |
| P02 | deposit then redeem in one block never profits | holds |
| P03 | a donation does not move the share price | holds |
| P04 | a donation does not change what a holder is owed | holds |
| P05 | totalAssets + locked is exactly the pool, always | holds |
| P06 | locked never increases as blocks pass | holds |
| P07 | the stream is exhausted at exactly unlockEndsAt, not before | holds |
| P08 | with unlockBlocks = 0 the whole harvest lands in one block | holds |
| P09 | with the unlock on, a harvest moves nothing in its own block | holds |
| P10 | the share price rises on every block of the stream | holds |
| P11 | the whole harvest is credited, exactly, after unlockBlocks | holds |
| P12 | a second harvest carries the remainder; nothing is lost or double-counted | holds |
| P13 | holders together are never owed more than has been released | holds |
| P14 | the cut cannot exceed the cap, by anyone, including the owner | holds |
| P15 | the cut is exactly cutBps of the gain and the rest reaches shareholders | holds |
| P16 | the owner reaches the surplus and never a wei of principal | holds |
| P17 | every owner-only entry point rejects a stranger | holds |
| P18 | redeeming for another account needs an allowance and spends it | holds |
| P19 | previewDeposit is exactly what a deposit mints | holds |
| P20 | previewRedeem is exactly what a redemption pays | holds |
| P21 | nobody else's deposit or redemption can lower the share price | holds |
| P22 | a one-block visit takes strictly less with the unlock, by over 100x | holds |
| P23 | a deposit never mints shares worth more than the assets paid for them | holds |
| P24 | a withdrawal burns at least what it takes, and a mint charges at least what it gives | holds |
Run at block 55,485,172 in 114.5 seconds.
Spate.sol compiles to 6.5 kB of runtime.
And the suite is tested too
Break it on purpose, 11 ways
A suite that has never been shown to fail is a suite nobody has tested. The contract is compiled again with one deliberate defect each time and every property is re-run against it. A sabotage whose anchor no longer matches throws rather than warning — otherwise it silently compiles the untouched contract, every property passes, and the run reports "not caught" for a defect that was never introduced.
| Sabotage | What it does | Result |
|---|---|---|
| donation-priced | read assets from balanceOf instead of the storage counter | caught by P3, P4 |
| instant-credit | credit the harvest to the share price at once, ignoring unlockBlocks | caught by P7, P9, P10, P12, P22 |
| stream-not-carried | drop the unreleased remainder when a second harvest arrives | caught by P12 |
| cap-removed | let the owner set the protocol cut above the hard cap | caught by P14 |
| sweep-principal | let the owner sweep the whole balance, principal included | caught by P16 |
| no-allowance | let anyone redeem anyone else’s shares | caught by P18 |
| price-after-assets | price a deposit after its own assets have landed | caught by P8, P19, P22 |
| stream-ends-early | finish the release one block before unlockEndsAt | caught by P7 |
| preview-rounds-up-1 | over-issue ONE share unit on every deposit (worth 10**-OFFSET asset units) | survives — by design; see below |
| preview-rounds-up-unit | over-issue one whole asset unit’s worth of shares on every deposit | caught by P23 |
| extra-owner-hatch | add an owner-only rescue() that no property forbids | survives — caught only by the ABI surface check (rescue) |
Two are expected to survive
If every sabotage were caught by half the suite, that would look like strength and would in fact mean the properties are not saying anything specific. Two are expected to get through, for different reasons, and both reasons are checkable.
extra-owner-hatchadds an owner-onlyrescue(). It breaks no invariant any property states, and is seen only by comparing the compiled ABI against a written-down surface.preview-rounds-up-1over-issues one share unit on every deposit and is caught by nothing — which is the virtual offset doing its measurable job rather than a hole.
And that second one is a measurement
A share unit is 106 times finer than an asset unit here, so a one-unit over-issue is worth less
than the smallest amount the asset can express and every economic property floors it away. Over-issue a whole
asset unit's worth — preview-rounds-up-unit, the row above — and the same suite catches it
immediately, at P23.
Publishing only the first would look like a gap. Publishing only the second would hide where the floor actually is. The pair says where it is.
And the page, not just the contract
The front end's own byte strings, executed
Proving the contract is not proving the page. Every property above calls Spate through Solidity,
which cannot be wrong about an ABI encoding; your browser sends hand-built hex. These checks take the exact
strings js/vault.js produces and run them against USDG
— the real token, at its real address — inside one eth_call, with the caller's balance written in
by a state override. live
| Check | Detail | Result |
|---|---|---|
| the asset came from the chain scan, not from a constant | USDG 0x5fc5360d0400a0fd4f2af552add042d716f1d168 (6 decimals) | pass |
| the balance slot was DISCOVERED by probing, not remembered | slot 1 | pass |
| the deploy string is creation code plus encoded arguments | 8.0 kB | pass |
| the app’s calldata executed against real USDG | 1217 bytes back | pass |
| the vault landed at the address the app predicts | 0x97b0abf484ecbcc9c901f4cfd91c5842d7ddb623 vs predicted 0x97b0abf484ecbcc9c901f4cfd91c5842d7ddb623 | pass |
| the override funded the caller with real USDG | 1010000000 units | pass |
| the deposit and the harvest both left the caller | 0 left | pass |
| the deposit minted shares | 1000000000000000 share units | pass |
| the share token’s decimals are assetDecimals + OFFSET | decimals 12 | pass |
| the OFFSET the app encoded arrived intact | pass | |
| the unlockBlocks the app encoded arrived intact | 36000 blocks | pass |
| MAX_CUT_BPS is the constant the site prints | pass | |
| the harvest is locked, not credited, in its own block | locked 9000000 of 9000000 net | pass |
| totalAssets still shows only the deposit | 1000000000 | pass |
| the pool holds deposit plus the net harvest | 1009000000 | pass |
| the cut left the vault for the treasury | pass | |
| the redeem string the app builds pays the caller back | 1000000000 units | pass |
| redeeming in the harvest block returns the deposit and NOT the harvest | 1000000000 vs deposit 1000000000 — the locked income stayed behind | pass |
| the caller ends holding exactly what came back | 1000000000 | pass |
eth_call is a real
EVM with real chain state and no persistence — the vault is really deployed, the token is really
USDG, and the evaluator is Robinhood Chain's own — but nothing above
was signed and nothing was spent.
Read it
The source
Four files, and all four ship with the site rather than being described by it:
contracts/Spate.sol is the vault, contracts/SpateTest.sol holds the properties,
contracts/Capture.sol runs the sequence on the flood page, and
contracts/AppRun.sol executes the front end's calldata.
No Spate vault is deployed by us. Deploying costs gas from a wallet and this repository holds no key. The app deploys one from yours, on mainnet, and simulates every write from your address before it is offered for signature. none none