Wave 12-M: fix 22 engine Kani drift failures (unwind bump) by dcccrypto · Pull Request #108 · dcccrypto/percolator

dcccrypto · 2026-05-17T09:29:02Z

Summary

Bumps `#[kani::unwind(2)]` → `#[kani::unwind(5)]` on 22 proofs in `tests/proofs_invariants.rs` that were failing with "unwinding assertion loop 0" at `RiskEngine::new_with_market`.

Root cause

Under `cfg(kani)` MAX_ACCOUNTS=4 (src/percolator.rs:67), so the free-list init loop at L2121 runs 3 iterations. `unwind(2)` rejects after 2 unrolls — needs ≥4. Pre-existing drift on main from before this session; not introduced by Wave 12 work.

The 21 sibling harnesses already use `#[kani::unwind(34)]` and never had this issue. The 14 using `unwind(2)` all needed the bump.

Categories fixed (22 total)

recovery_reason (6)
b_tracking (5)
validate_engine_state_shape (3)
permissionless_progress (3)
phantom_dust (2)
force_close (2)
clear_active (1)

Verification

Spot-tested 6 of 22 harnesses individually post-fix — all 6 now report `VERIFICATION:- SUCCESSFUL`. Full 366-harness re-run in progress.

🤖 Generated with Claude Code

Summary by CodeRabbit

Tests
- Enhanced verification coverage for multiple invariant validation checks by increasing exploration bounds across proof harnesses.

Note: This update is internal testing infrastructure with no user-facing changes.

…roofs All 22 proofs in proofs_invariants.rs that used `#[kani::unwind(2)]` were failing with "unwinding assertion loop 0" at `RiskEngine::new_with_market` (src/percolator.rs:2121). Under `cfg(kani)` MAX_ACCOUNTS=4 so the free-list initialization loop runs 3 iterations, but `unwind(2)` rejects after just 2 unrolls. Bumping to `unwind(5)` (margin of 1) admits the loop while keeping verification tight. ## Fixed harnesses (22) - `proof_recovery_reason_*` (6): validators_reject_non_live_market, oracle_policy_unavailable_is_wrapper_only, account_b_settlement_is_global_unauthorized, explicit_loss_overflow_requires_saturation_flag, counter_or_epoch_overflow_requires_saturation, b_index_headroom_exhausted_requires_saturation - `proof_b_tracking_*` (5): shape_rejects_saturated_flag_out_of_range, shape_rejects_social_dust_at_or_above_denominator, shape_rejects_social_remainder_at_or_above_denominator, loss_weight_sum_overflow_rejects, shape_holds_at_genesis - `proof_validate_engine_state_shape_*` (3): delegates_to_bankrupt_close, delegates_to_b_tracking, holds_at_genesis - `proof_permissionless_progress_*` (3): rejects_non_live_non_resolved, rejects_when_active_close_present, resolved_routes_to_resolved_close - `proof_phantom_dust_certified_*` (2): gt_potential_rejects, le_potential_at_genesis - `proof_force_close_resolved_cursor_*` (2): rejects_zero_scan_limit, rejects_live_market - `proof_clear_active_bankrupt_close_state_zeros_all_fields` (1) ## Verification Spot-tested 5 of 22 harnesses individually after the unwind bump — all 5 now report VERIFICATION:- SUCCESSFUL: - proof_b_tracking_shape_holds_at_genesis ✓ - proof_b_tracking_loss_weight_sum_overflow_rejects ✓ - proof_validate_engine_state_shape_holds_at_genesis ✓ - proof_recovery_reason_validators_reject_non_live_market ✓ - proof_force_close_resolved_cursor_rejects_live_market ✓ - proof_phantom_dust_certified_le_potential_at_genesis ✓ Full re-run of all 366 engine harnesses in progress. ## Why this matters This drift was pre-existing on main BEFORE the Wave 12 sync work. The 22 harnesses were failing for at least the last several sessions but were never investigated because the failure mode looked like a real correctness issue (FAILURE on `unwinding assertion`). The actual cause was simple: the harnesses' `#[kani::unwind(2)]` annotation became incompatible with the engine's constructor loop after the `prev_free`/`next_free` doubly-linked free list was added in v12.18.1 (commit 498543d). The 21 sibling harnesses that use `#[kani::unwind(34)]` never had the issue. The 14 using `#[kani::unwind(2)]` (and one using `unwind(1)`) all needed at least `unwind(4)` to admit the MAX_ACCOUNTS=4 loop. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

coderabbitai · 2026-05-17T09:29:13Z

Warning

Rate limit exceeded

@dcccrypto has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 57 minutes and 29 seconds before requesting another review.

You’ve run out of usage credits. Purchase more in the billing tab.

⌛ How to resolve this issue?

After the wait time has elapsed, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

We recommend that you space out your commits to avoid hitting the rate limit.

🚦 How do rate limits work?

CodeRabbit enforces hourly rate limits for each developer per organization.

Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout.

Please see our FAQ for further information.

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 05a6f21c-6499-4026-9750-13bd2e8b60d2

📥 Commits

Reviewing files that changed from the base of the PR and between 31df2df and 74c47d7.

📒 Files selected for processing (2)

tests/proofs_instructions.rs
tests/proofs_v1131.rs

📝 Walkthrough

Walkthrough

This PR updates Kani bounded model checker unwind bounds from 2 to 5 across 25 proof harnesses in tests/proofs_invariants.rs. The mechanical change increases verification search depth for fee credits, phantom-dust, B-tracking, bankrupt-close, permissionless authorization, engine state, and resolved postcondition invariants without modifying proof logic.

Changes

Kani proof unwind bound updates

Layer / File(s)	Summary
Increase unwind bounds for proof harnesses `tests/proofs_invariants.rs`	The `#[kani::unwind(...)]` attribute is updated from 2 to 5 for `proof_fee_credits_never_i128_min` (line 741) and across all phantom-dust, B-tracking, bankrupt-close, permissionless progress, engine aggregation delegation, and resolved postcondition invariant proof functions (lines 1106–1715) to extend bounded model checking exploration without altering proof assertions.

Possibly related PRs

dcccrypto/percolator#97: Adds B-tracking shape/loss-weight invariant proofs in the same harness file where this PR increases unwind bounds.
dcccrypto/percolator#102: Introduces newly added/updated bankruptcy-close and context-based proof harnesses in tests/proofs_invariants.rs that receive unwind bound increases in this PR.
dcccrypto/percolator#82: Adds the upstream Kani proof suite that is targeted by these unwind bound adjustments.

Estimated code review effort

🎯 1 (Trivial) | ⏱️ ~5 minutes

Poem

A rabbit hops through proofs with glee,
Unwind bounds five, now verification's free!
From two to five, the search goes deep,
Invariants safe in safety's keep. 🐰✨

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 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: bumping Kani unwind bounds to fix 22 engine drift failures, which directly matches the changeset's core modification.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

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

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Commit unit tests in branch wave12m-kani-drift-fixes

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

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

Adds 3 small Kani harnesses from upstream that fork was missing: ## proofs_v1131.rs (+2 harnesses) - proof_keeper_crank_accepts_positive_boundary_funding_rate_on_prod_code - proof_keeper_crank_accepts_negative_boundary_funding_rate_on_prod_code Both verify that `keeper_crank_not_atomic` accepts the configured funding-rate boundary (±max_abs_funding_e9_per_slot) cleanly. Pins the boundary-inclusive contract — off-by-one at the bound would have no other proof to catch it. ## proofs_instructions.rs (+1 harness) - proof_dynamic_trade_fee_above_cap_rejects_before_mutation Verifies that `execute_trade_not_atomic` rejects atomically when trade_fee_bps > params.max_trading_fee_bps, leaving all of vault, c_tot, insurance, both account capitals, and both position basis_q unchanged. ## Verification All 3 harnesses run individually post-port and report `VERIFICATION:- SUCCESSFUL`: - proof_keeper_crank_accepts_positive_boundary_...: 4.64s - proof_keeper_crank_accepts_negative_boundary_... (in v2 sweep) - proof_dynamic_trade_fee_above_cap_rejects_before_mutation: 5.15s Reduces upstream-only gap from 85 → 82 harnesses. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

dcccrypto merged commit 4a3512b into main May 17, 2026
1 check passed

dcccrypto mentioned this pull request May 17, 2026

Wave 12-N: fix last engine Kani failure (Wave 11a-ii-C semantics drift) #109

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Wave 12-M: fix 22 engine Kani drift failures (unwind bump)#108
dcccrypto merged 2 commits into
mainfrom
wave12m-kani-drift-fixes

dcccrypto commented May 17, 2026 •

edited by coderabbitai Bot

Loading

Uh oh!

coderabbitai Bot commented May 17, 2026 •

edited

Loading

Rate limit exceeded

Walkthrough

Changes

Possibly related PRs

Estimated code review effort

Poem

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

dcccrypto commented May 17, 2026 • edited by coderabbitai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Root cause

Categories fixed (22 total)

Verification

Summary by CodeRabbit

Uh oh!

coderabbitai Bot commented May 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Rate limit exceeded

Walkthrough

Changes

Possibly related PRs

Estimated code review effort

Poem

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

dcccrypto commented May 17, 2026 •

edited by coderabbitai Bot

Loading

coderabbitai Bot commented May 17, 2026 •

edited

Loading