theory ADT_C

lemma (in kernel_m)  carch_state_to_H_correct:
  assumes valid:  "valid_arch_state' astate"
  assumes rel:    "carch_state_relation (ksArchState astate) (cstate)"
  assumes gpts:   "armKSGlobalPTs (ksArchState astate) =
                   [symbol_table ''armKSGlobalPT'']"
  shows           "carch_state_to_H cstate = ksArchState astate" apply (case_tac "ksArchState astate", simp) apply (rename_tac v1 v2 v3 v4 v5 v6 v7) using gpts rel[simplified carch_state_relation_def carch_globals_def] apply (clarsimp simp: carch_state_to_H_def
                        casid_map_to_H_correct[OF valid rel]) apply (rule conjI[rotated]) apply (rule array_relation_map_conv2[OF _ eq_option_to_0_rev]) apply assumption using valid[simplified valid_arch_state'_def] 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 (rule array_relation_map_conv2[OF _ eq_option_to_ptr_rev]) apply assumption using valid[simplified valid_arch_state'_def] apply (fastforce simp: valid_asid_table'_def) using valid[simplified valid_arch_state'_def] apply (fastforce simp: valid_asid_table'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. carch_state_to_H cstate = ksArchState astate proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7. ksArchState astate = ARMKernelState x1 x2 x3 x4 x5 x6 x7 \<Longrightarrow> carch_state_to_H cstate = ARMKernelState x1 x2 x3 x4 x5 x6 x7 proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2 v3 v4 v5 v6 v7. ksArchState astate = ARMKernelState v1 v2 v3 v4 v5 v6 v7 \<Longrightarrow> carch_state_to_H cstate = ARMKernelState v1 v2 v3 v4 v5 v6 v7 proof (prove)
using this:
armKSGlobalPTs (ksArchState astate) = [symbol_table ''armKSGlobalPT'']
armKSNextASID_' cstate = armKSNextASID (ksArchState astate) \<and> armKSKernelVSpace (ksArchState astate) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState astate)) (armKSHWASIDTable_' cstate) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState astate)) (armKSASIDTable_' cstate) \<and> 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) \<and> armKSGlobalPD (ksArchState astate) = ptr_val armKSGlobalPD_Ptr \<and> armKSGlobalPTs (ksArchState astate) = [ptr_val armKSGlobalPT_Ptr]

goal (1 subgoal):
 1. \<And>v1 v2 v3 v4 v5 v6 v7. ksArchState astate = ARMKernelState v1 v2 v3 v4 v5 v6 v7 \<Longrightarrow> carch_state_to_H cstate = ARMKernelState v1 v2 v3 v4 v5 v6 v7 proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 \<and> array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = v2 proof (prove)
goal (2 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = 0 then None else Some x) 0xFF (armKSHWASIDTable_' cstate) = v2
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
goal (4 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate)
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range v2
 3. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>0xFF. v2 i = None
 4. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
goal (3 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range v2
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>0xFF. v2 i = None
 3. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
using this:
valid_asid_table' (armKSASIDTable (ksArchState astate)) astate \<and> page_directory_at' (armKSGlobalPD (ksArchState astate)) astate \<and> valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate \<and> is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)) \<and> valid_asid_map' (armKSASIDMap (ksArchState astate))

goal (3 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range v2
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>0xFF. v2 i = None
 3. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
goal (2 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>0xFF. v2 i = None
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
goal (2 subgoals):
 1. \<And>v1 v2 v4 i. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot); 0xFF < i\<rbrakk> \<Longrightarrow> v2 i = None
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_map_conv (\<lambda>x. if x = NULL then None else Some (ptr_val x)) (2 ^ local.asid_high_bits - 1) (armKSASIDTable_' cstate) = v1 proof (prove)
goal (3 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate)
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range v1
 3. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>2 ^ local.asid_high_bits - 1. v1 i = None proof (prove)
goal (2 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range v1
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>2 ^ local.asid_high_bits - 1. v1 i = None proof (prove)
using this:
valid_asid_table' (armKSASIDTable (ksArchState astate)) astate \<and> page_directory_at' (armKSGlobalPD (ksArchState astate)) astate \<and> valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate \<and> is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)) \<and> valid_asid_map' (armKSASIDMap (ksArchState astate))

goal (2 subgoals):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> Some 0 \<notin> range v1
 2. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>2 ^ local.asid_high_bits - 1. v1 i = None proof (prove)
goal (1 subgoal):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>2 ^ local.asid_high_bits - 1. v1 i = None proof (prove)
using this:
valid_asid_table' (armKSASIDTable (ksArchState astate)) astate \<and> page_directory_at' (armKSGlobalPD (ksArchState astate)) astate \<and> valid_global_pts' (armKSGlobalPTs (ksArchState astate)) astate \<and> is_inv (armKSHWASIDTable (ksArchState astate)) (map_option fst \<circ> armKSASIDMap (ksArchState astate)) \<and> valid_asid_map' (armKSASIDMap (ksArchState astate))

goal (1 subgoal):
 1. \<And>v1 v2 v4. \<lbrakk>ksArchState astate = ARMKernelState v1 v2 (armKSNextASID_' cstate) v4 (symbol_table ''armKSGlobalPD'') [symbol_table ''armKSGlobalPT''] armKSKernelVSpace_C; array_relation ((=) \<circ> option_to_0) 0xFF v2 (armKSHWASIDTable_' cstate); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) v1 (armKSASIDTable_' cstate); asid_map_pd_to_hwasids v4 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)\<rbrakk> \<Longrightarrow> \<forall>i>2 ^ local.asid_high_bits - 1. v1 i = None proof (prove)
goal:
No subgoals!