elicitation_kani 0.8.2

Kani formal verification proofs for elicitation contracts
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

//! Kani proofs for integer contract types.

use elicitation::{I8NonNegative, I8Positive, I16Positive, U8NonZero, U16NonZero};

// ============================================================================
// Integer Contract Proofs
// ============================================================================

#[kani::proof]
fn verify_i8_positive() {
    let value: i8 = kani::any();

    match I8Positive::new(value) {
        Ok(positive) => {
            // If construction succeeds, value must be positive
            assert!(value > 0, "I8Positive invariant: value > 0");
            assert!(positive.get() > 0, "get() returns positive value");
            assert!(
                positive.into_inner() > 0,
                "into_inner() returns positive value"
            );
        }
        Err(_) => {
            // If construction fails, value must be <= 0
            assert!(value <= 0, "Construction fails when value <= 0");
        }
    }
}

#[kani::proof]
fn verify_i8_non_negative() {
    let value: i8 = kani::any();

    match I8NonNegative::new(value) {
        Ok(non_neg) => {
            assert!(value >= 0, "I8NonNegative invariant: value >= 0");
            let val: i8 = non_neg.get();
            assert!(val >= 0, "get() returns non-negative value");
        }
        Err(_) => {
            assert!(value < 0, "Construction fails when value < 0");
        }
    }
}

#[kani::proof]
fn verify_u8_non_zero() {
    let value: u8 = kani::any();

    match U8NonZero::new(value) {
        Ok(non_zero) => {
            assert!(value != 0, "U8NonZero invariant: value != 0");
            let val: u8 = non_zero.get();
            assert!(val != 0, "get() returns non-zero value");
        }
        Err(_) => {
            assert!(value == 0, "Construction fails when value == 0");
        }
    }
}

#[kani::proof]
fn verify_i16_positive() {
    let value: i16 = kani::any();

    match I16Positive::new(value) {
        Ok(positive) => {
            assert!(value > 0, "I16Positive invariant: value > 0");
            assert!(positive.get() > 0, "get() preserves invariant");
        }
        Err(_) => {
            assert!(value <= 0, "Construction rejects non-positive");
        }
    }
}

#[kani::proof]
fn verify_u16_non_zero() {
    let value: u16 = kani::any();

    match U16NonZero::new(value) {
        Ok(non_zero) => {
            assert!(value != 0, "U16NonZero invariant");
            let val: u16 = non_zero.get();
            assert!(val != 0, "get() preserves invariant");
        }
        Err(_) => {
            assert!(value == 0, "Construction rejects zero");
        }
    }
}

// ============================================================================