perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

crates/domain/src/memory/frame/proofs.rs

@@ -35,13 +35,17 @@ fn any_use() -> FrameUse {
     }
 }
 
-fn any_slot() -> Option<FrameUse> {
-    if kani::any() { Some(any_use()) } else { None }
+fn any_slot() -> Slot<FrameUse> {
+    if kani::any() {
+        Slot::Full(any_use())
+    } else {
+        Slot::Empty
+    }
 }
 
 fn any_table() -> FrameTable<N> {
     let frames = [any_slot(), any_slot(), any_slot(), any_slot()];
-    let free = frames.iter().filter(|f| f.is_none()).count();
+    let free = frames.iter().filter(|f| !f.is_full()).count();
     FrameTable {
         base: PhysicalAddress::from_raw(BASE),
         total: N,
@@ -53,7 +57,7 @@ fn any_table() -> FrameTable<N> {
 }
 
 fn well_formed(t: &FrameTable<N>) -> bool {
-    t.free == t.frames[..t.total].iter().filter(|f| f.is_none()).count()
+    t.free == t.frames[..t.total].iter().filter(|f| !f.is_full()).count()
 }
 
 fn any_pa() -> PhysicalAddress {
@@ -71,8 +75,8 @@ fn alloc_only_hands_out_free_frames() {
         Some(pa) => {
             let idx = (pa.raw() - BASE) / PAGE_SIZE;
             assert!(idx < N);
-            assert!(before[idx].is_none());
-            assert!(t.frames[idx] == Some(usage));
+            assert!(!before[idx].is_full());
+            assert!(t.frames[idx] == Slot::Full(usage));
             for i in 0..N {
                 if i != idx {
                     assert!(t.frames[i] == before[i]);
@@ -80,7 +84,7 @@ fn alloc_only_hands_out_free_frames() {
             }
         }
         None => {
-            assert!(before.iter().all(Option::is_some));
+            assert!(before.iter().all(Slot::is_full));
             assert!(t.frames == before);
         }
     }
@@ -97,8 +101,8 @@ fn free_releases_exactly_one_allocated_frame_or_nothing() {
         Some(usage) => {
             let idx = (pa.raw() - BASE) / PAGE_SIZE;
             assert!(pa.raw() % PAGE_SIZE == 0);
-            assert!(before[idx] == Some(usage));
-            assert!(t.frames[idx].is_none());
+            assert!(before[idx] == Slot::Full(usage));
+            assert!(!t.frames[idx].is_full());
             for i in 0..N {
                 if i != idx {
                     assert!(t.frames[i] == before[i]);
@@ -119,8 +123,8 @@ fn retag_never_allocates() {
     let usage = any_use();
     let changed = t.retag(pa, usage);
     for i in 0..N {
-        if before[i].is_none() {
-            assert!(t.frames[i].is_none());
+        if !before[i].is_full() {
+            assert!(!t.frames[i].is_full());
         }
     }
     if !changed {
@@ -138,11 +142,11 @@ fn free_owned_by_spares_everyone_else() {
     t.free_owned_by(owner);
     for i in 0..N {
         let was_owned = matches!(
-            before[i],
-            Some(FrameUse::User { owner: o, .. } | FrameUse::PageTable { owner: o }) if o == owner
+            before[i].as_ref(),
+            Some(FrameUse::User { owner: o, .. } | FrameUse::PageTable { owner: o }) if *o == owner
         );
         if was_owned {
-            assert!(t.frames[i].is_none());
+            assert!(!t.frames[i].is_full());
         } else {
             assert!(t.frames[i] == before[i]);
         }
@@ -162,7 +166,7 @@ fn find_user_only_reports_the_owners_mapping() {
         assert!(va.raw() % PAGE_SIZE == 0);
         assert!(
             t.frames[idx]
-                == Some(FrameUse::User {
+                == Slot::Full(FrameUse::User {
                     owner,
                     page: (va.raw() / PAGE_SIZE) as u32,
                     perms,
@@ -184,8 +188,8 @@ fn alloc_contiguous_only_claims_a_free_run() {
             assert!(count > 0 && start + count <= N);
             for i in 0..N {
                 if i >= start && i < start + count {
-                    assert!(before[i].is_none());
-                    assert!(t.frames[i] == Some(FrameUse::Region { region }));
+                    assert!(!before[i].is_full());
+                    assert!(t.frames[i] == Slot::Full(FrameUse::Region { region }));
                 } else {
                     assert!(t.frames[i] == before[i]);
                 }