theory Fastpath_C

lemma stored_hw_asid_get_ccorres_split':
  assumes  ptr: "ptr = CTypesDefs.ptr_add pd 0xFF0"
  assumes ceqv: "\<And>rv' t t'. ceqv Gamm stored_hw_asid___struct_pde_C_' rv' t t' c (c' rv')"
   and ccorres: "\<And>shw_asid. pde_get_tag shw_asid = scast pde_pde_invalid \<Longrightarrow>
                      ccorres_underlying rf_sr Gamm r xf ar axf
                                   (Q shw_asid) (R shw_asid) hs
                                   a (c' shw_asid)"
  shows "ccorres_underlying rf_sr Gamm r xf ar axf
                (\<lambda>s. page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s
                      \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd)
                               = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = scast pde_pde_invalid
                             \<longrightarrow> P shw_asid \<and> Q shw_asid s))
                {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = scast pde_pde_invalid
                            \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid
                      \<longrightarrow> s \<lparr> stored_hw_asid___struct_pde_C_' := stored_hw_asid \<rparr>
                                 \<in> R stored_hw_asid} hs
                a (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t ptr\<rbrace>
                       (\<acute>stored_hw_asid___struct_pde_C :==
                               h_val (hrs_mem \<acute>t_hrs) ptr);; c)" unfolding ptr apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard_Seq) apply (rule ccorres_symb_exec_r) apply (rule ccorres_abstract_all[OF ceqv]) apply (rule_tac A="\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd)
                               = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = scast pde_pde_invalid
                            \<longrightarrow> P rv' \<and> Q rv' s"
                and A'="{s. P rv' \<longrightarrow> s \<in> R rv'}
                         \<inter> {s. (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd)
                                  = Some rv' \<and> pde_get_tag rv' = scast pde_pde_invalid}"
                in ccorres_guard_imp2) apply (rule_tac P="pde_get_tag rv' = scast pde_pde_invalid" in ccorres_gen_asm) apply (erule ccorres) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                           carch_state_relation_def
                           map_comp_Some_iff) apply vcg apply (rule conseqPre, vcg) apply clarsimp apply clarsimp apply (frule_tac x=pd_asid_slot in page_directory_pde_atI') apply (simp add: pd_asid_slot_def pageBits_def) apply (cases pd) apply (simp add: typ_at_to_obj_at_arches) apply (drule obj_at_ko_at') apply (clarsimp simp: pd_asid_slot_def) apply (erule cmap_relationE1[OF rf_sr_cpde_relation], erule ko_at_projectKO_opt) apply (frule(1) valid_pde_mappings_ko_atD') apply (clarsimp simp: typ_heap_simps' map_comp_Some_iff
                        valid_pde_mapping'_def) apply (clarsimp simp: pd_pointer_to_asid_slot_def page_directory_at'_def
                        add_mask_eq pdBits_def pageBits_def word_bits_def
                        valid_pde_mapping_offset'_def pd_asid_slot_def
                         pdeBits_def) apply (simp add: cpde_relation_def Let_def pde_lift_def
            split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr Gamm r xf ar axf (\<lambda>s. page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s)) {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid} hs a (Guard C_Guard {s. s \<Turnstile>\<^sub>c ptr} (\<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) ptr);;
c) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr Gamm r xf ar axf (\<lambda>s. page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s)) {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid} hs a (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} (\<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080));;
c) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr Gamm r xf ar axf ?Q ?Q' hs a (Guard C_Guard {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} (\<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080));;
c)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr Gamm r xf ar axf ?Q ?C'3 hs a (\<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080);;
c)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (4 subgoals):
 1. ccorres_underlying rf_sr Gamm r xf ar axf ?Q ?Q'5 hs a c
 2. Gamm\<turnstile> ?C'3 \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) ?Q'5
 3. \<And>s. ?Q s \<Longrightarrow> Gamm\<turnstile> (?C'3 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (4 subgoals):
 1. \<And>rv'. ccorres_underlying rf_sr Gamm r xf ar axf (?G9 rv') (?G'9 rv') hs a (c' rv')
 2. Gamm\<turnstile> ?C'3 \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s. s \<in> ?G'9 (stored_hw_asid___struct_pde_C_' s)}
 3. \<And>s. \<forall>rv'. ?G9 rv' s \<Longrightarrow> Gamm\<turnstile> (?C'3 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. ?G9 rv' s) \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (5 subgoals):
 1. \<And>rv'. ccorres_underlying rf_sr Gamm r xf ar axf (?Q14 rv') (?Q'14 rv') hs a (c' rv')
 2. \<And>rv' s s'. \<lbrakk>(s, s') \<in> rf_sr; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s; s' \<in> {s. P rv' \<longrightarrow> s \<in> R rv'} \<inter> {s. (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some rv' \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}\<rbrakk> \<Longrightarrow> ?Q14 rv' s \<and> s' \<in> ?Q'14 rv'
 3. Gamm\<turnstile> ?C'3 \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s. s \<in> {sa. P (stored_hw_asid___struct_pde_C_' s) \<longrightarrow> sa \<in> R (stored_hw_asid___struct_pde_C_' s)} \<inter> {sa. (cslift sa \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (stored_hw_asid___struct_pde_C_' s) \<and> pde_get_tag (stored_hw_asid___struct_pde_C_' s) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}
 4. \<And>s. \<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s \<Longrightarrow> Gamm\<turnstile> (?C'3 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (5 subgoals):
 1. \<And>rv'. pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf ar axf (?G15 rv') (?Q'14 rv') hs a (c' rv')
 2. \<And>rv' s s'. \<lbrakk>(s, s') \<in> rf_sr; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s; s' \<in> {s. P rv' \<longrightarrow> s \<in> R rv'} \<inter> {s. (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some rv' \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}\<rbrakk> \<Longrightarrow> (?G15 rv' and (\<lambda>_. pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) s \<and> s' \<in> ?Q'14 rv'
 3. Gamm\<turnstile> ?C'3 \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s. s \<in> {sa. P (stored_hw_asid___struct_pde_C_' s) \<longrightarrow> sa \<in> R (stored_hw_asid___struct_pde_C_' s)} \<inter> {sa. (cslift sa \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (stored_hw_asid___struct_pde_C_' s) \<and> pde_get_tag (stored_hw_asid___struct_pde_C_' s) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}
 4. \<And>s. \<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s \<Longrightarrow> Gamm\<turnstile> (?C'3 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (4 subgoals):
 1. \<And>rv' s s'. \<lbrakk>(s, s') \<in> rf_sr; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s; s' \<in> {s. P rv' \<longrightarrow> s \<in> R rv'} \<inter> {s. (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some rv' \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}\<rbrakk> \<Longrightarrow> (Q rv' and (\<lambda>_. pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) s \<and> s' \<in> R rv'
 2. Gamm\<turnstile> ?C'3 \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s. s \<in> {sa. P (stored_hw_asid___struct_pde_C_' s) \<longrightarrow> sa \<in> R (stored_hw_asid___struct_pde_C_' s)} \<inter> {sa. (cslift sa \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (stored_hw_asid___struct_pde_C_' s) \<and> pde_get_tag (stored_hw_asid___struct_pde_C_' s) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}
 3. \<And>s. \<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s \<Longrightarrow> Gamm\<turnstile> (?C'3 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (3 subgoals):
 1. Gamm\<turnstile> ?C'3 \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s. s \<in> {sa. P (stored_hw_asid___struct_pde_C_' s) \<longrightarrow> sa \<in> R (stored_hw_asid___struct_pde_C_' s)} \<inter> {sa. (cslift sa \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (stored_hw_asid___struct_pde_C_' s) \<and> pde_get_tag (stored_hw_asid___struct_pde_C_' s) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}
 2. \<And>s. \<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s \<Longrightarrow> Gamm\<turnstile> (?C'3 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> ?C'3 \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s \<Longrightarrow> Gamm\<turnstile> ({s. (P (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080))) \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid} \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>stored_hw_asid___struct_pde_C :== h_val (hrs_mem \<acute>t_hrs) (pd +\<^sub>p 4080) {s'. (s, s') \<in> rf_sr}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> {s. (P (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080))) \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid} \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s \<Longrightarrow> {s. (P (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080))) \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid} \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, sa\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals sa))) (pd +\<^sub>p 4080)\<rparr>) \<in> rf_sr}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> {s. (P (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080))) \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid} \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' (ptr_val pd) s \<and> valid_pde_mappings' s \<and> (\<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s); s' \<in> {s. \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid}\<rbrakk> \<Longrightarrow> (\<forall>rv'. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid rv') \<and> pde_get_tag rv' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P rv' \<and> Q rv' s) \<and> s' \<in> {s. (P (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<longrightarrow> s\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080))) \<and> (cslift s \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid} \<inter> {s. s \<Turnstile>\<^sub>c (pd +\<^sub>p 4080)} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' (ptr_val pd) s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c (pd +\<^sub>p 4080) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' (ptr_val pd) s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s\<rbrakk> \<Longrightarrow> pd_asid_slot < 2 ^ pageBits
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' (ptr_val pd) s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pde_at' (ptr_val pd + (pd_asid_slot << 2)) s\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c (pd +\<^sub>p 4080) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' (ptr_val pd) s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pde_at' (ptr_val pd + (pd_asid_slot << 2)) s\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c (pd +\<^sub>p 4080) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' (ptr_val pd) s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) (ptr_val pd) = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pde_at' (ptr_val pd + (pd_asid_slot << 2)) s; pd = pde_Ptr x\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) (ptr_val pd) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pd +\<^sub>p 4080)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c (pd +\<^sub>p 4080) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' x s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; obj_at' (\<lambda>_. True) (x + (pd_asid_slot << 2)) s; pd = pde_Ptr x\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0)))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c pde_Ptr (x + 0x3FC0) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' x s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pd = pde_Ptr x; \<exists>ko. ko_at' ko (x + (pd_asid_slot << 2)) s \<and> True\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0)))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c pde_Ptr (x + 0x3FC0) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x ko. \<lbrakk>(s, s') \<in> rf_sr; \<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' x s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pd = pde_Ptr x; ko_at' ko (x + 0x3FC0) s\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0)))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c pde_Ptr (x + 0x3FC0) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x ko y'. \<lbrakk>\<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' x s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pd = pde_Ptr x; ko_at' ko (x + 0x3FC0) s; map_to_pdes (ksPSpace s) (x + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (x + 0x3FC0)) = Some y'\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0)))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c pde_Ptr (x + 0x3FC0) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x ko y'. \<lbrakk>\<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some stored_hw_asid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' x s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pd = pde_Ptr x; ko_at' ko (x + 0x3FC0) s; map_to_pdes (ksPSpace s) (x + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (x + 0x3FC0)) = Some y'; ko_at' ko (x + 0x3FC0) s \<and> valid_pde_mapping' (x + 0x3FC0 && mask pdBits) ko\<rbrakk> \<Longrightarrow> (P (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))\<rparr> \<in> R (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0)))) \<and> (cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) x = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) \<and> pde_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (pde_Ptr (x + 0x3FC0))) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> s' \<Turnstile>\<^sub>c pde_Ptr (x + 0x3FC0) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x ko y' k'. \<lbrakk>\<forall>stored_hw_asid. P stored_hw_asid \<and> pde_get_tag stored_hw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (\<exists>k'. pd_pointer_to_asid_slot x = Some k' \<and> cslift s' k' = Some stored_hw_asid) \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := stored_hw_asid\<rparr> \<in> R stored_hw_asid; page_directory_at' x s; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pd = pde_Ptr x; cpde_relation ko y'; cslift s' (pde_Ptr (x + 0x3FC0)) = Some y'; ko_at' ko (x + 0x3FC0) s; ko = ARM_H.InvalidPDE \<or> valid_pde_mapping_offset' (x + 0x3FC0 && mask pdBits); ksPSpace s (x + 0x3FC0) = Some k'; projectKO_opt k' = Some ko\<rbrakk> \<Longrightarrow> (P y' \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := y'\<rparr> \<in> R y') \<and> (\<exists>k'. pd_pointer_to_asid_slot x = Some k' \<and> cslift s' k' = Some y') \<and> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>s s' x y' k'. \<lbrakk>P y' \<and> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := y'\<rparr> \<in> R y'; valid_pde_mappings' s; \<forall>shw_asid. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) x = set_option (pde_stored_asid shw_asid) \<and> pde_get_tag shw_asid = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> P shw_asid \<and> Q shw_asid s; pd = pde_Ptr x; cpde_relation ARM_H.InvalidPDE y'; cslift s' (pde_Ptr (x + 0x3FC0)) = Some y'; ko_at' ARM_H.InvalidPDE (x + 0x3FC0) s; ksPSpace s (x + 0x3FC0) = Some k'; projectKO_opt k' = Some ARM_H.InvalidPDE; is_aligned x 14; \<forall>y<0x1000. pde_at' (x + (y << 2)) s\<rbrakk> \<Longrightarrow> (P y' \<longrightarrow> s'\<lparr>stored_hw_asid___struct_pde_C_' := y'\<rparr> \<in> R y') \<and> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal:
No subgoals!