Wave 12-N: fix last engine Kani failure (Wave 11a-ii-C semantics drift) - #109
Conversation
…e 11a-ii-C semantics The last remaining engine Kani failure post-Wave-12-M: `proof_permissionless_progress_rejects_when_active_close_present`. ## Root cause The harness was written for Wave 11a-ii-B when the active_close branch of `permissionless_progress_not_atomic` returned a static `Err(RecoveryRequired)` gate. Wave 11a-ii-C upgraded the branch to actually DO work: - If `active_bankrupt_close_recovery_required()` returns true → resolver path → `Ok(PermissionlessProgressOutcome::Recovered(...))` - Else → continue the state machine via `continue_active_bankrupt_close_not_atomic` → `Ok(PermissionlessProgressOutcome::ActiveCloseContinued)` On the harness's freshly-init engine with `active_close_present = 1` but partial state (missing `bankruptcy_hmax_lock_active`, `active_close_phase`, `active_close_close_price`, etc.), `validate_active_bankrupt_close_shape` returns `CorruptState` — NOT `RecoveryRequired`. The Wave 11a-ii-B contract is gone. ## Fix Update the assertion to test the actual contract the harness intends to verify: that a partial active_close state MUST cause the dispatcher to reject (any error), never silently take the ordinary live-mode branches. `assert!(... .is_err())` covers both `CorruptState` (current Wave 11a-ii-C behavior) and `RecoveryRequired` (legacy Wave 11a-ii-B gate) — either is acceptable for the defense-in-depth contract. ## Verification ``` cargo kani --tests --harness proof_permissionless_progress_rejects_when_active_close_present VERIFICATION:- SUCCESSFUL ``` Brings engine Kani to 366/366 SUCCESSFUL. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Warning Rate limit exceeded
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 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 configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (1)
✨ Finishing Touches🧪 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 |
1 participant
Summary
Fixes the last remaining engine Kani failure: `proof_permissionless_progress_rejects_when_active_close_present` (in `tests/proofs_invariants.rs`).
Root cause
Harness was written for Wave 11a-ii-B's gate-only contract. Wave 11a-ii-C upgraded the active_close branch to actually do work (continue state machine OR invoke recovery resolver), so the function no longer returns a static `Err(RecoveryRequired)`.
On the harness's partial init state, fork now returns `Err(CorruptState)` (via `validate_active_bankrupt_close_shape` rejection). Harness asserted `Err(RecoveryRequired)` and failed.
Fix
Change `assert_eq!(..., Err(RecoveryRequired))` → `assert!(... .is_err())`. The harness intent is to verify the dispatcher must reject partial active_close state — never silently advance. Both `CorruptState` (current Wave 11a-ii-C) and `RecoveryRequired` (legacy Wave 11a-ii-B) satisfy this contract.
Doc comment also updated to reflect Wave 11a-ii-C semantics.
Verification
`cargo kani --tests --harness proof_permissionless_progress_rejects_when_active_close_present` → `VERIFICATION:- SUCCESSFUL`
Combined Kani status (engine main after this PR)
🤖 Generated with Claude Code