use core::num::{NonZeroU32, NonZeroU64};
use crate::{Pipe, TimerCancellationRefusal, TimerOut, storage::warp_table::Capacity};
use super::*;
struct Worker;
struct Completed;
impl Pipe for Worker {
type In<'message> = ();
type Out<'message> = Completed;
}
#[kani::proof]
#[kani::unwind(10)]
fn exactly_one_of_completion_or_expiry_resolves_an_admitted_continuation() {
let capacity = Capacity::new(NonZeroU32::MIN);
let Ok(mut ledger) = ContinuationLedger::<()>::try_new(capacity) else {
return;
};
let owed = Owed::wait(TimeoutAfter::nanoseconds(NonZeroU64::MIN));
let ContinuationAdmissionOutcome::Admitted { admission } = ledger.admit::<Worker>((), owed)
else {
assert!(false, "empty continuation ledger must admit one item");
return;
};
let token = admission.timer_token();
let Ok(armed) = (TimerOut::Armed { token }).into_arm_outcome() else {
assert!(false, "armed timer output must convert to an arm outcome");
return;
};
let Ok(ContinuationArmOutcome::Armed { work }) = admission.settle_timer_arm(armed) else {
assert!(false, "matching timer arm must release admitted work");
return;
};
kani::cover!(true, "continuation.armed");
let ((), reply) = work.begin();
let completion = reply.fulfill(Completed);
if kani::any::<bool>() {
let Ok(cancelled) = (TimerOut::Cancelled { token }).into_cancellation_outcome() else {
assert!(false, "cancelled timer output must convert to cancellation");
return;
};
let Ok(ContinuationCancellationOutcome::Cancelled { completion }) =
completion.settle_timer_cancellation(cancelled)
else {
assert!(false, "matching cancellation must release completion");
return;
};
kani::cover!(true, "continuation.completion_first");
assert!(matches!(
ledger.resolve(completion),
ContinuationResolutionOutcome::Resolved { .. }
));
assert!(matches!(
ledger.expire(token),
ContinuationExpirationOutcome::Stale { .. }
));
} else {
assert!(matches!(
ledger.expire(token),
ContinuationExpirationOutcome::Expired { .. }
));
let Ok(refused) = (TimerOut::CancellationRefused {
token,
reason: TimerCancellationRefusal::NotArmed,
})
.into_cancellation_outcome() else {
assert!(false, "refused timer output must convert to cancellation");
return;
};
kani::cover!(true, "continuation.expiry_first");
assert!(matches!(
completion.settle_timer_cancellation(refused),
Ok(ContinuationCancellationOutcome::Stale { .. })
));
}
assert!(ledger.is_empty());
}
#[kani::proof]
#[kani::unwind(10)]
fn exactly_one_of_retraction_or_expiry_removes_unstarted_work() {
let capacity = Capacity::new(NonZeroU32::MIN);
let Ok(mut ledger) = ContinuationLedger::<u8>::try_new(capacity) else {
return;
};
let address: u8 = kani::any();
let timeout = TimeoutAfter::nanoseconds(NonZeroU64::MIN);
let ContinuationAdmissionOutcome::Admitted { admission } =
ledger.admit::<Worker>(address, Owed::wait(timeout))
else {
assert!(false, "empty continuation ledger must admit one item");
return;
};
let token = admission.timer_token();
let Ok(armed) = (TimerOut::Armed { token }).into_arm_outcome() else {
assert!(false, "armed timer output must convert to an arm outcome");
return;
};
let Ok(ContinuationArmOutcome::Armed { work }) = admission.settle_timer_arm(armed) else {
assert!(false, "matching timer arm must release admitted work");
return;
};
kani::cover!(true, "retraction.armed");
if kani::any::<bool>() {
assert!(
matches!(ledger.expire(token), ContinuationExpirationOutcome::Expired { return_to, .. } if return_to == address)
);
}
let pending_before_cancellation = ledger.len();
let Some(wrong_value) = NonZeroU64::new(2) else {
assert!(false, "two is nonzero");
return;
};
let wrong_token = TimerToken::from(wrong_value);
let cancellation_token = if kani::any::<bool>() {
token
} else {
wrong_token
};
let cancellation = if kani::any::<bool>() {
TimerOut::Cancelled {
token: cancellation_token,
}
} else {
TimerOut::CancellationRefused {
token: cancellation_token,
reason: TimerCancellationRefusal::NotArmed,
}
};
let Ok(cancellation) = cancellation.into_cancellation_outcome() else {
assert!(false, "both cancellation variants must convert");
return;
};
match work.settle_timer_cancellation(cancellation) {
Ok(ContinuationWorkCancellationOutcome::Cancelled { work }) => match ledger.retract(work) {
ContinuationRetractionOutcome::Retracted {
return_to,
rejected,
} => {
kani::cover!(true, "retraction.retracted");
assert_eq!(pending_before_cancellation, 1);
assert_eq!(return_to, address);
assert_eq!(rejected.timeout_after(), timeout);
assert!(ledger.is_empty());
assert!(matches!(
ledger.expire(token),
ContinuationExpirationOutcome::Stale { .. }
));
}
ContinuationRetractionOutcome::Stale { work } => {
kani::cover!(true, "retraction.expired");
assert_eq!(pending_before_cancellation, 0);
assert_eq!(work.id().value(), token.value());
assert_eq!(work.owed().timeout_after(), timeout);
assert!(ledger.is_empty());
}
},
Ok(ContinuationWorkCancellationOutcome::Stale { work }) => {
kani::cover!(true, "retraction.refused");
assert_eq!(ledger.len(), pending_before_cancellation);
assert_eq!(work.timer_token(), token);
assert_eq!(work.timeout_after(), timeout);
}
Err(mismatch) => {
kani::cover!(true, "retraction.mismatched");
assert_eq!(ledger.len(), pending_before_cancellation);
let (work, decision) = mismatch.into_parts();
assert_eq!(work.timer_token(), token);
assert_eq!(work.timeout_after(), timeout);
assert!(
matches!(decision, TimerCancellationDecision::Cancelled { token: returned }
| TimerCancellationDecision::Refused { token: returned, .. } if returned == wrong_token)
);
}
}
}