pipecircuit 0.0.23

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

use super::*;
use crate::storage::warp_table::Capacity;
use core::num::{NonZeroU32, NonZeroU64};

#[kani::proof]
fn session_generation_never_reuses_or_accepts_old_carrier_events() {
    let mut client =
        SubscribedView::<u32, u32>::new(ContinuousView::new(Capacity::new(NonZeroU32::MIN)));
    assert_eq!(client.generation, 0);
    assert_eq!(client.phase, Phase::Disconnected);
    assert_eq!(client.view().connection(), ViewConnection::Disconnected);
    let previous: u64 = kani::any();
    client.generation = previous;
    let request = RequestId(NonZeroU64::MIN);
    let result = client.subscribe::<(), (), _>(request, 7_u8, Guarantee::Accepted);
    if previous == u64::MAX {
        assert!(matches!(result, Err((7, Error::Exhausted))));
        assert_eq!(client.generation, previous);
        assert_eq!(client.phase, Phase::Disconnected);
        kani::cover!(true, "subscription.exhaustion");
    } else {
        assert!(result.is_ok());
        if let Ok(SubscriptionStart {
            session: current, ..
        }) = result
        {
            assert!(current.0 > previous);
            let old: u64 = kani::any();
            kani::assume(old <= previous);
            assert!(matches!(
                client.disconnect(SubscriptionSession(old)),
                Err(SubscriptionReceiveError::WrongSession)
            ));
            let reply: ContinuousReply<(), (), (), u32, u32> =
                ContinuousReply::SubscriptionRefused {
                    id: request,
                    reason: SubscriptionRefusal::Full,
                };
            assert!(matches!(
                client.step(ReceiveSubscription {
                    session: SubscriptionSession(old),
                    reply: &reply
                }),
                Err(SubscriptionReceiveError::WrongSession)
            ));
            assert_eq!(client.phase, Phase::Subscribing(request));
            assert!(matches!(
                client.subscribe::<(), (), _>(request, 9_u8, Guarantee::Accepted),
                Err((9, Error::Busy))
            ));
            assert!(client.disconnect(current).is_ok());
            assert_eq!(client.phase, Phase::Disconnected);
            assert_eq!(client.generation, current.0);
            kani::cover!(true, "subscription.old_carrier_refused");
        }
    }
}