feat(kernel): implement generation-based capability revocation with proofs and tests

crates/kernel/src/proofs/revocation.rs

@@ -1,9 +1,10 @@
 use domain::capability::{Capability, CapabilityTable};
+use domain::endpoint::Endpoint;
 use domain::resource::Resource;
 use super::{arbitrary_endpoint_cap, insert_cap};
 use types::generation::Generation;
 use types::id::EndpointId;
-use types::permission::PermissionSet;
+use types::permission::{Permission, PermissionSet};
 
 #[kani::proof]
 fn revoke_invalidates_cap_slot() {
@@ -61,3 +62,77 @@ fn grant_cap_preserves_resource_identity() {
         _ => panic!("resource type changed"),
     }
 }
+
+#[kani::proof]
+fn generation_revocation_invalidates_all_caps() {
+    let bits: u8 = kani::any();
+    let ep_id: u16 = kani::any();
+    kani::assume(ep_id < 256);
+
+    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
+    let original_gen = *endpoint.generation();
+
+    let cap = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::from_bits(bits),
+        original_gen,
+    );
+
+    let mut table = CapabilityTable::new();
+    let slot = insert_cap(&mut table, cap);
+
+    assert!(table.get(slot).unwrap().generation().is_valid_against(&original_gen));
+
+    endpoint.revoke();
+    let new_gen = *endpoint.generation();
+
+    assert!(!table.get(slot).unwrap().generation().is_valid_against(&new_gen));
+}
+
+#[kani::proof]
+fn cap_created_after_revoke_is_valid() {
+    let ep_id: u16 = kani::any();
+    kani::assume(ep_id < 256);
+    let bits: u8 = kani::any();
+
+    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
+    endpoint.revoke();
+    let current_gen = *endpoint.generation();
+
+    let cap = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::from_bits(bits),
+        current_gen,
+    );
+
+    assert!(cap.generation().is_valid_against(&current_gen));
+}
+
+#[kani::proof]
+fn multiple_revocations_invalidate_all_prior_caps() {
+    let ep_id: u16 = kani::any();
+    kani::assume(ep_id < 256);
+
+    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
+
+    let gen0 = *endpoint.generation();
+    let cap0 = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::empty().with(Permission::Read),
+        gen0,
+    );
+
+    endpoint.revoke();
+    let gen1 = *endpoint.generation();
+    let cap1 = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::empty().with(Permission::Read),
+        gen1,
+    );
+
+    endpoint.revoke();
+    let gen2 = *endpoint.generation();
+
+    assert!(!cap0.generation().is_valid_against(&gen2));
+    assert!(!cap1.generation().is_valid_against(&gen2));
+}