theory ArchFinalise_AI

lemma invs_arm_asid_table_unmap:
  "invs s \<and> is_aligned base asid_low_bits \<and> base \<le> mask asid_bits
       \<and> (\<forall>x\<in>set [0.e.2 ^ asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None)
       \<and> tab = arm_asid_table (arch_state s)
     \<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)" apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def) apply (strengthen valid_asid_map_unmap valid_vspace_objs_unmap_strg
                    valid_vs_lookup_unmap_strg valid_arch_state_unmap_strg) apply (simp add: valid_irq_node_def valid_kernel_mappings_def
                   valid_global_objs_arch_update) apply (simp add: valid_table_caps_def valid_machine_state_def second_level_tables_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<and> is_aligned base local.asid_low_bits \<and> base \<le> mask local.asid_bits \<and> (\<forall>x\<in>set [0 .e. 2 ^ local.asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) \<and> tab = asid_table s \<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace 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_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state 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; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; tab = asid_table s\<rbrakk> \<Longrightarrow> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace 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_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state 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; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; tab = asid_table s\<rbrakk> \<Longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) \<and> valid_asid_map s \<and> is_aligned base local.asid_low_bits \<and> base \<le> mask local.asid_bits \<and> (\<forall>x\<in>set [0 .e. 2 ^ local.asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace 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; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; 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; is_aligned base local.asid_low_bits; base \<le> mask local.asid_bits; \<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None; tab = asid_table s\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!