Skip to main content

Module account_recovery

Module account_recovery 

Source
Expand description

Which account of a provider a request goes out on, and after a failure whether it goes out again on the same account, moves to another, or stops. The part crates/kernel/spec/AccountRecovery.lean specifies this module (crates/kernel/Spec.lean §8-86, kernel D54 and D55).

One round is one logical request, from its first send to an answer, a stop or a Halt. Both drivers - the model path in the runtime and the web_search tool in accounting - only carry out the AccountStep a round gives them, so neither grows a retry loop or an account choice of its own. AccountRound::next answers and changes nothing; AccountRound::apply changes and answers nothing.

A round is neither recorded nor persisted: a restarted process opens the next round from the binding the ledger rebuilds.

Structs§

AccountRound
One round’s state. Every field is private: a round moves only through AccountRound::apply and AccountRound::repaired.

Enums§

AccountRetries
How many more times one account is asked the same request before the round moves on. A person picks one or two on the provider’s advanced form; it is read only where the roster has two accounts or more. On the wire and in the ledger "one" or "two"; the default lives in gateway’s EndpointTuning::DEFAULTS alone.
AccountStep
What the driver does after one failed send.
Roster
The accounts a round can send on.
RoundEnd
Why a round stopped.