pipecircuit 0.0.23

Correct. Robust. Fast. Portable. Pick four.
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87

use super::Error;

/// Numbers are issued only from a durably reserved range. Restart abandons the
/// complete previous reservation, including numbers that might have escaped.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct RevisionClock {
    next: Option<u64>,
    reserved_through: u64,
}
impl RevisionClock {
    pub fn restart(previous_reservation: u64, reserved_through: u64) -> Result<Self, Error> {
        if previous_reservation == u64::MAX && reserved_through == u64::MAX {
            return Ok(Self {
                next: None,
                reserved_through,
            });
        }
        if reserved_through <= previous_reservation {
            return Err(Error::InvalidRecovery);
        }
        Ok(Self {
            next: previous_reservation.checked_add(1),
            reserved_through,
        })
    }
    pub const fn reserved_through(self) -> u64 {
        self.reserved_through
    }
    pub fn reserve(&mut self, through: u64) -> Result<(), Error> {
        if through <= self.reserved_through {
            return Err(Error::InvalidRecovery);
        }
        self.reserved_through = through;
        Ok(())
    }
    pub fn available(self) -> Result<u64, Error> {
        let next = self.next.ok_or(Error::Exhausted)?;
        if next > self.reserved_through {
            Err(Error::ReservationRequired)
        } else {
            Ok(next)
        }
    }
    pub fn issue(&mut self) -> Result<u64, Error> {
        let next = self.available()?;
        self.next = next.checked_add(1);
        Ok(next)
    }
}

#[cfg(kani)]
mod proofs {
    use super::*;
    #[kani::proof]
    fn reservation_never_reuses_an_issued_revision() {
        let previous: u64 = kani::any();
        let reserved: u64 = kani::any();
        if let Ok(mut clock) = RevisionClock::restart(previous, reserved) {
            assert!(clock.available().is_ok() || (previous == u64::MAX && reserved == u64::MAX));
            let before = clock;
            if let Ok(issued) = clock.issue() {
                assert!(issued > previous);
                assert!(issued <= reserved);
                kani::cover!(issued == u64::MAX, "persistent.revision_exhaustion");
                kani::cover!(issued < reserved, "persistent.reserved_capacity");
                match clock.available() {
                    Ok(next) => assert!(next > issued),
                    Err(error) => {
                        assert!(error == Error::Exhausted || error == Error::ReservationRequired)
                    }
                }
                let extension: u64 = kani::any();
                let result = clock.reserve(extension);
                if result.is_err() {
                    assert_eq!(clock.reserved_through(), reserved);
                }
                if let Ok(restarted) = RevisionClock::restart(before.reserved_through(), extension)
                {
                    if let Ok(next) = restarted.available() {
                        assert!(next > issued);
                        kani::cover!(next > issued, "persistent.restart_gap");
                    }
                }
            }
        }
    }
}