pipecircuit 0.0.9

Correct. Robust. Fast. Portable.
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

use core::num::NonZeroU64;

use crate::{StateMachine, StepInputOf};

use super::{
    ContinuationCompletion, ContinuationCoordinator, ContinuationIds, ContinuationInput,
    ContinuationNotPending, ContinuationSettlement, ContinuationSlot, NextContinuationId, Owed,
    PositiveDuration,
};

struct Machine;
struct Completed;
struct Expired;

impl StateMachine for Machine {}

impl StepInputOf<Machine> for ContinuationInput<Machine, Completed, Expired> {
    type Outcome = ();

    fn step(self, _machine: &mut Machine) -> Self::Outcome {
        match self.settlement() {
            ContinuationSettlement::Completed(Completed)
            | ContinuationSettlement::Expired(Expired) => {}
        }
    }
}

#[kani::proof]
fn issued_identifiers_are_nonzero_and_advance_without_wrapping() {
    let raw = kani::any::<u64>();
    if let Some(current) = NonZeroU64::new(raw) {
        let mut ids = ContinuationIds::<()> {
            next: NextContinuationId::Available(current),
            machine: core::marker::PhantomData,
        };
        let issued = ids.try_issue();
        assert!(issued.is_ok());
        assert_eq!(issued.ok().map(|id| id.value()), Some(current));
        match current.get().checked_add(1).and_then(NonZeroU64::new) {
            Some(expected) => assert!(matches!(
                ids.next,
                NextContinuationId::Available(next) if next == expected
            )),
            None => assert!(matches!(ids.next, NextContinuationId::Exhausted)),
        }
    }
}

#[kani::proof]
fn exactly_one_of_completion_or_expiry_can_settle_an_admitted_continuation() {
    let mut coordinator = ContinuationCoordinator::new();
    let mut slot = ContinuationSlot::new();
    let owed = Owed::<Machine, Completed, Expired>::wait(
        Expired,
        PositiveDuration::from_nanoseconds(NonZeroU64::MIN),
    );
    let parked = coordinator.try_admit(owed, &mut slot).ok();
    assert!(parked.is_some());
    let id = slot.pending_id();
    assert!(id.is_some());

    if let Some(id) = id {
        if kani::any::<bool>() {
            assert!(
                slot.try_complete(ContinuationCompletion::new(id, Completed))
                    .is_ok()
            );
            assert!(matches!(
                slot.try_expire(id),
                Err(ContinuationNotPending::Vacant { .. })
            ));
        } else {
            assert!(slot.try_expire(id).is_ok());
            assert!(matches!(
                slot.try_complete(ContinuationCompletion::new(id, Completed)),
                Err(_)
            ));
        }
    }
}