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

mod definition;
use definition::define_public_operation_kernel;

define_public_operation_kernel! {
    phases {
        Idle,
        Poisoned,
        Send,
        Recv,
        Offer,
        RouteBranch,
        RestoredRouteBranch,
        BranchRecv,
        BranchSend,
    }
    edges {
        BeginOffer => (Idle, Offer),
        ResumeOffer => (RestoredRouteBranch, Offer),
        PublishRouteBranch => (Offer, RouteBranch),
        FinishOffer => (Offer, Idle),
        ParkOffer => (Offer, RestoredRouteBranch),
        ParkRouteBranch => (RouteBranch, RestoredRouteBranch),
        BeginSend => (Idle, Send),
        BeginBranchSend => (RouteBranch, BranchSend),
        FinishSend => (Send, Idle),
        FinishBranchSend => (BranchSend, Idle),
        ParkBranchSend => (BranchSend, RestoredRouteBranch),
        BeginRecv => (Idle, Recv),
        BeginBranchRecv => (RouteBranch, BranchRecv),
        FinishRecv => (Recv, Idle),
        FinishBranchRecv => (BranchRecv, Idle),
        ParkBranchRecv => (BranchRecv, RestoredRouteBranch),
    }
}

impl PublicActiveOp {
    #[inline(always)]
    pub(in crate::endpoint::kernel) fn transition(self, edge: PublicOpEdge) -> PublicOpTransition {
        if self == Self::Poisoned {
            PublicOpTransition::new(PublicOpLease::Faulted, Self::Poisoned)
        } else if self == edge.expected() {
            PublicOpTransition::new(PublicOpLease::Held, edge.next())
        } else {
            PublicOpTransition::new(PublicOpLease::Rejected, Self::Poisoned)
        }
    }

    #[inline(always)]
    pub(in crate::endpoint::kernel) fn clear_if_current(self, expected: Self) -> Self {
        if self == expected { Self::Idle } else { self }
    }

    #[inline(always)]
    pub(in crate::endpoint::kernel) const fn clear_terminal(self) -> Self {
        Self::Idle
    }

    #[inline(always)]
    pub(in crate::endpoint::kernel) const fn fault(self) -> Self {
        Self::Poisoned
    }
}

#[repr(u8)]
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) enum PublicOpLease {
    Rejected = 0,
    Held = 1,
    Faulted = 2,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(in crate::endpoint::kernel) struct PublicOpTransition {
    lease: PublicOpLease,
    phase: PublicActiveOp,
}

impl PublicOpTransition {
    #[inline(always)]
    const fn new(lease: PublicOpLease, phase: PublicActiveOp) -> Self {
        Self { lease, phase }
    }

    #[inline(always)]
    pub(in crate::endpoint::kernel) const fn lease(self) -> PublicOpLease {
        self.lease
    }

    #[inline(always)]
    pub(in crate::endpoint::kernel) const fn phase(self) -> PublicActiveOp {
        self.phase
    }
}

#[cfg(kani)]
mod kani;

#[cfg(all(test, hibana_repo_tests))]
mod tests;