theory ArchArch_IF

lemma find_pd_for_asid_not_arm_global_pd:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs
                   and valid_vs_lookup and valid_global_refs and valid_arch_state\<rbrace>
   find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>, -" apply (wp find_pd_for_asid_lots) apply clarsimp apply (subst(asm) lookup_pd_slot_pd) apply (erule page_directory_at_aligned_pd_bits, simp+) apply (frule (4) not_in_global_refs_vs_lookup2) apply (auto simp: global_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state) s \<Longrightarrow> (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> ((\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. True)) proof (prove)
goal (1 subgoal):
 1. \<And>s rv. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_global_objs s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; typ_at (AArch APageDirectory) rv s; lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s rv. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_global_objs s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; typ_at (AArch APageDirectory) rv s\<rbrakk> \<Longrightarrow> is_aligned rv pd_bits
 2. \<And>s rv. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_global_objs s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; typ_at (AArch APageDirectory) rv s; rv = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s rv. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_global_objs s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; rv = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s rv. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_global_objs s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; rv = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> arm_global_pd (arch_state s)) s
 2. \<And>s rv. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_global_objs s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; rv = arm_global_pd (arch_state s); arm_global_pd (arch_state s) \<notin> global_refs s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!