kings-crown/FVELER_Isabelle huggingface dataset:
theory IsolatedThreadAction

lemma doMachineOp_isolatable:
  "thread_actions_isolatable idx (doMachineOp m)" apply (simp add: doMachineOp_def split_def) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               gets_isolatable thread_actions_isolatable_returns
               modify_isolatable select_f_isolatable) apply (simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (doMachineOp m) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do ms <- gets ksMachineState;
p <- select_f (m ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od) proof (prove)
goal (8 subgoals):
 1. \<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> ksMachineState (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = ksMachineState s
 2. \<And>x xa tsrs act s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksMachineState := snd xa, ksSchedulerAction := act\<rparr>) = ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)\<lparr>ksMachineState := snd xa\<rparr>
 3. \<And>x xa t. \<lbrace>?Q9 x xa t\<rbrace> modify (ksMachineState_update (\<lambda>_. snd xa)) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x xa t s. tcb_at' t s \<Longrightarrow> ?Q9 x xa t s
 5. \<And>x t. \<lbrace>?Q5 x t\<rbrace> select_f (m x) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 6. \<And>x t s. tcb_at' t s \<Longrightarrow> ?Q5 x t s
 7. \<And>t. \<lbrace>?Q1 t\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 8. \<And>t s. tcb_at' t s \<Longrightarrow> ?Q1 t s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma page_directory_at_partial_overwrite:
  "\<forall>x. tcb_at' (idx x) s \<Longrightarrow>
   page_directory_at' p (ksPSpace_update (partial_overwrite idx f) s)
      = page_directory_at' p s" by (simp add: page_directory_at'_def typ_at_to_obj_at_arches
                obj_at_partial_overwrite_id2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> page_directory_at' p (ksPSpace_update (partial_overwrite idx f) s) = page_directory_at' p s
theory IsolatedThreadAction

lemma transferCaps_simple:
  "transferCaps mi [] ep receiver rcvrBuf =
        do
          getReceiveSlots receiver rcvrBuf;
          return (mi\<lparr>msgExtraCaps := 0, msgCapsUnwrapped := 0\<rparr>)
        od" apply (cases mi) apply (clarsimp simp: transferCaps_def getThreadCSpaceRoot_def locateSlot_conv) apply (rule ext bind_apply_cong[OF refl])+ apply (simp add: upto_enum_def
            split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transferCaps mi [] ep receiver rcvrBuf = do getReceiveSlots receiver rcvrBuf;
return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))
od proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. mi = Types_H.message_info.MI x1 x2 x3 x4 \<Longrightarrow> transferCaps mi [] ep receiver rcvrBuf = do getReceiveSlots receiver rcvrBuf;
return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))
od proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. mi = Types_H.message_info.MI x1 x2 x3 x4 \<Longrightarrow> do destSlots <- getReceiveSlots receiver rcvrBuf;
case rcvrBuf of None \<Rightarrow> return (Types_H.message_info.MI x1 0 0 x4) | _ \<Rightarrow> return (Types_H.message_info.MI x1 0 0 x4)
od = do y <- getReceiveSlots receiver rcvrBuf;
return (Types_H.message_info.MI x1 0 0 x4)
od proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x rv st. \<lbrakk>mi = Types_H.message_info.MI x1 x2 x3 x4; (rv, st) \<in> fst (getReceiveSlots receiver rcvrBuf x)\<rbrakk> \<Longrightarrow> (case rcvrBuf of None \<Rightarrow> return (Types_H.message_info.MI x1 0 0 x4) | _ \<Rightarrow> return (Types_H.message_info.MI x1 0 0 x4)) st = return (Types_H.message_info.MI x1 0 0 x4) st proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma transferCaps_simple_rewrite:
  "monadic_rewrite True True ((\<lambda>_. caps = []) and \<top>)
   (transferCaps mi caps ep r rBuf)
   (return (mi \<lparr> msgExtraCaps := 0, msgCapsUnwrapped := 0 \<rparr>))" including no_pre supply empty_fail_getReceiveSlots[wp]  (* FIXME *)
   apply (rule monadic_rewrite_gen_asm) apply (simp add: transferCaps_simple) apply (monadic_rewrite_symb_exec_l_drop, rule monadic_rewrite_refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True ((\<lambda>_. caps = []) and (\<lambda>_. True)) (transferCaps mi caps ep r rBuf) (return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True ((\<lambda>_. caps = []) and (\<lambda>_. True)) (transferCaps mi caps ep r rBuf) (return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True ((\<lambda>_. caps = []) and (\<lambda>_. True)) (transferCaps mi caps ep r rBuf) (return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True ((\<lambda>_. caps = []) and (\<lambda>_. True)) (transferCaps mi caps ep r rBuf) (return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))) proof (prove)
goal (1 subgoal):
 1. caps = [] \<Longrightarrow> monadic_rewrite True True (\<lambda>_. True) (transferCaps mi caps ep r rBuf) (return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))) proof (prove)
goal (1 subgoal):
 1. caps = [] \<Longrightarrow> monadic_rewrite True True (\<lambda>_. True) (do y <- getReceiveSlots r rBuf;
return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))
od) (return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>caps = []; True\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma lookupExtraCaps_simple_rewrite:
  "msgExtraCaps mi = 0 \<Longrightarrow>
      (lookupExtraCaps thread rcvBuf mi = returnOk [])" by (cases mi, simp add: lookupExtraCaps_def getExtraCPtrs_def
                          liftE_bindE upto_enum_step_def mapM_Nil
                   split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msgExtraCaps mi = 0 \<Longrightarrow> lookupExtraCaps thread rcvBuf mi = returnOk []
theory IsolatedThreadAction

lemma lookupIPC_inv: "\<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>rv. P\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>rv. P\<rbrace>
theory IsolatedThreadAction

lemma empty_fail_isRunnable[intro!, wp, simp]:
  "empty_fail (isRunnable t)" by (simp add: isRunnable_def isStopped_def empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (isRunnable t)
theory IsolatedThreadAction

lemma oblivious_getObject_ksPSpace_default:
  "\<lbrakk> \<forall>s. ksPSpace (f s) = ksPSpace s;
      \<And>a b c ko. (loadObject a b c ko :: 'a kernel) \<equiv> loadObject_default a b c ko \<rbrakk> \<Longrightarrow>
   oblivious f (getObject p :: ('a :: pspace_storable) kernel)" apply (simp add: getObject_def split_def loadObject_default_def
                   projectKO_def2 alignCheck_assert magnitudeCheck_assert) apply (intro oblivious_bind, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. ksPSpace (f s) = ksPSpace s; \<And>a b c ko. loadObject a b c ko \<equiv> loadObject_default a b c ko\<rbrakk> \<Longrightarrow> oblivious f (getObject p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. ksPSpace (f s) = ksPSpace s; \<And>a b c ko. loadObject a b c ko \<equiv> do y <- assert (a = b);
val <- assert_opt (projectKO_opt ko);
y <- assert (is_aligned a (objBits val));
y <- assert (case c of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits val \<le> z - a);
return val
od\<rbrakk> \<Longrightarrow> oblivious f (do map <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p map));
y <- assert (p = fst pa);
val <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits val));
y <- assert (case snd (lookupAround2 p map) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits val \<le> z - p);
return val
od) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma oblivious_setObject_ksPSpace_tcb[simp]:
  "\<lbrakk> \<forall>s. ksPSpace (f s) = ksPSpace s;
     \<forall>s g. ksPSpace_update g (f s) = f (ksPSpace_update g s) \<rbrakk> \<Longrightarrow>
   oblivious f (setObject p (v :: tcb))" apply (simp add: setObject_def split_def updateObject_default_def
                   projectKO_def2 alignCheck_assert magnitudeCheck_assert) apply (intro oblivious_bind, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. ksPSpace (f s) = ksPSpace s; \<forall>s g. ksPSpace_update g (f s) = f (ksPSpace_update g s)\<rbrakk> \<Longrightarrow> oblivious f (setObject p v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. ksPSpace (f s) = ksPSpace s; \<forall>s g. ksPSpace_update g (f s) = f (ksPSpace_update g s)\<rbrakk> \<Longrightarrow> oblivious f (do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- assert_opt (projectKO_opt (snd pa));
y <- assert (is_aligned p (objBits v));
y <- assert (case snd (lookupAround2 p ps) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits v \<le> z - p);
return (KOTCB v)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma oblivious_doMachineOp[simp]:
  "\<lbrakk> \<forall>s. ksMachineState (f s) = ksMachineState s;
     \<forall>g s. ksMachineState_update g (f s) = f (ksMachineState_update g s) \<rbrakk>
      \<Longrightarrow> oblivious f (doMachineOp oper)" apply (simp add: doMachineOp_def split_def) apply (intro oblivious_bind, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. ksMachineState (f s) = ksMachineState s; \<forall>g s. ksMachineState_update g (f s) = f (ksMachineState_update g s)\<rbrakk> \<Longrightarrow> oblivious f (doMachineOp oper) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. ksMachineState (f s) = ksMachineState s; \<forall>g s. ksMachineState_update g (f s) = f (ksMachineState_update g s)\<rbrakk> \<Longrightarrow> oblivious f (do ms <- gets ksMachineState;
p <- select_f (oper ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma oblivious_setVMRoot_schact:
  "oblivious (ksSchedulerAction_update f) (setVMRoot t)" apply (simp add: setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv
                   getSlotCap_def getCTE_def armv_contextSwitch_def) by (safe intro!: oblivious_bind oblivious_bindE oblivious_catch
             | simp_all add: liftE_def getHWASID_def
                             findPDForASID_def liftME_def loadHWASID_def
                             findPDForASIDAssert_def checkPDAt_def
                             checkPDUniqueToASID_def
                             checkPDASIDMapMembership_def
                             findFreeHWASID_def invalidateASID_def
                             invalidateHWASIDEntry_def storeHWASID_def
                             checkPDNotInASIDMap_def armv_contextSwitch_def
                      split: capability.split arch_capability.split option.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious (ksSchedulerAction_update f) (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. oblivious (ksSchedulerAction_update f) (do cte <- getObject (t + 2 ^ cte_level_bits * tcbVTableSlot);
(case cteCap cte of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do y <- case cteCap cte of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
od)
theory IsolatedThreadAction

lemma oblivious_switchToThread_schact:
  "oblivious (ksSchedulerAction_update f) (ThreadDecls_H.switchToThread t)" apply (simp add: Thread_H.switchToThread_def switchToThread_def bind_assoc
                   getCurThread_def setCurThread_def threadGet_def liftM_def
                   threadSet_def tcbSchedEnqueue_def unless_when asUser_def
                   getQueue_def setQueue_def storeWordUser_def setRegister_def
                   pointerInUserData_def isRunnable_def isStopped_def
                   getThreadState_def tcbSchedDequeue_def bitmap_fun_defs) by (safe intro!: oblivious_bind
              | simp_all add: oblivious_setVMRoot_schact)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious (ksSchedulerAction_update f) (global.switchToThread t) proof (prove)
goal (1 subgoal):
 1. oblivious (ksSchedulerAction_update f) (do x <- setVMRoot t;
y <- doMachineOp ARM.clearExMonitor;
x <- getObject t;
y <- when (tcbQueued x) (do x <- getObject t;
xa <- getObject t;
queue <- gets (\<lambda>ks. ksReadyQueues ks (tcbDomain x, tcbPriority xa));
y <- modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((tcbDomain x, tcbPriority xa) := filter (\<lambda>x. x \<noteq> t) queue)\<rparr>);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (do xb <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (tcbDomain x, invertL1Index (prioToL1Index (tcbPriority xa))));
y <- modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap ks)((tcbDomain x, invertL1Index (prioToL1Index (tcbPriority xa))) := xb && ~~ 2 ^ unat (tcbPriority xa && mask wordRadix))\<rparr>);
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (tcbDomain x, invertL1Index (prioToL1Index (tcbPriority xa))));
when (l2 = 0) (do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks (tcbDomain x));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap ks)(tcbDomain x := l1 && ~~ 2 ^ prioToL1Index (tcbPriority xa))\<rparr>)
od)
od);
tcb <- getObject t;
setObject t (tcbQueued_update (\<lambda>_. False) tcb)
od);
modify (ksCurThread_update (\<lambda>_. t))
od)
theory IsolatedThreadAction

lemma empty_fail_getCurThread[intro!, wp, simp]:
  "empty_fail getCurThread" by (simp add: getCurThread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail getCurThread
theory IsolatedThreadAction

lemma tcbSchedEnqueue_tcbPriority[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>
     tcbSchedEnqueue t'
   \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp | simp cong: if_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> do queued <- threadGet tcbQueued t';
when (\<not> queued) (do tdom <- threadGet tcbDomain t';
prio <- threadGet tcbPriority t';
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t' # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t'
od)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma asUser_obj_at_unchangedT:
  assumes x: "\<forall>tcb con con'. con' \<in> fst (m con)
        \<longrightarrow> P (tcbArch_update (\<lambda>_. atcbContextSet (snd con') (tcbArch tcb)) tcb) = P tcb" shows
  "\<lbrace>obj_at' P t\<rbrace> asUser t' m \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_obj_at' threadGet_wp) apply (clarsimp simp: obj_at'_def projectKOs x cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> asUser t' m \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t';
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t';
return (fst p)
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> \<forall>tcb. ko_at' tcb t' s \<longrightarrow> (\<forall>x\<in>fst (m ((atcbContextGet \<circ> tcbArch) tcb)). obj_at' (\<lambda>obj. if t' = t then P (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj) else P obj) t s) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma bind_assoc:
  "do y \<leftarrow> do x \<leftarrow> m; f x od; g y od
     = do x \<leftarrow> m; y \<leftarrow> f x; g y od" by (rule bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= f >>= g = do x <- m;
f x >>= g
od
theory IsolatedThreadAction

lemma partial_overwrite_fun_upd2:
  "partial_overwrite idx tsrs (f (x := y))
     = (partial_overwrite idx tsrs f)
          (x := if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) y
                else y)" by (simp add: fun_eq_iff partial_overwrite_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partial_overwrite idx tsrs (f(x := y)) = (partial_overwrite idx tsrs f)(x := if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) y else y)
theory IsolatedThreadAction

lemma assert_isolatable:
  "thread_actions_isolatable idx (assert P)" by (simp add: assert_def thread_actions_isolatable_if
                thread_actions_isolatable_returns
                thread_actions_isolatable_fail)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (assert P)
theory IsolatedThreadAction

lemma thread_actions_isolatableD:
  "\<lbrakk> thread_actions_isolatable idx f; inj idx \<rbrakk>
     \<Longrightarrow> monadic_rewrite False True (\<lambda>s. (\<forall>x. tcb_at' (idx x) s))
            f (isolate_thread_actions idx f id id)" by (clarsimp simp: thread_actions_isolatable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>thread_actions_isolatable idx f; inj idx\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f id id)
theory IsolatedThreadAction

lemma switchToThread_rewrite:
  "monadic_rewrite True True
       (ct_in_state' (Not \<circ> runnable') and cur_tcb' and obj_at' (Not \<circ> tcbQueued) t)
       (switchToThread t)
       (do Arch.switchToThread t; setCurThread t od)" apply (simp add: switchToThread_def Thread_H.switchToThread_def) apply (monadic_rewrite_l tcbSchedDequeue_rewrite, simp) apply (rule monadic_rewrite_refl) apply (clarsimp simp: comp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (ct_in_state' (Not \<circ> runnable') and cur_tcb' and obj_at' (Not \<circ> tcbQueued) t) (global.switchToThread t) (do Arch.switchToThread t;
setCurThread t
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (ct_in_state' (Not \<circ> runnable') and cur_tcb' and obj_at' (Not \<circ> tcbQueued) t) (do y <- do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od;
y <- tcbSchedDequeue t;
setCurThread t
od) (do y <- do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od;
setCurThread t
od) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do y <- do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od;
setCurThread t
od) (do y <- do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od;
setCurThread t
od)
 2. \<And>s. (ct_in_state' (Not \<circ> runnable') and cur_tcb' and obj_at' (Not \<circ> tcbQueued) t) s \<Longrightarrow> (obj_at' (Not \<circ> tcbQueued) t and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ct_in_state' (Not \<circ> runnable') and cur_tcb' and obj_at' (Not \<circ> tcbQueued) t) s \<Longrightarrow> (obj_at' (Not \<circ> tcbQueued) t and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma switchToThread_isolatable:
  "thread_actions_isolatable idx (Arch.switchToThread t)" apply (simp add: switchToThread_def
                   storeWordUser_def stateAssert_def2) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               gets_isolatable setVMRoot_isolatable
               thread_actions_isolatable_if
               doMachineOp_isolatable
               threadGet_isolatable [OF all_tcbI]
               thread_actions_isolatable_returns
               thread_actions_isolatable_fail) apply (wp |
           simp add: pointerInUserData_def
                       typ_at_to_obj_at_arches
                       obj_at_partial_overwrite_id2
                       put_tcb_state_regs_tcb_def
                split: tcb_state_regs.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (Arch.switchToThread t) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od) proof (prove)
goal (2 subgoals):
 1. \<And>ta. \<lbrace>?Q1 ta\<rbrace> setVMRoot t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace>
 2. \<And>t s. tcb_at' t s \<Longrightarrow> ?Q1 t s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma setCurThread_isolatable:
  "thread_actions_isolatable idx (setCurThread t)" by (simp add: setCurThread_def modify_isolatable)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setCurThread t)