theory ArchArch_AC

lemma perform_page_table_invocation_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and valid_pti iv and K (authorised_page_table_inv aag iv)\<rbrace>
   perform_page_table_invocation iv
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: perform_page_table_invocation_def
             cong: page_table_invocation.case_cong option.case_cong prod.case_cong
                   cap.case_cong arch_cap.case_cong) apply (rule hoare_pre) apply (wp get_cap_wp mapM_wp' store_pte_cte_wp_at do_machine_op_cte_wp_at
            hoare_vcg_all_lift set_cap_pas_refined_not_transferable
         | (wp hoare_vcg_imp_lift, unfold disj_not1)
         | simp add: mapM_x_mapM authorised_page_table_inv_def imp_conjR pte_ref_simps
         | wpc | wps | blast | strengthen invs_vspace_objs invs_arch_state)+ apply (clarsimp simp: invs_psp_aligned) apply (cases iv) apply (fastforce simp: cte_wp_at_caps_of_state Option.is_none_def
                          is_transferable_is_arch_update[symmetric]
                          valid_pti_def is_cap_simps pas_refined_refl auth_graph_map_def2
                    dest: pde_ref_pde_ref2) apply (rename_tac s pt_cap page_cslot) apply (case_tac page_cslot) apply (rename_tac page_ptr page_slot) apply (case_tac "\<exists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)") prefer 2 apply fastforce apply (elim exE) apply clarsimp apply (rename_tac page_cap) apply (subgoal_tac
            "cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow>
             cte_wp_at (\<lambda>c. \<not> is_transferable (Some c)) (page_ptr, page_slot) s \<and>
             pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None))") apply (fastforce simp: cte_wp_at_caps_of_state valid_pti_def valid_cap_def
                          mask_2pm1 cap_aligned_def vmsz_aligned_def) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule (1) cap_cur_auth_caps_of_state) apply simp apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state mask_PTCap_eq) apply (clarsimp simp: cap_auth_conferred_def arch_cap_auth_conferred_def update_map_data_def
                        is_page_cap_def cap_links_asid_slot_def cap_links_irq_def aag_cap_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and valid_pti iv and K (authorised_page_table_inv aag iv)\<rbrace> perform_page_table_invocation iv \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_page_table_inv aag iv \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_pti iv\<rbrace> perform_page_table_invocation iv \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_page_table_inv aag iv \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_pti iv\<rbrace> case iv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do y <- set_cap cap ct_slot;
y <- store_pde pd_slot pde;
do_machine_op (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot))
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do y <- case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmap_page_table asid vaddr p;
y <- mapM_x (swp store_pte InvalidPTE) [p , p + 4 .e. p + 2 ^ pt_bits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ pt_bits - 1) (addrFromPPtr p))
od;
cap <- liftM the_arch_cap (get_cap ct_slot);
set_cap (ArchObjectCap (update_map_data cap None)) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. authorised_page_table_inv aag iv \<Longrightarrow> \<lbrace>?Q16\<rbrace> case iv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do y <- set_cap cap ct_slot;
y <- store_pde pd_slot pde;
do_machine_op (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot))
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do y <- case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmap_page_table asid vaddr p;
y <- mapM_x (swp store_pte InvalidPTE) [p , p + 4 .e. p + 2 ^ pt_bits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ pt_bits - 1) (addrFromPPtr p))
od;
cap <- liftM the_arch_cap (get_cap ct_slot);
set_cap (ArchObjectCap (update_map_data cap None)) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>authorised_page_table_inv aag iv; (pas_refined aag and invs and valid_pti iv) s\<rbrakk> \<Longrightarrow> ?Q16 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s \<and> invs s \<and> valid_pti iv s\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> pspace_aligned s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pspace_aligned s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x13 x14. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableMap x11 x12 x13 x14\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None)))))))))
 2. \<And>s x21 x22. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x21 x22. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pt_cap page_cslot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pt_cap page_cslot a b. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (a, b)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pt_cap page_cslot page_ptr page_slot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt_cap page_cslot page_ptr page_slot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot); \<exists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None)))))))))
 2. \<And>s pt_cap page_cslot page_ptr page_slot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot); \<nexists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt_cap page_cslot page_ptr page_slot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot); \<nexists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None)))))))))
 2. \<And>s pt_cap page_cslot page_ptr page_slot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot); \<exists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pt_cap page_cslot page_ptr page_slot. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot); \<exists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pt_cap page_cslot page_ptr page_slot pt_ptr mapping. \<lbrakk>case iv of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); pas_refined aag s; invs s; valid_pti iv s; iv = PageTableUnmap pt_cap page_cslot; page_cslot = (page_ptr, page_slot); pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> aag_cap_auth aag (pasObjectAbs aag xa) x) \<and> (iv = PageTableMap x (xa, xb) xc xd \<longrightarrow> UCAST(32 \<rightarrow> 12) (xd && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xc = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(xd && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))) \<and> (\<forall>x xa xb. iv = PageTableUnmap x (xa, xb) \<longrightarrow> (\<forall>xc. x = ArchObjectCap xc \<longrightarrow> (\<forall>x xd. xc = PageTableCap x xd \<longrightarrow> (\<forall>x. (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (xa, xb) s) \<and> (xd = None \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>xc xd. (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xc \<le> mask local.asid_bits) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> xd < kernel_base) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> vmsz_aligned xd ARMSection) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (xa, xb) s) \<and> (a = xc \<and> b = xd \<longrightarrow> cte_wp_at ((=) x) (xa, xb) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s page_ptr page_slot pt_ptr mapping x. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (mapping = None \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (page_ptr, page_slot) s) \<and> (mapping = None \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))) \<and> (\<forall>a b. mapping = Some (a, b) \<longrightarrow> (\<forall>xa xb. (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> xa \<le> mask local.asid_bits) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> xb < kernel_base) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> vmsz_aligned xb ARMSection) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> xa \<le> mask local.asid_bits) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> xb < kernel_base) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> vmsz_aligned xb ARMSection) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (page_ptr, page_slot) s) \<and> (a = xa \<and> b = xb \<longrightarrow> cte_wp_at ((=) x) (page_ptr, page_slot) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap x) None))))) proof (prove)
goal (1 subgoal):
 1. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (mapping = None \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (page_ptr, page_slot) s) \<and> (mapping = None \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None))) \<and> (\<forall>a b. mapping = Some (a, b) \<longrightarrow> (\<forall>x xa. (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> x \<le> mask local.asid_bits) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> xa < kernel_base) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> vmsz_aligned xa ARMSection) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> x \<le> mask local.asid_bits) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> xa < kernel_base) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> vmsz_aligned xa ARMSection) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (page_ptr, page_slot) s) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None))))) proof (prove)
goal (2 subgoals):
 1. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)); cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (page_ptr, page_slot) s \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None))\<rbrakk> \<Longrightarrow> (mapping = None \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (page_ptr, page_slot) s) \<and> (mapping = None \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None))) \<and> (\<forall>a b. mapping = Some (a, b) \<longrightarrow> (\<forall>x xa. (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> x \<le> mask local.asid_bits) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> xa < kernel_base) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> vmsz_aligned xa ARMSection) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> x \<le> mask local.asid_bits) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> xa < kernel_base) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> vmsz_aligned xa ARMSection) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) (page_ptr, page_slot) s) \<and> (a = x \<and> b = xa \<longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None)))))
 2. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (page_ptr, page_slot) s \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None)) proof (prove)
goal (1 subgoal):
 1. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (page_ptr, page_slot) s \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None)) proof (prove)
goal (1 subgoal):
 1. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)); caps_of_state s (page_ptr, page_slot) = Some page_cap\<rbrakk> \<Longrightarrow> \<not> is_transferable_cap page_cap \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None)) proof (prove)
goal (2 subgoals):
 1. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)); caps_of_state s (page_ptr, page_slot) = Some page_cap\<rbrakk> \<Longrightarrow> is_subject aag (fst (page_ptr, page_slot))
 2. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)); caps_of_state s (page_ptr, page_slot) = Some page_cap; pas_cap_cur_auth aag page_cap\<rbrakk> \<Longrightarrow> \<not> is_transferable_cap page_cap \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None)) proof (prove)
goal (1 subgoal):
 1. \<And>s page_ptr page_slot pt_ptr mapping page_cap. \<lbrakk>pas_refined aag s; invs s; valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot)) s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)); caps_of_state s (page_ptr, page_slot) = Some page_cap; pas_cap_cur_auth aag page_cap\<rbrakk> \<Longrightarrow> \<not> is_transferable_cap page_cap \<and> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (the_arch_cap page_cap) None)) proof (prove)
goal (1 subgoal):
 1. \<And>s page_ptr page_slot pt_ptr mapping. \<lbrakk>pas_refined aag s; invs s; iv = PageTableUnmap (ArchObjectCap (PageTableCap pt_ptr mapping)) (page_ptr, page_slot); is_subject aag page_ptr; \<forall>asid. (\<exists>vspace_ref. mapping = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [pt_ptr , pt_ptr + 4 .e. pt_ptr + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)); caps_of_state s (page_ptr, page_slot) = Some (ArchObjectCap (PageTableCap pt_ptr mapping)); pas_cap_cur_auth aag (ArchObjectCap (PageTableCap pt_ptr mapping)); s \<turnstile> ArchObjectCap (PageTableCap pt_ptr mapping); is_final_cap' (ArchObjectCap (PageTableCap pt_ptr mapping)) s; is_pt_cap (ArchObjectCap (PageTableCap pt_ptr mapping))\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (update_map_data (PageTableCap pt_ptr mapping) None)) proof (prove)
goal:
No subgoals!