From b731cffa20f4e8722be5f4c8a968219bc14d8ec0 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 18:19:08 +0100 Subject: [PATCH 1/4] =?UTF-8?q?sync(engine):=20add=20ENG-PORT-A=20Kani=20h?= =?UTF-8?q?arness=20=E2=80=94=20empty-market-after-resolve=20invariant?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a Kani proof for `withdraw_resolved_insurance_not_atomic`'s empty-market-after-resolve invariant. The method itself is already present in fork engine (line 7289) byte-equivalent to toly upstream (line 10296); this harness pulls in the matching toly invariant proof that has been missing since the method was originally landed. The harness asserts: - rejects with `RiskError::Unauthorized` when any account is still used - on empty market: drains only insurance into vault payout (vault decreases by exactly insurance_before) leaves c_tot == 0, insurance_fund == 0, num_used_accounts == 0 - preserves MarketMode::Resolved across the call - preserves check_conservation invariant Mirrors toly tests/proofs_safety.rs:362-410 (`proof_resolved_insurance_withdraw_requires_empty_market_and_drains_only_insurance_on_prod_code`). Test helper added to tests/common/mod.rs: - `small_zero_fee_params(max_accounts: u64)` — shrinks the account tier on top of `zero_fee_params` so Kani can bound the state space without changing the solvency-envelope calibration. Mirrors toly's helper of the same name. Verification: - cargo build --release: clean (26 dead-code warnings pre-existing) - cargo test --features test --lib --tests: 52/0/0 (unchanged) - tests/proofs_*.rs Kani count: 306 (was 305; +1 new harness) - scripts/verify-engine-preservation.sh: silent / OK - scripts/verify-engine-deferred-absent.sh: silent / OK - scripts/verify-eng-port-preservation.sh: silent / OK This is part of the Wave 1 epic (engine deferred ports). ENG-PORT-A is closed; remaining: ENG-PORT-B (force_close_resolved_with_fee_not_atomic) and ENG-PORT-C (external-oracle-target subsystem with schema change). --- tests/common/mod.rs | 11 +++++++ tests/proofs_safety.rs | 66 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+) 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_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 // ############################################################################ From d0f2779438a19470f490b803e0dfc3802a94c133 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 18:22:36 +0100 Subject: [PATCH 2/4] =?UTF-8?q?sync(engine):=20port=20force=5Fclose=5Freso?= =?UTF-8?q?lved=5Fwith=5Ffee=5Fnot=5Fatomic=20=E2=80=94=20closes=20ENG-POR?= =?UTF-8?q?T-B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the fee-aware variant of force-close at the resolved-mode terminal path. Mirrors toly engine src/percolator.rs:9688-9716; previously fork deliberately skipped the maintenance-fee charge here as a FEATURE-DIVERGENCE (see comment block above `force_close_resolved_not_atomic` at fork:6814-6818). With this method, wrappers that run with `maintenance_fee_per_slot > 0` can charge the recurring fee at the frozen resolved-slot anchor — keeping fee accounting consistent with the live-market path. Implementation: Phase 1: `reconcile_resolved_not_atomic(idx)` — same as no-fee variant (idempotent on already-reconciled accounts). Phase 2: `maybe_finalize_ready_reset_sides()` — same. Phase 2b: `position_basis_q != 0 → ProgressOnly` — same. NEW: `sync_account_fee_to_slot(i, resolved_slot, fee_rate_per_slot)` — charges recurring fees BEFORE the terminal-close decision so capital seen by the close path is post-fee. No-op when fee_rate_per_slot == 0. Phase 3: `pnl > 0 && !is_terminal_ready → ProgressOnly` — same. Phase 4: `close_resolved_terminal_not_atomic` — existing fork helper (no fee re-charge; we already synced above). Wrappers that don't enable maintenance fees can keep calling `force_close_resolved_not_atomic` (zero-fee path); both share the same Phase 1/2/2b/3/4 sequence — only the new sync_account_fee_to_slot call between Phase 2b and Phase 3 differs. Kani harness added (tests/proofs_liveness.rs): `proof_force_close_resolved_with_fee_progress_only_syncs_before_payout_on_prod_code` Mirrors toly tests/proofs_liveness.rs:1825-1869. Asserts: - on `pnl > 0 && !is_terminal_ready` path: returns ProgressOnly, account remains used, last_fee_slot == resolved_slot, pnl unchanged, capital decreased by fee_rate, insurance increased by fee_rate, neg_pnl_account_count == 1, market_mode == Resolved, check_conservation holds. Verification: - cargo build --release: clean (26 dead-code warnings pre-existing) - cargo test --features test --lib --tests: 52/0/0 (unchanged) - tests/proofs_*.rs Kani count: 307 (was 305; +2 new harnesses for ENG-PORT-A and ENG-PORT-B) - scripts/verify-engine-preservation.sh: silent / OK - scripts/verify-engine-deferred-absent.sh: silent / OK - scripts/verify-eng-port-preservation.sh: silent / OK Unblocks wrapper PORT-19 (Tag 21+30 wrappers can now thread config.maintenance_fee_per_slot through to this engine method). --- src/percolator.rs | 52 +++++++++++++++++++++++++++++++ tests/proofs_liveness.rs | 66 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 118 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index 82558b6bc..2c752cadb 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -6834,6 +6834,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/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" + ); +} From c9c707020a09eb812f2a064f4bc4d68d989d7093 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 18:27:04 +0100 Subject: [PATCH 3/4] =?UTF-8?q?sync(engine):=20port=20external-oracle-targ?= =?UTF-8?q?et=20subsystem=20(KL=20revoked)=20=E2=80=94=20closes=20ENG-PORT?= =?UTF-8?q?-C?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ⚠️ SCHEMA CHANGE: adds two RiskEngine fields. Breaks NFT `EXPECTED_RISK_ENGINE_SIZE` compile-time assertion → fixed in Wave 2 (coordinated NFT vendored bytes update before this engine PR merges into mainnet). New RiskEngine fields: - `oracle_target_price_e6: u64` — latest target observation seen via the wrapper's `read_price_clamped` path. Effective price (mark / index) staircases toward this target across slots, bounded by `params.max_price_move_bps_per_slot * dt_slots`. - `oracle_target_publish_time: i64` — publish_time of the latest target observation (Pyth/Chainlink). Used by the wrapper's `read_price_and_stamp` to gate `last_good_oracle_slot` advancement on strictly-advanced timestamps (defeats publish-time replay). Initialization in `init_in_place`: - Both fields zero at market genesis. The wrapper's strictly-advanced gate treats `(0, 0)` as "no target observed yet" so the first Pyth publish post-genesis is admitted unconditionally. Architectural note (engine vs wrapper placement): Toly carries these on MarketConfig (wrapper-side) per `toly/src/percolator.rs:740-741`. Fork hosts them on RiskEngine (engine-side) per the FULL_SYNC_PLAN.md decision. Rationale: - Engine becomes the canonical source of truth for per-market oracle target state. - State-shape validation + Kani invariants run uniformly. - The NFT vendored bytes match exactly (single struct mirror). - Future wrappers (or the SDK's anchor-targeted struct) consume a single field-set instead of a wrapper-specific layout. Kani harness added (tests/proofs_invariants.rs): `proof_oracle_target_init_zero_and_persistence` — symbolic harness that proves init zeroes both fields, arbitrary writes are observable, and `check_conservation` is preserved (oracle-target fields are pure metadata, they don't enter the conservation aggregate). KEEP_LIST evolution (companion commit follows): Revoke the oracle-target portion of KL-FORK-ENGINE-FIELDS — this schema-state is no longer "fork rejects toly's port"; it's "fork carries it engine-side". Verification: - cargo build --release: clean (26 dead-code warnings pre-existing). - tests/proofs_*.rs Kani count: 308 (was 305; +3 new harnesses for Wave 1 ports A, B, C — meets the FULL_SYNC_PLAN target). - scripts/verify-engine-preservation.sh: silent / OK. - scripts/verify-engine-deferred-absent.sh: silent / OK (oracle_target items were never engine-side in fork's prior deferred list — only on wrapper MarketConfig — so the engine deferred-absent script needs no edits for this wave; the wrapper-side script remains unchanged because PORT-10/11/13 add the wrapper-side fields in Wave 3). - scripts/verify-eng-port-preservation.sh: silent / OK. Unblocks wrapper PORT-10/11/13 in Wave 3. Cross-program impact (Phase 4 SDK + Wave 2 NFT): - NFT (~/percolator-nft): EXPECTED_RISK_ENGINE_SIZE constant must be recomputed; slab_types.rs RiskEngine mirror must add the two new fields in matching positions. Coordinated as Wave 2. - SDK: any anchor-targeted RiskEngine struct binding must mirror the new fields. Phase 4 SDK update. - On-chain markets: the new struct is 16 bytes wider than before. Existing slabs allocated with the old layout cannot be read by the new engine — wraps as a breaking schema migration. Operators deploying to existing mainnet markets MUST run a migration window or retire-and-redeploy before the engine PR ships to mainnet. --- src/percolator.rs | 29 ++++++++++++++++++++++ tests/proofs_invariants.rs | 50 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index 2c752cadb..4e591daf5 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) @@ -1457,6 +1479,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; 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" + ); +} From 49b89824282c265c71126667a453e9989e56a5cb Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 18:29:26 +0100 Subject: [PATCH 4/4] fix(engine): add oracle_target_* to test-only new_with_market constructor MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Schema follow-up to ENG-PORT-C (commit c9c7070). The `#[cfg(any(feature = "test", kani))]` constructor `new_with_market` constructs `RiskEngine` via struct literal — the schema change in the previous commit added `oracle_target_price_e6` and `oracle_target_publish_time` but did not update this literal, breaking `cargo test --features test` compilation. Fix: add both fields to the literal, initialised to 0 (matching the init_in_place behavior for the same fields). Verification: - cargo build --release: clean. - cargo test --features test --lib --tests: 52/0/0 (49 lib + 3 integration; matches Phase 0 baseline). - tests/proofs_*.rs Kani count: 308 (unchanged). - All three engine verify scripts: silent / OK. --- src/percolator.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index 4e591daf5..239a2b0f6 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -1386,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,