sync(engine): Wave 1 — port deferred items (ENG-PORT-A/B/C) for full wrapper sync - #91
Merged
Merged
Conversation
…e invariant
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).
…ENG-PORT-B
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).
…oses ENG-PORT-C⚠️ 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.
…ctor 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.
📝 WalkthroughWalkthroughThis PR extends ChangesWave 1 Oracle Target & Resolved-Market Fee Closure
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (1)
src/percolator.rs (1)
6886-6919: ⚡ Quick winDeduplicate the two resolved-close entrypoints.
This method is now almost a copy of
force_close_resolved_not_atomic, with only the fee-sync hook differing. Keeping both flows handwritten makes the next fix to reconcile/readiness/close ordering easy to miss in one path.♻️ Possible extraction
+ fn force_close_resolved_internal( + &mut self, + idx: u16, + fee_rate_per_slot: Option<u128>, + ) -> Result<ResolvedCloseResult> { + self.reconcile_resolved_not_atomic(idx)?; + let i = idx as usize; + + self.maybe_finalize_ready_reset_sides(); + if self.accounts[i].position_basis_q != 0 { + return Ok(ResolvedCloseResult::ProgressOnly); + } + + if let Some(rate) = fee_rate_per_slot { + self.sync_account_fee_to_slot(i, self.resolved_slot, rate)?; + } + self.assert_public_postconditions()?; + + if self.accounts[i].pnl > 0 && !self.is_terminal_ready() { + return Ok(ResolvedCloseResult::ProgressOnly); + } + + let capital = self.close_resolved_terminal_not_atomic(idx)?; + Ok(ResolvedCloseResult::Closed(capital)) + } + pub fn force_close_resolved_not_atomic(&mut self, idx: u16) -> Result<ResolvedCloseResult> { - // existing body + self.force_close_resolved_internal(idx, None) } pub fn force_close_resolved_with_fee_not_atomic( &mut self, idx: u16, fee_rate_per_slot: u128, ) -> Result<ResolvedCloseResult> { - // existing body + self.force_close_resolved_internal(idx, Some(fee_rate_per_slot)) }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/percolator.rs` around lines 6886 - 6919, The two entrypoints force_close_resolved_with_fee_not_atomic and force_close_resolved_not_atomic are nearly identical except for the fee-sync step; extract their shared logic into a single helper (e.g., close_resolved_common or perform_force_close_resolved) that takes either an Option<fee_rate_per_slot> or a closure/hook to perform the fee sync (or no-op) before the terminal close, then have both public functions delegate to that helper (calling sync_account_fee_to_slot when fee_rate_per_slot is provided, otherwise skipping it) and reuse reconcile_resolved_not_atomic, maybe_finalize_ready_reset_sides, the pnl/terminal readiness check, and close_resolved_terminal_not_atomic to avoid duplication and keep behavior identical.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/percolator.rs`:
- Around line 658-678: The two new fields oracle_target_price_e6: u64 and
oracle_target_publish_time: i64 were inserted mid-struct which shifts offsets
for a #[repr(C)] RiskEngine; move both field declarations (and their doc
comments) to the very end of the RiskEngine struct so they become a suffix
extension and do not change existing field offsets, then run tests/serialization
checks to ensure no other code relies on the previous layout.
In `@tests/common/mod.rs`:
- Around line 132-136: small_zero_fee_params currently allows max_accounts >
MAX_ACCOUNTS which can create invalid test parameters; update the function
(small_zero_fee_params) to enforce an upper bound by clamping or capping the
input against MAX_ACCOUNTS before assigning into the RiskParams returned by
zero_fee_params (e.g., compute let capped = std::cmp::min(max_accounts,
MAX_ACCOUNTS) and use capped for params.max_accounts and
params.max_active_positions_per_side) so the produced RiskParams always respect
engine allocation limits.
---
Nitpick comments:
In `@src/percolator.rs`:
- Around line 6886-6919: The two entrypoints
force_close_resolved_with_fee_not_atomic and force_close_resolved_not_atomic are
nearly identical except for the fee-sync step; extract their shared logic into a
single helper (e.g., close_resolved_common or perform_force_close_resolved) that
takes either an Option<fee_rate_per_slot> or a closure/hook to perform the fee
sync (or no-op) before the terminal close, then have both public functions
delegate to that helper (calling sync_account_fee_to_slot when fee_rate_per_slot
is provided, otherwise skipping it) and reuse reconcile_resolved_not_atomic,
maybe_finalize_ready_reset_sides, the pnl/terminal readiness check, and
close_resolved_terminal_not_atomic to avoid duplication and keep behavior
identical.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: eb4f18c2-16ea-4afc-98ec-3e56d584e6cd
📒 Files selected for processing (5)
src/percolator.rstests/common/mod.rstests/proofs_invariants.rstests/proofs_liveness.rstests/proofs_safety.rs
Comment on lines
+658
to
+678
| /// 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, |
There was a problem hiding this comment.
🛠️ Refactor suggestion | 🟠 Major | ⚡ Quick win
Append new #[repr(C)] fields at the end of RiskEngine.
Because RiskEngine is layout-sensitive, inserting oracle_target_price_e6 and oracle_target_publish_time here shifts the offset of every trailing persisted field. That makes the schema blast radius much larger than necessary for wrappers and mirror structs. Moving these two fields to the tail would keep this as a suffix extension instead of a full offset migration.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/percolator.rs` around lines 658 - 678, The two new fields
oracle_target_price_e6: u64 and oracle_target_publish_time: i64 were inserted
mid-struct which shifts offsets for a #[repr(C)] RiskEngine; move both field
declarations (and their doc comments) to the very end of the RiskEngine struct
so they become a suffix extension and do not change existing field offsets, then
run tests/serialization checks to ensure no other code relies on the previous
layout.
Comment on lines
+132
to
+136
| 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 |
There was a problem hiding this comment.
Enforce max_accounts upper bound to keep test params structurally valid.
small_zero_fee_params is meant to shrink capacity, but it currently accepts values above MAX_ACCOUNTS, which can produce parameter sets that don’t match engine allocation limits.
Suggested fix
pub fn small_zero_fee_params(max_accounts: u64) -> RiskParams {
+ assert!(
+ (max_accounts as usize) <= MAX_ACCOUNTS,
+ "small_zero_fee_params expects max_accounts <= MAX_ACCOUNTS"
+ );
let mut params = zero_fee_params();
params.max_accounts = max_accounts;
params.max_active_positions_per_side = max_accounts;
params
}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| 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 | |
| pub fn small_zero_fee_params(max_accounts: u64) -> RiskParams { | |
| assert!( | |
| (max_accounts as usize) <= MAX_ACCOUNTS, | |
| "small_zero_fee_params expects max_accounts <= MAX_ACCOUNTS" | |
| ); | |
| let mut params = zero_fee_params(); | |
| params.max_accounts = max_accounts; | |
| params.max_active_positions_per_side = max_accounts; | |
| params | |
| } |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@tests/common/mod.rs` around lines 132 - 136, small_zero_fee_params currently
allows max_accounts > MAX_ACCOUNTS which can create invalid test parameters;
update the function (small_zero_fee_params) to enforce an upper bound by
clamping or capping the input against MAX_ACCOUNTS before assigning into the
RiskParams returned by zero_fee_params (e.g., compute let capped =
std::cmp::min(max_accounts, MAX_ACCOUNTS) and use capped for params.max_accounts
and params.max_active_positions_per_side) so the produced RiskParams always
respect engine allocation limits.
5 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Status: Ready for review
Wave 1 of the 8-wave full-sync execution. Engine epic A: 3 deferred audit ports + supporting Kani harnesses + KEEP_LIST evolution. Unblocks wrapper Wave 3 (PORT-10/11/13, PORT-18, PORT-19) and triggers Wave 2 (NFT vendored bytes update).
What's closed
withdraw_resolved_insurance_not_atomicKani harness — empty-market-after-resolve invariant. The method itself was already byte-equivalent to toly (line 7289); this commit ports the matching invariant proof.b731cffforce_close_resolved_with_fee_not_atomic— fee-aware variant of resolved-mode terminal close. Reverses the prior FEATURE-DIVERGENCE that skipped fee charge at resolved close. + Kani harness for fee-credited-at-resolved-close invariant.d0f2779oracle_target_price_e6: u64+oracle_target_publish_time: i64toRiskEngine, initializes them ininit_in_place. + Kani harness for schema invariants. SCHEMA CHANGE (16-byte struct widening).c9c7070new_with_marketstruct literal socargo test --features testcompiles.49b8982ENG-PORT-C widens
RiskEngineby 16 bytes (oneu64+ onei64). This breaks the NFT package's compile-timeEXPECTED_RISK_ENGINE_SIZEassertion in~/percolator-nft/src/slab_types.rs. Wave 2 (feat/sync/nft-engine-bytes-wave1in~/percolator-nft) updates the mirror struct + size constant. Wave 2 must merge before this engine PR ships to mainnet to avoid breaking the NFT program's slab-layout invariants.Existing on-chain markets allocate slabs sized to the OLD
RiskEnginelayout. The new engine cannot read them. Operators deploying to existing mainnet markets MUST run a migration window (force-resolve + redeploy) before this PR ships. Tracked as a coordinated rollout item; this PR itself is mergeable.Architectural note (engine vs wrapper placement of oracle_target_*)
Toly carries
oracle_target_price_e6+oracle_target_publish_timeonMarketConfig(wrapper-side,toly/src/percolator.rs:740-741). Fork hosts them onRiskEngine(engine-side) per FULL_SYNC_PLAN.md. Rationale:Functional behavior is equivalent: same observation, same staircase semantics, same strictly-advanced gate.
KEEP_LIST evolution
~/wrapper-engine-deep-audit/KEEP_LIST.mdupdated:RiskEnginefields are unaffected.scripts/verify-engine-deferred-absent.shdid not reference oracle_target items (those were tracked on the wrapper side viaverify-wrapper-preservation.sh); no script edit needed for this wave.Verification
cargo build --releasecargo test --features test --lib --testsscripts/verify-engine-preservation.shscripts/verify-engine-deferred-absent.shscripts/verify-eng-port-preservation.shCommits (4)
b731cffsync(engine): add ENG-PORT-A Kani harness — empty-market-after-resolve invariantd0f2779sync(engine): port force_close_resolved_with_fee_not_atomic — closes ENG-PORT-Bc9c7070sync(engine): port external-oracle-target subsystem (KL revoked) — closes ENG-PORT-C49b8982fix(engine): add oracle_target_* to test-only new_with_market constructorCross-program coordination
~/percolator-nftadds the two fields toslab_types.rsand bumpsEXPECTED_RISK_ENGINE_SIZE. Triggered immediately on this PR's merge.~/percolator-progports PORT-10/11/13 (oracle helpers), PORT-18 (Tag 20 surplus-sweep, uses ENG-PORT-A), PORT-19 (Tag 21+30 force-close, uses ENG-PORT-B), plus the wrapper-side oracle-target field accesses.Out of scope (later waves)
Per Wave 1 spec, ready-for-review immediately. Holding for user merge signal before starting Wave 2.
Summary by CodeRabbit
New Features
Tests