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.

forall account A managed by protocol:
    A.owner == PROGRAM_ID

INV-G2: PDA Authenticity

All PDAs must derive correctly from their seeds.

forall PDA P with seeds S and bump B:
    P == create_program_address(S ++ [B], PROGRAM_ID)

INV-G3: Discriminator Integrity

All accounts must have correct discriminators.

forall account A of type T:
    A.data[0..8] == T::DISCRIMINATOR

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.

forall market M:
    state(M) transitions only:
        PENDING -> CREATED -> TRADING -> SETTLING -> RESOLVED -> CLOSED

INV-M5: Resolution Rule

Outcome determined by price comparison.

forall resolved market M:
    M.outcome == (M.end_price >= M.start_price ? UP : DOWN)

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.

forall order ord in orderbook:
    0 < ord.price_bps < 10_000

INV-O3: Quantity Positive

All orders have positive quantity.

forall order ord in orderbook:
    ord.quantity > 0

INV-O4: Order Ownership

All orders have valid owner positions.

forall order ord:
    exists position P: P.owner == ord.owner

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.

forall position P:
    P.collateral_locked == sum(buy_order.value for buy_order in P.orders)

Vault Invariants

INV-V1: Solvency

Vault covers worst-case payouts.

forall market M with vault V:
    V.amount >= max(M.total_yes_shares, M.total_no_shares)

INV-V2: Conservation

Trading preserves total value.

forall trade T:
    collateral_in == collateral_out + fees

INV-V3: Empty at Close

Vault empty when market closes.

forall market M transitioning to CLOSED:
    M.vault.amount == 0

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.

forall settlement S in market M:
    M.outcome != None

Fee Invariants

INV-F1: Fee Collection

Fees properly collected from takers.

forall trade T:
    T.taker_fee == T.value * taker_fee_bps / 10_000 (ceiling)

INV-F2: Rebate Distribution

Rebates properly paid to makers.

forall trade T:
    T.maker_rebate == T.value * maker_rebate_bps / 10_000

INV-F3: Fee Constraint

Maker rebate never exceeds taker fee.

forall config:
    config.maker_rebate_bps <= config.taker_fee_bps

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