theory ArchFinalCaps

lemma arch_derive_cap_silc[FinalCaps_assms]:
  "\<lbrace>\<lambda>s. cap = ArchObjectCap acap \<and>
        (\<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s))\<rbrace>
   arch_derive_cap acap
   \<lbrace>\<lambda>cap' s. \<not> cap_points_to_label aag cap' l \<longrightarrow> R (slots_holding_overlapping_caps cap' s)\<rbrace>, -" apply (simp add: arch_derive_cap_def) apply wpsimp 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. cap = ArchObjectCap acap \<and> (\<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s))\<rbrace> arch_derive_cap acap \<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. cap = ArchObjectCap acap \<and> (\<not> cap_points_to_label aag cap l \<longrightarrow> R (slots_holding_overlapping_caps cap s))\<rbrace> case acap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | _ \<Rightarrow> returnOk (ArchObjectCap acap) \<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. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap acap) l \<longrightarrow> R (slots_holding_overlapping_caps (ArchObjectCap acap) s); cap = ArchObjectCap acap\<rbrakk> \<Longrightarrow> (\<forall>x xa. acap = ASIDPoolCap x xa \<longrightarrow> \<not> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) l \<longrightarrow> R (slots_holding_overlapping_caps (ArchObjectCap (ASIDPoolCap x xa)) s)) \<and> (acap = ASIDControlCap \<longrightarrow> \<not> cap_points_to_label aag (ArchObjectCap ASIDControlCap) l \<longrightarrow> R (slots_holding_overlapping_caps (ArchObjectCap ASIDControlCap) s)) \<and> (\<forall>x xa xb xc. (\<exists>xd. acap = PageCap x xa xb xc xd) \<longrightarrow> \<not> cap_points_to_label aag (ArchObjectCap (PageCap x xa xb xc None)) l \<longrightarrow> R (slots_holding_overlapping_caps (ArchObjectCap (PageCap x xa xb xc None)) s)) \<and> (\<forall>x xa. acap = PageTableCap x xa \<longrightarrow> (\<forall>a b. xa = Some (a, b) \<longrightarrow> \<not> cap_points_to_label aag (ArchObjectCap (PageTableCap x (Some (a, b)))) l \<longrightarrow> R (slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x (Some (a, b)))) s))) \<and> (\<forall>x xa. acap = PageDirectoryCap x xa \<longrightarrow> (\<forall>xb. xa = Some xb \<longrightarrow> \<not> cap_points_to_label aag (ArchObjectCap (PageDirectoryCap x (Some xb))) l \<longrightarrow> R (slots_holding_overlapping_caps (ArchObjectCap (PageDirectoryCap x (Some xb))) s))) proof (prove)
goal:
No subgoals!