invariants

These are the ledger relationships that must hold at the end of every external call. Every test in the suite either explicitly checks one of these, or its behavior implicitly relies on them being preserved.

I-1 · band-borrow conservation

sum over all bands of band.borrowedETH ==  totalDebtETH       (debt owed by open positions) + protocolReserve    (real ETH the hook holds as cash) + totalBadDebtETH    (write-off marker — phantom ETH)

Every wei of ETH that leaves a band via the borrow walk ends up in exactly one of three buckets. Closes and liquidations move it between buckets; donations heal the bad-debt one.

Tracked redundantly as totalBandBorrow for O(1) cap checks (D8). The two values must always agree.

I-2 · reserve solvency

protocolReserve  ≤  address(hook).balance

protocolReserve represents real ETH the hook holds. If it ever exceeds the actual balance, deployReserveToBands() would revert in its settle{value:} call. Fixed in v0.1 by H-01.

I-3 · holding-token conservation

sum over open positions of pos.holdingTOKEN +  PerpToken.balanceOf(hook) backing bands ==  PerpToken.totalSupply  ( = LDF.TOTAL_SUPPLY, fixed at deploy)

PerpToken is OZ ERC-20 with all supply minted to the hook at construction and no mint after that. The hook either holds tokens for positions or has them deployed as LP in the bands.

I-4 · position-list integrity

For every positionId in _openIds:

• _positions[id].owner is non-zero.
• userPositions[owner][_userPosIndex[id]] == id.
• _openIds[_openIdIndex[id]] == id.

Closed/liquidated positions are removed via swap-pop, which preserves all three relationships. delete _positions[id] zeros the struct.

verification status