Wave 12-M: fix 22 engine Kani drift failures (unwind bump)

tests/proofs_instructions.rs

@@ -2628,3 +2628,56 @@ fn v19_accrue_market_envelope_enforces_goal52_bound() {
     assert_eq!(engine.last_oracle_price, p_last as u64);
     assert_eq!(engine.last_market_slot, 0);
 }
+
+// ############################################################################
+// Wave 12-M — dynamic trade-fee cap harness (toly upstream port)
+// ############################################################################
+
+/// Trade-fee bps exceeding `max_trading_fee_bps` must reject pre-mutation
+/// (atomic), leaving vault, c_tot, insurance, both capital balances, and
+/// both position basis_q unchanged.
+#[kani::proof]
+#[kani::unwind(12)]
+#[kani::solver(cadical)]
+fn proof_dynamic_trade_fee_above_cap_rejects_before_mutation() {
+    let mut params = zero_fee_params();
+    params.max_trading_fee_bps = 10;
+    let mut engine = RiskEngine::new_with_market(params, DEFAULT_SLOT, DEFAULT_ORACLE);
+    let a = add_user_test(&mut engine, 0).unwrap();
+    let b = add_user_test(&mut engine, 0).unwrap();
+    engine.deposit_not_atomic(a, 100_000, DEFAULT_SLOT).unwrap();
+    engine.deposit_not_atomic(b, 100_000, DEFAULT_SLOT).unwrap();
+
+    let vault_before = engine.vault.get();
+    let c_tot_before = engine.c_tot.get();
+    let insurance_before = engine.insurance_fund.balance.get();
+    let a_cap_before = engine.accounts[a as usize].capital.get();
+    let b_cap_before = engine.accounts[b as usize].capital.get();
+
+    let trade_result = engine.execute_trade_not_atomic(
+        a,
+        b,
+        DEFAULT_ORACLE,
+        DEFAULT_SLOT,
+        POS_SCALE as i128,
+        DEFAULT_ORACLE,
+        0i128,
+        11,
+        0,
+        100,
+        None,
+    );
+
+    assert_eq!(trade_result, Err(RiskError::Overflow));
+    assert_eq!(engine.vault.get(), vault_before);
+    assert_eq!(engine.c_tot.get(), c_tot_before);
+    assert_eq!(engine.insurance_fund.balance.get(), insurance_before);
+    assert_eq!(engine.accounts[a as usize].capital.get(), a_cap_before);
+    assert_eq!(engine.accounts[b as usize].capital.get(), b_cap_before);
+    assert_eq!(engine.accounts[a as usize].position_basis_q, 0);
+    assert_eq!(engine.accounts[b as usize].position_basis_q, 0);
+    kani::cover!(
+        engine.is_used(a as usize) && engine.is_used(b as usize),
+        "fee cap rejection is checked on real materialized trade parties"
+    );
+}

tests/proofs_invariants.rs

@@ -738,7 +738,7 @@ fn proof_attach_effective_position_updates_side_counts() {
 /// The settle_maintenance_fee path uses checked_sub which can produce i128::MIN,
 /// but fee_debt_u128_checked uses unsigned_abs() which safely returns 2^127.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_fee_credits_never_i128_min() {
     // Part 1: fee_debt_u128_checked is safe for ALL i128 values
@@ -1103,7 +1103,7 @@ fn proof_bankrupt_close_state_machine_schema() {
 /// so the gate trivially passes; when B-tracking lands, this harness will
 /// detect any setter that violates the lower-bound ≤ upper-bound contract.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_phantom_dust_certified_le_potential_at_genesis() {
     let engine = RiskEngine::new(zero_fee_params());
@@ -1123,7 +1123,7 @@ fn proof_phantom_dust_certified_le_potential_at_genesis() {
 /// `certified` from liquidation step 7, this guards against off-by-one or
 /// step-ordering bugs.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_phantom_dust_certified_gt_potential_rejects() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1159,7 +1159,7 @@ fn proof_phantom_dust_certified_gt_potential_rejects() {
 /// init-time predicate so future Wave 11a-ii writers can't silently
 /// regress the genesis state.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_b_tracking_shape_holds_at_genesis() {
     let engine = RiskEngine::new(zero_fee_params());
@@ -1183,7 +1183,7 @@ fn proof_b_tracking_shape_holds_at_genesis() {
 /// starts incrementing loss_weight_sum, this catches off-by-one and
 /// overflow-style regressions.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_b_tracking_loss_weight_sum_overflow_rejects() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1215,7 +1215,7 @@ fn proof_b_tracking_loss_weight_sum_overflow_rejects() {
 /// `set_social_remainder(side, plan.rem_new)`, this catches a wrap or
 /// off-by-one that would push the numerator into invalid range.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_b_tracking_shape_rejects_social_remainder_at_or_above_denominator() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1239,7 +1239,7 @@ fn proof_b_tracking_shape_rejects_social_remainder_at_or_above_denominator() {
 /// `transfer_scaled_dust_side` that fails to flush the post-mod dust
 /// correctly.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_b_tracking_shape_rejects_social_dust_at_or_above_denominator() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1264,7 +1264,7 @@ fn proof_b_tracking_shape_rejects_social_dust_at_or_above_denominator() {
 /// `checked_add` overflow; this harness catches any future writer that
 /// might store an out-of-range value.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_b_tracking_shape_rejects_saturated_flag_out_of_range() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1286,7 +1286,7 @@ fn proof_b_tracking_shape_rejects_saturated_flag_out_of_range() {
 /// the encoded byte; `continue_active_bankrupt_close_core` reads it back)
 /// depend on for end-to-end correctness.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_encode_decode_active_close_side_roundtrip() {
     let pick_long: bool = kani::any();
@@ -1308,7 +1308,7 @@ fn proof_encode_decode_active_close_side_roundtrip() {
 /// shows `active_close_present = 1` but `opp_side` is `0` (NONE) or any
 /// other byte, the decoder MUST surface `CorruptState`.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_decode_active_close_side_rejects_invalid_byte() {
     let byte: u8 = kani::any();
@@ -1327,7 +1327,7 @@ fn proof_decode_active_close_side_rejects_invalid_byte() {
 /// in the recovery terminal — both paths rely on the clear being
 /// total.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_clear_active_bankrupt_close_state_zeros_all_fields() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1370,7 +1370,7 @@ fn proof_clear_active_bankrupt_close_state_zeros_all_fields() {
 /// extension adds a third mode, the dispatcher must not silently take any
 /// of the two branches it understands.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_permissionless_progress_resolved_routes_to_resolved_close() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1418,7 +1418,7 @@ fn proof_permissionless_progress_resolved_routes_to_resolved_close() {
 /// instead of taking either of the two live-mode branches the
 /// dispatcher knows.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_permissionless_progress_rejects_when_active_close_present() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1454,7 +1454,7 @@ fn proof_permissionless_progress_rejects_when_active_close_present() {
 /// market — Live markets must take the keeper-crank path, not the
 /// cursor-scan path.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_force_close_resolved_cursor_rejects_live_market() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1470,7 +1470,7 @@ fn proof_force_close_resolved_cursor_rejects_live_market() {
 /// limit — silently treating it as a no-op would mean the wrapper's
 /// liveness contract has no guarantee the cursor advanced.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_force_close_resolved_cursor_rejects_zero_scan_limit() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1491,7 +1491,7 @@ fn proof_force_close_resolved_cursor_rejects_zero_scan_limit() {
 /// Genesis state has every B-tracking and bankrupt-close field at the
 /// no-continuation default, so the aggregator must accept.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_validate_engine_state_shape_holds_at_genesis() {
     let engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1504,7 +1504,7 @@ fn proof_validate_engine_state_shape_holds_at_genesis() {
 /// `validate_b_tracking_shape` call from inside the aggregator, Kani
 /// catches it.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_validate_engine_state_shape_delegates_to_b_tracking() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1520,7 +1520,7 @@ fn proof_validate_engine_state_shape_delegates_to_b_tracking() {
 /// state-machine validator would reject (e.g., active_close_present > 1).
 /// Pins the second delegation arm of the aggregator.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_validate_engine_state_shape_delegates_to_bankrupt_close() {
     let mut engine = RiskEngine::new(zero_fee_params());
@@ -1544,7 +1544,7 @@ fn proof_validate_engine_state_shape_delegates_to_bankrupt_close() {
 /// neither Live nor Resolved with `Unauthorized` — the dispatcher must
 /// not silently advance an unknown-mode market.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_permissionless_progress_rejects_non_live_non_resolved() {
     let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1587,7 +1587,7 @@ fn proof_permissionless_progress_rejects_non_live_non_resolved() {
 /// or `b_short_num` has saturated at `u128::MAX`. Pins the headroom-
 /// detection contract.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_recovery_reason_b_index_headroom_exhausted_requires_saturation() {
     let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1617,7 +1617,7 @@ fn proof_recovery_reason_b_index_headroom_exhausted_requires_saturation() {
 /// `sweep_generation`, `adl_epoch_long`, or `adl_epoch_short` is at
 /// `u64::MAX`.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_recovery_reason_counter_or_epoch_overflow_requires_saturation() {
     let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1647,7 +1647,7 @@ fn proof_recovery_reason_counter_or_epoch_overflow_requires_saturation() {
 /// `ExplicitLossOrDustAuditOverflow` branch is authorised iff
 /// `explicit_unallocated_loss_saturated != 0`.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_recovery_reason_explicit_loss_overflow_requires_saturation_flag() {
     let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1672,7 +1672,7 @@ fn proof_recovery_reason_explicit_loss_overflow_requires_saturation_flag() {
 /// `Unauthorized` — that reason is account-scoped and only the
 /// per-account validator may authorise it.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_recovery_reason_account_b_settlement_is_global_unauthorized() {
     let engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1693,7 +1693,7 @@ fn proof_recovery_reason_account_b_settlement_is_global_unauthorized() {
 /// and it must opt in by deciding to call the resolver directly. The
 /// permissionless dispatcher refuses to take the branch unilaterally.
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_recovery_reason_oracle_policy_unavailable_is_wrapper_only() {
     let engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
@@ -1712,7 +1712,7 @@ fn proof_recovery_reason_oracle_policy_unavailable_is_wrapper_only() {
 /// when the market is not Live (already-Resolved markets must route
 /// through the resolved-close branch instead).
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(cadical)]
 fn proof_recovery_reason_validators_reject_non_live_market() {
     let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);

tests/proofs_v1131.rs

@@ -1220,3 +1220,63 @@ fn proof_deposit_nonflat_no_sweep_no_resolve() {
     );
     assert!(engine.check_conservation());
 }
+
+// ############################################################################
+// Wave 12-M — keeper-crank funding-rate boundary harnesses (toly upstream port)
+// ############################################################################
+
+/// keeper_crank_not_atomic accepts the configured positive funding-rate
+/// boundary at the production crank boundary.
+#[kani::proof]
+#[kani::unwind(8)]
+#[kani::solver(cadical)]
+fn proof_keeper_crank_accepts_positive_boundary_funding_rate_on_prod_code() {
+    let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
+    let supplied_rate = engine.params.max_abs_funding_e9_per_slot as i128;
+
+    let result = engine.keeper_crank_not_atomic(
+        DEFAULT_SLOT + 1,
+        DEFAULT_ORACLE,
+        &[],
+        0,
+        supplied_rate,
+        0,
+        100,
+        None,
+        0,
+    );
+    assert!(result.is_ok());
+    assert_eq!(engine.last_market_slot, DEFAULT_SLOT + 1);
+    kani::cover!(
+        result.is_ok() && engine.last_market_slot == DEFAULT_SLOT + 1,
+        "keeper accepts positive configured funding-rate boundary"
+    );
+}
+
+/// keeper_crank_not_atomic accepts the configured negative funding-rate
+/// boundary at the production crank boundary.
+#[kani::proof]
+#[kani::unwind(8)]
+#[kani::solver(cadical)]
+fn proof_keeper_crank_accepts_negative_boundary_funding_rate_on_prod_code() {
+    let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE);
+    let supplied_rate = -(engine.params.max_abs_funding_e9_per_slot as i128);
+
+    let result = engine.keeper_crank_not_atomic(
+        DEFAULT_SLOT + 1,
+        DEFAULT_ORACLE,
+        &[],
+        0,
+        supplied_rate,
+        0,
+        100,
+        None,
+        0,
+    );
+    assert!(result.is_ok());
+    assert_eq!(engine.last_market_slot, DEFAULT_SLOT + 1);
+    kani::cover!(
+        result.is_ok() && engine.last_market_slot == DEFAULT_SLOT + 1,
+        "keeper accepts negative configured funding-rate boundary"
+    );
+}