theory FinalCaps

lemma derive_cap_silc:
  "\<lbrace>\<lambda>s :: det_state. \<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s)\<rbrace>
   derive_cap slot cap
   \<lbrace>\<lambda>cap' s. \<not> cap_points_to_label aag cap' l \<longrightarrow> R (slots_holding_overlapping_caps cap' s)\<rbrace>,-" apply (simp add: derive_cap_def) apply (wp arch_derive_cap_silc | wpc | simp add: split_def)+ apply (auto simp: cap_points_to_label_def slots_holding_overlapping_caps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>cap' s. \<not> cap_points_to_label aag cap' l \<longrightarrow> R (slots_holding_overlapping_caps cap' s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s)\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>cap' s. \<not> cap_points_to_label aag cap' l \<longrightarrow> R (slots_holding_overlapping_caps cap' s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s) \<Longrightarrow> (cap = NullCap \<longrightarrow> \<not> cap_points_to_label aag NullCap l \<longrightarrow> R (slots_holding_overlapping_caps NullCap s)) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> \<not> cap_points_to_label aag (UntypedCap x xa xb xc) l \<longrightarrow> R (slots_holding_overlapping_caps (UntypedCap x xa xb xc) s)) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> \<not> cap_points_to_label aag (EndpointCap x xa xb) l \<longrightarrow> R (slots_holding_overlapping_caps (EndpointCap x xa xb) s)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> \<not> cap_points_to_label aag (NotificationCap x xa xb) l \<longrightarrow> R (slots_holding_overlapping_caps (NotificationCap x xa xb) s)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> \<not> cap_points_to_label aag NullCap l \<longrightarrow> R (slots_holding_overlapping_caps NullCap s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> \<not> cap_points_to_label aag (CNodeCap x xa xb) l \<longrightarrow> R (slots_holding_overlapping_caps (CNodeCap x xa xb) s)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> \<not> cap_points_to_label aag (ThreadCap x) l \<longrightarrow> R (slots_holding_overlapping_caps (ThreadCap x) s)) \<and> (cap = DomainCap \<longrightarrow> \<not> cap_points_to_label aag DomainCap l \<longrightarrow> R (slots_holding_overlapping_caps DomainCap s)) \<and> (cap = IRQControlCap \<longrightarrow> \<not> cap_points_to_label aag NullCap l \<longrightarrow> R (slots_holding_overlapping_caps NullCap s)) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> \<not> cap_points_to_label aag (IRQHandlerCap x) l \<longrightarrow> R (slots_holding_overlapping_caps (IRQHandlerCap x) s)) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> \<not> cap_points_to_label aag NullCap l \<longrightarrow> R (slots_holding_overlapping_caps NullCap s)) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?cap116 x = ArchObjectCap x \<and> (\<not> cap_points_to_label aag (?cap116 x) l \<longrightarrow> R (slots_holding_overlapping_caps (?cap116 x) s))) proof (prove)
goal:
No subgoals!