kings-crown/FVELER_Isabelle huggingface dataset:
theory Interrupt_R

lemma resetTimer_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp resetTimer \<lbrace>\<lambda>_. invs'\<rbrace>" apply (wp dmo_invs' no_irq no_irq_resetTimer) apply clarsimp apply (drule_tac Q="%_ b. underlying_memory b p = underlying_memory m p"
                in use_valid) apply (simp add: resetTimer_def
                     machine_op_lift_def machine_rest_lift_def split_def) apply wp apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp resetTimer \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (resetTimer m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (resetTimer m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P13 s m b p\<rbrace> resetTimer \<lbrace>\<lambda>_ b. underlying_memory b p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P13 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P13 s m b p\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (ignore_failure resetTimer_impl mr);
modify (machine_state_rest_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ b. underlying_memory b p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P13 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (2 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (ignore_failure resetTimer_impl (machine_state_rest m)). underlying_memory (m\<lparr>machine_state_rest := snd x\<rparr>) p = underlying_memory m p
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma dmo_ackInterrupt[wp]:
"\<lbrace>invs'\<rbrace> doMachineOp (ackInterrupt irq) \<lbrace>\<lambda>y. invs'\<rbrace>" apply (wp dmo_invs' no_irq no_irq_ackInterrupt) apply safe apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
          in use_valid) apply ((clarsimp simp: ackInterrupt_def machine_op_lift_def
                           machine_rest_lift_def split_def | wp)+)[3] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (ackInterrupt irq) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (ackInterrupt irq m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (ackInterrupt irq m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P13 s m b p\<rbrace> ackInterrupt irq \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P13 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma syscall_corres:
  assumes corres:
    "corres (fr \<oplus> r_flt_rel) P P' m_flt m_flt'"
    "\<And>flt flt'. flt' = fault_map flt \<Longrightarrow>
        corres r (P_flt flt) (P'_flt flt') (h_flt flt) (h_flt' flt')"
    "\<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow>
        corres (ser \<oplus> r_err_rel rv rv')
               (P_no_flt rv) (P'_no_flt rv')
               (m_err rv) (m_err' rv')"
    "\<And>rv rv' err err'. \<lbrakk>r_flt_rel rv rv'; err' = syscall_error_map err \<rbrakk>
     \<Longrightarrow> corres r (P_err rv err)
            (P'_err rv' err') (h_err err) (h_err' err')"
    "\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk>
     \<Longrightarrow> corres (dc \<oplus> r)
           (P_no_err rvf rve) (P'_no_err rvf' rve')
           (m_fin rve) (m_fin' rve')"

  assumes wp:
    "\<And>rv.  \<lbrace>Q_no_flt rv\<rbrace>   m_err rv   \<lbrace>P_no_err rv\<rbrace>,  \<lbrace>P_err rv\<rbrace>"
    "\<And>rv'. \<lbrace>Q'_no_flt rv'\<rbrace> m_err' rv' \<lbrace>P'_no_err rv'\<rbrace>,\<lbrace>P'_err rv'\<rbrace>"
    "\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>"
    "\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>"

  shows "corres (dc \<oplus> r) (P and Q) (P' and Q')
           (Syscall_A.syscall m_flt  h_flt m_err h_err m_fin)
           (Syscall_H.syscall m_flt' h_flt' m_err' h_err' m_fin')" apply (simp add: Syscall_A.syscall_def Syscall_H.syscall_def liftE_bindE) apply (rule corres_split_bind_case_sum) apply (rule corres_split_bind_case_sum | rule corres | rule wp | simp add: liftE_bindE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> r) (P and Q) (P' and Q') (Syscall_A.syscall m_flt h_flt m_err h_err m_fin) (Syscall_H.syscall m_flt' h_flt' m_err' h_err' m_fin') proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> r) (P and Q) (P' and Q') (m_flt >>= case_sum (\<lambda>f. without_preemption $ h_flt f) (\<lambda>a. (without_preemption $ m_err a) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin)) (m_flt' >>= case_sum (\<lambda>f. withoutPreemption $ h_flt' f) (\<lambda>a. (withoutPreemption $ runExceptT $ m_err' a) >>=E case_sum (\<lambda>e. withoutPreemption $ h_err' e) m_fin')) proof (prove)
goal (5 subgoals):
 1. corres (?lr \<oplus> ?rr) P P' m_flt m_flt'
 2. \<And>rv rv'. ?lr rv rv' \<Longrightarrow> corres (dc \<oplus> r) (?R rv) (?R' rv') (without_preemption $ h_flt rv) (withoutPreemption $ h_flt' rv')
 3. \<And>rv rv'. ?rr rv rv' \<Longrightarrow> corres (dc \<oplus> r) (?S rv) (?S' rv') ((without_preemption $ m_err rv) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin) ((withoutPreemption $ runExceptT $ m_err' rv') >>=E case_sum (\<lambda>e. withoutPreemption $ h_err' e) m_fin')
 4. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>?R\<rbrace>
 5. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>?R'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma syscall_valid':
  assumes x:
             "\<And>ft. \<lbrace>P_flt ft\<rbrace> h_flt ft \<lbrace>Q\<rbrace>"
             "\<And>err. \<lbrace>P_err err\<rbrace> h_err err \<lbrace>Q\<rbrace>"
             "\<And>rv. \<lbrace>P_no_err rv\<rbrace> m_fin rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
             "\<And>rv. \<lbrace>P_no_flt rv\<rbrace> m_err rv \<lbrace>P_no_err\<rbrace>, \<lbrace>P_err\<rbrace>"
             "\<lbrace>P\<rbrace> m_flt \<lbrace>P_no_flt\<rbrace>, \<lbrace>P_flt\<rbrace>"
  shows "\<lbrace>P\<rbrace> Syscall_H.syscall m_flt h_flt m_err h_err m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" apply (simp add: Syscall_H.syscall_def liftE_bindE
             cong: sum.case_cong) apply (rule hoare_split_bind_case_sumE) apply (wp x)[1] apply (rule hoare_split_bind_case_sumE) apply (wp x|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> Syscall_H.syscall m_flt h_flt m_err h_err m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m_flt >>= case_sum (\<lambda>f. liftE (h_flt f)) (\<lambda>a. m_err a >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrace>?R6 rv\<rbrace> liftE (h_flt rv) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>rv. \<lbrace>?S6 rv\<rbrace> m_err rv >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 3. \<lbrace>P\<rbrace> m_flt \<lbrace>?S6\<rbrace>, \<lbrace>?R6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrace>?S6 rv\<rbrace> m_err rv >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>P\<rbrace> m_flt \<lbrace>?S6\<rbrace>, \<lbrace>P_flt\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva. \<lbrace>?R14 rv rva\<rbrace> liftE (h_err rva) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>rv rva. \<lbrace>?S14 rv rva\<rbrace> m_fin rva \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>rv. \<lbrace>?S6 rv\<rbrace> m_err rv \<lbrace>?S14 rv\<rbrace>, \<lbrace>?R14 rv\<rbrace>
 4. \<lbrace>P\<rbrace> m_flt \<lbrace>?S6\<rbrace>, \<lbrace>P_flt\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma setObject_F_ct_activatable':
  "\<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb \<rbrakk> \<Longrightarrow>  \<lbrace>ct_in_state' activatable' and obj_at' ((=) tcb) t\<rbrace>
    setObject t (F f tcb)
   \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>" apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def) apply (rule hoare_pre) apply (wps setObject_ct_inv) apply (wp setObject_tcb_strongest) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>ct_in_state' activatable' and obj_at' ((=) tcb) t\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s) and obj_at' ((=) tcb) t\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>_ s. obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>?Q\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>_ s. obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s\<rbrace>
 2. \<And>s. \<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb; ((\<lambda>s. obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s) and obj_at' ((=) tcb) t) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>?P3 prev_s\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>rv. obj_at' (activatable' \<circ> tcbState) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. \<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb; ((\<lambda>s. obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s) and obj_at' ((=) tcb) t) s\<rbrakk> \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb; ((\<lambda>s. obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s) and obj_at' ((=) tcb) t) s\<rbrakk> \<Longrightarrow> if t = ksCurThread s then (activatable' \<circ> tcbState) (F f tcb) else obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma setObject_F_st_tcb_at':
  "\<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb \<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at' P t' and obj_at' ((=) tcb) t\<rbrace>
    setObject t (F f tcb)
   \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" apply (simp add: st_tcb_at'_def) apply (rule hoare_pre) apply (wp setObject_tcb_strongest) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>st_tcb_at' P t' and obj_at' ((=) tcb) t\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>obj_at' (P \<circ> tcbState) t' and obj_at' ((=) tcb) t\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>_. obj_at' (P \<circ> tcbState) t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>tcb f. tcbState (F f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>?Q\<rbrace> setObject t (F f tcb) \<lbrace>\<lambda>_. obj_at' (P \<circ> tcbState) t'\<rbrace>
 2. \<And>s. \<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb; (obj_at' (P \<circ> tcbState) t' and obj_at' ((=) tcb) t) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb; (obj_at' (P \<circ> tcbState) t' and obj_at' ((=) tcb) t) s\<rbrakk> \<Longrightarrow> if t = t' then (P \<circ> tcbState) (F f tcb) else obj_at' (P \<circ> tcbState) t' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma sendSignal_tcb_at'[wp]:
  "\<lbrace>tcb_at' t\<rbrace>
     sendSignal ntfnptr bdg
   \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>" apply (simp add: sendSignal_def
              cong: list.case_cong Structures_H.notification.case_cong) apply (wp ntfn'_cases_weak_wp list_cases_weak_wp hoare_drop_imps | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> sendSignal ntfnptr bdg \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> do nTFN <- getNotification ntfnptr;
case ntfnObj nTFN of Structures_H.ntfn.IdleNtfn \<Rightarrow> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn bdg) nTFN | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do cancelIPC tcb;
setThreadState Structures_H.thread_state.Running tcb;
asUser tcb $ setRegister Notification_H.badgeRegister bdg;
possibleSwitchTo tcb
od else setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn bdg) nTFN
od | Structures_H.ntfn.ActiveNtfn badge' \<Rightarrow> do newBadge <- return (bdg || badge');
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn newBadge) nTFN
od | Structures_H.ntfn.WaitingNtfn [] \<Rightarrow> haskell_fail [] | Structures_H.ntfn.WaitingNtfn (dest # queue) \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister bdg;
possibleSwitchTo dest
od
od \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma sts_cte_at[wp]:
  "\<lbrace>cte_at' p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_at' p\<rbrace>" apply (simp add: setThreadState_def) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) p\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) p\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma sts_mcpriority_tcb_at'[wp]:
  "\<lbrace>mcpriority_tcb_at' P t\<rbrace>
    setThreadState st t'
   \<lbrace>\<lambda>_. mcpriority_tcb_at' P t\<rbrace>" apply (cases "t = t'",
         simp_all add: setThreadState_def
                  split del: if_split) apply ((wp threadSet_pred_tcb_at_state | simp)+)[1] apply (wp threadSet_obj_at'_really_strongest
               | simp add: pred_tcb_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>mcpriority_tcb_at' P t\<rbrace> setThreadState st t' \<lbrace>\<lambda>_. mcpriority_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>mcpriority_tcb_at' P t'\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. mcpriority_tcb_at' P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>mcpriority_tcb_at' P t\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. mcpriority_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t = t'; mcpriority_tcb_at' P t' s\<rbrakk> \<Longrightarrow> tcb_at' t' s \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbMCP tcb)) t' s
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>mcpriority_tcb_at' P t\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. mcpriority_tcb_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma ct_running_imp_simple'[elim!]:
  "ct_running' s \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s" by (clarsimp simp: ct_in_state'_def
              elim!: pred_tcb'_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running' s \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
theory Syscall_R

lemma handleFaultReply_invs[wp]:
  "\<lbrace>invs' and tcb_at' t\<rbrace> handleFaultReply x t label msg \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: handleFaultReply_def) apply (case_tac x, simp_all) apply (wp | clarsimp simp: handleArchFaultReply_def
                          split: arch_fault.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> handleFaultReply x t label msg \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> case x of Fault_H.fault.UserException x xa \<Rightarrow> do b <- local.getSanitiseRegisterInfo t;
asUser t $ zipWithM_x (\<lambda>r v. setRegister r $ local.sanitiseRegister b r v) FaultHandler_H.exceptionMessage msg;
return (label = 0)
od | Fault_H.fault.CapFault x xa xb \<Rightarrow> return True | Fault_H.fault.UnknownSyscallException x \<Rightarrow> do b <- local.getSanitiseRegisterInfo t;
asUser t $ zipWithM_x (\<lambda>r v. setRegister r $ local.sanitiseRegister b r v) FaultHandler_H.syscallMessage msg;
return (label = 0)
od | Fault_H.fault.ArchFault af \<Rightarrow> handleArchFaultReply af t label msg \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12. x = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> do b <- local.getSanitiseRegisterInfo t;
y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister b r v)) FaultHandler_H.exceptionMessage msg);
return (label = 0)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x21 x22 x23. x = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> return True \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x3. x = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> do b <- local.getSanitiseRegisterInfo t;
y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister b r v)) FaultHandler_H.syscallMessage msg);
return (label = 0)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x4. x = Fault_H.fault.ArchFault x4 \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> handleArchFaultReply x4 t label msg \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma copyMRs_cte_wp_at'[wp]:
  "\<lbrace>cte_wp_at' P ptr\<rbrace> copyMRs sender sendBuf receiver recvBuf n \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>" unfolding copyMRs_def apply (wp mapM_wp | wpc | simp add: split_def | rule equalityD1)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P ptr\<rbrace> copyMRs sender sendBuf receiver recvBuf n \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P ptr\<rbrace> do intSize <- return (fromIntegral wordSize);
hardwareMRs <- return (take (fromIntegral n) TCB_H.msgRegisters);
forM hardwareMRs (\<lambda>r. do v <- asUser sender $ getRegister r;
asUser receiver $ setRegister r v
od);
bufferMRs <- case (sendBuf, recvBuf) of (None, b) \<Rightarrow> return [] | (Some sbPtr, None) \<Rightarrow> return [] | (Some sbPtr, Some rbPtr) \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + PPtr (x * intSize)) >>= storeWordUser (rbPtr + PPtr (x * intSize))) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. n];
return $ min n $ fromIntegral $ length hardwareMRs + length bufferMRs
od \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma setMRs_cte_wp_at'[wp]:
  "\<lbrace>cte_wp_at' P ptr\<rbrace> setMRs thread buffer messageData \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>" by (simp add: setMRs_def zipWithM_x_mapM split_def, wp crunch_wps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P ptr\<rbrace> setMRs thread buffer messageData \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>
theory Syscall_R

lemma doFaultTransfer_cte_wp_at'[wp]:
  "\<lbrace>cte_wp_at' P ptr\<rbrace>
   doFaultTransfer badge sender receiver receiverIPCBuffer
   \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>" unfolding doFaultTransfer_def apply (wp | wpc | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P ptr\<rbrace> doFaultTransfer badge sender receiver receiverIPCBuffer \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P ptr\<rbrace> do fault <- threadGet tcbFault sender;
f <- case fault of None \<Rightarrow> haskell_fail [] | Some f \<Rightarrow> return f;
(faultLabel, faultMsg) <- makeFaultMessage f sender;
sent <- setMRs receiver receiverIPCBuffer faultMsg;
msgInfo <- return (Types_H.message_info.MI sent 0 0 faultLabel);
setMessageInfo receiver msgInfo;
asUser receiver $ setRegister Notification_H.badgeRegister badge
od \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace> proof (prove)
goal:
No subgoals!