pipecircuit 0.0.18

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

use super::change::{ProjectionChange, projection_change};

#[kani::proof]
fn projection_change_reconstructs_the_exact_new_state() {
    let before: Option<(u64, u8)> = kani::any();
    let after: Option<(u64, u8)> = kani::any();
    let change = projection_change(
        before
            .as_ref()
            .map(|(incarnation, value)| (*incarnation, value)),
        after
            .as_ref()
            .map(|(incarnation, value)| (*incarnation, value)),
    );
    let reconstructed = match change {
        ProjectionChange::Unchanged => {
            assert!(before == after);
            kani::cover!(true, "observed.change_unchanged");
            before
        }
        ProjectionChange::Upsert => {
            assert!(after.is_some() && before != after);
            kani::cover!(true, "observed.change_upsert");
            after
        }
        ProjectionChange::Remove { incarnation } => {
            assert!(matches!(before, Some((old, _)) if old == incarnation));
            assert!(after.is_none());
            kani::cover!(true, "observed.change_remove");
            None
        }
    };
    assert!(reconstructed == after);
}