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
//! FJ-036: Kani bounded-model proofs for the `disk_budget` resource.
//!
//! Gated behind `#[cfg(kani)]`; normal builds ignore them.
//! Run with: `cargo kani --harness proof_disk_budget_hysteresis_total`.
//!
//! These prove the watermark algebra exhaustively over the whole u8 x u8 input
//! space, which is the part of this resource a unit test can only sample. The
//! deletion behaviour is proved by execution instead, in
//! `tests/falsification_disk_budget.rs` — a bounded model cannot say anything
//! useful about `rm -rf` on a real filesystem.
// ── Disk Budget Proofs (FJ-036 / disk-budget-v1) ──────────────────────
/// Contract `watermark_hysteresis`: no accepted budget can thrash.
///
/// For EVERY (high, target_free) pair in the u8 x u8 space, `DiskBudget::new`
/// either rejects it or returns a budget whose reclaim target sits strictly
/// below its trigger. A pass that satisfies its target therefore always clears
/// the alarm, so the reaper cannot re-trigger on the next tick forever.
#[cfg(kani)]
#[kani::proof]
fn proof_disk_budget_hysteresis_total() {
use super::types::DiskBudget;
let high: u8 = kani::any();
let target_free: u8 = kani::any();
// Target the PURE predicate, not `DiskBudget::new`.
//
// The constructor allocates several Strings (path, schedule, Vec), and
// modelling the allocator over a 65,536-point input space made this harness
// run past 10 minutes without terminating. An intractable proof is
// indistinguishable from no proof, and this one was cited as evidence in
// contracts/disk-budget-v1.yaml while never having been executed.
//
// The property being proved is integer algebra; it does not need a heap.
//
// Retargeting at `validate_hysteresis` was NOT enough — measured 2026-08-17
// at 48 GB RSS and still running at 48 minutes, because that function calls
// `format!` on its error path and CBMC models every path regardless of
// which one the property asserts on. `hysteresis_holds` is the same
// decision with the message rendering lifted into the caller.
if DiskBudget::hysteresis_holds(high, target_free) {
let target_used = 100u8.saturating_sub(target_free);
assert!(target_used < high);
}
}
/// Contract `watermark_hysteresis`: `target_used_pct` never underflows.
///
/// `100 - target_free_pct` is computed on u8. Any accepted budget must keep
/// `target_free_pct` in 1..=99, so the subtraction is total. An accepted
/// budget with target_free_pct > 100 would panic in release-with-overflow
/// checks and silently wrap otherwise.
#[cfg(kani)]
#[kani::proof]
fn proof_disk_budget_target_used_no_underflow() {
let target_free: u8 = kani::any();
kani::assume(target_free >= 1 && target_free <= 99);
// `target_used_pct()` is `100 - target_free_pct`. Accepted budgets constrain
// target_free_pct to 1..=99, so the subtraction is total. Proved on the
// integers directly — see the note in the harness above on why the
// constructor is not used here.
let used = 100u8 - target_free;
assert!(used <= 99);
assert!(used >= 1);
}
/// Contract `watermark_hysteresis`: the shipped defaults are themselves valid.
///
/// A default pair that violated hysteresis would ship a thrashing reaper to
/// every machine that omits the tuning knobs — the common case.
#[cfg(kani)]
#[kani::proof]
fn proof_disk_budget_defaults_are_accepted() {
use super::types::{
DiskBudget, DEFAULT_CRITICAL_FREE_GB, DEFAULT_HIGH_WATERMARK_PCT, DEFAULT_SCHEDULE,
DEFAULT_TARGET_FREE_PCT,
};
let b = DiskBudget::new(
"/",
DEFAULT_HIGH_WATERMARK_PCT,
DEFAULT_TARGET_FREE_PCT,
DEFAULT_CRITICAL_FREE_GB,
DEFAULT_SCHEDULE,
vec![],
);
assert!(b.is_ok());
assert!(b.unwrap().target_used_pct() < DEFAULT_HIGH_WATERMARK_PCT);
}