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

use super::{FrontierProgressCandidate, LaneOfferState, OfferEntryObservedState};

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) struct OfferEntryEvidence {
    bits: u8,
}

impl OfferEntryEvidence {
    pub(crate) const FLAG_READY_ARM: u8 = 1;
    pub(crate) const FLAG_INGRESS_READY: u8 = 1 << 1;

    #[inline]
    pub(crate) const fn empty() -> Self {
        Self { bits: 0 }
    }

    #[inline]
    pub(crate) const fn with_ready_arm(self) -> Self {
        Self {
            bits: self.bits | Self::FLAG_READY_ARM,
        }
    }

    #[inline]
    pub(crate) const fn with_ingress_ready(self) -> Self {
        Self {
            bits: self.bits | Self::FLAG_INGRESS_READY,
        }
    }

    #[inline]
    pub(crate) const fn has_ready_arm(self) -> bool {
        (self.bits & Self::FLAG_READY_ARM) != 0
    }

    #[inline]
    pub(crate) const fn ingress_ready(self) -> bool {
        (self.bits & Self::FLAG_INGRESS_READY) != 0
    }
}

#[inline]
pub(crate) fn candidate_has_progress_evidence(evidence: OfferEntryEvidence) -> bool {
    evidence.has_ready_arm() || evidence.ingress_ready()
}

#[inline]
pub(crate) fn offer_entry_observed_state(
    info: LaneOfferState,
    evidence: OfferEntryEvidence,
) -> OfferEntryObservedState {
    let has_progress_evidence = candidate_has_progress_evidence(evidence);
    let ready = has_progress_evidence || info.intrinsic_ready();
    let mut flags = 0u8;
    if info.is_controller() {
        flags |= OfferEntryObservedState::FLAG_CONTROLLER;
    }
    if info.is_dynamic() {
        flags |= OfferEntryObservedState::FLAG_DYNAMIC;
    }
    if has_progress_evidence {
        flags |= OfferEntryObservedState::FLAG_PROGRESS;
    }
    if evidence.has_ready_arm() {
        flags |= OfferEntryObservedState::FLAG_READY_ARM;
    }
    if ready {
        flags |= OfferEntryObservedState::FLAG_READY;
    }
    OfferEntryObservedState {
        key: crate::invariant_some(info.key()),
        frontier_mask: info.frontier.bit(),
        flags,
    }
}

#[inline]
pub(crate) fn offer_entry_frontier_progress_candidate(
    info: LaneOfferState,
    observed: OfferEntryObservedState,
) -> Option<FrontierProgressCandidate> {
    if Some(observed.key) != info.key() {
        crate::invariant();
    }
    if !observed.has_progress_evidence() {
        return None;
    }
    if !observed.is_ready() {
        crate::invariant();
    }
    Some(FrontierProgressCandidate {
        scope_id: info.scope,
        entry: observed.key.entry(),
        parallel_root: info.parallel_root,
        frontier: info.frontier,
    })
}

#[cfg(kani)]
mod kani;