Invariants

Core

• Escrow balance ≥ total obligations for every token.
• Leg supply equals matched notional for every series.
• A struck series never changes its levels.
• Each observation is processed at most once.

Oracle and calendar

• No observation uses a round updated before its scheduled close.
• No observation falls on a non-trading day.

Token engine

• Buyback price never below the floor.
• Daily floor redemptions never above 1.5% of reserves.
• sBERRIER rate never decreases.

Suite structure

Handlers drive random deposits, strikes, observations, transfers and redemptions; ghost variables track expected balances.