theory VSpace_R

lemma performPageTableInvocation_corres:
  "page_table_invocation_map pti pti' \<Longrightarrow>
   corres dc
          (invs and valid_etcbs and valid_pti pti)
          (invs' and valid_pti' pti')
          (perform_page_table_invocation pti)
          (performPageTableInvocation pti')"
  (is "?mp \<Longrightarrow> corres dc ?P ?P' ?f ?g") apply (simp add: perform_page_table_invocation_def performPageTableInvocation_def) apply (cases pti) apply (clarsimp simp: page_table_invocation_map_def) apply (rule corres_guard_imp) apply (rule corres_split[OF updateCap_same_master]) apply assumption apply (rule corres_split) apply (rule storePDE_corres') apply (simp add: pde_relation_aligned_def) apply (rule corres_machine_op) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_cleanByVA_PoU) apply (wp set_cap_typ_at)+ apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state is_arch_update_def) apply (clarsimp simp: is_cap_simps cap_master_cap_simps
                    dest!: cap_master_cap_eqDs) apply auto[1] apply (clarsimp simp: cte_wp_at_ctes_of valid_pti'_def) apply auto[1] apply (clarsimp simp:valid_pde_mapping'_def split:ARM_H.pde.split) apply (rename_tac cap a b) apply (clarsimp simp: page_table_invocation_map_def) apply (rule_tac F="is_pt_cap cap" in corres_req) apply (clarsimp simp: valid_pti_def) apply (clarsimp simp: is_pt_cap_def split_def
                        pt_bits_stuff objBits_simps archObjSize_def
                  cong: option.case_cong) apply (simp add: case_option_If2 getSlotCap_def split del: if_split) apply (rule corres_guard_imp) apply (rule corres_split_nor) apply (rule corres_if[OF refl _ corres_trivial]) apply (rule corres_split[OF unmapPageTable_corres]) apply (rule corres_split_nor) apply (simp add: pteBits_def)+ apply (rule clear_page_table_corres) apply (rule corres_machine_op, rule corres_Id) apply wpsimp+ apply (simp add: liftM_def) apply (rule corres_split[OF get_cap_corres]) apply (rule_tac F="is_pt_cap x" in corres_gen_asm) apply (rule updateCap_same_master) apply (clarsimp simp: is_pt_cap_def update_map_data_def) apply (wp get_cap_wp) apply wp apply (simp add: cte_wp_at_caps_of_state pred_conj_def
                  split del: if_split) apply (rule hoare_lift_Pf2[where f=caps_of_state]) apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
                mapM_x_wp' | simp split del: if_split)+ apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state
                         cap_master_cap_simps
                         update_map_data_def is_cap_simps
                         cap_rights_update_def acap_rights_update_def
                  dest!: cap_master_cap_eqDs) apply (auto simp: valid_cap_def mask_def cap_master_cap_def
                     cap_rights_update_def acap_rights_update_def
              split: option.split_asm)[1] apply (auto simp: valid_pti'_def cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_table_invocation_map pti pti' \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (perform_page_table_invocation pti) (performPageTableInvocation pti') proof (prove)
goal (1 subgoal):
 1. page_table_invocation_map pti pti' \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableMap x11 x12 x13 x14\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od)
 2. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) (do y <- set_cap x11 (a, b);
y <- store_pde x14 x13;
do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))
od) (do y <- updateCap (cte_map (a, b)) cap';
y <- storePDE x14 pde';
doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14))
od)
 2. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (4 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> corres dc (?Q11 x11 a b x13 x14 cap' pde') (?Q'11 x11 a b x13 x14 cap' pde') (do y <- set_cap x11 (a, b);
y <- store_pde x14 x13;
do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))
od) (do y <- updateCap (cte_map (a, b)) cap';
y <- storePDE x14 pde';
doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14))
od)
 2. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> ?Q11 x11 a b x13 x14 cap' pde' s
 3. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> ?Q'11 x11 a b x13 x14 cap' pde' s
 4. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (7 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> cap_relation x11 cap'
 2. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 x11 a b x13 x14 cap' pde' y) (?R'15 x11 a b x13 x14 cap' pde' ya) (do y <- store_pde x14 x13;
do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))
od) (do y <- storePDE x14 pde';
doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14))
od)
 3. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>?R15 x11 a b x13 x14 cap' pde'\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>?R'15 x11 a b x13 x14 cap' pde'\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 6. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 7. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (6 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 x11 a b x13 x14 cap' pde' y) (?R'15 x11 a b x13 x14 cap' pde' ya) (do y <- store_pde x14 x13;
do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))
od) (do y <- storePDE x14 pde';
doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14))
od)
 2. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>?R15 x11 a b x13 x14 cap' pde'\<rbrace>
 3. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>?R'15 x11 a b x13 x14 cap' pde'\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 5. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 6. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (9 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> corres (?r'21 x11 a b x13 x14 cap' pde' y ya) (?P22 x11 a b x13 x14 cap' pde' y) (?P'24 x11 a b x13 x14 cap' pde' ya) (store_pde x14 x13) (storePDE x14 pde')
 2. \<And>x11 a b x13 x14 cap' pde' y ya yb yc. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya; ?r'21 x11 a b x13 x14 cap' pde' y ya yb yc\<rbrakk> \<Longrightarrow> corres dc (?R21 x11 a b x13 x14 cap' pde' y ya yb) (?R'21 x11 a b x13 x14 cap' pde' y ya yc) (do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))) (doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14)))
 3. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 x11 a b x13 x14 cap' pde' y\<rbrace> store_pde x14 x13 \<lbrace>?R21 x11 a b x13 x14 cap' pde' y ya\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace> storePDE x14 pde' \<lbrace>?R'21 x11 a b x13 x14 cap' pde' y ya\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. ?P22 x11 a b x13 x14 cap' pde' y and ?Q23 x11 a b x13 x14 cap' pde' y\<rbrace>
 6. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>\<lambda>ya. ?P'24 x11 a b x13 x14 cap' pde' ya and ?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace>
 7. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 8. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 9. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (9 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> pde_relation_aligned (x14 >> 2) x13 pde'
 2. \<And>x11 a b x13 x14 cap' pde' y ya yb yc. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres dc (?R21 x11 a b x13 x14 cap' pde' y ya yb) (?R'21 x11 a b x13 x14 cap' pde' y ya yc) (do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))) (doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14)))
 3. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 x11 a b x13 x14 cap' pde' y\<rbrace> store_pde x14 x13 \<lbrace>?R21 x11 a b x13 x14 cap' pde' y ya\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace> storePDE x14 pde' \<lbrace>?R'21 x11 a b x13 x14 cap' pde' y ya\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. pde_at x14 and pspace_aligned and valid_etcbs and ?Q23 x11 a b x13 x14 cap' pde' y\<rbrace>
 6. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace>
 7. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 8. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 9. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (8 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya yb yc. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres dc (?R21 x11 a b x13 x14 cap' pde' y ya yb) (?R'21 x11 a b x13 x14 cap' pde' y ya yc) (do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))) (doMachineOp (cleanByVA_PoU x14 (addrFromPPtr x14)))
 2. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 x11 a b x13 x14 cap' pde' y\<rbrace> store_pde x14 x13 \<lbrace>?R21 x11 a b x13 x14 cap' pde' y ya\<rbrace>
 3. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace> storePDE x14 pde' \<lbrace>?R'21 x11 a b x13 x14 cap' pde' y ya\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. pde_at x14 and pspace_aligned and valid_etcbs and ?Q23 x11 a b x13 x14 cap' pde' y\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace>
 6. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 7. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 8. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (8 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya yb yc. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (cleanByVA_PoU x14 (addrFromPPtr x14)) (cleanByVA_PoU x14 (addrFromPPtr x14))
 2. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 x11 a b x13 x14 cap' pde' y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>yb _. True\<rbrace>
 3. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace> storePDE x14 pde' \<lbrace>\<lambda>yc _. True\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. pde_at x14 and pspace_aligned and valid_etcbs and ?Q23 x11 a b x13 x14 cap' pde' y\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace>
 6. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 7. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 8. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (8 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya yb yc. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya; dc yb yc; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (cleanByVA_PoU x14 (addrFromPPtr x14))
 2. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 x11 a b x13 x14 cap' pde' y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>yb _. True\<rbrace>
 3. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace> storePDE x14 pde' \<lbrace>\<lambda>yc _. True\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. pde_at x14 and pspace_aligned and valid_etcbs and ?Q23 x11 a b x13 x14 cap' pde' y\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace>
 6. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 7. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 8. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (7 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 x11 a b x13 x14 cap' pde' y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>yb _. True\<rbrace>
 2. \<And>x11 a b x13 x14 cap' pde' y ya. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace> storePDE x14 pde' \<lbrace>\<lambda>yc _. True\<rbrace>
 3. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 x11 a b x13 x14 cap' pde'\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. pde_at x14 and pspace_aligned and valid_etcbs and ?Q23 x11 a b x13 x14 cap' pde' y\<rbrace>
 4. \<And>x11 a b x13 x14 cap' pde'. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 x11 a b x13 x14 cap' pde'\<rbrace> updateCap (cte_map (a, b)) cap' \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'25 x11 a b x13 x14 cap' pde' ya\<rbrace>
 5. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q15 x11 a b x13 x14 cap' pde') s
 6. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'15 x11 a b x13 x14 cap' pde') s
 7. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs and valid_etcbs and valid_pti (ARM_A.PageTableMap x11 (a, b) x13 x14)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap x11 \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and (\<lambda>s. pde_at x14 s \<and> pspace_aligned s \<and> valid_etcbs s \<and> True)) s
 2. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True)) s
 3. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' s cap p' ref y ao. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); invs s; valid_etcbs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_cap x11; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_master_cap x11 = cap_master_cap cap; cap_asid cap = None; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p'; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_ep_cap cap \<and> \<not> is_ntfn_cap cap \<and> pspace_aligned s
 2. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True)) s
 3. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (3 subgoals):
 1. \<And>a b x13 x14 pde' s ref y ao p asid data. \<lbrakk>pti = ARM_A.PageTableMap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b) x13 x14; pti' = ARM_H.PageTableMap (capability.ArchObjectCap (arch_capability.PageTableCap p asid)) (cte_map (a, b)) pde' x14; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); invs s; valid_etcbs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> cap.ArchObjectCap (arch_cap.PageTableCap p asid); empty_pde_at x14 s; caps_of_state s (a, b) = Some (cap.ArchObjectCap (arch_cap.PageTableCap p data)); cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) = Some y; vs_cap_ref (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid (cap.ArchObjectCap (arch_cap.PageTableCap p data)) = None; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> pspace_aligned s
 2. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True)) s
 3. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' s. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); (invs' and valid_pti' (ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14)) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True)) s
 2. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14 cap' pde' s cte. \<lbrakk>pti = ARM_A.PageTableMap x11 (a, b) x13 x14; pti' = ARM_H.PageTableMap cap' (cte_map (a, b)) pde' x14; cap_relation x11 cap'; pde_relation' x13 pde'; is_aligned (x14 >> 2) (case pde' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); invs' s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x14 s; ctes_of s (cte_map (a, b)) = Some cte; is_arch_update' cap' cte; valid_cap' cap' s; valid_pde' pde' s; valid_pde_mapping' (x14 && mask pdBits) pde'; vs_entry_align (KOArch (KOPDE pde')) = 0\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s
 2. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>page_table_invocation_map pti pti'; pti = ARM_A.PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti pti) (invs' and valid_pti' pti') (case pti of ARM_A.PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (cap.ArchObjectCap $ update_map_data cap None) ct_slot
od | ARM_A.PageTableUnmap (cap.ArchObjectCap _) ct_slot \<Rightarrow> fail | ARM_A.PageTableUnmap _ ct_slot \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x21 a b. \<lbrakk>page_table_invocation_map (ARM_A.PageTableUnmap x21 (a, b)) pti'; pti = ARM_A.PageTableUnmap x21 (a, b)\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap x21 (a, b))) (invs' and valid_pti' pti') (case x21 of cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address) \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap (a, b);
set_cap (cap.ArchObjectCap $ update_map_data cap None) (a, b)
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>page_table_invocation_map (ARM_A.PageTableUnmap cap (a, b)) pti'; pti = ARM_A.PageTableUnmap cap (a, b)\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap cap (a, b))) (invs' and valid_pti' pti') (case cap of cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address) \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap (a, b);
set_cap (cap.ArchObjectCap $ update_map_data cap None) (a, b)
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case pti' of ARM_H.PageTableUnmap cap ctSlot \<Rightarrow> do case capPTMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmapPageTable asid vaddr (capPTBasePtr cap);
ptr <- return (capPTBasePtr cap);
slots <- return [ptr , ptr + HaskellLib_H.bit pteBits .e. ptr + HaskellLib_H.bit ptBits - 1];
mapM_x (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ ptr) (VPtr $ fromPPtr $ ptr + HaskellLib_H.bit ptBits - 1) (addrFromPPtr ptr)
od;
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capPTMappedAddress_update (\<lambda>_. Nothing) cap)
od | ARM_H.PageTableMap cap ctSlot pde pdSlot \<Rightarrow> do updateCap ctSlot cap;
storePDE pdSlot pde;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr $ pdSlot) (addrFromPPtr pdSlot)
od) proof (prove)
goal (1 subgoal):
 1. \<And>cap a b cap'. \<lbrakk>pti = ARM_A.PageTableUnmap cap (a, b); cap_relation cap (capability.ArchObjectCap cap'); pti' = ARM_H.PageTableUnmap cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap cap (a, b))) (invs' and valid_pti' (ARM_H.PageTableUnmap cap' (cte_map (a, b)))) (case cap of cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address) \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap (a, b);
set_cap (cap.ArchObjectCap $ update_map_data cap None) (a, b)
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (do y <- case capPTMappedAddress cap' of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr cap');
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr cap' , capPTBasePtr cap' + 2 ^ pteBits .e. capPTBasePtr cap' + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr cap') (capPTBasePtr cap' + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr cap')))
od;
cap <- liftM capCap (getSlotCap (cte_map (a, b)));
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od) proof (prove)
goal (2 subgoals):
 1. \<And>cap a b cap' s s'. \<lbrakk>pti = ARM_A.PageTableUnmap cap (a, b); cap_relation cap (capability.ArchObjectCap cap'); pti' = ARM_H.PageTableUnmap cap' (cte_map (a, b)); (s, s') \<in> state_relation; (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap cap (a, b))) s; (invs' and valid_pti' (ARM_H.PageTableUnmap cap' (cte_map (a, b)))) s'\<rbrakk> \<Longrightarrow> is_pt_cap cap
 2. \<And>cap a b cap'. \<lbrakk>pti = ARM_A.PageTableUnmap cap (a, b); cap_relation cap (capability.ArchObjectCap cap'); pti' = ARM_H.PageTableUnmap cap' (cte_map (a, b)); is_pt_cap cap\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap cap (a, b))) (invs' and valid_pti' (ARM_H.PageTableUnmap cap' (cte_map (a, b)))) (case cap of cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address) \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap (a, b);
set_cap (cap.ArchObjectCap $ update_map_data cap None) (a, b)
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (do y <- case capPTMappedAddress cap' of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr cap');
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr cap' , capPTBasePtr cap' + 2 ^ pteBits .e. capPTBasePtr cap' + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr cap') (capPTBasePtr cap' + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr cap')))
od;
cap <- liftM capCap (getSlotCap (cte_map (a, b)));
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od) proof (prove)
goal (1 subgoal):
 1. \<And>cap a b cap'. \<lbrakk>pti = ARM_A.PageTableUnmap cap (a, b); cap_relation cap (capability.ArchObjectCap cap'); pti' = ARM_H.PageTableUnmap cap' (cte_map (a, b)); is_pt_cap cap\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap cap (a, b))) (invs' and valid_pti' (ARM_H.PageTableUnmap cap' (cte_map (a, b)))) (case cap of cap.ArchObjectCap (arch_cap.PageTableCap p mapped_address) \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte ARM_A.InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap (a, b);
set_cap (cap.ArchObjectCap $ update_map_data cap None) (a, b)
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (do y <- case capPTMappedAddress cap' of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr cap');
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr cap' , capPTBasePtr cap' + 2 ^ pteBits .e. capPTBasePtr cap' + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr cap') (capPTBasePtr cap' + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr cap')))
od;
cap <- liftM capCap (getSlotCap (cte_map (a, b)));
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) (do y <- case asid of None \<Rightarrow> return () | Some x2 \<Rightarrow> do y <- unmap_page_table (fst x2) (snd x2) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od;
cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do y <- case asid of None \<Rightarrow> return () | Some x2 \<Rightarrow> do y <- unmapPageTable (fst x2) (snd x2) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od;
cap <- liftM capCap (getSlotCap (cte_map (a, b)));
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) (do y <- if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return ();
cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do y <- if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return ();
cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od) proof (prove)
goal (3 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?Q146 a b p asid) (?Q'146 a b p asid) (do y <- if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return ();
cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do y <- if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return ();
cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 2. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ?Q146 a b p asid s
 3. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ?Q'146 a b p asid s proof (prove)
goal (6 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?P150 a b p asid) (?P'150 a b p asid) (if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return ()) (if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return ())
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
 5. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> (?P150 a b p asid and ?Q150 a b p asid) s
 6. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> (?P'150 a b p asid and ?Q'150 a b p asid) s proof (prove)
goal (7 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?P155 a b p asid) (?P'155 a b p asid) (do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od) (do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od)
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
 6. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then ?P155 a b p asid else (\<lambda>_. True)) and ?Q150 a b p asid) s
 7. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then ?P'155 a b p asid else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (9 subgoals):
 1. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R161 a b p asid y) (?R'161 a b p asid ya) (do y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od) (do y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od)
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q161 a b p asid\<rbrace> unmap_page_table (fst (the asid)) (snd (the asid)) p \<lbrace>?R161 a b p asid\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'161 a b p asid\<rbrace> unmapPageTable (fst (the asid)) (snd (the asid)) p \<lbrace>?R'161 a b p asid\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 6. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 7. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
 8. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and ?Q161 a b p asid else (\<lambda>_. True)) and ?Q150 a b p asid) s
 9. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and ?Q'161 a b p asid else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (12 subgoals):
 1. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?P167 a b p asid y) (?P'169 a b p asid ya) (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1])
 2. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R166 a b p asid y ya) (?R'166 a b p asid y ya) (do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))) (doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p)))
 3. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q168 a b p asid y\<rbrace> mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. ?R166 a b p asid y ya\<rbrace>
 4. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'170 a b p asid ya\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. ?R'166 a b p asid y ya\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q161 a b p asid\<rbrace> unmap_page_table (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>y. ?P167 a b p asid y and ?Q168 a b p asid y\<rbrace>
 6. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'161 a b p asid\<rbrace> unmapPageTable (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>ya. ?P'169 a b p asid ya and ?Q'170 a b p asid ya\<rbrace>
 7. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 8. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 9. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 10. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?P167 a b p asid ()) (?P'169 a b p asid ()) (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1])
 2. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R166 a b p asid y ya) (?R'166 a b p asid y ya) (do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))) (doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p)))
 3. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q168 a b p asid y\<rbrace> mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. ?R166 a b p asid y ya\<rbrace>
 4. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'170 a b p asid ya\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. ?R'166 a b p asid y ya\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q161 a b p asid\<rbrace> unmap_page_table (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>y. ?P167 a b p asid y and ?Q168 a b p asid y\<rbrace>
 6. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'161 a b p asid\<rbrace> unmapPageTable (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>ya. ?P'169 a b p asid ya and ?Q'170 a b p asid ya\<rbrace>
 7. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 8. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 9. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 10. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R166 a b p asid y ya) (?R'166 a b p asid y ya) (do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))) (doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p)))
 2. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q168 a b p asid y\<rbrace> mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. ?R166 a b p asid y ya\<rbrace>
 3. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'170 a b p asid ya\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. ?R'166 a b p asid y ya\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q161 a b p asid\<rbrace> unmap_page_table (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>y. pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs and ?Q168 a b p asid y\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'161 a b p asid\<rbrace> unmapPageTable (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'170 a b p asid ya\<rbrace>
 6. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 7. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 8. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 9. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
 10. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and ?Q161 a b p asid else (\<lambda>_. True)) and ?Q150 a b p asid) s
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p) = cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p)
 2. \<And>a b p asid y ya rv. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> dc rv rv
 3. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
 4. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q168 a b p asid y\<rbrace> mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>a b p asid y ya. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'170 a b p asid ya\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1] \<lbrace>\<lambda>x _. True\<rbrace>
 6. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q161 a b p asid\<rbrace> unmap_page_table (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>y. pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs and ?Q168 a b p asid y\<rbrace>
 7. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'161 a b p asid\<rbrace> unmapPageTable (fst (the asid)) (snd (the asid)) p \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and ?Q'170 a b p asid ya\<rbrace>
 8. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 9. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 10. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
A total of 13 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (cap.ArchObjectCap (update_map_data cap None)) (a, b)
od) (do cap <- liftM capCap (do cte <- getCTE (cte_map (a, b));
return (cteCap cte)
od);
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od)
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
 4. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 5. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (5 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?R150 a b p asid) (?R'150 a b p asid) (do x <- get_cap (a, b);
set_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) (a, b)
od) (do cte <- getCTE (cte_map (a, b));
updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte))))
od)
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R150 a b p asid\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. ?R'150 a b p asid\<rbrace>
 4. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 5. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (7 subgoals):
 1. \<And>a b p asid x cte. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); cap_relation x (cteCap cte)\<rbrakk> \<Longrightarrow> corres dc (?R219 a b p asid x) (?R'219 a b p asid cte) (set_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) (a, b)) (updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))))
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q219 a b p asid\<rbrace> get_cap (a, b) \<lbrace>?R219 a b p asid\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'219 a b p asid\<rbrace> getCTE (cte_map (a, b)) \<lbrace>?R'219 a b p asid\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) (a, b) and ?Q219 a b p asid\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and ?Q'219 a b p asid\<rbrace>
 6. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 7. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (7 subgoals):
 1. \<And>a b p asid x cte. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); cap_relation x (cteCap cte); is_pt_cap x\<rbrakk> \<Longrightarrow> corres dc (?P225 a b p asid x) (?R'219 a b p asid cte) (set_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) (a, b)) (updateCap (cte_map (a, b)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))))
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q219 a b p asid\<rbrace> get_cap (a, b) \<lbrace>\<lambda>x. ?P225 a b p asid x and (\<lambda>s. is_pt_cap x)\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'219 a b p asid\<rbrace> getCTE (cte_map (a, b)) \<lbrace>?R'219 a b p asid\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) (a, b) and ?Q219 a b p asid\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and ?Q'219 a b p asid\<rbrace>
 6. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 7. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (7 subgoals):
 1. \<And>a b p asid x cte. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); cap_relation x (cteCap cte); is_pt_cap x\<rbrakk> \<Longrightarrow> cap_relation (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte))))
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q219 a b p asid\<rbrace> get_cap (a, b) \<lbrace>\<lambda>x. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and (\<lambda>s. is_pt_cap x)\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'219 a b p asid\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>cte. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b))\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) (a, b) and ?Q219 a b p asid\<rbrace>
 5. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and ?Q'219 a b p asid\<rbrace>
 6. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 7. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (6 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q219 a b p asid\<rbrace> get_cap (a, b) \<lbrace>\<lambda>x. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and (\<lambda>s. is_pt_cap x)\<rbrace>
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'219 a b p asid\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>cte. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b))\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) (a, b) and ?Q219 a b p asid\<rbrace>
 4. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and ?Q'219 a b p asid\<rbrace>
 5. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 6. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (5 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'219 a b p asid\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>cte. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b))\<rbrace>
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) (a, b) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (a, b) s \<longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and (\<lambda>s. is_pt_cap cap)) s)\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and ?Q'219 a b p asid\<rbrace>
 4. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 5. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (4 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) (a, b) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (a, b) s \<longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and (\<lambda>s. is_pt_cap cap)) s)\<rbrace>
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)))\<rbrace>
 3. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 4. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (4 subgoals):
 1. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x xa. (\<exists>cap. caps_of_state xa (a, b) = Some cap) \<and> (\<forall>cap. caps_of_state xa (a, b) = Some cap \<longrightarrow> valid_objs xa \<and> pspace_aligned xa \<and> pspace_distinct xa \<and> cap_master_cap cap = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_ep_cap cap \<and> \<not> is_ntfn_cap cap \<and> is_pt_cap cap)\<rbrace>
 2. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)))\<rbrace>
 3. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and ?Q150 a b p asid) s
 4. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (5 subgoals):
 1. \<And>a b p asid x. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q242 a b p asid x\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>_ c. (\<exists>cap. x (a, b) = Some cap) \<and> (\<forall>cap. x (a, b) = Some cap \<longrightarrow> valid_objs c \<and> pspace_aligned c \<and> pspace_distinct c \<and> cap_master_cap cap = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_ep_cap cap \<and> \<not> is_ntfn_cap cap \<and> is_pt_cap cap)\<rbrace>
 2. \<And>a b p asid P. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. P (caps_of_state x)\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmap_page_table (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>_ x. P (caps_of_state x)\<rbrace>
 3. \<And>a b p asid. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'150 a b p asid\<rbrace> if \<exists>a b. asid = Some (a, b) then do y <- unmapPageTable (fst (the asid)) (snd (the asid)) p;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 2 ^ pteBits .e. p + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU p (p + 2 ^ ptBits - 1) (addrFromPPtr p))
od else return () \<lbrace>\<lambda>x. pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)))\<rbrace>
 4. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs and valid_etcbs and valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) and (\<lambda>s. ?Q242 a b p asid (caps_of_state s) s)) s
 5. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and ?Q'150 a b p asid) s proof (prove)
goal (2 subgoals):
 1. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); invs s \<and> valid_etcbs s \<and> valid_pti (ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b)) s\<rbrakk> \<Longrightarrow> (if \<exists>a b. asid = Some (a, b) then invs and valid_etcbs and typ_at (AArch APageTable) p and K (0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits) and (\<lambda>s. pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s \<and> True) else (\<lambda>_. True)) s \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (\<forall>x. caps_of_state s (a, b) = Some x \<longrightarrow> ((\<exists>a b. asid = Some (a, b)) \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> cap_master_cap x = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) \<and> \<not> is_reply_cap x \<and> \<not> is_master_reply_cap x \<and> \<not> is_ep_cap x \<and> \<not> is_ntfn_cap x \<and> is_pt_cap x) \<and> (asid = None \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> cap_master_cap x = cap_master_cap (cap.ArchObjectCap (update_map_data (the_arch_cap x) None)) \<and> \<not> is_reply_cap x \<and> \<not> is_master_reply_cap x \<and> \<not> is_ep_cap x \<and> \<not> is_ntfn_cap x \<and> is_pt_cap x))
 2. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and (\<lambda>s. ((\<exists>a b. asid = Some (a, b)) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) s) \<and> ((\<nexists>a b. asid = Some (a, b)) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b))) s))) s proof (prove)
goal (2 subgoals):
 1. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); invs s; valid_etcbs s; caps_of_state s (a, b) = Some (cap.ArchObjectCap (arch_cap.PageTableCap p asid)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageTableCap p asid); is_final_cap' (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) s\<rbrakk> \<Longrightarrow> ((\<exists>a b. asid = Some (a, b)) \<longrightarrow> typ_at (AArch APageTable) p s \<and> 0 < fst (the asid) \<and> is_aligned (snd (the asid)) 20 \<and> fst (the asid) \<le> mask local.asid_bits \<and> pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (asid = None \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s)) \<and> (asid = None \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s)
 2. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and (\<lambda>s. ((\<exists>a b. asid = Some (a, b)) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) s) \<and> ((\<nexists>a b. asid = Some (a, b)) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b))) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>a b p asid s. \<lbrakk>pti = ARM_A.PageTableUnmap (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) (a, b); pti' = ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)); (invs' and valid_pti' (ARM_H.PageTableUnmap (arch_capability.PageTableCap p asid) (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((if \<exists>a b. asid = Some (a, b) then valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True) else (\<lambda>_. True)) and (\<lambda>s. ((\<exists>a b. asid = Some (a, b)) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) s) \<and> ((\<nexists>a b. asid = Some (a, b)) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b))) s))) s proof (prove)
goal:
No subgoals!