theory ArchArch_IF

lemma find_pd_for_asid_not_arm_global_pd_large_page:
  "\<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 6 = 0
           \<longrightarrow> (\<forall>x \<in> set [0 , 4 .e. 0x3C].
                  x + 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) is_aligned_mask[symmetric]) apply (frule is_aligned_6_masks[where bits=pd_bits]) apply simp+ apply (subst(asm) lookup_pd_slot_eq) 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 6 = 0 \<longrightarrow> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + 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 6 = 0 \<longrightarrow> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + 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 x. \<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 6 = 0; x \<in> set [0 , 4 .e. 0x3C]; x + lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s rv x. \<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; is_aligned (lookup_pd_slot rv vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; x + 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 x. \<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; is_aligned (lookup_pd_slot rv vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; x + lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> pd_bits = pt_bits \<or> pd_bits = pd_bits
 2. \<And>s rv x. \<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; is_aligned (lookup_pd_slot rv vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; x + lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s); \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot rv vptr && ~~ mask pd_bits = lookup_pd_slot rv vptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s rv x. \<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; is_aligned (lookup_pd_slot rv vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s); \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + 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 x. \<lbrakk>\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s); 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; is_aligned (lookup_pd_slot rv vptr) 6; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> is_aligned rv pd_bits
 2. \<And>s rv x. \<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; is_aligned (lookup_pd_slot rv vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; rv = arm_global_pd (arch_state s); \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot rv vptr && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s rv x. \<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; is_aligned (lookup_pd_slot (arm_global_pd (arch_state s)) vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; rv = arm_global_pd (arch_state s); \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot (arm_global_pd (arch_state s)) vptr && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s rv x. \<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; is_aligned (lookup_pd_slot (arm_global_pd (arch_state s)) vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; rv = arm_global_pd (arch_state s); \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot (arm_global_pd (arch_state s)) vptr && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> arm_global_pd (arch_state s)) s
 2. \<And>s rv x. \<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; is_aligned (lookup_pd_slot (arm_global_pd (arch_state s)) vptr) 6; x \<in> set [0 , 4 .e. 0x3C]; rv = arm_global_pd (arch_state s); \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot (arm_global_pd (arch_state s)) vptr && ~~ mask pd_bits = arm_global_pd (arch_state s); arm_global_pd (arch_state s) \<notin> global_refs s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!