theory ArchDeterministic_AI

lemma perform_page_invocation_valid_list[wp]:
  "\<lbrace>valid_list\<rbrace> perform_page_invocation a \<lbrace>\<lambda>_.valid_list\<rbrace>" apply (simp add: perform_page_invocation_def) apply (cases a,simp_all) apply (wp mapM_x_wp' mapM_wp' crunch_wps | intro impI conjI allI | wpc | simp add: set_message_info_def set_mrs_def split: cap.splits arch_cap.splits option.splits sum.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> perform_page_invocation a \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> case a of PageMap asid cap ct_slot entries \<Rightarrow> do set_cap cap ct_slot;
case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od;
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 x14. a = PageMap x11 x12 x13 x14 \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- set_cap x12 x13;
y <- case x14 of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid x11 else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. \<And>x21 x22. a = PageUnmap x21 x22 \<Longrightarrow> \<lbrace>valid_list\<rbrace> case x21 of PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap x22;
set_cap (ArchObjectCap $ update_map_data cap None) x22;
return []
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. valid_list\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36. a = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!