theory Refine_C

lemma handleUnknownSyscall_ccorres:
  "ccorres dc xfdc
           (invs' and ct_running' and
              (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
           (UNIV \<inter> {s. of_nat n = w_' s}) []
           (callKernel (UnknownSyscall n)) (Call handleUnknownSyscall_'proc)" apply (cinit' lift: w_') 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 fastforce 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 (clarsimp simp: cfault_rel_def seL4_Fault_UnknownSyscall_lift is_cap_fault_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (UNIV \<inter> \<lbrace>word_of_nat n = \<acute>w\<rbrace>) [] (callKernel (UnknownSyscall n)) (Call handleUnknownSyscall_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>w. word_of_nat n = w \<Longrightarrow> ccorres dc xfdc (?Q135 w) (?Q'135 w) [SKIP] (callKernel (UnknownSyscall n)) (\<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(UCAST(32 \<rightarrow> 32) w);;
(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 s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q135 w s \<and> s' \<in> ?Q'135 w proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?Q135 (word_of_nat n)) (?Q'135 (word_of_nat n)) [SKIP] (do y <- stateAssert fastpathKernelAssertions [];
y <- liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat n))
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n);;
(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 s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q135 w s \<and> s' \<in> ?Q'135 w proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?P148 (word_of_nat n)) (?Q'135 (word_of_nat n)) [SKIP] (do y <- liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat n))
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n);;
(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 s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P148 w s) \<and> s' \<in> ?Q'135 w proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?P148 (word_of_nat n)) (?Q'135 (word_of_nat n)) [SKIP] (do thread <- getCurThread;
rv <- handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat n));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n);;
(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 s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P148 w s) \<and> s' \<in> ?Q'135 w proof (prove)
goal (4 subgoals):
 1. ccorres dc xfdc (?P148 (word_of_nat n)) ?Q'155 [SKIP] (do thread <- getCurThread;
rv <- handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat n));
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. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) ?Q'155
 3. \<And>s. ?P148 (word_of_nat n) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 4. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P148 w s) \<and> s' \<in> ?Q'135 w proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres dc xfdc (\<lambda>a. ?P160 (word_of_nat n) a rv) (?P'159 rv) [SKIP] (do rv <- handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n));
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. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'159 rv}
 3. \<And>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P160 (word_of_nat n) s rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 4. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P160 w s rv)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (5 subgoals):
 1. \<And>rv rva xfdca. dc rva xfdca \<Longrightarrow> ccorres dc xfdc (?Q166 rv rva) (?Q'166 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>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>?Q166 rv\<rbrace>
 3. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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'166 rv rva (xfdc t)}}
 4. \<And>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 5. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (6 subgoals):
 1. \<And>rv rva xfdca rvb xfdcb. \<lbrakk>dc rva xfdca; dc rvb xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q192 rv rva xfdca rvb) (?Q'192 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>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q192 rv rva xfdc\<rbrace>
 3. \<And>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 4. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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'192 rv rva (xfdc t) rvb (xfdc ta)}}}
 5. \<And>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 6. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (6 subgoals):
 1. \<And>rv rva xfdca rvb xfdcb. \<lbrakk>dc rva xfdca; dc rvb xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q192 rv rva xfdca rvb and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'192 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>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q192 rv rva xfdc\<rbrace>
 3. \<And>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 4. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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'192 rv rva (xfdc t) rvb (xfdc ta)}}}
 5. \<And>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 6. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (6 subgoals):
 1. \<And>rv rva xfdca rvb xfdcb. \<lbrakk>dc rva xfdca; dc rvb xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q192 rv rva xfdca rvb and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'192 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>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 rv rva\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q192 rv rva xfdc\<rbrace>
 3. \<And>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 4. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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'192 rv rva (xfdc t) rvb (xfdc ta)}}}
 5. \<And>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 6. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (7 subgoals):
 1. \<And>rv rva xfdca rvb xfdcb rvc xfdcc. \<lbrakk>dc rva xfdca; dc rvb xfdcb; dc rvc xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q220 rv rva xfdca rvb xfdcb rvc) (?Q'220 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>rv rva xfdca rvb xfdc. \<lbrakk>dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>?Q220 rv rva xfdca rvb xfdc\<rbrace>
 3. \<And>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 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>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 5. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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'220 rv rva (xfdc t) rvb (xfdc ta) rvc (xfdc tb)}}}}
 6. \<And>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 7. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (7 subgoals):
 1. \<And>rv rva xfdca rvb xfdcb rvc xfdcc. \<lbrakk>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>rv rva xfdca rvb xfdc. \<lbrakk>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>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 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>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 5. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 7. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (7 subgoals):
 1. \<And>rv rva xfdca rvb xfdcb rvc xfdcc \<sigma>. \<lbrakk>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>rv rva xfdca rvb xfdc. \<lbrakk>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>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 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>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 5. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 7. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (6 subgoals):
 1. \<And>rv rva xfdca rvb xfdc. \<lbrakk>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>rv rva xfdc. dc rva xfdc \<Longrightarrow> \<lbrace>?R194 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>rv. \<lbrace>?R169 (word_of_nat n) rv\<rbrace> handleFault rv (Fault_H.fault.UnknownSyscallException (word_of_nat n)) \<lbrace>\<lambda>a. invs' and ?R194 rv a\<rbrace>
 4. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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>s. \<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 ?R169 (word_of_nat n) rv) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 6. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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 ?R169 w rv) s)) \<and> s' \<in> ?Q'135 w proof (prove)
goal (3 subgoals):
 1. \<Gamma>\<turnstile> (?Q'135 (word_of_nat n)) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {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.UnknownSyscallException (word_of_nat n))) (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>s. \<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 \<Longrightarrow> \<Gamma>\<turnstile> (?Q'135 (word_of_nat n) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>current_fault :== CALL seL4_Fault_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 3. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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'135 w proof (prove)
goal (2 subgoals):
 1. \<And>s. \<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 \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>\<forall>t. seL4_Fault_UnknownSyscall_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = \<lparr>syscallNumber_CL = word_of_nat n && mask 32\<rparr> \<and> seL4_Fault_get_tag \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall \<longrightarrow> (\<exists>rv. \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_new_'proc(word_of_nat n) {s'. (s, s') \<in> rf_sr}
 2. \<And>w s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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_UnknownSyscall_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = \<lparr>syscallNumber_CL = w && mask 32\<rparr> \<and> seL4_Fault_get_tag \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall \<longrightarrow> (\<exists>rv. \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException w)) (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 s s'. \<lbrakk>word_of_nat n = w; (s, s') \<in> rf_sr; (invs' 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_UnknownSyscall_lift \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = \<lparr>syscallNumber_CL = w && mask 32\<rparr> \<and> seL4_Fault_get_tag \<^bsup>t\<^esup>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall \<longrightarrow> (\<exists>rv. \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException w)) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall \<longrightarrow> (\<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv) \<longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; \<exists>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall\<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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; ksCurThread s = ksIdleThread s \<longrightarrow> Structures_H.thread_state.IdleThreadState = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (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_UnknownSyscall_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>syscallNumber_CL = word_of_nat n\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall; ksCurThread s = ksIdleThread s \<longrightarrow> Structures_H.thread_state.IdleThreadState = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> cfault_rel (Some (Fault_H.fault.UnknownSyscallException (word_of_nat n))) (seL4_Fault_lift (ret__struct_seL4_Fault_C_' t)) (lookup_fault_lift (current_lookup_fault_' (globals s'))) proof (prove)
goal:
No subgoals!