capDL-api, sys-init: fix for GrantReply (SELFOUR-6)
The badge condition for the CNode_Mint lemmas was incorrect and ought to be untangled. This commit patches up the specs, but with ad-hoc proof fixes.
This commit is contained in:
Japheth Lim
parent
bd6b934613
commit
5516fea8a0
|
|
@ -130,7 +130,7 @@ lemma seL4_CNode_Mint_sep:
|
|||
dest_slot = offset dest_index dest_size \<and>
|
||||
|
||||
cap' = update_cap_data_det data (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap) \<and>
|
||||
(ep_related_cap src_cap \<longrightarrow> cap_badge src_cap = 0) \<and>
|
||||
(is_ep_cap src_cap \<or> is_ntfn_cap src_cap \<longrightarrow> cap_badge src_cap = 0) \<and>
|
||||
cap_has_type src_cap \<and> \<not> is_untyped_cap src_cap
|
||||
\<rbrace>
|
||||
seL4_CNode_Mint dest_root dest_index dest_depth src_root src_index src_depth rights data
|
||||
|
|
|
|||
|
|
@ -61,14 +61,14 @@ lemma reset_cap_asid_simps2:
|
|||
"reset_cap_asid cap = (UntypedCap dev a ra) \<Longrightarrow> cap = UntypedCap dev a ra"
|
||||
"reset_cap_asid cap = (EndpointCap b c d) \<Longrightarrow> cap = EndpointCap b c d"
|
||||
"reset_cap_asid cap = (NotificationCap e f g) \<Longrightarrow> cap = NotificationCap e f g"
|
||||
"reset_cap_asid cap = (ReplyCap h) \<Longrightarrow> cap = ReplyCap h"
|
||||
"reset_cap_asid cap = (ReplyCap h R) \<Longrightarrow> cap = ReplyCap h R"
|
||||
"reset_cap_asid cap = (MasterReplyCap i) \<Longrightarrow> cap = MasterReplyCap i"
|
||||
"reset_cap_asid cap = (CNodeCap j k l sz) \<Longrightarrow> cap = CNodeCap j k l sz"
|
||||
"reset_cap_asid cap = (TcbCap m) \<Longrightarrow> cap = TcbCap m"
|
||||
"reset_cap_asid cap = DomainCap \<Longrightarrow> cap = DomainCap"
|
||||
"reset_cap_asid cap = RestartCap \<Longrightarrow> cap = RestartCap"
|
||||
"reset_cap_asid cap = (PendingSyncSendCap n p q r s) \<Longrightarrow> cap = (PendingSyncSendCap n p q r s)"
|
||||
"reset_cap_asid cap = (PendingSyncRecvCap t isf ) \<Longrightarrow> cap = (PendingSyncRecvCap t isf)"
|
||||
"reset_cap_asid cap = (PendingSyncSendCap n p q r s rp) \<Longrightarrow> cap = (PendingSyncSendCap n p q r s rp)"
|
||||
"reset_cap_asid cap = (PendingSyncRecvCap t isf rp) \<Longrightarrow> cap = (PendingSyncRecvCap t isf rp)"
|
||||
"reset_cap_asid cap = (PendingNtfnRecvCap u) \<Longrightarrow> cap = (PendingNtfnRecvCap u)"
|
||||
"reset_cap_asid cap = IrqControlCap \<Longrightarrow> cap = IrqControlCap"
|
||||
"reset_cap_asid cap = (IrqHandlerCap v) \<Longrightarrow> cap = (IrqHandlerCap v)"
|
||||
|
|
@ -656,9 +656,10 @@ lemma reset_cap_asid_cap_type:
|
|||
|
||||
lemma ep_related_cap_update_cap_rights[simp]:
|
||||
"ep_related_cap (update_cap_rights rights cap) = ep_related_cap cap"
|
||||
"ep_related_cap cap \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap"
|
||||
by (auto simp:ep_related_cap_def cap_badge_def
|
||||
update_cap_rights_def split:cdl_cap.splits)
|
||||
"\<lbrakk> is_ep_cap cap \<rbrakk> \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap"
|
||||
"\<lbrakk> is_ntfn_cap cap \<rbrakk> \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap"
|
||||
by (auto simp:ep_related_cap_def cap_badge_def cap_type_def update_cap_rights_def
|
||||
split:cdl_cap.splits)
|
||||
|
||||
lemma reset_cap_asid_cap_badge:
|
||||
"\<lbrakk>reset_cap_asid cap = reset_cap_asid cap';ep_related_cap cap\<rbrakk>
|
||||
|
|
@ -674,6 +675,18 @@ lemma reset_cap_asid_ep_related_cap:
|
|||
apply (case_tac cap, (case_tac cap', simp_all add: reset_cap_asid_def)+)
|
||||
done
|
||||
|
||||
lemma reset_cap_asid_ep_cap:
|
||||
"reset_cap_asid cap = reset_cap_asid cap'
|
||||
\<Longrightarrow> is_ep_cap cap = is_ep_cap cap'"
|
||||
apply (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def)
|
||||
done
|
||||
|
||||
lemma reset_cap_asid_ntfn_cap:
|
||||
"reset_cap_asid cap = reset_cap_asid cap'
|
||||
\<Longrightarrow> is_ntfn_cap cap = is_ntfn_cap cap'"
|
||||
apply (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def)
|
||||
done
|
||||
|
||||
lemma cap_rights_reset_cap_asid:
|
||||
"reset_cap_asid cap = reset_cap_asid cap'
|
||||
\<Longrightarrow> cap_rights cap = cap_rights cap'"
|
||||
|
|
@ -892,7 +905,7 @@ lemma lookup_cap_and_slot_rvu:
|
|||
|
||||
lemma update_cap_data:
|
||||
"\<lbrace>\<lambda>s. valid_src_cap cap badge \<and> cap_has_type cap
|
||||
\<and> (ep_related_cap cap \<longrightarrow> \<not> preserve \<and> cap_badge cap = 0)
|
||||
\<and> ((is_ep_cap cap \<or> is_ntfn_cap cap) \<longrightarrow> \<not> preserve \<and> cap_badge cap = 0)
|
||||
\<and> Q (update_cap_data_det badge cap) s \<rbrace>
|
||||
update_cap_data preserve badge cap
|
||||
\<lbrace>\<lambda>rv s. Q rv s\<rbrace>"
|
||||
|
|
@ -974,11 +987,21 @@ lemma cap_has_type_asid_cong:
|
|||
\<Longrightarrow> cap_has_type cap' = cap_has_type src_cap"
|
||||
by (drule reset_cap_asid_cap_type, simp)
|
||||
|
||||
(* FIXME: MOVE *)
|
||||
fun is_reply_cap
|
||||
where "is_reply_cap (ReplyCap _ _) = True"
|
||||
| "is_reply_cap _ = False"
|
||||
|
||||
lemma ep_related_capI:
|
||||
"is_ep_cap cap \<Longrightarrow> ep_related_cap cap"
|
||||
"is_ntfn_cap cap \<Longrightarrow> ep_related_cap cap"
|
||||
"is_reply_cap cap \<Longrightarrow> ep_related_cap cap"
|
||||
by (cases cap; simp add: ep_related_cap_def cap_type_def)+
|
||||
|
||||
lemma decode_cnode_mint_rvu:
|
||||
"\<lbrace>\<lambda>s. caps \<noteq> [] \<and>
|
||||
cap_has_type src_cap \<and> valid_src_cap src_cap badge
|
||||
\<and> (ep_related_cap src_cap \<longrightarrow>
|
||||
\<and> ((is_ep_cap src_cap \<or> is_ntfn_cap src_cap) \<longrightarrow>
|
||||
cap_badge src_cap = 0)
|
||||
\<and> (\<forall>src_cap'. (reset_cap_asid src_cap'
|
||||
= reset_cap_asid src_cap) \<longrightarrow>
|
||||
|
|
@ -1021,8 +1044,13 @@ lemma decode_cnode_mint_rvu:
|
|||
simp:conj_comms is_exclusive_cap_update_cap_data
|
||||
safe_for_derive_not_non valid_src_cap_def)
|
||||
apply (intro conjI impI allI)
|
||||
apply (metis reset_cap_asid_cap_type)
|
||||
apply (metis reset_cap_asid_cap_badge reset_cap_asid_ep_related_cap)
|
||||
apply (metis reset_cap_asid_cap_type)
|
||||
apply (frule (1) reset_cap_asid_ep_cap[THEN iffD1])
|
||||
apply simp
|
||||
apply (metis reset_cap_asid_cap_badge ep_related_capI)
|
||||
apply (frule (1) reset_cap_asid_ntfn_cap[THEN iffD1])
|
||||
apply simp
|
||||
apply (metis reset_cap_asid_cap_badge ep_related_capI)
|
||||
apply (metis option.inject reset_cap_asid_cnode_cap)
|
||||
apply (metis cap_rights_reset_cap_asid)
|
||||
apply sep_solve
|
||||
|
|
@ -1079,7 +1107,9 @@ lemma decode_cnode_mutate_rvu:
|
|||
apply (sep_solve)
|
||||
apply (clarsimp dest!: mapu_dest_opt_cap
|
||||
simp: conj_comms update_cap_data_non cong:non_cap_cong)
|
||||
apply (metis reset_cap_asid_cap_type reset_cap_asid_ep_related_cap valid_src_cap_asid_cong)
|
||||
apply (subst (asm) reset_cap_asid_ep_related_cap[OF sym], assumption)
|
||||
apply (metis reset_cap_asid_cap_type reset_cap_asid_ep_related_cap valid_src_cap_asid_cong
|
||||
ep_related_capI)
|
||||
apply sep_solve
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -196,12 +196,12 @@ where
|
|||
| TcbCap _ \<Rightarrow> TcbCap obj_id
|
||||
| CNodeCap _ f2 f3 f4 \<Rightarrow> CNodeCap obj_id f2 f3 f4
|
||||
| MasterReplyCap _ \<Rightarrow> MasterReplyCap obj_id
|
||||
| ReplyCap _ \<Rightarrow> ReplyCap obj_id
|
||||
| ReplyCap _ f2 \<Rightarrow> ReplyCap obj_id f2
|
||||
| NotificationCap _ f2 f3 \<Rightarrow> NotificationCap obj_id f2 f3
|
||||
| EndpointCap _ f2 f3 \<Rightarrow> EndpointCap obj_id f2 f3
|
||||
| ZombieCap _ \<Rightarrow> ZombieCap obj_id
|
||||
| PendingSyncSendCap _ f2 f3 f4 f5 \<Rightarrow> PendingSyncSendCap obj_id f2 f3 f4 f5
|
||||
| PendingSyncRecvCap _ f2 \<Rightarrow> PendingSyncRecvCap obj_id f2
|
||||
| PendingSyncSendCap _ f2 f3 f4 f5 f6 \<Rightarrow> PendingSyncSendCap obj_id f2 f3 f4 f5 f6
|
||||
| PendingSyncRecvCap _ f2 f3 \<Rightarrow> PendingSyncRecvCap obj_id f2 f3
|
||||
| PendingNtfnRecvCap _ \<Rightarrow> PendingNtfnRecvCap obj_id
|
||||
| BoundNotificationCap _ \<Rightarrow> BoundNotificationCap obj_id
|
||||
| _ \<Rightarrow> cap"
|
||||
|
|
@ -686,12 +686,12 @@ lemma is_cnode_cap_simps:
|
|||
"is_cnode_cap (FrameCap dev x g h i j) = False"
|
||||
"is_cnode_cap (TcbCap x) = False"
|
||||
"is_cnode_cap (MasterReplyCap x) = False"
|
||||
"is_cnode_cap (ReplyCap x) = False"
|
||||
"is_cnode_cap (ReplyCap x q) = False"
|
||||
"is_cnode_cap (NotificationCap x m n) = False"
|
||||
"is_cnode_cap (EndpointCap x p q) = False"
|
||||
"is_cnode_cap (ZombieCap x) = False"
|
||||
"is_cnode_cap (PendingSyncSendCap x s t u v) = False"
|
||||
"is_cnode_cap (PendingSyncRecvCap x t) = False"
|
||||
"is_cnode_cap (PendingSyncSendCap x s t u v w) = False"
|
||||
"is_cnode_cap (PendingSyncRecvCap x t w) = False"
|
||||
"is_cnode_cap (PendingNtfnRecvCap x) = False"
|
||||
|
||||
"is_cnode_cap (CNodeCap x k l sz) = True"
|
||||
|
|
@ -863,12 +863,12 @@ lemma cap_has_object_simps [simp]:
|
|||
"cap_has_object (TcbCap x)"
|
||||
"cap_has_object (CNodeCap x k l sz)"
|
||||
"cap_has_object (MasterReplyCap x)"
|
||||
"cap_has_object (ReplyCap x)"
|
||||
"cap_has_object (ReplyCap x q)"
|
||||
"cap_has_object (NotificationCap x m n)"
|
||||
"cap_has_object (EndpointCap x p q)"
|
||||
"cap_has_object (ZombieCap x)"
|
||||
"cap_has_object (PendingSyncSendCap x s t u v)"
|
||||
"cap_has_object (PendingSyncRecvCap x t)"
|
||||
"cap_has_object (PendingSyncSendCap x s t u v w)"
|
||||
"cap_has_object (PendingSyncRecvCap x t w)"
|
||||
"cap_has_object (PendingNtfnRecvCap x)"
|
||||
"cap_has_object (UntypedCap dev ids ids') = True"
|
||||
by (simp_all add:cap_has_object_def)
|
||||
|
|
@ -971,7 +971,7 @@ where
|
|||
|
||||
definition derived_cap :: "cdl_cap \<Rightarrow> cdl_cap"
|
||||
where "derived_cap cap \<equiv> case cap of
|
||||
ReplyCap _ \<Rightarrow> NullCap
|
||||
ReplyCap _ _ \<Rightarrow> NullCap
|
||||
| MasterReplyCap _ \<Rightarrow> NullCap
|
||||
| IrqControlCap \<Rightarrow> NullCap
|
||||
| FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None
|
||||
|
|
@ -992,7 +992,7 @@ where "safe_for_derive cap \<equiv> case cap of
|
|||
| UntypedCap _ _ _ \<Rightarrow> False
|
||||
| PageTableCap _ _ _ \<Rightarrow> False
|
||||
| PageDirectoryCap _ _ _ \<Rightarrow> False
|
||||
| ReplyCap _ \<Rightarrow> False
|
||||
| ReplyCap _ _ \<Rightarrow> False
|
||||
| MasterReplyCap _ \<Rightarrow> False
|
||||
| IrqControlCap \<Rightarrow> False
|
||||
| ZombieCap _ \<Rightarrow> False
|
||||
|
|
|
|||
|
|
@ -1349,6 +1349,18 @@ lemma init_cnode_slot_copy_original_sep:
|
|||
apply (wp|clarsimp)+
|
||||
done
|
||||
|
||||
lemma ep_cap_default_cap:
|
||||
"cap_type cap = Some type \<Longrightarrow>
|
||||
is_ep_cap (default_cap type ids sz dev) = is_ep_cap cap"
|
||||
by (fastforce simp: cap_type_def default_cap_def
|
||||
split: cdl_cap.splits cdl_object_type.splits)
|
||||
|
||||
lemma ntfn_cap_default_cap:
|
||||
"cap_type cap = Some type \<Longrightarrow>
|
||||
is_ntfn_cap (default_cap type ids sz dev) = is_ntfn_cap cap"
|
||||
by (fastforce simp: cap_type_def default_cap_def
|
||||
split: cdl_cap.splits cdl_object_type.splits)
|
||||
|
||||
lemma seL4_CNode_Mint_object_slot_initialised_sep_helper:
|
||||
"\<lbrakk>well_formed spec;
|
||||
cnode_at obj_id spec;
|
||||
|
|
@ -1379,6 +1391,7 @@ lemma seL4_CNode_Mint_object_slot_initialised_sep_helper:
|
|||
si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
|
||||
si_cap_at t dup_caps spec dev obj_id \<and>*
|
||||
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
|
||||
supply ep_related_capI[intro, dest]
|
||||
apply (rule hoare_chain)
|
||||
apply (cut_tac cnode_cap = si_cspace_cap
|
||||
and cnode_cap' = si_cnode_cap
|
||||
|
|
@ -1389,19 +1402,32 @@ lemma seL4_CNode_Mint_object_slot_initialised_sep_helper:
|
|||
and tcb=root_tcb
|
||||
and src_cap = "default_cap type {client_object_id} (object_size_bits spec_cap_obj) dev"
|
||||
in seL4_CNode_Mint_sep,
|
||||
(assumption|simp add: ep_related_cap_default_cap get_index_def
|
||||
default_cap_has_type ep_related_cap_badge_of_default)+)
|
||||
(assumption|simp add: ep_cap_default_cap ntfn_cap_default_cap get_index_def
|
||||
default_cap_has_type
|
||||
ep_related_cap_badge_of_default[OF ep_related_capI(1)]
|
||||
ep_related_cap_badge_of_default[OF ep_related_capI(2)])+)
|
||||
apply (frule_tac s=s and t=t and dup_caps=dup_caps and orig_caps=orig_caps
|
||||
in mint_pre,(assumption|rule refl|simp)+)
|
||||
apply (elim conjE)
|
||||
(* FIXME: need to refactor ep_related_cap rules. For now, discharge these manually *)
|
||||
apply (subgoal_tac
|
||||
"(type = EndpointType \<longrightarrow>
|
||||
cap_badge (default_cap EndpointType {client_object_id}
|
||||
(object_size_bits spec_cap_obj) dev) = 0)
|
||||
\<and> (type = NotificationType \<longrightarrow>
|
||||
cap_badge (default_cap NotificationType {client_object_id}
|
||||
(object_size_bits spec_cap_obj) dev) = 0)")
|
||||
prefer 2
|
||||
apply (blast intro: ep_related_capI ep_related_cap_badge_of_default)
|
||||
apply clarsimp
|
||||
apply (intro conjI,
|
||||
simp_all add:has_type_default_not_non ep_related_cap_default_cap
|
||||
valid_src_cap_if_cnode)
|
||||
apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
|
||||
dest!: guard_equal_si_cspace_cap |
|
||||
rule is_cnode_cap_si_cnode_cap | sep_cancel)+)[2]
|
||||
apply (drule_tac s=s and dest_root=dest_root and src_index=src_index and R=R
|
||||
in mint_post, (assumption|simp)+)
|
||||
apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
|
||||
dest!: guard_equal_si_cspace_cap |
|
||||
rule is_cnode_cap_si_cnode_cap | sep_cancel)+)[2]
|
||||
apply (drule_tac s=s and dest_root=dest_root and src_index=src_index and R=R
|
||||
in mint_post, (assumption|simp)+)
|
||||
apply sep_cancel+
|
||||
apply (subst default_cap_data_if_cnode[symmetric],simp+)
|
||||
done
|
||||
|
|
|
|||
|
|
@ -41,12 +41,12 @@ lemma is_fake_vm_cap_cap_has_object [simp]:
|
|||
lemma cap_has_object_simps [simp]:
|
||||
"cap_has_object (EndpointCap obj_id badge rights)"
|
||||
"cap_has_object (NotificationCap obj_id badge rights)"
|
||||
"cap_has_object (ReplyCap obj_id)"
|
||||
"cap_has_object (ReplyCap obj_id rights)"
|
||||
"cap_has_object (MasterReplyCap obj_id)"
|
||||
"cap_has_object (CNodeCap obj_id guard gs sz)"
|
||||
"cap_has_object (TcbCap obj_id)"
|
||||
"cap_has_object (PendingSyncSendCap obj_id badge a b c)"
|
||||
"cap_has_object (PendingSyncRecvCap obj_id d)"
|
||||
"cap_has_object (PendingSyncSendCap obj_id badge a b c grant)"
|
||||
"cap_has_object (PendingSyncRecvCap obj_id d grant)"
|
||||
"cap_has_object (PendingNtfnRecvCap obj_id)"
|
||||
"cap_has_object (FrameCap dev obj_id rights sz type maddr)"
|
||||
"cap_has_object (PageTableCap obj_id cdl_frame_cap_type maddr)"
|
||||
|
|
|
|||
|
|
@ -829,7 +829,7 @@ lemma well_formed_orig_ep_cap_is_default:
|
|||
opt_cap (obj_id, slot) spec = Some cap;
|
||||
ep_related_cap cap; cap \<noteq> NullCap\<rbrakk>
|
||||
\<Longrightarrow> is_default_cap cap"
|
||||
apply (case_tac "\<exists>obj_id. cap = ReplyCap obj_id")
|
||||
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 (frule (3) well_formed_well_formed_orig_cap)
|
||||
|
|
|
|||
Loading…
Reference in New Issue