fix(kani): Fix kani.rs compilation — 3 bitrotted references (PERC-238)

[dcccrypto]

Summary

Fixes 3 compilation errors that made all 152 kani harnesses non-functional:

Error 1: No field funding_rate_bps_per_slot on RiskEngine

• Line 7661: engine.funding_rate_bps_per_slot = funding_rate;
• Fix: Renamed to funding_rate_bps_per_slot_last to match current struct

Error 2: Method takes 5 args but 3 supplied

• Line 7666: engine.keeper_crank(now_slot, 1_000_000, false)
• Fix: Added missing caller_idx (user) and funding_rate params

Error 3: No method set_mode_resolved

• Line 7698: engine.set_mode_resolved(1_000_000)
• Fix: Replaced with proof_stale_sweep_blocks_risk_increasing_trade. The 'Resolved mode' was replaced by force-realize mode + sweep staleness. New proof tests the actual mechanism.

Impact

All 152 kani harnesses should now compile and be runnable.

Task: PERC-238

Summary by CodeRabbit

Release Notes

• Breaking Changes

  • keeper_crank function now requires an additional funding_rate parameter when called.

• Bug Fixes

  • Updated funding rate tracking behavior in risk calculations to accurately reflect last observed funding rates.

[coderabbitai]

📝 Walkthrough

Walkthrough

A test file is updated with a field rename from funding_rate_bps_per_slot to funding_rate_bps_per_slot_last, the keeper_crank function signature is extended to accept a funding_rate parameter, and a test is renamed to reflect new stale sweep validation logic with corresponding test setup adjustments.

Changes

Cohort / File(s)

Summary

Test Suite Updates tests/kani.rs

Field renamed to funding_rate_bps_per_slot_last for tracking last observed funding rate. keeper_crank function signature updated to accept new funding_rate: i64 parameter positioned between amount and caller_settle_ok. Test proof_resolved_mode_blocks_trading renamed to proof_stale_sweep_blocks_risk_increasing_trade with updated setup to initialize last_full_sweep_start_slot and max_crank_staleness_slots for stale sweep scenario validation. Call sites updated to pass new parameter.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

Poem

🐰 A funding rate hops into view,
Last observed, tracked fresh and true,
The crank swings wide with rates in hand,
Tests now sweep through stale-ish land,
Logic flows where staleness grows! 📊

🚥 Pre-merge checks | ✅ 3

✅ Passed checks (3 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly and specifically describes the main change: fixing compilation errors in kani.rs by addressing three bitrotted references, with a task reference for context.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

• 📝 Generate docstrings (stacked PR)
• 📝 Generate docstrings (commit on current branch)

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Post copyable unit tests in a comment
• Commit unit tests in branch fix/PERC-238-kani-compilation

---

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

🧹 Nitpick comments (1)

tests/kani.rs (1)

7666-7666: Avoid a vacuous proof by checking crank success.

Line 7666 drops the Result; if crank returns Err, the proof can pass without actually exercising the intended funding path.

Suggested diff

-    let _ = engine.keeper_crank(user, now_slot, 1_000_000, funding_rate, false);
+    let crank_res = engine.keeper_crank(user, now_slot, 1_000_000, funding_rate, false);
+    assert_ok!(crank_res, "non-vacuity: keeper_crank must succeed");

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@tests/kani.rs` at line 7666, The call to engine.keeper_crank(user, now_slot,
1_000_000, funding_rate, false) currently drops the Result which can let a
failure silently pass; change this to explicitly check the Result (e.g.,
unwrap(), expect(...), or assert!(res.is_ok())) so the test fails if
keeper_crank returns Err and the funding path is actually exercised—locate the
invocation of engine.keeper_crank in tests/kani.rs and replace the discarded-let
with a checked result handling using the same parameters (user, now_slot,
1_000_000, funding_rate, false).

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Nitpick comments:
In `@tests/kani.rs`:
- Line 7666: The call to engine.keeper_crank(user, now_slot, 1_000_000,
funding_rate, false) currently drops the Result which can let a failure silently
pass; change this to explicitly check the Result (e.g., unwrap(), expect(...),
or assert!(res.is_ok())) so the test fails if keeper_crank returns Err and the
funding path is actually exercised—locate the invocation of engine.keeper_crank
in tests/kani.rs and replace the discarded-let with a checked result handling
using the same parameters (user, now_slot, 1_000_000, funding_rate, false).

---

ℹ️ Review info

Configuration used: defaults

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 65f1aac and f33d273.

📒 Files selected for processing (1)

• tests/kani.rs