Escrow Invariant
On this page
The escrow identities reconcile recorded assets with outstanding claims for each series. They are accounting rules, not a claim that an external token can always be transferred.
Statement
fact For every series s and at every point in time after every external call:
fact Quote Escrow Identity
fact Stock Escrow Identity
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
- No path can pay out more than escrowed. Every transfer out of
NoteCoredebits exactly one bucket on the right-hand side andquoteEscrow/stockEscrowon the left by the same amount. The identity is checked in tests after every handler call. - No liquidations. Because SHIELD’s maximum liability is escrowed at subscription, there is never a moment where a price move creates an unfunded obligation.
- Separate fee accounting.
accruedFeesis accounted for separately from coupon and principal liabilities. This does not remove contract, oracle or issuer risk. - 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
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
claimableQuoteand is unreachable, which is conservative. - Stock matched at strike is rounded up so the physical-settlement quantity
units × 1e12 × 1e8 / s0can always be delivered. - Prefund matched is rounded up so
prefundRemainingalways 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 cover recorded claims, leg supply and physical-settlement rounding. The repository contains handler-based core invariant tests under contracts/test/invariant/core/, alongside unit and stateless fuzz tests. This documentation pass did not execute those contract suites; see Testing Methodology for the recorded coverage scope.
Keep exploring, or revisit this topic from the navigation.