fix(proofs): replace tautological delegate guard proof with check_cap path verification

crates/kernel/src/proofs.rs

@@ -108,15 +108,56 @@ mod kani_proofs {
     }
 
     #[kani::proof]
-    fn kernel_delegate_requires_delegate_permission() {
+    fn kernel_delegate_rejects_without_delegate_permission() {
         let source_bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
         let source_perms = PermissionSet::from_bits(source_bits);
         kani::assume(!source_perms.allows(Permission::Delegate));
 
-        // Without Delegate permission, the kernel's check_cap would reject.
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
-        // This proves the guard: a cap without Delegate permission
+        let cap = Capability::new(resource, source_perms, Generation::initial());
-        // cannot be used for delegation.
+
-        assert!(!source_perms.allows(Permission::Delegate));
+        let mut table = CapabilityTable::new();
+        let slot = table.insert(cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        // This is what check_cap does: look up the cap and check permission
+        let retrieved = table.get(slot).unwrap();
+        let has_delegate = retrieved.permissions().allows(Permission::Delegate);
+
+        // The guard MUST reject: a cap inserted without Delegate
+        // permission is never retrievable with Delegate permission
+        assert!(!has_delegate);
+    }
+
+    #[kani::proof]
+    fn kernel_check_cap_faithfully_reflects_stored_permissions() {
+        let bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let perms = PermissionSet::from_bits(bits);
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
+        let cap = Capability::new(resource, perms, Generation::initial());
+
+        let mut table = CapabilityTable::new();
+        let slot = table.insert(cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        let retrieved = table.get(slot).unwrap();
+
+        // check_cap checks allows(needed). Prove the table doesn't
+        // corrupt permissions: every permission check on the retrieved
+        // cap matches what was stored.
+        assert!(retrieved.permissions().allows(Permission::Read) == perms.allows(Permission::Read));
+        assert!(retrieved.permissions().allows(Permission::Write) == perms.allows(Permission::Write));
+        assert!(retrieved.permissions().allows(Permission::Execute) == perms.allows(Permission::Execute));
+        assert!(retrieved.permissions().allows(Permission::Delegate) == perms.allows(Permission::Delegate));
+        assert!(retrieved.permissions().allows(Permission::Revoke) == perms.allows(Permission::Revoke));
     }
 
     #[kani::proof]