theory ArchDecode_IF

lemma lookup_pt_slot_no_fail_is_subject:
  "\<lbrakk> (\<exists>\<rhd> pd) s; valid_vspace_objs s; pspace_aligned s; pas_refined aag s;
     is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base;
     kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (ucast (vptr >> 20)) = PageTablePDE p x xa \<rbrakk>
     \<Longrightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr p) vptr && ~~ mask pt_bits)" apply (clarsimp simp: lookup_pt_slot_no_fail_def) apply (drule valid_vspace_objsD) apply (simp add: obj_at_def) apply assumption apply (drule kheap_eq_state_vrefs_pas_refinedD) apply (erule vs_refs_no_global_pts_pdI) apply (drule(1) less_kernel_base_mapping_slots) apply (simp add: kernel_mapping_slots_def lookup_pd_slot_def pd_shifting_dual' triple_shift_fun) apply assumption apply (simp add: aag_has_Control_iff_owns) apply (drule_tac f="\<lambda>pde. valid_pde pde s" in arg_cong, simp) apply (clarsimp simp: obj_at_def kernel_base_kernel_mapping_slots) apply (erule pspace_alignedE, erule domI) apply (simp add: pt_bits_def pageBits_def) apply (subst is_aligned_add_helper, assumption) apply (rule shiftl_less_t2n) apply (rule order_le_less_trans, rule word_and_le1, simp) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ref. (ref \<rhd> pd) s; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr p) vptr && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; (ref \<rhd> pd) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (3 subgoals):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> ako_at (?ao1 ref) pd s
 2. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (?ao1 ref) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (2 subgoals):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pdo)); pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (3 subgoals):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> (?p'6 ref, ?r6 ref, ?t6 ref, ?a6 ref) \<in> vs_refs_no_global_pts (ArchObj (PageDirectory pdo))
 2. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> pas_refined (?aag6 ref) s
 3. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s; (pasObjectAbs (?aag6 ref) pd, ?a6 ref, pasObjectAbs (?aag6 ref) (?p'6 ref)) \<in> pasPolicy (?aag6 ref)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (3 subgoals):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> pas_refined (?aag6 ref) s
 3. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s; (pasObjectAbs (?aag6 ref) pd, Control, pasObjectAbs (?aag6 ref) (ptrFromPAddr p)) \<in> pasPolicy (?aag6 ref)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (3 subgoals):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; valid_vspace_obj (PageDirectory pdo) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> pas_refined (?aag6 ref) s
 3. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s; (pasObjectAbs (?aag6 ref) pd, Control, pasObjectAbs (?aag6 ref) (ptrFromPAddr p)) \<in> pasPolicy (?aag6 ref)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (2 subgoals):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s\<rbrakk> \<Longrightarrow> pas_refined (?aag6 ref) s
 2. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s; (pasObjectAbs (?aag6 ref) pd, Control, pasObjectAbs (?aag6 ref) (ptrFromPAddr p)) \<in> pasPolicy (?aag6 ref)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; valid_vspace_obj (PageDirectory pdo) s; (pasObjectAbs aag pd, Control, pasObjectAbs aag (ptrFromPAddr p)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); valid_pde (pdo (UCAST(32 \<rightarrow> 12) (vptr >> 20))) s = typ_at (AArch APageTable) (ptrFromPAddr p) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) (obj_bits (the (kheap s (ptrFromPAddr p))))\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2) && ~~ mask 10) proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 2. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p) proof (prove)
goal (3 subgoals):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (10 - 2)
 2. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 3. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p) proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdo x) s; is_subject aag (ptrFromPAddr p); kheap s (ptrFromPAddr p) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr p) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr p) proof (prove)
goal:
No subgoals!