kernel/
account_recovery.rs

1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at https://mozilla.org/MPL/2.0/.
4// Copyright (c) 2026 2youg1 and the sprawling contributors
5
6//! Which account of a provider a request goes out on, and after a failure
7//! whether it goes out again on the same account, moves to another, or
8//! stops.
9//! The part `crates/kernel/spec/AccountRecovery.lean` specifies this
10//! module (`crates/kernel/Spec.lean` §8-86, kernel D54 and D55).
11//!
12//! **One round is one logical request**, from its first send to an
13//! answer, a stop or a `Halt`. Both drivers - the model path in the
14//! runtime and the `web_search` tool in accounting - only carry out the
15//! [`AccountStep`] a round gives them, so neither grows a retry loop or
16//! an account choice of its own. [`AccountRound::next`] answers and
17//! changes nothing; [`AccountRound::apply`] changes and answers nothing.
18//!
19//! A round is neither recorded nor persisted: a restarted process opens
20//! the next round from the binding the ledger rebuilds.
21
22use std::collections::BTreeSet;
23
24use crate::error::{AccountDisposition, AxError, Retry};
25use crate::retries::Retries;
26use crate::tool::ServerLabel;
27
28/// How many more times one account is asked the same request before the
29/// round moves on. A person picks one or two on the provider's advanced
30/// form; it is read only where the roster has two accounts or more. On
31/// the wire and in the ledger `"one"` or `"two"`; the default lives in
32/// gateway's `EndpointTuning::DEFAULTS` alone.
33#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
34#[serde(rename_all = "snake_case")]
35#[cfg_attr(feature = "schema", derive(schemars::JsonSchema))]
36pub enum AccountRetries {
37    One,
38    Two,
39}
40
41impl AccountRetries {
42    const fn count(self) -> u32 {
43        match self {
44            AccountRetries::One => 1,
45            AccountRetries::Two => 2,
46        }
47    }
48}
49
50/// The accounts a round can send on.
51#[derive(Debug, Clone, PartialEq, Eq)]
52pub enum Roster {
53    /// A registration with one credential, or with one listed account:
54    /// there is no second account, so a failure is handled as it was
55    /// before accounts existed - `retry` alone decides, up to the
56    /// person's ceiling.
57    Single,
58    /// Two accounts or more. The order is the priority.
59    Several {
60        accounts: Vec<ServerLabel>,
61        retries: AccountRetries,
62    },
63}
64
65/// Why a round stopped.
66#[derive(Debug, Clone, Copy, PartialEq, Eq)]
67pub enum RoundEnd {
68    /// The request itself is wrong, or the store every account shares
69    /// failed: sent again anywhere it would fail the same way.
70    Refused,
71    /// The answer was lost on the last account's last allowed send, and
72    /// whether its effect landed is not known.
73    Unknown,
74    /// The person's ceiling on retries was reached.
75    Cap,
76    /// No account is left to switch to.
77    Exhausted,
78}
79
80/// What the driver does after one failed send.
81#[derive(Debug, Clone, PartialEq, Eq)]
82pub enum AccountStep {
83    /// Send the same request again on the same account, after the
84    /// driver's back-off.
85    Resend,
86    /// Send the same request on this account at once.
87    Switch { to: ServerLabel },
88    /// Send nothing more; hand the failure on.
89    Stop { why: RoundEnd },
90}
91
92/// One round's state. Every field is private: a round moves only through
93/// [`AccountRound::apply`] and [`AccountRound::repaired`].
94#[derive(Debug, Clone, PartialEq, Eq)]
95pub struct AccountRound {
96    roster: Roster,
97    /// The accounts whose reference could be redeemed when the round
98    /// opened (D55); asked once, never re-read mid-round.
99    usable: BTreeSet<ServerLabel>,
100    cap: Retries,
101    current: Option<ServerLabel>,
102    /// The accounts this round has sent on.
103    tried: BTreeSet<ServerLabel>,
104    /// Sends on the current account.
105    here: u32,
106    /// Sends in this round.
107    total: u32,
108}
109
110impl AccountRound {
111    /// Opens a round before its first send, and counts that send. The
112    /// account `held` - the Session's binding on the model path, absent
113    /// for `web_search` - opens the round while it is listed and
114    /// redeemable; otherwise the first redeemable account in roster
115    /// order does.
116    ///
117    /// # Errors
118    /// [`RoundEnd::Exhausted`] when no listed account is redeemable: the
119    /// round sends nothing.
120    pub fn start(
121        roster: Roster,
122        usable: BTreeSet<ServerLabel>,
123        cap: Retries,
124        held: Option<ServerLabel>,
125    ) -> Result<AccountRound, RoundEnd> {
126        let current = match &roster {
127            Roster::Single => None,
128            Roster::Several { accounts, .. } => {
129                let opening = held
130                    .filter(|account| accounts.contains(account) && usable.contains(account))
131                    .or_else(|| {
132                        accounts
133                            .iter()
134                            .find(|account| usable.contains(*account))
135                            .cloned()
136                    });
137                Some(opening.ok_or(RoundEnd::Exhausted)?)
138            }
139        };
140        Ok(AccountRound {
141            roster,
142            usable,
143            cap,
144            tried: current.iter().cloned().collect(),
145            current,
146            here: 1,
147            total: 1,
148        })
149    }
150
151    /// The account the next send goes out on; `None` for a single-account
152    /// roster, which names none.
153    #[must_use]
154    pub fn current(&self) -> Option<&ServerLabel> {
155        self.current.as_ref()
156    }
157
158    /// What to do after `failure`, read from its `retry` and its
159    /// `account` disposition alone (D54).
160    #[must_use]
161    pub fn next(&self, failure: &AxError) -> AccountStep {
162        match &self.roster {
163            Roster::Single => match failure.retry() {
164                Retry::No => AccountStep::Stop {
165                    why: RoundEnd::Refused,
166                },
167                Retry::Yes | Retry::Unknown => self.resend(),
168            },
169            Roster::Several { retries, .. } => {
170                let spare = self.here <= retries.count();
171                match (failure.retry(), failure.account()) {
172                    (Retry::Unknown, AccountDisposition::Keep | AccountDisposition::Advance) => {
173                        if spare {
174                            self.resend()
175                        } else {
176                            AccountStep::Stop {
177                                why: RoundEnd::Unknown,
178                            }
179                        }
180                    }
181                    (Retry::Yes | Retry::No, AccountDisposition::Advance) => self.switch(),
182                    (Retry::Yes, AccountDisposition::Keep) => {
183                        if spare {
184                            self.resend()
185                        } else {
186                            self.switch()
187                        }
188                    }
189                    (Retry::No, AccountDisposition::Keep) => AccountStep::Stop {
190                        why: RoundEnd::Refused,
191                    },
192                }
193            }
194        }
195    }
196
197    /// The round after the driver carried out `step`. `Stop` changes
198    /// nothing. The counts saturate rather than wrap: a single-account
199    /// round under `UntilHalted` resends until a `Halt`, and a count that
200    /// wrapped would read as a fresh account's spare sends.
201    #[must_use]
202    pub fn apply(self, step: &AccountStep) -> AccountRound {
203        match step {
204            AccountStep::Resend => AccountRound {
205                here: self.here.saturating_add(1),
206                total: self.total.saturating_add(1),
207                ..self
208            },
209            AccountStep::Switch { to } => {
210                let mut tried = self.tried;
211                tried.insert(to.clone());
212                AccountRound {
213                    current: Some(to.clone()),
214                    tried,
215                    here: 1,
216                    total: self.total.saturating_add(1),
217                    ..self
218                }
219            }
220            AccountStep::Stop { .. } => self,
221        }
222    }
223
224    /// Whether the repair stage may send the request again through the
225    /// blocking door. With several accounts that send is one more on the
226    /// current account, so it needs the account's spare sends and the
227    /// person's ceiling; a single-account roster is let through as
228    /// before.
229    #[must_use]
230    pub fn admits_repair(&self) -> bool {
231        match &self.roster {
232            Roster::Single => true,
233            Roster::Several { retries, .. } => {
234                self.here <= retries.count() && admits(self.cap, self.total)
235            }
236        }
237    }
238
239    /// The round after the repair stage sent again: one more send on the
240    /// current account with several accounts, uncounted with one.
241    #[must_use]
242    pub fn repaired(self) -> AccountRound {
243        match self.roster {
244            Roster::Single => self,
245            Roster::Several { .. } => self.apply(&AccountStep::Resend),
246        }
247    }
248
249    fn resend(&self) -> AccountStep {
250        if admits(self.cap, self.total) {
251            AccountStep::Resend
252        } else {
253            AccountStep::Stop { why: RoundEnd::Cap }
254        }
255    }
256
257    /// Switches to the first listed account that is redeemable and not
258    /// yet tried this round. Running out is said before the ceiling is,
259    /// because "no account is left" points at the way out (D54, rule 7).
260    fn switch(&self) -> AccountStep {
261        let Roster::Several { accounts, .. } = &self.roster else {
262            return AccountStep::Stop {
263                why: RoundEnd::Exhausted,
264            };
265        };
266        match accounts
267            .iter()
268            .find(|account| self.usable.contains(*account) && !self.tried.contains(*account))
269        {
270            None => AccountStep::Stop {
271                why: RoundEnd::Exhausted,
272            },
273            Some(to) if admits(self.cap, self.total) => AccountStep::Switch { to: to.clone() },
274            Some(_) => AccountStep::Stop { why: RoundEnd::Cap },
275        }
276    }
277}
278
279/// Whether the person's ceiling lets one more send follow `sent` sends.
280/// `AtMost(0)` sends once and stops, as the watchdog has always read it.
281fn admits(cap: Retries, sent: u32) -> bool {
282    match cap {
283        Retries::UntilHalted => true,
284        Retries::AtMost(retries) => sent <= retries,
285    }
286}
287
288#[cfg(test)]
289#[allow(
290    clippy::unwrap_used,
291    clippy::expect_used,
292    clippy::panic,
293    clippy::indexing_slicing,
294    clippy::arithmetic_side_effects,
295    reason = "test code"
296)]
297mod tests {
298    use std::collections::BTreeMap;
299
300    use proptest::prelude::*;
301
302    use super::*;
303    use crate::error::AxCode;
304
305    /// What a driver meets in a round: the four failures the error
306    /// builders can spell (`Advance` only ever comes with `Retry::No`,
307    /// kernel D53), and the repair stage wanting to send again.
308    #[derive(Debug, Clone, Copy, PartialEq, Eq)]
309    enum Event {
310        Busy,
311        Unusable,
312        Refused,
313        Lost,
314        Repair,
315    }
316
317    fn failure(event: Event) -> Option<AxError> {
318        let draft = AxError::failure(AxCode::Provider, "call model", "account");
319        match event {
320            Event::Busy => Some(draft.retriable().with_recovery("r")),
321            Event::Unusable => Some(draft.account_unusable().with_recovery("r")),
322            Event::Refused => Some(draft.with_recovery("r")),
323            Event::Lost => Some(draft.effect_unknown().with_recovery("r")),
324            Event::Repair => None,
325        }
326    }
327
328    fn label(name: &str) -> ServerLabel {
329        ServerLabel::parse(name).unwrap()
330    }
331
332    fn several(names: &[&str], retries: AccountRetries) -> Roster {
333        Roster::Several {
334            accounts: names.iter().map(|name| label(name)).collect(),
335            retries,
336        }
337    }
338
339    /// Lean's `AccountRound.decisions`: a failure asks `next` and stops
340    /// on `Stop`; a repair asks `admits_repair`, and is `None` when it is
341    /// not let through.
342    fn decisions(mut round: AccountRound, events: &[Event]) -> Vec<(Event, Option<AccountStep>)> {
343        let mut out = Vec::new();
344        for &event in events {
345            match failure(event) {
346                None if round.admits_repair() => {
347                    out.push((event, Some(AccountStep::Resend)));
348                    round = round.repaired();
349                }
350                None => out.push((event, None)),
351                Some(err) => {
352                    let step = round.next(&err);
353                    out.push((event, Some(step.clone())));
354                    if let AccountStep::Stop { .. } = step {
355                        break;
356                    }
357                    round = round.apply(&step);
358                }
359            }
360        }
361        out
362    }
363
364    type Decided = Option<(Option<ServerLabel>, Vec<(Event, Option<AccountStep>)>)>;
365
366    /// Lean's `vector`: open the round, then walk the events.
367    fn vector(
368        roster: Roster,
369        missing: &[&str],
370        cap: Retries,
371        held: Option<&str>,
372        events: &[Event],
373    ) -> Decided {
374        let usable = match &roster {
375            Roster::Single => BTreeSet::new(),
376            Roster::Several { accounts, .. } => accounts
377                .iter()
378                .filter(|account| !missing.contains(&account.as_str()))
379                .cloned()
380                .collect(),
381        };
382        let round = AccountRound::start(roster, usable, cap, held.map(label)).ok()?;
383        Some((round.current().cloned(), decisions(round, events)))
384    }
385
386    fn resend() -> Option<AccountStep> {
387        Some(AccountStep::Resend)
388    }
389
390    fn switch(to: &str) -> Option<AccountStep> {
391        Some(AccountStep::Switch { to: label(to) })
392    }
393
394    fn stop(why: RoundEnd) -> Option<AccountStep> {
395        Some(AccountStep::Stop { why })
396    }
397
398    /// The trace vectors `crates/kernel/spec/AccountRecovery.lean` prints
399    /// with `#eval`, in its order, each with the answer Lean gave, and
400    /// the `decide` example after them.
401    #[test]
402    fn the_lean_trace_vectors_replay_one_by_one() {
403        use Event::{Busy, Lost, Refused, Repair, Unusable};
404        let two = || several(&["a", "b"], AccountRetries::Two);
405        let a = Some(label("a"));
406        let b = Some(label("b"));
407        let found = [
408            vector(
409                two(),
410                &[],
411                Retries::UntilHalted,
412                None,
413                &[Busy, Busy, Busy, Busy],
414            ),
415            vector(
416                two(),
417                &[],
418                Retries::UntilHalted,
419                None,
420                &[Unusable, Unusable],
421            ),
422            vector(two(), &[], Retries::UntilHalted, None, &[Refused]),
423            vector(two(), &[], Retries::UntilHalted, None, &[Lost, Lost, Lost]),
424            vector(two(), &[], Retries::AtMost(1), None, &[Busy, Busy]),
425            vector(
426                several(&["a", "b", "c"], AccountRetries::One),
427                &["b"],
428                Retries::UntilHalted,
429                Some("c"),
430                &[Busy, Busy, Unusable],
431            ),
432            vector(
433                several(&["a", "b"], AccountRetries::One),
434                &[],
435                Retries::UntilHalted,
436                Some("b"),
437                &[Repair, Busy, Repair],
438            ),
439            vector(two(), &["a", "b"], Retries::UntilHalted, None, &[]),
440            vector(
441                Roster::Single,
442                &[],
443                Retries::AtMost(2),
444                None,
445                &[Busy, Lost, Busy],
446            ),
447            vector(
448                Roster::Single,
449                &[],
450                Retries::UntilHalted,
451                None,
452                &[Repair, Unusable],
453            ),
454            vector(two(), &[], Retries::UntilHalted, Some("b"), &[Busy]),
455        ];
456        let lean: [Decided; 11] = [
457            Some((
458                a.clone(),
459                vec![
460                    (Busy, resend()),
461                    (Busy, resend()),
462                    (Busy, switch("b")),
463                    (Busy, resend()),
464                ],
465            )),
466            Some((
467                a.clone(),
468                vec![
469                    (Unusable, switch("b")),
470                    (Unusable, stop(RoundEnd::Exhausted)),
471                ],
472            )),
473            Some((a.clone(), vec![(Refused, stop(RoundEnd::Refused))])),
474            Some((
475                a.clone(),
476                vec![
477                    (Lost, resend()),
478                    (Lost, resend()),
479                    (Lost, stop(RoundEnd::Unknown)),
480                ],
481            )),
482            Some((a, vec![(Busy, resend()), (Busy, stop(RoundEnd::Cap))])),
483            Some((
484                Some(label("c")),
485                vec![
486                    (Busy, resend()),
487                    (Busy, switch("a")),
488                    (Unusable, stop(RoundEnd::Exhausted)),
489                ],
490            )),
491            Some((
492                b.clone(),
493                vec![(Repair, resend()), (Busy, switch("a")), (Repair, resend())],
494            )),
495            None,
496            Some((
497                None,
498                vec![
499                    (Busy, resend()),
500                    (Lost, resend()),
501                    (Busy, stop(RoundEnd::Cap)),
502                ],
503            )),
504            Some((
505                None,
506                vec![(Repair, resend()), (Unusable, stop(RoundEnd::Refused))],
507            )),
508            Some((b, vec![(Busy, resend())])),
509        ];
510        assert_eq!(found, lean);
511    }
512
513    fn switched(step: &AccountStep) -> bool {
514        matches!(step, AccountStep::Switch { .. })
515    }
516
517    fn event() -> impl Strategy<Value = Event> {
518        prop_oneof![
519            Just(Event::Busy),
520            Just(Event::Unusable),
521            Just(Event::Refused),
522            Just(Event::Lost),
523            Just(Event::Repair),
524        ]
525    }
526
527    fn cap() -> impl Strategy<Value = Retries> {
528        prop_oneof![
529            Just(Retries::UntilHalted),
530            (0u32..8).prop_map(Retries::AtMost)
531        ]
532    }
533
534    /// Five names a roster draws from, and one it never lists, so a held
535    /// account can be one the person removed.
536    const NAMES: [&str; 6] = ["a", "b", "c", "d", "e", "z"];
537
538    proptest! {
539        /// The quantified theorems of `crates/kernel/spec/AccountRecovery.lean`
540        /// on any roster of two to five accounts, any redeemable subset,
541        /// any ceiling, any held account (listed or not) and any trace:
542        /// `a_request_error_is_never_sent_again`,
543        /// `an_unusable_account_is_never_asked_again`,
544        /// `an_unknown_effect_never_switches`,
545        /// `sends_on_one_account_stay_within_the_budget`,
546        /// `a_round_visits_each_account_once`, `the_cap_bounds_every_round`,
547        /// `a_held_account_opens_the_round` and
548        /// `a_roster_with_nothing_redeemable_sends_nothing`. The sends are
549        /// counted here from the steps the driver carries out, not read
550        /// from the round.
551        #[test]
552        fn every_round_keeps_the_lean_properties(
553            listed in 2usize..=5,
554            missing in proptest::collection::vec(any::<bool>(), 5),
555            two in any::<bool>(),
556            cap in cap(),
557            held in proptest::option::of(0usize..6),
558            events in proptest::collection::vec(event(), 0..40),
559        ) {
560            let accounts: Vec<ServerLabel> = NAMES[..listed].iter().map(|name| label(name)).collect();
561            let usable: BTreeSet<ServerLabel> = accounts
562                .iter()
563                .zip(&missing)
564                .filter(|(_, gone)| !**gone)
565                .map(|(account, _)| account.clone())
566                .collect();
567            let retries = if two { AccountRetries::Two } else { AccountRetries::One };
568            let budget = if two { 3 } else { 2 };
569            let held = held.map(|at| label(NAMES[at]));
570            let opened = AccountRound::start(
571                Roster::Several { accounts: accounts.clone(), retries },
572                usable.clone(),
573                cap,
574                held.clone(),
575            );
576            if usable.is_empty() {
577                prop_assert_eq!(opened, Err(RoundEnd::Exhausted));
578                return Ok(());
579            }
580            let mut round = opened.unwrap();
581            let first = held
582                .filter(|account| usable.contains(account))
583                .or_else(|| accounts.iter().find(|account| usable.contains(*account)).cloned());
584            prop_assert_eq!(round.current().cloned(), first.clone());
585            let mut on = first.unwrap();
586            let mut visited = vec![on.clone()];
587            let mut sends = BTreeMap::from([(on.clone(), 1u32)]);
588            let mut total = 1u32;
589            for event in events {
590                let Some(err) = failure(event) else {
591                    if round.admits_repair() {
592                        *sends.get_mut(&on).unwrap() += 1;
593                        total += 1;
594                        round = round.repaired();
595                    }
596                    continue;
597                };
598                let step = round.next(&err);
599                match event {
600                    Event::Refused => {
601                        prop_assert_eq!(&step, &AccountStep::Stop { why: RoundEnd::Refused });
602                    }
603                    Event::Unusable => prop_assert_ne!(&step, &AccountStep::Resend),
604                    Event::Lost => prop_assert_ne!(switched(&step), true),
605                    Event::Busy | Event::Repair => {}
606                }
607                match &step {
608                    AccountStep::Resend => {
609                        *sends.get_mut(&on).unwrap() += 1;
610                    }
611                    AccountStep::Switch { to } => {
612                        prop_assert!(
613                            usable.contains(to) && !visited.contains(to),
614                            "{to} was tried already or is not redeemable"
615                        );
616                        visited.push(to.clone());
617                        sends.insert(to.clone(), 1);
618                        on = to.clone();
619                    }
620                    AccountStep::Stop { .. } => break,
621                }
622                total += 1;
623                round = round.apply(&step);
624                prop_assert_eq!(round.current(), Some(&on));
625            }
626            prop_assert!(sends.values().all(|&sent| sent <= budget), "{sends:?} over {budget}");
627            prop_assert!(total <= u32::try_from(listed).unwrap() * budget);
628            if let Retries::AtMost(retries) = cap {
629                prop_assert!(total <= retries + 1, "{total} sends under AtMost({retries})");
630            }
631        }
632
633        /// A single-account roster reads `retry` alone
634        /// (`a_single_account_ignores_the_disposition`): it never switches,
635        /// a refusal stops it whether or not it says to switch, the repair
636        /// stage is always let through uncounted, and the person's ceiling
637        /// bounds its sends.
638        #[test]
639        fn a_single_account_round_reads_retry_alone(
640            cap in cap(),
641            events in proptest::collection::vec(event(), 0..40),
642        ) {
643            let mut round = AccountRound::start(Roster::Single, BTreeSet::new(), cap, None).unwrap();
644            prop_assert_eq!(round.current(), None);
645            let mut total = 1u32;
646            for event in events {
647                let Some(err) = failure(event) else {
648                    prop_assert!(round.admits_repair());
649                    round = round.repaired();
650                    continue;
651                };
652                let step = round.next(&err);
653                match event {
654                    Event::Refused | Event::Unusable => {
655                        prop_assert_eq!(&step, &AccountStep::Stop { why: RoundEnd::Refused });
656                    }
657                    Event::Busy | Event::Lost | Event::Repair => {
658                        prop_assert_ne!(switched(&step), true);
659                    }
660                }
661                if let AccountStep::Stop { .. } = step {
662                    break;
663                }
664                total += 1;
665                round = round.apply(&step);
666            }
667            if let Retries::AtMost(retries) = cap {
668                prop_assert!(total <= retries + 1);
669            }
670        }
671    }
672}
kernel/account_recovery.rs

kernel/
account_recovery.rs
