hibana 0.9.4

Session-typed choreographic programming for no_std Rust protocols, inspired by affine MPST
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

use super::{
    CursorEndpoint, OfferEntryPosition, OfferScopeSelection, RecvError, RecvResult, ScopeId,
    Transport,
};

impl<'r, const ROLE: u8, T> CursorEndpoint<'r, ROLE, T>
where
    T: Transport + 'r,
{
    pub(in crate::endpoint::kernel::offer) fn offer_scope_selection_for_scope_lane(
        &self,
        scope_id: ScopeId,
        current_idx: usize,
        offer_lane: u8,
    ) -> RecvResult<OfferScopeSelection> {
        self.offer_scope_selection_for_scope_lane_with_selected_arm(
            scope_id,
            current_idx,
            offer_lane,
            self.preview_live_selected_arm_for_scope(scope_id),
        )
    }

    pub(in crate::endpoint::kernel::offer) fn offer_scope_selection_for_scope_lane_with_selected_arm(
        &self,
        scope_id: ScopeId,
        current_idx: usize,
        offer_lane: u8,
        selected_arm: Option<u8>,
    ) -> RecvResult<OfferScopeSelection> {
        let lane_idx = usize::from(offer_lane);
        if lane_idx >= self.cursor.logical_lane_count() {
            return Err(RecvError::PhaseInvariant);
        }
        if !self
            .cursor
            .route_offer_entry_allows_current(scope_id, current_idx, selected_arm)
        {
            return Err(RecvError::PhaseInvariant);
        }
        let offer_lanes = self.offer_lane_set_for_scope(scope_id);
        if !offer_lanes.contains(lane_idx) {
            return Err(RecvError::PhaseInvariant);
        }
        let entry_position = if crate::invariant_some(
            self.cursor
                .route_offer_entry_cursor_position(scope_id, current_idx, selected_arm),
        )
        .is_at_entry()
        {
            OfferEntryPosition::RouteEntry
        } else {
            OfferEntryPosition::AfterRouteEntry
        };
        Ok(OfferScopeSelection {
            scope_id,
            frontier_parallel_root: CursorEndpoint::<ROLE, T>::parallel_scope_root(
                &self.cursor,
                scope_id,
            ),
            offer_lane,
            entry_position,
            observed_target: crate::global::typestate::StateIndex::ABSENT,
        })
    }
}