Escrow invariant

Statement

fact For every series s and at every point in time after every external call:

quoteEscrow(s) == N_c(s) + prefundRemaining(s) + claimableQuote(s) + refundableQuote(s) + accruedFees(s) stockEscrow(s) == stockMatched(s) + refundableStock(s) + claimableStock(s)

where

Term	Meaning
quoteEscrow, stockEscrow	USDG and Stock Token balances the series holds inside NoteCore
N_c	Matched COUPON notional not yet redeemed (COUPON principal); 0 once breached, when it becomes SHIELD’s claimableQuote
prefundRemaining	SHIELD’s remaining maximum coupon liability
claimableQuote	Net coupons accrued (the couponPool) and terminal payouts booked but not yet pulled
refundableQuote	Unmatched COUPON deposits and unmatched SHIELD prefund
accruedFees	Protocol fees not yet swept, from which keeper rewards are paid
stockMatched	Stock backing matched notional; on breached it becomes COUPON’s claimableStock
refundableStock	Unmatched SHIELD stock

The implementation states the same identity in its own bucket names (couponSideQuote + prefundRemaining + prefundRefundable + couponPool + accruedFees), where couponSideQuote covers both matched principal and unmatched COUPON deposits.

Consequences

1. No path can pay out more than escrowed. Every transfer out of NoteCore debits exactly one bucket on the right-hand side and quoteEscrow/stockEscrow on the left by the same amount. The identity is checked in tests after every handler call.
2. No liquidations. Because SHIELD’s maximum liability is escrowed at subscription, there is never a moment where a price move creates an unfunded obligation.
3. No principal risk in NoteCore. The protocol’s only balance is accruedFees. It is never used to fund coupons or redemptions.
4. Isolation. The invariant is per series. A failure in one series (for example an oracle deferral) cannot draw on another series’ escrow.

Flow of value

Every observation moves one gross coupon out of prefundRemaining: the net part into claimableQuote, the fee into accruedFees. Nothing enters or leaves the sum except through deposits and pulls.

Bucket transitions

Event	Debit	Credit
depositCoupon	external USDG	refundableQuote (until strike)
depositShield	external USDG, stock	prefund and stock buckets (until strike)
finalizeStrike	deposits	N_c, prefundRemaining, stockMatched; unmatched → refundable; notional fee → accruedFees
Coupon observation	prefundRemaining (gross)	claimableQuote (net), accruedFees (fee)
Keeper payment	accruedFees, quoteEscrow	external (keeper)
Autocall / maturity, barrier holds	—	shieldUnusedPerUnit fixed from prefundRemaining
Maturity, breached	N_c → SHIELD claimable; stockMatched → COUPON claimable	—
claim, redeem, redeemShield, refund	corresponding bucket and escrow	external (holder)
sweepFees	accruedFees, quoteEscrow	external (feeSink)

Rounding

• Coupon index is WAD, rounded down; dust stays in claimableQuote and is unreachable, which is conservative.
• Stock matched at strike is rounded up so the physical-settlement quantity units × 1e12 × 1e8 / s0 can always be delivered.
• Prefund matched is rounded up so prefundRemaining always covers (observations.length − 1) gross coupons at the cap.

How it is tested

The invariant is the primary target of the specified handler-based invariant suite: random sequences of deposits, strikes, observations with fuzzed prices, transfers, claims, redemptions, refunds and sweeps across many actors and series, with the identity asserted after every call. Additional assertions: total USDG paid out never exceeds total deposited plus zero; NoteLegs total supply per id equals matched notional until redemption. status At the time of writing the repository contains unit tests for the core and token modules and stateless fuzz tests (test/fuzz/core/Settlement.fuzz.t.sol checks coupon-index conservation across transfers and the physical-settlement sum bound); the handler-based invariant suite in test/invariant is not yet committed. See Security: Invariants.