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

use super::*;

#[kani::proof]
#[kani::unwind(3)]
fn report_classification_and_capacity_preserve_exact_events() {
    let mut report = AppliedViewChanges {
        changes: Vec::with_capacity(1),
        maximum: 1,
    };
    let full: bool = kani::any();
    let id: u8 = kani::any();
    let existing = AppliedViewChange::Left { id };
    if full {
        report.changes.push(existing);
    }
    let before: Option<(u64, u8)> = kani::any();
    let after: (u64, u8) = kani::any();
    let result = report.compare_row(
        id,
        before.as_ref().map(|(identity, value)| (*identity, value)),
        (after.0, &after.1),
    );
    if before == Some(after) {
        assert!(result.is_ok());
        assert_eq!(report.changes.len(), usize::from(full));
        kani::cover!(true, "subscription.report_unchanged");
    } else if full {
        assert_eq!(result, Err(ViewApplyError::ReportCapacityExceeded));
        assert_eq!(report.changes.as_slice(), &[existing]);
        kani::cover!(true, "subscription.report_full");
    } else {
        assert!(result.is_ok());
        assert_eq!(report.changes.len(), 1);
        let actual = report.changes.first();
        match before {
            None => {
                assert_eq!(actual, Some(&AppliedViewChange::Entered { id }));
                kani::cover!(true, "subscription.report_entered");
            }
            Some((identity, _)) if identity != after.0 => {
                assert_eq!(actual, Some(&AppliedViewChange::Replaced { id }));
                kani::cover!(true, "subscription.report_replaced");
            }
            Some((identity, value)) => {
                assert_eq!(identity, after.0);
                assert_ne!(value, after.1);
                assert_eq!(actual, Some(&AppliedViewChange::Updated { id }));
                kani::cover!(true, "subscription.report_updated");
            }
        }
    }
    report.clear();
    assert!(report.as_slice().is_empty());
    assert_eq!(report.maximum, 1);
}