theory ArchAcc_AI

lemma set_pd_invs_unmap:
  "\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and
    (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and
    obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and
    obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and
    obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd')
                       \<and> (\<forall>x \<in> kernel_mapping_slots. pd x = pd' x)) p and
    (\<lambda>s. p \<notin> global_refs s) and
    (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow>
     empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))))\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def) apply (rule hoare_pre) apply (wp set_pd_valid_objs set_pd_iflive set_pd_zombies
             set_pd_zombies_state_refs set_pd_valid_mdb
             set_pd_valid_idle set_pd_ifunsafe set_pd_reply_caps
             set_pd_valid_arch set_pd_valid_global set_pd_cur
             set_pd_reply_masters valid_irq_node_typ set_pd_zombies_state_hyp_refs
             set_pd_vspace_objs_unmap set_pd_vs_lookup_unmap
             valid_irq_handlers_lift
             set_pd_unmap_mappings set_pd_equal_kernel_mappings_triv) apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def
    del: disjCI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)))\<rbrace> set_pd p pd \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)))\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)))) s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)))) s \<Longrightarrow> ((\<lambda>s. \<forall>i. wellformed_pde (pd i)) and valid_objs) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> (valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p) s \<and> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p) s \<and> (valid_table_caps and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot cap. caps_of_state s slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<and> valid_caps (caps_of_state s) s \<and> unique_table_caps (caps_of_state s))) s \<and> (unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p \<in> obj_refs cap) slot s))) s \<and> (valid_kernel_mappings and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p) s \<and> (obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and equal_kernel_mappings) s \<and> valid_asid_map s \<and> (valid_global_vspace_mappings s \<and> valid_global_objs s \<and> p \<notin> global_refs s) \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s proof (prove)
goal:
No subgoals!