theory Refine_C

lemma handleUserLevelFault_ccorres:
  "ccorres dc xfdc
           (invs' and sch_act_simple and ct_running' and
               (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
           (UNIV \<inter> {s.  w_a_' s = word1} \<inter> {s. w_b_' s = word2 }) []
           (callKernel (UserLevelFault word1 word2)) (Call handleUserLevelFault_'proc)" apply (cinit' lift:w_a_' w_b_') apply (simp add: callKernel_def handleEvent_def) apply (rule ccorres_stateAssert) apply (simp add: liftE_bind bind_assoc) apply (rule ccorres_symb_exec_r) apply (rule ccorres_pre_getCurThread) apply (ctac (no_vcg) add: handleFault_ccorres) apply (ctac (no_vcg) add: schedule_ccorres) apply (rule ccorres_stateAssert_after) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: activateThread_ccorres) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply (wp schedule_sch_act_wf schedule_invs'
              | strengthen invs_queues_imp invs_valid_objs_strengthen)+ apply (clarsimp, vcg) apply (clarsimp, rule conseqPre, vcg, clarsimp) apply clarsimp apply (intro impI conjI allI) apply (simp add: ct_in_state'_def) apply (erule pred_tcb'_weakenE) apply simp apply (clarsimp simp: ct_not_ksQ) apply (clarsimp simp add: sch_act_simple_def split: scheduler_action.split) apply (rule active_ex_cap') apply (erule active_from_running') apply (erule invs_iflive') apply (clarsimp simp: ct_in_state'_def) apply (frule st_tcb_idle'[rotated]) apply (erule invs_valid_idle') apply simp apply (clarsimp simp: cfault_rel_def seL4_Fault_UserException_lift) apply (simp add: is_cap_fault_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (UNIV \<inter> \<lbrace>\<acute>w_a = word1\<rbrace> \<inter> \<lbrace>\<acute>w_b = word2\<rbrace>) [] (callKernel (UserLevelFault word1 word2)) (Call handleUserLevelFault_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q256 w_b w_a) (?Q'256 w_b w_a) [SKIP] (callKernel (UserLevelFault word1 word2)) (\<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(UCAST(32 \<rightarrow> 32) w_a,UCAST(32 \<rightarrow> 32) w_b);;
(CALL handleFault_'proc(\<acute>ksCurThread);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q256 w_b w_a s \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (2 subgoals):
 1. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q256 word2 word1) (?Q'256 word2 word1) [SKIP] (do y <- stateAssert fastpathKernelAssertions [];
y <- liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException word1 (word2 && mask 28))
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2);;
(CALL handleFault_'proc(\<acute>ksCurThread);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q256 w_b w_a s \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (2 subgoals):
 1. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P264 word2 word1) (?Q'256 word2 word1) [SKIP] (do y <- liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException word1 (word2 && mask 28))
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2);;
(CALL handleFault_'proc(\<acute>ksCurThread);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P264 w_b w_a s) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (2 subgoals):
 1. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P264 word2 word1) (?Q'256 word2 word1) [SKIP] (do thread <- getCurThread;
rv <- handleFault thread (Fault_H.fault.UserException word1 (word2 && mask 28));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2);;
(CALL handleFault_'proc(\<acute>ksCurThread);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P264 w_b w_a s) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (4 subgoals):
 1. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P264 word2 word1) (?Q'271 w_b w_a) [SKIP] (do thread <- getCurThread;
rv <- handleFault thread (Fault_H.fault.UserException word1 (word2 && mask 28));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL handleFault_'proc(\<acute>ksCurThread);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) (?Q'271 w_b w_a)
 3. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; ?P264 word2 word1 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 4. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P264 w_b w_a s) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (4 subgoals):
 1. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?P278 word2 word1 a rv) (?P'277 w_b w_a rv) [SKIP] (do rv <- handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL handleFault_'proc(\<acute>ksCurThread);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'277 w_b w_a rv}
 3. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P278 word2 word1 s rv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 4. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P278 w_b w_a s rv)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (5 subgoals):
 1. \<And>w_b w_a rv rva xfdca. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q285 w_b w_a rv rva) (?Q'285 w_b w_a rv rva xfdca) [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>?Q285 w_b w_a rv\<rbrace>
 3. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'285 w_b w_a rv rva (xfdc t)}}
 4. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 5. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (6 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdcb. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q316 w_b w_a rv rva xfdca rvb) (?Q'316 w_b w_a rv rva xfdca rvb xfdcb) [SKIP] (do y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q316 w_b w_a rv rva xfdc\<rbrace>
 3. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 4. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rvb. dc rvb (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'316 w_b w_a rv rva (xfdc t) rvb (xfdc ta)}}}
 5. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 6. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (6 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdcb. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q316 w_b w_a rv rva xfdca rvb and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'316 w_b w_a rv rva xfdca rvb xfdcb) [SKIP] activateThread (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q316 w_b w_a rv rva xfdc\<rbrace>
 3. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 4. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rvb. dc rvb (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'316 w_b w_a rv rva (xfdc t) rvb (xfdc ta)}}}
 5. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 6. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (6 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdcb. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q316 w_b w_a rv rva xfdca rvb and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'316 w_b w_a rv rva xfdca rvb xfdcb) [SKIP] (activateThread >>= return) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q316 w_b w_a rv rva xfdc\<rbrace>
 3. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 4. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rvb. dc rvb (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'316 w_b w_a rv rva (xfdc t) rvb (xfdc ta)}}}
 5. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 6. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (7 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdcb rvc xfdcc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdcb; dc rvc xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q346 w_b w_a rv rva xfdca rvb xfdcb rvc) (?Q'346 w_b w_a rv rva xfdca rvb xfdcb rvc xfdcc) [SKIP] (return rvc) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>w_b w_a rv rva xfdca rvb xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>?Q346 w_b w_a rv rva xfdca rvb xfdc\<rbrace>
 3. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rvb. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 5. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rvb. dc rvb (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvc. dc rvc (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'346 w_b w_a rv rva (xfdc t) rvb (xfdc ta) rvc (xfdc tb)}}}}
 6. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 7. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (7 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdcb rvc xfdcc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdcb; dc rvc xfdcc\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return rvc \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>w_b w_a rv rva xfdca rvb xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>rvc _. True\<rbrace>
 3. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rvb. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 5. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}
 6. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 7. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (7 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdcb rvc xfdcc \<sigma>. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdcb; dc rvc xfdcc\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return rvc \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>w_b w_a rv rva xfdca rvb xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>rvc _. True\<rbrace>
 3. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rvb. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 5. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}
 6. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 7. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (6 subgoals):
 1. \<And>w_b w_a rv rva xfdca rvb xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>rvc _. True\<rbrace>
 2. \<And>w_b w_a rv rva xfdc. \<lbrakk>w_b = word2; w_a = word1; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R318 w_b w_a rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rvb. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 3. \<And>w_b w_a rv. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<lbrace>?R288 word2 word1 rv\<rbrace> handleFault rv (Fault_H.fault.UserException word1 (word2 && mask 28)) \<lbrace>\<lambda>a. invs' and ?R318 w_b w_a rv a\<rbrace>
 4. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}
 5. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 word2 word1 rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 6. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and ?R288 w_b w_a rv) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (3 subgoals):
 1. \<And>w_b w_a. \<lbrakk>w_b = word2; w_a = word1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}
 2. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and (\<lambda>a. (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'256 word2 word1 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 3. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and (\<lambda>a. (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a)) s)) \<and> s' \<in> ?Q'256 w_b w_a proof (prove)
goal (2 subgoals):
 1. \<And>w_b w_a s. \<lbrakk>w_b = word2; w_a = word1; \<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and (\<lambda>a. (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>\<forall>t. seL4_Fault_UserException_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = \<lparr>number_CL = word1 && mask 32, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException \<longrightarrow> (\<exists>rv. \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UserException_new_'proc(word1,word2) {s'. (s, s') \<in> rf_sr}
 2. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and (\<lambda>a. (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a)) s)) \<and> s' \<in> \<lbrace>\<forall>t. seL4_Fault_UserException_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = \<lparr>number_CL = w_a && mask 32, code_CL = w_b && mask 28\<rparr> \<and> seL4_Fault_get_tag \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException \<longrightarrow> (\<exists>rv. \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UserException w_a (w_b && mask 28))) (seL4_Fault_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>w_b w_a s s'. \<lbrakk>w_b = word2; w_a = word1; (s, s') \<in> rf_sr; (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and (\<lambda>a. (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a \<and> (invs' and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' rv and ex_nonz_cap_to' rv and (\<lambda>s. rv \<noteq> ksIdleThread s)) a)) s)) \<and> s' \<in> \<lbrace>\<forall>t. seL4_Fault_UserException_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = \<lparr>number_CL = w_a && mask 32, code_CL = w_b && mask 28\<rparr> \<and> seL4_Fault_get_tag \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException \<longrightarrow> (\<exists>rv. \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UserException w_a (w_b && mask 28))) (seL4_Fault_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> st_tcb_at' simple' (ksCurThread s) s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s) \<and> (\<forall>t. seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException \<longrightarrow> (\<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s')))) proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 2. \<And>s s' a b. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (a, b))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 5. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 2. \<And>s s' a b. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (a, b))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 5. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (5 subgoals):
 1. \<And>s s' st. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s; st = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> simple' st
 2. \<And>s s' a b. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (a, b))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 5. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (4 subgoals):
 1. \<And>s s' a b. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (a, b))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 4. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 3. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 2. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> ct_active' s
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap' s
 3. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; fastpathKernelAssertions s\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap' s
 2. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_running' s; ksSchedulerAction s = ResumeCurrentThread; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException\<rbrakk> \<Longrightarrow> valid_idle' s
 2. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; ksCurThread s = ksIdleThread s \<longrightarrow> Structures_H.thread_state.IdleThreadState = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; ksCurThread s = ksIdleThread s \<longrightarrow> Structures_H.thread_state.IdleThreadState = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException; ksCurThread s \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UserException word1 (word2 && mask 28))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; seL4_Fault_UserException_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>; seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_UserException \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>); ksCurThread s \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> if is_cap_fault (SeL4_Fault_UserException \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>) then \<exists>lf'. lookup_fault_lift (current_lookup_fault_' (globals s')) = Some lf' \<and> fault_to_H (SeL4_Fault_UserException \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>) lf' = Some (Fault_H.fault.UserException word1 (word2 && mask 28)) else fault_to_H (SeL4_Fault_UserException \<lparr>number_CL = word1, code_CL = word2 && mask 28\<rparr>) undefined = Some (Fault_H.fault.UserException word1 (word2 && mask 28)) proof (prove)
goal:
No subgoals!