Weir Open the app

The quote

Solve it, don't approximate it.

The obvious way to answer “what can I take out” is to ask what your shares are worth. That answer is wrong in a specific, reproducible way, and the error is exactly one unit — which is the difference between a quote and a revert.

The two roundings

Weir charges an exit fee, left behind for the holders who did not leave. So between the assets you ask for and the shares that are burned there are two conversions, and both round against you, as they must:

previewWithdraw(a) = ceil( ceil(a·B / (B−f)) · D / N )

  a = the assets you want in hand      f = the exit fee, in basis points
  B = 10,000                           N = totalAssets + 1
                                       D = totalSupply + 10^offset

A vault that answers maxWithdraw with convertToAssets(balanceOf(o)) has applied one conversion, in the other direction, with the other rounding. The result is above the real edge almost every time a fee is charged, and withdraw reverts on it — after burning nothing, having told you a moment earlier that it would work.

Peeling the ceilings

For integers, ceil(p/q) ≤ s is exactly p ≤ s·q. So each ceiling comes off from the outside in, and each one becomes a floor:

ceil(g·D/N) ≤ s          ⟺  g ≤ floor(s·N/D)        =: G
ceil(a·B/(B−f)) ≤ G      ⟺  a ≤ floor(G·(B−f)/B)

maxWithdraw(o) = floor( floor(bal·N/D) · (B−f) / B )

Two floors, no search, no slack. And it is tight, which the contract does not merely claim: property 8 executes previewWithdraw(M) ≤ balance and previewWithdraw(M+1) > balance on this chain's EVM, and property 10 takes the naive formula, shows it is strictly larger, and shows the vault reverting on it.

The crest

The second bound is liquidity. A vault that has deployed its assets is worth more than it can pay, and the honest quote is the smaller of the two:

crest()      = the assets this vault can pay out this block
crestFor(o)  = crest · balanceOf(o) / totalSupply     (rounded down)

maxWithdraw(o) = min( the inversion above , crestFor(o) )

The division is the point. Served first come, a shortfall is a race: the first holder to notice takes the whole crest and everybody behind them is quoted a number the vault can no longer honour. Shared pro rata, every holder is quoted their own share of what is actually there, and the sum of every quote is never more than the vault is holding — which is why the claim is rounded down.

Property 14 puts two equal holders in front of a crest that cannot pay both and requires neither to be quoted more than half of it. Property 15 then has the first one leave and the second one actually withdraw their whole quote — because checking that the second holder is still quoted a positive number is the flattering version of that test, and it passes against a vault that rounds each claim up.

And the exit path enforces what the quote published

There is no second formula for withdraw to drift away from. It calls maxWithdraw, refuses anything above it with ExceedsQuote(asked, quoted), and pays the rest. Property 9 checks the selector, not merely that something reverted — a guard is not tested by observing that something else also says no.

What is deliberately not here

  • No upgrade path and no owner who can take principal.
  • The steward may move assets between the vault and one named berth, and nowhere else — so the deployed fraction is visible and bounded.
  • The exit fee is capped in code at 100 bps and accrues to the holders who stayed, not to a recipient.
  • settle() is permissionless: income only a privileged address can recognise is income the holders wait for.