hax_lib_protocol/
state_machine.rs

1//! This module provides types and traits for implementing a protocol state
2//! machine.
3//!
4//! A protocol party is conceived of as having a set of possible states, one of
5//! which is the initial state. Transitioning to a different state is possible
6//! either through receiving and processing a message or through writing a
7//! message.
8
9use crate::ProtocolResult;
10
11/// A trait for protocol initial states.
12pub trait InitialState {
13    /// Initializes the state given initialization data in `prologue`.
14    ///
15    /// Errors on invalid initialization data.
16    fn init(prologue: Option<Vec<u8>>) -> ProtocolResult<Self>
17    where
18        Self: Sized;
19}
20
21/// A state where a message must be written before transitioning to the next state.
22///
23/// `WriteState` can only be implemented once by every state type, implying that
24/// in any protocol party state, if a message is to be written, that message and
25/// the state the party is in after writing the message are uniquely determined.
26pub trait WriteState {
27    /// The uniquely determined state that is transitioned to after writing the message.
28    type NextState;
29    /// The type of the message that is being written.
30    type Message;
31    /// Produce the message to be written when transitioning to the next state.
32    fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>;
33}
34
35/// A state where a message must be read before transitioning to the next state.
36///
37/// A state type may implement `ReadState` multiple times, for different
38/// instances of `NextState`, allowing the following state to depend on the
39/// message that was received.
40pub trait ReadState<NextState> {
41    /// The type of message to be read.
42    type Message;
43
44    /// Generate the next state based on the current state and the received
45    /// message.
46    fn read(self, msg: Self::Message) -> ProtocolResult<NextState>;
47}
hax_lib_protocol/state_machine.rs

hax_lib_protocol/
state_machine.rs
