Deposit

You approve the asset and call deposit. The vault measures its own balance either side of the transfer and credits what arrived, not what you asked for — a token that takes a cut in transit delivers less, and crediting the request mints shares nobody paid for.

That fix is also what makes a reentrancy guard necessary. A token with a transfer hook can re-enter between the two measurements and have the outer caller credited with the inner caller's tokens. The guard is there, and property 25 fires a real hook at it — the property fails outright if the attack did not actually run, because an exploit that never fires is not a passing test.

Earn

Fee income arrives at the vault as an ordinary transfer. It is not in the share price. totalAssets() reads a tracked counter, not the balance, so anything sitting above that counter is pending and visible through pendingFees().

This is the same mechanism that closes the ERC-4626 inflation attack, used deliberately: a donation and a fee payment are the same transaction, and the only difference is whether it goes through a function that pays the finder and takes the protocol cut.

Glean

Anybody calls glean(). It books the pending fees into the share price, sends the protocol cut to the treasury, and pays the caller 200 basis points of the harvest. booked + cut + bounty equals the pending amount exactly, with both rounding remainders going to depositors rather than to either fee — property 9 runs it on an amount chosen to divide cleanly by neither rate.

It refuses below minHarvest. That threshold is the honest half of this design and the whole subject of the measurement.

Redeem

Burn Comb, take the underlying at the current price. No lockup and no queue — and, stated plainly because it is true: no fees that have not been gleaned yet. Redeeming the moment before a harvest lands is worse than redeeming the moment after, and property 13 executes that difference rather than leaving it as a caveat.

If that bothers you — it should — the answer is that you can fix it yourself. glean() is permissionless, so a redeemer who wants their share of the pending fees can call it first and be paid for doing so.

The words