theory ADT_C

lemma (in kernel_m)
  assumes valid: "valid_arch_state' astate"
  assumes rel: "carch_state_relation (ksArchState astate) cstate"
  shows casid_map_to_H_correct:
    "casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)) =
     armKSASIDMap (ksArchState astate)" apply (rule ext) using valid rel using [[hypsubst_thin]] apply (clarsimp simp: valid_arch_state'_def carch_state_relation_def
                        casid_map_to_H_def) apply (drule array_relation_map_conv2[OF _ eq_option_to_0_rev]) apply (fastforce simp: is_inv_def valid_asid_map'_def) apply clarsimp apply (cut_tac w=i in word_le_p2m1, simp add: minus_one_norm) apply clarsimp apply (case_tac "armKSASIDMap (ksArchState astate) x") apply (clarsimp simp: option_to_0_def split:option.splits) apply (fastforce simp: is_inv_def) apply clarsimp apply (rule conjI) apply (frule is_inv_inj) apply (clarsimp simp: the_inv_map_def is_inv_def dom_option_map
                   split: if_split) apply (intro conjI[rotated] impI domI, assumption) apply (rule the_equality) apply (clarsimp simp: ran_def dom_def Collect_eq) apply (drule_tac x=x in spec) apply (fastforce simp: inj_on_def) apply (fastforce simp: inj_on_def) apply (rule the_the_inv_mapI) apply (frule inj_hwasidsI) apply (simp add: valid_asid_map'_def) apply (frule is_inv_inj2, simp add: dom_option_map) apply simp apply (thin_tac "array_map_conv f n c = a" for f n c a) apply (clarsimp simp: asid_map_pd_to_hwasids_def ran_def) apply (subst (asm) fun_eq_iff) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)) = armKSASIDMap (ksArchState astate) proof (prove)
goal (1 subgoal):
 1. \<And>x. casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)) x = armKSASIDMap (ksArchState astate) x proof (prove)
using this:
valid_arch_state' astate
carch_state_relation (ksArchState astate) cstate

goal (1 subgoal):
 1. \<And>x. casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)) x = armKSASIDMap (ksArchState astate) x proof (prove)
using this:
valid_arch_state' astate
carch_state_relation (ksArchState astate) cstate

goal (1 subgoal):
 1. \<And>x. casid_map_to_H (armKSHWASIDTable_' cstate) (clift (t_hrs_' cstate)) x = armKSASIDMap (ksArchState astate) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState astate)) (armKSHWASIDTable_' cstate); is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate)\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range (armKSHWASIDTable (ksArchState astate))
 2. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate)\<rbrakk> \<Longrightarrow> \<forall>i>0xFF. armKSHWASIDTable (ksArchState astate) i = None
 3. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate)\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate)\<rbrakk> \<Longrightarrow> \<forall>i>0xFF. armKSHWASIDTable (ksArchState astate) i = None
 2. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate)\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); 0xFF < i\<rbrakk> \<Longrightarrow> armKSHWASIDTable (ksArchState astate) i = None
 2. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate)\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate)\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate)\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (armKSHWASIDTable (ksArchState astate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = None\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (armKSHWASIDTable (ksArchState astate)) x) = armKSASIDMap (ksArchState astate) x
 2. \<And>x a. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some a\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (armKSHWASIDTable (ksArchState astate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = None; x \<in> ran (armKSHWASIDTable (ksArchState astate))\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some a\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (armKSHWASIDTable (ksArchState astate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some a\<rbrakk> \<Longrightarrow> map_option (\<lambda>hw_asid. (hw_asid, the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) hw_asid))) (the_inv_map (armKSHWASIDTable (ksArchState astate)) x) = armKSASIDMap (ksArchState astate) x proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the_inv_map (armKSHWASIDTable (ksArchState astate)) x = Some a \<and> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the_inv_map (armKSHWASIDTable (ksArchState astate)) x = Some a
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate)))\<rbrakk> \<Longrightarrow> the_inv_map (armKSHWASIDTable (ksArchState astate)) x = Some a
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b))\<rbrakk> \<Longrightarrow> (x \<in> dom (armKSASIDMap (ksArchState astate)) \<longrightarrow> (THE xa. armKSHWASIDTable (ksArchState astate) xa = Some x) = a) \<and> x \<in> dom (armKSASIDMap (ksArchState astate))
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); x \<in> dom (armKSASIDMap (ksArchState astate))\<rbrakk> \<Longrightarrow> (THE xa. armKSHWASIDTable (ksArchState astate) xa = Some x) = a
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); x \<in> dom (armKSASIDMap (ksArchState astate))\<rbrakk> \<Longrightarrow> armKSHWASIDTable (ksArchState astate) a = Some x
 2. \<And>x a b xa. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); x \<in> dom (armKSASIDMap (ksArchState astate)); armKSHWASIDTable (ksArchState astate) xa = Some x\<rbrakk> \<Longrightarrow> xa = a
 3. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) {a. \<exists>y. armKSHWASIDTable (ksArchState astate) a = Some y}; \<forall>b. (\<exists>a. armKSHWASIDTable (ksArchState astate) a = Some b) = (\<exists>a ba. armKSASIDMap (ksArchState astate) b = Some (a, ba)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b))\<rbrakk> \<Longrightarrow> armKSHWASIDTable (ksArchState astate) a = Some x
 2. \<And>x a b xa. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); x \<in> dom (armKSASIDMap (ksArchState astate)); armKSHWASIDTable (ksArchState astate) xa = Some x\<rbrakk> \<Longrightarrow> xa = a
 3. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) {a. \<exists>y. armKSHWASIDTable (ksArchState astate) a = Some y}; \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); (\<exists>a. armKSHWASIDTable (ksArchState astate) a = Some x) = (\<exists>a b. armKSASIDMap (ksArchState astate) x = Some (a, b))\<rbrakk> \<Longrightarrow> armKSHWASIDTable (ksArchState astate) a = Some x
 2. \<And>x a b xa. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); x \<in> dom (armKSASIDMap (ksArchState astate)); armKSHWASIDTable (ksArchState astate) xa = Some x\<rbrakk> \<Longrightarrow> xa = a
 3. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b xa. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (armKSHWASIDTable (ksArchState astate)) (dom (armKSHWASIDTable (ksArchState astate))); ran (armKSHWASIDTable (ksArchState astate)) = dom (armKSASIDMap (ksArchState astate)); \<forall>x y. armKSHWASIDTable (ksArchState astate) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState astate) y = Some (x, b)); x \<in> dom (armKSASIDMap (ksArchState astate)); armKSHWASIDTable (ksArchState astate) xa = Some x\<rbrakk> \<Longrightarrow> xa = a
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> the (the_inv_map (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) a) = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (4 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState astate)) (dom (armKSASIDMap (ksArchState astate)))
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> inj_on (map_option fst \<circ> armKSASIDMap (ksArchState astate)) (dom (armKSASIDMap (ksArchState astate)))
 3. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))\<rbrakk> \<Longrightarrow> inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))
 4. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> inj_on (map_option fst \<circ> armKSASIDMap (ksArchState astate)) (dom (armKSASIDMap (ksArchState astate)))
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))\<rbrakk> \<Longrightarrow> inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))
 3. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b); inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))\<rbrakk> \<Longrightarrow> inj_on (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) (dom (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot))
 2. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = armKSHWASIDTable (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState astate)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); (\<lambda>pd. {hwasid. \<exists>a. armKSASIDMap (ksArchState astate) a = Some (hwasid, pd)}) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState astate)) astate; armKSNextASID_' cstate = armKSNextASID (ksArchState astate); page_directory_at' (armKSGlobalPD (ksArchState astate)) astate; valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate; is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)); valid_asid_map' (armKSASIDMap (ksArchState astate)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate); \<forall>x. {hwasid. \<exists>a. armKSASIDMap (ksArchState astate) a = Some (hwasid, x)} = (set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)) x; carch_globals (ksArchState astate); armKSASIDMap (ksArchState astate) x = Some (a, b)\<rbrakk> \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) b = Some a proof (prove)
goal:
No subgoals!