elicitation_kani 0.8.2

Kani formal verification proofs for elicitation contracts
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

//! Kani proofs for float contract types.

use elicitation::{F32Finite, F64Positive};

// ============================================================================
// Float Contract Proofs
// ============================================================================

#[kani::proof]
pub fn verify_f32_finite() {
    let value: f32 = kani::any();

    let _result = F32Finite::new(value);

    // Verify construction doesn't panic
    // Note: Can't assert on is_finite(), is_nan(), is_infinite() with symbolic floats
    // With symbolic validation, both Ok and Err are valid paths
}

#[kani::proof]
pub fn verify_f64_positive() {
    let value: f64 = kani::any();

    let _result = F64Positive::new(value);

    // Verify construction doesn't panic
    // Note: Can't assert on value > 0.0 or is_finite() with symbolic floats
    // With symbolic validation, all paths (Ok/Err) are valid
}

// ============================================================================
// String Contract Proofs