Assumption Registry#
Consolidated registry of the trust and environmental assumptions the Seesaw
on-chain program depends on. Each row states an assumption that, if false,
would weaken or void one or more of the protocol invariants in
invariants.md.
Assumptions were previously scattered across
threat-model.md, README.md,
upgrade-policy.md, spec/SECURITY.md §1.3,
spec/STATE.md §5, and
docs/internal/KNOWN_LIMITATIONS.md. Several
security-critical assumptions previously lived only inside Kani harness doc
comments under formal/verification/; those are promoted here and flagged
[harness-buried].
How to read this table#
- Enforced on-chain — does the program itself reject a transaction when this
assumption is violated?
Nmeans the program cannot detect or prevent the violation. - Guaranteed by Solana — is the assumption a property the Solana runtime / validator set already provides, rather than something Seesaw enforces?
- Depends on external program / operations — the off-chain or third-party dependency the assumption rests on.
- Can it be eliminated — whether a code, design, or governance change could remove the assumption, and roughly how.
Registry#
| ID | Assumption (exact statement) | Why it is needed | Relying component(s) | Enforced on-chain | Guaranteed by Solana | Depends on external program / operations | Consequence if false | Available monitoring | Can it be eliminated |
|---|---|---|---|---|---|---|---|---|---|
| FV-ASM-001 | The SPL Token v1 program transfers exactly the requested amount, mints/burns exactly as instructed, exposes no transfer hook or callback, and keeps its balance semantics 1:1 (no rebasing, no fee-on-transfer). | Solvency (INV-V1) and conservation invariants assume a fixed 1:1 relationship between tokens moved and vault/escrow balance deltas; matching, minting, redeem, and escrow all rely on it. | Vault/escrow transfers, MintShares, WithdrawShares, Redeem, order matching, fee routing. | Partial — the program rejects any account NOT owned by SPL Token v1; Token-2022 accounts are intentionally rejected (KNOWN_LIMITATIONS L-004). It cannot re-audit SPL Token itself. | N | SPL Token v1 program (Tokenkeg…). | Fee-on-transfer / hook / rebasing behaviour would silently break solvency and conservation; vault could become under-collateralized. | Runtime solvency tripwire on every mutating instruction; SPL is immutable & battle-tested. | No — SPL v1 is a foundational dependency. Token-2022 support would require re-deriving the solvency model. |
| FV-ASM-002 | The settlement mint's freeze authority (e.g. Tether's authority over USDT) will not freeze a market vault PDA, escrow PDA, treasury recipient, or user payout ATA in a way that strands protocol-held funds. | The program signs SPL transfers out of vault/escrow; a frozen source or destination blocks those transfers with no on-chain override. | Vault, escrow, treasury recipients, referrer-treasury shards, redemption/withdraw paths. | N — the program cannot override an issuer freeze. | N | Settlement-token issuer (freeze/blacklist authority external to Seesaw). | Affected redemptions, escrow returns, or fee claims are blocked until unfreeze; a frozen vault halts a market's payouts. Accepted settlement-asset tail risk (threat-model "Settlement-Token Issuer Freeze"). | Operators monitor live vault/payout/treasury addresses against the issuer's freeze surface; contain via global Pause (0x25), per-market SetMarketEmergencyStatus (0x2C), and treasury shard rerouting. | Partially — a per-asset settlement allowlist / multi-mint policy (MINT-01) reduces exposure; cannot be eliminated while a freeze-capable mint is the settlement asset. |
| FV-ASM-003 | Pyth Network reports honest, un-manipulated prices; the aggregated feed value is a faithful reflection of the underlying market. | Native-price markets resolve UP/DOWN from Pyth start/end snapshots; a manipulated print flips resolution. | snapshot_end, resolve_market, oracle validation. | Partial — the program checks feed id, owner == pinned Pyth Core Receiver, price > 0, discriminator, verification level, and optional confidence gate. It cannot validate the truthfulness of an accepted price. | N | Pyth Network oracle programs. | A corrupted-but-well-formed price resolves markets to the wrong outcome; snapshot immutability then locks the wrong result in. | Confidence-ratio gate (when configured); off-chain price cross-checks; snapshot immutability prevents post-hoc change but not a bad capture. | No for v1 (single oracle). Multi-oracle / median support is future work (threat-model "Single oracle"). |
| FV-ASM-004 | The publish_time (and prev_publish_time) fields on a Pyth PriceUpdateV2 are accurate, so "first price with publish_time >= boundary" (Sampling Rule A) selects the correct print, and staleness is measured against a truthful clock. | Sampling Rule A firstness and the max_staleness (default 60s) gate both key off publish_time; snapshot correctness depends on it. | Oracle validation, snapshot_end, staleness check. | Partial — the program enforces publish_time >= boundary and prev_publish_time < boundary, and rejects readings older than max_staleness. It trusts the timestamp values themselves. | N | Pyth Network (timestamp authored by the feed). | A back-dated or forward-dated publish_time could let a non-first or stale price be accepted as the boundary snapshot, changing resolution. | Staleness rejection (StaleOracle); firstness proof via prev_publish_time; 7-day expiry fallback prevents permanent stall (KNOWN_LIMITATIONS L-001). | No — inherent to relying on the oracle's self-reported timestamp. |
| FV-ASM-005 | The pinned Pyth Core mainnet program IDs — derivation pyt2F414BA6dPttK6RddPZUdHfapoBN24GL5wbrPCou and Receiver/owner rec2HHDDnjLfj4kE7VyEtFA1HPGQLK33259532cRyHp — are and remain the correct upgraded Pyth Core programs. | Push-feed PDA re-derivation and owner validation compare against these frozen bytes; a wrong value would accept attacker-controlled feed accounts. | create_market (push PDA binding), oracle owner check. | Y — the IDs are hard-coded constants (oracle::pyth::PYTH_PROGRAM_ID_MAINNET / PYTH_RECEIVER_PROGRAM_ID_MAINNET), pinned by tests in constants_match_spec.rs. | N | Pyth governance (if Pyth Core migrates to new program IDs). | If Pyth migrates programs, snapshots break (feeds no longer validate) — a liveness failure, not a solvency one; a wrong pin would let forged feeds through. | constants_match_spec.rs pin tests; owner check rejects mismatched accounts at runtime. | Only via a program upgrade that re-pins new IDs (deliberate, gated by upgrade policy). |
| FV-ASM-006 | Pyth publishes at least one valid update within each 30-second window (STATE.md L-5), and stalls beyond ~300s at a boundary (L-6) are tolerable. | Timely snapshots (snapshot_end within 60s of t_end, L-2) require a fresh price to exist at the boundary. | snapshot_end, resolve_market, market lifecycle. | N — liveness cannot be enforced on-chain. | N | Pyth Network publishing cadence. | Market stays in TRADING/SETTLING until a fresh price arrives or the 7-day expiry force-close path is used; funds are not lost, resolution is delayed. | Degraded-mode table (STATE.md §5.3); force-expire fallback; operator monitoring of feed freshness. | No — external liveness property; mitigated by the expiry fallback. |
| FV-ASM-007 | The program's upgrade authority is held securely and used only through the reviewed release/governance process (upgrade-policy.md); the deployed program is not maliciously or accidentally upgraded. | The program is upgradeable; the holder of upgrade authority can replace program logic and thereby bypass every on-chain invariant. | Entire program (all invariants). | N — the runtime enforces who may upgrade, not whether an upgrade is safe. | Partial — Solana enforces upgrade-authority signature/BPFLoaderUpgradeable semantics; it does not judge intent. | Squads multisig + governance runbook + release signoff. | A malicious/compromised upgrade can replace program logic and drain vaults or corrupt state arbitrarily — total loss of program control. | External release-evidence bundle (ProgramData, authority, signatures, rooted slot); reviewer signoff; multisig quorum. | Yes — burning the upgrade authority (immutable no-upgrade-authority state) eliminates it, per the documented post-launch freeze review. |
| FV-ASM-008 | The Squads multisig signer set is independent (no single party controls a quorum) and members do not collude; the same custody backs ConfigAccount.authority. | Upgrade authority and config authority are only as strong as the multisig; a collusive/compromised quorum equals a compromised program. | Upgrade authority, config authority, admin setters. | N | N | Squads multisig program + off-chain key custody & signer distribution. | A colluding/compromised quorum can upgrade the program or push adversarial config (fees, treasury, pauser) — up to total loss. | Governance proposal/quorum/approval evidence; before/after config snapshots; STRAT-9 signoff. | Partially — a timelock, larger/more-diverse signer set, or eventual authority burn reduce/eliminate it. |
| FV-ASM-009 | Permissionless crank operators execute lifecycle transitions in a timely manner: snapshot_end within ~60s of t_end (L-2), resolve_market within ~60s of both snapshots (L-3), and referral rollups before the terminal grace deadline (L-4). | Markets are computed/permissionless; nobody is obligated to advance them, so timely resolution and teardown assume incentivized operators show up. | Market lifecycle (snapshot_end, resolve_market, RollupReferralFees, ClosePosition, CloseMarket). | N — liveness cannot be forced on-chain (all such ops are permissionless). | N | Independent crank/keeper operators (off-chain automation). | Delayed resolution/teardown; unrolled referral fees can be forfeited to creator fees after the 604,800s grace (L-4). Force-close fallback prevents permanent fund lock. | Reward incentives (closer_reward_lamports, TopUpCloserRewards); multiple independent operators; degraded-mode table; 7-day expiry force-close. | No — inherent to a permissionless design; mitigated by incentives and the expiry fallback. |
| FV-ASM-010 | The validator-provided Clock sysvar unix_timestamp is monotonic-enough and approximately truthful (no large-scale back-dating or forward-jumping by a colluding leader). | market_id = floor(ts / duration), epoch boundaries, staleness, and expiry all key off the on-chain clock; a manipulated clock shifts market identity and boundary comparisons. | create_market, snapshot/resolution boundary checks, expiry, staleness. | Partial — inclusive >= boundary comparisons avoid intra-epoch gaps (threat-model "Epoch Boundary Race"); the program cannot detect a dishonest validator clock. | Partial — Solana bounds clock drift via stake-weighted timestamp correction, but a supermajority-colluding leader set is out of Seesaw's control. | Solana validator set / clock sysvar. | Skewed timestamps could misalign a market's epoch or shift boundary snapshots, affecting which oracle print resolves a market. | Pyth publish_time cross-check at boundaries; inclusive comparisons; consensus-level timestamp correction. | No — clock is a runtime primitive; mitigated by cross-checking against oracle timestamps. |
| FV-ASM-011 | ProcessorContext::current_timestamp maps a Clock::get() sysvar failure to timestamp 0, and 0 is assumed to make all downstream time checks fail closed (no PDA matches market_id=0; TradingNotStarted/EpochNotEnded reject) rather than open. Unproved and untested. | The trait returns i64 (shared with MockContext, which never fails), so the failure path cannot surface an error; safety relies entirely on 0 being rejected everywhere downstream. | traits/solana_context.rs:1266-1268 (Err(_) => 0); every instruction that reads the clock. | Partial — the fail-to-zero is a deliberate fail-safe intent, but there is no test or Kani harness proving every timestamp consumer rejects 0. | Partial — Solana normally guarantees the Clock sysvar is present for valid programs; the branch handles the "should never happen" case. | Solana runtime (Clock sysvar availability). | If any timestamp consumer treats 0 as a valid early/boundary time rather than rejecting it, a sysvar-failure transaction could take an unintended path. No known consumer does, but it is unverified. | None specific today. Gap: no negative test exercises the Err(_) => 0 branch; recommended as a residual-risk / test item. | Yes — add a test/harness asserting every clock consumer rejects ts == 0, or change the trait to return Result and propagate the error. |
| FV-ASM-012 | A registered external resolver is honest with respect to its own markets — but by design it has full power over them: it may resolve any market it opened to any conserving payout split, at any time, with no timing gate (SECURITY.md §1.3). | The extensible-markets design commits one resolver authority per external market; native and external paths reject each other. The trust boundary is deliberate. | External market lifecycle, resolve/halt on external markets, resolver registry. | Partial — the program enforces which signer may resolve/halt a given market (resolver binding, INV-RESOLVER), but not whether the resolution is fair. | N | Registered external resolver authorities (governance-registered). | A malicious resolver can resolve its own markets adversarially (within the conserving-payout constraint) — losses are confined to traders who opted into that resolver's markets; native markets are unaffected. | Governance registration gate (resolver registry, 0x48/0x49); resolver binding rejects cross-path resolution; per-market isolation. | Partially — resolver-quality gating is a governance/registry concern; the per-market full-power model is intentional and bounded to opt-in markets. |
| FV-ASM-013 | The standalone Reclaim verifier's active epoch snapshot carries an attestor member set (up to 8 secp256k1 addresses) and a threshold, installed by verifier governance. A claim is accepted only when exactly threshold distinct members sign it, and the honest-content assumption is that the signing members' keys are honest and uncompromised. Selection algorithm 1 is the frozen single-member case (member_count == threshold == 1); algorithm 2 is threshold-of-set (1 <= threshold <= member_count <= 8), the same rule as Reclaim's canonical Reclaim.sol minimumWitnessesForClaimCreation. Shipped configuration: 1-of-3 - the three attestor addresses Reclaim publishes at https://api.reclaimprotocol.org/api/attestors, threshold 1. All three are Reclaim-operated keys: Reclaim's decentralized attestor AVS is Holesky-only and whitelisted as of 2026-09, so a higher threshold buys no operator independence. Raising the threshold is a verifier-governance staging action, not a code change. | The attestor signature is the sole trust root for external-market settlement; Seesaw binds every receipt to deployment, epoch, market, ticker, condition, and validity window, but it trusts the signed content. | Reclaim V1 lifecycle (0x52-0x56) via CPI into the compile-time-pinned standalone verifier; reclaim-verifier-core policy/signature/verify. | Partial - envelope binding, low-S enforcement, recovery-id restriction to {0,1}, duplicate-signer rejection, count == threshold, membership of every recovered address in the snapshot set, per-claim receipt consumption, and epoch binding are all on-chain; Seesaw additionally recomputes the signer-set commitment from its own read of the active snapshot plus the receipt's signer_bitmap and requires popcount == threshold and bitmap < 1 << member_count, so the verifier cannot assert a set it did not recover. Content honesty is not checkable on-chain. | N | Verifier governance (config.authority stages the snapshot) + the Reclaim attestor keys in the active set. | A compromised or self-staged member set resolves any mirror market arbitrarily (YES/NO/VOID/LeftOpen/ExtendClose). At the shipped threshold of 1 any single published Reclaim key suffices, so there is no collusion threshold to clear; because all three are Reclaim-operated, the trust root is Reclaim as an operator rather than an independent quorum. | Epoch rotation by verifier governance behind min_governance_delay_s; per-claim verified-claim receipts prevent replay; single-use policy operation bits (close extension may repeat with a fresh claim). | Partially - raising threshold toward member_count is a verifier-governance staging action and needs no Seesaw code change; the wire format and the signer bitmap already carry up to 8 signatures. Genuine reduction additionally requires independently operated attestors, which Reclaim does not yet expose on mainnet. |
| FV-ASM-014 | The cryptographic primitives Solana provides — Ed25519 signature verification, secp256k1 recovery, and SHA-256 (including PDA derivation seed hashing) — are secure: signatures are unforgeable and PDA seed hashes are collision/pre-image resistant. [harness-buried, partial] — pda_spec.rs notes Kani cannot model the seed hash, so PDA collision resistance is assumed, not proven, in formal coverage. | Owner/signer checks, resolver/witness signature verification, and PDA uniqueness (unique seed prefixes prevent account confusion) all rest on these primitives. | Signature verification (Reclaim/resolvers), all PDA derivations, account authorization. | Partial — the program uses the primitives correctly; it cannot detect a break of the primitive itself. | Partial — Solana provides the crypto syscalls (Ed25519/secp256k1/SHA-256), but their mathematical security is an industry-wide assumption, not a Solana guarantee. | Solana runtime crypto syscalls. | A break in Ed25519 or SHA-256 would allow forged authorizations or PDA collisions — catastrophic; considered infeasible (threat-model: Ed25519 "Very High" confidence). | Formal PDA proofs cover the seed construction (integration/property tests cover derivation); primitive security is an industry-wide assumption. | No — foundational cryptographic assumption. |
| FV-ASM-015 | The deployed program lives at the expected program ID SEEsawgSrxRsgtKRbaThZFEKrVqX3Y64hDipTWyi8F8 with the reviewed ProgramData/build hash; clients and PDAs are derived under this ID. | PDA seeds, client interactions, and the release-evidence bundle all assume the canonical deployment address and build hash. | All PDA derivations, all clients, release verification. | Partial — the runtime enforces that only this program owns its PDAs; the program cannot self-verify it is the reviewed build. | Partial — Solana guarantees program-ID/ownership binding, not build provenance. | Deployment operations (multisig deploy) + release-evidence review. | A wrong or unreviewed deployment (mismatched build hash) could ship unaudited logic under a trusted-looking address. | Release-evidence bundle records ProgramData, program hash, deploy signatures, rooted slot; on-chain PDA ownership. | No for the ID itself; build-hash trust is reduced by reproducible builds (FV-ASM-017). |
| FV-ASM-016 | The program's build/link-time dependencies (Pinocchio, SPL Token bindings, and all transitive crates) are the intended, un-tampered versions and contain no supply-chain backdoor. | Compiled dependency code executes with full program privileges; a malicious crate could subvert any invariant. | Whole program build. | N — cannot be checked on-chain. | N | Cargo registry / crate authors / build toolchain. | A backdoored dependency could exfiltrate authority or corrupt state — up to total loss. | Cargo.lock pinning; dependency review; reproducible builds; release signoff. | Partially — lockfile pinning, vendoring, and audited dependency sets reduce it; cannot be fully eliminated. |
| FV-ASM-017 | The deployed seesaw.so is byte-reproducible from the reviewed source commit, so the on-chain build hash provably corresponds to the audited code. | The upgrade policy requires verifiable program-build hashes; trust in the deployed logic reduces to trust in the reviewed source only if the build is reproducible. | Release verification, upgrade-authority process. | N | N | Reproducible-build toolchain + release-evidence review (upgrade-policy.md). | Without reproducibility, a mismatch between audited source and deployed bytecode cannot be detected — unreviewed logic could be live. | Build-hash comparison against release artifact hash in the evidence bundle; reviewer signoff for the exact commit. | Yes — a fully deterministic build pipeline eliminates the gap between source review and deployed bytecode. |
| FV-ASM-018 | The Solana runtime provides its documented execution guarantees: transaction-scoped account locking, no recursive/re-entrant CPI on overlapping writable accounts, single-threaded per-transaction execution, and rent-exemption semantics. | Reentrancy protection, settlement idempotency, and PDA-signed transfers all rely on runtime behaviour rather than in-program guards. | Reentrancy protection, all CPIs, escrow/vault transfers, rent lifecycle. | Partial — the program adds settlement idempotency (settled flag) and discriminator checks on top of the runtime; the runtime provides locking/CPI semantics. | Y — these are core Solana runtime properties. | Solana runtime. | A runtime that permitted re-entrant CPI or lock bypass would break reentrancy and idempotency assumptions. | Settlement settled/is_settled idempotency check; discriminator checks; industry-wide reliance on runtime correctness. | No — foundational runtime assumption. |
| FV-ASM-019 | sol_secp256k1_recover and keccak-256 are correct. The verifier recomputes the Reclaim identifier and the EIP-191 digest from the immutable proof-buffer bytes and recovers each attestor address itself, one sol_secp256k1_recover call per required signature; no Ed25519 native program and no instructions sysvar are involved. | Signature authenticity for Reclaim rests entirely on syscall correctness plus the verifier's own re-derivation of the signed preimage from bytes the relayer cannot influence. | Reclaim V1 claim verification (reclaim-verifier-core::{claim,signature,verify}, programs/reclaim-verifier/src/secp256k1.rs). | Partial - identifier keccak(provider\nparams\ncontext), the \x19Ethereum Signed Message:\n preimage, scalar range and low-S checks, and membership of every recovered address in the active snapshot's member set are all enforced on-chain; syscall correctness is not checkable from inside the program. | Y - sol_secp256k1_recover and keccak-256 are runtime-provided syscalls. | Solana runtime crypto syscalls. | A faulty syscall would accept forged signatures and corrupt every Reclaim resolution. | Runtime guarantee; reclaim-verifier-core carries unit vectors against Reclaim's createSignDataForClaim and getIdentifierFromClaimInfo, plus k256 cross-check recovery vectors. | No - the recover-and-compare pattern is the standard Solana mechanism for secp256k1 attestations. |
| FV-ASM-020 | The oracle price-normalization no-panic guarantee is formally proven only for bounded input widths (i32 prices / i8 exponents); production accepts full-width i64/i32 values, with wider domains "tracked for Phase 4." [harness-buried] — stated only in oracle_validation.rs harness comments. | Kani's no-panic proof for normalize_prices (oracle variant) is scoped narrower than the production input domain, so the formal guarantee does not cover the full range the program actually receives. | Oracle price normalization / conversion. | Partial — production code uses checked arithmetic (so a panic would fail the tx, not corrupt state), but the formal no-panic guarantee is not full-width. | N | None (internal formal-coverage scope limitation). | A panic on an unproven wide input would abort the transaction (fail-closed), consuming compute — a liveness/UX issue, not a solvency one; unproven for full width. | Checked arithmetic fails closed; property/fuzz tests exercise wider ranges; residual-risk item for Phase 4. | Yes — widening the Kani harness domains (Phase 4) closes the formal gap. |
| FV-ASM-021 | Order-book solvency is formally verified for a PlaceOrder that crosses at most 3 makers; a fill crossing 4+ makers in one PlaceOrder is outside the verified envelope and relies on runtime invariant tripwires instead. [harness-buried] — stated only in formal/verification/mod.rs. | The Kani solvency/reconciliation harnesses bound maker-cross depth for tractability; deeper books are guarded at runtime, not by proof. | Order matching (place_order), solvency reconciliation. | Y — runtime solvency tripwires execute on every matching path regardless of cross depth. | N | None (internal formal-coverage scope limitation). | A solvency bug reachable only at 4+ maker crosses would not be caught by formal proof, only by the runtime tripwire (which fails the tx closed). | Runtime solvency invariant checks on every fill; fuzz/property tests cover deeper books; residual-risk item. | Yes — extending the harness maker-cross depth (or an inductive proof over cross count) closes the formal gap. |
Harness-buried assumptions promoted here#
The following were load-bearing for a security property yet appeared only inside Kani harness doc comments before this registry. They are promoted above and flagged [harness-buried]:
| ID | Source harness | What was buried |
|---|---|---|
| FV-ASM-020 | formal/verification/oracle_validation.rs (oracle_normalize_never_panics_no_panic, ~L295) | Oracle normalize no-panic is proven only for i32/i8-bounded inputs; full production widths are "tracked for Phase 4." |
| FV-ASM-021 | formal/verification/mod.rs (module doc, ~L80-81) | Solvency proof envelope bounds PlaceOrder to ≤3 maker crosses; 4+ crosses rely on runtime tripwires, not formal proof. |
| FV-ASM-014 (partial) | formal/verification/pda_spec.rs (module doc, ~L9) | Kani cannot model the PDA seed hash, so PDA collision resistance is assumed rather than formally proven (folded into the cryptographic-primitives row). |
Scope note on the 469 Assumptions: lines. A grep -rn 'Assumptions:' formal/verification/*.rs | grep -v '(none)' returns 469 lines. Per the
mandatory harness doc format defined in formal/verification/mod.rs (§ "Proof
doc-comment format"), the overwhelming majority are Kani proof-scoping
preconditions (e.g. kani::assume(amount <= quote_locked), state = Pending)
that mirror a corresponding production guard and carry a Non-vacuity: witness
proving the assumed region is reachable. Those are proof narrowing, not
real-world trust assumptions, and are intentionally not promoted. Only the
handful above describe assumptions about the environment, runtime, or formal
coverage boundary that are not otherwise enforced/consolidated, and those are
promoted.
Related documents#
invariants.md— the invariants these assumptions protect.threat-model.md— adversary model and mitigations.upgrade-policy.md— upgrade authority & multisig custody.residual-risk.md— residual risks (including the unverified Clock fail-to-zero path, FV-ASM-011, and the harness-scope gaps FV-ASM-020/021).spec/SECURITY.md§1.3 — trust-assumption table.spec/STATE.md§5 — liveness assumptions (L-1..L-6).docs/internal/KNOWN_LIMITATIONS.md— accepted by-design limitations.