sync(engine): Wave 1 — port deferred items (ENG-PORT-A/B/C) for full wrapper sync

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<ResolvedCloseResult> {
+        // 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.

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

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"
+    );
+}

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"
+    );
+}

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
 // ############################################################################