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
93
94
95
96
97

//! Kani proofs for WKB elicitation wrappers.
//!
//! Available with the `wkb-types` feature.

/// WkbEndianness preserves the upstream byte-order variant through roundtrip conversion.
#[cfg(feature = "wkb-types")]
#[kani::proof]
fn verify_wkb_endianness_roundtrip() {
    let original = if kani::any::<bool>() {
        wkb::Endianness::BigEndian
    } else {
        wkb::Endianness::LittleEndian
    };

    let wrapper = elicitation::WkbEndianness::from(original);
    let restored: wkb::Endianness = wrapper.into();

    assert!(restored == original, "Endianness roundtrip preserved");
}

/// WkbDimension preserves the upstream dimension variant through roundtrip conversion.
#[cfg(feature = "wkb-types")]
#[kani::proof]
fn verify_wkb_dimension_roundtrip() {
    let selector: u8 = kani::any();
    let original = match selector % 4 {
        0 => wkb::reader::Dimension::Xy,
        1 => wkb::reader::Dimension::Xyz,
        2 => wkb::reader::Dimension::Xym,
        _ => wkb::reader::Dimension::Xyzm,
    };

    let wrapper = elicitation::WkbDimension::from(original);
    let restored: wkb::reader::Dimension = wrapper.into();

    assert!(restored == original, "Dimension roundtrip preserved");
}

/// WkbGeometryType preserves supported upstream geometry variants through roundtrip conversion.
#[cfg(feature = "wkb-types")]
#[kani::proof]
fn verify_wkb_geometry_type_roundtrip() {
    let selector: u8 = kani::any();
    let original = match selector % 7 {
        0 => wkb::reader::GeometryType::Point,
        1 => wkb::reader::GeometryType::LineString,
        2 => wkb::reader::GeometryType::Polygon,
        3 => wkb::reader::GeometryType::MultiPoint,
        4 => wkb::reader::GeometryType::MultiLineString,
        5 => wkb::reader::GeometryType::MultiPolygon,
        _ => wkb::reader::GeometryType::GeometryCollection,
    };

    let wrapper = elicitation::WkbGeometryType::try_from(original).expect("supported variant");
    let restored: wkb::reader::GeometryType = wrapper.into();

    assert!(restored == original, "Geometry type roundtrip preserved");
}

/// WkbWriteOptions preserves its endianness field through roundtrip conversion.
#[cfg(feature = "wkb-types")]
#[kani::proof]
fn verify_wkb_write_options_roundtrip() {
    let original = wkb::writer::WriteOptions {
        endianness: if kani::any::<bool>() {
            wkb::Endianness::BigEndian
        } else {
            wkb::Endianness::LittleEndian
        },
    };

    let expected_endianness = original.endianness;
    let wrapper = elicitation::WkbWriteOptions::from(original);
    let restored: wkb::writer::WriteOptions = wrapper.into();

    assert!(
        restored.endianness == expected_endianness,
        "WriteOptions endianness preserved"
    );
}

/// WkbBytes parsing delegates to hex::decode and wkb::reader::read_wkb,
/// both of which are trusted third-party byte parsers with complex internal
/// state that causes CBMC path explosion.  Marker proof only.
#[cfg(feature = "wkb-types")]
#[kani::proof]
fn verify_wkb_bytes_known_point_metadata() {
    // WkbBytes::from_hex calls hex::decode + wkb::reader::read_wkb.
    // The metadata accessor methods (endianness, dimension, geometry_type)
    // also call read_wkb internally.  All are trusted third-party parsing
    // logic; our wrapper adds no additional logic around them.
    kani::assume(true);
    assert!(
        true,
        "WkbBytes metadata extraction is trusted third-party parsing logic"
    );
}