theory Refine_C

lemma handleVMFaultEvent_ccorres:
  "ccorres dc xfdc
           (invs' and sch_act_simple and ct_running' and
               (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
           (UNIV \<inter> {s.  vm_faultType_' s = vm_fault_type_from_H vmfault_type}) []
           (callKernel (VMFaultEvent vmfault_type)) (Call handleVMFaultEvent_'proc)" apply (cinit' lift:vm_faultType_') apply (simp add: callKernel_def handleEvent_def) apply (rule ccorres_stateAssert) apply (simp add: liftE_bind bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rename_tac thread) apply (simp add: catch_def) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_split_nothrow_case_sum) apply (ctac (no_vcg) add: handleVMFault_ccorres) apply ceqv apply clarsimp apply clarsimp apply (rule ccorres_cond_univ) apply (rule_tac P="\<lambda>s. ksCurThread s = thread" in ccorres_cross_over_guard) apply (rule_tac xf'=xfdc in ccorres_call) apply (ctac (no_vcg) add: handleFault_ccorres) apply simp apply simp apply simp apply (wp hv_inv_ex') apply (simp add: guard_is_UNIV_def) apply (vcg exspec=handleVMFault_modifies) apply ceqv apply clarsimp 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 (case_tac x, clarsimp, wp) apply (clarsimp, wp, simp) apply wp apply (simp add: guard_is_UNIV_def) apply (clarsimp simp: simple_sane_strg[unfolded sch_act_sane_not]) by (auto simp: ct_in_state'_def cfault_rel_def is_cap_fault_def ct_not_ksQ
              elim: pred_tcb'_weakenE st_tcb_ex_cap''
              dest: st_tcb_at_idle_thread' rf_sr_ksCurThread)

(* 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>vm_faultType = vm_fault_type_from_H vmfault_type\<rbrace>) [] (callKernel (VMFaultEvent vmfault_type)) (Call handleVMFaultEvent_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>vm_faultType. vm_faultType = vm_fault_type_from_H vmfault_type \<Longrightarrow> ccorres dc xfdc (?Q151 vm_faultType) (?Q'151 vm_faultType) [SKIP] (callKernel (VMFaultEvent vmfault_type)) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_faultType);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?Q151 vm_faultType s \<and> s' \<in> ?Q'151 vm_faultType proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?Q151 (vm_fault_type_from_H vmfault_type)) (?Q'151 (vm_fault_type_from_H vmfault_type)) [SKIP] (do y <- stateAssert fastpathKernelAssertions [];
y <- liftE (do thread <- getCurThread;
handleVMFault thread vmfault_type <catch> handleFault thread
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?Q151 vm_faultType s \<and> s' \<in> ?Q'151 vm_faultType proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?P164 (vm_fault_type_from_H vmfault_type)) (?Q'151 (vm_fault_type_from_H vmfault_type)) [SKIP] (do y <- liftE (do thread <- getCurThread;
handleVMFault thread vmfault_type <catch> handleFault thread
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?P164 vm_faultType s) \<and> s' \<in> ?Q'151 vm_faultType proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?P164 (vm_fault_type_from_H vmfault_type)) (?Q'151 (vm_fault_type_from_H vmfault_type)) [SKIP] (do thread <- getCurThread;
rv <- handleVMFault thread vmfault_type <catch> handleFault thread;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?P164 vm_faultType s) \<and> s' \<in> ?Q'151 vm_faultType proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres dc xfdc (\<lambda>a. ?P173 (vm_fault_type_from_H vmfault_type) a rv) (?P'174 (vm_fault_type_from_H vmfault_type) rv) [SKIP] (do rv <- handleVMFault rv vmfault_type <catch> handleFault rv;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?P173 vm_faultType s rv)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'174 vm_faultType rv} proof (prove)
goal (2 subgoals):
 1. \<And>thread. ccorres dc xfdc (\<lambda>a. ?P173 (vm_fault_type_from_H vmfault_type) a thread) (?P'174 (vm_fault_type_from_H vmfault_type) thread) [SKIP] (do rv <- handleVMFault thread vmfault_type <catch> handleFault thread;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?P173 vm_faultType s rv)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'174 vm_faultType rv} proof (prove)
goal (2 subgoals):
 1. \<And>thread. ccorres dc xfdc (\<lambda>a. ?P173 (vm_fault_type_from_H vmfault_type) a thread) (?P'174 (vm_fault_type_from_H vmfault_type) thread) [SKIP] (do rv <- do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
(IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?P173 vm_faultType s rv)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'174 vm_faultType rv} proof (prove)
goal (2 subgoals):
 1. \<And>thread. ccorres dc xfdc (?P182 (vm_fault_type_from_H vmfault_type) thread) (?P'174 (vm_fault_type_from_H vmfault_type) thread) [SKIP] (do rv <- do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ?P182 vm_faultType rv s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'174 vm_faultType rv} proof (prove)
goal (6 subgoals):
 1. \<And>thread. ccorres (?r'184 thread) (?xf'184 thread) (?P188 (vm_fault_type_from_H vmfault_type) thread) (?P'174 (vm_fault_type_from_H vmfault_type) thread) [] (do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI)
 2. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 3. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 4. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 5. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 6. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> (?P188 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'174 vm_faultType rv} proof (prove)
goal (11 subgoals):
 1. \<And>thread. ccorres (?f'194 thread \<currency> ?r'194 thread) (liftxf (?es194 thread) (?ef'194 thread) (?vf'194 thread) (?xf'194 thread)) (?P200 (vm_fault_type_from_H vmfault_type) thread) (?P'196 (vm_fault_type_from_H vmfault_type) thread) [] (handleVMFault thread vmfault_type) (\<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type))
 2. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'194 thread) rv' t t' (IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI) (?d'194 thread rv')
 3. \<And>thread rv rv'. \<lbrakk>?r'194 thread rv (?vf'194 thread rv'); ?ef'194 thread rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?Q194 thread rv) (?Q'194 thread rv rv') [] (return rv) (?d'194 thread rv')
 4. \<And>thread err rv' err'. \<lbrakk>?ef'194 thread rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; ?f'194 thread err (?ef'194 thread rv') err'\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?QE194 thread err) (?Q''194 thread err rv' err') [] (handleFault thread err) (?d'194 thread rv')
 5. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>?QE194 thread\<rbrace>
 6. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. ?ef'194 thread (?xf'194 thread s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> ?r'194 thread rv' (?vf'194 thread (?xf'194 thread s)) \<longrightarrow> s \<in> ?Q'194 thread rv' (?xf'194 thread s)) \<and> (\<forall>ft. ?ef'194 thread (?xf'194 thread s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> ?f'194 thread ft (?ef'194 thread (?xf'194 thread s)) (?es194 thread s) \<longrightarrow> s \<in> ?Q''194 thread ft (?xf'194 thread s) (?es194 thread s))}
 7. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 8. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 9. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 10. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>thread rv' t t'. ceqv \<Gamma> status_' rv' t t' (IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI) (?d'194 thread rv')
 2. \<And>thread rv rv'. \<lbrakk>False; id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?Q194 thread rv) (?Q'194 thread rv rv') [] (return rv) (?d'194 thread rv')
 3. \<And>thread err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. err = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault err' = Some (SeL4_Fault_VMFault vf))\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?QE194 thread err) (?Q''194 thread err rv' err') [] (handleFault thread err) (?d'194 thread rv')
 4. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>?QE194 thread\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> ?Q''194 thread ft (status_' s) (errstate s))}
 6. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 7. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 8. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 9. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 10. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (9 subgoals):
 1. \<And>thread rv rv'. \<lbrakk>False; id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?Q194 thread rv) (?Q'194 thread rv rv') [] (return rv) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI)
 2. \<And>thread err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. err = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault err' = Some (SeL4_Fault_VMFault vf))\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?QE194 thread err) (?Q''194 thread err rv' err') [] (handleFault thread err) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI)
 3. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>?QE194 thread\<rbrace>
 4. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> ?Q''194 thread ft (status_' s) (errstate s))}
 5. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 6. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 7. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 8. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 9. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (8 subgoals):
 1. \<And>thread err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. err = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault err' = Some (SeL4_Fault_VMFault vf))\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?QE194 thread err) (?Q''194 thread err rv' err') [] (handleFault thread err) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleFault_'proc(\<acute>ksCurThread)
FI)
 2. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>?QE194 thread\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> ?Q''194 thread ft (status_' s) (errstate s))}
 4. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 5. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 6. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 7. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 8. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (8 subgoals):
 1. \<And>thread err' vf. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?QE194 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (?Q''194 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf])) (SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) err') [] (handleFault thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (Cond UNIV (CALL handleFault_'proc(\<acute>ksCurThread)) SKIP)
 2. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>?QE194 thread\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> ?Q''194 thread ft (status_' s) (errstate s))}
 4. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 5. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 6. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 7. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 8. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (8 subgoals):
 1. \<And>thread err' vf. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?QE194 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (?Q''194 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf])) (SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) err') [] (handleFault thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (CALL handleFault_'proc(\<acute>ksCurThread))
 2. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>?QE194 thread\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> ?Q''194 thread ft (status_' s) (errstate s))}
 4. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 5. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 6. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 7. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 8. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (8 subgoals):
 1. \<And>thread err' vf. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf'184 thread) (?P'461 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (?Q460 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf])) (SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) err') [] (handleFault thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (CALL handleFault_'proc(\<acute>ksCurThread))
 2. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>s. ksCurThread s = thread) and ?P'461 thread a\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>sa. (sa, s') \<in> rf_sr \<and> ksCurThread sa = thread \<longrightarrow> s' \<in> ?Q460 thread ft (status_' s) (errstate s)})}
 4. \<And>thread rv' t t'. ceqv \<Gamma> (?xf'184 thread) rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 5. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 6. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 7. \<And>thread. guard_is_UNIV (?r'184 thread) (?xf'184 thread) (?Q'184 thread)
 8. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (11 subgoals):
 1. \<And>thread err' vf. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> ccorres (?r'184 thread) (?xf''463 thread err' vf) (?P'461 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (?C'468 thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf])) (SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) err') [] (handleFault thread (Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))) (Call handleFault_'proc)
 2. \<And>thread err' vf x y s. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> globals s = globals s
 3. \<And>thread err' vf a s t. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = ?xf''463 thread err' vf t
 4. \<And>thread err' vf s. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> globals (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) = globals s
 5. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>s. ksCurThread s = thread) and ?P'461 thread a\<rbrace>
 6. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>sa. (sa, s') \<in> rf_sr \<and> ksCurThread sa = thread \<longrightarrow> s' \<in> {sa. tptr_'_update (\<lambda>_. ksCurThread_' (globals sa)) sa \<in> ?C'468 thread ft (status_' s) (errstate s)}})}
 7. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 8. \<And>thread rv rv'. ?r'184 thread rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 9. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 10. \<And>thread. guard_is_UNIV (?r'184 thread) xfdc (?Q'184 thread)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>thread err' vf x y s. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> globals s = globals s
 2. \<And>thread err' vf a s t. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = xfdc t
 3. \<And>thread err' vf s. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> globals (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) = globals s
 4. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>s. ksCurThread s = thread) and (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)))\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ksCurThread s = thread \<longrightarrow> s' \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some ft) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}})}
 6. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 7. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 8. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 9. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 10. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (9 subgoals):
 1. \<And>thread err' vf a s t. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = xfdc t
 2. \<And>thread err' vf s. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> globals (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) = globals s
 3. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>s. ksCurThread s = thread) and (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)))\<rbrace>
 4. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ksCurThread s = thread \<longrightarrow> s' \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some ft) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}})}
 5. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 6. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 7. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 8. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 9. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (8 subgoals):
 1. \<And>thread err' vf s. \<lbrakk>EXCEPTION_FAULT \<noteq> EXCEPTION_NONE; errfault err' = Some (SeL4_Fault_VMFault vf)\<rbrakk> \<Longrightarrow> globals (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) = globals s
 2. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>s. ksCurThread s = thread) and (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)))\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ksCurThread s = thread \<longrightarrow> s' \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some ft) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}})}
 4. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 5. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 6. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 7. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 8. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (7 subgoals):
 1. \<And>thread. \<lbrace>?R199 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?Q194 thread\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>s. ksCurThread s = thread) and (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)))\<rbrace>
 2. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ksCurThread s = thread \<longrightarrow> s' \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some ft) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}})}
 3. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 4. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 5. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 6. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 7. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ?R199 vm_faultType rv and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (6 subgoals):
 1. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> False \<longrightarrow> s \<in> ?Q'194 thread rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault (errstate s) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> s \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ksCurThread s = thread \<longrightarrow> s' \<in> {s. tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some ft) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}})}
 2. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 3. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 4. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 5. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 6. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (6 subgoals):
 1. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 (vm_fault_type_from_H vmfault_type) thread) \<acute>status :== CALL handleVMFault_'proc(\<acute>ksCurThread,vm_fault_type_from_H vmfault_type) {s. status_' s \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. status_' s = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals s)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, s) \<in> rf_sr \<and> ksCurThread sa = thread) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals s))) (lookup_fault_lift (current_lookup_fault_' (globals s))) \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread)}
 2. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 3. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 4. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 5. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 6. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> ?R'195 vm_faultType rv} proof (prove)
goal (5 subgoals):
 1. \<And>thread rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'184 thread rv')
 2. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (?d'184 thread rv')
 3. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 4. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv rv'. dc rv rv' \<Longrightarrow> ccorres dc xfdc (?Q184 thread rv) (?Q'184 thread rv rv') [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>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 3. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv'. ccorres dc xfdc (?Q184 thread ()) (?Q'184 thread () rv') [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>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>?Q184 thread\<rbrace>
 3. \<And>thread. guard_is_UNIV dc xfdc (?Q'184 thread)
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (5 subgoals):
 1. \<And>thread rv' rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q543 thread rv' rv) (?Q'543 thread rv' rv xfdca) [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>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q543 thread rv'\<rbrace>
 3. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 4. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'549 thread a b t rv})
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}}
flex-flex pairs:
\<lambda>thread. ?Q'549 thread () \<equiv>\<^sup>? \<lambda>thread rv' t rv. ?Q'543 thread rv' rv (xfdc t) proof (prove)
goal (5 subgoals):
 1. \<And>thread rv' rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q543 thread rv' rv and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'543 thread rv' rv xfdca) [SKIP] activateThread (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q543 thread rv'\<rbrace>
 3. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 4. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'549 thread a b t rv})
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}}
flex-flex pairs:
\<lambda>thread. ?Q'549 thread () \<equiv>\<^sup>? \<lambda>thread rv' t rv. ?Q'543 thread rv' rv (xfdc t) proof (prove)
goal (5 subgoals):
 1. \<And>thread rv' rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q543 thread rv' rv and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'543 thread rv' rv xfdca) [SKIP] (activateThread >>= return) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q543 thread rv'\<rbrace>
 3. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 4. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'549 thread a b t rv})
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}}
flex-flex pairs:
\<lambda>thread. ?Q'549 thread () \<equiv>\<^sup>? \<lambda>thread rv' t rv. ?Q'543 thread rv' rv (xfdc t) proof (prove)
goal (6 subgoals):
 1. \<And>thread rv' rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q588 thread rv' rv xfdca rva) (?Q'588 thread rv' rv xfdca rva xfdcb) [SKIP] (return rva) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>thread rv' rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>?Q588 thread rv' rv xfdc\<rbrace>
 3. \<And>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 5. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'593 thread a b t rv ta rva}})
 6. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}}
flex-flex pairs:
\<lambda>thread. ?Q'593 thread () \<equiv>\<^sup>? \<lambda>thread rv' t rv ta rva. ?Q'588 thread rv' rv (xfdc t) rva (xfdc ta) proof (prove)
goal (6 subgoals):
 1. \<And>thread rv' rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<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 rva \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>thread rv' rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 5. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread rv' rv xfdca rva xfdcb \<sigma>. \<lbrakk>dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return rva \<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>thread rv' rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 5. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (5 subgoals):
 1. \<And>thread rv' rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>thread rv'. \<lbrace>?R552 thread ()\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 3. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> do x <- handleVMFault thread vmfault_type;
case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>a. invs' and ?R552 thread a\<rbrace>
 4. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread x. \<lbrace>?B671 thread x\<rbrace> case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b \<lbrace>\<lambda>rv s. invs' s \<and> invs' s \<and> invs' s \<and> invs' s \<and> invs' s\<rbrace>
 2. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>?B671 thread\<rbrace>
 3. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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}})
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread x b. x = Inr b \<Longrightarrow> \<lbrace>invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s)\<rbrace> case x of Inl e \<Rightarrow> handleFault thread e | Inr b \<Rightarrow> return b \<lbrace>\<lambda>rv s. invs' s \<and> invs' s \<and> invs' s \<and> invs' s \<and> invs' s\<rbrace>
 2. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>\<lambda>x2. invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s)\<rbrace>
 3. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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}})
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?R187 (vm_fault_type_from_H vmfault_type) thread\<rbrace> handleVMFault thread vmfault_type \<lbrace>\<lambda>x2. invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s)\<rbrace>
 2. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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}})
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (invs' and st_tcb_at' simple' rv and sch_act_not rv and (\<lambda>s. \<forall>p. rv \<notin> set (ksReadyQueues s p)))) and ?R187 vm_faultType rv) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (2 subgoals):
 1. \<And>thread. guard_is_UNIV dc xfdc (\<lambda>a b. {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>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (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 tcb_at' rv) a \<and> sch_act_not rv a \<and> (\<forall>p. rv \<notin> set (ksReadyQueues a p)) \<and> st_tcb_at' simple' rv a \<and> ex_nonz_cap_to' rv a \<and> rv \<noteq> ksIdleThread a)) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} proof (prove)
goal (1 subgoal):
 1. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vmfault_type; (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> ((\<lambda>a. True) and ((\<lambda>s. ksCurThread s = rv) and (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 tcb_at' rv) a \<and> sch_act_not rv a \<and> (\<forall>p. rv \<notin> set (ksReadyQueues a p)) \<and> st_tcb_at' simple' rv a \<and> ex_nonz_cap_to' rv a \<and> rv \<noteq> ksIdleThread a)) s)) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_faultType) (thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_faultType\<rbrace>} \<inter> {s. \<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>sa. (sa, status_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) (s\<lparr>globals := globals s\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>)) \<in> rf_sr \<and> ksCurThread sa = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)}} 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> tcb_at' (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>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> (\<forall>t. ret__unsigned_long_' t \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>ft. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. ft = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> seL4_Fault_lift (current_fault_' (globals t)) = Some (SeL4_Fault_VMFault vf)) \<longrightarrow> (\<exists>s. (s, s'\<lparr>globals := globals s'\<lparr>active_irq_' := active_irq_' (globals t), armKSASIDTable_' := armKSASIDTable_' (globals t), armKSHWASIDTable_' := armKSHWASIDTable_' (globals t), armKSNextASID_' := armKSNextASID_' (globals t), avail_reg_' := avail_reg_' (globals t), current_extra_caps_' := current_extra_caps_' (globals t), current_fault_' := current_fault_' (globals t), current_lookup_fault_' := current_lookup_fault_' (globals t), current_syscall_error_' := current_syscall_error_' (globals t), intStateIRQTable_' := intStateIRQTable_' (globals t), isFPUEnabledCached_' := isFPUEnabledCached_' (globals t), ksCurDomain_' := ksCurDomain_' (globals t), ksCurThread_' := ksCurThread_' (globals t), ksDomScheduleIdx_' := ksDomScheduleIdx_' (globals t), ksDomainTime_' := ksDomainTime_' (globals t), ksIdleThread_' := ksIdleThread_' (globals t), ksNumCPUs_' := ksNumCPUs_' (globals t), ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), ksWorkUnitsCompleted_' := ksWorkUnitsCompleted_' (globals t), ndks_boot_' := ndks_boot_' (globals t), phantom_machine_state_' := phantom_machine_state_' (globals t), rootserver_' := rootserver_' (globals t), rootserver_mem_' := rootserver_mem_' (globals t), t_hrs_' := t_hrs_' (globals t), tlbLockCount_' := tlbLockCount_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> ksCurThread s = rv) \<longrightarrow> cfault_rel (Some ft) (seL4_Fault_lift (current_fault_' (globals t))) (lookup_fault_lift (current_lookup_fault_' (globals t))) \<and> ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr rv)))