theory IsolatedThreadAction

lemma findPDForASID_isolatable:
  "thread_actions_isolatable idx (findPDForASID asid)" supply if_split[split del] apply (simp add: findPDForASID_def liftE_bindE liftME_def bindE_assoc
                   case_option_If2 assertE_def liftE_def checkPDAt_def
                   stateAssert_def2
             cong: if_cong) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_bindE[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_if thread_actions_isolatable_returns
               thread_actions_isolatable_fail
               gets_isolatable getObject_isolatable) apply (simp add: projectKO_opt_asidpool page_directory_at_partial_overwrite
           | wp getASID_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (findPDForASID asid) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (findPDForASID asid) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (doE y <- if 0 < asid then returnOk () else fail;
y <- if asid \<le> snd asidRange then returnOk () else fail;
asidTable <- do r <- gets (armKSASIDTable \<circ> ksArchState);
return (Inr r)
od;
x <- if \<exists>y. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some y then do r <- getObject (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid))));
return (Inr r)
od else throwError Fault_H.lookup_failure.InvalidRoot;
if \<exists>y. inv asidpool.ASIDPool x (asid && mask local.asid_low_bits) = Some y then doE y <- if the (inv asidpool.ASIDPool x (asid && mask local.asid_low_bits)) \<noteq> 0 then returnOk () else fail;
y <- do r <- do v <- gets (page_directory_at' (the (inv asidpool.ASIDPool x (asid && mask local.asid_low_bits))));
if v then return () else fail
od;
return (Inr ())
od;
returnOk (the (inv asidpool.ASIDPool x (asid && mask local.asid_low_bits)))
odE else throwError Fault_H.lookup_failure.InvalidRoot
odE) proof (prove)
goal (24 subgoals):
 1. \<And>x xa g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> (armKSASIDTable \<circ> ksArchState) (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = (armKSASIDTable \<circ> ksArchState) s
 2. \<And>x xa t. \<lbrace>?Q59 x xa t\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<And>x xa t s. tcb_at' t s \<Longrightarrow> ?Q59 x xa t s
 4. \<And>x xa xb a b c d. \<exists>y. xb (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some y \<Longrightarrow> loadObject a b c d = loadObject_default a b c d
 5. \<And>x xa xb tcb. \<exists>y. xb (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some y \<Longrightarrow> projectKO_opt (KOTCB tcb) = None
 6. \<And>x xa xb t. \<exists>y. xb (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some y \<Longrightarrow> \<lbrace>?Q53 x xa xb t\<rbrace> getObject (the (xb (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 7. \<And>x xa xb t s. \<lbrakk>\<exists>y. xb (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some y; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q53 x xa xb t s
 8. \<And>x xa xb xc xd g s. \<lbrakk>\<exists>y. inv asidpool.ASIDPool xc (asid && mask local.asid_low_bits) = Some y; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> page_directory_at' (the (inv asidpool.ASIDPool xc (asid && mask local.asid_low_bits))) (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = page_directory_at' (the (inv asidpool.ASIDPool xc (asid && mask local.asid_low_bits))) s
 9. \<And>x xa xb xc xd t. \<exists>y. inv asidpool.ASIDPool xc (asid && mask local.asid_low_bits) = Some y \<Longrightarrow> \<lbrace>?Q40 x xa xb xc xd t\<rbrace> gets (page_directory_at' (the (inv asidpool.ASIDPool xc (asid && mask local.asid_low_bits)))) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 10. \<And>x xa xb xc xd t s. \<lbrakk>\<exists>y. inv asidpool.ASIDPool xc (asid && mask local.asid_low_bits) = Some y; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q40 x xa xb xc xd t s
A total of 24 subgoals... proof (prove)
goal:
No subgoals!