elicitation_kani 0.11.1

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

//! Kani proofs for unit type ().

// Unit Type Proofs
// ============================================================================

#[kani::proof]
pub fn verify_unit_type_unique_value() {
    // Unit type has exactly one value
    let unit1: () = ();
    let unit2: () = ();

    assert!(unit1 == unit2, "All unit values are equal");
}

#[kani::proof]
pub fn verify_unit_type_zero_sized() {
    let unit: () = ();

    assert!(std::mem::size_of_val(&unit) == 0, "Unit type has zero size");
}

#[kani::proof]
pub fn verify_unit_type_default() {
    let unit: () = Default::default();

    assert!(unit == (), "Default::default() returns ()");
}