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
//! Kani proof harnesses for contract types.
//!
//! This module contains formal verification proofs using the Kani model checker.
//! Each proof harness verifies that contract invariants hold by construction.
//!
//! # Global Configuration
//!
//! Run with global unwind bound to prevent memchr infinite loops:
//! ```bash
//! cargo kani --package elicitation --features verify-kani -- --default-unwind 20
//! ```
//!
//!
//! # Running Proofs
//!
//! ```bash
//! # Run all Kani proofs
//! cargo kani --package elicitation --features verify-kani -- --default-unwind 20
//!
//! # Run specific proof
//! cargo kani --package elicitation --features verify-kani --harness verify_i8_positive
//! ```
//!
//! # Proof Strategy
//!
//! For each contract type T, we prove:
//! 1. **Construction Safety**: `T::new(x)` succeeds ⟹ invariant holds
//! 2. **Invalid Rejection**: `T::new(x)` fails ⟹ invariant violated
//! 3. **Accessor Correctness**: `t.get()` returns validated value
//! 4. **Unwrap Correctness**: `t.into_inner()` returns validated value
#![cfg(kani)]
mod bools;
mod chars;
mod collections;
mod durations;
mod errors;
mod floats;
mod integers;
mod ipaddr_bytes;
mod macaddr;
mod mechanisms;
mod networks;
mod regexbytes;
mod socketaddr;
mod strings;
mod systemtime;
mod unit;
mod urlbytes;
mod utf8;
#[cfg(unix)]
mod pathbytes;
#[cfg(feature = "uuid")]
mod uuid_bytes;
#[cfg(feature = "url")]
mod urls;
#[cfg(feature = "regex")]
mod regexes;
#[cfg(feature = "chrono")]
mod datetime_chrono;
#[cfg(feature = "time")]
mod datetime_time;
#[cfg(feature = "jiff")]
mod datetime_jiff;