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

use super::*;

#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)]
struct Revision(u8);

impl SynchronizedViewRevision for Revision {
    type ChangeId = u8;

    fn changed_through(change_id: Self::ChangeId) -> Self {
        Self(change_id)
    }

    fn next_change_id(self) -> Option<Self::ChangeId> {
        self.0.checked_add(1)
    }
}

#[kani::proof]
fn change_classification_is_exact() {
    let synchronized_through = Revision(kani::any());
    let change_id = kani::any();
    let mut view = SynchronizedView::new(Revision(0));
    let _ = view.apply_snapshot(synchronized_through, ());

    match view.apply_change(change_id, |_| Ok::<(), ()>(()), |_, _| Ok(()), |_, ()| {}) {
        ApplySynchronizedViewChangeOutcome::Applied { through } => {
            assert!(synchronized_through.next_change_id() == Some(change_id));
            assert!(through == Revision(change_id));
        }
        ApplySynchronizedViewChangeOutcome::Stale {
            change_through,
            synchronized_through,
        } => {
            assert!(change_through <= synchronized_through);
        }
        ApplySynchronizedViewChangeOutcome::SnapshotRequired {
            observed_through,
            reason:
                SynchronizedViewSnapshotRequiredReason::ChangeGap {
                    synchronized_through,
                },
        } => {
            assert!(change_id > synchronized_through.0);
            assert!(synchronized_through.next_change_id() != Some(change_id));
            assert!(observed_through == Revision(change_id));
        }
        ApplySynchronizedViewChangeOutcome::SnapshotRequired { .. } => unreachable!(),
    }
}