theory ArchArch_AC

lemma perform_page_invocation_pas_refined [wp]:
  "\<lbrace>pas_refined aag and invs and K (authorised_page_inv aag pgi) and valid_page_inv pgi\<rbrace>
   perform_page_invocation pgi
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: perform_page_invocation_def mapM_discarded valid_page_inv_def valid_unmap_def
                   swp_def authorised_page_inv_def authorised_slots_def
             cong: page_invocation.case_cong sum.case_cong) apply (rule hoare_pre) apply wpc apply (wp set_cap_pas_refined unmap_page_pas_refined case_sum_wp case_prod_wp get_cap_wp
                mapM_x_and_const_wp[OF store_pte_pas_refined] hoare_vcg_all_lift
                mapM_x_and_const_wp[OF store_pde_pas_refined] hoare_vcg_const_imp_lift unmap_page_invs
             | (wp hoare_vcg_imp_lift, unfold disj_not1)
             | strengthen clas_update_map_data_strg
             | wpc | wps | simp | strengthen invs_vspace_objs invs_arch_state)+ apply (case_tac pgi) apply ((force simp: valid_slots_def pte_ref_def cte_wp_at_caps_of_state
                         is_transferable_is_arch_update[symmetric] valid_cap_def
                         pde_ref2_def auth_graph_map_mem pas_refined_refl mask_2pm1
                  split: sum.splits)+)[2] apply (clarsimp simp: cte_wp_at_caps_of_state is_transferable_is_arch_update[symmetric]
                          pte_ref_def pde_ref2_def is_cap_simps is_pg_cap_def) apply (frule(1) cap_cur_auth_caps_of_state, simp) apply (intro impI conjI;
           clarsimp; (* NB: for speed *)
           clarsimp simp: update_map_data_def clas_no_asid aag_cap_auth_def
                          cap_auth_conferred_def arch_cap_auth_conferred_def
                          vspace_cap_rights_to_auth_def cli_no_irqs is_pg_cap_def
                          valid_cap_def mask_2pm1 pte_ref_def[simplified aag_cap_auth_def])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and K (authorised_page_inv aag pgi) and valid_page_inv pgi\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and (\<lambda>y. case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) and (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True)\<rbrace> case pgi of PageMap asid cap ct_slot entries \<Rightarrow> do y <- set_cap cap ct_slot;
y <- case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
y <- store_pte (hd slots) pte;
_ <- mapM_x (\<lambda>y. store_pte y InvalidPTE) (tl slots);
y <- do_machine_op (cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots)));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
y <- store_pde (hd slots) pde;
_ <- mapM_x (\<lambda>y. store_pde y InvalidPDE) (tl slots);
y <- do_machine_op (cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots)));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do y <- when (start < end) (do root_switched <- set_vm_root_for_flush pd asid;
y <- do_machine_op (do_flush typ start end pstart);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q26\<rbrace> case pgi of PageMap asid cap ct_slot entries \<Rightarrow> do y <- set_cap cap ct_slot;
y <- case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
y <- store_pte (hd slots) pte;
_ <- mapM_x (\<lambda>y. store_pte y InvalidPTE) (tl slots);
y <- do_machine_op (cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots)));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
y <- store_pde (hd slots) pde;
_ <- mapM_x (\<lambda>y. store_pde y InvalidPDE) (tl slots);
y <- do_machine_op (cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots)));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do y <- when (start < end) (do root_switched <- set_vm_root_for_flush pd asid;
y <- do_machine_op (do_flush typ start end pstart);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and invs and (\<lambda>y. case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) and (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True)) s \<Longrightarrow> ?Q26 s proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14. pgi = PageMap x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?R53 x11 x12 x13 x14\<rbrace> do y <- set_cap x12 x13;
y <- case x14 of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
y <- store_pte (hd slots) pte;
_ <- mapM_x (\<lambda>y. store_pte y InvalidPTE) (tl slots);
y <- do_machine_op (cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots)));
if flush then invalidate_tlb_by_asid x11 else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
y <- store_pde (hd slots) pde;
_ <- mapM_x (\<lambda>y. store_pde y InvalidPDE) (tl slots);
y <- do_machine_op (cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots)));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x21 x22. pgi = PageUnmap x21 x22 \<Longrightarrow> \<lbrace>?R54 x21 x22\<rbrace> case x21 of PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap x22;
set_cap (ArchObjectCap $ update_map_data cap None) x22;
return []
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>?R55 x31 x32 x33 x34 x35 x36\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>?R56 x4\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>s. (pas_refined aag and invs and (\<lambda>y. case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) and (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True)) s \<Longrightarrow> (\<forall>x xa xb xc. pgi = PageMap x xa xb xc \<longrightarrow> ?R53 x xa xb xc s) \<and> (\<forall>x xa. pgi = PageUnmap x xa \<longrightarrow> ?R54 x xa s) \<and> (\<forall>x xa xb xc xd xe. pgi = PageFlush x xa xb xc xd xe \<longrightarrow> ?R55 x xa xb xc xd xe s) \<and> (\<forall>x. pgi = PageGetAddr x \<longrightarrow> ?R56 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None)))))) proof (prove)
goal (4 subgoals):
 1. \<And>s x11 x12 x13 x14. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageMap x11 x12 x13 x14\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 2. \<And>s x21 x22. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageUnmap x21 x22\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 3. \<And>s x31 x32 x33 x34 x35 x36. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageFlush x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 4. \<And>s x4. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageGetAddr x4\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None)))))) proof (prove)
goal (3 subgoals):
 1. \<And>s x21 x22. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageUnmap x21 x22\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 2. \<And>s x31 x32 x33 x34 x35 x36. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageFlush x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 3. \<And>s x4. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageGetAddr x4\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None)))))) proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb xc xd xe xf xg. \<lbrakk>pgi = PageUnmap (PageCap xb xc xd xe xf) (x, xa); pas_refined aag s; invs s; pas_cap_cur_auth aag (ArchObjectCap (PageCap xb xc xd xe xf)); is_subject aag x; case xf of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (xe = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (xe = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (xe = ARMSection \<longrightarrow> is_aligned vptr 20); caps_of_state s (x, xa) = Some (ArchObjectCap (PageCap xb xc xd xe xf)); s \<turnstile> ArchObjectCap (PageCap xb xc xd xe xf)\<rbrakk> \<Longrightarrow> (xf = None \<longrightarrow> ArchObjectCap (PageCap xb xc xd xe None) = xg \<longrightarrow> pspace_aligned s \<and> (is_transferable_cap xg \<and> \<not> Option.is_none (cdt s (x, xa)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (x, xa)))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap xg) None))) \<and> (\<forall>a b. xf = Some (a, b) \<longrightarrow> ArchObjectCap (PageCap xb xc xd xe (Some (a, b))) = xg \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xe \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xe \<and> (is_transferable_cap xg \<and> \<not> Option.is_none (cdt s (x, xa)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (x, xa)))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap xg) None)))
 2. \<And>s x31 x32 x33 x34 x35 x36. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageFlush x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 3. \<And>s x4. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageGetAddr x4\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None)))))) proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb xc xd xe xf xg. \<lbrakk>pgi = PageUnmap (PageCap xb xc xd xe xf) (x, xa); pas_refined aag s; invs s; pas_cap_cur_auth aag (ArchObjectCap (PageCap xb xc xd xe xf)); is_subject aag x; case xf of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (xe = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (xe = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (xe = ARMSection \<longrightarrow> is_aligned vptr 20); caps_of_state s (x, xa) = Some (ArchObjectCap (PageCap xb xc xd xe xf)); s \<turnstile> ArchObjectCap (PageCap xb xc xd xe xf); pas_cap_cur_auth aag (ArchObjectCap (PageCap xb xc xd xe xf))\<rbrakk> \<Longrightarrow> (xf = None \<longrightarrow> ArchObjectCap (PageCap xb xc xd xe None) = xg \<longrightarrow> pspace_aligned s \<and> (is_transferable_cap xg \<and> \<not> Option.is_none (cdt s (x, xa)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (x, xa)))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap xg) None))) \<and> (\<forall>a b. xf = Some (a, b) \<longrightarrow> ArchObjectCap (PageCap xb xc xd xe (Some (a, b))) = xg \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xe \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xe \<and> (is_transferable_cap xg \<and> \<not> Option.is_none (cdt s (x, xa)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (x, xa)))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap xg) None)))
 2. \<And>s x31 x32 x33 x34 x35 x36. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageFlush x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))))))
 3. \<And>s x4. \<lbrakk>pas_refined aag s \<and> invs s \<and> (case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> (case slots of Inl (pte, slots) \<Rightarrow> (\<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))) | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True) \<and> (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some (asid, vptr) \<Rightarrow> 0 < asid \<and> is_aligned vptr pageBits \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned vptr 20)) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; pgi = PageGetAddr x4\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. pgi = PageMap x xa (xb, xc) xd \<longrightarrow> (\<forall>x xe. xd = Inl (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (\<forall>a aa b. pte_ref x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag)) \<and> (\<forall>v\<in>set (tl xe). \<forall>a aa b. pte_ref InvalidPTE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pt_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>x xe. xd = Inr (x, xe) \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xb, xc) s \<and> \<not> Option.is_none (cdt s (xb, xc)) \<longrightarrow> is_transferable_cap xa \<or> (pasObjectAbs aag (fst (the (cdt s (xb, xc)))), Control, pasObjectAbs aag xb) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xb) xa \<and> (UCAST(32 \<rightarrow> 12) (hd xe && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 x = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(hd xe && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))) \<and> (\<forall>v\<in>set (tl xe). UCAST(32 \<rightarrow> 12) (v && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 InvalidPDE = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(v && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag))))) \<and> (\<forall>x xa xb. pgi = PageUnmap x (xa, xb) \<longrightarrow> (\<forall>xc xd xe xf xg. x = PageCap xc xd xe xf xg \<longrightarrow> (\<forall>x. (xg = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xg = Some (a, b) \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xf \<and> (is_transferable_in (xa, xb) s \<and> \<not> Option.is_none (cdt s (xa, xb)) \<longrightarrow> (pasObjectAbs aag (fst (the (cdt s (xa, xb)))), Control, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag xa) (ArchObjectCap (update_map_data (the_arch_cap x) None)))))) proof (prove)
goal:
No subgoals!