theory VSpace_C

lemma pd_at_asid_cross_over:
  "\<lbrakk> pd_at_asid' pd asid s; asid \<le> mask asid_bits;
          (s, s') \<in> rf_sr\<rbrakk>
      \<Longrightarrow> \<exists>apptr ap pde. index (armKSASIDTable_' (globals s')) (unat (asid >> asid_low_bits))
                     = (ap_Ptr apptr) \<and> cslift s' (ap_Ptr apptr) = Some (asid_pool_C.asid_pool_C ap)
                  \<and> index ap (unat (asid && 2 ^ asid_low_bits - 1)) = pde_Ptr pd
                  \<and> cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde
                  \<and> is_aligned pd pdBits
                  \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s')))
                  \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = scast pde_pde_invalid)" apply (clarsimp simp: pd_at_asid'_def) apply (subgoal_tac "asid >> asid_low_bits \<le> 2 ^ asid_high_bits - 1") prefer 2 apply (simp add: asid_high_bits_word_bits) apply (rule shiftr_less_t2n) apply (simp add: mask_def) apply (simp add: asid_low_bits_def asid_high_bits_def asid_bits_def) apply (simp add: rf_sr_armKSASIDTable) apply (subgoal_tac "ucast (asid_high_bits_of asid) = asid >> asid_low_bits") prefer 2 apply (simp add: asid_high_bits_of_def ucast_ucast_mask asid_high_bits_def[symmetric]) apply (subst mask_eq_iff_w2p, simp add: asid_high_bits_def word_size) apply (rule shiftr_less_t2n) apply (simp add: mask_def, simp add: asid_bits_def asid_low_bits_def asid_high_bits_def) apply (simp add: option_to_ptr_def option_to_0_def) apply (rule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation],
         assumption, erule ko_at_projectKO_opt) apply (clarsimp simp: casid_pool_relation_def array_relation_def
                 split: asid_pool_C.split_asm) apply (drule spec, drule sym [OF mp]) apply (rule_tac y=asid in word_and_le1) apply (frule(1) page_directory_at_rf_sr) apply (clarsimp simp: mask_2pm1[symmetric] option_to_ptr_def option_to_0_def
                        page_directory_at'_def typ_at_to_obj_at_arches) apply (drule_tac x="pd_asid_slot" in spec, simp add: pd_asid_slot_def) apply (drule obj_at_ko_at'[where 'a=pde], clarsimp) apply (rule cmap_relationE1 [OF rf_sr_cpde_relation],
         assumption, erule ko_at_projectKO_opt) apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) apply (clarsimp simp: valid_pde_mappings'_def) apply (elim allE, drule(1) mp) apply (simp add: valid_pde_mapping'_def valid_pde_mapping_offset'_def
                   pd_asid_slot_def mask_add_aligned) apply (simp add: mask_def pdBits_def pageBits_def) apply (clarsimp simp add: cpde_relation_def Let_def) by (simp add: pde_lift_def Let_def pdeBits_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd_at_asid' pd asid s; asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>apptr ap pde. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> cslift s' (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 s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)))
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits < 2 ^ local.asid_high_bits
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s\<rbrakk> \<Longrightarrow> asid < 2 ^ (local.asid_low_bits + local.asid_high_bits)
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid < 2 ^ local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && 2 ^ local.asid_low_bits - 1) = Some pd; page_directory_at' pd s\<rbrakk> \<Longrightarrow> asid < 2 ^ (local.asid_low_bits + local.asid_high_bits)
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. armKSASIDTable_' (globals s').[unat (asid >> local.asid_low_bits)] = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)))
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) ((asid >> local.asid_low_bits) && mask local.asid_high_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> (asid >> local.asid_low_bits) && mask local.asid_high_bits = asid >> local.asid_low_bits
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) ((asid >> local.asid_low_bits) && mask local.asid_high_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits < 2 ^ local.asid_high_bits
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) ((asid >> local.asid_low_bits) && mask local.asid_high_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> asid < 2 ^ (local.asid_low_bits + local.asid_high_bits)
 2. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apptr. option_to_ptr (armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits)) = ap_Ptr apptr \<and> (\<exists>ap. cslift s' (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> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid))) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> \<exists>apa. cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C apa) \<and> apa.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool y'. \<lbrakk>asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); casid_pool_relation (asidpool.ASIDPool pool) y'; cslift s' (ap_Ptr ap) = Some y'\<rbrakk> \<Longrightarrow> \<exists>apa. cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C apa) \<and> apa.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); \<forall>i\<le>2 ^ local.asid_low_bits - 1. option_to_ptr (pool i) = x.[unat i]\<rbrakk> \<Longrightarrow> x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) proof (prove)
goal (2 subgoals):
 1. \<And>ap pool x. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool)\<rbrakk> \<Longrightarrow> ?i30 ap pool x \<le> 2 ^ local.asid_low_bits - 1
 2. \<And>ap pool x. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (?i30 ap pool x)] = option_to_ptr (pool (?i30 ap pool x))\<rbrakk> \<Longrightarrow> x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = option_to_ptr (pool (asid && 2 ^ local.asid_low_bits - 1))\<rbrakk> \<Longrightarrow> x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; page_directory_at' pd s; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = option_to_ptr (pool (asid && 2 ^ local.asid_low_bits - 1)); cslift s' (pd_Ptr pd) \<noteq> None\<rbrakk> \<Longrightarrow> x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd \<and> (\<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> is_aligned pd pdBits \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid)) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; \<forall>y<0x1000. obj_at' (\<lambda>_. True) (pd + (y << 2)) s\<rbrakk> \<Longrightarrow> \<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; obj_at' (\<lambda>_. True) (pd + 0x3FC0) s\<rbrakk> \<Longrightarrow> \<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; ko_at' ko (pd + 0x3FC0) s\<rbrakk> \<Longrightarrow> \<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'\<rbrakk> \<Longrightarrow> \<exists>pde. cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde \<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s'))) \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'\<rbrakk> \<Longrightarrow> valid_pde_mappings' s \<longrightarrow> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'; \<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde\<rbrakk> \<Longrightarrow> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'; valid_pde_mapping' (pd + 0x3FC0 && mask pdBits) ko\<rbrakk> \<Longrightarrow> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid \<le> mask local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && mask local.asid_low_bits) = Some pd; asid >> local.asid_low_bits \<le> mask local.asid_high_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && mask local.asid_low_bits)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd pdBits; ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'; ko = ARM_H.InvalidPDE \<or> 0x3FC0 && mask pdBits \<noteq> 0x3FC0\<rbrakk> \<Longrightarrow> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid < 2 ^ local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && 2 ^ local.asid_low_bits - 1) = Some pd; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd (12 + pdeBits); ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; cpde_relation ko y'; cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'; ko = ARM_H.InvalidPDE \<or> 0x3FC0 && 2 ^ (12 + pdeBits) - 1 \<noteq> 0x3FC0\<rbrakk> \<Longrightarrow> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>ap pool x y ko y'. \<lbrakk>cslift s' (ap_Ptr ap) = Some (asid_pool_C.asid_pool_C x); asid < 2 ^ local.asid_bits; (s, s') \<in> rf_sr; armKSASIDTable (ksArchState s) (asid >> local.asid_low_bits) = Some ap; ko_at' (asidpool.ASIDPool pool) ap s; pool (asid && 2 ^ local.asid_low_bits - 1) = Some pd; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = asid >> local.asid_low_bits; map_to_asidpools (ksPSpace s) ap = Some (asidpool.ASIDPool pool); x.[unat (asid && 2 ^ local.asid_low_bits - 1)] = pde_Ptr pd; cslift s' (pd_Ptr pd) = Some y; is_aligned pd (12 + pdeBits); ko_at' ko (pd + 0x3FC0) s; map_to_pdes (ksPSpace s) (pd + 0x3FC0) = Some ko; case ko of ARM_H.InvalidPDE \<Rightarrow> \<exists>inv. pde_lift y' = Some (Pde_pde_invalid inv) | ARM_H.PageTablePDE frame parity domain \<Rightarrow> pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = frame, P_CL = of_bool parity, Domain_CL = domain\<rparr>) | ARM_H.SectionPDE frame parity domain cacheable global xn rights \<Rightarrow> pde_lift y' = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 0, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = domain, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) | ARM_H.SuperSectionPDE frame parity cacheable global xn rights \<Rightarrow> pde_lift y' = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 1, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = 0, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>); cslift s' (pde_Ptr (pd + 0x3FC0)) = Some y'; ko = ARM_H.InvalidPDE \<or> 0x3FC0 && 2 ^ (12 + pdeBits) - 1 \<noteq> 0x3FC0\<rbrakk> \<Longrightarrow> pde_get_tag y' = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid