hibana 0.9.6

Choreography-derived runtime enforcement kernel for no_std Rust multiparty protocols
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

use super::TAP_EVENTS;

#[repr(u8)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub(super) enum HeadEra {
    Initial,
    Wrapped,
}

#[repr(C)]
#[derive(Clone, Copy)]
pub(super) struct RingState {
    write_index: u8,
    resident_len: u8,
    head_era: HeadEra,
}

impl RingState {
    pub(super) const EMPTY: Self = Self {
        write_index: 0,
        resident_len: 0,
        head_era: HeadEra::Initial,
    };

    #[inline(always)]
    pub(super) fn after_push(self, head: usize) -> Self {
        let write_index = if self.write_index as usize + 1 == TAP_EVENTS {
            0
        } else {
            self.write_index + 1
        };
        Self {
            write_index,
            resident_len: if self.resident_len as usize == TAP_EVENTS {
                self.resident_len
            } else {
                self.resident_len + 1
            },
            head_era: if head == usize::MAX {
                HeadEra::Wrapped
            } else {
                self.head_era
            },
        }
    }

    #[inline(always)]
    pub(super) fn oldest_index(self) -> u8 {
        ((self.write_index as usize + TAP_EVENTS - self.resident_len as usize) % TAP_EVENTS) as u8
    }

    #[inline(always)]
    pub(super) const fn write_index(self) -> u8 {
        self.write_index
    }

    #[inline(always)]
    pub(super) const fn resident_len(self) -> u8 {
        self.resident_len
    }

    #[inline(always)]
    pub(super) const fn head_era(self) -> HeadEra {
        self.head_era
    }
}

#[cfg(kani)]
mod kani {
    use super::{HeadEra, RingState, TAP_EVENTS};

    #[kani::proof]
    fn ring_state_step_preserves_the_exact_slot_domain() {
        let write_candidate: u8 = kani::any();
        let resident_candidate: u8 = kani::any();
        let write_index = if (write_candidate as usize) < TAP_EVENTS {
            write_candidate
        } else {
            0
        };
        let resident_len = if resident_candidate as usize <= TAP_EVENTS {
            resident_candidate
        } else {
            TAP_EVENTS as u8
        };
        let head_era = if kani::any() {
            HeadEra::Initial
        } else {
            HeadEra::Wrapped
        };
        let head: usize = kani::any();
        let state = RingState {
            write_index,
            resident_len,
            head_era,
        };

        let next = state.after_push(head);

        assert!((next.write_index as usize) < TAP_EVENTS);
        assert!(next.resident_len as usize <= TAP_EVENTS);
        assert!((next.oldest_index() as usize) < TAP_EVENTS);
        assert!(!matches!(head_era, HeadEra::Wrapped) || matches!(next.head_era, HeadEra::Wrapped));
        assert!(head != usize::MAX || matches!(next.head_era, HeadEra::Wrapped));
    }
}