How Ebb works

One contract, 5,008 bytes of it, which holds tokens and counts seconds and does nothing else. This page is what it does, why each decision was made that way, and every check that was run against it — including the deliberate breaks that got through, which are the interesting part.

The contract

contracts/EbbAuction.sol. No owner, no pause, no upgrade path, no admin key, no fee, and no oracle. It has 10 functions, 14 named errors and 3 events, and it uses two storage slots: an array of sales, and a re-entry lock.

The address is a function of the bytecode, so it is a claim about the code: put the source in this repository through solc 0.8.26 at 400 optimiser runs, hash the creation code, and you get that address or you do not. This project holds no key with anything in it — the first person who wants a sale sends the deploy transaction from their own wallet, and from then on it is there for everybody. Until then, every page that offers to open a sale says so and refuses.

The schedule

A sale carries a start time, a span, and two numbers: what the whole lot is asking at the start and what it is asking at the floor. Between them the ask is a straight line in time.

ask(t) = startQuote − (startQuote − floorQuote) × min(t − start, span) ÷ span

After the span it does not expire — it rests. The ask stays at the floor for as long as the seller leaves it there, which turns a finished fall into a plain limit order. A sale that expired would leave the shares stuck in a contract waiting for somebody to notice.

The two prices are totals for the whole lot, in dollar base units — not a price per share. Nothing in the contract divides by a token's decimals, because that is where the arithmetic bugs live: a per-share price needs a unit, the unit needs the decimals, and a wrong decimals is a factor of 10¹² that reads as a plausible number. A buyer taking a fraction of the lot pays that fraction of the ask, and the only division is by the lot size, which the contract set itself from a balance it measured.

Where the rounding goes

Three roundings, and every one of them favours the seller:

• the decrement is floored, so the ask is rounded up;
• the cost of a fraction is ceiled, so dust is never free;
• therefore no buyer can ever pay less than the published schedule.

Get either of them backwards and the contract quietly pays the seller one unit less than the page promised, forever. That is the class of bug that reads as noise, so property 7 buys an inexact fraction on purpose and requires the charge to be exactly one unit above the floor division.

Escrow, and what it costs

The shares go into the contract when the sale opens, and they stay there until they are bought or the seller takes them back. The alternative — leaving them in the seller's wallet under an allowance, which is how most order systems on this chain work — keeps custody but makes every sale a race: the seller can move the shares and the buyer's transaction reverts after they have paid the gas. An auction that can be pulled out from under a bidder is not an auction.

That is a decision with a real cost, and the cost is this: an unaudited contract is holding your shares. It is said on the app page, next to the button. The mitigations are that only the lot you opened is ever at risk, the contract has no owner and no upgrade path, and cancel works at any moment and is refused for everybody but the seller on the books.

open measures the balance before and after the pull and escrows what arrived, not what was asked for — so a token that takes a cut on transfer cannot leave the contract promising more than it holds. The measurement is a delta, so other sellers' lots of the same token sitting in the contract do not disturb it.

What size costs here

The whole premise was measured before a line of the contract was written, because if this chain's pools are deep then nobody needs an auction. For every token with a USDG pool, Uniswap's own quoters were asked what selling $1,000, $5,000, $25,000, $100,000, $250,000 would pay.

The size of each trade is worked out from the pool itself — how many shares $1,000 of USDG buys — and not from a price feed. The first version of that tool sized its trades from a sibling project's list of Robinhood feeds, and so measured 31 of 51 candidates while silently dropping every token whose feed was not in that file. A census is not the set you happened to inherit.

What has been checked

Properties, on chain

23/23, each one a single eth_call with no to, so the harness's creation code runs against the real tokenized stock, the real dollar and the real EbbAuction runtime installed at its own CREATE2 address — at block 68,790,632, with 940 assertions. Nothing is deployed and nothing is spent. Every named balance change must be exact and every unnamed pair must not move at all, which is what catches a fee, a third recipient, or shares that went somewhere nobody asked about.

1. 1. the ask is exactly the start price up to the first second, and exactly the floor from the last (17 assertions)
2. 2. the ask the page draws is the ask the contract will charge, at every boundary of the fall (20 assertions)
3. 3. across the whole fall the ask never rises and never leaves [floor, start] (320 assertions)
4. 4. a flat sale — start equal to floor — is legal and never moves (289 assertions)
5. 5. a buy moves exactly the shares one way and exactly the dollars the other, and nothing else moves (14 assertions)
6. 6. the auction is never paid: it holds no dollars after a fill (12 assertions)
7. 7. a partial buy costs its fraction of the ask ROUNDED UP, and leaves exactly the rest (15 assertions)
8. 8. two partial buys that add up to the lot leave nothing, and never deliver more than was escrowed (16 assertions)
9. 9. asking for more than is left is refused (control: exactly what is left goes through) (13 assertions)
10. 10. a buy before the start is refused (control: the same buy at the start goes through) (14 assertions)
11. 11. maxCost one unit under the cost is refused; maxCost exactly equal is accepted (13 assertions)
12. 12. cancel returns exactly the remainder to the seller, and nothing else moves (15 assertions)
13. 13. a stranger cannot cancel (control: the seller can) (15 assertions)
14. 14. a cancelled sale cannot be bought, and cannot be cancelled twice (16 assertions)
15. 15. a sale opened with the start below the floor is refused (control: equal is accepted) (12 assertions)
16. 16. a span of zero, a floor of zero, a start in the past and a token sold for itself are each refused (17 assertions)
17. 17. what a token actually delivers is what gets escrowed, not what was asked for (16 assertions)
18. 18. a token that answers false is refused; a token that answers nothing is accepted (16 assertions)
19. 19. a re-entry from inside a token transfer is refused BY THE LOCK, named (control: the same assertion against the wrong error fails) (19 assertions)
20. 20. two sellers in the same token do not touch each other, and the auction always holds what it owes (19 assertions)
21. 21. CONTROL: shares written to the wrong storage slot fund nothing (13 assertions)
22. 22. the whole lot bought in one go leaves nothing and pays exactly the ask (15 assertions)
23. 23. two sales falling at DIFFERENT speeds each keep their own clock (24 assertions)

Sabotage

26/28 deliberate breaks, each caught by the property named for it. A sweep that counts "the suite went red" reads far higher than the truth, because one wrong invariant firing on everything takes credit for every break in the run.

• the fall is computed from the wrong end, so the price RISES — caught by property 2, 3
• past the end of the fall the ask jumps back to the START price — caught by property 1, 2, 3
• the fall is twice as fast, so the ask leaves the band below the floor — caught by property 2, 3
• the cost of a fraction is rounded DOWN, so dust is free and the seller eats it — caught by property 7
• the fraction is taken against what is LEFT rather than the whole lot — caught by property 8
• the dollars go to the buyer instead of the seller — caught by property 5, 6
• the shares go to whoever sent the transaction, not where they were asked to go — caught by property 22
• a fill does not reduce what is left, so a lot can be sold twice — caught by property 5, 8, 20
• a buyer may take more than is left — caught by property 9, 14
• a sale can be bought before it starts — caught by property 10
• the buyer's price cap is off by one: paying exactly the cap is refused — caught by property 11
• anybody may cancel anybody else’s sale — caught by property 13
• cancel does not close the sale, so the remainder can be taken again — caught by property 12, 14
• a sale may start below its floor, which is a price that rises — caught by property 15
• a span of zero is accepted, which divides by zero in the schedule — caught by property 16
• a token may be sold for itself — caught by property 16
• a sale may be backdated, so it opens already part-way down — caught by property 16
• the escrow records what was ASKED FOR rather than what arrived — caught by property 17
• a token that answers `false` is treated as having paid — caught by property 18
• the re-entry lock is removed — caught by property 19
• the lock is removed AND the books are written after the transfers — caught by property 19
• the page rounds the ask DOWN where the contract rounds it up — caught by property 2
• the page floors the cost of a fraction where the contract ceils it — caught by property 7
• the page builds the sale with the start and the floor swapped — caught by property 1, 2, 15
• the page sends the shares to the auction rather than to the buyer — caught by property 5, 22
• every sale falls on SALE ZERO’s clock, whatever its own span says — caught by property 23
• cancel pays whoever called it rather than the seller on the books — escaped
• a buy is always charged at the START price, whatever the clock says — escaped

Fuzz

6 random sequences of 40 operations each, against a real deploy on a fork that mines, with 10 invariants checked after every one. This layer exists because of a specific blind spot: every property above lives inside one eth_call, so every operation in it happens at the same block timestamp — a suite that cannot advance the clock cannot see a contract that ignores the clock. The sabotage sweep proved it by walking a break that charges every buyer the start price straight through all of them.

1. 1. the auction always holds at least what it still owes, in every token
2. 2. every buy was charged the schedule price for the block it landed in
3. 3. a sale’s ask never rose, and never left [floor, start]
4. 4. the seller received exactly the cost and the buyer paid exactly the cost
5. 5. the buyer received exactly the shares bought, and nobody else moved
6. 6. what is left fell by exactly what was bought
7. 7. the auction never held a single unit of the quote token
8. 8. the sale rebuilt from its own events equals the sale on chain
9. 9. cancel returned exactly the remainder, to the seller on the books
10. 10. a refused operation moved nothing at all

Each seed is then replayed against 7 broken builds: 7/7 caught by the invariant named for them.

• every buy is charged the START price, whatever the clock says — caught by invariant 2
• the Opened event reports the amount asked for, not the amount escrowed — caught by invariant 8
• the Bought event reports the lot size where it should report what is left — caught by invariant 8
• a fill does not reduce what is left — caught by invariant 6
• the fall is computed from the wrong end, so the price rises — caught by invariant 3
• cancel pays whoever called it, and anyone may call it — caught by invariant 9
• the auction keeps one unit of every payment — caught by invariant 4

What got through

This is the section worth reading. A sweep in which nothing ever escapes has not shown that it can report an escape, so after the first pass came back clean, three more breaks were written to be deliberately subtle and replayed against the suite as it was before the properties written for them existed: 3/3 were invisible to the 22 properties that existed at the time.

• every sale falls on SALE ZERO’s clock, whatever its own span says — seen by nothing, now caught by property 23.
• cancel pays whoever called it rather than the seller on the books — seen by nothing, and declared a survivor with a reason.
• a buy is always charged at the START price, whatever the clock says — seen by nothing, and declared a survivor with a reason.

The fuzz had a hole of its own, and its replay found it. The break in which the Opened event reports the amount asked for rather than the amount escrowed walked through every seed, because the fuzz only traded real stock tokens — and they take no fee on transfer, so the two numbers were always the same. A token that keeps 1% of every transfer is now part of every sequence, and that break is caught by the invariant that rebuilds each sale from its own events.

And these breaks survive the property suite on purpose, each with its reason:

• cancel pays whoever called it rather than the seller on the books — Only the seller can reach this line: the guard two lines above refuses everybody else, so `msg.sender` and `s.seller` are the same address whenever the push happens. Two guards hiding each other is exactly the pattern that ships a real hole, so break 12 removes the OTHER one and property 13 catches that; the pair is what is actually tested, not either half.
• a buy is always charged at the START price, whatever the clock says — Every property in this suite runs inside ONE eth_call, so every buy in it happens at the same block timestamp as the open — which IS the start. A suite that cannot advance the clock cannot see a contract that ignores it. This is not a hole that another property would close; it is the boundary of the layer. tools/fuzz.mjs runs on a fork that mines, and its `charged the schedule price` invariant is what catches this one.

The other way of doing this

A falling-price sale does not have to escrow. It can be a Seaport order whose price descends, with a zone that refuses a fill below a floor read from Robinhood's live feed — which is what Taper does, built alongside this one. The two make different promises and the difference is worth understanding before you pick:

What can go wrong

• The contract is not audited and it holds your shares. Every check on this page was written by the same person who wrote the contract. That is a real limitation and no amount of green ticks changes it.
• Nobody has to buy. A falling-price sale is an offer, not a guarantee. If nothing takes it, the price reaches your floor and waits there until you cancel — you have spent gas and some time and are holding the same shares.
• The market can move under you. The schedule knows only the clock. If the stock falls faster than your ebb, your floor is above the market and the sale simply never fills. If it rises, you may sell cheaply to somebody paying attention. A start above the feed and a span short enough to be about today are the defences, and neither is automatic.
• Partial fills. Somebody may take a tenth of your lot and leave the rest falling. That is the design, not a fault, but it means "sold" is not a binary.
• This chain prunes state. Reads on Robinhood Chain answer from a short window of history. The board is a state read for exactly that reason, but a deep audit of past fills is not something this site can promise you.