mc: Add is_valid predicate for granule status table

The added predicate can be used to ensure that all granule
entries in Granule Status Table (GST) are in valid status.

forall granule in GST :: granule.is_valid()

Usage)

assert!(GRANULE_STATUS_TABLE.is_valid());

A2.2.1 Granule attributes in beta0-eac4

If the state of a Granule is not UNDELEGATED then the PAS of the Granule is REALM.
If the state of a Granule is UNDELEGATED then the PAS of the Granule is not REALM.

Signed-off-by: Changho Choi <[email protected]>

rmm/src/granule/array/entry.rs

@@ -44,7 +44,15 @@ impl Granule {
     fn new() -> Self {
         let state = kani::any();
         kani::assume(state >= GranuleState::Undelegated && state <= GranuleState::RTT);
-        let gpt = kani::any();
+        let gpt = {
+            if state != GranuleState::Undelegated {
+                GranuleGpt::GPT_REALM
+            } else {
+                let gpt = kani::any();
+                kani::assume(gpt != GranuleGpt::GPT_REALM);
+                gpt
+            }
+        };
         Granule { state, gpt }
     }
 
@@ -53,6 +61,18 @@ impl Granule {
         self.gpt = gpt;
     }
 
+    #[cfg(kani)]
+    pub fn is_valid(&self) -> bool {
+        self.state >= GranuleState::Undelegated &&
+        self.state <= GranuleState::RTT &&
+        // XXX: the below condition holds from beta0 to eac4
+        if self.state != GranuleState::Undelegated {
+            self.gpt == GranuleGpt::GPT_REALM
+        } else {
+            self.gpt != GranuleGpt::GPT_REALM
+        }
+    }
+
     pub fn state(&self) -> u8 {
         self.state
     }
@@ -110,9 +130,17 @@ impl Granule {
 
 pub struct Entry(Spinlock<Granule>);
 impl Entry {
+    #[cfg(not(kani))]
     pub fn new() -> Self {
         Self(Spinlock::new(Granule::new()))
     }
+    #[cfg(kani)]
+    // DIFF: assertion is added to reduce the proof burden
+    pub fn new() -> Self {
+        let granule = Granule::new();
+        assert!(granule.is_valid());
+        Self(Spinlock::new(granule))
+    }
 
     pub fn lock(&self) -> Result<SpinlockGuard<'_, Granule>, Error> {
         let granule = self.0.lock();

rmm/src/granule/array/mod.rs

@@ -89,6 +89,13 @@ impl GranuleStatusTable {
             entries: core::array::from_fn(|_| Entry::new()),
         }
     }
+
+    #[cfg(kani)]
+    pub fn is_valid(&self) -> bool {
+        self.entries
+            .iter()
+            .fold(true, |acc, x| acc && x.lock().unwrap().is_valid())
+    }
 }
 
 #[macro_export]