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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
// This Source Code Form is subject to the terms of the Mozilla Public
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at https://mozilla.org/MPL/2.0/.
// Copyright (c) 2026 2youg1 and the sprawling contributors
//! Admission control: the city-wide shedding posture.
//! One function serves every queue-shaped resource — signal queues and fd
//! headroom alike; capacity semantics belong to the caller. Queues and
//! counters live in storage::queue, never here.
//! The part `crates/kernel/spec/Backpressure.lean` specifies this module.
/// A queue's occupancy snapshot.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct QueueStats {
pub depth: u64,
pub capacity: u64,
}
/// What admitting this item would cost: one slot for a Signal, more for
/// a new-Run fd reservation.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct ItemMeta {
pub cost: u64,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ShedReason {
CapacityExhausted,
}
/// Deliberately exhaustive: a new admission outcome must force every
/// caller to decide.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Admission {
Admit,
Shed { reason: ShedReason },
}
/// Decides whether the queue admits one more item. Pure and total:
/// `depth + cost <= capacity` admits; checked arithmetic, overflow sheds
/// (fail-closed). Shedding refuses new items only — starving what is
/// already queued is a liveness property and citysim's to assert.
pub fn admit(stats: &QueueStats, item: &ItemMeta) -> Admission {
match stats.depth.checked_add(item.cost) {
Some(total) if total <= stats.capacity => Admission::Admit,
_ => Admission::Shed {
reason: ShedReason::CapacityExhausted,
},
}
}
#[cfg(kani)]
mod verification {
//! V5: admission is total, monotone — a shallower queue never makes
//! the same item harder to admit — and fail-closed when the sum
//! overflows. Both harnesses range over every `u64`, and the
//! arithmetic is linear, so CBMC returns in under a minute.
use super::*;
#[kani::proof]
fn admit_is_total_and_monotone_in_depth() {
let capacity: u64 = kani::any();
let deep: u64 = kani::any();
let shallow: u64 = kani::any();
kani::assume(shallow <= deep);
let item = ItemMeta { cost: kani::any() };
let deep_verdict = admit(
&QueueStats {
depth: deep,
capacity,
},
&item,
);
let shallow_verdict = admit(
&QueueStats {
depth: shallow,
capacity,
},
&item,
);
if deep_verdict == Admission::Admit {
assert_eq!(shallow_verdict, Admission::Admit);
}
}
/// Fail-closed at the top of the range: whenever admitting the item
/// would carry the queue past `u64::MAX`, the answer is Shed. The
/// `#[test]` beside it fixes the depth at `u64::MAX`; this holds for
/// every depth, capacity and cost whose sum overflows.
#[kani::proof]
fn an_overflowing_sum_never_admits() {
let stats = QueueStats {
depth: kani::any(),
capacity: kani::any(),
};
let item = ItemMeta { cost: kani::any() };
kani::assume(stats.depth.checked_add(item.cost).is_none());
assert_eq!(
admit(&stats, &item),
Admission::Shed {
reason: ShedReason::CapacityExhausted
}
);
}
}
#[cfg(test)]
#[allow(
clippy::unwrap_used,
clippy::expect_used,
clippy::panic,
clippy::indexing_slicing,
reason = "test code"
)]
mod tests {
use super::*;
use proptest::prelude::*;
#[test]
fn admits_up_to_capacity_and_sheds_past_it() {
let stats = QueueStats {
depth: 9,
capacity: 10,
};
assert_eq!(admit(&stats, &ItemMeta { cost: 1 }), Admission::Admit);
assert_eq!(
admit(&stats, &ItemMeta { cost: 2 }),
Admission::Shed {
reason: ShedReason::CapacityExhausted
}
);
}
#[test]
fn overflow_sheds_instead_of_wrapping() {
let stats = QueueStats {
depth: u64::MAX,
capacity: u64::MAX,
};
assert_eq!(
admit(&stats, &ItemMeta { cost: 1 }),
Admission::Shed {
reason: ShedReason::CapacityExhausted
}
);
// Zero-cost probes still fit a full-but-not-overflowing queue.
assert_eq!(admit(&stats, &ItemMeta { cost: 0 }), Admission::Admit);
}
proptest! {
/// Kani mirror: monotone in depth.
#[test]
fn shallower_is_never_harder(capacity in any::<u64>(), deep in any::<u64>(),
delta in any::<u64>(), cost in any::<u64>()) {
let shallow = deep.saturating_sub(delta);
let item = ItemMeta { cost };
let deep_verdict = admit(&QueueStats { depth: deep, capacity }, &item);
let shallow_verdict = admit(&QueueStats { depth: shallow, capacity }, &item);
if deep_verdict == Admission::Admit {
prop_assert_eq!(shallow_verdict, Admission::Admit);
}
}
/// Kani mirror: a sum past `u64::MAX` sheds rather than wraps.
#[test]
fn an_overflowing_sum_sheds(capacity in any::<u64>(), depth in any::<u64>(),
cost in any::<u64>()) {
if depth.checked_add(cost).is_none() {
prop_assert_eq!(
admit(&QueueStats { depth, capacity }, &ItemMeta { cost }),
Admission::Shed { reason: ShedReason::CapacityExhausted }
);
}
}
}
}