elicitation_kani 0.11.0

Kani model-checking proofs for elicitation contract types
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

//! Kani proofs for bool contract types.

use elicitation::{BoolFalse, BoolTrue};

// Bool Contract Proofs
// ============================================================================

#[kani::proof]
pub fn verify_bool_true() {
    let value: bool = kani::any();

    match BoolTrue::new(value) {
        Ok(bool_true) => {
            assert!(value == true, "BoolTrue invariant: value is true");
            assert!(bool_true.get() == true, "get() returns true");
        }
        Err(_) => {
            assert!(value == false, "Construction rejects false");
        }
    }
}

#[kani::proof]
pub fn verify_bool_false() {
    let value: bool = kani::any();

    match BoolFalse::new(value) {
        Ok(bool_false) => {
            assert!(value == false, "BoolFalse invariant: value is false");
            let val: bool = bool_false.get();
            assert!(val == false, "get() returns false");
        }
        Err(_) => {
            assert!(value == true, "Construction rejects true");
        }
    }
}

// ============================================================================
// Char Contract Proofs