theory Finalise_DR

lemma dcorres_set_vm_root:
  "dcorres dc \<top> \<top> (return x) (set_vm_root rvd)" apply (clarsimp simp: set_vm_root_def) apply (rule dcorres_symb_exec_r)+ apply (clarsimp simp:catch_def throwError_def) 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 wpc apply (wp do_machine_op_wp | clarsimp)+ apply (rule_tac Q = "\<lambda>_ s. transform s = cs" in hoare_post_imp) apply simp apply (wpsimp wp: whenE_wp do_machine_op_wp [OF allI] hoare_drop_imps find_pd_for_asid_inv
                simp: arm_context_switch_def get_hw_asid_def load_hw_asid_def if_apply_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (set_vm_root rvd) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (do thread_root <- CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0));
(case thread_root of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q'1 rv) (return x) ((case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od))
 2. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>?Q'1\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q'1 rv) (return x) (do x <- case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot;
case x of Inl e \<Rightarrow> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od | Inr b \<Rightarrow> return b
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>?Q'1\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q'1 rv) (return x) (do x <- case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot;
case x of Inl e \<Rightarrow> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od | Inr b \<Rightarrow> return b
od >>= return)
 2. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>?Q'1\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrace>?Q'1 rv\<rbrace> do x <- case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot;
case x of Inl e \<Rightarrow> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do x <- case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot;
case x of Inl e \<Rightarrow> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>?Q'1\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv cs x. \<lbrace>?B21 rv cs x\<rbrace> case x of Inl e \<Rightarrow> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od | Inr b \<Rightarrow> return b \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>rv cs. \<lbrace>?Q20 rv cs\<rbrace> case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot \<lbrace>?B21 rv cs\<rbrace>
 3. \<And>rv cs s. transform s = cs \<Longrightarrow> ?Q20 rv cs s
 4. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r _. True\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv cs x x1. x = Inl x1 \<Longrightarrow> \<lbrace>?R32 rv cs x x1\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>rv cs x x2. x = Inr x2 \<Longrightarrow> \<lbrace>?R33 rv cs x x2\<rbrace> return x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv cs. \<lbrace>?Q20 rv cs\<rbrace> case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot \<lbrace>\<lambda>x s. (\<forall>xa. x = Inl xa \<longrightarrow> ?R32 rv cs x xa s) \<and> (\<forall>xa. x = Inr xa \<longrightarrow> ?R33 rv cs x xa s)\<rbrace>
 4. \<And>rv cs s. transform s = cs \<Longrightarrow> ?Q20 rv cs s
 5. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r _. True\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv cs. \<lbrace>?Q20 rv cs\<rbrace> case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot \<lbrace>\<lambda>x s. ((\<exists>xa. x = Inl xa) \<longrightarrow> transform s = cs) \<and> (x = Inr () \<longrightarrow> transform s = cs)\<rbrace>
 2. \<And>rv cs s. transform s = cs \<Longrightarrow> ?Q20 rv cs s
 3. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv cs rva s. transform s = cs \<Longrightarrow> ((\<exists>x. rva = Inl x) \<longrightarrow> transform s = cs) \<and> (rva = Inr () \<longrightarrow> transform s = cs)
 2. \<And>rv cs. \<lbrace>?Q20 rv cs\<rbrace> case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot \<lbrace>\<lambda>_ s. transform s = cs\<rbrace>
 3. \<And>rv cs s. transform s = cs \<Longrightarrow> ?Q20 rv cs s
 4. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r _. True\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv cs. \<lbrace>?Q20 rv cs\<rbrace> case rv of ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot \<lbrace>\<lambda>_ s. transform s = cs\<rbrace>
 2. \<And>rv cs s. transform s = cs \<Longrightarrow> ?Q20 rv cs s
 3. \<lbrace>\<lambda>_. True\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> CSpaceAcc_A.get_cap (rvd, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!