theory Arch_DR

lemma invoke_page_directory_corres:
  "transform_page_dir_inv ip' = Some ip  \<Longrightarrow>
   dcorres dc \<top> (invs  and valid_pdpt_objs and valid_etcbs)
    (invoke_page_directory ip) (perform_page_directory_invocation ip')" apply (clarsimp simp:invoke_page_directory_def) apply (case_tac ip') apply (simp_all add:perform_page_invocation_def) apply (simp_all add: when_def  transform_page_dir_inv_def) apply safe apply (clarsimp) apply (rule corres_dummy_return_r) apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]]) apply wp apply (clarsimp simp: perform_page_directory_invocation_def) apply (wp) apply (rule dcorres_to_wp, rule dcorres_set_vm_root) apply (wp) apply (clarsimp cong: if_cong) apply (wp do_machine_op_wp, clarsimp, wp+) apply (clarsimp) apply (rule corres_dummy_return_r) apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]]) apply wp apply (clarsimp simp: perform_page_directory_invocation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_page_dir_inv ip' = Some ip \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_page_directory ip) (perform_page_directory_invocation ip') proof (prove)
goal (1 subgoal):
 1. transform_page_dir_inv ip' = Some ip \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case ip of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation ip') proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>transform_page_dir_inv ip' = Some ip; ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case ip of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation ip')
 2. \<lbrakk>transform_page_dir_inv ip' = Some ip; ip' = page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case ip of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation ip') proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>transform_page_dir_inv (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16) = Some ip; ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case ip of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16))
 2. \<lbrakk>transform_page_dir_inv page_directory_invocation.PageDirectoryNothing = Some ip; ip' = page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case ip of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11) = ip; ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case ip of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16))
 2. \<lbrakk>cdl_page_directory_invocation.PageDirectoryNothing = ip; ip' = page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (case cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11) of cdl_page_directory_invocation.PageDirectoryFlush flush \<Rightarrow> return () | _ \<Rightarrow> return ()) (perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16))
 2. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16))
 2. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16) >>= return)
 2. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs\<rbrace> perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> perform_page_directory_invocation (page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (x12 < x13) (do root_switched <- set_vm_root_for_flush x15 x16;
y <- do_machine_op (do_flush x11 x12 x13 x14);
when root_switched (gets cur_thread >>= set_vm_root)
od) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs root_switched y x. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B31 x11 x12 x13 x14 x15 x16 cs root_switched y x\<rbrace> set_vm_root x \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 cs root_switched y. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 x11 x12 x13 x14 x15 x16 cs root_switched y\<rbrace> gets cur_thread \<lbrace>?B31 x11 x12 x13 x14 x15 x16 cs root_switched y\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 cs root_switched. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs root_switched\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>y. if root_switched then ?Q30 x11 x12 x13 x14 x15 x16 cs root_switched y else (\<lambda>s. transform s = cs)\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 x11 x12 x13 x14 x15 x16 cs\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16 cs s. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); transform s = cs\<rbrakk> \<Longrightarrow> (if x12 < x13 then ?Q27 x11 x12 x13 x14 x15 x16 cs else (\<lambda>s. transform s = cs)) s
 6. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs root_switched y. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 x11 x12 x13 x14 x15 x16 cs root_switched y\<rbrace> gets cur_thread \<lbrace>\<lambda>x s. True \<and> transform s = cs\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 cs root_switched. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs root_switched\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>y. if root_switched then ?Q30 x11 x12 x13 x14 x15 x16 cs root_switched y else (\<lambda>s. transform s = cs)\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 x11 x12 x13 x14 x15 x16 cs\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16 cs s. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); transform s = cs\<rbrakk> \<Longrightarrow> (if x12 < x13 then ?Q27 x11 x12 x13 x14 x15 x16 cs else (\<lambda>s. transform s = cs)) s
 5. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs root_switched. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs root_switched\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>y. if root_switched then \<lambda>s. True \<and> transform s = cs else (\<lambda>s. transform s = cs)\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 x11 x12 x13 x14 x15 x16 cs\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 cs s. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); transform s = cs\<rbrakk> \<Longrightarrow> (if x12 < x13 then ?Q27 x11 x12 x13 x14 x15 x16 cs else (\<lambda>s. transform s = cs)) s
 4. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs root_switched. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs root_switched\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>y s. transform s = cs\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); x12 < x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 x11 x12 x13 x14 x15 x16 cs\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>?B28 x11 x12 x13 x14 x15 x16 cs\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 cs s. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); transform s = cs\<rbrakk> \<Longrightarrow> (if x12 < x13 then ?Q27 x11 x12 x13 x14 x15 x16 cs else (\<lambda>s. transform s = cs)) s
 4. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 cs s. \<lbrakk>ip' = page_directory_invocation.PageDirectoryFlush x11 x12 x13 x14 x15 x16; ip = cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map x11); transform s = cs\<rbrakk> \<Longrightarrow> (if x12 < x13 then \<lambda>ps. transform ps = cs else (\<lambda>s. transform s = cs)) s
 2. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (return ()) (perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing >>= return) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs\<rbrace> perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>ip' = page_directory_invocation.PageDirectoryNothing; ip = cdl_page_directory_invocation.PageDirectoryNothing\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> perform_page_directory_invocation page_directory_invocation.PageDirectoryNothing \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!