rootle-kernel 0.13.1

Allocation-free request lifetime decisions extracted to Lean with Charon and Aeneas
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

//! A request accepts partial replies until exactly one terminal reply lands.

#[derive(Clone, Copy)]
pub enum Phase {
    Idle,
    Loading,
    Ready,
    Failed,
}

#[derive(Clone, Copy)]
pub enum Reply {
    Partial,
    Complete,
    Failed,
}

/// Decide acceptance and the next phase in one operation. Rejection leaves
/// the caller's state untouched. Payload identity is additionally checked by
/// the adapter; generation equality alone must never override that check.
pub fn accept(current: u64, phase: Phase, incoming: u64, reply: Reply) -> Option<Phase> {
    if current != incoming {
        return None;
    }
    match phase {
        Phase::Loading => Some(match reply {
            Reply::Partial => Phase::Loading,
            Reply::Complete => Phase::Ready,
            Reply::Failed => Phase::Failed,
        }),
        Phase::Idle | Phase::Ready | Phase::Failed => None,
    }
}