secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

sys-init: exclude SGISignalCap 

For now exclude SGISignalCap from wellformed specs. To be relaxed
later.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2024-02-16 21:20:24 +11:00
parent a690fd7288
commit 08c7d7da98
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
sys-init/WellFormed_SI.thy
View File

@ -121,6 +121,7 @@ where
| UntypedCap _ _ _ \<Rightarrow> False
| AsidControlCap \<Rightarrow> False
| AsidPoolCap _ _ \<Rightarrow> False
| SGISignalCap _ _ \<Rightarrow> False \<comment> \<open>FIXME SGI: eventually 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 target. cap = SGISignalCap irq target")
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)