A level, not a tank

ERC-4626 over one position

Deposit an asset, receive Spar in proportion to what the position is worth when it is read. Fees are harvested back in, which raises every share by the same factor. Redemption unwinds a pro-rata slice.

Two design choices are worth stating because the category usually does the opposite:

• The share price is a mark, not a counter. It is computed from the position's reserves at the block it is read, so it can go down. A share price maintained as a storage counter only ever rises, and it stops being a measurement the moment it does.
• Redemption is quoted at your size. The value of a pro-rata slice is not linear in the slice, and a vault that quotes it as though it were has told you the average when you asked for the margin.

Both are implemented, and both are checked: the price falling when the position loses, and rounding going against the person leaving, are two of the 45 properties the build executes on an EVM. Deploy one below and you can watch the first of them happen to your own money. G5

It compiles, and its properties are executed

contracts/Aquifer.sol is 6,420 bytes of runtime bytecode with 11 state-changing functions and no imports — the whole of it is one file, so there is nothing behind a name you would have to go and read elsewhere. It is not deployed. There is no address and no audit.

What the build does do, every time, is compile it and run it: tools/verify-contracts.mjs deploys the test harness by overriding the code at a scratch address inside an eth_call against a Base node and calls it, so 45 properties are asserted by the compiled bytecode executing on an EVM rather than claimed about the source. G5

A round trip is worth what went in

and rounding never pays out more

THE SHARE PRICE FALLS when the position loses

it is a mark, not a counter

…and still falls after a recharge

no high-water mark

The shares a withdrawal burns cover what it takes

rounding goes against the leaver

CHOKED, A WITHDRAWAL STILL WORKS

and maxWithdraw is never reduced

Choked, deposits revert and the guardian cannot allocate

flow in only

The guardian never holds the asset or a share

at any point in the run

The inflation attack leaves the victim ≥ 99.9%

virtual shares, no dead-shares mint

And then it is broken on purpose

A suite that passes tells you nothing until you have watched it fail for the right reason. The build recompiles the vault 7 times with one property sabotaged each time — Choke made to block withdrawals, the inflation offset removed, the share price turned into a high-water mark, rounding turned in the depositor's favour — and requires that the suite catches each one and names the property that broke. 7 of 7 are caught. G5

Two of the four were missed on the first run, which is the whole argument for doing it: removing the offset was caught by an assertion about a constant that fired before the property it protects, and turning the rounding around was not tested at all. Both are now exact inequalities that name themselves.

Nobody has a function that moves your money

The site says that, so something checks it: the build reads the compiled ABI and fails if a state-changing function appears that is not on a named list, or if one is called anything that has moved somebody's money in somebody else's vault. The list today is allocate, approve, choke, deposit, lowerCap, mint, recharge, redeem, transfer, transferFrom, withdraw. G5

Deploying it needs a key, which this repository does not have and should not have. The creation bytecode is published in data/contracts.json — the constructor takes the asset, the position, a guardian, a name and a symbol — so anybody can put it on a chain themselves and nobody has to take this page's word for what it does.

The parts that are physics, and the parts that are a clock

The site does not claim this reproduces a named cave. It claims the feedback is real and that its consequence — a sum that moves smoothly while a minimum jumps — follows from the loop rather than from the constants. tools/verify-model.mjs sweeps a decade of rate, three saturation lengths and four seeds; the cut stays under two per cent of the total in every one of them.

Cubic law, flow ∝ aperture³ G5

Hagen–Poiseuille for a slot

Mass balance at every node G5

solved, residual published

Max-flow / min-cut G5

Ford–Fulkerson, a theorem

Transported saturation G3

water saturates as it travels and then does nothing

Rate law, 1st order then 4th G3

Dreybrodt’s shape; the switch is why caves exist

The constants G2

a clock and a length scale, not calcite at 10 °C

A square lattice G2

real fracture networks are not a grid

The version without the switch made a cave one row deep

With a purely first-order rate law, water saturates in the first fracture it enters. Run six hundred steps and the surface widens to sixty times its aperture while nothing below the first row ever moves. That is the published result for linear kinetics and it is why the nonlinear regime was proposed: at ninety-nine per cent saturation the rate is five orders down, and five orders down over a long fast passage is what cuts a cave.

And the check that caught the solver

Conductance goes as the cube of aperture, so by the end of a run it spans five orders of magnitude — and a head-based convergence test that reads as converged is then wrong about flux by several per cent. The first version of this model reported the spring delivering more water than the catchment supplied, in 64 of 143 recorded steps, with every residual looking fine. The residual is a flux now; the worst mass imbalance across the canonical run is 0.030%. G5

The busiest one per cent

After breakthrough, one per cent of the fractures carry 12.2% of the water and the quietest half carry 0.02%. Set the saturation length to zero — water that never gives up its dissolving power — and the massif widens uniformly instead: no conduit, no concentration, Gini 0.003. The structure comes from the fact that water gets tired, which is a sentence about markets as well as about rock.