# Protocol Invariants Properties held under stateful fuzzing (256 runs × 500 calls per invariant, randomized action sequences across deposits, exits, coupon cycles, losses, recoveries, transfers, and wrapper flows). A violating sequence is a bug in the code; a vacuous pass is a bug in the tests. ``` * Structure / settlement * Conservation: Σ class NAVs == total NAV after every settlement (both pricing modes) * Solvency: paid exits + strategy funding never exceed cash + reported value * Dual-NAV ordering: optimistic NAV >= conservative NAV for every class * Principal deployed: facility deployed principal reconciles with funded − returned * Token cash segregation: class token balance == pending deposits + claimable exits + coupon pool * Coupon ledger * Coupon solvency: Σ claimable coupon <= coupon cash held (class tokens and wrapper's underlying) * Pool bounded: coupon pool <= cumulative funded cash * Accumulating wrapper — pricing * PPS never drops from mechanics: wrap / requestUnwrap / claim / cancel / transfer can never reduce price per share (only funding raises it; a drop == value extracted from holders) * claimUnwrap is exactly PPS-neutral * Redeemable solvency: all shares redeem to no more than the wrapper holds * totalAssets composition: totalAssets == value(unlocked) + claimableCoupon(self) + couponReserve − exitCouponOwed (exact identity) * Principal backing: totalAssets covers the unlocked principal slice (up to rounding dust) * Accumulating wrapper — exit-coupon clock * Liability covered: exitCouponOwed <= claimableCoupon(self) + couponReserve * Locked-share conservation (exact): totalLockedShares == underlying.lockedShares(wrapper) + Σ filled-but-unclaimed bucket shares * Bucket/global agreement: Σ bucket owed == global liability (wei-dust bound) * Fill-window robustness: the handler deliberately fills exits WITHOUT claiming (fillWithoutClaim) and funds coupon across the open window — every property above must hold with fills unobserved, since burned shares stop earning at the fill (fill checkpoints), not at the claim * Accumulating wrapper — cash rations * Abuse bound: Σ cash-first legs paid <= Σ coupon ever funded (principal can never exit through the cash leg) * Ration solvency: Σ live cash allowances <= distributable coupon on hand * Ration conservation: transfers move rations pro-rata and conserve the sum exactly ``` ## Where they live * `test/invariant/RiverInvariants.t.sol` — full-system suite (Structure + classes + facility + wrapper), driven by `RiverHandler` * `test/invariant/DistributingVault4626Invariant.t.sol` — wrapper-focused suite with a PPS-tracking handler and ghost accounting for the cash-leg bounds Alongside the invariants, ~490 unit/integration/blackbox tests pin exact values for every worked example in these docs. The forward-looking business intent behind each property is recorded in the audit brief (`docs/audit/business-requirements.md`), which maps each requirement to the invariant that machine-checks it.