kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_R

lemma unbindMaybeNotification_valid_objs'[wp]:
  "\<lbrace>valid_objs'\<rbrace>
     unbindMaybeNotification t
   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (rule hoare_pre) apply (wp threadSet_valid_objs' gbn_wp' set_ntfn_valid_objs' hoare_vcg_all_lift
            setNotification_valid_tcb' getNotification_wp
        | wpc | clarsimp simp: setBoundNotification_def unbindNotification_valid_objs'_helper)+ apply (clarsimp elim!: obj_atE' simp: projectKOs) apply (rule valid_objsE', assumption+) apply (clarsimp simp: valid_obj'_def unbindNotification_valid_objs'_helper') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do ntfn <- getNotification t;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>valid_objs' and ko_at' ntfn t\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q8 ntfn\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>ntfn s. (valid_objs' and ko_at' ntfn t) s \<Longrightarrow> ?Q8 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>valid_objs' s; ko_at' ntfn t s; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>valid_objs' s; ntfnBoundTCB ntfn = Some x; ksPSpace s t = Some (KONotification ntfn); is_aligned t (objBitsKO (KONotification ntfn)); ps_clear t (objBitsKO (KONotification ntfn)) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>valid_objs' s; ntfnBoundTCB ntfn = Some x; ksPSpace s t = Some (KONotification ntfn); is_aligned t (objBitsKO (KONotification ntfn)); ps_clear t (objBitsKO (KONotification ntfn)) s; valid_obj' (KONotification ntfn) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindMaybeNotification_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> unbindMaybeNotification t
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (rule hoare_pre) apply (wp sbn_sch_act' | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> do ntfn <- getNotification t;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do ntfn <- getNotification t;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>s. sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma valid_cong:
  "\<lbrakk> \<And>s. P s = P' s; \<And>s. P' s \<Longrightarrow> f s = f' s;
        \<And>rv s' s. \<lbrakk> (rv, s') \<in> fst (f' s); P' s \<rbrakk> \<Longrightarrow> Q rv s' = Q' rv s' \<rbrakk>
    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> = \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>" by (clarsimp simp add: valid_def, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = P' s; \<And>s. P' s \<Longrightarrow> f s = f' s; \<And>rv s' s. \<lbrakk>(rv, s') \<in> fst (f' s); P' s\<rbrakk> \<Longrightarrow> Q rv s' = Q' rv s'\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> = \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>
theory Finalise_R

lemma capDeleteOne_bound_tcb_at':
  "\<lbrace>bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap\<rbrace>
      cteDeleteOne callerCap \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>" apply (simp add: cteDeleteOne_def unless_def) apply (rule hoare_pre) apply (wp finaliseCapTrue_standin_bound_tcb_at' hoare_vcg_all_lift
            hoare_vcg_if_lift2 getCTE_cteCap_wp
        | wpc | simp | wp (once) hoare_drop_imp)+ apply (clarsimp simp:  cteCaps_of_def projectKOs isReplyCap_def cte_wp_at_ctes_of
                 split: option.splits) apply (case_tac "cteCap cte", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap\<rbrace> cteDeleteOne callerCap \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap\<rbrace> do cte <- getCTE callerCap;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder callerCap \<and> info = capability.NullCap);
emptySlot callerCap capability.NullCap
od)
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cte <- getCTE callerCap;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder callerCap \<and> info = capability.NullCap);
emptySlot callerCap capability.NullCap
od)
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 2. \<And>s. (bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. bound_tcb_at' P tptr s \<and> cte_wp_at' (isReplyCap \<circ> cteCap) callerCap s \<Longrightarrow> case cteCaps_of s callerCap of None \<Rightarrow> True | Some cap \<Rightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>tt b r. cap = capability.ReplyCap tt b r) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>bound_tcb_at' P tptr s; case cteCap cte of capability.ReplyCap v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False; ctes_of s callerCap = Some cte; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>tt b r. cteCap cte = capability.ReplyCap tt b r proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindNotification_bound_tcb_at':
  "\<lbrace>\<lambda>_. True\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. bound_tcb_at' ((=) None) t\<rbrace>" apply (simp add: unbindNotification_def) apply (wp setBoundNotification_bound_tcb gbn_wp' | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. bound_tcb_at' ((=) None) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>rv. bound_tcb_at' ((=) None) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindNotification_tcb_at'[wp]:
  "\<lbrace>tcb_at' t'\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" apply (simp add: unbindNotification_def) apply (wp gbn_wp' | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindMaybeNotification_tcb_at'[wp]:
  "\<lbrace>tcb_at' t'\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (wp gbn_wp' | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> do ntfn <- getNotification t;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od
od \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteDeleteOne_cte_wp_at_preserved:
  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
  shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>
           cteDeleteOne ptr
         \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>" apply (simp add: tree_cte_cteCap_eq[unfolded o_def]) apply (rule hoare_pre, wp cteDeleteOne_cteCaps_of) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2 \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) ptr s \<longrightarrow> (case ((cteCaps_of s)(ptr \<mapsto> capability.NullCap)) p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cancelIPC_cte_wp_at':
  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
  shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>
           cancelIPC t
         \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>" apply (simp add: tree_cte_cteCap_eq[unfolded o_def]) apply (rule hoare_pre, wp cancelIPC_cteCaps_of) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> cancelIPC t \<lbrace>\<lambda>rv s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2 \<Longrightarrow> (\<forall>pa. cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) pa s \<longrightarrow> (case ((cteCaps_of s)(pa \<mapsto> capability.NullCap)) p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2)) \<and> (case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma deleteASID_cte_wp_at'[wp]:
  "\<lbrace>cte_wp_at' P p\<rbrace> deleteASID param_a param_b \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>" apply (simp add: deleteASID_def invalidateHWASIDEntry_def invalidateASID_def
              cong: option.case_cong) apply (wp setObject_cte_wp_at'[where Q="\<top>"] getObject_inv
            loadObject_default_inv setVMRoot_cte_wp_at'
          | clarsimp simp: updateObject_default_def in_monad
                           projectKOs
          | rule equals0I
          | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p\<rbrace> deleteASID param_a param_b \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p\<rbrace> do asidTable <- gets (armKSASIDTable \<circ> ksArchState);
case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of param_a)) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) (getObject poolPtr);
when (pool (param_a && mask local.asid_low_bits) = Some param_b) (do y <- flushSpace param_a;
y <- invalidateASIDEntry param_a;
y <- setObject poolPtr (asidpool.ASIDPool (pool(param_a && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od
od \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma deletingIRQHandler_cte_preserved:
  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
  shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>
           deletingIRQHandler irq
         \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>" apply (simp add: deletingIRQHandler_def getSlotCap_def
                   getIRQSlot_def locateSlot_conv getInterruptState_def) apply (wp cteDeleteOne_cte_wp_at_preserved getCTE_wp'
              | simp add: x)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> deletingIRQHandler irq \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
cte <- getCTE (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq);
y <- assert (isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma setThreadState_st_tcb_at_simplish':
  "simple' st \<Longrightarrow>
   \<lbrace>st_tcb_at' (P or simple') t\<rbrace>
     setThreadState st t'
   \<lbrace>\<lambda>rv. st_tcb_at' (P or simple') t\<rbrace>" apply (wp sts_st_tcb_at'_cases) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple' st \<Longrightarrow> \<lbrace>st_tcb_at' (P or simple') t\<rbrace> setThreadState st t' \<lbrace>\<lambda>rv. st_tcb_at' (P or simple') t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>simple' st; st_tcb_at' (P or simple') t s\<rbrakk> \<Longrightarrow> (t' = t \<longrightarrow> (P or simple') st \<and> tcb_at' t s) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' (P or simple') t s) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteDeleteOne_st_tcb_at[wp]:
  assumes x[simp]: "\<And>st. simple' st \<longrightarrow> P st" shows
  "\<lbrace>st_tcb_at' P t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" apply (subgoal_tac "\<exists>Q. P = (Q or simple')") apply (clarsimp simp: pred_disj_def) apply (rule cteDeleteOne_st_tcb_at_simplish) apply (rule_tac x=P in exI) apply (auto intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<exists>Q. P = (Q or simple') \<Longrightarrow> \<lbrace>st_tcb_at' P t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 2. \<exists>Q. P = (Q or simple') proof (prove)
goal (2 subgoals):
 1. \<And>Q. P = (\<lambda>x. Q x \<or> simple' x) \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>x. Q x \<or> simple' x) t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. st_tcb_at' (\<lambda>x. Q x \<or> simple' x) t\<rbrace>
 2. \<exists>Q. P = (Q or simple') proof (prove)
goal (1 subgoal):
 1. \<exists>Q. P = (Q or simple') proof (prove)
goal (1 subgoal):
 1. P = (P or simple') proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma rescheduleRequired_sch_act_not[wp]:
  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_not t\<rbrace>" apply (simp add: rescheduleRequired_def setSchedulerAction_def) apply (wp hoare_post_taut | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_not t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
modify (ksSchedulerAction_update (\<lambda>_. ChooseNewThread))
od \<lbrace>\<lambda>rv. sch_act_not t\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cancelAllIPC_mapM_x_weak_sch_act:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   mapM_x (\<lambda>t. do
                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                 tcbSchedEnqueue t
               od) q
   \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (rule mapM_x_wp_inv) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread x \<longrightarrow> runnable' Structures_H.thread_state.Restart) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cancelAllIPC_mapM_x_valid_objs':
  "\<lbrace>valid_objs'\<rbrace>
   mapM_x (\<lambda>t. do
                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                 tcbSchedEnqueue t
               od) q
   \<lbrace>\<lambda>_. valid_objs'\<rbrace>" apply (wp mapM_x_wp' sts_valid_objs') apply (clarsimp simp: valid_tcb_state'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set q; valid_objs' s\<rbrakk> \<Longrightarrow> (valid_objs' and valid_tcb_state' Structures_H.thread_state.Restart) s
 2. \<And>s. valid_objs' s \<Longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cancelAllIPC_mapM_x_tcbDomain_obj_at':
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
   mapM_x (\<lambda>t. do
                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                 tcbSchedEnqueue t
               od) q
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (wp mapM_x_wp' tcbSchedEnqueue_not_st setThreadState_oa_queued | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cancelAllIPC_tcbDomain_obj_at':
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
     cancelAllIPC epptr
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (simp add: cancelAllIPC_def) apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
          rescheduleRequired_oa_queued' cancelAllIPC_mapM_x_tcbDomain_obj_at'
          getEndpoint_wp
     | wpc
     | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!