theory IsolatedThreadAction

lemma setVMRoot_isolatable:
  "thread_actions_isolatable idx (setVMRoot t)" supply if_split[split del] apply (simp add: setVMRoot_def getThreadVSpaceRoot_def
                   locateSlot_conv getSlotCap_def
                   cap_case_isPageDirectoryCap if_bool_simps
                   whenE_def liftE_def
                   checkPDNotInASIDMap_def stateAssert_def2
                   checkPDASIDMapMembership_def armv_contextSwitch_def
             cong: if_cong) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_bindE[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_catch[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_if thread_actions_isolatable_returns
               thread_actions_isolatable_fail
               gets_isolatable getCTE_isolatable getHWASID_isolatable
               findPDForASID_isolatable doMachineOp_isolatable) apply (simp add: projectKO_opt_asidpool
           | wp getASID_wp typ_at_lifts [OF getHWASID_typ_at'])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do cte <- getCTE (t + 2 ^ cte_level_bits * tcbVTableSlot);
(if isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap cte)) = Some y) then doE pd' <- findPDForASID (the (capPDMappedASID (capCap (cteCap cte))));
y <- if capPDBasePtr (capCap (cteCap cte)) \<noteq> pd' then throwError Fault_H.lookup_failure.InvalidRoot else returnOk ();
do r <- do hwasid <- getHWASID (the (capPDMappedASID (capCap (cteCap cte))));
doMachineOp (armv_contextSwitch_HWASID (capPDBasePtr (capCap (cteCap cte))) hwasid)
od;
return (Inr ())
od
odE else throwError Fault_H.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do y <- if isArchObjectCap (cteCap cte) \<and> isPageDirectoryCap (capCap (cteCap cte)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap cte)) = Some y) then do v <- gets (\<lambda>s. capPDBasePtr (capCap (cteCap cte)) \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` UNIV));
if v then return () else fail
od else return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
od) proof (prove)
goal (20 subgoals):
 1. \<And>x xa xb t. isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y) \<Longrightarrow> \<lbrace>?Q58 x xa xb t\<rbrace> getHWASID (the (capPDMappedASID (capCap (cteCap x)))) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 2. \<And>x xa xb t s. \<lbrakk>isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y); tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q58 x xa xb t s
 3. \<And>x xa xb t. isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y) \<Longrightarrow> \<lbrace>?Q53 x xa xb t\<rbrace> do hwasid <- getHWASID (the (capPDMappedASID (capCap (cteCap x))));
doMachineOp (armv_contextSwitch_HWASID (capPDBasePtr (capCap (cteCap x))) hwasid)
od \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x xa xb t s. \<lbrakk>isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y); tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q53 x xa xb t s
 5. \<And>x xa t. isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y) \<Longrightarrow> \<lbrace>?Q49 x xa t\<rbrace> if capPDBasePtr (capCap (cteCap x)) \<noteq> xa then throwError Fault_H.lookup_failure.InvalidRoot else returnOk () \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 6. \<And>x xa t s. \<lbrakk>isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y); tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q49 x xa t s
 7. \<And>x t. isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y) \<Longrightarrow> \<lbrace>?Q45 x t\<rbrace> findPDForASID (the (capPDMappedASID (capCap (cteCap x)))) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 8. \<And>x t s. \<lbrakk>isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y); tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q45 x t s
 9. \<And>x xa g s. \<lbrakk>isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y); \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (capPDBasePtr (capCap (cteCap x)) \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s))) |` UNIV)) = (capPDBasePtr (capCap (cteCap x)) \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` UNIV))
 10. \<And>x xa t. isArchObjectCap (cteCap x) \<and> isPageDirectoryCap (capCap (cteCap x)) \<and> (\<exists>y. capPDMappedASID (capCap (cteCap x)) = Some y) \<Longrightarrow> \<lbrace>?Q35 x xa t\<rbrace> gets (\<lambda>s. capPDBasePtr (capCap (cteCap x)) \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` UNIV)) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
A total of 20 subgoals... proof (prove)
goal:
No subgoals!