kunobi_daemon/
retry.rs

1//! Persistable replacement attempt budgets. Never use these to replay requests.
2
3/// Consumer policy for candidate retries across controller restarts.
4#[derive(Clone, Copy, Debug)]
5#[cfg_attr(kani, derive(kani::Arbitrary))]
6pub struct Policy {
7    /// Maximum attempts for one unchanged candidate selection.
8    pub limit: u64,
9    /// Initial delay in seconds, doubled after each attempted start.
10    pub delay: u64,
11    /// Maximum delay in seconds.
12    pub maximum_delay: u64,
13}
14/// State stored alongside the consumer's candidate fingerprint.
15#[derive(Clone, Copy, Debug, Default)]
16#[cfg_attr(kani, derive(kani::Arbitrary))]
17pub struct State {
18    /// Reserved attempts, including candidates that die immediately after commit.
19    pub attempts: u64,
20    /// Earliest permitted retry in the consumer's persisted time domain (seconds).
21    pub next_attempt: u64,
22}
23impl State {
24    /// Whether this campaign may attempt a candidate now.
25    pub fn allowed(&self, policy: Policy, now: u64) -> bool {
26        self.attempts < policy.limit && now >= self.next_attempt
27    }
28    /// Reserve before launching. Persist the returned state before spawning;
29    /// cancellation and controller crashes must not restore the spent attempt.
30    pub fn reserve(&mut self, policy: Policy, now: u64) {
31        self.attempts = self.attempts.saturating_add(1);
32        let multiplier = 1u64 << self.attempts.min(63);
33        self.next_attempt = now.saturating_add(
34            policy
35                .delay
36                .saturating_mul(multiplier)
37                .min(policy.maximum_delay),
38        );
39    }
40    /// A permanent candidate failure exhausts this fingerprint's campaign.
41    pub fn exhaust(&mut self, policy: Policy) {
42        self.attempts = policy.limit;
43    }
44    /// Next retry time, or None once a new candidate selection is required.
45    pub fn next(&self, policy: Policy) -> Option<u64> {
46        (self.attempts < policy.limit).then_some(self.next_attempt)
47    }
48}
49
50/// Properties of the budget for every policy, clock reading and persisted
51/// state, including the extremes a stale or hand-edited record can hold.
52#[cfg(kani)]
53mod proofs {
54    use super::*;
55
56    /// Reserving never panics, never wraps the clock and never schedules the
57    /// next attempt beyond the maximum delay.
58    #[kani::proof]
59    fn a_reservation_waits_no_longer_than_the_maximum_delay() {
60        let policy: Policy = kani::any();
61        let mut state: State = kani::any();
62        let now: u64 = kani::any();
63        let attempts = state.attempts;
64        state.reserve(policy, now);
65        assert!(state.attempts == attempts.saturating_add(1));
66        assert!(now <= state.next_attempt);
67        assert!(state.next_attempt <= now.saturating_add(policy.maximum_delay));
68    }
69
70    /// Backoff never shrinks as attempts grow, and never retries sooner than
71    /// the initial delay unless the maximum is lower.
72    ///
73    /// The delay is bounded to 16 bits, about 18 hours, to keep the
74    /// multiplication tractable for the solver. The doubled delay still
75    /// saturates, from the 49th attempt for the longest one, so the capped
76    /// arithmetic is covered.
77    #[kani::proof]
78    fn backoff_never_shrinks_as_attempts_grow() {
79        let policy: Policy = kani::any();
80        kani::assume(policy.delay <= u64::from(u16::MAX));
81        let now: u64 = kani::any();
82        let mut earlier = State {
83            attempts: kani::any(),
84            next_attempt: 0,
85        };
86        let mut later = State {
87            attempts: kani::any(),
88            next_attempt: 0,
89        };
90        kani::assume(earlier.attempts <= later.attempts);
91        earlier.reserve(policy, now);
92        later.reserve(policy, now);
93        assert!(earlier.next_attempt <= later.next_attempt);
94        let floor = policy.delay.min(policy.maximum_delay);
95        assert!(earlier.next_attempt >= now.saturating_add(floor));
96    }
97
98    /// A consumer that reserves only when allowed never spends more than the
99    /// limit, and an exhausted campaign allows nothing at any later time.
100    #[kani::proof]
101    fn a_campaign_never_exceeds_its_attempt_limit() {
102        let policy: Policy = kani::any();
103        let mut state: State = kani::any();
104        let now: u64 = kani::any();
105        // Both readings a consumer may act on give the same answer.
106        let allowed = state.allowed(policy, now);
107        assert!(allowed == state.next(policy).is_some_and(|at| now >= at));
108        if allowed {
109            state.reserve(policy, now);
110            assert!(state.attempts <= policy.limit);
111        }
112        state.exhaust(policy);
113        assert!(!state.allowed(policy, kani::any()));
114        assert!(state.next(policy).is_none());
115    }
116}
kunobi_daemon/retry.rs

kunobi_daemon/
retry.rs
