sys-init: exclude SGISignalCap

For now exclude SGISignalCap from wellformed specs. To be relaxed later. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Mar 26, 2024 · 3f971a8 · 3f971a8
1 parent 9116b66
commit 3f971a8
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/sys-init/WellFormed_SI.thy b/sys-init/WellFormed_SI.thy
@@ -121,6 +121,7 @@ where
     | UntypedCap _ _ _          \<Rightarrow> False
     | AsidControlCap          \<Rightarrow> False
     | AsidPoolCap _ _         \<Rightarrow> False
+    | SGISignalCap _ _        \<Rightarrow> False \<comment> \<open>FIXME SGI: allow this\<close>
     | _                       \<Rightarrow> False)"
 
 (* LIMITATION: The specification cannot contain ASID numbers. *)
@@ -812,6 +813,9 @@ lemma well_formed_orig_ep_cap_is_default:
   apply (case_tac "\<exists>obj_id R. cap = ReplyCap obj_id R")
    apply (frule (1) well_formed_well_formed_cap', simp)
    apply (clarsimp simp: well_formed_cap_def)
+  apply (case_tac "\<exists>irq targets. cap = SGISignalCap irq targets")
+   apply (frule (1) well_formed_well_formed_cap', simp)
+   apply (clarsimp simp: well_formed_cap_def)
   apply (frule (3) well_formed_well_formed_orig_cap)
   apply (erule (1) well_formed_orig_ep_cap_is_default_helper)
   apply (fastforce simp: ep_related_cap_def split: cdl_cap.splits)