From 3f2cb01b812a5bf953cc735f1e9fa4ff127254cf Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 17 May 2026 11:11:35 +0100 Subject: [PATCH] =?UTF-8?q?fix(kani):=20Wave=2012-N=20=E2=80=94=20update?= =?UTF-8?q?=20permissionless=5Fprogress=20harness=20for=20Wave=2011a-ii-C?= =?UTF-8?q?=20semantics?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- tests/proofs_invariants.rs | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/tests/proofs_invariants.rs b/tests/proofs_invariants.rs index 87706b9c3..45b5d1d7e 100644 --- a/tests/proofs_invariants.rs +++ b/tests/proofs_invariants.rs @@ -1411,12 +1411,26 @@ fn proof_permissionless_progress_resolved_routes_to_resolved_close() { } } -/// `permissionless_progress_not_atomic` short-circuits with -/// `RecoveryRequired` when an active bankrupt-close is in flight. This -/// is the defense-in-depth gate the Wave 11a-ii-B port adds while the -/// full recovery resolver is deferred — surfaces a stable error -/// instead of taking either of the two live-mode branches the -/// dispatcher knows. +/// `permissionless_progress_not_atomic` enters the active bankrupt-close +/// dispatch branch when `active_close_present != 0`. Wave 11a-ii-C made +/// this branch DO work (either continue the state machine via +/// `continue_active_bankrupt_close_not_atomic` or invoke the recovery +/// resolver via `active_bankrupt_close_recovery_required`) instead of +/// returning a static `RecoveryRequired` gate. +/// +/// On a freshly-init engine where `active_close_present = 1` is set +/// without populating the rest of the state machine +/// (`bankruptcy_hmax_lock_active`, `active_close_phase`, +/// `active_close_close_price`, `active_close_residual_remaining`), the +/// branch must REJECT — not silently advance — because the state is +/// partial and unsafe to process. Wave 11a-ii-C's +/// `validate_active_bankrupt_close_shape` returns `CorruptState` in +/// this case, surfacing via `active_bankrupt_close_recovery_required`'s +/// `?` propagation. +/// +/// This harness pins the contract: with a partial active_close state +/// the dispatcher MUST return an error (any error) — it must never +/// take either of the two normal live-mode branches. #[kani::proof] #[kani::unwind(5)] #[kani::solver(cadical)] @@ -1444,10 +1458,11 @@ fn proof_permissionless_progress_rejects_when_active_close_present() { resolved_fee_rate_per_slot: 0, }; - assert_eq!( - engine.permissionless_progress_not_atomic(req), - Err(RiskError::RecoveryRequired) - ); + // Partial active_close state must REJECT — never silently take the + // ordinary live-mode branches. Wave 11a-ii-C returns CorruptState + // via shape validation; Wave 11a-ii-B used to return RecoveryRequired. + // Either is acceptable; what matters is it's an Err. + assert!(engine.permissionless_progress_not_atomic(req).is_err()); } /// `force_close_resolved_cursor_with_fee_not_atomic` rejects a non-Resolved