x64 refine: update for GrantReply (SELFOUR-6)
This commit is contained in:
Rafal Kolanski
Japheth Lim
parent
0ead52863d
commit
103fc3656e
|
|
@ -379,16 +379,17 @@ fun
|
|||
where
|
||||
"CapabilityMap capability.NullCap = cap.NullCap"
|
||||
| "CapabilityMap (capability.UntypedCap d ref n idx) = cap.UntypedCap d ref n idx"
|
||||
| "CapabilityMap (capability.EndpointCap ref b sr rr gr) =
|
||||
| "CapabilityMap (capability.EndpointCap ref b sr rr gr grr) =
|
||||
cap.EndpointCap ref b {x. sr \<and> x = AllowSend \<or> rr \<and> x = AllowRecv \<or>
|
||||
gr \<and> x = AllowGrant}"
|
||||
gr \<and> x = AllowGrant \<or> grr \<and> x = AllowGrantReply}"
|
||||
| "CapabilityMap (capability.NotificationCap ref b sr rr) =
|
||||
cap.NotificationCap ref b {x. sr \<and> x = AllowSend \<or> rr \<and> x = AllowRecv}"
|
||||
| "CapabilityMap (capability.CNodeCap ref n L l) =
|
||||
cap.CNodeCap ref n (bin_to_bl l (uint L))"
|
||||
| "CapabilityMap (capability.ThreadCap ref) = cap.ThreadCap ref"
|
||||
| "CapabilityMap capability.DomainCap = cap.DomainCap"
|
||||
| "CapabilityMap (capability.ReplyCap ref master) = cap.ReplyCap ref master"
|
||||
| "CapabilityMap (capability.ReplyCap ref master gr) =
|
||||
cap.ReplyCap ref master {x. gr \<and> x = AllowGrant \<or> x = AllowWrite}"
|
||||
| "CapabilityMap capability.IRQControlCap = cap.IRQControlCap"
|
||||
| "CapabilityMap (capability.IRQHandlerCap irq) = cap.IRQHandlerCap irq"
|
||||
| "CapabilityMap (capability.Zombie p b n) =
|
||||
|
|
@ -435,10 +436,13 @@ done
|
|||
lemma cap_relation_imp_CapabilityMap:
|
||||
"\<lbrakk>wellformed_cap c; cap_relation c c'\<rbrakk> \<Longrightarrow> CapabilityMap c' = c"
|
||||
apply (case_tac c; simp add: wellformed_cap_simps)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac "x", simp_all)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac "x", simp_all)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac "x", simp_all add: word_bits_def)
|
||||
apply (case_tac "x", simp_all add: word_bits_def)
|
||||
apply clarsimp
|
||||
apply (simp add: set_eq_iff, rule allI)
|
||||
apply (case_tac x; clarsimp)
|
||||
apply (simp add: uint_of_bl_is_bl_to_bin bl_bin_bl[simplified])
|
||||
apply (simp add: zbits_map_def split: option.splits)
|
||||
apply (rename_tac arch_cap)
|
||||
|
|
@ -459,12 +463,13 @@ where
|
|||
Structures_A.thread_state.IdleThreadState"
|
||||
| "ThStateMap Structures_H.thread_state.BlockedOnReply =
|
||||
Structures_A.thread_state.BlockedOnReply"
|
||||
| "ThStateMap (Structures_H.thread_state.BlockedOnReceive oref) =
|
||||
Structures_A.thread_state.BlockedOnReceive oref"
|
||||
| "ThStateMap (Structures_H.thread_state.BlockedOnSend oref badge grant call) =
|
||||
| "ThStateMap (Structures_H.thread_state.BlockedOnReceive oref grant) =
|
||||
Structures_A.thread_state.BlockedOnReceive oref \<lparr> receiver_can_grant = grant \<rparr>"
|
||||
| "ThStateMap (Structures_H.thread_state.BlockedOnSend oref badge grant grant_reply call) =
|
||||
Structures_A.thread_state.BlockedOnSend oref
|
||||
\<lparr> sender_badge = badge,
|
||||
sender_can_grant = grant,
|
||||
sender_can_grant_reply = grant_reply,
|
||||
sender_is_call = call \<rparr>"
|
||||
| "ThStateMap (Structures_H.thread_state.BlockedOnNotification oref) =
|
||||
Structures_A.thread_state.BlockedOnNotification oref"
|
||||
|
|
|
|||
|
|
@ -74,9 +74,9 @@ lemma isCap_simps:
|
|||
"isThreadCap v = (\<exists>v0. v = ThreadCap v0)"
|
||||
"isCNodeCap v = (\<exists>v0 v1 v2 v3. v = CNodeCap v0 v1 v2 v3)"
|
||||
"isNotificationCap v = (\<exists>v0 v1 v2 v3. v = NotificationCap v0 v1 v2 v3)"
|
||||
"isEndpointCap v = (\<exists>v0 v1 v2 v3 v4. v = EndpointCap v0 v1 v2 v3 v4)"
|
||||
"isEndpointCap v = (\<exists>v0 v1 v2 v3 v4 v5. v = EndpointCap v0 v1 v2 v3 v4 v5)"
|
||||
"isUntypedCap v = (\<exists>d v0 v1 f. v = UntypedCap d v0 v1 f)"
|
||||
"isReplyCap v = (\<exists>v0 v1. v = ReplyCap v0 v1)"
|
||||
"isReplyCap v = (\<exists>v0 v1 v2. v = ReplyCap v0 v1 v2)"
|
||||
"isIRQControlCap v = (v = IRQControlCap)"
|
||||
"isIRQHandlerCap v = (\<exists>v0. v = IRQHandlerCap v0)"
|
||||
"isNullCap v = (v = NullCap)"
|
||||
|
|
@ -159,7 +159,7 @@ lemmas projectKOs =
|
|||
projectKO_eq projectKO_eq2
|
||||
|
||||
lemma capAligned_epI:
|
||||
"ep_at' p s \<Longrightarrow> capAligned (EndpointCap p a b c d)"
|
||||
"ep_at' p s \<Longrightarrow> capAligned (EndpointCap p a b c d e)"
|
||||
apply (clarsimp simp: obj_at'_real_def capAligned_def
|
||||
objBits_simps word_bits_def)
|
||||
apply (drule ko_wp_at_norm)
|
||||
|
|
@ -185,7 +185,7 @@ lemma capAligned_tcbI:
|
|||
done
|
||||
|
||||
lemma capAligned_reply_tcbI:
|
||||
"tcb_at' p s \<Longrightarrow> capAligned (ReplyCap p m)"
|
||||
"tcb_at' p s \<Longrightarrow> capAligned (ReplyCap p m r)"
|
||||
apply (clarsimp simp: obj_at'_real_def capAligned_def
|
||||
objBits_simps word_bits_def capUntypedPtr_def isCap_simps)
|
||||
apply (fastforce dest: ko_wp_at_norm
|
||||
|
|
@ -539,9 +539,7 @@ proof (rule iffI)
|
|||
apply -
|
||||
apply (drule (1) is_aligned_addD1 [where y = "x - y", simplified add_diff_eq])
|
||||
apply (simp add: tcb_cte_cases_def)
|
||||
apply (auto simp: is_aligned_def dvd_def)
|
||||
apply arith+
|
||||
done
|
||||
by (auto simp: is_aligned_def dvd_def; arith)
|
||||
next
|
||||
assume "x = y"
|
||||
thus "tcb_at' (t + x - y) s" using tat by simp
|
||||
|
|
|
|||
|
|
@ -4745,10 +4745,7 @@ lemma isReplyMaster_eq:
|
|||
"(isReplyCap new \<and> capReplyMaster new)
|
||||
= (isReplyCap old \<and> capReplyMaster old)"
|
||||
using derived
|
||||
apply (clarsimp simp: weak_derived'_def)
|
||||
apply (rule iffI)
|
||||
apply (clarsimp simp: isCap_simps)+
|
||||
done
|
||||
by (fastforce simp: weak_derived'_def isCap_simps)
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -8696,9 +8693,8 @@ lemma sameRegion_cap'_src [simp]:
|
|||
"sameRegionAs cap' c = sameRegionAs src_cap c"
|
||||
using parency unfolding weak_derived'_def
|
||||
apply (case_tac "isReplyCap src_cap")
|
||||
apply simp
|
||||
apply (clarsimp simp: capMasterCap_def split: capability.splits arch_capability.splits)
|
||||
apply (auto simp: sameRegionAs_def X64_H.sameRegionAs_def isCap_simps split: if_split_asm)
|
||||
apply (clarsimp simp: capMasterCap_def split: capability.splits arch_capability.splits
|
||||
; fastforce simp: sameRegionAs_def X64_H.sameRegionAs_def isCap_simps split: if_split_asm)+
|
||||
done
|
||||
|
||||
lemma chunked':
|
||||
|
|
|
|||
|
|
@ -1507,7 +1507,9 @@ definition
|
|||
capASID cap = capASID cap' \<and>
|
||||
cap_asid_base' cap = cap_asid_base' cap' \<and>
|
||||
cap_vptr' cap = cap_vptr' cap' \<and>
|
||||
(isReplyCap cap \<longrightarrow> cap = cap')"
|
||||
(* check all fields of ReplyCap except capReplyCanGrant *)
|
||||
(isReplyCap cap \<longrightarrow> capTCBPtr cap = capTCBPtr cap' \<and>
|
||||
capReplyMaster cap = capReplyMaster cap')"
|
||||
|
||||
lemma capASID_update [simp]:
|
||||
"capASID (RetypeDecls_H.updateCapData P x c) = capASID c"
|
||||
|
|
@ -3139,11 +3141,11 @@ lemma isArchCap_simps[simp]:
|
|||
"isArchCap P capability.NullCap = False"
|
||||
"isArchCap P capability.DomainCap = False"
|
||||
"isArchCap P (capability.NotificationCap xca xba xaa xd) = False"
|
||||
"isArchCap P (capability.EndpointCap xda xcb xbb xab xe) = False"
|
||||
"isArchCap P (capability.EndpointCap xda xcb xbb xab xe xi) = False"
|
||||
"isArchCap P (capability.IRQHandlerCap xf) = False"
|
||||
"isArchCap P (capability.Zombie xbc xac xg) = False"
|
||||
"isArchCap P (capability.ArchObjectCap xh) = P xh"
|
||||
"isArchCap P (capability.ReplyCap xad xi) = False"
|
||||
"isArchCap P (capability.ReplyCap xad xi xia) = False"
|
||||
"isArchCap P (capability.UntypedCap d xae xj f) = False"
|
||||
"isArchCap P (capability.CNodeCap xfa xea xdb xcc) = False"
|
||||
"isArchCap P capability.IRQControlCap = False"
|
||||
|
|
@ -4266,7 +4268,7 @@ lemma revokable'_fold:
|
|||
"isCapRevocable cap srcCap =
|
||||
(case cap of capability.NotificationCap _ _ _ _ \<Rightarrow> capNtfnBadge cap \<noteq> capNtfnBadge srcCap
|
||||
| capability.IRQHandlerCap _ \<Rightarrow> isIRQControlCap srcCap
|
||||
| capability.EndpointCap _ _ _ _ _ \<Rightarrow> capEPBadge cap \<noteq> capEPBadge srcCap
|
||||
| capability.EndpointCap _ _ _ _ _ _ \<Rightarrow> capEPBadge cap \<noteq> capEPBadge srcCap
|
||||
| capability.UntypedCap _ _ _ _ \<Rightarrow> True
|
||||
| capability.ArchObjectCap (arch_capability.IOPortCap _ _) \<Rightarrow> isIOPortControlCap' srcCap | _ \<Rightarrow> False)"
|
||||
by (simp add: Retype_H.isCapRevocable_def X64_H.isCapRevocable_def isCap_simps
|
||||
|
|
@ -4524,9 +4526,9 @@ lemma set_untyped_cap_as_full_corres:
|
|||
lemma isUntypedCap_simps[simp]:
|
||||
"isUntypedCap (capability.UntypedCap uu uv uw ux) = True"
|
||||
"isUntypedCap (capability.NullCap) = False"
|
||||
"isUntypedCap (capability.EndpointCap v va vb vc vd) = False"
|
||||
"isUntypedCap (capability.EndpointCap v va vb vc vd ve) = False"
|
||||
"isUntypedCap (capability.NotificationCap v va vb vc) = False"
|
||||
"isUntypedCap (capability.ReplyCap v1 v2) = False"
|
||||
"isUntypedCap (capability.ReplyCap v1 v2 v3) = False"
|
||||
"isUntypedCap (capability.CNodeCap x1 x2 x3 x4) = False"
|
||||
"isUntypedCap (capability.ThreadCap v) = False"
|
||||
"isUntypedCap (capability.DomainCap) = False"
|
||||
|
|
|
|||
|
|
@ -23,12 +23,12 @@ context begin interpretation Arch . (*FIXME: arch_split*)
|
|||
lemma capUntypedPtr_simps [simp]:
|
||||
"capUntypedPtr (ThreadCap r) = r"
|
||||
"capUntypedPtr (NotificationCap r badge a b) = r"
|
||||
"capUntypedPtr (EndpointCap r badge a b c) = r"
|
||||
"capUntypedPtr (EndpointCap r badge a b c d) = r"
|
||||
"capUntypedPtr (Zombie r bits n) = r"
|
||||
"capUntypedPtr (ArchObjectCap x) = Arch.capUntypedPtr x"
|
||||
"capUntypedPtr (UntypedCap d r n f) = r"
|
||||
"capUntypedPtr (CNodeCap r n g n2) = r"
|
||||
"capUntypedPtr (ReplyCap r m) = r"
|
||||
"capUntypedPtr (ReplyCap r m a) = r"
|
||||
"Arch.capUntypedPtr (X64_H.ASIDPoolCap r asid) = r"
|
||||
"Arch.capUntypedPtr (X64_H.PageCap r rghts mt sz d mapdata) = r"
|
||||
"Arch.capUntypedPtr (X64_H.PageTableCap r mapdata2) = r"
|
||||
|
|
@ -620,15 +620,16 @@ lemma isPhysicalCap[simp]:
|
|||
by (simp add: isPhysicalCap_def X64_H.isPhysicalCap_def
|
||||
split: capability.split arch_capability.split)
|
||||
|
||||
(* FIXME instead of a definition and then a simp rule in the simp set, we should use fun *)
|
||||
definition
|
||||
capMasterCap :: "capability \<Rightarrow> capability"
|
||||
where
|
||||
"capMasterCap cap \<equiv> case cap of
|
||||
EndpointCap ref bdg s r g \<Rightarrow> EndpointCap ref 0 True True True
|
||||
EndpointCap ref bdg s r g gr \<Rightarrow> EndpointCap ref 0 True True True True
|
||||
| NotificationCap ref bdg s r \<Rightarrow> NotificationCap ref 0 True True
|
||||
| CNodeCap ref bits gd gs \<Rightarrow> CNodeCap ref bits 0 0
|
||||
| ThreadCap ref \<Rightarrow> ThreadCap ref
|
||||
| ReplyCap ref master \<Rightarrow> ReplyCap ref True
|
||||
| ReplyCap ref master g \<Rightarrow> ReplyCap ref True True
|
||||
| UntypedCap d ref n f \<Rightarrow> UntypedCap d ref n 0
|
||||
| ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of
|
||||
PageCap ref rghts mt sz d mapdata \<Rightarrow>
|
||||
|
|
@ -647,7 +648,7 @@ where
|
|||
| _ \<Rightarrow> cap"
|
||||
|
||||
lemma capMasterCap_simps[simp]:
|
||||
"capMasterCap (EndpointCap ref bdg s r g) = EndpointCap ref 0 True True True"
|
||||
"capMasterCap (EndpointCap ref bdg s r g gr) = EndpointCap ref 0 True True True True"
|
||||
"capMasterCap (NotificationCap ref bdg s r) = NotificationCap ref 0 True True"
|
||||
"capMasterCap (CNodeCap ref bits gd gs) = CNodeCap ref bits 0 0"
|
||||
"capMasterCap (ThreadCap ref) = ThreadCap ref"
|
||||
|
|
@ -674,13 +675,13 @@ lemma capMasterCap_simps[simp]:
|
|||
"capMasterCap (ArchObjectCap IOPortControlCap) = ArchObjectCap IOPortControlCap"
|
||||
"capMasterCap (UntypedCap d word n f) = UntypedCap d word n 0"
|
||||
"capMasterCap IRQControlCap = IRQControlCap"
|
||||
"capMasterCap (ReplyCap word m) = ReplyCap word True"
|
||||
"capMasterCap (ReplyCap word m g) = ReplyCap word True True"
|
||||
by (simp_all add: capMasterCap_def)
|
||||
|
||||
lemma capMasterCap_eqDs1:
|
||||
"capMasterCap cap = EndpointCap ref bdg s r g
|
||||
\<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g
|
||||
\<and> (\<exists>bdg s r g. cap = EndpointCap ref bdg s r g)"
|
||||
"capMasterCap cap = EndpointCap ref bdg s r g gr
|
||||
\<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g \<and> gr
|
||||
\<and> (\<exists>bdg s r g gr. cap = EndpointCap ref bdg s r g gr)"
|
||||
"capMasterCap cap = NotificationCap ref bdg s r
|
||||
\<Longrightarrow> bdg = 0 \<and> s \<and> r
|
||||
\<and> (\<exists>bdg s r. cap = NotificationCap ref bdg s r)"
|
||||
|
|
@ -700,8 +701,8 @@ lemma capMasterCap_eqDs1:
|
|||
\<Longrightarrow> cap = Zombie ref tp n"
|
||||
"capMasterCap cap = UntypedCap d ref bits 0
|
||||
\<Longrightarrow> \<exists>f. cap = UntypedCap d ref bits f"
|
||||
"capMasterCap cap = ReplyCap ref master
|
||||
\<Longrightarrow> \<exists>master. cap = ReplyCap ref master"
|
||||
"capMasterCap cap = ReplyCap ref master g
|
||||
\<Longrightarrow> master \<and> g \<and> (\<exists>master g. cap = ReplyCap ref master g)"
|
||||
"capMasterCap cap = ArchObjectCap (PageCap ref rghts mt sz d mapdata)
|
||||
\<Longrightarrow> rghts = VMReadWrite \<and> mapdata = None \<and> mt = VMNoMap
|
||||
\<and> (\<exists>rghts mapdata mt. cap = ArchObjectCap (PageCap ref rghts mt sz d mapdata))"
|
||||
|
|
@ -734,18 +735,18 @@ where
|
|||
else None"
|
||||
|
||||
lemma capBadge_simps[simp]:
|
||||
"capBadge (UntypedCap d p n f) = None"
|
||||
"capBadge (UntypedCap d p n f) = None"
|
||||
"capBadge (NullCap) = None"
|
||||
"capBadge (DomainCap) = None"
|
||||
"capBadge (EndpointCap ref badge s r w) = Some badge"
|
||||
"capBadge (NotificationCap ref badge s r) = Some badge"
|
||||
"capBadge (EndpointCap ref badge s r g gr) = Some badge"
|
||||
"capBadge (NotificationCap ref badge s r) = Some badge"
|
||||
"capBadge (CNodeCap ref bits gd gs) = None"
|
||||
"capBadge (ThreadCap ref) = None"
|
||||
"capBadge (Zombie ref b n) = None"
|
||||
"capBadge (ArchObjectCap cap) = None"
|
||||
"capBadge (IRQControlCap) = None"
|
||||
"capBadge (IRQHandlerCap irq) = None"
|
||||
"capBadge (ReplyCap tcb master) = None"
|
||||
"capBadge (ReplyCap tcb master g) = None"
|
||||
by (simp add: capBadge_def isCap_defs)+
|
||||
|
||||
lemma capClass_Master:
|
||||
|
|
@ -912,14 +913,14 @@ lemma isMDBParent_Null [simp]:
|
|||
lemma capUntypedSize_simps [simp]:
|
||||
"capUntypedSize (ThreadCap r) = 1 << objBits (undefined::tcb)"
|
||||
"capUntypedSize (NotificationCap r badge a b) = 1 << objBits (undefined::Structures_H.notification)"
|
||||
"capUntypedSize (EndpointCap r badge a b c) = 1 << objBits (undefined::endpoint)"
|
||||
"capUntypedSize (EndpointCap r badge a b c d) = 1 << objBits (undefined::endpoint)"
|
||||
"capUntypedSize (Zombie r zs n) = 1 << (zBits zs)"
|
||||
"capUntypedSize NullCap = 0"
|
||||
"capUntypedSize DomainCap = 1"
|
||||
"capUntypedSize (ArchObjectCap x) = Arch.capUntypedSize x"
|
||||
"capUntypedSize (UntypedCap d r n f) = 1 << n"
|
||||
"capUntypedSize (CNodeCap r n g n2) = 1 << (objBits (undefined::cte) + n)"
|
||||
"capUntypedSize (ReplyCap r m) = 1 << objBits (undefined :: tcb)"
|
||||
"capUntypedSize (ReplyCap r m a) = 1 << objBits (undefined :: tcb)"
|
||||
"capUntypedSize IRQControlCap = 1"
|
||||
"capUntypedSize (IRQHandlerCap irq) = 1"
|
||||
by (auto simp add: capUntypedSize_def isCap_simps objBits_simps'
|
||||
|
|
|
|||
|
|
@ -4187,16 +4187,16 @@ lemma setCTE_work_units_completed[wp]:
|
|||
done
|
||||
|
||||
lemma create_reply_master_corres:
|
||||
"sl' = cte_map sl \<Longrightarrow>
|
||||
"\<lbrakk> sl' = cte_map sl ; AllowGrant \<in> rights \<rbrakk> \<Longrightarrow>
|
||||
corres dc
|
||||
(cte_wp_at ((=) cap.NullCap) sl and valid_pspace and valid_mdb and valid_list)
|
||||
(cte_wp_at' (\<lambda>c. cteCap c = NullCap \<and> mdbPrev (cteMDBNode c) = 0) sl'
|
||||
and valid_mdb' and valid_pspace')
|
||||
(do
|
||||
y \<leftarrow> set_original sl True;
|
||||
set_cap (cap.ReplyCap thread True) sl
|
||||
set_cap (cap.ReplyCap thread True rights) sl
|
||||
od)
|
||||
(setCTE sl' (CTE (capability.ReplyCap thread True) initMDBNode))"
|
||||
(setCTE sl' (CTE (capability.ReplyCap thread True True) initMDBNode))"
|
||||
apply clarsimp
|
||||
apply (rule corres_caps_decomposition)
|
||||
defer
|
||||
|
|
@ -4301,7 +4301,7 @@ lemma valid_nullcaps_next:
|
|||
done
|
||||
|
||||
defs noReplyCapsFor_def:
|
||||
"noReplyCapsFor \<equiv> \<lambda>t s. \<forall>sl m. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m) sl s"
|
||||
"noReplyCapsFor \<equiv> \<lambda>t s. \<forall>sl m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m r) sl s"
|
||||
|
||||
lemma pspace_relation_no_reply_caps:
|
||||
assumes pspace: "pspace_relation (kheap s) (ksPSpace s')"
|
||||
|
|
@ -4328,10 +4328,10 @@ proof -
|
|||
apply (clarsimp elim!: cte_wp_at_weakenE simp: m_null)
|
||||
done
|
||||
have no_reply_caps:
|
||||
"\<forall>sl m. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m) sl s"
|
||||
"\<forall>sl m r. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m r) sl s"
|
||||
by (rule no_reply_caps_for_thread [OF invs tcb m_cte_null])
|
||||
hence noReplyCaps:
|
||||
"\<forall>sl m. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m) sl s'"
|
||||
"\<forall>sl m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m r) sl s'"
|
||||
apply (intro allI)
|
||||
apply (clarsimp simp: cte_wp_at_neg2 cte_wp_at_ctes_of simp del: split_paired_All)
|
||||
apply (frule pspace_relation_cte_wp_atI [OF pspace _ invs_valid_objs [OF invs]])
|
||||
|
|
@ -4359,8 +4359,7 @@ lemma setup_reply_master_corres:
|
|||
apply (rule corres_when)
|
||||
apply fastforce
|
||||
apply (rule_tac P'="einvs and tcb_at t" in corres_stateAssert_implied)
|
||||
apply (rule create_reply_master_corres)
|
||||
apply simp
|
||||
apply (rule create_reply_master_corres; simp)
|
||||
apply (subgoal_tac "\<exists>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s'
|
||||
\<and> cteCap cte = capability.NullCap")
|
||||
apply (fastforce dest: pspace_relation_no_reply_caps
|
||||
|
|
@ -4437,7 +4436,7 @@ lemma setupReplyMaster_wps[wp]:
|
|||
"\<lbrace>pspace_aligned'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
|
||||
"\<lbrace>pspace_distinct'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
|
||||
"slot = cte_map (t, tcb_cnode_index 2) \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> (capability.ReplyCap t True))) \<and> P (cteCaps_of s)\<rbrace>
|
||||
\<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> (capability.ReplyCap t True True))) \<and> P (cteCaps_of s)\<rbrace>
|
||||
setupReplyMaster t
|
||||
\<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>"
|
||||
apply (simp_all add: setupReplyMaster_def locateSlot_conv)
|
||||
|
|
|
|||
|
|
@ -101,8 +101,8 @@ lemma descendants_range'_def2:
|
|||
|
||||
|
||||
defs deletionIsSafe_def:
|
||||
"deletionIsSafe \<equiv> \<lambda>ptr bits s. \<forall>p t m.
|
||||
(cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m) p s \<longrightarrow>
|
||||
"deletionIsSafe \<equiv> \<lambda>ptr bits s. \<forall>p t m r.
|
||||
(cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) p s \<longrightarrow>
|
||||
t \<notin> {ptr .. ptr + 2 ^ bits - 1}) \<and>
|
||||
(\<forall>ko. ksPSpace s p = Some (KOArch ko) \<and> p \<in> {ptr .. ptr + 2 ^ bits - 1}
|
||||
\<longrightarrow> 6 \<le> bits)"
|
||||
|
|
@ -490,17 +490,17 @@ proof -
|
|||
note blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff
|
||||
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
|
||||
atLeastAtMost_iff
|
||||
have "\<And>t m. \<exists>ptr. cte_wp_at ((=) (cap.ReplyCap t m)) ptr s
|
||||
have "\<And>t m r. \<exists>ptr. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s
|
||||
\<Longrightarrow> t \<notin> {base .. base + 2 ^ magnitude - 1}"
|
||||
by (fastforce dest!: valid_cap2 simp: cap obj_reply_refs_def)
|
||||
hence "\<forall>ptr t m. cte_wp_at ((=) (cap.ReplyCap t m)) ptr s
|
||||
hence "\<forall>ptr t m r. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s
|
||||
\<longrightarrow> t \<notin> {base .. base + 2 ^ magnitude - 1}"
|
||||
by (fastforce simp del: split_paired_All)
|
||||
hence "\<forall>t. t \<in> {base .. base + 2 ^ magnitude - 1} \<longrightarrow>
|
||||
(\<forall>ptr m. \<not> cte_wp_at ((=) (cap.ReplyCap t m)) ptr s)"
|
||||
(\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s)"
|
||||
by fastforce
|
||||
hence cte: "\<forall>t. t \<in> {base .. base + 2 ^ magnitude - 1} \<longrightarrow>
|
||||
(\<forall>ptr m. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m) ptr s')"
|
||||
(\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m r) ptr s')"
|
||||
unfolding deletionIsSafe_def
|
||||
apply -
|
||||
apply (erule allEI)
|
||||
|
|
@ -876,7 +876,8 @@ lemma valid_cap_ctes_pre:
|
|||
done
|
||||
|
||||
lemma replycap_argument:
|
||||
"\<And>p t m. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m) p s \<Longrightarrow> t \<notin> {base .. base + (2 ^ bits - 1)}"
|
||||
"\<And>p t m r. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m r) p s
|
||||
\<Longrightarrow> t \<notin> {base .. base + (2 ^ bits - 1)}"
|
||||
using safe
|
||||
by (fastforce simp add: deletionIsSafe_def cte_wp_at_ctes_of field_simps)
|
||||
|
||||
|
|
|
|||
|
|
@ -1160,11 +1160,11 @@ primrec
|
|||
threadCapRefs :: "capability \<Rightarrow> machine_word set"
|
||||
where
|
||||
"threadCapRefs (ThreadCap r) = {r}"
|
||||
| "threadCapRefs (ReplyCap t m) = {}"
|
||||
| "threadCapRefs (ReplyCap t m x) = {}"
|
||||
| "threadCapRefs NullCap = {}"
|
||||
| "threadCapRefs (UntypedCap d r n i) = {}"
|
||||
| "threadCapRefs (EndpointCap r badge x y z) = {}"
|
||||
| "threadCapRefs (NotificationCap r badge x y) = {}"
|
||||
| "threadCapRefs (UntypedCap d r n i) = {}"
|
||||
| "threadCapRefs (EndpointCap r badge x y z t) = {}"
|
||||
| "threadCapRefs (NotificationCap r badge x y) = {}"
|
||||
| "threadCapRefs (CNodeCap r b g gsz) = {}"
|
||||
| "threadCapRefs (Zombie r b n) = {}"
|
||||
| "threadCapRefs (ArchObjectCap ac) = {}"
|
||||
|
|
@ -1966,7 +1966,7 @@ definition
|
|||
final_matters' :: "capability \<Rightarrow> bool"
|
||||
where
|
||||
"final_matters' cap \<equiv> case cap of
|
||||
EndpointCap ref bdg s r g \<Rightarrow> True
|
||||
EndpointCap ref bdg s r g gr \<Rightarrow> True
|
||||
| NotificationCap ref bdg s r \<Rightarrow> True
|
||||
| ThreadCap ref \<Rightarrow> True
|
||||
| CNodeCap ref bits gd gs \<Rightarrow> True
|
||||
|
|
@ -2910,7 +2910,9 @@ crunch bound_tcb_at'[wp]: cancelSignal, cancelAllIPC "bound_tcb_at' P t"
|
|||
ignore: getObject setObject threadSet)
|
||||
|
||||
lemma finaliseCapTrue_standin_bound_tcb_at':
|
||||
"\<lbrace>\<lambda>s. bound_tcb_at' P t s \<and> (\<exists>tt b. cap = ReplyCap tt b) \<rbrace> finaliseCapTrue_standin cap final \<lbrace>\<lambda>_. bound_tcb_at' P t\<rbrace>"
|
||||
"\<lbrace>\<lambda>s. bound_tcb_at' P t s \<and> (\<exists>tt b r. cap = ReplyCap tt b r) \<rbrace>
|
||||
finaliseCapTrue_standin cap final
|
||||
\<lbrace>\<lambda>_. bound_tcb_at' P t\<rbrace>"
|
||||
apply (case_tac cap, simp_all add:finaliseCapTrue_standin_def)
|
||||
apply (clarsimp simp: isNotificationCap_def)
|
||||
apply (wp, clarsimp)
|
||||
|
|
@ -3214,7 +3216,7 @@ lemma cteDeleteOne_st_tcb_at[wp]:
|
|||
done
|
||||
|
||||
lemma cteDeleteOne_reply_pred_tcb_at:
|
||||
"\<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t'. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False) slot s)\<rbrace>
|
||||
"\<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False r) slot s)\<rbrace>
|
||||
cteDeleteOne slot
|
||||
\<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>"
|
||||
apply (simp add: cteDeleteOne_def unless_def isFinalCapability_def)
|
||||
|
|
|
|||
|
|
@ -166,14 +166,14 @@ where
|
|||
"max_ipc_words \<equiv> capTransferDataSize + msgMaxLength + msgMaxExtraCaps + 2"
|
||||
|
||||
definition
|
||||
tcb_st_refs_of' :: "Structures_H.thread_state \<Rightarrow> (machine_word \<times> reftype) set"
|
||||
tcb_st_refs_of' :: "Structures_H.thread_state \<Rightarrow> (machine_word \<times> reftype) set"
|
||||
where
|
||||
"tcb_st_refs_of' z \<equiv> case z of (Running) => {}
|
||||
| (Inactive) => {}
|
||||
| (Restart) => {}
|
||||
| (BlockedOnReceive x) => {(x, TCBBlockedRecv)}
|
||||
| (BlockedOnSend x a b c) => {(x, TCBBlockedSend)}
|
||||
| (BlockedOnNotification x) => {(x, TCBSignal)}
|
||||
| (BlockedOnReceive x a) => {(x, TCBBlockedRecv)}
|
||||
| (BlockedOnSend x a b c d) => {(x, TCBBlockedSend)}
|
||||
| (BlockedOnNotification x) => {(x, TCBSignal)}
|
||||
| (BlockedOnReply) => {}
|
||||
| (IdleThreadState) => {}"
|
||||
|
||||
|
|
@ -246,15 +246,15 @@ where
|
|||
"zobj_refs' NullCap = {}"
|
||||
| "zobj_refs' DomainCap = {}"
|
||||
| "zobj_refs' (UntypedCap d r n f) = {}"
|
||||
| "zobj_refs' (EndpointCap r badge x y z) = {r}"
|
||||
| "zobj_refs' (NotificationCap r badge x y) = {r}"
|
||||
| "zobj_refs' (EndpointCap r badge x y z t) = {r}"
|
||||
| "zobj_refs' (NotificationCap r badge x y) = {r}"
|
||||
| "zobj_refs' (CNodeCap r b g gsz) = {}"
|
||||
| "zobj_refs' (ThreadCap r) = {r}"
|
||||
| "zobj_refs' (Zombie r b n) = {}"
|
||||
| "zobj_refs' (ArchObjectCap ac) = {}"
|
||||
| "zobj_refs' (IRQControlCap) = {}"
|
||||
| "zobj_refs' (IRQHandlerCap irq) = {}"
|
||||
| "zobj_refs' (ReplyCap tcb m) = {}"
|
||||
| "zobj_refs' (ReplyCap tcb m x) = {}"
|
||||
|
||||
definition
|
||||
ex_nonz_cap_to' :: "machine_word \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
|
|
@ -275,8 +275,8 @@ where
|
|||
"cte_refs' (UntypedCap d p n f) x = {}"
|
||||
| "cte_refs' (NullCap) x = {}"
|
||||
| "cte_refs' (DomainCap) x = {}"
|
||||
| "cte_refs' (EndpointCap ref badge s r g) x = {}"
|
||||
| "cte_refs' (NotificationCap ref badge s r) x = {}"
|
||||
| "cte_refs' (EndpointCap ref badge s r g gr) x = {}"
|
||||
| "cte_refs' (NotificationCap ref badge s r) x = {}"
|
||||
| "cte_refs' (CNodeCap ref bits g gs) x =
|
||||
(\<lambda>x. ref + (x * 2^cteSizeBits)) ` {0 .. 2 ^ bits - 1}"
|
||||
| "cte_refs' (ThreadCap ref) x =
|
||||
|
|
@ -286,7 +286,7 @@ where
|
|||
| "cte_refs' (ArchObjectCap cap) x = {}"
|
||||
| "cte_refs' (IRQControlCap) x = {}"
|
||||
| "cte_refs' (IRQHandlerCap irq) x = {x + (ucast irq) * 32}"
|
||||
| "cte_refs' (ReplyCap tcb m) x = {}"
|
||||
| "cte_refs' (ReplyCap tcb m g) x = {}"
|
||||
|
||||
|
||||
abbreviation
|
||||
|
|
@ -339,14 +339,14 @@ where
|
|||
"capBits NullCap = 0"
|
||||
| "capBits DomainCap = 0"
|
||||
| "capBits (UntypedCap d r b f) = b"
|
||||
| "capBits (EndpointCap r b x y z) = objBits (undefined::endpoint)"
|
||||
| "capBits (EndpointCap r b x y z t) = objBits (undefined::endpoint)"
|
||||
| "capBits (NotificationCap r b x y) = objBits (undefined::Structures_H.notification)"
|
||||
| "capBits (CNodeCap r b g gs) = objBits (undefined::cte) + b"
|
||||
| "capBits (ThreadCap r) = objBits (undefined::tcb)"
|
||||
| "capBits (Zombie r z n) = zBits z"
|
||||
| "capBits (IRQControlCap) = 0"
|
||||
| "capBits (IRQHandlerCap irq) = 0"
|
||||
| "capBits (ReplyCap tcb m) = objBits (undefined :: tcb)"
|
||||
| "capBits (ReplyCap tcb m x) = objBits (undefined :: tcb)"
|
||||
| "capBits (ArchObjectCap x) = acapBits x"
|
||||
|
||||
definition
|
||||
|
|
@ -422,14 +422,14 @@ where valid_cap'_def:
|
|||
valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits
|
||||
\<and> f \<le> 2^n \<and> is_aligned (of_nat f :: machine_word) minUntypedSizeBits
|
||||
\<and> canonical_address r \<and> r \<in> kernel_mappings
|
||||
| Structures_H.EndpointCap r badge x y z \<Rightarrow> ep_at' r s
|
||||
| Structures_H.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s
|
||||
| Structures_H.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s
|
||||
| Structures_H.CNodeCap r bits guard guard_sz \<Rightarrow>
|
||||
bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and>
|
||||
guard && mask guard_sz = guard \<and>
|
||||
(\<forall>addr. real_cte_at' (r + 2^cteSizeBits * (addr && mask bits)) s)
|
||||
| Structures_H.ThreadCap r \<Rightarrow> tcb_at' r s
|
||||
| Structures_H.ReplyCap r m \<Rightarrow> tcb_at' r s
|
||||
| Structures_H.ReplyCap r m x \<Rightarrow> tcb_at' r s
|
||||
| Structures_H.IRQControlCap \<Rightarrow> True
|
||||
| Structures_H.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ
|
||||
| Structures_H.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits
|
||||
|
|
@ -474,8 +474,8 @@ definition
|
|||
valid_tcb_state' :: "Structures_H.thread_state \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_tcb_state' ts s \<equiv> case ts of
|
||||
Structures_H.BlockedOnReceive ref \<Rightarrow> ep_at' ref s
|
||||
| Structures_H.BlockedOnSend ref b d c \<Rightarrow> ep_at' ref s
|
||||
Structures_H.BlockedOnReceive ref a \<Rightarrow> ep_at' ref s
|
||||
| Structures_H.BlockedOnSend ref a b d c \<Rightarrow> ep_at' ref s
|
||||
| Structures_H.BlockedOnNotification ref \<Rightarrow> ntfn_at' ref s
|
||||
| _ \<Rightarrow> True"
|
||||
|
||||
|
|
@ -714,14 +714,14 @@ where
|
|||
"capClass (NullCap) = NullClass"
|
||||
| "capClass (DomainCap) = DomainClass"
|
||||
| "capClass (UntypedCap d p n f) = PhysicalClass"
|
||||
| "capClass (EndpointCap ref badge s r g) = PhysicalClass"
|
||||
| "capClass (NotificationCap ref badge s r) = PhysicalClass"
|
||||
| "capClass (EndpointCap ref badge s r g gr) = PhysicalClass"
|
||||
| "capClass (NotificationCap ref badge s r) = PhysicalClass"
|
||||
| "capClass (CNodeCap ref bits g gs) = PhysicalClass"
|
||||
| "capClass (ThreadCap ref) = PhysicalClass"
|
||||
| "capClass (Zombie r b n) = PhysicalClass"
|
||||
| "capClass (IRQControlCap) = IRQClass"
|
||||
| "capClass (IRQHandlerCap irq) = IRQClass"
|
||||
| "capClass (ReplyCap tcb m) = ReplyClass tcb"
|
||||
| "capClass (ReplyCap tcb m g) = ReplyClass tcb"
|
||||
| "capClass (ArchObjectCap cap) = acapClass cap"
|
||||
|
||||
definition
|
||||
|
|
@ -909,10 +909,10 @@ where
|
|||
| "runnable' (Structures_H.Inactive) = False"
|
||||
| "runnable' (Structures_H.Restart) = True"
|
||||
| "runnable' (Structures_H.IdleThreadState) = False"
|
||||
| "runnable' (Structures_H.BlockedOnReceive a) = False"
|
||||
| "runnable' (Structures_H.BlockedOnReceive a b) = False"
|
||||
| "runnable' (Structures_H.BlockedOnReply) = False"
|
||||
| "runnable' (Structures_H.BlockedOnSend a b c d) = False"
|
||||
| "runnable' (Structures_H.BlockedOnNotification x) = False"
|
||||
| "runnable' (Structures_H.BlockedOnSend a b c d e) = False"
|
||||
| "runnable' (Structures_H.BlockedOnNotification x) = False"
|
||||
|
||||
definition
|
||||
inQ :: "domain \<Rightarrow> priority \<Rightarrow> tcb \<Rightarrow> bool"
|
||||
|
|
@ -1373,11 +1373,11 @@ lemma capability_splits[split]:
|
|||
| capability.NullCap \<Rightarrow> f2
|
||||
| capability.NotificationCap x xa xb xc \<Rightarrow> f3 x xa xb xc
|
||||
| capability.IRQHandlerCap x \<Rightarrow> f4 x
|
||||
| capability.EndpointCap x xa xb xc xd \<Rightarrow> f5 x xa xb xc xd
|
||||
| capability.EndpointCap x xa xb xc xd xe \<Rightarrow> f5 x xa xb xc xd xe
|
||||
| capability.DomainCap \<Rightarrow> f6
|
||||
| capability.Zombie x xa xb \<Rightarrow> f7 x xa xb
|
||||
| capability.ArchObjectCap x \<Rightarrow> f8 x
|
||||
| capability.ReplyCap x xa \<Rightarrow> f9 x xa
|
||||
| capability.ReplyCap x xa xb \<Rightarrow> f9 x xa xb
|
||||
| capability.UntypedCap dev x xa xb \<Rightarrow> f10 dev x xa xb
|
||||
| capability.CNodeCap x xa xb xc \<Rightarrow> f11 x xa xb xc
|
||||
| capability.IRQControlCap \<Rightarrow> f12) =
|
||||
|
|
@ -1389,19 +1389,19 @@ lemma capability_splits[split]:
|
|||
P (f3 x31 x32 x33 x34)) \<and>
|
||||
(\<forall>x4. capability = capability.IRQHandlerCap x4 \<longrightarrow>
|
||||
P (f4 x4)) \<and>
|
||||
(\<forall>x51 x52 x53 x54 x55.
|
||||
(\<forall>x51 x52 x53 x54 x55 x56.
|
||||
capability =
|
||||
capability.EndpointCap x51 x52 x53 x54 x55 \<longrightarrow>
|
||||
P (f5 x51 x52 x53 x54 x55)) \<and>
|
||||
capability.EndpointCap x51 x52 x53 x54 x55 x56 \<longrightarrow>
|
||||
P (f5 x51 x52 x53 x54 x55 x56)) \<and>
|
||||
(capability = capability.DomainCap \<longrightarrow> P f6) \<and>
|
||||
(\<forall>x71 x72 x73.
|
||||
capability = capability.Zombie x71 x72 x73 \<longrightarrow>
|
||||
P (f7 x71 x72 x73)) \<and>
|
||||
(\<forall>x8. capability = capability.ArchObjectCap x8 \<longrightarrow>
|
||||
P (f8 x8)) \<and>
|
||||
(\<forall>x91 x92.
|
||||
capability = capability.ReplyCap x91 x92 \<longrightarrow>
|
||||
P (f9 x91 x92)) \<and>
|
||||
(\<forall>x91 x92 x93.
|
||||
capability = capability.ReplyCap x91 x92 x93 \<longrightarrow>
|
||||
P (f9 x91 x92 x93)) \<and>
|
||||
(\<forall>dev x101 x102 x103.
|
||||
capability = capability.UntypedCap dev x101 x102 x103 \<longrightarrow>
|
||||
P (f10 dev x101 x102 x103)) \<and>
|
||||
|
|
@ -1413,11 +1413,11 @@ lemma capability_splits[split]:
|
|||
| capability.NullCap \<Rightarrow> f2
|
||||
| capability.NotificationCap x xa xb xc \<Rightarrow> f3 x xa xb xc
|
||||
| capability.IRQHandlerCap x \<Rightarrow> f4 x
|
||||
| capability.EndpointCap x xa xb xc xd \<Rightarrow> f5 x xa xb xc xd
|
||||
| capability.EndpointCap x xa xb xc xd xe \<Rightarrow> f5 x xa xb xc xd xe
|
||||
| capability.DomainCap \<Rightarrow> f6
|
||||
| capability.Zombie x xa xb \<Rightarrow> f7 x xa xb
|
||||
| capability.ArchObjectCap x \<Rightarrow> f8 x
|
||||
| capability.ReplyCap x xa \<Rightarrow> f9 x xa
|
||||
| capability.ReplyCap x xa xb \<Rightarrow> f9 x xa xb
|
||||
| capability.UntypedCap dev x xa xb \<Rightarrow> f10 dev x xa xb
|
||||
| capability.CNodeCap x xa xb xc \<Rightarrow> f11 x xa xb xc
|
||||
| capability.IRQControlCap \<Rightarrow> f12) =
|
||||
|
|
@ -1430,19 +1430,19 @@ lemma capability_splits[split]:
|
|||
\<not> P (f3 x31 x32 x33 x34)) \<or>
|
||||
(\<exists>x4. capability = capability.IRQHandlerCap x4 \<and>
|
||||
\<not> P (f4 x4)) \<or>
|
||||
(\<exists>x51 x52 x53 x54 x55.
|
||||
(\<exists>x51 x52 x53 x54 x55 x56.
|
||||
capability =
|
||||
capability.EndpointCap x51 x52 x53 x54 x55 \<and>
|
||||
\<not> P (f5 x51 x52 x53 x54 x55)) \<or>
|
||||
capability.EndpointCap x51 x52 x53 x54 x55 x56 \<and>
|
||||
\<not> P (f5 x51 x52 x53 x54 x55 x56)) \<or>
|
||||
capability = capability.DomainCap \<and> \<not> P f6 \<or>
|
||||
(\<exists>x71 x72 x73.
|
||||
capability = capability.Zombie x71 x72 x73 \<and>
|
||||
\<not> P (f7 x71 x72 x73)) \<or>
|
||||
(\<exists>x8. capability = capability.ArchObjectCap x8 \<and>
|
||||
\<not> P (f8 x8)) \<or>
|
||||
(\<exists>x91 x92.
|
||||
capability = capability.ReplyCap x91 x92 \<and>
|
||||
\<not> P (f9 x91 x92)) \<or>
|
||||
(\<exists>x91 x92 x93.
|
||||
capability = capability.ReplyCap x91 x92 x93 \<and>
|
||||
\<not> P (f9 x91 x92 x93)) \<or>
|
||||
(\<exists>x101 x102 x103 dev.
|
||||
capability = capability.UntypedCap dev x101 x102 x103 \<and>
|
||||
\<not> P (f10 dev x101 x102 x103)) \<or>
|
||||
|
|
@ -1455,19 +1455,19 @@ lemma capability_splits[split]:
|
|||
|
||||
lemma thread_state_splits[split]:
|
||||
" P (case thread_state of
|
||||
Structures_H.thread_state.BlockedOnReceive x \<Rightarrow> f1 x
|
||||
Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> f1 x xa
|
||||
| Structures_H.thread_state.BlockedOnReply \<Rightarrow> f2
|
||||
| Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> f3 x
|
||||
| Structures_H.thread_state.Running \<Rightarrow> f4
|
||||
| Structures_H.thread_state.Inactive \<Rightarrow> f5
|
||||
| Structures_H.thread_state.IdleThreadState \<Rightarrow> f6
|
||||
| Structures_H.thread_state.BlockedOnSend x xa xb xc \<Rightarrow>
|
||||
f7 x xa xb xc
|
||||
| Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow>
|
||||
f7 x xa xb xc xd
|
||||
| Structures_H.thread_state.Restart \<Rightarrow> f8) =
|
||||
((\<forall>x11.
|
||||
((\<forall>x11 x12.
|
||||
thread_state =
|
||||
Structures_H.thread_state.BlockedOnReceive x11 \<longrightarrow>
|
||||
P (f1 x11)) \<and>
|
||||
Structures_H.thread_state.BlockedOnReceive x11 x12 \<longrightarrow>
|
||||
P (f1 x11 x12)) \<and>
|
||||
(awaiting_reply' thread_state \<longrightarrow> P f2) \<and>
|
||||
(\<forall>x3. thread_state =
|
||||
Structures_H.thread_state.BlockedOnNotification x3 \<longrightarrow>
|
||||
|
|
@ -1477,26 +1477,26 @@ lemma thread_state_splits[split]:
|
|||
(thread_state = Structures_H.thread_state.Inactive \<longrightarrow>
|
||||
P f5) \<and>
|
||||
(idle' thread_state \<longrightarrow> P f6) \<and>
|
||||
(\<forall>x71 x72 x73 x74.
|
||||
(\<forall>x71 x72 x73 x74 x75.
|
||||
thread_state =
|
||||
Structures_H.thread_state.BlockedOnSend x71 x72 x73
|
||||
x74 \<longrightarrow>
|
||||
P (f7 x71 x72 x73 x74)) \<and>
|
||||
x74 x75 \<longrightarrow>
|
||||
P (f7 x71 x72 x73 x74 x75)) \<and>
|
||||
(thread_state = Structures_H.thread_state.Restart \<longrightarrow> P f8))"
|
||||
"P (case thread_state of
|
||||
Structures_H.thread_state.BlockedOnReceive x \<Rightarrow> f1 x
|
||||
Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> f1 x xa
|
||||
| Structures_H.thread_state.BlockedOnReply \<Rightarrow> f2
|
||||
| Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> f3 x
|
||||
| Structures_H.thread_state.Running \<Rightarrow> f4
|
||||
| Structures_H.thread_state.Inactive \<Rightarrow> f5
|
||||
| Structures_H.thread_state.IdleThreadState \<Rightarrow> f6
|
||||
| Structures_H.thread_state.BlockedOnSend x xa xb xc \<Rightarrow>
|
||||
f7 x xa xb xc
|
||||
| Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow>
|
||||
f7 x xa xb xc xd
|
||||
| Structures_H.thread_state.Restart \<Rightarrow> f8) =
|
||||
(\<not> ((\<exists>x11.
|
||||
(\<not> ((\<exists>x11 x12.
|
||||
thread_state =
|
||||
Structures_H.thread_state.BlockedOnReceive x11 \<and>
|
||||
\<not> P (f1 x11)) \<or>
|
||||
Structures_H.thread_state.BlockedOnReceive x11 x12 \<and>
|
||||
\<not> P (f1 x11 x12)) \<or>
|
||||
awaiting_reply' thread_state \<and> \<not> P f2 \<or>
|
||||
(\<exists>x3. thread_state =
|
||||
Structures_H.thread_state.BlockedOnNotification
|
||||
|
|
@ -1507,11 +1507,11 @@ lemma thread_state_splits[split]:
|
|||
thread_state = Structures_H.thread_state.Inactive \<and>
|
||||
\<not> P f5 \<or>
|
||||
idle' thread_state \<and> \<not> P f6 \<or>
|
||||
(\<exists>x71 x72 x73 x74.
|
||||
(\<exists>x71 x72 x73 x74 x75.
|
||||
thread_state =
|
||||
Structures_H.thread_state.BlockedOnSend x71 x72 x73
|
||||
x74 \<and>
|
||||
\<not> P (f7 x71 x72 x73 x74)) \<or>
|
||||
x74 x75 \<and>
|
||||
\<not> P (f7 x71 x72 x73 x74 x75)) \<or>
|
||||
thread_state = Structures_H.thread_state.Restart \<and>
|
||||
\<not> P f8))"
|
||||
by (case_tac thread_state; simp)+
|
||||
|
|
@ -1677,9 +1677,9 @@ lemma tcb_st_refs_of'_simps[simp]:
|
|||
"tcb_st_refs_of' (Running) = {}"
|
||||
"tcb_st_refs_of' (Inactive) = {}"
|
||||
"tcb_st_refs_of' (Restart) = {}"
|
||||
"\<And>x. tcb_st_refs_of' (BlockedOnReceive x) = {(x, TCBBlockedRecv)}"
|
||||
"\<And>x c. tcb_st_refs_of' (BlockedOnSend x a b c) = {(x, TCBBlockedSend)}"
|
||||
"\<And>x. tcb_st_refs_of' (BlockedOnNotification x) = {(x, TCBSignal)}"
|
||||
"tcb_st_refs_of' (BlockedOnReceive x'' a') = {(x'', TCBBlockedRecv)}"
|
||||
"tcb_st_refs_of' (BlockedOnSend x a b c d) = {(x, TCBBlockedSend)}"
|
||||
"tcb_st_refs_of' (BlockedOnNotification x') = {(x', TCBSignal)}"
|
||||
"tcb_st_refs_of' (BlockedOnReply) = {}"
|
||||
"tcb_st_refs_of' (IdleThreadState) = {}"
|
||||
by (auto simp: tcb_st_refs_of'_def)
|
||||
|
|
@ -1708,9 +1708,9 @@ lemma tcb_bound_refs'_simps[simp]:
|
|||
|
||||
lemma refs_of_rev':
|
||||
"(x, TCBBlockedRecv) \<in> refs_of' ko =
|
||||
(\<exists>tcb. ko = KOTCB tcb \<and> tcbState tcb = BlockedOnReceive x)"
|
||||
(\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = BlockedOnReceive x a))"
|
||||
"(x, TCBBlockedSend) \<in> refs_of' ko =
|
||||
(\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a b c. tcbState tcb = BlockedOnSend x a b c))"
|
||||
(\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a b c d. tcbState tcb = BlockedOnSend x a b c d))"
|
||||
"(x, TCBSignal) \<in> refs_of' ko =
|
||||
(\<exists>tcb. ko = KOTCB tcb \<and> tcbState tcb = BlockedOnNotification x)"
|
||||
"(x, EPRecv) \<in> refs_of' ko =
|
||||
|
|
@ -1745,11 +1745,11 @@ lemma projectKO_opt_tcbD:
|
|||
|
||||
lemma st_tcb_at_refs_of_rev':
|
||||
"ko_wp_at' (\<lambda>ko. (x, TCBBlockedRecv) \<in> refs_of' ko) t s
|
||||
= st_tcb_at' (\<lambda>ts. ts = BlockedOnReceive x ) t s"
|
||||
= st_tcb_at' (\<lambda>ts. \<exists>a. ts = BlockedOnReceive x a) t s"
|
||||
"ko_wp_at' (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of' ko) t s
|
||||
= st_tcb_at' (\<lambda>ts. \<exists>a b c. ts = BlockedOnSend x a b c) t s"
|
||||
= st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = BlockedOnSend x a b c d) t s"
|
||||
"ko_wp_at' (\<lambda>ko. (x, TCBSignal) \<in> refs_of' ko) t s
|
||||
= st_tcb_at' (\<lambda>ts. ts = BlockedOnNotification x) t s"
|
||||
= st_tcb_at' (\<lambda>ts. ts = BlockedOnNotification x) t s"
|
||||
by (fastforce simp: refs_of_rev' pred_tcb_at'_def obj_at'_real_def
|
||||
projectKO_opt_tcb[where e="KOTCB y" for y]
|
||||
elim!: ko_wp_at'_weakenE
|
||||
|
|
@ -1918,14 +1918,13 @@ lemma next_unfold:
|
|||
(case s c of Some cte \<Rightarrow> Some (mdbNext (cteMDBNode cte)) | None \<Rightarrow> None)"
|
||||
by (simp add: mdb_next_def split: option.split)
|
||||
|
||||
lemma
|
||||
is_physical_cases:
|
||||
lemma is_physical_cases:
|
||||
"(capClass cap = PhysicalClass) =
|
||||
(case cap of NullCap \<Rightarrow> False
|
||||
| DomainCap \<Rightarrow> False
|
||||
| IRQControlCap \<Rightarrow> False
|
||||
| IRQHandlerCap irq \<Rightarrow> False
|
||||
| ReplyCap r m \<Rightarrow> False
|
||||
| ReplyCap r m cr \<Rightarrow> False
|
||||
| ArchObjectCap ASIDControlCap \<Rightarrow> False
|
||||
| ArchObjectCap (IOPortCap _ _) \<Rightarrow> False
|
||||
| ArchObjectCap IOPortControlCap \<Rightarrow> False
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ locale delete_one_conc_pre =
|
|||
assumes delete_one_sch_act_not:
|
||||
"\<And>t. \<lbrace>sch_act_not t\<rbrace> cteDeleteOne sl \<lbrace>\<lambda>rv. sch_act_not t\<rbrace>"
|
||||
assumes delete_one_reply_st_tcb_at:
|
||||
"\<And>P t. \<lbrace>\<lambda>s. st_tcb_at' P t s \<and> (\<exists>t'. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False) slot s)\<rbrace>
|
||||
"\<And>P t. \<lbrace>\<lambda>s. st_tcb_at' P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False r) slot s)\<rbrace>
|
||||
cteDeleteOne slot
|
||||
\<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>"
|
||||
assumes delete_one_ksCurDomain:
|
||||
|
|
@ -160,7 +160,7 @@ crunch tcb_at[wp]: set_endpoint "tcb_at t"
|
|||
crunch tcb_at'[wp]: setEndpoint "tcb_at' t"
|
||||
|
||||
lemma blocked_cancel_ipc_corres:
|
||||
"\<lbrakk> st = Structures_A.BlockedOnReceive epPtr \<or>
|
||||
"\<lbrakk> st = Structures_A.BlockedOnReceive epPtr p' \<or>
|
||||
st = Structures_A.BlockedOnSend epPtr p; thread_state_relation st st' \<rbrakk> \<Longrightarrow>
|
||||
corres dc (invs and st_tcb_at ((=) st) t) (invs' and st_tcb_at' ((=) st') t)
|
||||
(blocked_cancel_ipc st t)
|
||||
|
|
@ -360,6 +360,16 @@ lemmas cte_index_repair_sym = cte_index_repair[symmetric]
|
|||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
lemma cte_wp_at_master_reply_cap_to_ex_rights:
|
||||
"cte_wp_at (is_master_reply_cap_to t) ptr
|
||||
= (\<lambda>s. \<exists>rights. cte_wp_at ((=) (cap.ReplyCap t True rights)) ptr s)"
|
||||
by (rule ext, rule iffI; clarsimp simp: cte_wp_at_def is_master_reply_cap_to_def)
|
||||
|
||||
lemma cte_wp_at_reply_cap_to_ex_rights:
|
||||
"cte_wp_at (is_reply_cap_to t) ptr
|
||||
= (\<lambda>s. \<exists>rights. cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s)"
|
||||
by (rule ext, rule iffI; clarsimp simp: cte_wp_at_def is_reply_cap_to_def)
|
||||
|
||||
lemma reply_no_descendants_mdbNext_null:
|
||||
assumes descs: "descendants_of (t, tcb_cnode_index 2) (cdt s) = {}"
|
||||
and sr: "(s, s') \<in> state_relation"
|
||||
|
|
@ -371,12 +381,15 @@ lemma reply_no_descendants_mdbNext_null:
|
|||
shows "mdbNext (cteMDBNode cte) = nullPointer"
|
||||
proof -
|
||||
from invs st_tcb_at_reply_cap_valid[OF tcb]
|
||||
have "cte_wp_at ((=) (cap.ReplyCap t True)) (t, tcb_cnode_index 2) s"
|
||||
by (fastforce simp: cte_wp_at_caps_of_state is_cap_simps)
|
||||
hence "cteCap cte = capability.ReplyCap t True"
|
||||
have "cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s"
|
||||
by (fastforce simp: cte_wp_at_caps_of_state is_cap_simps is_master_reply_cap_to_def)
|
||||
|
||||
hence "\<exists>r. cteCap cte = capability.ReplyCap t True r"
|
||||
using invs sr
|
||||
by (fastforce simp: cte_wp_at_ctes_of cte cte_map_def tcb_cnode_index_def
|
||||
by (fastforce simp: cte_wp_at_master_reply_cap_to_ex_rights
|
||||
cte_wp_at_ctes_of cte cte_map_def tcb_cnode_index_def
|
||||
dest: pspace_relation_cte_wp_at state_relation_pspace_relation)
|
||||
|
||||
hence class_link:
|
||||
"\<forall>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<longrightarrow>
|
||||
capClass (cteCap cte') = ReplyClass t"
|
||||
|
|
@ -388,16 +401,17 @@ proof -
|
|||
apply simp
|
||||
done
|
||||
|
||||
from invs tcb descs have "\<forall>ptr m.
|
||||
cte_wp_at ((=) (cap.ReplyCap t m)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2)"
|
||||
apply (intro allI)
|
||||
from invs tcb descs have "\<forall>ptr m g.
|
||||
cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2)"
|
||||
apply (intro allI impI)
|
||||
apply (case_tac m)
|
||||
apply (clarsimp simp: invs_def valid_state_def valid_reply_masters_def)
|
||||
apply (fastforce simp: has_reply_cap_def
|
||||
dest: st_tcb_at_tcb_at reply_master_no_descendants_no_reply)
|
||||
apply (fastforce simp: invs_def valid_state_def valid_reply_masters_def
|
||||
cte_wp_at_master_reply_cap_to_ex_rights)
|
||||
apply (fastforce simp: has_reply_cap_def cte_wp_at_reply_cap_to_ex_rights
|
||||
dest: reply_master_no_descendants_no_reply elim: st_tcb_at_tcb_at)
|
||||
done
|
||||
hence "\<forall>ptr m mdb.
|
||||
ctes_of s' ptr = Some (CTE (capability.ReplyCap t m) mdb) \<longrightarrow> ptr = t + 2*2^cte_level_bits"
|
||||
hence "\<forall>ptr m mdb r.
|
||||
ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2*2^cte_level_bits"
|
||||
using sr invs
|
||||
apply (intro allI impI)
|
||||
apply (drule(2) pspace_relation_cte_wp_atI
|
||||
|
|
@ -551,14 +565,15 @@ lemma (in delete_one) reply_cancel_ipc_corres:
|
|||
apply (rule hoare_vcg_conj_lift [OF getCTE_inv getCTE_cte_wp_at, simplified])
|
||||
apply (rename_tac cte)
|
||||
apply (rule corres_symb_exec_l [OF _ _ gets_sp])
|
||||
apply (rule_tac F="cap = cap.ReplyCap t True \<and>
|
||||
cteCap cte = capability.ReplyCap t True" in corres_req)
|
||||
apply (rule_tac F="\<exists>r. cap = cap.ReplyCap t True r \<and>
|
||||
cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r)" in corres_req)
|
||||
apply (fastforce simp: cte_wp_at_caps_of_state is_cap_simps
|
||||
dest: st_tcb_at_reply_cap_valid)
|
||||
dest!: st_tcb_at_reply_cap_valid)
|
||||
apply (rule_tac F="(descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer)"
|
||||
in corres_req)
|
||||
apply (fastforce simp: st_tcb_at_tcb_at cte_wp_at_ctes_of st_tcb_def2 cte_index_repair
|
||||
dest: reply_descendants_of_mdbNext)
|
||||
apply (elim exE)
|
||||
apply (case_tac "descs = {}", simp add: when_def)
|
||||
apply (rule_tac F="\<exists>sl. descs = {sl}" in corres_req)
|
||||
apply (fastforce intro: st_tcb_at_tcb_at dest: reply_master_one_descendant)
|
||||
|
|
@ -570,12 +585,12 @@ lemma (in delete_one) reply_cancel_ipc_corres:
|
|||
apply (simp add: when_def getSlotCap_def capHasProperty_def
|
||||
del: split_paired_Ex)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule_tac P'="cte_wp_at ((=) (cap.ReplyCap t False)) sl"
|
||||
apply (rule_tac P'="\<lambda>s. \<exists>r'. cte_wp_at ((=) (cap.ReplyCap t False r')) sl s"
|
||||
in corres_stateAssert_implied [OF delete_one_corres])
|
||||
apply (fastforce dest: pspace_relation_cte_wp_at
|
||||
state_relation_pspace_relation
|
||||
simp: cte_wp_at_ctes_of isCap_simps)
|
||||
apply (clarsimp simp: invs_def valid_state_def valid_mdb_def reply_mdb_def
|
||||
apply (fastforce simp: invs_def valid_state_def valid_mdb_def reply_mdb_def
|
||||
reply_masters_mdb_def cte_wp_at_caps_of_state
|
||||
can_fast_finalise_def)
|
||||
apply (fastforce simp: valid_mdb'_def valid_mdb_ctes_def
|
||||
|
|
@ -812,8 +827,8 @@ proof -
|
|||
apply (wp, simp)
|
||||
done
|
||||
have Q:
|
||||
"\<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. (st = BlockedOnReceive epptr )
|
||||
\<or> (\<exists>a b c. st = BlockedOnSend epptr a b c)) t
|
||||
"\<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. \<exists>a. (st = BlockedOnReceive epptr a)
|
||||
\<or> (\<exists>a b c d. st = BlockedOnSend epptr a b c d)) t
|
||||
and invs'\<rbrace>
|
||||
do ep \<leftarrow> getEndpoint epptr;
|
||||
y \<leftarrow> assert (\<not> (case ep of IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
|
||||
|
|
@ -1890,14 +1905,7 @@ lemma (in delete_one_conc_pre) cancelIPC_queues[wp]:
|
|||
| rule hoare_drop_imps
|
||||
| clarsimp simp: valid_tcb'_def tcb_cte_cases_def
|
||||
elim!: pred_tcb'_weakenE)+
|
||||
apply (safe)
|
||||
apply (drule_tac t=t in valid_queues_not_runnable'_not_ksQ)
|
||||
apply (erule pred_tcb'_weakenE, simp)
|
||||
apply (drule_tac x=xb in spec, simp)
|
||||
apply (erule pred_tcb'_weakenE, simp)
|
||||
apply (drule_tac t=t in valid_queues_not_runnable'_not_ksQ)
|
||||
apply (erule pred_tcb'_weakenE, simp)
|
||||
apply (drule_tac x=xe in spec, simp)
|
||||
apply (fastforce dest: valid_queues_not_runnable'_not_ksQ elim: pred_tcb'_weakenE)
|
||||
done
|
||||
|
||||
(* FIXME: move to Schedule_R *)
|
||||
|
|
|
|||
|
|
@ -1315,7 +1315,7 @@ lemma updateCapData_capReplyMaster:
|
|||
by (clarsimp simp: isCap_simps updateCapData_def split del: if_split)
|
||||
|
||||
lemma updateCapData_is_Reply[simp]:
|
||||
"(updateCapData p d cap = ReplyCap x y) = (cap = ReplyCap x y)"
|
||||
"(updateCapData p d cap = ReplyCap x y z) = (cap = ReplyCap x y z)"
|
||||
by (rule ccontr,
|
||||
clarsimp simp: isCap_simps updateCapData_def Let_def
|
||||
X64_H.updateCapData_def
|
||||
|
|
@ -2192,16 +2192,17 @@ lemma capClass_Reply:
|
|||
done
|
||||
|
||||
lemma reply_cap_end_mdb_chain:
|
||||
"\<lbrakk> cte_wp_at ((=) (cap.ReplyCap t False)) slot s; invs s;
|
||||
"\<lbrakk> cte_wp_at (is_reply_cap_to t) slot s; invs s;
|
||||
invs' s';
|
||||
(s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte \<rbrakk>
|
||||
\<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer
|
||||
\<and> mdbNext (cteMDBNode cte) = nullPointer)
|
||||
\<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte))
|
||||
(mdbPrev (cteMDBNode cte)) s'"
|
||||
apply (clarsimp simp only: cte_wp_at_reply_cap_to_ex_rights)
|
||||
apply (frule(1) pspace_relation_ctes_ofI[OF state_relation_pspace_relation],
|
||||
clarsimp+)
|
||||
apply (subgoal_tac "\<exists>slot'. caps_of_state s slot' = Some (cap.ReplyCap t True)
|
||||
apply (subgoal_tac "\<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights')
|
||||
\<and> descendants_of slot' (cdt s) = {slot}")
|
||||
apply (elim state_relationE exE)
|
||||
apply (clarsimp simp: cdt_relation_def
|
||||
|
|
@ -2247,7 +2248,8 @@ lemma reply_cap_end_mdb_chain:
|
|||
valid_reply_caps_def reply_caps_mdb_def
|
||||
cte_wp_at_caps_of_state
|
||||
simp del: split_paired_All)
|
||||
apply (drule spec, drule spec, drule(1) mp)
|
||||
|
||||
apply (erule_tac x=slot in allE, erule_tac x=t in allE, erule impE, fast)
|
||||
apply (elim exEI)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "P" for P, rule sym, rule equalityI, assumption)
|
||||
|
|
@ -2400,23 +2402,28 @@ lemma restart_rewrite:
|
|||
od"
|
||||
by (simp add: when_def)
|
||||
|
||||
lemma cte_wp_at_is_reply_cap_toI:
|
||||
"cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s
|
||||
\<Longrightarrow> cte_wp_at (is_reply_cap_to t) ptr s"
|
||||
by (fastforce simp: cte_wp_at_reply_cap_to_ex_rights)
|
||||
|
||||
lemma do_reply_transfer_corres:
|
||||
"corres dc
|
||||
(einvs and tcb_at receiver and tcb_at sender
|
||||
and cte_wp_at ((=) (cap.ReplyCap receiver False)) slot)
|
||||
and cte_wp_at ((=) (cap.ReplyCap receiver False rights)) slot)
|
||||
(invs' and tcb_at' sender and tcb_at' receiver
|
||||
and valid_pspace' and cte_at' (cte_map slot))
|
||||
(do_reply_transfer sender receiver slot)
|
||||
(doReplyTransfer sender receiver (cte_map slot))"
|
||||
(do_reply_transfer sender receiver slot grant)
|
||||
(doReplyTransfer sender receiver (cte_map slot) grant)"
|
||||
apply (simp add: do_reply_transfer_def doReplyTransfer_def restart_rewrite cong: option.case_cong)
|
||||
apply (rule corres_split' [OF _ _ gts_sp gts_sp'])
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule gts_corres, (clarsimp simp add: st_tcb_at_tcb_at)+)
|
||||
apply (rule_tac F = "awaiting_reply state" in corres_req)
|
||||
apply (clarsimp simp add: st_tcb_at_def obj_at_def is_tcb)
|
||||
apply (fastforce simp: invs_def valid_state_def
|
||||
apply (fastforce simp: invs_def valid_state_def intro: has_reply_cap_cte_wpD
|
||||
dest: has_reply_cap_cte_wpD
|
||||
dest!: valid_reply_caps_awaiting_reply)
|
||||
dest!: valid_reply_caps_awaiting_reply cte_wp_at_is_reply_cap_toI)
|
||||
apply (case_tac state, simp_all add: bind_assoc)
|
||||
apply (simp add: isReply_def liftM_def)
|
||||
apply (rule corres_symb_exec_r[OF _ getCTE_sp getCTE_inv, rotated])
|
||||
|
|
@ -2428,6 +2435,7 @@ lemma do_reply_transfer_corres:
|
|||
apply assumption
|
||||
apply (rule conjI, assumption)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (drule cte_wp_at_is_reply_cap_toI)
|
||||
apply (erule(4) reply_cap_end_mdb_chain)
|
||||
apply (rule corres_assert_assume[rotated], simp)
|
||||
apply (simp add: getSlotCap_def)
|
||||
|
|
@ -2512,7 +2520,7 @@ lemma do_reply_transfer_corres:
|
|||
apply (clarsimp simp add: invs_def valid_state_def)
|
||||
apply (rule_tac Q="\<lambda>_. tcb_at' sender and tcb_at' receiver and invs'"
|
||||
in hoare_strengthen_post [rotated])
|
||||
apply (auto simp: invs'_def valid_state'_def intro: sch_act_wf_weak)[1]
|
||||
apply (solves\<open>auto simp: invs'_def valid_state'_def\<close>)
|
||||
apply wp
|
||||
apply clarsimp
|
||||
apply (rule conjI)
|
||||
|
|
@ -2524,6 +2532,18 @@ lemma do_reply_transfer_corres:
|
|||
apply (clarsimp)
|
||||
done
|
||||
|
||||
(* when we cannot talk about reply cap rights explicitly (for instance, when a schematic ?rights
|
||||
would be generated too early *)
|
||||
lemma do_reply_transfer_corres':
|
||||
"corres dc
|
||||
(einvs and tcb_at receiver and tcb_at sender
|
||||
and cte_wp_at (is_reply_cap_to receiver) slot)
|
||||
(invs' and tcb_at' sender and tcb_at' receiver
|
||||
and valid_pspace' and cte_at' (cte_map slot))
|
||||
(do_reply_transfer sender receiver slot grant)
|
||||
(doReplyTransfer sender receiver (cte_map slot) grant)"
|
||||
using do_reply_transfer_corres[of receiver sender _ slot]
|
||||
by (fastforce simp add: cte_wp_at_reply_cap_to_ex_rights corres_underlying_def)
|
||||
|
||||
lemma valid_pspace'_splits[elim!]:
|
||||
"valid_pspace' s \<Longrightarrow> valid_objs' s"
|
||||
|
|
@ -2556,22 +2576,23 @@ lemma setup_caller_corres:
|
|||
valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3))
|
||||
(tcb_at' sender and tcb_at' receiver and valid_pspace'
|
||||
and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
|
||||
(setup_caller_cap sender receiver)
|
||||
(setupCallerCap sender receiver)"
|
||||
(setup_caller_cap sender receiver grant)
|
||||
(setupCallerCap sender receiver grant)"
|
||||
supply if_split[split del]
|
||||
apply (simp add: setup_caller_cap_def setupCallerCap_def
|
||||
getThreadReplySlot_def locateSlot_conv
|
||||
getThreadCallerSlot_def)
|
||||
apply (rule stronger_corres_guard_imp)
|
||||
apply (rule corres_split_nor)
|
||||
apply (rule corres_symb_exec_r)
|
||||
apply (rule_tac F="cteCap masterCTE = capability.ReplyCap sender True
|
||||
apply (rule_tac F="\<exists>r. cteCap masterCTE = capability.ReplyCap sender True r
|
||||
\<and> mdbNext (cteMDBNode masterCTE) = nullPointer"
|
||||
in corres_gen_asm2, simp add: isCap_simps)
|
||||
in corres_gen_asm2, clarsimp simp add: isCap_simps)
|
||||
apply (rule corres_symb_exec_r)
|
||||
apply (rule_tac F="rv = capability.NullCap"
|
||||
in corres_gen_asm2, simp)
|
||||
apply (rule cins_corres)
|
||||
apply simp
|
||||
apply (simp split: if_splits)
|
||||
apply (simp add: cte_map_def tcbReplySlot_def
|
||||
tcb_cnode_index_def cte_level_bits_def)
|
||||
apply (simp add: cte_map_def tcbCallerSlot_def
|
||||
|
|
@ -2615,7 +2636,7 @@ lemma getThreadReplySlot_tcb_at'[wp]:
|
|||
by (simp add: getThreadReplySlot_def, wp)
|
||||
|
||||
lemma setupCallerCap_tcb_at'[wp]:
|
||||
"\<lbrace>tcb_at' t\<rbrace> setupCallerCap sender receiver \<lbrace>\<lambda>_. tcb_at' t\<rbrace>"
|
||||
"\<lbrace>tcb_at' t\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>_. tcb_at' t\<rbrace>"
|
||||
by (simp add: setupCallerCap_def, wp hoare_drop_imp)
|
||||
|
||||
crunch ct'[wp]: setupCallerCap "\<lambda>s. P (ksCurThread s)"
|
||||
|
|
@ -2629,7 +2650,7 @@ by (wp sch_act_wf_lift tcb_in_cur_domain'_lift)
|
|||
|
||||
lemma setupCallerCap_sch_act [wp]:
|
||||
"\<lbrace>\<lambda>s. sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
|
||||
setupCallerCap t r \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
|
||||
setupCallerCap t r g \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getSlotCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv)
|
||||
apply (wp getCTE_wp' sts_sch_act' hoare_drop_imps hoare_vcg_all_lift)
|
||||
|
|
@ -2638,7 +2659,7 @@ lemma setupCallerCap_sch_act [wp]:
|
|||
|
||||
lemma setupCallerCap_weak_sch_act_from_sch_act:
|
||||
"\<lbrace>\<lambda>s. sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
|
||||
setupCallerCap t r \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
|
||||
setupCallerCap t r g \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
|
||||
apply (rule hoare_strengthen_post, rule setupCallerCap_sch_act)
|
||||
apply (clarsimp simp: weak_sch_act_wf_def)
|
||||
done
|
||||
|
|
@ -2703,7 +2724,7 @@ lemma send_ipc_corres:
|
|||
shows
|
||||
"corres dc (einvs and st_tcb_at active t and ep_at ep and ex_nonz_cap_to t)
|
||||
(invs' and sch_act_not t and tcb_at' t and ep_at' ep)
|
||||
(send_ipc bl call bg cg t ep) (sendIPC bl call bg cg t ep)"
|
||||
(send_ipc bl call bg cg cgr t ep) (sendIPC bl call bg cg cgr t ep)"
|
||||
proof -
|
||||
show ?thesis
|
||||
apply (insert assms)
|
||||
|
|
@ -2752,20 +2773,17 @@ proof -
|
|||
apply (simp add: isReceive_def split del:if_split)
|
||||
apply (rule corres_split [OF _ gts_corres])
|
||||
apply (rule_tac
|
||||
F="recv_state = Structures_A.BlockedOnReceive ep"
|
||||
F="\<exists>data. recv_state = Structures_A.BlockedOnReceive ep data"
|
||||
in corres_gen_asm)
|
||||
apply (clarsimp simp: case_bool_If case_option_If if3_fold
|
||||
simp del: dc_simp split del: if_split cong: if_cong)
|
||||
apply (rule corres_split [OF _ dit_corres])
|
||||
apply (rule corres_split [OF _ sts_corres])
|
||||
apply (rule corres_split [OF _ possibleSwitchTo_corres])
|
||||
apply (rule corres_split [OF _ threadget_fault_corres])
|
||||
apply (fold when_def)[1]
|
||||
apply (rename_tac fault fault')
|
||||
apply (rule_tac P="call \<or> fault \<noteq> None"
|
||||
and P'="call \<or> fault' \<noteq> None"
|
||||
in corres_symmetric_bool_cases)
|
||||
apply (auto simp: fault_rel_optionation_def)[1]
|
||||
|
||||
apply (rule_tac P="call" and P'="call"
|
||||
in corres_symmetric_bool_cases, blast)
|
||||
apply (simp add: when_def dc_def[symmetric] split del: if_split)
|
||||
apply (rule corres_if2, simp)
|
||||
apply (rule setup_caller_corres)
|
||||
|
|
@ -2798,8 +2816,9 @@ proof -
|
|||
ep_redux_simps' st_tcb_at_tcb_at valid_ep_def
|
||||
cong: list.case_cong)
|
||||
apply (drule(1) sym_refs_obj_atD[where P="\<lambda>ob. ob = e" for e])
|
||||
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_at_reply_cap_valid st_tcb_at_caller_cap_null)
|
||||
apply (fastforce simp: st_tcb_def2 valid_sched_def valid_sched_action_def)
|
||||
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_at_reply_cap_valid
|
||||
st_tcb_def2 valid_sched_def valid_sched_action_def)
|
||||
apply (force simp: st_tcb_def2 dest!: st_tcb_at_caller_cap_null[simplified,rotated])
|
||||
subgoal by (auto simp: valid_ep'_def invs'_def valid_state'_def split: list.split)
|
||||
apply wp+
|
||||
apply (clarsimp simp: ep_at_def2)+
|
||||
|
|
@ -2834,36 +2853,21 @@ proof -
|
|||
apply (rule corres_split [OF _ set_ep_corres])
|
||||
apply (rule corres_split [OF _ gts_corres])
|
||||
apply (rule_tac
|
||||
F="recv_state = Structures_A.BlockedOnReceive ep"
|
||||
F="\<exists>data. recv_state = Structures_A.BlockedOnReceive ep data"
|
||||
in corres_gen_asm)
|
||||
apply (clarsimp simp: isReceive_def case_bool_If
|
||||
split del: if_split cong: if_cong)
|
||||
apply (rule corres_split [OF _ dit_corres])
|
||||
apply (rule corres_split [OF _ sts_corres])
|
||||
apply (rule corres_split [OF _ possibleSwitchTo_corres])
|
||||
apply (rule corres_split [OF _ threadget_fault_corres])
|
||||
apply (rename_tac rv rv')
|
||||
apply (case_tac rv)
|
||||
apply (clarsimp simp: fault_rel_optionation_def when_def split del: if_split)
|
||||
apply (clarsimp simp: fault_rel_optionation_def when_def
|
||||
case_bool_If
|
||||
split del: if_split)
|
||||
apply (fold dc_def)[1]
|
||||
apply (rule corres_if2, simp)
|
||||
apply (rule setup_caller_corres)
|
||||
apply (rule sts_corres, simp)
|
||||
apply wp+
|
||||
apply (rule possibleSwitchTo_corres)
|
||||
apply (simp add: if_apply_def2)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply (simp add: if_apply_def2)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply simp
|
||||
apply ((wp sts_cur_tcb set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at_cases |
|
||||
simp add: if_apply_def2 split del: if_split)+)[1]
|
||||
apply (wp setThreadState_valid_queues' sts_valid_queues sts_weak_sch_act_wf
|
||||
sts_cur_tcb' setThreadState_tcb' sts_st_tcb_at'_cases)
|
||||
apply (simp add: valid_tcb_state_def pred_conj_def)
|
||||
apply (strengthen reply_cap_doesnt_exist_strg disjI2_strg)
|
||||
apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift
|
||||
| clarsimp simp:is_cap_simps)+)[1]
|
||||
apply (simp add: valid_tcb_state'_def pred_conj_def)
|
||||
|
|
@ -3582,8 +3586,6 @@ lemma receive_ipc_corres:
|
|||
apply (rule corres_split [OF _ dit_corres])
|
||||
apply (simp split del: if_split cong: if_cong)
|
||||
apply (fold dc_def)[1]
|
||||
apply (rule corres_split [OF _ threadget_fault_corres
|
||||
thread_get_inv threadGet_inv])
|
||||
apply (rule_tac P="valid_objs and valid_mdb and valid_list
|
||||
and valid_sched
|
||||
and cur_tcb
|
||||
|
|
@ -3848,7 +3850,7 @@ crunch cur_tcb[wp]: setupCallerCap "cur_tcb'"
|
|||
(wp: crunch_wps)
|
||||
|
||||
lemma setupCallerCap_valid_objs[wp]:
|
||||
"\<lbrace>valid_objs' and tcb_at' sender\<rbrace> setupCallerCap sender receiver \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
|
||||
"\<lbrace>valid_objs' and tcb_at' sender\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def)
|
||||
apply (rule hoare_pre)
|
||||
|
|
@ -3861,7 +3863,7 @@ lemma setupCallerCap_valid_objs[wp]:
|
|||
|
||||
lemma setupCallerCap_state_refs_of[wp]:
|
||||
"\<lbrace>\<lambda>s. P ((state_refs_of' s) (sender := {r \<in> state_refs_of' s sender. snd r = TCBBound}))\<rbrace>
|
||||
setupCallerCap sender rcvr
|
||||
setupCallerCap sender rcvr grant
|
||||
\<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def)
|
||||
|
|
@ -3888,7 +3890,7 @@ crunch vq[wp]: getThreadReplySlot "Invariants_H.valid_queues"
|
|||
|
||||
lemma setupCallerCap_vq[wp]:
|
||||
"\<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>p. send \<notin> set (ksReadyQueues s p))\<rbrace>
|
||||
setupCallerCap send recv \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
|
||||
setupCallerCap send recv grant \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def)
|
||||
apply (wp crunch_wps sts_valid_queues)
|
||||
apply (fastforce simp: valid_queues_def obj_at'_def inQ_def)
|
||||
|
|
@ -3898,7 +3900,8 @@ crunch vq'[wp]: setupCallerCap "valid_queues'"
|
|||
(wp: crunch_wps)
|
||||
|
||||
lemma is_derived_ReplyCap' [simp]:
|
||||
"\<And>m p. is_derived' m p (capability.ReplyCap t False) = (\<lambda>c. c = capability.ReplyCap t True)"
|
||||
"\<And>m p g. is_derived' m p (capability.ReplyCap t False g) =
|
||||
(\<lambda>c. \<exists> g. c = capability.ReplyCap t True g)"
|
||||
apply (subst fun_eq_iff)
|
||||
apply clarsimp
|
||||
apply (case_tac x, simp_all add: is_derived'_def isCap_simps
|
||||
|
|
@ -3907,7 +3910,8 @@ lemma is_derived_ReplyCap' [simp]:
|
|||
done
|
||||
|
||||
lemma unique_master_reply_cap':
|
||||
"\<And>c t. (isReplyCap c \<and> capReplyMaster c \<and> capTCBPtr c = t) = (c = capability.ReplyCap t True)"
|
||||
"\<And>c t. isReplyCap c \<and> capReplyMaster c \<and> capTCBPtr c = t \<longleftrightarrow>
|
||||
(\<exists>g . c = capability.ReplyCap t True g)"
|
||||
by (fastforce simp: isCap_simps conj_comms)
|
||||
|
||||
lemma getSlotCap_cte_wp_at:
|
||||
|
|
@ -3921,7 +3925,7 @@ crunch no_0_obj'[wp]: setThreadState no_0_obj'
|
|||
|
||||
lemma setupCallerCap_vp[wp]:
|
||||
"\<lbrace>valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace>
|
||||
setupCallerCap sender rcvr \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
|
||||
setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
|
||||
apply (simp add: valid_pspace'_def setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv getSlotCap_def)
|
||||
apply (wp getCTE_wp)
|
||||
|
|
@ -3939,23 +3943,25 @@ declare haskell_assert_inv[wp del]
|
|||
|
||||
lemma setupCallerCap_iflive[wp]:
|
||||
"\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' sender\<rbrace>
|
||||
setupCallerCap sender rcvr
|
||||
setupCallerCap sender rcvr grant
|
||||
\<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
|
||||
unfolding setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv
|
||||
by (wp getSlotCap_cte_wp_at
|
||||
| simp add: unique_master_reply_cap'
|
||||
| strengthen eq_imp_strg)+
|
||||
| strengthen eq_imp_strg
|
||||
| wp_once hoare_drop_imp[where f="getCTE rs" for rs])+
|
||||
|
||||
lemma setupCallerCap_ifunsafe[wp]:
|
||||
"\<lbrace>if_unsafe_then_cap' and valid_objs' and
|
||||
ex_nonz_cap_to' rcvr and tcb_at' rcvr\<rbrace>
|
||||
setupCallerCap sender rcvr
|
||||
setupCallerCap sender rcvr grant
|
||||
\<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>"
|
||||
unfolding setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv
|
||||
apply (wp getSlotCap_cte_wp_at
|
||||
| simp add: unique_master_reply_cap' | strengthen eq_imp_strg)+
|
||||
| simp add: unique_master_reply_cap' | strengthen eq_imp_strg
|
||||
| wp_once hoare_drop_imp[where f="getCTE rs" for rs])+
|
||||
apply (rule_tac Q="\<lambda>rv. valid_objs' and tcb_at' rcvr and ex_nonz_cap_to' rcvr"
|
||||
in hoare_post_imp)
|
||||
apply (clarsimp simp: ex_nonz_tcb_cte_caps' tcbCallerSlot_def
|
||||
|
|
@ -3966,13 +3972,17 @@ lemma setupCallerCap_ifunsafe[wp]:
|
|||
|
||||
lemma setupCallerCap_global_refs'[wp]:
|
||||
"\<lbrace>valid_global_refs'\<rbrace>
|
||||
setupCallerCap sender rcvr \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>"
|
||||
setupCallerCap sender rcvr grant
|
||||
\<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>"
|
||||
unfolding setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv
|
||||
by (wp getSlotCap_cte_wp_at
|
||||
apply (wp getSlotCap_cte_wp_at
|
||||
| simp add: o_def unique_master_reply_cap'
|
||||
| strengthen eq_imp_strg
|
||||
| wp_once getCTE_wp | clarsimp simp: cte_wp_at_ctes_of)+
|
||||
(* at setThreadState *)
|
||||
apply (rule_tac Q="\<lambda>_. valid_global_refs'" in hoare_post_imp, wpsimp+)
|
||||
done
|
||||
|
||||
crunch valid_arch'[wp]: setupCallerCap "valid_arch_state'"
|
||||
(wp: hoare_drop_imps)
|
||||
|
|
@ -3984,7 +3994,7 @@ crunch irq_node'[wp]: setupCallerCap "\<lambda>s. P (irq_node' s)"
|
|||
|
||||
lemma setupCallerCap_irq_handlers'[wp]:
|
||||
"\<lbrace>valid_irq_handlers'\<rbrace>
|
||||
setupCallerCap sender rcvr
|
||||
setupCallerCap sender rcvr grant
|
||||
\<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>"
|
||||
unfolding setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv
|
||||
|
|
@ -3996,7 +4006,7 @@ lemma safe_ioport_insert'_not_ioport:
|
|||
|
||||
lemma setupCallerCap_ioports'[wp]:
|
||||
"\<lbrace>valid_ioports'\<rbrace>
|
||||
setupCallerCap sender rcvr
|
||||
setupCallerCap sender rcvr grant
|
||||
\<lbrace>\<lambda>rv. valid_ioports'\<rbrace>"
|
||||
unfolding setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def locateSlot_conv
|
||||
|
|
@ -4042,7 +4052,7 @@ crunch it[wp]: setupCallerCap "\<lambda>s. P (ksIdleThread s)"
|
|||
lemma setupCallerCap_idle'[wp]:
|
||||
"\<lbrace>valid_idle' and valid_pspace' and
|
||||
(\<lambda>s. st \<noteq> ksIdleThread s \<and> rt \<noteq> ksIdleThread s)\<rbrace>
|
||||
setupCallerCap st rt
|
||||
setupCallerCap st rt gr
|
||||
\<lbrace>\<lambda>_. valid_idle'\<rbrace>"
|
||||
by (simp add: setupCallerCap_def capRange_def | wp hoare_drop_imps)+
|
||||
|
||||
|
|
@ -4065,7 +4075,7 @@ crunch ct_not_inQ[wp]: getThreadCallerSlot "ct_not_inQ"
|
|||
crunch ct_not_inQ[wp]: getThreadReplySlot "ct_not_inQ"
|
||||
|
||||
lemma setupCallerCap_ct_not_inQ[wp]:
|
||||
"\<lbrace>ct_not_inQ\<rbrace> setupCallerCap sender receiver \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
|
||||
"\<lbrace>ct_not_inQ\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def)
|
||||
apply (wp hoare_drop_imp setThreadState_ct_not_inQ)
|
||||
done
|
||||
|
|
@ -4141,7 +4151,7 @@ lemma completeSignal_invs:
|
|||
|
||||
lemma setupCallerCap_urz[wp]:
|
||||
"\<lbrace>untyped_ranges_zero' and valid_pspace' and tcb_at' sender\<rbrace>
|
||||
setupCallerCap sender t \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>"
|
||||
setupCallerCap sender t g \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getSlotCap_def
|
||||
getThreadCallerSlot_def getThreadReplySlot_def
|
||||
locateSlot_conv)
|
||||
|
|
@ -4449,7 +4459,7 @@ apply (wp sch_act_wf_lift valid_queues_lift
|
|||
done
|
||||
|
||||
lemma setupCallerCap_cap_to' [wp]:
|
||||
"\<lbrace>ex_nonz_cap_to' p\<rbrace> setupCallerCap a b \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
|
||||
"\<lbrace>ex_nonz_cap_to' p\<rbrace> setupCallerCap a b c \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getThreadCallerSlot_def getThreadReplySlot_def)
|
||||
apply (wp cteInsert_cap_to')
|
||||
apply (rule_tac Q="\<lambda>rv. ex_nonz_cap_to' p
|
||||
|
|
@ -4461,7 +4471,7 @@ lemma setupCallerCap_cap_to' [wp]:
|
|||
done
|
||||
|
||||
lemma setupCaller_pred_tcb_recv':
|
||||
"\<lbrace>pred_tcb_at' proj P r and K (s \<noteq> r)\<rbrace> setupCallerCap s r \<lbrace>\<lambda>_. pred_tcb_at' proj P r\<rbrace>"
|
||||
"\<lbrace>pred_tcb_at' proj P r and K (s \<noteq> r)\<rbrace> setupCallerCap s r g \<lbrace>\<lambda>_. pred_tcb_at' proj P r\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getThreadCallerSlot_def getSlotCap_def
|
||||
getThreadReplySlot_def locateSlot_conv)
|
||||
apply (wp getCTE_wp' hoare_drop_imps hoare_vcg_all_lift sts_pred_tcb_neq')
|
||||
|
|
@ -4489,8 +4499,9 @@ lemma si_invs'[wp]:
|
|||
and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))
|
||||
and sch_act_not t
|
||||
and ex_nonz_cap_to' ep and ex_nonz_cap_to' t\<rbrace>
|
||||
sendIPC bl call ba cg t ep
|
||||
sendIPC bl call ba cg cgr t ep
|
||||
\<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
supply if_split[split del]
|
||||
apply (simp add: sendIPC_def split del: if_split)
|
||||
apply (rule hoare_seq_ext [OF _ get_ep_sp'])
|
||||
apply (case_tac epa)
|
||||
|
|
@ -4510,12 +4521,15 @@ lemma si_invs'[wp]:
|
|||
hoare_convert_imp [OF setEndpoint_nosch setEndpoint_ct']
|
||||
hoare_drop_imp [where f="threadGet tcbFault t"]
|
||||
| rule_tac f="getThreadState a" in hoare_drop_imp
|
||||
| wp_once hoare_drop_imp[where R="\<lambda>_ _. call"]
|
||||
hoare_drop_imp[where R="\<lambda>_ _. \<not> call"]
|
||||
hoare_drop_imp[where R="\<lambda>_ _. cg"]
|
||||
| simp add: valid_tcb_state'_def case_bool_If
|
||||
case_option_If
|
||||
cong: if_cong
|
||||
split del: if_split
|
||||
| wp_once sch_act_sane_lift tcb_in_cur_domain'_lift)+
|
||||
apply (clarsimp simp: pred_tcb_at'
|
||||
| wp_once sch_act_sane_lift tcb_in_cur_domain'_lift hoare_vcg_const_imp_lift)+
|
||||
apply (clarsimp simp: pred_tcb_at' cong: conj_cong imp_cong
|
||||
split del: if_split)
|
||||
apply (frule obj_at_valid_objs', clarsimp)
|
||||
apply (frule(1) sym_refs_ko_atD')
|
||||
|
|
@ -4525,18 +4539,20 @@ lemma si_invs'[wp]:
|
|||
split del: if_split)
|
||||
apply (frule pred_tcb_at')
|
||||
apply (drule simple_st_tcb_at_state_refs_ofD' st_tcb_at_state_refs_ofD')+
|
||||
apply (clarsimp simp: valid_pspace'_splits)
|
||||
apply (subst fun_upd_idem[where x=t])
|
||||
apply clarsimp
|
||||
apply (clarsimp split: if_split)
|
||||
apply (rule conjI, clarsimp simp: obj_at'_def projectKOs)
|
||||
apply (drule bound_tcb_at_state_refs_ofD')
|
||||
apply (fastforce simp: tcb_bound_refs'_def)
|
||||
apply (clarsimp split del: if_split)
|
||||
apply (rule conjI, clarsimp)+
|
||||
apply (rule conjI)
|
||||
apply (subgoal_tac "ex_nonz_cap_to' a s")
|
||||
prefer 2
|
||||
apply (clarsimp elim!: if_live_state_refsE)
|
||||
apply clarsimp
|
||||
apply (rule conjI)
|
||||
apply (drule bound_tcb_at_state_refs_ofD')
|
||||
apply (fastforce simp: tcb_bound_refs'_def set_eq_subset)
|
||||
apply (clarsimp simp: conj_ac)
|
||||
apply (rule conjI, clarsimp simp: idle'_no_refs)
|
||||
apply (rule conjI, clarsimp simp: global'_no_ex_cap)
|
||||
apply (rule conjI)
|
||||
|
|
@ -4544,12 +4560,11 @@ lemma si_invs'[wp]:
|
|||
apply (frule(1) ct_not_in_epQueue, clarsimp, clarsimp)
|
||||
apply (clarsimp)
|
||||
apply (simp add: ep_redux_simps')
|
||||
apply (rule conjI, fastforce simp: tcb_bound_refs'_def set_eq_subset)
|
||||
apply (clarsimp, rule conjI, erule delta_sym_refs)
|
||||
apply (auto simp: symreftype_inverse' tcb_bound_refs'_def split: if_split_asm)[2]
|
||||
apply (rule conjI, clarsimp split: list.splits)
|
||||
apply (erule delta_sym_refs)
|
||||
apply (auto simp: symreftype_inverse' tcb_bound_refs'_def split: if_split_asm)[2]
|
||||
apply (rule conjI, clarsimp split: if_split)
|
||||
apply (rule conjI, fastforce simp: tcb_bound_refs'_def set_eq_subset)
|
||||
apply (clarsimp, erule delta_sym_refs;
|
||||
solves\<open>auto simp: symreftype_inverse' tcb_bound_refs'_def split: if_split_asm\<close>)
|
||||
apply (solves\<open>clarsimp split: list.splits\<close>)
|
||||
\<comment> \<open>epa = IdleEP\<close>
|
||||
apply (cases bl)
|
||||
apply (simp add: invs'_def valid_state'_def)
|
||||
|
|
@ -4725,7 +4740,7 @@ declare setEndpoint_ct' [wp]
|
|||
|
||||
lemma setupCallerCap_pred_tcb_unchanged:
|
||||
"\<lbrace>pred_tcb_at' proj P t and K (t \<noteq> t')\<rbrace>
|
||||
setupCallerCap t' t''
|
||||
setupCallerCap t' t'' g
|
||||
\<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>"
|
||||
apply (simp add: setupCallerCap_def getThreadCallerSlot_def
|
||||
getThreadReplySlot_def)
|
||||
|
|
@ -4735,7 +4750,7 @@ lemma setupCallerCap_pred_tcb_unchanged:
|
|||
|
||||
lemma si_blk_makes_simple':
|
||||
"\<lbrace>st_tcb_at' simple' t and K (t \<noteq> t')\<rbrace>
|
||||
sendIPC True call bdg x t' ep
|
||||
sendIPC True call bdg x x' t' ep
|
||||
\<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>"
|
||||
apply (simp add: sendIPC_def)
|
||||
apply (rule hoare_seq_ext [OF _ get_ep_inv'])
|
||||
|
|
@ -4755,7 +4770,7 @@ lemma si_blk_makes_simple':
|
|||
|
||||
lemma si_blk_makes_runnable':
|
||||
"\<lbrace>st_tcb_at' runnable' t and K (t \<noteq> t')\<rbrace>
|
||||
sendIPC True call bdg x t' ep
|
||||
sendIPC True call bdg x x' t' ep
|
||||
\<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace>"
|
||||
apply (simp add: sendIPC_def)
|
||||
apply (rule hoare_seq_ext [OF _ get_ep_inv'])
|
||||
|
|
@ -4781,8 +4796,8 @@ lemma sfi_makes_simple':
|
|||
apply (rule hoare_gen_asm)
|
||||
apply (simp add: sendFaultIPC_def
|
||||
cong: if_cong capability.case_cong bool.case_cong)
|
||||
apply (wp si_blk_makes_simple' threadSet_pred_tcb_no_state hoare_drop_imps
|
||||
| wpc | simp)+
|
||||
apply (wpsimp wp: si_blk_makes_simple' threadSet_pred_tcb_no_state hoare_drop_imps
|
||||
hoare_vcg_all_lift_R)
|
||||
done
|
||||
|
||||
lemma sfi_makes_runnable':
|
||||
|
|
@ -4792,8 +4807,8 @@ lemma sfi_makes_runnable':
|
|||
apply (rule hoare_gen_asm)
|
||||
apply (simp add: sendFaultIPC_def
|
||||
cong: if_cong capability.case_cong bool.case_cong)
|
||||
apply (wp si_blk_makes_runnable' threadSet_pred_tcb_no_state hoare_drop_imps
|
||||
| wpc | simp)+
|
||||
apply (wpsimp wp: si_blk_makes_runnable' threadSet_pred_tcb_no_state hoare_drop_imps
|
||||
hoare_vcg_all_lift_R)
|
||||
done
|
||||
|
||||
lemma hf_makes_runnable_simple':
|
||||
|
|
@ -4828,17 +4843,13 @@ lemma ri_makes_runnable_simple':
|
|||
apply (rule hoare_pre)
|
||||
apply (wp sts_st_tcb_at'_cases setupCallerCap_pred_tcb_unchanged
|
||||
hoare_vcg_const_imp_lift)+
|
||||
apply (rule_tac Q="\<lambda>_. st_tcb_at' P t' and K (a \<noteq> t')"
|
||||
in hoare_post_imp)
|
||||
apply (clarsimp simp: pred_tcb_at'_def obj_at'_def)
|
||||
apply (wp threadGet_inv static_imp_wp)+
|
||||
apply (simp, simp only: imp_conv_disj)
|
||||
apply (wp hoare_vcg_disj_lift)+
|
||||
apply (clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs)
|
||||
apply (fastforce simp: pred_tcb_at'_def obj_at'_def isSend_def
|
||||
split: Structures_H.thread_state.split_asm)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc | clarsimp)+
|
||||
apply wpsimp+
|
||||
done
|
||||
|
||||
lemma rai_makes_runnable_simple':
|
||||
|
|
|
|||
|
|
@ -1249,7 +1249,7 @@ crunch no_orphans [wp]: getThreadReplySlot "no_orphans"
|
|||
|
||||
lemma setupCallerCap_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
|
||||
setupCallerCap sender receiver
|
||||
setupCallerCap sender receiver gr
|
||||
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
|
||||
unfolding setupCallerCap_def
|
||||
apply (wp setThreadState_not_active_no_orphans
|
||||
|
|
@ -1265,7 +1265,7 @@ crunch almost_no_orphans [wp]: getThreadReplySlot "almost_no_orphans tcb_ptr"
|
|||
|
||||
lemma setupCallerCap_almost_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and> valid_queues' s \<rbrace>
|
||||
setupCallerCap sender receiver
|
||||
setupCallerCap sender receiver gr
|
||||
\<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>"
|
||||
unfolding setupCallerCap_def
|
||||
apply (wp setThreadState_not_active_almost_no_orphans
|
||||
|
|
@ -1286,7 +1286,7 @@ crunch no_orphans [wp]: setEndpoint "no_orphans"
|
|||
|
||||
lemma sendIPC_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<rbrace>
|
||||
sendIPC blocking call badge canGrant thread epptr
|
||||
sendIPC blocking call badge canGrant canGrantReply thread epptr
|
||||
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
|
||||
unfolding sendIPC_def
|
||||
apply (wp hoare_drop_imps setThreadState_not_active_no_orphans sts_st_tcb'
|
||||
|
|
@ -1317,12 +1317,11 @@ lemma sendFaultIPC_no_orphans [wp]:
|
|||
|
||||
lemma sendIPC_valid_queues' [wp]:
|
||||
"\<lbrace> \<lambda>s. valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<rbrace>
|
||||
sendIPC blocking call badge canGrant thread epptr
|
||||
sendIPC blocking call badge canGrant canGrantReply thread epptr
|
||||
\<lbrace> \<lambda>rv s. valid_queues' s \<rbrace>"
|
||||
unfolding sendIPC_def
|
||||
apply (wp hoare_drop_imps | wpc | clarsimp)+
|
||||
apply (wp_once sts_st_tcb', clarsimp)
|
||||
apply (wp)+
|
||||
apply (wpsimp wp: hoare_drop_imps)
|
||||
apply (wpsimp | wp_once sts_st_tcb')+
|
||||
apply (rule_tac Q="\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr
|
||||
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp)
|
||||
apply (clarsimp)
|
||||
|
|
@ -1956,7 +1955,7 @@ crunch valid_queues' [wp]: handleFaultReply "valid_queues'"
|
|||
|
||||
lemma doReplyTransfer_no_orphans[wp]:
|
||||
"\<lbrace>no_orphans and invs' and tcb_at' sender and tcb_at' receiver\<rbrace>
|
||||
doReplyTransfer sender receiver slot
|
||||
doReplyTransfer sender receiver slot grant
|
||||
\<lbrace>\<lambda>rv. no_orphans\<rbrace>"
|
||||
unfolding doReplyTransfer_def
|
||||
apply (wp sts_st_tcb' setThreadState_not_active_no_orphans threadSet_no_orphans
|
||||
|
|
|
|||
|
|
@ -103,19 +103,19 @@ where
|
|||
Structures_H.NullCap)"
|
||||
| "cap_relation Structures_A.DomainCap c = (c =
|
||||
Structures_H.DomainCap)"
|
||||
| "cap_relation (Structures_A.UntypedCap dev ref n f) c = (c =
|
||||
| "cap_relation (Structures_A.UntypedCap dev ref n f) c = (c =
|
||||
Structures_H.UntypedCap dev ref n f)"
|
||||
| "cap_relation (Structures_A.EndpointCap ref b r) c = (c =
|
||||
Structures_H.EndpointCap ref b (AllowSend \<in> r)
|
||||
(AllowRecv \<in> r) (AllowGrant \<in> r))"
|
||||
| "cap_relation (Structures_A.NotificationCap ref b r) c = (c =
|
||||
(AllowRecv \<in> r) (AllowGrant \<in> r) (AllowGrantReply \<in> r))"
|
||||
| "cap_relation (Structures_A.NotificationCap ref b r) c = (c =
|
||||
Structures_H.NotificationCap ref b (AllowSend \<in> r) (AllowRecv \<in> r))"
|
||||
| "cap_relation (Structures_A.CNodeCap ref n L) c = (c =
|
||||
| "cap_relation (Structures_A.CNodeCap ref n L) c = (c =
|
||||
Structures_H.CNodeCap ref n (of_bl L) (length L))"
|
||||
| "cap_relation (Structures_A.ThreadCap ref) c = (c =
|
||||
Structures_H.ThreadCap ref)"
|
||||
| "cap_relation (Structures_A.ReplyCap ref master) c = (c =
|
||||
Structures_H.ReplyCap ref master)"
|
||||
| "cap_relation (Structures_A.ReplyCap ref master r) c = (c =
|
||||
Structures_H.ReplyCap ref master (AllowGrant \<in> r))"
|
||||
| "cap_relation (Structures_A.IRQControlCap) c = (c =
|
||||
Structures_H.IRQControlCap)"
|
||||
| "cap_relation (Structures_A.IRQHandlerCap irq) c = (c =
|
||||
|
|
@ -173,11 +173,11 @@ where
|
|||
= (ts' = Structures_H.IdleThreadState)"
|
||||
| "thread_state_relation (Structures_A.BlockedOnReply) ts'
|
||||
= (ts' = Structures_H.BlockedOnReply)"
|
||||
| "thread_state_relation (Structures_A.BlockedOnReceive oref) ts'
|
||||
= (ts' = Structures_H.BlockedOnReceive oref)"
|
||||
| "thread_state_relation (Structures_A.BlockedOnReceive oref sp) ts'
|
||||
= (ts' = Structures_H.BlockedOnReceive oref (receiver_can_grant sp))"
|
||||
| "thread_state_relation (Structures_A.BlockedOnSend oref sp) ts'
|
||||
= (ts' = Structures_H.BlockedOnSend oref (sender_badge sp)
|
||||
(sender_can_grant sp) (sender_is_call sp))"
|
||||
(sender_can_grant sp) (sender_can_grant_reply sp) (sender_is_call sp))"
|
||||
| "thread_state_relation (Structures_A.BlockedOnNotification oref) ts'
|
||||
= (ts' = Structures_H.BlockedOnNotification oref)"
|
||||
|
||||
|
|
@ -500,10 +500,10 @@ where
|
|||
\<and> x64_irq_relation (x64_irq_state s) (x64KSIRQState s')}"
|
||||
|
||||
definition
|
||||
(* NOTE: this map discards the Ident right, needed on endpoints only *)
|
||||
rights_mask_map :: "rights set \<Rightarrow> Types_H.cap_rights"
|
||||
where
|
||||
"rights_mask_map \<equiv> \<lambda>rs. CapRights (AllowWrite \<in> rs) (AllowRead \<in> rs) (AllowGrant \<in> rs)"
|
||||
"rights_mask_map \<equiv> \<lambda>rs. CapRights (AllowWrite \<in> rs) (AllowRead \<in> rs) (AllowGrant \<in> rs)
|
||||
(AllowGrantReply \<in> rs)"
|
||||
|
||||
|
||||
lemma obj_relation_cutsE:
|
||||
|
|
|
|||
|
|
@ -88,12 +88,12 @@ primrec
|
|||
where
|
||||
"inv_relation (Invocations_A.InvokeUntyped i) x =
|
||||
(\<exists>i'. untypinv_relation i i' \<and> x = InvokeUntyped i')"
|
||||
| "inv_relation (Invocations_A.InvokeEndpoint w w2 b) x =
|
||||
(x = InvokeEndpoint w w2 b)"
|
||||
| "inv_relation (Invocations_A.InvokeEndpoint w w2 b c) x =
|
||||
(x = InvokeEndpoint w w2 b c)"
|
||||
| "inv_relation (Invocations_A.InvokeNotification w w2) x =
|
||||
(x = InvokeNotification w w2)"
|
||||
| "inv_relation (Invocations_A.InvokeReply w ptr) x =
|
||||
(x = InvokeReply w (cte_map ptr))"
|
||||
| "inv_relation (Invocations_A.InvokeReply w ptr grant) x =
|
||||
(x = InvokeReply w (cte_map ptr) grant)"
|
||||
| "inv_relation (Invocations_A.InvokeTCB i) x =
|
||||
(\<exists>i'. tcbinv_relation i i' \<and> x = InvokeTCB i')"
|
||||
| "inv_relation (Invocations_A.InvokeDomain tptr domain) x =
|
||||
|
|
@ -118,13 +118,13 @@ primrec
|
|||
valid_invocation' :: "Invocations_H.invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_invocation' (Invocations_H.InvokeUntyped i) = valid_untyped_inv' i"
|
||||
| "valid_invocation' (Invocations_H.InvokeEndpoint w w2 b) = (ep_at' w and ex_nonz_cap_to' w)"
|
||||
| "valid_invocation' (Invocations_H.InvokeEndpoint w w2 b c) = (ep_at' w and ex_nonz_cap_to' w)"
|
||||
| "valid_invocation' (Invocations_H.InvokeNotification w w2) = (ntfn_at' w and ex_nonz_cap_to' w)"
|
||||
| "valid_invocation' (Invocations_H.InvokeTCB i) = tcb_inv_wf' i"
|
||||
| "valid_invocation' (Invocations_H.InvokeDomain thread domain) =
|
||||
(tcb_at' thread and K (domain \<le> maxDomain))"
|
||||
| "valid_invocation' (Invocations_H.InvokeReply thread slot) =
|
||||
(tcb_at' thread and cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap thread False) slot)"
|
||||
| "valid_invocation' (Invocations_H.InvokeReply thread slot grant) =
|
||||
(tcb_at' thread and cte_wp_at' (\<lambda>cte. \<exists>gr. cteCap cte = ReplyCap thread False gr) slot)"
|
||||
| "valid_invocation' (Invocations_H.InvokeIRQControl i) = irq_control_inv_valid' i"
|
||||
| "valid_invocation' (Invocations_H.InvokeIRQHandler i) = irq_handler_inv_valid' i"
|
||||
| "valid_invocation' (Invocations_H.InvokeCNode i) = valid_cnode_inv' i"
|
||||
|
|
@ -491,7 +491,7 @@ lemma pinv_corres:
|
|||
(einvs and valid_invocation i
|
||||
and simple_sched_action
|
||||
and ct_active
|
||||
and (\<lambda>s. (\<exists>w w2 b. i = Invocations_A.InvokeEndpoint w w2 b) \<longrightarrow> st_tcb_at simple (cur_thread s) s))
|
||||
and (\<lambda>s. (\<exists>w w2 b c. i = Invocations_A.InvokeEndpoint w w2 b c) \<longrightarrow> st_tcb_at simple (cur_thread s) s))
|
||||
(invs' and sch_act_simple and valid_invocation' i' and ct_active')
|
||||
(perform_invocation block call i) (performInvocation block call i')"
|
||||
apply (simp add: performInvocation_def)
|
||||
|
|
@ -527,11 +527,12 @@ lemma pinv_corres:
|
|||
apply simp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_eqr [OF _ gct_corres])
|
||||
apply (rule corres_split_nor [OF _ do_reply_transfer_corres])
|
||||
apply (rule corres_split_nor [OF _ do_reply_transfer_corres'])
|
||||
apply (rule corres_trivial, simp)
|
||||
apply wp+
|
||||
apply (clarsimp simp: tcb_at_invs)
|
||||
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def)
|
||||
apply (erule cte_wp_at_weakenE, fastforce simp: is_reply_cap_to_def)
|
||||
apply (clarsimp simp: tcb_at_invs')
|
||||
apply (fastforce elim!: cte_wp_at_weakenE')
|
||||
apply (clarsimp simp: liftME_def)
|
||||
|
|
@ -714,15 +715,6 @@ lemma diminished_IRQHandler' [simp]:
|
|||
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
lemma diminished_ReplyCap' [simp]:
|
||||
"diminished' (ReplyCap x y) cap = (cap = ReplyCap x y)"
|
||||
apply (rule iffI)
|
||||
apply (clarsimp simp: diminished'_def maskCapRights_def Let_def split del: if_split)
|
||||
apply (cases cap, simp_all add: isCap_simps)[1]
|
||||
apply (simp add: X64_H.maskCapRights_def isPageCap_def split: arch_capability.splits)
|
||||
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
lemma diminished_IRQControlCap' [simp]:
|
||||
"diminished' IRQControlCap cap = (cap = IRQControlCap)"
|
||||
apply (rule iffI)
|
||||
|
|
@ -749,6 +741,14 @@ lemma dec_dom_inv_wf[wp]:
|
|||
apply (simp add:numDomains_def maxDomain_def)
|
||||
done
|
||||
|
||||
lemma diminished_ReplyCap':
|
||||
"diminished' (capability.ReplyCap t False r) cap
|
||||
\<Longrightarrow> \<exists>gr. cap = capability.ReplyCap t False gr"
|
||||
apply (clarsimp simp: diminished'_def maskCapRights_def Let_def split del: if_split)
|
||||
apply (cases cap, simp_all add: isCap_simps)[1]
|
||||
apply (simp add: X64_H.maskCapRights_def isPageCap_def split: arch_capability.splits)
|
||||
done
|
||||
|
||||
lemma decode_inv_wf'[wp]:
|
||||
"\<lbrace>valid_cap' cap and invs' and sch_act_simple
|
||||
and cte_wp_at' (diminished' cap \<circ> cteCap) slot and real_cte_at' slot
|
||||
|
|
@ -766,10 +766,10 @@ lemma decode_inv_wf'[wp]:
|
|||
apply (case_tac cap, simp_all add: decodeInvocation_def Let_def isCap_defs uncurry_def split_def
|
||||
split del: if_split
|
||||
cong: if_cong)
|
||||
apply ((rule hoare_pre,
|
||||
((wp_trace decodeTCBInv_wf | simp add: o_def)+)[1],
|
||||
clarsimp simp: valid_cap'_def cte_wp_at_ctes_of
|
||||
| (rule exI, rule exI, erule (1) conjI))+)
|
||||
apply ((rule hoare_pre,
|
||||
((wp decodeTCBInv_wf | simp add: o_def)+)[1],
|
||||
clarsimp simp: valid_cap'_def cte_wp_at_ctes_of diminished_ReplyCap'
|
||||
| (rule exI, rule exI, erule (1) conjI))+)
|
||||
done
|
||||
|
||||
lemma ct_active_imp_simple'[elim!]:
|
||||
|
|
@ -892,9 +892,9 @@ lemma isReply_awaiting_reply':
|
|||
|
||||
lemma doReply_invs[wp]:
|
||||
"\<lbrace>tcb_at' t and tcb_at' t' and
|
||||
cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t False) slot and
|
||||
cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = ReplyCap t False grant) slot and
|
||||
invs' and sch_act_simple\<rbrace>
|
||||
doReplyTransfer t' t slot
|
||||
doReplyTransfer t' t slot grant
|
||||
\<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
apply (simp add: doReplyTransfer_def liftM_def)
|
||||
apply (rule hoare_seq_ext [OF _ gts_sp'])
|
||||
|
|
@ -926,10 +926,9 @@ lemma doReply_invs[wp]:
|
|||
apply (wp cteDeleteOne_reply_pred_tcb_at)+
|
||||
apply (clarsimp)
|
||||
apply (rule_tac Q="\<lambda>_. (\<lambda>s. t \<noteq> ksIdleThread s)
|
||||
and cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t False) slot"
|
||||
and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot"
|
||||
in hoare_strengthen_post [rotated])
|
||||
apply clarsimp
|
||||
apply (rule_tac x=t in exI, clarsimp)
|
||||
apply (fastforce simp: cte_wp_at'_def)
|
||||
apply (wp)
|
||||
apply (rule hoare_strengthen_post [OF doIPCTransfer_non_null_cte_wp_at'])
|
||||
apply (erule conjE)
|
||||
|
|
@ -985,7 +984,6 @@ lemma doReply_invs[wp]:
|
|||
apply (auto dest!: st_tcb_idle'[rotated] simp:isCap_simps)
|
||||
done
|
||||
|
||||
|
||||
lemma ct_active_runnable' [simp]:
|
||||
"ct_active' s \<Longrightarrow> ct_in_state' runnable' s"
|
||||
by (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
|
||||
|
|
@ -1914,7 +1912,7 @@ lemma hr_corres:
|
|||
intro!: corres_guard_imp [OF delete_caller_cap_corres]
|
||||
corres_guard_imp [OF do_reply_transfer_corres]
|
||||
corres_fail
|
||||
simp: valid_cap_def valid_cap'_def is_cap_simps assert_def)[1]
|
||||
simp: valid_cap_def valid_cap'_def is_cap_simps assert_def is_reply_cap_to_def)[1]
|
||||
apply (fastforce simp: invs_def valid_state_def
|
||||
cte_wp_at_caps_of_state st_tcb_def2
|
||||
dest: valid_reply_caps_of_stateD)
|
||||
|
|
@ -1971,8 +1969,8 @@ lemmas handleReply_ct_in_state_simple[wp] =
|
|||
(* FIXME: move *)
|
||||
lemma doReplyTransfer_st_tcb_at_active:
|
||||
"\<lbrace>st_tcb_at' active' t and tcb_at' t' and K (t \<noteq> t') and
|
||||
cte_wp_at' (\<lambda>cte. cteCap cte = (capability.ReplyCap t' False)) sl\<rbrace>
|
||||
doReplyTransfer t t' sl
|
||||
cte_wp_at' (\<lambda>cte. cteCap cte = (capability.ReplyCap t' False g)) sl\<rbrace>
|
||||
doReplyTransfer t t' sl g
|
||||
\<lbrace>\<lambda>rv. st_tcb_at' active' t\<rbrace>"
|
||||
apply (simp add: doReplyTransfer_def liftM_def)
|
||||
apply (wp setThreadState_st_tcb sts_pred_tcb_neq' cteDeleteOne_reply_pred_tcb_at
|
||||
|
|
@ -2055,7 +2053,7 @@ crunch sane [wp]: doIPCTransfer sch_act_sane
|
|||
|
||||
lemma doReplyTransfer_sane:
|
||||
"\<lbrace>\<lambda>s. sch_act_sane s \<and> t' \<noteq> ksCurThread s\<rbrace>
|
||||
doReplyTransfer t t' callerSlot \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>"
|
||||
doReplyTransfer t t' callerSlot g \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>"
|
||||
apply (simp add: doReplyTransfer_def liftM_def)
|
||||
apply (wp possibleSwitchTo_sane hoare_drop_imps hoare_vcg_all_lift|wpc)+
|
||||
apply simp
|
||||
|
|
@ -2087,7 +2085,7 @@ lemma doReplyTransfer_ct_not_ksQ:
|
|||
and ct_in_state' simple'
|
||||
and (\<lambda>s. ksCurThread s \<noteq> word)
|
||||
and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set(ksReadyQueues s p))\<rbrace>
|
||||
doReplyTransfer thread word callerSlot
|
||||
doReplyTransfer thread word callerSlot g
|
||||
\<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set(ksReadyQueues s p)\<rbrace>"
|
||||
proof -
|
||||
have astct: "\<And>t p.
|
||||
|
|
|
|||
|
|
@ -236,6 +236,7 @@ lemma restart_corres:
|
|||
apply (clarsimp simp add: invs'_def valid_state'_def sch_act_wf_weak)
|
||||
done
|
||||
|
||||
|
||||
lemma setupReplyMaster_sch_act_simple[wp]:
|
||||
"\<lbrace>sch_act_simple\<rbrace> setupReplyMaster thread \<lbrace>\<lambda>_. sch_act_simple\<rbrace>"
|
||||
apply (simp add: setupReplyMaster_def sch_act_simple_def)
|
||||
|
|
@ -1521,7 +1522,7 @@ proof -
|
|||
qed
|
||||
|
||||
lemma isReplyCapD:
|
||||
"isReplyCap cap \<Longrightarrow> \<exists>ptr master. cap = capability.ReplyCap ptr master"
|
||||
"isReplyCap cap \<Longrightarrow> \<exists>ptr master grant. cap = capability.ReplyCap ptr master grant"
|
||||
by (simp add: isCap_simps)
|
||||
|
||||
lemmas threadSet_ipcbuffer_trivial
|
||||
|
|
|
|||
Loading…
Reference in New Issue