theory ArchArch_IF

lemma unmap_page_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs
                     and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace>
   unmap_page pgsz asid vptr pptr
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding unmap_page_def cleanCacheRange_PoU_def including no_pre apply (induct pgsz) prefer 4 apply (simp only: vmpage_size.simps) apply (wp mapM_swp_store_pde_globals_equiv dmo_cacheRangeOp_lift | simp add: cleanByVA_PoU_def)+ apply (rule hoare_drop_imps) apply (wp)+ apply (simp) apply (rule hoare_drop_imps) apply (wp)+ apply (rule hoare_pre) apply (rule_tac Q="\<lambda>x. globals_equiv st and
                             (\<lambda>sa. lookup_pd_slot x vptr && mask 6 = 0
                                   \<longrightarrow> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. xa + lookup_pd_slot x vptr
                                                                     && ~~ mask pd_bits
                                                                   \<noteq> arm_global_pd (arch_state sa)))"
                  and E="\<lambda>_. globals_equiv st" in hoare_post_impErr) apply (wp find_pd_for_asid_not_arm_global_pd_large_page) apply simp apply simp apply simp apply (wp store_pte_globals_equiv | simp add: cleanByVA_PoU_def)+ apply (wp hoare_drop_imps)+ apply (wp (once) lookup_pt_slot_inv) apply (wp (once) lookup_pt_slot_inv) apply (wp (once) lookup_pt_slot_inv) apply (wp (once) lookup_pt_slot_inv) apply (simp) apply (rule hoare_pre) apply wp apply (simp) apply (simp) apply (rule hoare_pre) apply ((wp dmo_cacheRangeOp_lift mapM_swp_store_pde_globals_equiv store_pde_globals_equiv
               lookup_pt_slot_inv mapM_swp_store_pte_globals_equiv hoare_drop_imps
            | simp add: cleanByVA_PoU_def)+)[2] apply (rule hoare_pre) apply (wp store_pde_globals_equiv | simp add: cleanByVA_PoU_def)+ apply (wp find_pd_for_asid_not_arm_global_pd hoare_drop_imps)+ apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> unmap_page pgsz asid vptr pptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case pgsz of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page pgsz pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case pgsz of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr pgsz (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page pgsz pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSuperSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSuperSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSuperSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSuperSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSuperSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x xa. \<lbrace>?P61 x xa\<rbrace> check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> globals_equiv st s\<rbrace>
 2. \<And>x xa. \<lbrace>?P'61 x xa\<rbrace> throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>xb s. (xa && mask 6 = 0 \<longrightarrow> True) \<and> (xa && mask 6 = 0 \<longrightarrow> True \<and> (globals_equiv st and (\<lambda>s. \<forall>x\<in>set (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]). x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) s)\<rbrace>, -
 3. \<And>x. \<lbrace>?B11 x\<rbrace> returnOk (lookup_pd_slot x vptr) \<lbrace>\<lambda>xa s. ?P61 x xa s \<and> ?P'61 x xa s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B11\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x xa. \<lbrace>?P61 x xa\<rbrace> check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>
 2. \<And>x xa. \<lbrace>?P'61 x xa\<rbrace> throw_on_false undefined $ check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>xb s. (xa && mask 6 = 0 \<longrightarrow> True) \<and> (xa && mask 6 = 0 \<longrightarrow> True \<and> (globals_equiv st and (\<lambda>s. \<forall>x\<in>set (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]). x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) s)\<rbrace>, -
 3. \<And>x. \<lbrace>?B11 x\<rbrace> returnOk (lookup_pd_slot x vptr) \<lbrace>\<lambda>xa s. ?P61 x xa s \<and> ?P'61 x xa s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B11\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrace>?P'61 x xa\<rbrace> check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>rv s. (rv \<longrightarrow> (xa && mask 6 = 0 \<longrightarrow> True) \<and> (xa && mask 6 = 0 \<longrightarrow> True \<and> (globals_equiv st and (\<lambda>s. \<forall>x\<in>set (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]). x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) s)) \<and> (\<not> rv \<longrightarrow> True)\<rbrace>
 2. \<And>x. \<lbrace>?B11 x\<rbrace> returnOk (lookup_pd_slot x vptr) \<lbrace>\<lambda>xa s. globals_equiv st s \<and> ?P'61 x xa s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B11\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrace>?P'61 x xa\<rbrace> check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>rv s. rv \<longrightarrow> xa && mask 6 = 0 \<longrightarrow> globals_equiv st s \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + xa && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
 2. \<And>x. \<lbrace>?B11 x\<rbrace> returnOk (lookup_pd_slot x vptr) \<lbrace>\<lambda>xa s. globals_equiv st s \<and> ?P'61 x xa s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B11\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrace>?P'61 x xa\<rbrace> check_mapping_pptr pptr ARMSuperSection (Inr xa) \<lbrace>\<lambda>rv s. xa && mask 6 = 0 \<longrightarrow> globals_equiv st s \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + xa && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
 2. \<And>x. \<lbrace>?B11 x\<rbrace> returnOk (lookup_pd_slot x vptr) \<lbrace>\<lambda>xa s. globals_equiv st s \<and> ?P'61 x xa s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B11\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x a. globals_equiv st a \<and> (lookup_pd_slot x vptr && mask 6 = 0 \<longrightarrow> globals_equiv st a \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. xa + lookup_pd_slot x vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state a)))\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q84\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x a. globals_equiv st a \<and> (lookup_pd_slot x vptr && mask 6 = 0 \<longrightarrow> globals_equiv st a \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. xa + lookup_pd_slot x vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state a)))\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 2. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> ?Q84 s
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrace>?Q84\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x. globals_equiv st and (\<lambda>sa. lookup_pd_slot x vptr && mask 6 = 0 \<longrightarrow> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. xa + lookup_pd_slot x vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state sa)))\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>rv s. (globals_equiv st and (\<lambda>sa. lookup_pd_slot rv vptr && mask 6 = 0 \<longrightarrow> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. xa + lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state sa)))) s \<Longrightarrow> globals_equiv st s \<and> (lookup_pd_slot rv vptr && mask 6 = 0 \<longrightarrow> globals_equiv st s \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)))
 3. \<And>e s. globals_equiv st s \<Longrightarrow> globals_equiv st s
 4. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> ?Q84 s
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv s. (globals_equiv st and (\<lambda>sa. lookup_pd_slot rv vptr && mask 6 = 0 \<longrightarrow> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. xa + lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state sa)))) s \<Longrightarrow> globals_equiv st s \<and> (lookup_pd_slot rv vptr && mask 6 = 0 \<longrightarrow> globals_equiv st s \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)))
 2. \<And>e s. globals_equiv st s \<Longrightarrow> globals_equiv st s
 3. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> globals_equiv st s \<and> globals_equiv st s \<and> (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state) s
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>e s. globals_equiv st s \<Longrightarrow> globals_equiv st s
 2. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> globals_equiv st s \<and> globals_equiv st s \<and> (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state) s
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> globals_equiv st s \<and> globals_equiv st s \<and> (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state) s
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSmallPage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSmallPage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSmallPage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrace>?B118 x xa\<rbrace> check_mapping_pptr pptr ARMSmallPage (Inl xa) \<lbrace>\<lambda>rv s. (rv \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> rv \<longrightarrow> globals_equiv st s)\<rbrace>
 2. \<And>x. \<lbrace>?B104 x\<rbrace> lookup_pt_slot x vptr \<lbrace>?B118 x\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B104\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?B104 x\<rbrace> lookup_pt_slot x vptr \<lbrace>\<lambda>xa s. globals_equiv st s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>?B104\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P'137 x\<rbrace> lookup_pt_slot x vptr \<lbrace>\<lambda>xa s. globals_equiv st s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrace>, -
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x s. globals_equiv st s \<and> ?P'137 x s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P'141 x\<rbrace> lookup_pt_slot x vptr \<lbrace>\<lambda>rv s. valid_arch_state s \<and> globals_equiv st s\<rbrace>, -
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x s. globals_equiv st s \<and> globals_equiv st s \<and> ?P'141 x s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P'145 x\<rbrace> lookup_pt_slot x vptr \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>, -
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x s. globals_equiv st s \<and> globals_equiv st s \<and> valid_arch_state s \<and> ?P'145 x s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x s. globals_equiv st s \<and> globals_equiv st s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>a. globals_equiv st a \<and> valid_arch_state a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_global_objs a \<and> valid_vs_lookup a \<and> valid_global_refs a\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x s. globals_equiv st s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q152\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>x s. globals_equiv st s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 2. \<And>s. globals_equiv st s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_global_refs s \<Longrightarrow> ?Q152 s
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. globals_equiv st s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_global_refs s \<Longrightarrow> globals_equiv st s \<and> globals_equiv st s \<and> valid_arch_state s \<and> globals_equiv st s
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMLargePage of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMLargePage (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMLargePage pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>a. globals_equiv st a \<and> valid_arch_state a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_global_objs a \<and> valid_vs_lookup a \<and> valid_global_refs a\<rbrace> doE pd <- find_pd_for_asid asid;
a <- doE p <- lookup_pt_slot pd vptr;
y <- throw_on_false undefined (check_mapping_pptr pptr ARMLargePage (Inl p));
liftE (do y <- assert (p && mask 6 = 0);
y <- mapM (swp store_pte InvalidPTE) (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
do_machine_op (cacheRangeOp cleanByVA_PoU (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) (last_byte_pte (last (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))) (addrFromPPtr (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))))
od)
odE;
liftE (flush_page ARMLargePage pd asid vptr)
odE <catch> (\<lambda>a. return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q165\<rbrace> doE pd <- find_pd_for_asid asid;
a <- doE p <- lookup_pt_slot pd vptr;
y <- throw_on_false undefined (check_mapping_pptr pptr ARMLargePage (Inl p));
liftE (do y <- assert (p && mask 6 = 0);
y <- mapM (swp store_pte InvalidPTE) (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
do_machine_op (cacheRangeOp cleanByVA_PoU (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) (last_byte_pte (last (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))) (addrFromPPtr (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))))
od)
odE;
liftE (flush_page ARMLargePage pd asid vptr)
odE <catch> (\<lambda>a. return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. globals_equiv st s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_global_refs s \<Longrightarrow> ?Q165 s
 3. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q220\<rbrace> doE pd <- find_pd_for_asid asid;
case ARMSection of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inl p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $ check_mapping_pptr pptr ARMSection (Inr p);
liftE $ do assert $ p && mask 6 = 0;
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots))
od
odE;
liftE $ flush_page ARMSection pd asid vptr
odE <catch> (K $ return ()) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> ?Q220 s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B230 x\<rbrace> check_mapping_pptr pptr ARMSection (Inr (lookup_pd_slot x vptr)) \<lbrace>\<lambda>rv s. (rv \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot x vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> (\<not> rv \<longrightarrow> globals_equiv st s)\<rbrace>
 2. \<lbrace>?Q220\<rbrace> find_pd_for_asid asid \<lbrace>?B230\<rbrace>, \<lbrace>\<lambda>x. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> ?Q220 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs) s \<Longrightarrow> globals_equiv st s \<and> globals_equiv st s \<and> (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state) s \<and> globals_equiv st s proof (prove)
goal:
No subgoals!