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
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

//! Kani proofs for WKT elicitation wrappers.
//!
//! Available with the `wkt-types` feature.

/// WktString delegates parsing to the upstream `wkt` crate.
#[cfg(feature = "wkt-types")]
#[kani::proof]
fn verify_wkt_string_trusted() {
    kani::assume(true);
    assert!(true, "WktString parsing is trusted third-party logic");
}

/// WktCoord preserves all fields through wrapper conversion roundtrip.
#[cfg(feature = "wkt-types")]
#[kani::proof]
fn verify_wkt_coord_from_roundtrip() {
    let x: f64 = kani::any();
    let y: f64 = kani::any();
    let z: Option<f64> = kani::any();
    let m: Option<f64> = kani::any();

    kani::assume(x.is_finite() && y.is_finite());
    kani::assume(z.is_none_or(f64::is_finite));
    kani::assume(m.is_none_or(f64::is_finite));

    let original = wkt::types::Coord { x, y, z, m };
    let wrapper = elicitation::WktCoord::from(original);
    let restored: wkt::types::Coord<f64> = wrapper.into();

    assert!(restored.x == x, "Coord x preserved");
    assert!(restored.y == y, "Coord y preserved");
    assert!(restored.z == z, "Coord z preserved");
    assert!(restored.m == m, "Coord m preserved");
}

/// WktCoord exposes the same field values as the wrapped coordinate.
#[cfg(feature = "wkt-types")]
#[kani::proof]
fn verify_wkt_coord_wrapper_fields() {
    let x: f64 = kani::any();
    let y: f64 = kani::any();
    let z: Option<f64> = kani::any();
    let m: Option<f64> = kani::any();

    kani::assume(x.is_finite() && y.is_finite());
    kani::assume(z.is_none_or(f64::is_finite));
    kani::assume(m.is_none_or(f64::is_finite));

    let original = wkt::types::Coord { x, y, z, m };
    let wrapper = elicitation::WktCoord::from(original);

    assert!(wrapper.x == x, "wrapper.x matches");
    assert!(wrapper.y == y, "wrapper.y matches");
    assert!(wrapper.z == z, "wrapper.z matches");
    assert!(wrapper.m == m, "wrapper.m matches");
}

/// WktPoint preserves emptiness through wrapper conversion.
#[cfg(feature = "wkt-types")]
#[kani::proof]
fn verify_wkt_point_empty_roundtrip() {
    let original = wkt::types::Point::<f64>::new(None, wkt::types::Dimension::XY);
    let wrapper = elicitation::WktPoint::from(original);
    let coord_is_none = wrapper.coord.is_none();
    let restored: wkt::types::Point<f64> = wrapper.into();

    assert!(coord_is_none, "wrapper preserves emptiness");
    assert!(restored.coord().is_none(), "roundtrip preserves emptiness");
}

/// WktGeom preserves the Point variant through conversion.
#[cfg(feature = "wkt-types")]
#[kani::proof]
fn verify_wkt_geom_point_variant() {
    let x: f64 = kani::any();
    let y: f64 = kani::any();

    kani::assume(x.is_finite() && y.is_finite());

    let original = wkt::Wkt::Point(wkt::types::Point::from_coord(wkt::types::Coord {
        x,
        y,
        z: None,
        m: None,
    }));
    let wrapper = elicitation::WktGeom::from(original);

    assert!(
        matches!(wrapper, elicitation::WktGeom::Point(_)),
        "Point variant preserved"
    );
}