diff --git a/src/percolator.rs b/src/percolator.rs index 82558b6bc..239a2b0f6 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -655,6 +655,28 @@ pub struct RiskEngine { /// `admit_h_max_consumption_threshold_bps_opt = Some(t)`. pub price_move_consumed_bps_this_generation: u128, + /// Wave 1 / ENG-PORT-C: external-oracle target tracking. + /// + /// Latest target observation seen via the wrapper's `read_price_clamped` + /// path. The "target" is the raw external price the next admin/keeper + /// progress should clamp toward; the "effective" price (mark / index) + /// is allowed to staircase toward this target over multiple slots + /// (per `params.max_price_move_bps_per_slot * dt_slots`). + /// + /// Engine-side rather than wrapper-side: this is the canonical source + /// of truth for per-market oracle target state. Wrappers consume it + /// via `read_price_clamped` (no-mutation form) and + /// `read_price_and_stamp` (strictly-advanced form). + /// Toly carries these on MarketConfig (wrapper-side); fork hosts them + /// on RiskEngine to keep state-shape validation + Kani invariants + /// uniform. + pub oracle_target_price_e6: u64, + /// Publish time of the latest target observation (Pyth/Chainlink + /// `publish_time` field). Used by `read_price_and_stamp` to gate + /// `last_good_oracle_slot` advancement on strictly-advanced timestamps + /// (defeats publish-time replay). + pub oracle_target_publish_time: i64, + /// Last oracle price used in accrue_market_to (P_last, spec §5.5) pub last_oracle_price: u64, /// Last funding-sample price (fund_px_last, spec §5.5 step 11) @@ -1364,6 +1386,10 @@ impl RiskEngine { rr_cursor_position: 0, sweep_generation: 0, price_move_consumed_bps_this_generation: 0, + // Wave 1 / ENG-PORT-C: oracle target init — see init_in_place + // for the matching rationale comment. + oracle_target_price_e6: 0, + oracle_target_publish_time: 0, last_oracle_price: init_oracle_price, fund_px_last: init_oracle_price, last_market_slot: init_slot, @@ -1457,6 +1483,13 @@ impl RiskEngine { self.rr_cursor_position = 0; self.sweep_generation = 0; self.price_move_consumed_bps_this_generation = 0; + // Wave 1 / ENG-PORT-C: oracle target init. At market genesis the + // wrapper's first `read_price_clamped` will populate these from + // the live oracle observation; init to (0, 0) signals "no target + // observed yet" so the strictly-advanced gate accepts the first + // observation unconditionally. + self.oracle_target_price_e6 = 0; + self.oracle_target_publish_time = 0; self.last_oracle_price = init_oracle_price; self.fund_px_last = init_oracle_price; self.last_market_slot = init_slot; @@ -6834,6 +6867,58 @@ impl RiskEngine { Ok(ResolvedCloseResult::Closed(capital)) } + /// Wave 1 / ENG-PORT-B: force-close a resolved account with optional + /// recurring maintenance fee charged at the resolved-slot anchor. + /// + /// Mirrors toly engine src/percolator.rs:9688-9716. Reverses the prior + /// FEATURE-DIVERGENCE decision (see comment in + /// `force_close_resolved_not_atomic` above) where fork deliberately + /// skipped the maintenance-fee charge. With this method, wrappers that + /// run with `maintenance_fee_per_slot > 0` can pay the fee at terminal + /// close — keeping fee accounting consistent with the live-market path + /// (where `sync_account_fee_to_slot_not_atomic` is the canonical sync + /// primitive). + /// + /// Wrappers that don't enable maintenance fees can keep calling + /// `force_close_resolved_not_atomic` (zero-fee path); both paths share + /// the same Phase 1 reconcile + Phase 2 terminal close. The only + /// difference is the `sync_account_fee_to_slot` call between phases. + pub fn force_close_resolved_with_fee_not_atomic( + &mut self, + idx: u16, + fee_rate_per_slot: u128, + ) -> Result { + // Phase 1: always reconcile (persists on success, idempotent). + self.reconcile_resolved_not_atomic(idx)?; + + let i = idx as usize; + + // Finalize any sides that are fully ready for reopening. + self.maybe_finalize_ready_reset_sides(); + if self.accounts[i].position_basis_q != 0 { + return Ok(ResolvedCloseResult::ProgressOnly); + } + // Charge recurring maintenance fees at the resolved-slot anchor + // BEFORE the terminal close so capital seen by the close path is + // post-fee. No-op when fee_rate_per_slot == 0. + self.sync_account_fee_to_slot(i, self.resolved_slot, fee_rate_per_slot)?; + self.assert_public_postconditions()?; + + // pnl <= 0: can close immediately (loser/zero — no payout gate) + // pnl > 0: needs terminal readiness for payout + if self.accounts[i].pnl > 0 && !self.is_terminal_ready() { + // Reconciled but not yet payable. Progress persisted. + return Ok(ResolvedCloseResult::ProgressOnly); + } + + // Phase 2: terminal close. Existing fork helper closes without + // re-charging fees (we already synced above). Wrappers that need + // the fee charge call this method; wrappers that don't can keep + // using `force_close_resolved_not_atomic`. + let capital = self.close_resolved_terminal_not_atomic(idx)?; + Ok(ResolvedCloseResult::Closed(capital)) + } + /// Phase 1: Reconcile a resolved account. Materializes K-pair PnL, /// zeroes position, settles losses, absorbs insurance. Always persists /// on success. Idempotent on already-reconciled accounts. diff --git a/tests/common/mod.rs b/tests/common/mod.rs index 5227c6c37..1cc55c123 100644 --- a/tests/common/mod.rs +++ b/tests/common/mod.rs @@ -125,6 +125,17 @@ pub fn zero_fee_params() -> RiskParams { } } +/// Test helper: shrink the account tier of `zero_fee_params` for Kani proofs +/// that need to model a small market. Mirrors toly's helper of the same name +/// (Wave 1 ENG-PORT-A harness needs `small_zero_fee_params(4)` to bound the +/// state space without changing solvency-envelope calibration). +pub fn small_zero_fee_params(max_accounts: u64) -> RiskParams { + let mut params = zero_fee_params(); + params.max_accounts = max_accounts; + params.max_active_positions_per_side = max_accounts; + params +} + /// Test helper: materialize a user account via deposit_not_atomic (spec §10.2). /// /// v12.18.1 removed add_user / add_lp / materialize_with_fee. The sole diff --git a/tests/proofs_invariants.rs b/tests/proofs_invariants.rs index 79def6c95..16037e67b 100644 --- a/tests/proofs_invariants.rs +++ b/tests/proofs_invariants.rs @@ -766,3 +766,53 @@ fn proof_fee_credits_never_i128_min() { } } } + +// ############################################################################ +// Wave 1 ENG-PORT-C: external-oracle-target schema invariant +// ############################################################################ + +/// Wave 1 / ENG-PORT-C: oracle-target schema invariant. +/// +/// `init_in_place` MUST zero both `oracle_target_price_e6` and +/// `oracle_target_publish_time`. The wrapper's strictly-advanced gate +/// in `read_price_and_stamp` relies on `(0, 0)` representing "no +/// target observed yet" so the first observation is admitted +/// unconditionally. Mis-initializing these fields would either +/// reject the first valid Pyth publish or accept a stale replay. +/// +/// Also asserts that arbitrary writes through the field are +/// observable (the schema addition is well-formed) and that adding +/// these fields doesn't break `check_conservation` — the +/// conservation aggregate only reads value-bearing fields, and +/// oracle-target fields are pure metadata. +#[kani::proof] +#[kani::unwind(34)] +#[kani::solver(cadical)] +fn proof_oracle_target_init_zero_and_persistence() { + let mut engine = + RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE); + + // Init zeros both fields. + assert_eq!(engine.oracle_target_price_e6, 0); + assert_eq!(engine.oracle_target_publish_time, 0); + // Conservation holds at genesis with the new fields present. + assert!(engine.check_conservation()); + + // Symbolic write-back: arbitrary values persist and are observable. + let target_price: u64 = kani::any(); + let target_time: i64 = kani::any(); + kani::assume(target_price <= MAX_ORACLE_PRICE); + + engine.oracle_target_price_e6 = target_price; + engine.oracle_target_publish_time = target_time; + + assert_eq!(engine.oracle_target_price_e6, target_price); + assert_eq!(engine.oracle_target_publish_time, target_time); + // Conservation still holds — oracle-target fields are pure metadata. + assert!(engine.check_conservation()); + + kani::cover!( + target_price > 0 && target_time > 0, + "non-zero target observation persists and conservation is preserved" + ); +} diff --git a/tests/proofs_liveness.rs b/tests/proofs_liveness.rs index 8342787bc..8ccc0a2fd 100644 --- a/tests/proofs_liveness.rs +++ b/tests/proofs_liveness.rs @@ -559,3 +559,69 @@ fn proof_adl_pipeline_trade_liquidate_reopen() { "post-ADL market reopens with balanced OI" ); } + +// ############################################################################ +// Wave 1 ENG-PORT-B: force_close_resolved_with_fee_not_atomic invariant +// ############################################################################ + +/// Wave 1 / ENG-PORT-B: fee-credited-at-resolved-close invariant. +/// +/// `force_close_resolved_with_fee_not_atomic` MUST sync the recurring +/// maintenance fee at the resolved-slot anchor BEFORE returning +/// ProgressOnly when the account is in the not-yet-payable case +/// (`pnl > 0 && !is_terminal_ready`). The fee charge moves capital +/// from the user to the insurance fund and stamps last_fee_slot to +/// resolved_slot — without this, a wrapper that re-calls the function +/// would either re-charge the same dt (double-charge) or skip the +/// charge entirely. +/// +/// Mirrors toly engine tests/proofs_liveness.rs:1825-1869 +/// (`proof_force_close_resolved_with_fee_progress_only_syncs_before_payout_on_prod_code`). +#[kani::proof] +#[kani::unwind(80)] +#[kani::solver(cadical)] +fn proof_force_close_resolved_with_fee_progress_only_syncs_before_payout_on_prod_code() { + let mut engine = + RiskEngine::new_with_market(small_zero_fee_params(4), DEFAULT_SLOT, DEFAULT_ORACLE); + engine.deposit_not_atomic(0, 100, DEFAULT_SLOT).unwrap(); + engine.deposit_not_atomic(1, 100, DEFAULT_SLOT).unwrap(); + engine.market_mode = MarketMode::Resolved; + engine.current_slot = DEFAULT_SLOT; + engine.resolved_slot = DEFAULT_SLOT; + engine.resolved_price = DEFAULT_ORACLE; + engine.resolved_live_price = DEFAULT_ORACLE; + engine.set_pnl(0, 10).unwrap(); + engine.set_pnl(1, -5).unwrap(); + engine.accounts[0].last_fee_slot = DEFAULT_SLOT - 1; + + let fee_rate: u8 = kani::any(); + kani::assume(fee_rate > 0 && fee_rate <= 10); + let capital_before = engine.accounts[0].capital.get(); + let pnl_before = engine.accounts[0].pnl; + let insurance_before = engine.insurance_fund.balance.get(); + + let result = engine.force_close_resolved_with_fee_not_atomic(0, fee_rate as u128); + + assert_eq!(result, Ok(ResolvedCloseResult::ProgressOnly)); + assert!(engine.is_used(0)); + assert_eq!(engine.accounts[0].last_fee_slot, engine.resolved_slot); + assert_eq!(engine.accounts[0].pnl, pnl_before); + assert_eq!( + engine.accounts[0].capital.get(), + capital_before - fee_rate as u128 + ); + assert_eq!( + engine.insurance_fund.balance.get(), + insurance_before + fee_rate as u128 + ); + assert_eq!(engine.neg_pnl_account_count, 1); + assert_eq!(engine.market_mode, MarketMode::Resolved); + assert!(engine.check_conservation()); + kani::cover!( + result == Ok(ResolvedCloseResult::ProgressOnly) + && engine.is_used(0) + && engine.accounts[0].last_fee_slot == engine.resolved_slot + && engine.insurance_fund.balance.get() > insurance_before, + "fee-aware resolved close syncs fee before ProgressOnly without payout/free" + ); +} diff --git a/tests/proofs_safety.rs b/tests/proofs_safety.rs index 5653b445f..19eecc070 100644 --- a/tests/proofs_safety.rs +++ b/tests/proofs_safety.rs @@ -3007,6 +3007,72 @@ fn proof_close_account_fee_forgiveness_bounded() { assert!(engine.check_conservation()); } +// ############################################################################ +// Wave 1 ENG-PORT-A: withdraw_resolved_insurance_not_atomic invariants +// ############################################################################ + +/// Wave 1 / ENG-PORT-A: empty-market-after-resolve invariant. +/// +/// `withdraw_resolved_insurance_not_atomic` MUST: +/// - reject if any account remains used (positions / capital still live) +/// - on empty market: drain only the insurance fund, leave c_tot == 0, +/// and never decrement vault by more than insurance_before +/// - preserve MarketMode::Resolved post-call +/// - preserve check_conservation +/// +/// Harness mirrors toly-engine `proof_resolved_insurance_withdraw_requires_empty_market_and_drains_only_insurance_on_prod_code` +/// (toly tests/proofs_safety.rs:362-410), now reachable in fork because +/// `withdraw_resolved_insurance_not_atomic` is byte-equivalent to toly's. +#[kani::proof] +#[kani::unwind(96)] +#[kani::solver(cadical)] +fn proof_resolved_insurance_withdraw_requires_empty_market_and_drains_only_insurance_on_prod_code( +) { + let mut engine = + RiskEngine::new_with_market(small_zero_fee_params(4), DEFAULT_SLOT, DEFAULT_ORACLE); + let nonempty: bool = kani::any(); + if nonempty { + engine.deposit_not_atomic(0, 10, DEFAULT_SLOT).unwrap(); + } + engine.top_up_insurance_fund(50, DEFAULT_SLOT).unwrap(); + engine.market_mode = MarketMode::Resolved; + engine.current_slot = DEFAULT_SLOT; + engine.resolved_slot = DEFAULT_SLOT; + engine.resolved_price = DEFAULT_ORACLE; + engine.resolved_live_price = DEFAULT_ORACLE; + + let vault_before = engine.vault.get(); + let capital_before = engine.c_tot.get(); + let insurance_before = engine.insurance_fund.balance.get(); + let used_before = engine.num_used_accounts; + + let result = engine.withdraw_resolved_insurance_not_atomic(); + + if nonempty { + assert_eq!(result, Err(RiskError::Unauthorized)); + assert_eq!(engine.vault.get(), vault_before); + assert_eq!(engine.c_tot.get(), capital_before); + assert_eq!(engine.insurance_fund.balance.get(), insurance_before); + assert_eq!(engine.num_used_accounts, used_before); + } else { + assert_eq!(result, Ok(insurance_before)); + assert_eq!(engine.vault.get(), vault_before - insurance_before); + assert_eq!(engine.c_tot.get(), 0); + assert_eq!(engine.insurance_fund.balance.get(), 0); + assert_eq!(engine.num_used_accounts, 0); + } + assert_eq!(engine.market_mode, MarketMode::Resolved); + assert!(engine.check_conservation()); + kani::cover!( + nonempty && result == Err(RiskError::Unauthorized), + "resolved insurance withdrawal rejects while any account remains" + ); + kani::cover!( + !nonempty && result == Ok(insurance_before) && engine.vault.get() == 0, + "resolved insurance withdrawal drains only terminal insurance after market is empty" + ); +} + // ############################################################################ // Gap #11 (Weakness): Symbolic trade size for conservation // ############################################################################