theory IsolatedThreadAction

lemma getHWASID_isolatable:
  "thread_actions_isolatable idx (getHWASID asid)" apply (simp add: getHWASID_def loadHWASID_def
                   findFreeHWASID_def
                   case_option_If2 findPDForASIDAssert_def
                   checkPDAt_def checkPDUniqueToASID_def
                   checkPDASIDMapMembership_def
                   stateAssert_def2 const_def assert_def
                   findFreeHWASID_def
                   invalidateASID_def
                   invalidateHWASIDEntry_def
                   storeHWASID_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 modify_isolatable
               findPDForASID_isolatable doMachineOp_isolatable) apply (wp hoare_drop_imps
            | simp add: page_directory_at_partial_overwrite)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (getHWASID asid) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do maybe_hw_asid <- do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- do pd <- findPDForASID asid <catch> (\<lambda>y. fail);
y <- if pd && mask pdBits = 0 then return () else fail;
y <- do v <- gets (page_directory_at' pd);
if v then return () else fail
od;
y <- do v <- gets (\<lambda>s. pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})));
if v then return () else fail
od;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- if if \<exists>a b. asidMap asid = Some (a, b) then case the (asidMap asid) of (x, xa) \<Rightarrow> pd = xa else True then return () else fail;
return pd
od;
return (if \<exists>a b. asidMap asid = Some (a, b) then case the (asidMap asid) of (hw_asid, x) \<Rightarrow> Some hw_asid else None)
od;
if \<exists>y. maybe_hw_asid = Some y then return (the maybe_hw_asid) else do new_hw_asid <- do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
if \<exists>y. find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) = Some y then return (the (find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]))) else do y <- do y <- do pd <- findPDForASID (the (hwASIDTable nextASID)) <catch> (\<lambda>y. fail);
y <- if pd && mask pdBits = 0 then return () else fail;
y <- do v <- gets (page_directory_at' pd);
if v then return () else fail
od;
y <- do v <- gets (\<lambda>s. pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (hwASIDTable nextASID)})));
if v then return () else fail
od;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- if if \<exists>a b. asidMap (the (hwASIDTable nextASID)) = Some (a, b) then case the (asidMap (the (hwASIDTable nextASID))) of (x, xa) \<Rightarrow> pd = xa else True then return () else fail;
return pd
od;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>)
od;
y <- doMachineOp (invalidateLocalTLB_ASID nextASID);
y <- do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(nextASID := None)) (ksArchState s)\<rparr>)
od;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od
od;
y <- do pd <- do pd <- findPDForASID asid <catch> (\<lambda>y. fail);
y <- if pd && mask pdBits = 0 then return () else fail;
y <- do v <- gets (page_directory_at' pd);
if v then return () else fail
od;
y <- do v <- gets (\<lambda>s. pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})));
if v then return () else fail
od;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- if if \<exists>a b. asidMap asid = Some (a, b) then case the (asidMap asid) of (x, xa) \<Rightarrow> pd = xa else True then return () else fail;
return pd
od;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid \<mapsto> (new_hw_asid, pd))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(new_hw_asid \<mapsto> asid)) (ksArchState s)\<rparr>)
od;
return new_hw_asid
od
od) proof (prove)
goal (111 subgoals):
 1. \<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> (armKSASIDMap \<circ> ksArchState) (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = (armKSASIDMap \<circ> ksArchState) s
 2. \<And>x t. \<lbrace>?Q264 x t\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<And>x t s. tcb_at' t s \<Longrightarrow> ?Q264 x t s
 4. \<And>x xa xb g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> page_directory_at' xa (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = page_directory_at' xa s
 5. \<And>x xa xb t. \<lbrace>?Q253 x xa xb t\<rbrace> gets (page_directory_at' xa) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 6. \<And>x xa xb t s. tcb_at' t s \<Longrightarrow> ?Q253 x xa xb t s
 7. \<And>x xa xb xc g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> (xa \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s))) |` (- {asid}))) = (xa \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})))
 8. \<And>x xa xb xc t. \<lbrace>?Q245 x xa xb xc t\<rbrace> gets (\<lambda>s. xa \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid}))) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 9. \<And>x xa xb xc t s. tcb_at' t s \<Longrightarrow> ?Q245 x xa xb xc t s
 10. \<And>x xa xb xc xd g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> (armKSASIDMap \<circ> ksArchState) (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = (armKSASIDMap \<circ> ksArchState) s
A total of 111 subgoals... proof (prove)
goal:
No subgoals!