Protocol Invariants#

Formal invariants that must hold at all times in the Seesaw protocol.

Overview#

Invariants are properties that must remain true across all state transitions. Violating any invariant indicates a bug or attack.

Global Invariants#

INV-G1: Account Ownership#

All protocol accounts must be owned by the program.

INV-G2: PDA Authenticity#

All PDAs must derive correctly from their seeds.

INV-G3: Discriminator Integrity#

All accounts must have correct discriminators.

Market Invariants#

INV-M1: Epoch Alignment#

Market timing must align to the configured duration epochs.

forall market M:
    M.t_start == M.market_id * 900
    M.t_end == M.t_start + 900
    M.t_start % 900 == 0

INV-M2: Snapshot Immutability#

Once captured, snapshots never change.

forall market M:
    once(M.start_price != 0) -> always(M.start_price unchanged)
    once(M.end_price != 0) -> always(M.end_price unchanged)

INV-M3: Resolution Determinism#

Same snapshots produce same outcome.

forall markets M1, M2:
    (M1.start_price == M2.start_price AND M1.end_price == M2.end_price)
    -> M1.outcome == M2.outcome

INV-M4: State Monotonicity#

States only transition forward.

INV-M5: Resolution Rule#

Outcome determined by price comparison.

Order Book Invariants#

INV-O1: No Crossed Book#

Best bid must be less than best ask.

forall orderbook O with non-empty bids and asks:
    O.best_bid < O.best_ask

INV-O2: Price Bounds#

All prices within valid range.

INV-O3: Quantity Positive#

All orders have positive quantity.

INV-O4: Order Ownership#

All orders have valid owner positions.

INV-O5: Sorted Orders#

Bids sorted descending, asks sorted ascending.

forall orderbook O:
    O.bids is sorted descending by price
    O.asks is sorted ascending by price

Position Invariants#

INV-P1: Non-Negative Shares#

No negative share balances.

forall position P:
    P.yes_shares >= 0
    P.no_shares >= 0

INV-P2: Locked Less Than Total#

Locked shares cannot exceed total.

forall position P:
    P.locked_yes_shares <= P.yes_shares
    P.locked_no_shares <= P.no_shares

INV-P3: Single Settlement#

Positions settle at most once.

forall position P:
    once(P.settled) -> always(P.settled)
    P.settled -> P.payout is final

INV-P4: Collateral Coverage#

Locked collateral covers buy orders.

Vault Invariants#

INV-V1: Solvency#

Vault covers worst-case payouts.

INV-V2: Conservation#

Trading preserves total value.

INV-V3: Empty at Close#

Vault empty when market closes.

INV-V4: Share Balance#

Total shares match sum of positions.

forall market M:
    M.total_yes_shares == sum(P.yes_shares + P.locked_yes_shares for P in positions)
    M.total_no_shares == sum(P.no_shares + P.locked_no_shares for P in positions)

Timing Invariants#

INV-T1: Snapshot Timing#

Snapshots captured after boundaries.

forall market M:
    M.start_price_timestamp >= M.t_start
    M.end_price_timestamp >= M.t_end

INV-T2: Trading Window#

Trading only during trading period.

forall order placed at time t in market M:
    M.t_start <= t < M.t_end

INV-T3: Settlement After Resolution#

Settlement only after outcome determined.

Fee Invariants#

INV-F1: Fee Collection#

Fees properly collected from takers.

INV-F2: Rebate Distribution#

Rebates properly paid to makers.

INV-F3: Fee Constraint#

Maker rebate never exceeds taker fee.

Verification#

Runtime Checks#

Each invariant has corresponding runtime assertions:

fn assert_solvency(market: &Market, vault: &TokenAccount) {
    let max_shares = max(market.total_yes_shares, market.total_no_shares);
    assert!(vault.amount >= max_shares, "INV-V1 violated");
}

fn assert_no_crossed_book(orderbook: &Orderbook) {
    if orderbook.bid_count > 0 && orderbook.ask_count > 0 {
        assert!(
            orderbook.best_bid_price < orderbook.best_ask_price,
            "INV-O1 violated"
        );
    }
}

Property Tests#

Invariants verified with property testing:

#[test]
fn test_solvency_preserved() {
    proptest!(|(operations in vec(arbitrary_operation(), 0..100))| {
        let mut state = initial_state();

        for op in operations {
            state = apply_operation(state, op);

            // Invariant must hold after every operation
            assert!(
                state.vault >= max(state.total_yes, state.total_no),
                "Solvency violated"
            );
        }
    });
}

Formal Verification Targets#

Invariant Violations#

Detection#

Invariant violations manifest as:

• Transaction failures with specific errors
• Inconsistent state (detectable via indexer)
• Unexpected account balances

Response#

If an invariant is violated:

1. P0 Alert: Immediate investigation
2. Root Cause: Identify the violation
3. Mitigation: Pause if possible
4. Fix: Deploy corrected code

Next Steps#

• See Threat Model for attack analysis
• Review Architecture Security for implementation