theory VSpace_C

lemma invalidateASID_ccorres:
  "ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits))
                   (UNIV \<inter> {s. asid_' s = asid}) []
     (invalidateASID asid) (Call invalidateASID_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: asid_') apply (rule ccorres_Guard_Seq)+ apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_findPDForASIDAssert]) apply (rename_tac pd) apply (rule_tac P="\<lambda>s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s
                               \<and> pd \<notin> ran (option_map snd o armKSASIDMap (ksArchState s)
                                                     |` (- {asid}))
                               \<and> option_map snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}"
                   in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: Collect_const_mem word_sle_def word_sless_def
                           asidLowBits_handy_convs simpler_gets_def
                           simpler_modify_def bind_def) apply (frule(2) pd_at_asid_cross_over) apply (clarsimp simp: typ_heap_simps) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                           cpspace_relation_def
                           ptr_add_assertion_positive
                           array_assertion_shrink_right) apply (clarsimp simp: typ_heap_simps cmachine_state_relation_def
                           carch_state_relation_def pd_at_asid'_def carch_globals_def
                           fun_upd_def[symmetric] order_le_less_trans[OF word_and_le1]
                           arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) apply (intro conjI) apply (erule iffD1 [OF cmap_relation_cong, rotated -1], simp_all)[1] apply (simp split: if_split_asm) apply (clarsimp simp: cpde_relation_def Let_def
                            pde_lift_pde_invalid
                      cong: ARM_H.pde.case_cong) apply (subst asid_map_pd_to_hwasids_clear, assumption) subgoal by clarsimp apply (rule ext, simp add: pd_pointer_to_asid_slot_def map_comp_def split: if_split) subgoal by (clarsimp simp: pde_stored_asid_def) apply wp[1] apply (wp findPDForASIDAssert_pd_at_wp2) apply (clarsimp simp: asidLowBits_handy_convs word_sle_def word_sless_def
                        asid_shiftr_low_bits_less) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (invalidateASID asid) (Call invalidateASID_'proc) proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> ccorres dc xfdc valid_pde_mappings' (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (invalidateASID asid) (Call invalidateASID_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q552 asida) (?Q'552 asida) [SKIP] (do y <- findPDForASIDAssert asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od) (Guard ArrayBounds \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>asidPool :== \<acute>armKSASIDTable.[unat (asida >> unat Kernel_C.asidLowBits)])));;
(Guard ArrayBounds \<lbrace>asida && 2 ^ unat Kernel_C.asidLowBits - 1 < 0x400\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c asidPool_' s} (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>pd :== h_val (hrs_mem \<acute>t_hrs) (PTR(pde_C ptr[1024]) &(\<acute>asidPool\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]))));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) false);;
Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd_' s +\<^sub>p 4080)} (Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>pd +\<^sub>p 4080) \<acute>ret__struct_pde_C))))))))
 2. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> ?Q'552 asida proof (prove)
goal (2 subgoals):
 1. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q552 asida) (?C'562 asida) [SKIP] (do y <- findPDForASIDAssert asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od) (\<acute>asidPool :== \<acute>armKSASIDTable.[unat (asida >> unat Kernel_C.asidLowBits)];;
(Guard ArrayBounds \<lbrace>asida && 2 ^ unat Kernel_C.asidLowBits - 1 < 0x400\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c asidPool_' s} (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>pd :== h_val (hrs_mem \<acute>t_hrs) (PTR(pde_C ptr[1024]) &(\<acute>asidPool\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]))));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) false);;
Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd_' s +\<^sub>p 4080)} (Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>pd +\<^sub>p 4080) \<acute>ret__struct_pde_C))))))))
 2. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> ?C'562 asida \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>asida y. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q564 asida y) (?Q'564 asida y) [SKIP] (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od) (\<acute>asidPool :== \<acute>armKSASIDTable.[unat (asida >> unat Kernel_C.asidLowBits)];;
(Guard ArrayBounds \<lbrace>asida && 2 ^ unat Kernel_C.asidLowBits - 1 < 0x400\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c asidPool_' s} (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>pd :== h_val (hrs_mem \<acute>t_hrs) (PTR(pde_C ptr[1024]) &(\<acute>asidPool\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]))));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) false);;
Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd_' s +\<^sub>p 4080)} (Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>pd +\<^sub>p 4080) \<acute>ret__struct_pde_C))))))))
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>?Q564 asida\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q564 asida rv s \<longrightarrow> s' \<in> ?Q'564 asida rv} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>asida pd. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q564 asida pd) (?Q'564 asida pd) [SKIP] (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od) (\<acute>asidPool :== \<acute>armKSASIDTable.[unat (asida >> unat Kernel_C.asidLowBits)];;
(Guard ArrayBounds \<lbrace>asida && 2 ^ unat Kernel_C.asidLowBits - 1 < 0x400\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c asidPool_' s} (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>pd :== h_val (hrs_mem \<acute>t_hrs) (PTR(pde_C ptr[1024]) &(\<acute>asidPool\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]))));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) false);;
Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd_' s +\<^sub>p 4080)} (Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>pd +\<^sub>p 4080) \<acute>ret__struct_pde_C))))))))
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>?Q564 asida\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q564 asida rv s \<longrightarrow> s' \<in> ?Q'564 asida rv} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>asida pd. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (pd_at_asid' pd asid \<sigma> \<and> valid_pde_mappings' \<sigma> \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState \<sigma>) asid) \<in> {None, Some pd}) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>asidPool :== \<acute>armKSASIDTable.[unat (asida >> unat Kernel_C.asidLowBits)];;
(Guard ArrayBounds \<lbrace>asida && 2 ^ unat Kernel_C.asidLowBits - 1 < 0x400\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c asidPool_' s} (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>pd :== h_val (hrs_mem \<acute>t_hrs) (PTR(pde_C ptr[1024]) &(\<acute>asidPool\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]))));;
(\<acute>ret__struct_pde_C :== CALL pde_pde_invalid_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) false);;
Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd_' s +\<^sub>p 4080)} (Guard MemorySafety \<lbrace>ptr_add_assertion \<acute>pd 4080 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>pd +\<^sub>p 4080) \<acute>ret__struct_pde_C))))))) {s. \<exists>(rv, \<sigma>')\<in>fst ((do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>asida pd \<sigma>. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> {s. (pd_at_asid' pd asid \<sigma> \<and> valid_pde_mappings' \<sigma> \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState \<sigma>) asid) \<in> {None, Some pd}) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. asida && 2 ^ unat Kernel_C.asidLowBits - 1 < 0x400 \<and> s \<Turnstile>\<^sub>c armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)] \<and> 0 \<le>s Kernel_C.asidLowBits \<and> Kernel_C.asidLowBits <s 0x20 \<and> (\<forall>t. pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 8, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> ptr_add_assertion (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]) 4080 False (hrs_htd (t_hrs_' (globals s))) \<and> s \<Turnstile>\<^sub>c (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)] +\<^sub>p 4080) \<and> ptr_add_assertion (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)]) 4080 True (hrs_htd (t_hrs_' (globals s))) \<and> (\<exists>(rv, \<sigma>')\<in>fst ((do asidMap <- gets (\<lambda>x. armKSASIDMap (ksArchState x));
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)] +\<^sub>p 4080) (ret__struct_pde_C_' t)))) (s\<lparr>asidPool_' := armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)], pd_' := h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)], ret__struct_pde_C_' := ret__struct_pde_C_' t\<rparr>)) \<in> rf_sr \<and> dc rv (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)] +\<^sub>p 4080) (ret__struct_pde_C_' t)))) (s\<lparr>asidPool_' := armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)], pd_' := h_val (hrs_mem (t_hrs_' (globals s))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals s).[unat (asida >> unat Kernel_C.asidLowBits)]\<rightarrow>[''array_C''])).[unat (asida && 2 ^ unat Kernel_C.asidLowBits - 1)], ret__struct_pde_C_' := ret__struct_pde_C_' t\<rparr>)))))}
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x. \<lbrakk>asid \<le> mask local.asid_bits; pd_at_asid' pd asid \<sigma>; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> asid && 2 ^ local.asid_low_bits - 1 < 0x400 \<and> x \<Turnstile>\<^sub>c armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] \<and> (\<forall>t. pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> ptr_add_assertion (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)]) 4080 False (hrs_htd (t_hrs_' (globals x))) \<and> x \<Turnstile>\<^sub>c (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)] +\<^sub>p 4080) \<and> ptr_add_assertion (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)]) 4080 True (hrs_htd (t_hrs_' (globals x))) \<and> (\<sigma>\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState \<sigma>))(asid := None)) (ksArchState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)] +\<^sub>p 4080) (ret__struct_pde_C_' t)))) (x\<lparr>asidPool_' := armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)], pd_' := h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)], ret__struct_pde_C_' := ret__struct_pde_C_' t\<rparr>)) \<in> rf_sr)
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x. \<lbrakk>asid \<le> mask local.asid_bits; pd_at_asid' pd asid \<sigma>; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); (\<sigma>, x) \<in> rf_sr; \<exists>apptr ap pde. armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap) \<and> ap.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))) \<and> (valid_pde_mappings' \<sigma> \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)\<rbrakk> \<Longrightarrow> asid && 2 ^ local.asid_low_bits - 1 < 0x400 \<and> x \<Turnstile>\<^sub>c armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] \<and> (\<forall>t. pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> ptr_add_assertion (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)]) 4080 False (hrs_htd (t_hrs_' (globals x))) \<and> x \<Turnstile>\<^sub>c (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)] +\<^sub>p 4080) \<and> ptr_add_assertion (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)]) 4080 True (hrs_htd (t_hrs_' (globals x))) \<and> (\<sigma>\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState \<sigma>))(asid := None)) (ksArchState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)] +\<^sub>p 4080) (ret__struct_pde_C_' t)))) (x\<lparr>asidPool_' := armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)], pd_' := h_val (hrs_mem (t_hrs_' (globals x))) (PTR(pde_C ptr[1024]) &(armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rightarrow>[''array_C''])).[unat (asid && 2 ^ local.asid_low_bits - 1)], ret__struct_pde_C_' := ret__struct_pde_C_' t\<rparr>)) \<in> rf_sr)
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde. \<lbrakk>asid \<le> mask local.asid_bits; pd_at_asid' pd asid \<sigma>; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); (\<sigma>, x) \<in> rf_sr; armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> asid && 2 ^ local.asid_low_bits - 1 < 0x400 \<and> (\<forall>t. pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> ptr_add_assertion (pde_Ptr pd) 4080 False (hrs_htd (t_hrs_' (globals x))) \<and> ptr_add_assertion (pde_Ptr pd) 4080 True (hrs_htd (t_hrs_' (globals x))) \<and> (\<sigma>\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState \<sigma>))(asid := None)) (ksArchState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)))) (x\<lparr>asidPool_' := ap_Ptr apptr, pd_' := pde_Ptr pd, ret__struct_pde_C_' := ret__struct_pde_C_' t\<rparr>)) \<in> rf_sr)
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde. \<lbrakk>asid \<le> mask local.asid_bits; pd_at_asid' pd asid \<sigma>; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid && 2 ^ local.asid_low_bits - 1 < 0x400 \<and> (\<forall>t. pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> cmap_relation (ctes_of \<sigma>) (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace \<sigma>) (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t)) (t_hrs_' (globals x))) \<and> carch_state_relation (armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState \<sigma>))(asid := None)) (ksArchState \<sigma>)) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr (pd + 0x3FC0)) (ret__struct_pde_C_' t))) (globals x)))
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) ((cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t)) pde_Ptr cpde_relation \<and> asid_map_pd_to_hwasids ((armKSASIDMap (ksArchState \<sigma>))(asid := None)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) ((cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t)) pde_Ptr cpde_relation
 2. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> asid_map_pd_to_hwasids ((armKSASIDMap (ksArchState \<sigma>))(asid := None)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 3. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool p a a' b b'. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; a' = a; map_to_pdes (ksPSpace \<sigma>) p = Some a; cslift x (pde_Ptr p) = Some b; (if p = pd + 0x3FC0 then Some (ret__struct_pde_C_' t) else cslift x (pde_Ptr p)) = Some b'\<rbrakk> \<Longrightarrow> cpde_relation a b = cpde_relation a b'
 2. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> asid_map_pd_to_hwasids ((armKSASIDMap (ksArchState \<sigma>))(asid := None)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 3. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool p a a' b b'. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some b; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag b = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift b' = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag b' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; a' = a; map_to_pdes (ksPSpace \<sigma>) (pd + 0x3FC0) = Some a; pde = b; p = pd + 0x3FC0; ret__struct_pde_C_' t = b'\<rbrakk> \<Longrightarrow> cpde_relation a b = cpde_relation a b'
 2. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> asid_map_pd_to_hwasids ((armKSASIDMap (ksArchState \<sigma>))(asid := None)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 3. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> asid_map_pd_to_hwasids ((armKSASIDMap (ksArchState \<sigma>))(asid := None)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<forall>hw_asid pd'. armKSASIDMap (ksArchState \<sigma>) asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd
 2. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> (asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)))(pd := {}) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 3. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>_; pd_ \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>_)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>_) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>_) asid = Some (a, pd_)); armKSASIDTable_' (globals x_).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr_; cslift x_ (ap_Ptr apptr_) = Some (asid_pool_C.asid_pool_C ap_); ap_.[unat (asid && 0x3FF)] = pde_Ptr pd_; cslift x_ (pde_Ptr (pd_ + 0x3FC0)) = Some pde_; is_aligned pd_ pdBits; array_assertion (pde_Ptr pd_) 4096 (hrs_htd (t_hrs_' (globals x_))); pde_get_tag pde_ = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>_) (cslift x_) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>_)) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>_)) (cslift x_) ntfn_Ptr (cnotification_relation (cslift x_)); cmap_relation (map_to_pdes (ksPSpace \<sigma>_)) (cslift x_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>_)) (cslift x_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>_)) (cslift x_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>_)) (c_h_t_valid x_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>_)) (c_h_t_valid x_) pt_Ptr; cready_queues_relation (cslift x_) (ksReadyQueues_' (globals x_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals x_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals x_)); cte_array_relation \<sigma>_ (globals x_); tcb_cte_array_relation \<sigma>_ (globals x_); apsnd fst (ghost'state_' (globals x_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals x_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals x_) = ksWorkUnitsCompleted \<sigma>_; x_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals x_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals x_) = ksDomainTime \<sigma>_; armKSNextASID_' (globals x_) = armKSNextASID (ksArchState \<sigma>_); irq_masks (ksMachineState \<sigma>_) = irq_masks (phantom_machine_state_' (globals x_)); armKSASIDTable (ksArchState \<sigma>_) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa_; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>_); irq_state (ksMachineState \<sigma>_) = irq_state (phantom_machine_state_' (globals x_)); ko_at' (asidpool.ASIDPool pool_) apa_ \<sigma>_; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>_)) (armKSHWASIDTable_' (globals x_)); device_state (ksMachineState \<sigma>_) = device_state (phantom_machine_state_' (globals x_)); pool_ (asid && mask local.asid_low_bits) = Some pd_; page_directory_at' pd_ \<sigma>_; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>_)) (armKSASIDTable_' (globals x_)); exclusive_state (ksMachineState \<sigma>_) = exclusive_state (phantom_machine_state_' (globals x_)); machine_state_rest (ksMachineState \<sigma>_) = machine_state_rest (phantom_machine_state_' (globals x_)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>_)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x_ \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>_) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>_) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t_) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t_) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<forall>hw_asid pd'. armKSASIDMap (ksArchState \<sigma>_) asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd_ proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> (asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)))(pd := {}) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m (cslift x)(pde_Ptr (pd + 0x3FC0) \<mapsto> ret__struct_pde_C_' t) \<circ>\<^sub>m pd_pointer_to_asid_slot)
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd \<sigma> x apptr ap pde apa t pool xa. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>) asid = Some (a, pd)); armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr; cslift x (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap); ap.[unat (asid && 0x3FF)] = pde_Ptr pd; cslift x (pde_Ptr (pd + 0x3FC0)) = Some pde; is_aligned pd pdBits; array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals x))); pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x) pde_Ptr cpde_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x) pte_Ptr cpte_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cte_array_relation \<sigma> (globals x); cvariable_array_map_relation (\<lambda>k. case ksPSpace \<sigma> k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); ko_at' (asidpool.ASIDPool pool) apa \<sigma>; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd \<sigma>; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (\<lambda>k. case if is_aligned k pdBits then Some (pde_Ptr (k + 0x3FC0)) else None of None \<Rightarrow> None | Some v \<Rightarrow> case cslift x v of None \<Rightarrow> None | Some x \<Rightarrow> pde_stored_asid x); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> xa = pd \<longrightarrow> {} = set_option (pde_stored_asid (ret__struct_pde_C_' t))
 2. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid \<le> mask local.asid_bits; valid_pde_mappings' \<sigma>_; pd_ \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState \<sigma>_)|\<^bsub>(- {asid})\<^esub>); armKSASIDMap (ksArchState \<sigma>_) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState \<sigma>_) asid = Some (a, pd_)); armKSASIDTable_' (globals x_).[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr_; cslift x_ (ap_Ptr apptr_) = Some (asid_pool_C.asid_pool_C ap_); ap_.[unat (asid && 0x3FF)] = pde_Ptr pd_; cslift x_ (pde_Ptr (pd_ + 0x3FC0)) = Some pde_; is_aligned pd_ pdBits; array_assertion (pde_Ptr pd_) 4096 (hrs_htd (t_hrs_' (globals x_))); pde_get_tag pde_ = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; cmap_relation (ctes_of \<sigma>_) (cslift x_) cte_Ptr ccte_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); cmap_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x_) ntfn_Ptr (cnotification_relation (cslift x_)); cmap_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x_) pde_Ptr cpde_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x_) pte_Ptr cpte_relation; cmap_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (cslift x_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (c_h_t_valid x_) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (c_h_t_valid x_) pt_Ptr; cready_queues_relation (cslift x_) (ksReadyQueues_' (globals x_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals x_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals x_)); cte_array_relation \<sigma>_ (globals x_); cvariable_array_map_relation (\<lambda>k. case ksPSpace \<sigma>_ k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x_))); apsnd fst (ghost'state_' (globals x_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals x_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals x_) = ksWorkUnitsCompleted \<sigma>_; x_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals x_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals x_) = ksDomainTime \<sigma>_; armKSNextASID_' (globals x_) = armKSNextASID (ksArchState \<sigma>_); irq_masks (ksMachineState \<sigma>_) = irq_masks (phantom_machine_state_' (globals x_)); armKSASIDTable (ksArchState \<sigma>_) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some apa_; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>_); irq_state (ksMachineState \<sigma>_) = irq_state (phantom_machine_state_' (globals x_)); ko_at' (asidpool.ASIDPool pool_) apa_ \<sigma>_; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>_)) (armKSHWASIDTable_' (globals x_)); device_state (ksMachineState \<sigma>_) = device_state (phantom_machine_state_' (globals x_)); pool_ (asid && mask local.asid_low_bits) = Some pd_; page_directory_at' pd_ \<sigma>_; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>_)) (armKSASIDTable_' (globals x_)); exclusive_state (ksMachineState \<sigma>_) = exclusive_state (phantom_machine_state_' (globals x_)); machine_state_rest (ksMachineState \<sigma>_) = machine_state_rest (phantom_machine_state_' (globals x_)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>_)) = set_option \<circ> (\<lambda>k. case if is_aligned k pdBits then Some (pde_Ptr (k + 0x3FC0)) else None of None \<Rightarrow> None | Some v \<Rightarrow> case cslift x_ v of None \<Rightarrow> None | Some x \<Rightarrow> pde_stored_asid x); armKSGlobalPD (ksArchState \<sigma>_) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>_) = [symbol_table ''armKSGlobalPT'']; pde_pde_invalid_lift (ret__struct_pde_C_' t_) = \<lparr>stored_hw_asid_CL = 0, stored_asid_valid_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; pde_get_tag (ret__struct_pde_C_' t_) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> xa_ = pd_ \<longrightarrow> {} = set_option (pde_stored_asid (ret__struct_pde_C_' t_)) proof (prove)
goal (3 subgoals):
 1. \<And>asida s. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?Q552 asida\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}\<rbrace>
 2. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q552 asida s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} \<longrightarrow> pd_at_asid' pd asid s \<and> valid_pde_mappings' s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}) \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> pd_at_asid' rv asid s \<and> valid_pde_mappings' s \<and> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some rv} \<longrightarrow> s' \<in> UNIV} \<inter> \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> \<inter> \<lbrace>asida >> unat Kernel_C.asidLowBits < 0x80\<rbrace> proof (prove)
goal:
No subgoals!