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
58
59
60
61
62
63
64
65
66
67
68

use super::*;

#[kani::proof]
#[kani::unwind(5)]
fn pending_routes_initialization_is_empty_and_bounded() {
    let pending = PendingRoutes::<u8, 3>::new();
    assert_eq!(pending.len(), 0);
    assert!(pending.slots.iter().all(Option::is_none));
}

#[kani::proof]
#[kani::unwind(6)]
fn pending_routes_preserves_dense_ownership_and_refuses_whole_fanout() {
    let length: usize = kani::any();
    kani::assume(length <= 3);
    let mut pending = PendingRoutes::<u8, 3>::new();
    for slot in pending.slots.iter_mut().take(length) {
        *slot = Some(kani::any());
    }
    pending.length = length;
    let before = pending.slots;
    let operation: u8 = kani::any();
    kani::assume(operation <= 5);
    match operation {
        0 => {
            let popped = pending.pop();
            assert_eq!(popped.is_some(), length > 0);
            assert_eq!(
                pending.len().checked_add(usize::from(popped.is_some())),
                Some(length)
            );
        }
        1..=5 => {
            let route = match operation {
                1 => Route::None,
                2 => Route::One(kani::any()),
                3 => Route::Two(kani::any()),
                4 => Route::Three(kani::any()),
                _ => Route::Four(kani::any()),
            };
            let count = route.len();
            let expected_refusal = length
                .checked_add(count.saturating_sub(1))
                .is_none_or(|n| n > 3);
            match pending.admit(route) {
                Ok(first) => {
                    assert!(!expected_refusal);
                    assert_eq!(first.is_some(), count > 0);
                    assert_eq!(
                        pending.len(),
                        length.saturating_add(count.saturating_sub(1))
                    );
                }
                Err(rejected) => {
                    assert!(expected_refusal);
                    assert_eq!(rejected.len(), count);
                    assert_eq!(pending.slots, before);
                    assert_eq!(pending.len(), length);
                }
            }
        }
        _ => {}
    }
    assert!(pending.len() <= pending.capacity());
    for (index, slot) in pending.slots.iter().enumerate() {
        assert_eq!(slot.is_some(), index < pending.len());
    }
}