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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51

//! Kani proofs for winit elicitation support.
//!
//! Available with the `winit-types` feature.

/// `WinitPhysicalSize` stores width and height without modification.
#[cfg(feature = "winit-types")]
#[kani::proof]
fn verify_winit_physical_size_fields() {
    let size = elicitation::WinitPhysicalSize {
        width: 1920_u32,
        height: 1080_u32,
    };
    assert!(size.width == 1920_u32, "width preserved");
    assert!(size.height == 1080_u32, "height preserved");
}

/// `WinitLogicalSize` stores width and height without modification.
#[cfg(feature = "winit-types")]
#[kani::proof]
fn verify_winit_logical_size_fields() {
    let size = elicitation::WinitLogicalSize {
        width: 1280_f64,
        height: 720_f64,
    };
    assert!(size.width == 1280_f64, "width preserved");
    assert!(size.height == 720_f64, "height preserved");
}

/// `WinitLogicalPosition` stores x and y coordinates without modification.
#[cfg(feature = "winit-types")]
#[kani::proof]
fn verify_winit_logical_position_fields() {
    let pos = elicitation::WinitLogicalPosition {
        x: 100_f64,
        y: 200_f64,
    };
    assert!(pos.x == 100_f64, "x preserved");
    assert!(pos.y == 200_f64, "y preserved");
}

/// Zero-sized `WinitPhysicalSize` is representable.
#[cfg(feature = "winit-types")]
#[kani::proof]
fn verify_winit_physical_size_zero() {
    let size = elicitation::WinitPhysicalSize {
        width: 0_u32,
        height: 0_u32,
    };
    assert!(size.width == 0_u32, "zero width");
    assert!(size.height == 0_u32, "zero height");
}