Capacity model

For one group and one output token, CAPACITY_GUARD admits a fill only when transferable inventory can cover that fill and every strategy's remaining configured entitlement. Inventory above all remaining entitlements is burst: any strategy may use it, but no fill may eat into a sibling's protected share.

Terms

The admission invariant

For a fill of strategy j, the guard first requires d <= v[j], rejecting a virtual-balance shortage itself instead of admitting a fill Aqua would later fail. It then admits and reserves d only if:

remaining(i, extra) = min(g[i], max(v[i] - b[i] - r[i] - extra, 0))

I >= sum(r[i]) + d + sum(remaining(i, i == j ? d : 0))

In words: count every pending reservation, add the proposed debit, and still cover what each strategy is owed after its own pending consumption. The filling strategy's own entitlement is counted after its debit, so it consumes its guarantee first and bursts beyond it only into inventory nobody else is owed.

Activation must be feasible for both tokens: I >= sum(g[i]).

The allowance floor

Every guarded output also requires:

allowance(vault, Aqua) >= sum(g[i]) + sum(r[i]) + d

Activation establishes this floor and every output preserves it, so a permissionless Aqua.push can never make restored entitlement look transferable when the allowance is gone. The cost is conservatism: an allowance exactly equal to the guarantee sum blocks every positive output. There is no reapproval API; the owner can pause, dock all and withdraw to migrate.

Guaranteed and burst

The benchmark compares two guarantee policies over the same real backing. Both advertise the full backing on every strategy; they differ only in how much of it is protected.

Worked example

Two strategies with g = 500, virtual balances of 1000 each, and a vault holding 1000 output tokens. Each row is a separate transaction, so no reservation is pending.

In step 1, S1's own remaining entitlement after the debit is zero, but S2 is still owed 500, and 1,100 exceeds the 1,000 available. After step 2 the real balance is 500 and only S2 is owed anything, so step 3 fails by exactly one unit.

The local transaction replay and the public Sepolia run execute this sequence and record these error arguments. The public run used larger raw amounts.

With g = 250 instead, the step-1 request is admitted: 600 + 0 + 250 = 850 <= 1000. S1 may take up to 750, its own 250 plus 500 of burst, while S2's 250 stays covered.

Consumption and replenishment

• Consumption. A successful output lowers the strategy's virtual balance toward its baseline, so its remaining entitlement falls naturally, down to zero.
• Replenishment. Input pushed into a strategy, by a reverse swap or a direct Aqua.push, raises its virtual balance. Entitlement recovers automatically, capped at g.
• Quotes. A quote is a same-state eligibility result. It creates no reservation, and the swap rechecks against current state.
• Pausing. Pausing makes every check reject and ends the commitment. Reactivation resets every baseline together and must pass feasibility again.

for (uint256 i; i < hashes.length; i++) {
    bytes32 sibling = hashes[i];
    Strategy storage s = strategies[sibling];
    uint256 reserved = reservation(sibling, token);
    required += reserved;
    uint256 available = _subtract(_virtual(sibling, token), token == tokenA ? s.baselineA : s.baselineB);
    available = _subtract(available, reserved);
    if (sibling == hash) available = _subtract(available, debit);
    uint256 guarantee = token == tokenA ? s.guaranteeA : s.guaranteeB;
    allowanceRequired += guarantee + reserved;
    required += available < guarantee ? available : guarantee;
}
_requireCapacity(token, required);

Verify

• CAPACITY_GUARD specificationView source on GitHub · docs/CAPACITY_GUARD_SPEC.md
• Vault checkCapacity()View source on GitHub · contracts/AquaQoSVault.sol#L149-L174
• Bounded arithmetic model checkView source on GitHub · scripts/check-capacity-model.mjs
• Separate-transaction validationView source on GitHub · docs/TRANSACTION_VALIDATION.md