theory ArchVSpace_AI

lemma set_asid_pool_invs_map:
  "\<lbrace>invs and ko_at (ArchObj (ASIDPool pool)) ap
    and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap
                                  \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ((VSRef (ucast asid) (Some AASIDPool)) # rf))
                              \<and> (VSRef (ucast asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]))
    and page_directory_at pd
    and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)
    and K (pool asid = None)\<rbrace>
  set_asid_pool ap (pool(asid \<mapsto> pd))
  \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre, wp valid_irq_node_typ set_asid_pool_typ_at set_asid_pool_arch_objs_map valid_irq_handlers_lift
                            set_asid_pool_valid_arch_caps_map set_asid_pool_asid_map) apply clarsimp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and K (pool asid = None)\<rbrace> set_asid_pool ap (pool(asid \<mapsto> pd)) \<lbrace>\<lambda>rv. 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_arch_caps 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 ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None])) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and (\<lambda>y. pool asid = None)\<rbrace> set_asid_pool ap (pool(asid \<mapsto> pd)) \<lbrace>\<lambda>rv. 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_arch_caps 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 (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_arch_caps 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 ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None])) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and (\<lambda>y. pool asid = None)) s \<Longrightarrow> 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 valid_arch_state and valid_global_objs and valid_kernel_mappings and ako_at (ASIDPool pool) ap and K (pool asid = None) and (\<lambda>s. \<exists>ref. (ref \<rhd> ap) s) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)) s \<and> (valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs and valid_vspace_objs and ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and K (pool asid = None)) s \<and> (valid_global_objs and valid_arch_state) s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> (valid_asid_map and ako_at (ASIDPool pool) ap and K (pool asid = None)) s \<and> valid_global_vspace_mappings 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 (1 subgoal):
 1. \<And>s rf a b cap. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ako_at (ASIDPool pool) ap s; typ_at (AArch APageDirectory) pd s; (rf \<rhd> ap) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> ap) s proof (prove)
goal:
No subgoals!