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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
//! Kani proofs for network and filesystem contract types.
use elicitation::{
IpPrivate, IpPublic, Ipv4Loopback, Ipv6Loopback, PathBufExists, PathBufIsDir, PathBufIsFile,
PathBufReadable,
};
#[cfg(feature = "uuid")]
use elicitation::{UuidNonNil, UuidV4};
// ============================================================================
// Network Proofs
// ----------------------------------------------------------------------------
#[kani::proof]
fn verify_ip_private() {
// Note: Kani struggles with complex IpAddr construction
// We prove the logic, assuming valid IpAddr input
use std::net::IpAddr;
// Test with concrete private IP (symbolic execution of IpAddr is complex)
let private_v4 = IpAddr::from([192, 168, 1, 1]);
let result = IpPrivate::new(private_v4);
assert!(result.is_ok(), "Private IPv4 accepted");
let public_v4 = IpAddr::from([8, 8, 8, 8]);
let result = IpPrivate::new(public_v4);
assert!(result.is_err(), "Public IPv4 rejected");
}
#[kani::proof]
fn verify_ip_public() {
use std::net::IpAddr;
let public_v4 = IpAddr::from([8, 8, 8, 8]);
let result = IpPublic::new(public_v4);
assert!(result.is_ok(), "Public IPv4 accepted");
let private_v4 = IpAddr::from([192, 168, 1, 1]);
let result = IpPublic::new(private_v4);
assert!(result.is_err(), "Private IPv4 rejected");
}
#[kani::proof]
fn verify_ipv4_loopback() {
use std::net::Ipv4Addr;
let loopback = Ipv4Addr::new(127, 0, 0, 1);
let result = Ipv4Loopback::new(loopback);
assert!(result.is_ok(), "Loopback accepted");
let not_loopback = Ipv4Addr::new(192, 168, 1, 1);
let result = Ipv4Loopback::new(not_loopback);
assert!(result.is_err(), "Non-loopback rejected");
}
#[kani::proof]
fn verify_ipv6_loopback() {
use std::net::Ipv6Addr;
let loopback = Ipv6Addr::new(0, 0, 0, 0, 0, 0, 0, 1);
let result = Ipv6Loopback::new(loopback);
assert!(result.is_ok(), "IPv6 loopback accepted");
let not_loopback = Ipv6Addr::new(0x2001, 0x0db8, 0, 0, 0, 0, 0, 1);
let result = Ipv6Loopback::new(not_loopback);
assert!(result.is_err(), "Non-loopback rejected");
}
// ----------------------------------------------------------------------------
// UUID Proofs
// ----------------------------------------------------------------------------
#[cfg(feature = "uuid")]
#[kani::proof]
fn verify_uuid_v4() {
use uuid::Uuid;
// Use from_bytes to avoid parse_str string parsing loops
let v4_bytes = [
0x55, 0x0e, 0x84, 0x00, 0xe2, 0x9b, 0x41, 0xd4, 0xa7, 0x16, 0x44, 0x66, 0x55, 0x44, 0x00,
0x00,
];
let v4_uuid = Uuid::from_bytes(v4_bytes);
let _result = UuidV4::new(v4_uuid);
// Note: from_bytes doesn't validate version bits
}
#[cfg(feature = "uuid")]
#[kani::proof]
fn verify_uuid_non_nil() {
use uuid::Uuid;
let nil_uuid = Uuid::nil();
let result = UuidNonNil::new(nil_uuid);
assert!(result.is_err(), "Nil UUID rejected");
// Use from_bytes to avoid parse_str
let non_nil_bytes = [
0x55, 0x0e, 0x84, 0x00, 0xe2, 0x9b, 0x41, 0xd4, 0xa7, 0x16, 0x44, 0x66, 0x55, 0x44, 0x00,
0x01,
];
let non_nil = Uuid::from_bytes(non_nil_bytes);
let result = UuidNonNil::new(non_nil);
assert!(result.is_ok(), "Non-nil UUID accepted");
}
// ----------------------------------------------------------------------------
// PathBuf Proofs (Runtime validation - limited symbolic execution)
// ----------------------------------------------------------------------------
#[kani::proof]
fn verify_pathbuf_contracts() {
// PathBuf validation requires filesystem access which Kani cannot verify
// These contracts test filesystem state (exists, readable, is_dir, is_file)
// which requires actual I/O operations (statx syscall) unsupported by Kani.
//
// Verification strategy: Trust stdlib's filesystem operations, verify only
// that our wrapper types correctly use Result<T, E> and appropriate error types.
//
// These contracts are validated in integration tests with real filesystem state.
// This proof just verifies the types exist and have the expected API
// without calling filesystem operations
use elicitation::{PathBufExists, PathBufIsDir, PathBufIsFile, PathBufReadable};
use std::path::PathBuf;
let _path = PathBuf::from("/test");
// Type checking only - verify API surface exists
// Cannot construct these in kani mode without filesystem access
}
// ============================================================================
// Phase 4: Collection Type Proofs