theory ArchFinalCaps

lemma perform_page_table_invocation_silc_inv_get_cap_helper:
   "\<lbrace>silc_inv aag st and cte_wp_at (is_pt_cap or is_pg_cap) xa\<rbrace>
    get_cap xa
    \<lbrace>(\<lambda>capa s. (\<not> cap_points_to_label aag (ArchObjectCap $ update_map_data capa None)
                                           (pasObjectAbs aag (fst xa))
                \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps
                                       (ArchObjectCap $ update_map_data capa None) s \<and>
                             pasObjectAbs aag (fst lslot) = SilcLabel))) \<circ> the_arch_cap\<rbrace>" apply (wp get_cap_wp) apply clarsimp apply (drule cte_wp_at_norm) apply (clarify) apply (drule (1) cte_wp_at_eqD2) apply (case_tac cap, simp_all add: is_pg_cap_def is_pt_cap_def) apply (clarsimp simp: cap_points_to_label_def update_map_data_def split: arch_cap.splits) apply (drule silc_invD) apply assumption apply (fastforce simp: intra_label_cap_def cap_points_to_label_def) apply (fastforce simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (drule silc_invD) apply assumption apply (fastforce simp: intra_label_cap_def cap_points_to_label_def) apply (fastforce simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and cte_wp_at (is_pt_cap or is_pg_cap) xa\<rbrace> get_cap xa \<lbrace>(\<lambda>capa s. \<not> cap_points_to_label aag (ArchObjectCap $ update_map_data capa None) (pasObjectAbs aag (fst xa)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap $ update_map_data capa None) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) \<circ> the_arch_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and cte_wp_at (is_pt_cap or is_pg_cap) xa) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) xa s \<longrightarrow> ((\<lambda>capa s. \<not> cap_points_to_label aag (ArchObjectCap $ update_map_data capa None) (pasObjectAbs aag (fst xa)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap $ update_map_data capa None) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) \<circ> the_arch_cap) cap s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>silc_inv aag st s; cte_wp_at (is_pt_cap or is_pg_cap) xa s; cte_wp_at ((=) cap) xa s; \<not> cap_points_to_label aag (ArchObjectCap (update_map_data (the_arch_cap cap) None)) (pasObjectAbs aag (fst xa))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (update_map_data (the_arch_cap cap) None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) xa s; \<not> cap_points_to_label aag (ArchObjectCap (update_map_data (the_arch_cap cap) None)) (pasObjectAbs aag (fst xa)); \<exists>c. cte_wp_at ((=) c) xa s \<and> (is_pt_cap or is_pg_cap) c\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (update_map_data (the_arch_cap cap) None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s cap c. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) xa s; \<not> cap_points_to_label aag (ArchObjectCap (update_map_data (the_arch_cap cap) None)) (pasObjectAbs aag (fst xa)); cte_wp_at ((=) c) xa s; (is_pt_cap or is_pg_cap) c\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (update_map_data (the_arch_cap cap) None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s cap c. \<lbrakk>silc_inv aag st s; \<not> cap_points_to_label aag (ArchObjectCap (update_map_data (the_arch_cap cap) None)) (pasObjectAbs aag (fst xa)); cte_wp_at ((=) c) xa s; (is_pt_cap or is_pg_cap) c; c = cap\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (update_map_data (the_arch_cap cap) None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s cap c x12. \<lbrakk>silc_inv aag st s; \<not> cap_points_to_label aag (ArchObjectCap (update_map_data x12 None)) (pasObjectAbs aag (fst xa)); cte_wp_at ((=) (ArchObjectCap x12)) xa s; (\<exists>p asid. x12 = PageTableCap p asid) \<or> (\<exists>dev p R sz m. x12 = PageCap dev p R sz m); c = ArchObjectCap x12; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (update_map_data x12 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; silc_inv aag st s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageCap x31 x32 x33 x34 None)) s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; silc_inv aag st s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (4 subgoals):
 1. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap62 s x31 x32 x33 x34 x35)) (?slot62 s x31 x32 x33 x34 x35) s
 2. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot62 s x31 x32 x33 x34 x35) s
 3. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap62 s x31 x32 x33 x34 x35) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageCap x31 x32 x33 x34 None)) s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; silc_inv aag st s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag xa s
 2. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageCap x31 x32 x33 x34 None)) s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; silc_inv aag st s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s x31 x32 x33 x34 x35. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) xa s; pasObjectAbs aag x32 \<noteq> pasObjectAbs aag (fst xa); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageCap x31 x32 x33 x34 None)) s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; silc_inv aag st s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; silc_inv aag st s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap76 s x41 x42)) (?slot76 s x41 x42) s
 2. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot76 s x41 x42) s
 3. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap76 s x41 x42) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag xa s
 2. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 x42)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s x41 x42. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) xa s; pasObjectAbs aag x41 \<noteq> pasObjectAbs aag (fst xa); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 x42)) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ArchObjectCap (PageTableCap x41 None)) s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal:
No subgoals!