theory ArchFinalise_AI

lemma vs_lookup_pages_eq:
  "\<lbrakk>valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s;
    valid_cap cap s; table_cap_ref cap = Some vref; oref \<in> obj_refs cap\<rbrakk>
   \<Longrightarrow> (vref \<unrhd> oref) s = (vref \<rhd> oref) s" apply (clarsimp simp: table_cap_ref_def
                        vs_lookup_pages_eq_at[symmetric, THEN fun_cong]
                        vs_lookup_pages_eq_ap[symmetric, THEN fun_cong]
                 split: cap.splits arch_cap.splits option.splits) apply (rule iffI[rotated, OF vs_lookup_pages_vs_lookupI], assumption) apply (simp add: valid_cap_def) apply (erule vs_lookup_vs_lookup_pagesI', clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; s \<turnstile> cap; table_cap_ref cap = Some vref; oref \<in> obj_refs cap\<rbrakk> \<Longrightarrow> (vref \<unrhd> oref) s = (vref \<rhd> oref) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; s \<turnstile> ArchObjectCap (PageTableCap oref (Some (a, b))); cap = ArchObjectCap (PageTableCap oref (Some (a, b))); vref = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]\<rbrakk> \<Longrightarrow> ([VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<unrhd> oref) s = ([VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> oref) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; s \<turnstile> ArchObjectCap (PageTableCap oref (Some (a, b))); cap = ArchObjectCap (PageTableCap oref (Some (a, b))); vref = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]; ([VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<unrhd> oref) s\<rbrakk> \<Longrightarrow> ([VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> oref) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; cap_aligned (ArchObjectCap (PageTableCap oref (Some (a, b)))) \<and> typ_at (AArch APageTable) oref s \<and> 0 < a \<and> a < 2 ^ local.asid_bits \<and> b < kernel_base \<and> is_aligned b 20; cap = ArchObjectCap (PageTableCap oref (Some (a, b))); vref = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]; ([VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<unrhd> oref) s\<rbrakk> \<Longrightarrow> ([VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> oref) s proof (prove)
goal:
No subgoals!