elicitation_kani 0.8.3

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

//! Kani proofs for string contract types.

use elicitation::StringNonEmpty;

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

#[kani::proof]
pub fn verify_string_non_empty() {
    // Reduced buffer size for Kani
    const MAX_LEN: usize = 2;

    // Empty string case
    let empty = String::new();
    let result = StringNonEmpty::<MAX_LEN>::new(empty);
    assert!(result.is_err(), "Construction rejects empty string");

    // Non-empty string case
    let non_empty = String::from("a");
    let result = StringNonEmpty::<MAX_LEN>::new(non_empty);

    // Verify construction doesn't panic and respects invariant
    if let Ok(contract) = result {
        assert!(!contract.is_empty(), "Non-empty invariant");
    }
}

// ============================================================================
// Bool Contract Proofs