lewis.moe
Nothing to see here, move along
1use crate::cap_table::{CapRef, CapSlot};
2use crate::error::KernelError;
3use crate::object_tag::ObjectTag;
4use crate::types::{Generation, ObjectId};
5
6pub const MIN_CNODE_BITS: u8 = 1;
7pub const MAX_CNODE_BITS: u8 = 12;
8pub const MAX_RESOLVE_DEPTH: u8 = 16;
9pub const CAPSLOT_SIZE: usize = core::mem::size_of::<CapSlot>();
10pub const PAGE_SIZE: usize = 4096;
11
12const _: () = {
13 let max_slots = 1usize << MAX_CNODE_BITS;
14 let max_bytes = max_slots * CAPSLOT_SIZE;
15 let max_frames = max_bytes.div_ceil(PAGE_SIZE);
16 assert!(max_frames <= u8::MAX as usize);
17};
18
19pub fn frames_for_cnode(size_bits: u8) -> u8 {
20 let slots = 1usize << size_bits;
21 let bytes = slots * CAPSLOT_SIZE;
22 bytes.div_ceil(PAGE_SIZE) as u8
23}
24
25pub fn extract_index(address: u64, remaining_depth: u8, size_bits: u8) -> u64 {
26 let shift = remaining_depth - size_bits;
27 let mask = (1u64 << size_bits) - 1;
28 (address >> shift) & mask
29}
30
31pub fn validate_size_bits(size_bits: u8) -> Result<(), KernelError> {
32 match (MIN_CNODE_BITS..=MAX_CNODE_BITS).contains(&size_bits) {
33 true => Ok(()),
34 false => Err(KernelError::InvalidParameter),
35 }
36}
37
38pub trait CNodeStore {
39 fn read_slot(
40 &self,
41 cnode_id: ObjectId,
42 cnode_gen: Generation,
43 index: usize,
44 ) -> Result<CapSlot, KernelError>;
45
46 fn size_bits(
47 &self,
48 cnode_id: ObjectId,
49 cnode_gen: Generation,
50 ) -> Result<u8, KernelError>;
51}
52
53pub fn resolve<S: CNodeStore>(
54 store: &S,
55 cnode_id: ObjectId,
56 cnode_gen: Generation,
57 address: u64,
58 depth: u8,
59) -> Result<CapSlot, KernelError> {
60 resolve_inner(store, cnode_id, cnode_gen, address, depth, 0)
61}
62
63fn resolve_inner<S: CNodeStore>(
64 store: &S,
65 cnode_id: ObjectId,
66 cnode_gen: Generation,
67 address: u64,
68 depth: u8,
69 recursion: u8,
70) -> Result<CapSlot, KernelError> {
71 if recursion >= MAX_RESOLVE_DEPTH {
72 return Err(KernelError::InvalidSlot);
73 }
74
75 let size_bits = store.size_bits(cnode_id, cnode_gen)?;
76
77 if depth < size_bits {
78 return Err(KernelError::InvalidSlot);
79 }
80
81 let index = extract_index(address, depth, size_bits) as usize;
82 let remaining = depth - size_bits;
83 let slot = store.read_slot(cnode_id, cnode_gen, index)?;
84
85 match remaining {
86 0 => Ok(slot),
87 _ => match slot {
88 CapSlot::Active(cap) if cap.tag() == ObjectTag::CNode => resolve_inner(
89 store,
90 cap.object_id(),
91 cap.generation(),
92 address,
93 remaining,
94 recursion + 1,
95 ),
96 _ => Err(KernelError::InvalidSlot),
97 },
98 }
99}
100
101pub fn resolve_and_validate<S: CNodeStore>(
102 store: &S,
103 cnode_id: ObjectId,
104 cnode_gen: Generation,
105 address: u64,
106 depth: u8,
107 expected_tag: ObjectTag,
108 required_rights: crate::cap_table::Rights,
109) -> Result<CapRef, KernelError> {
110 match resolve(store, cnode_id, cnode_gen, address, depth)? {
111 CapSlot::Empty => Err(KernelError::SlotEmpty),
112 CapSlot::Active(cap) => {
113 if cap.tag() != expected_tag {
114 return Err(KernelError::InvalidType);
115 }
116 if !cap.rights().contains(required_rights) {
117 return Err(KernelError::InsufficientRights);
118 }
119 Ok(cap)
120 }
121 }
122}
123
124pub fn resolve_and_read<S: CNodeStore>(
125 store: &S,
126 cnode_id: ObjectId,
127 cnode_gen: Generation,
128 address: u64,
129 depth: u8,
130) -> Result<CapRef, KernelError> {
131 match resolve(store, cnode_id, cnode_gen, address, depth)? {
132 CapSlot::Empty => Err(KernelError::SlotEmpty),
133 CapSlot::Active(cap) => Ok(cap),
134 }
135}
136
137#[cfg(kani)]
138mod kani_proofs {
139 use super::*;
140 use crate::cap_table::Rights;
141
142 struct SingleCNode {
143 slots: [CapSlot; 16],
144 size_bits: u8,
145 expected_id: ObjectId,
146 expected_gen: Generation,
147 }
148
149 impl SingleCNode {
150 fn new(id: ObjectId, generation: Generation) -> Self {
151 Self {
152 slots: [CapSlot::Empty; 16],
153 size_bits: 4,
154 expected_id: id,
155 expected_gen: generation,
156 }
157 }
158 }
159
160 impl CNodeStore for SingleCNode {
161 fn read_slot(
162 &self,
163 cnode_id: ObjectId,
164 cnode_gen: Generation,
165 index: usize,
166 ) -> Result<CapSlot, KernelError> {
167 if cnode_id != self.expected_id || cnode_gen != self.expected_gen {
168 return Err(KernelError::StaleGeneration);
169 }
170 match index < (1usize << self.size_bits) {
171 true => Ok(self.slots[index]),
172 false => Err(KernelError::InvalidSlot),
173 }
174 }
175
176 fn size_bits(
177 &self,
178 cnode_id: ObjectId,
179 cnode_gen: Generation,
180 ) -> Result<u8, KernelError> {
181 if cnode_id != self.expected_id || cnode_gen != self.expected_gen {
182 return Err(KernelError::StaleGeneration);
183 }
184 Ok(self.size_bits)
185 }
186 }
187
188 #[kani::proof]
189 fn extract_index_bounded() {
190 let address: u64 = kani::any();
191 let size_bits: u8 = kani::any();
192 let remaining_depth: u8 = kani::any();
193
194 kani::assume(size_bits >= MIN_CNODE_BITS && size_bits <= MAX_CNODE_BITS);
195 kani::assume(remaining_depth >= size_bits && remaining_depth <= 64);
196
197 let idx = extract_index(address, remaining_depth, size_bits);
198 assert!(idx < (1u64 << size_bits));
199 }
200
201 #[kani::proof]
202 fn extract_index_shift_correctness() {
203 let size_bits: u8 = kani::any();
204 let remaining_depth: u8 = kani::any();
205 let address: u64 = kani::any();
206
207 kani::assume(size_bits >= 1 && size_bits <= 8);
208 kani::assume(remaining_depth >= size_bits && remaining_depth <= 16);
209
210 let idx = extract_index(address, remaining_depth, size_bits);
211 let shift = remaining_depth - size_bits;
212 let reconstructed = idx << shift;
213
214 let mask = ((1u64 << size_bits) - 1) << shift;
215 assert!((reconstructed ^ (address & mask)) == 0);
216 }
217
218 #[kani::proof]
219 fn two_level_address_partitioning() {
220 let outer_bits: u8 = kani::any();
221 let inner_bits: u8 = kani::any();
222
223 kani::assume(outer_bits >= 1 && outer_bits <= 6);
224 kani::assume(inner_bits >= 1 && inner_bits <= 6);
225
226 let total_depth = outer_bits + inner_bits;
227 kani::assume(total_depth <= 12);
228
229 let outer_idx: u64 = kani::any();
230 let inner_idx: u64 = kani::any();
231 kani::assume(outer_idx < (1u64 << outer_bits));
232 kani::assume(inner_idx < (1u64 << inner_bits));
233
234 let address = (outer_idx << inner_bits) | inner_idx;
235
236 let got_outer = extract_index(address, total_depth, outer_bits);
237 let remaining = total_depth - outer_bits;
238 let got_inner = extract_index(address, remaining, inner_bits);
239
240 assert!(got_outer == outer_idx);
241 assert!(got_inner == inner_idx);
242 }
243
244 #[kani::proof]
245 fn frames_for_cnode_monotonic() {
246 let a: u8 = kani::any();
247 let b: u8 = kani::any();
248 kani::assume(a >= MIN_CNODE_BITS && a <= MAX_CNODE_BITS);
249 kani::assume(b >= MIN_CNODE_BITS && b <= MAX_CNODE_BITS);
250 kani::assume(a <= b);
251 assert!(frames_for_cnode(a) <= frames_for_cnode(b));
252 }
253
254 #[kani::proof]
255 fn resolve_empty_cnode_returns_empty() {
256 let id = ObjectId::new(0);
257 let generation = Generation::new(0);
258 let store = SingleCNode::new(id, generation);
259
260 let address: u8 = kani::any();
261 kani::assume(address < 16);
262
263 let result = resolve(&store, id, generation, address as u64, 4);
264 assert!(matches!(result, Ok(CapSlot::Empty)));
265 }
266
267 #[kani::proof]
268 fn resolve_finds_inserted_cap() {
269 let id = ObjectId::new(0);
270 let generation = Generation::new(0);
271 let mut store = SingleCNode::new(id, generation);
272
273 let slot_idx: u8 = kani::any();
274 kani::assume(slot_idx < 16);
275
276 let cap = CapRef::new(ObjectTag::Endpoint, ObjectId::new(1), Rights::ALL, Generation::new(0));
277 store.slots[slot_idx as usize] = CapSlot::Active(cap);
278
279 let result = resolve(&store, id, generation, slot_idx as u64, 4);
280 match result {
281 Ok(CapSlot::Active(found)) => {
282 assert!(found.tag() == ObjectTag::Endpoint);
283 assert!(found.object_id() == ObjectId::new(1));
284 }
285 _ => panic!("expected Active slot"),
286 }
287 }
288
289 #[kani::proof]
290 fn resolve_stale_generation_rejected() {
291 let id = ObjectId::new(0);
292 let generation = Generation::new(0);
293 let store = SingleCNode::new(id, generation);
294
295 let stale = Generation::new(1);
296 let result = resolve(&store, id, stale, 0, 4);
297 assert!(matches!(result, Err(KernelError::StaleGeneration)));
298 }
299
300 #[kani::proof]
301 fn resolve_depth_less_than_size_bits_rejected() {
302 let id = ObjectId::new(0);
303 let generation = Generation::new(0);
304 let store = SingleCNode::new(id, generation);
305
306 let depth: u8 = kani::any();
307 kani::assume(depth < 4);
308 let result = resolve(&store, id, generation, 0, depth);
309 assert!(matches!(result, Err(KernelError::InvalidSlot)));
310 }
311
312 #[kani::proof]
313 fn validate_size_bits_range() {
314 let s: u8 = kani::any();
315 let result = validate_size_bits(s);
316 match (MIN_CNODE_BITS..=MAX_CNODE_BITS).contains(&s) {
317 true => assert!(result.is_ok()),
318 false => assert!(matches!(result, Err(KernelError::InvalidParameter))),
319 }
320 }
321}