Residual-Risk Register#
Status: Authoritative residual-risk ledger for the verification-suite gap-closure plan Last updated: 2026-08-04 Scope: Every unresolved verification/assurance concern surfaced by Workstreams 0/A/B/C (Tasks 1–19) plus the controller-tracked cross-plan residuals. Each row is a concern that is known and accepted-for-now, not a hidden gap.
How to read this register#
- blocks deployment (Y/N) is a considered engineering judgement, not a rubber stamp.
Ymeans the item should be closed (or formally waived by the deployer) before mainnet.Nmeans the item is documented, low-severity, already mitigated, or a design assumption — it does not by itself gate a launch. - Liveness properties (
L-1..L-6,spec/STATE.md §5) are recorded as dependencies, not proofs. None of them is claimed as proven, because each depends on scheduling, validator behaviour, liquidity, or an off-chain actor. See the dedicated liveness section. - Line/file citations in this document were checked against source at the revision noted above. Where a cell reports the outcome of a source check (e.g. RR-CLK-01), that outcome reflects the specific lines cited in the cell; a cell that relays an unverified author claim says so explicitly rather than presenting it as an audited fact.
Register#
Current-candidate reconciliation (2026-08-05)#
- RR-SUB-01 is closed locally:
program/tests/adversarial_external_resolver.rspasses 26/26, including substituted-market probes for submit, halt, update-close, and expiry paths. The historical row below is retained for provenance and is not a current deployment blocker. - RR-FUZZ-01 has bounded local evidence: a 30-second
fuzz_market_lifecycle_realrun completed 62,435,492 executions with zero failures. The required 600-second Linux/CI release campaign remains pending. - RR-MUT-01 remains open: the recorded 7128-bps baseline is below the 9000-bps policy floor; no re-baseline or waiver is claimed here.
- RR-MUT-02 is fixed in the current harness:
run_mutation_baseline.shnow passes the declared killer targets through cargo-mutants' all-phase--cargo-argform. The historical row below is retained for provenance; a fresh Linux baseline is still required before changing RR-MUT-01. - RR-COV-04 has current local evidence: the canonical-v1-controller lane completed 26/26 tests after dependencies were restored. The historical environment-blocked wording below is retained for provenance and is not a current blocker.
| ID | Concern | Why unresolved | Impact | Mitigation | Next step | Blocks deployment (Y/N) |
|---|---|---|---|---|---|---|
| F-13-01 | close_market.rs:621-624 accepts any program-owned account ≥ MARKET_ACCOUNT_SIZE (464 B) lacking the market discriminator in the market slot; the early OrderbookProgress::default().set_return_data(); return Ok(()) short-circuits before the distinctness sweep ensure_close_market_writable_accounts_distinct (called at :630), so 3 substitution pairs (orderbook / trader_ledger / config → market slot) never reach that guard. | Left unpatched by design (LOW). The in-source comment at :618-620 claiming the branch is "unreachable in production" is factually false — the branch is reachable. | No state mutation, no fund loss: the only observable is a false-success OrderbookProgress return-data payload. Off-chain consumers of that return data could be misled into thinking a close made progress. | Atomic instruction; no child account is mutated on this path; SPL custody untouched. | Apply suggested fix: return Err(SeesawError::InvalidAccountType) at the discriminator branch; delete/correct the false "unreachable" comment. | N |
| F-15-01 | ensure_trader_ledger_space.rs is_uninitialized_trader_ledger_data (:118-122) and the oversized-slack no-op branch (:220-229) check only the 56-byte TraderLedgerHeader prefix, while the guard's doc comment ("Mirrors ensure_deep_orderbook_space's zeroness guard") claims whole-buffer parity with the orderbook guard. | INFORMATIONAL, unpatched by design. Harmless today: CreateMarket zero-fills the readable region (create_market.rs:896 ledger_data[..total_size].fill(0)) and readers are bound to header.capacity * SLOT::SIZE. | Latent only: if a future write path ever produced a zero-header / non-zero-body buffer, or the create-time zero-fill narrowed, a stale body could be mistaken for uninitialized slack. | Bounded by current zero-fill + capacity-bound reads; no live path produces the hazardous buffer. | Either widen the guard to a whole-buffer zeroness check (true parity with the orderbook guard) or correct the doc comment to state the header-prefix scope. | N |
| F-16-01 | Three token loaders — load_mint_shares_token_context_with_vault_authority (loaders.rs:928), load_withdraw_shares_token_context (:1002), load_redeem_token_context_with_vault_authority (:1068) — skip validate_token_account_initialized (utils/account.rs:354), so a frozen settlement ATA fails LATE at CPI (AccountFrozen) rather than at a clean pre-CPI guard. | INFORMATIONAL, unpatched by design. | Error-legibility only. Atomic revert contains it; no fund loss. Only the USDT settlement ATA is freezable (Tether holds freeze authority); YES/NO mints have freeze_authority = None, so those legs are unreachable. | Transaction reverts atomically; SPL Token program enforces the freeze at CPI. | Optionally add validate_token_account_initialized for a legible pre-CPI error; purely diagnostic. | N |
| F-18-01 | HaltMarket rejects a second halt with InvalidStateTransition (0x1011) — halt_market.rs:45-54 (market.is_halted() branch), unit-tested at :133-161 — while FOUR shipped docs assert idempotency: spec/IX.md:4109-4111, docs/security/invariants.md:287-288 (INV-EXT-3), spec/ORACLE.md:980-981, docs/security/instruction-validation-matrix.md:102. Also a stale 0x4C signer-shape description at spec/IX.md:4099-4104. | INFORMATIONAL doc-vs-code drift, unpatched by design. | The code takes the safer fail-closed side. Off-chain keepers built to the (wrong) idempotent spec get a hard revert instead of a retryable no-op event. | Code is the safer behaviour; the divergence is documentation, not on-chain risk. | Fix the DOCS (not the code): correct the four idempotency claims and the stale 0x4C signer-shape line to match fail-closed behaviour. | N |
| RR-MUT-01 | First-ever mutation baseline (Task 2): 2125 mutants, kill rate 7128 bps vs the 9000 bps policy floor in scripts/mutation_baseline_policy.json → the suite FAILS its own declared mutation policy (short by 1872 bps). Artifact: docs/internal/mutation-baseline-2026-08-03.md. | The 7128 bps figure measures only the policy's narrow test set (--lib + three killer targets), and most survivors are gap-classified as corruption-only-observable or equivalent — but the number, as declared, is below floor. | A declared, self-imposed quality gate is red. Survivor concentration is in validation guards (see RR-MUT-03), i.e. exactly the defensive code whose weakening is hardest to observe. | Extensive integration/property/fuzz/Kani suites cover behaviour the mutation policy set does not; survivors are triaged in the baseline doc. | Kill the gap-classed survivors (RR-MUT-03) and/or re-scope + re-baseline the policy; a red mutation gate must be green or explicitly waived before mainnet. | Y |
| RR-MUT-02 | Mutation harness-config bugs (Task 2): the policy testArgs place the target restriction after -- (test phase only) instead of via -C (both phases), so the BUILD phase runs unrestricted; plus the -C flag-placement and duplicate-enumeration harness bugs. | Documented, not yet fixed. | Distorts the mutation run (over-broad build phase, duplicated enumeration) — inflates cost and can misreport coverage; does not affect on-chain code. | Behaviour is understood and disclosed in the baseline doc §6/§ harness notes. | Move testArgs from post--- to -C form; fix flag placement and de-duplicate enumeration; re-run baseline. | N |
| RR-MUT-03 | Gap-classified surviving mutants concentrated in deep-orderbook validation guards: validate_pointer fn→Ok(()) (read path loaders-level and write path DeepOrderbookViewMutInner::validate_pointer L1615) and validate_live_slot ||→&& ×7 (L892-898) — each survivor is [NOWHERE] in cargo tests by name. | Accepted deferral (Task 2). These guards are exercised only indirectly by traversals that never feed corrupted bytes for the surviving predicates. | If a future regression genuinely weakened these guards, arena-bounds / liveness-predicate corruption could read adjacent arena bytes as nodes — but only on already-corrupt state, and no such input path exists today. | Guards are proven in formal/verification/dob_v3_proofs.rs; corruption is unreachable from legal inputs. | Add per-predicate corrupted-node/order killer fixtures asserting OrderbookTreeCorruption / arena-bounds errors. Note: _kani_validate_free_list fn→Ok(0)/Ok(1) was RECLASSIFIED equivalent (EQ-E, cfg(kani)-only dead code), NOT a gap survivor. | N |
| RR-KANI-01 | 22+ instruction discriminants have zero Kani (formal) coverage. | Formal proofs were scoped to the highest-value invariants (solvency, no-crossed-book, seat sizing, payout); the long tail of instructions is out of formal scope. | Absence of a machine-checked proof for these instructions — not a defect. Solana runtime checks + integration/property tests cover them. | Runtime tests, property tests, and fuzz targets exercise these paths. | Extend Kani harnesses opportunistically to the highest-value uncovered instructions; treat as continuous improvement, not a gate. | N |
| RR-COV-01 | 8 instructions with ZERO runtime coverage (Task 19 accepted deferrals): SettleSpline 0x44, DepositSplineVault 0x45, WithdrawSplineVault 0x46, CloseSpline 0x47 (missing spline-subsystem fixtures), TopUpCloserRewards 0x35 (no test builder), and UpdateOperationalParams 0x2F, InitResolverRegistry 0x48, UpdateResolverRegistry 0x49 (builderless governance). Retired prelaunch tag 0x32 is reserved and rejected, so it is not an executable coverage gap. | Test-builder / fixture gaps deferred in Task 19. | The four spline 0x44-0x47 plus 0x35 are fund-movers — shipping fund-moving code with no executed test is the higher-value residual. The three governance/config instructions move no funds. | Logic layers are shared with covered instructions; some paths are indirectly exercised. | Build spline-subsystem fixtures + a 0x35 builder and add execution tests for the 5 fund-movers before mainnet; governance builders can follow. | Y (fund-movers 0x44-0x47, 0x35; the 3 governance/config alone would be N) |
| RR-COV-04 | The canonical-v1-controller JavaScript lane is not currently verifiable in this worktree: pnpm test:canonical-v1-controller does not complete because the worktree has no installed node_modules; the nine failures reported in the prior review were not reproduced. | Environment/dependency state prevents reproducing the prior test result; no corresponding on-chain failure has been established. | The broad JS gate cannot be claimed green from this worktree until dependencies are restored and the lane completes. | The blocked command and prior review context remain explicit rather than being folded into a generic pass claim. | Restore the monorepo dependencies, rerun the lane, and reconcile any confirmed controller expectation drift with the current contract. | N |
| RR-COV-02 | ClaimReferrerEarnings 0x24: authorization (signer + wrong-authority) is NOW tested, but the vault-delta conservation assertion is deferred. | A faithful conservation test needs the real place_order-with-referral → rollup_referral_fees accrual pipeline; byte-patching a fake balance would be a vacuous fixture. | No conservation witness for the claim path; auth is covered, so unauthorized drains are blocked. Value-conservation on claim is un-witnessed. | Auth guards tested; accrual guards source-verified elsewhere (see RR-REF-01). | Add an end-to-end fixture: place referral order → rollup → claim → assert vault delta equals accrued fees. | N |
| RR-DIST-01 | The plan tracks ~49 processors that do not perform explicit writable-account distinctness checks (only ~31 of 75 processor/validation files carry a distinct/aliasing guard). | Per-processor distinctness triage was not completed across the whole surface; F-13-01 further shows one existing sweep can be bypassed on a false-success path. | Duplicate-mutable-account aliasing is a real Solana vuln class; however no aliasing exploit is demonstrated, and the high-value mutators (matching, settlement, close) carry explicit distinct checks. | Solana runtime borrow rules + explicit distinct guards on the fund-moving mutators contain the highest-value cases. | Triage each of the 49 processors: confirm either no two writable accounts can alias harmfully, or add a distinctness guard. No proven exploit gates launch. | N |
| RR-OB-01 | Bounded orderbook conservation (Task 17): conservation proofs run at #[kani::unwind(2)]–unwind(4) / match_limit=3 against a bounded shallow-book fixture with capacity 63 per side — a bounded result, now disclosed in orderbook/.../mod.rs and docs/security/invariants.md (INV-O1). The live runtime uses deep RBT tiers and is covered separately. The no-crossed-book harnesses run deeper (unwind(8) and unwind(33)). | Full-depth symbolic proof is intractable; the bound is a deliberate, disclosed model limitation (MODEL-LIMITED). | Conservation is machine-proven only for shallow fill sequences; behaviour at deeper fill depths relies on fuzz + property + integration tests, not formal proof. | Disclosed in-source and in INV-O1; complemented by fuzz (fuzz_orderbook_operations) and property tests; no-crossed-book proven deeper. | Raise unwind bounds where tractable; keep fuzz/property coverage as the deep-depth assurance. | N |
| RR-CLK-01 | The protocol has a trait-layer fail-to-zero clock read: traits/solana_context.rs:1266-1268 (impl ProcessorContext for SolanaContext, fn current_timestamp) returns match Clock::get() { Ok(clock) => clock.unix_timestamp, Err(_) => 0 } — a silent zero on Clock failure in LIVE (non-cfg-gated) code. This coexists with wrapper-level Clock::get()? error-propagation sites (e.g. halt_market.rs:41, close_market.rs:609); the protocol has TWO clock-read patterns, and every processor consuming ProcessorContext::current_timestamp() flows through the fail-to-zero path. | The zero-timestamp fail-safe has not been verified end-to-end: no adversarial test forces Clock::get() to fail, and the "fails safely" claim has not been checked across all current_timestamp() consumers. | If current_timestamp() returns 0, market_id = floor(0/duration) = 0 and lifecycle gates (TradingNotStarted/EpochNotEnded) evaluate against a zero clock — safe only if every downstream consumer rejects on that value. | The author's design comment (solana_context.rs:1258-1265) asserts zero fails safe (market_id=0 matches no PDA; lifecycle checks reject; avoids on-chain panic / full-CU burn). This register did NOT verify that assertion — it is the code author's claim, not an audited fact. The Solana runtime also normally guarantees the Clock sysvar is present for valid programs. | Verify zero-timestamp safety across all current_timestamp() consumers (does each reject a 0 clock?), and/or add an adversarial test that forces the Err(_) => 0 branch and asserts safe rejection. Cross-ref sibling assumption FV-ASM-011 (marks the fail-safe unproved + untested). | N — but this N rests on the author's fail-safe claim being true, which is itself unverified (see FV-ASM-011). If a single current_timestamp() consumer treats 0 as a valid clock, this would need re-rating. |
| RR-FUZZ-01 | fuzz_market_lifecycle_real (Task 17): the intended 600 s coverage-guided libFuzzer campaign NEVER RAN — ASan × macOS-dyld livelock before main. The harness builds and a 20 000-iteration deterministic sweep passed as a fallback. | Environmental (macOS ASan livelock), not a code defect; the real coverage-guided campaign was not obtained. | A fund-moving lifecycle path did not receive its intended coverage-guided fuzz assurance; only a deterministic sweep (no coverage feedback) ran. | Harness compiles; 20k deterministic sweep passed; other lifecycle paths have integration/property coverage. | Run the real coverage-guided campaign on a Linux host / CI before mainnet — low cost, closes the intended assurance. | Y (pre-mainnet) |
| RR-FV-01 | FV-ACCT-001 (Task 9): the seat-size whitelist proof's model restates the gate's own loop (same table), so it cannot catch a wrong constant inside the whitelist. | Strengthening requires an independent oracle; deferred as follow-up FV-ACCT-001-strengthen. | The proof gives weaker assurance than it appears — a mis-entered whitelist byte size would pass both gate and proof. | Whitelist values are also exercised by runtime layout-registry tests (account_layout_registry). | Implement FV-ACCT-001-strengthen: hardcode the 9 expected seat byte sizes as an independent oracle in the proof. | N |
| RR-FV-02 | P-LOADER-01 DELETED (Task 10): the PDA-binding proof was removed as SHA-256-intractable (create_program_address runs SHA-256; CBMC cannot symbolically execute it). FV-PDA-001 now proves the canonical-bump COMPARISON but NOT the derivation. | The hash is fundamentally out of formal reach. | No formal proof that a PDA's derivation binds to its seeds; only the bump comparison is proven. | The derivation is covered by runtime PDA-validation tests instead. | Keep runtime PDA tests as the assurance layer; document the formal boundary (done). No further formal work feasible. | N |
| RR-FV-03 | MODEL-LIMITED formal areas lacking a dedicated adversarial (negative) test: the bounded orderbook depth (RR-OB-01), the SHA-256 PDA derivation boundary (RR-FV-02), and the whitelist-restatement proof (RR-FV-01) each represent a formal model that is narrower than the real system. | Formal models are intentionally bounded/abstracted; adversarial coverage of the un-modelled remainder is partial. | Where a formal model is narrower than reality, "proven" applies only within the model's bounds — over-reading these proofs would overstate assurance. | Each model limit is disclosed at its site (INV-O1, FV-PDA-001, FV-ACCT-001) and complemented by runtime/fuzz tests. | Pair each MODEL-LIMITED proof with at least one adversarial/negative runtime test that probes just outside the model bound. | N |
| RR-SUB-01 | Cross-resolver substitution surface (Task 18 reviewer observation): non-external instructions load external markets via the same PDA-skipping load_market_context, and were NOT probed for cross-resolver market substitution. | Not probed — an unverified security surface, not a confirmed defect. | If PlaceOrder / Redeem / MarkPositionSettled etc. do not bind their vault / orderbook / position children to the market address, the same substitution surface exists there; likely-safe hypothesis is that they do bind to address. | The high-value external-lifecycle instructions carry explicit binding; the concern is the un-probed remainder. | Confirm (test or source proof) that these non-external instructions bind every child (vault/orderbook/position) to the market address — resolve this unknown before mainnet. | Y (verification gate; not a confirmed defect) |
| RR-REC-01 | Recreation-through-program (Task 14): the create_account_cpi zero-data-target tolerance (account revival after close) is DEMONSTRATED via set_account simulation but NOT mechanized through the program. The inheritance-impossibility half IS runtime-proven (drain-to-zero). | Mechanizing revival-through-program requires a program-driven fixture not yet built. | One half of the recreation model (revival) rests on a simulation, not a program-driven test; the more dangerous half (state inheritance) is runtime-proven impossible. | Drain-to-zero runtime proof covers the inheritance risk; revival tolerance is understood via simulation. | Add a program-driven fixture that closes then recreates an account and asserts no stale state survives. | N |
| RR-REF-01 | RollupReferralFees double-payout guard (Task 14): source-verified (rollup_referral_fees.rs:130 — per-position pending_referral_fees() == 0 → InvalidReferralRollupBatch before the only transfer) but has NO runtime witness. | A faithful witness needs the full accrual pipeline (ties to RR-COV-02). | The double-payout guard is correct by source review but un-witnessed by an executed test. | Guard is source-verified and structurally simple (reject-before-transfer). | Add a runtime test: roll the same position twice, assert the second batch rejects with InvalidReferralRollupBatch and no second transfer occurs. | N |
| RR-CI-01 | CI env drift (Task 3): cargo-mutants 27.1.0 installed vs 24.11.1 pinned; python3 3.14.3 vs 3.12.x pinned. ci-full.yml will hard-fail on the lean-gate once GitHub Actions is re-enabled. | A tracking comment was added; no install/pin step was implemented. | CI (not the program) will fail the lean-gate on re-enable; no on-chain impact. Note: GitHub Actions is currently disabled for this repo. | Drift is documented; failure mode is understood and loud (hard-fail, not silent). | Add pinned-install steps (or update pins) before re-enabling GitHub Actions. | N |
| RR-LIVE-01 (L-1) | create_market opens trading atomically against the current clock (market_id = floor(current_ts/duration); t_start ≤ current_ts < t_end) — CREATED→TRADING in one instruction. spec/STATE.md:336. | Not claimed as proven. Requires a permissionless operator to call create_market in the epoch. | If no operator calls it, the market stays PENDING and users cannot trade (degraded mode, spec/STATE.md:384). | Permissionless (anyone can call); crank-reward incentive. | None — this is a documented liveness dependency, not a defect. | N |
| RR-LIVE-02 (L-2) | snapshot_end is assumed called within 60 s of t_end (spec/STATE.md:338). | Not proven — depends on off-chain crank scheduling. | If unmet, market stays TRADING until force-expire (spec/STATE.md:385). | Permissionless crank + ForceClose/ExpireMarket fallbacks; crank rewards. | Documented dependency only. | N |
| RR-LIVE-03 (L-3) | resolve_market is assumed called within 60 s of both snapshots (spec/STATE.md:344). | Not proven — depends on off-chain crank scheduling. | Delay leaves the market in SETTLING; funds are not at risk, only resolution latency. | Permissionless; ForceClose may unwind eligible locks without setting outcome by t_expire (:388). | Documented dependency only. | N |
| RR-LIVE-04 (L-4) | Permissionless operators roll pending referral fees before teardown; unrolled fees are forfeited to creator fees at resolved_at + 604 800 s (spec/STATE.md:350-360). | Not proven — depends on an off-chain actor rolling fees before the grace deadline; the treasury shard must first exist via 0x37. | If no operator rolls in time, the referrer loses entitlement (fees reclassified to creator via ReferralPendingForfeited); CloseMarket is otherwise blocked by ReferralFeesPending. | Permissionless rollup + close-blocking guard preserves entitlement until the grace deadline. | Documented dependency only; not a solvency risk (liability is reclassified, not lost). | N |
| RR-LIVE-05 (L-5) | Pyth publishes ≥ 1 valid update per 30 s window (spec/STATE.md:370). | Not proven — external oracle/validator behaviour. | If violated, snapshots wait for a valid price (spec/STATE.md:386-387). | Sampling Rule A (first price ≥ boundary); market waits rather than resolving on stale data. | Documented external dependency only. | N |
| RR-LIVE-06 (L-6) | If Pyth is stale > 300 s at boundaries, the market MAY remain in SETTLING until an update arrives or it expires (spec/STATE.md:376). | Not proven — external oracle liveness; explicitly a "MAY" degraded-mode behaviour. | Prolonged SETTLING; resolved via later update or t_expire unwind, no fund loss. | Snapshot immutability + wait-for-valid-price + expiry fallback. | Documented external dependency only. | N |
Liveness treatment (Task Step 2)#
spec/STATE.md §5 defines six liveness assumptions (L-1..L-6). None is recorded as a proven property in this register, because every one depends on something outside the program's deterministic control:
| Property | Depends on | Recorded as |
|---|---|---|
| L-1 | An off-chain operator calling create_market in the epoch (scheduling) | Dependency (RR-LIVE-01) |
| L-2 | Crank scheduling of snapshot_end | Dependency (RR-LIVE-02) |
| L-3 | Crank scheduling of resolve_market | Dependency (RR-LIVE-03) |
| L-4 | An off-chain operator rolling referral fees before a deadline | Dependency (RR-LIVE-04) |
| L-5 | Pyth / validator publish cadence | Dependency (RR-LIVE-05) |
| L-6 | Pyth staleness / validator behaviour | Dependency (RR-LIVE-06) |
The protocol's degraded-mode table (spec/STATE.md:378-389) is the mitigation: every liveness failure degrades to a safe, no-fund-loss state (PENDING / TRADING-until-force-expire / wait-for-price / ForceClose unwind), never to an insolvent or value-destroying one. This is why all six are blocks deployment = N: they are design assumptions with documented safe fallbacks, not defects.
Deployment-blocking summary#
RR-COV-01 is closed on the current tree. The historical row above predates
the executed spline and closer-reward fixtures: program/tests/spline_lifecycle.rs
passes 34 tests, and program/tests/integration_top_up_closer_rewards.rs passes
its runtime flow. Keep the row for provenance, but do not treat its old zero-
coverage claim as a current blocker.
RR-SUB-01 is also closed on the current tree. The adversarial external resolver battery passes 26/26 tests, including substituted-market probes for submit, halt, close-time, and expiry paths; all reject before victim mutation.
Two items remain marked Y (should be closed or formally waived before mainnet):
- RR-MUT-01 — the suite fails its own declared 9000 bps mutation policy floor (7128 bps). A red, self-imposed quality gate must be green or explicitly waived.
- RR-FUZZ-01 — a bounded 30-second local
fuzz_market_lifecycle_realrun now passes (62,435,492 executions, zero failures), but the intended 600-second release campaign and Linux/CI evidence remain outstanding.
All other rows are documented, low-severity, already-mitigated, or design assumptions and do not by themselves block deployment.