elicitation_kani 0.11.0

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

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

/// `ProjArea::new` stores all four boundary values without modification.
#[cfg(feature = "proj-types")]
#[kani::proof]
fn verify_proj_area_new_fields() {
    let area = elicitation::ProjArea::new(1.0_f64, 2.0_f64, 3.0_f64, 4.0_f64);
    assert!(area.west == 1.0_f64, "west preserved");
    assert!(area.south == 2.0_f64, "south preserved");
    assert!(area.east == 3.0_f64, "east preserved");
    assert!(area.north == 4.0_f64, "north preserved");
}

/// `ProjArea` round-trips through `proj::Area` without losing any boundary value.
#[cfg(feature = "proj-types")]
#[kani::proof]
fn verify_proj_area_roundtrip() {
    let area = elicitation::ProjArea::new(-10.0_f64, -20.0_f64, 10.0_f64, 20.0_f64);
    let inner: proj::Area = area.into();
    let roundtrip = elicitation::ProjArea::from(inner);
    assert!(roundtrip.west == -10.0_f64, "west roundtrip");
    assert!(roundtrip.south == -20.0_f64, "south roundtrip");
    assert!(roundtrip.east == 10.0_f64, "east roundtrip");
    assert!(roundtrip.north == 20.0_f64, "north roundtrip");
}

/// Antimeridian-crossing areas are stored correctly (west > east is valid).
#[cfg(feature = "proj-types")]
#[kani::proof]
fn verify_proj_area_antimeridian() {
    let area = elicitation::ProjArea::new(170.0_f64, -10.0_f64, -170.0_f64, 10.0_f64);
    assert!(area.west > area.east, "antimeridian crossing: west > east");
}