theory Refine_C

lemma callKernel_corres_C:
  "corres_underlying rf_sr False True dc
           (all_invs' e)
           \<top>
           (callKernel e) (callKernel_C e)" using no_fail_callKernel [of e] apply (clarsimp simp: callKernel_C_def) apply (cases e, simp_all) prefer 4 apply (rule ccorres_corres_u) apply simp apply (rule ccorres_guard_imp) apply (rule handleInterruptEntry_ccorres) apply (clarsimp simp: all_invs'_def sch_act_simple_def) apply simp apply assumption prefer 2 apply (rule ccorres_corres_u [rotated], assumption) apply simp apply (rule ccorres_guard_imp) apply (rule ccorres_call) apply (rule handleUnknownSyscall_ccorres) apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ prefer 3 apply (rule ccorres_corres_u [rotated], assumption) apply (rule ccorres_guard_imp) apply (rule ccorres_call) apply (rule handleVMFaultEvent_ccorres) apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ prefer 2 apply (rule ccorres_corres_u [rotated], assumption) apply (rule ccorres_guard_imp) apply (rule ccorres_call) apply (rule handleUserLevelFault_ccorres) apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ apply (rule ccorres_corres_u [rotated], assumption) apply (rule ccorres_guard_imp) apply (rule ccorres_call) apply (rule handleSyscall_ccorres) apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ apply (rule ccorres_corres_u [rotated], assumption) apply (rule ccorres_guard_imp) apply (rule handleHypervisorEvent_ccorres) apply (clarsimp simp: all_invs'_def sch_act_simple_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e) proof (prove)
using this:
no_fail (all_invs' e) (callKernel e)

goal (1 subgoal):
 1. corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e) proof (prove)
goal (1 subgoal):
 1. no_fail (all_invs' e) (callKernel e) \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (case e of SyscallEvent n \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H n)) | UnknownSyscall n \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat n)) | UserLevelFault w1 w2 \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(w1,w2)) | Interrupt \<Rightarrow> exec_C \<Gamma> (Call handleInterruptEntry_'proc) | VMFaultEvent t \<Rightarrow> exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H t)) | HypervisorEvent t \<Rightarrow> exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (6 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 2. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' Interrupt) (\<lambda>_. True) (callKernel Interrupt) (exec_C \<Gamma> (Call handleInterruptEntry_'proc))
 5. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 6. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' Interrupt) (\<lambda>_. True) (callKernel Interrupt) (exec_C \<Gamma> (Call handleInterruptEntry_'proc))
 2. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 4. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 5. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 6. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' Interrupt) \<lbrace>True\<rbrace> [] (callKernel Interrupt) (Call handleInterruptEntry_'proc)
 2. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> no_fail (all_invs' Interrupt) (callKernel Interrupt)
 3. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 4. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 5. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 6. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 7. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' Interrupt) UNIV [] (callKernel Interrupt) (Call handleInterruptEntry_'proc)
 2. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> no_fail (all_invs' Interrupt) (callKernel Interrupt)
 3. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 4. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 5. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 6. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 7. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q6 ?Q'6 [] (callKernel Interrupt) (Call handleInterruptEntry_'proc)
 2. \<And>s. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt; all_invs' Interrupt s\<rbrakk> \<Longrightarrow> ?Q6 s
 3. \<And>s. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'6
 4. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> no_fail (all_invs' Interrupt) (callKernel Interrupt)
 5. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 6. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 7. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 8. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 9. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt; all_invs' Interrupt s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple) s
 2. \<And>s. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV
 3. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> no_fail (all_invs' Interrupt) (callKernel Interrupt)
 4. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 5. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 6. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 7. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 8. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV
 2. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> no_fail (all_invs' Interrupt) (callKernel Interrupt)
 3. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 4. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 5. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 6. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 7. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>no_fail (all_invs' Interrupt) (callKernel Interrupt); e = Interrupt\<rbrakk> \<Longrightarrow> no_fail (all_invs' Interrupt) (callKernel Interrupt)
 2. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 4. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 5. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 6. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 2. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 5. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UnknownSyscall x2)) (\<lambda>_. True) (callKernel (UnknownSyscall x2)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2)))
 2. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 5. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' (UnknownSyscall x2)) \<lbrace>True\<rbrace> [] (callKernel (UnknownSyscall x2)) (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2))
 2. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 5. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' (UnknownSyscall x2)) UNIV [] (callKernel (UnknownSyscall x2)) (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2))
 2. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 5. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (7 subgoals):
 1. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q30 x2) (?Q'30 x2) [] (callKernel (UnknownSyscall x2)) (\<acute>ret__unsigned_long :== CALL handleUnknownSyscall_'proc(word_of_nat x2))
 2. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2; all_invs' (UnknownSyscall x2) s\<rbrakk> \<Longrightarrow> ?Q30 x2 s
 3. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'30 x2
 4. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 5. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 6. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 7. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (10 subgoals):
 1. \<And>x2. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> ccorres dc (?xf''34 x2) (?Q30 x2) (?C'34 x2) [] (callKernel (UnknownSyscall x2)) (Call handleUnknownSyscall_'proc)
 2. \<And>x2 i t s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 3. \<And>x2 a s t. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = ?xf''34 x2 t
 4. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> globals (w_'_update (\<lambda>_. word_of_nat x2) s) = globals s
 5. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2; all_invs' (UnknownSyscall x2) s\<rbrakk> \<Longrightarrow> ?Q30 x2 s
 6. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> {s. w_'_update (\<lambda>_. word_of_nat x2) s \<in> ?C'34 x2}
 7. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 8. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 9. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 10. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (9 subgoals):
 1. \<And>x2 i t s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 2. \<And>x2 a s t. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = xfdc t
 3. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> globals (w_'_update (\<lambda>_. word_of_nat x2) s) = globals s
 4. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2; all_invs' (UnknownSyscall x2) s\<rbrakk> \<Longrightarrow> (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 5. \<And>x2 s. \<lbrakk>no_fail (all_invs' (UnknownSyscall x2)) (callKernel (UnknownSyscall x2)); e = UnknownSyscall x2; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> {s. w_'_update (\<lambda>_. word_of_nat x2) s \<in> UNIV \<inter> \<lbrace>word_of_nat x2 = \<acute>w\<rbrace>}
 6. \<And>x1. \<lbrakk>no_fail (all_invs' (SyscallEvent x1)) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (SyscallEvent x1)) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 7. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 8. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 9. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 2. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 3. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 4. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (4 subgoals):
 1. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (VMFaultEvent x5)) (\<lambda>_. True) (callKernel (VMFaultEvent x5)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5)))
 2. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (4 subgoals):
 1. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' (VMFaultEvent x5)) \<lbrace>True\<rbrace> [] (callKernel (VMFaultEvent x5)) (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5))
 2. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 4. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (6 subgoals):
 1. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q64 x5) (?Q'64 x5) [] (callKernel (VMFaultEvent x5)) (\<acute>ret__unsigned_long :== CALL handleVMFaultEvent_'proc(vm_fault_type_from_H x5))
 2. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5; all_invs' (VMFaultEvent x5) s\<rbrakk> \<Longrightarrow> ?Q64 x5 s
 3. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'64 x5
 4. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 5. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 6. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (9 subgoals):
 1. \<And>x5. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> ccorres dc (?xf''68 x5) (?Q64 x5) (?C'68 x5) [] (callKernel (VMFaultEvent x5)) (Call handleVMFaultEvent_'proc)
 2. \<And>x5 i t s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 3. \<And>x5 a s t. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = ?xf''68 x5 t
 4. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> globals (vm_faultType_'_update (\<lambda>_. vm_fault_type_from_H x5) s) = globals s
 5. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5; all_invs' (VMFaultEvent x5) s\<rbrakk> \<Longrightarrow> ?Q64 x5 s
 6. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_fault_type_from_H x5) s \<in> ?C'68 x5}
 7. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 8. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 9. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (8 subgoals):
 1. \<And>x5 i t s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 2. \<And>x5 a s t. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = xfdc t
 3. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> globals (vm_faultType_'_update (\<lambda>_. vm_fault_type_from_H x5) s) = globals s
 4. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5; all_invs' (VMFaultEvent x5) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 5. \<And>x5 s. \<lbrakk>no_fail (all_invs' (VMFaultEvent x5)) (callKernel (VMFaultEvent x5)); e = VMFaultEvent x5; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. vm_faultType_'_update (\<lambda>_. vm_fault_type_from_H x5) s \<in> UNIV \<inter> \<lbrace>\<acute>vm_faultType = vm_fault_type_from_H x5\<rbrace>}
 6. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 7. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 8. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 2. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 3. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (UserLevelFault x31 x32)) (\<lambda>_. True) (callKernel (UserLevelFault x31 x32)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32)))
 2. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' (UserLevelFault x31 x32)) \<lbrace>True\<rbrace> [] (callKernel (UserLevelFault x31 x32)) (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32))
 2. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 3. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q95 x31 x32) (?Q'95 x31 x32) [] (callKernel (UserLevelFault x31 x32)) (\<acute>ret__unsigned_long :== CALL handleUserLevelFault_'proc(x31,x32))
 2. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32; all_invs' (UserLevelFault x31 x32) s\<rbrakk> \<Longrightarrow> ?Q95 x31 x32 s
 3. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'95 x31 x32
 4. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 5. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (8 subgoals):
 1. \<And>x31 x32. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> ccorres dc (?xf''99 x31 x32) (?Q95 x31 x32) (?C'99 x31 x32) [] (callKernel (UserLevelFault x31 x32)) (Call handleUserLevelFault_'proc)
 2. \<And>x31 x32 i t s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 3. \<And>x31 x32 a s t. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = ?xf''99 x31 x32 t
 4. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> globals (w_b_'_update (\<lambda>_. x32) (w_a_'_update (\<lambda>_. x31) s)) = globals s
 5. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32; all_invs' (UserLevelFault x31 x32) s\<rbrakk> \<Longrightarrow> ?Q95 x31 x32 s
 6. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. w_b_'_update (\<lambda>_. x32) (w_a_'_update (\<lambda>_. x31) s) \<in> ?C'99 x31 x32}
 7. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 8. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x32 i t s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 2. \<And>x31 x32 a s t. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = xfdc t
 3. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> globals (w_b_'_update (\<lambda>_. x32) (w_a_'_update (\<lambda>_. x31) s)) = globals s
 4. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32; all_invs' (UserLevelFault x31 x32) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 5. \<And>x31 x32 s. \<lbrakk>no_fail (all_invs' (UserLevelFault x31 x32)) (callKernel (UserLevelFault x31 x32)); e = UserLevelFault x31 x32; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. w_b_'_update (\<lambda>_. x32) (w_a_'_update (\<lambda>_. x31) s) \<in> UNIV \<inter> \<lbrace>\<acute>w_a = x31\<rbrace> \<inter> \<lbrace>\<acute>w_b = x32\<rbrace>}
 6. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 7. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (SyscallEvent x1)) (exec_C \<Gamma> (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1)))
 2. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) \<lbrace>True\<rbrace> [] (callKernel (SyscallEvent x1)) (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1))
 2. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q126 x1) (?Q'126 x1) [] (callKernel (SyscallEvent x1)) (\<acute>ret__unsigned_long :== CALL handleSyscall_'proc(syscall_from_H x1))
 2. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1; \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_running' s \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ?Q126 x1 s
 3. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'126 x1
 4. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> ccorres dc (?xf''130 x1) (?Q126 x1) (?C'130 x1) [] (callKernel (SyscallEvent x1)) (Call handleSyscall_'proc)
 2. \<And>x1 i t s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 3. \<And>x1 a s t. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = ?xf''130 x1 t
 4. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> globals (syscall_'_update (\<lambda>_. syscall_from_H x1) s) = globals s
 5. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1; \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_running' s \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ?Q126 x1 s
 6. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. syscall_'_update (\<lambda>_. syscall_from_H x1) s \<in> ?C'130 x1}
 7. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (6 subgoals):
 1. \<And>x1 i t s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> globals (s\<lparr>ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = globals s
 2. \<And>x1 a s t. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = xfdc t
 3. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1\<rbrakk> \<Longrightarrow> globals (syscall_'_update (\<lambda>_. syscall_from_H x1) s) = globals s
 4. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1; \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_running' s \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 5. \<And>x1 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (SyscallEvent x1)); e = SyscallEvent x1; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. syscall_'_update (\<lambda>_. syscall_from_H x1) s \<in> UNIV \<inter> \<lbrace>\<acute>syscall = syscall_from_H x1\<rbrace>}
 6. \<And>x6. \<lbrakk>no_fail (all_invs' (HypervisorEvent x6)) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' (HypervisorEvent x6)) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel (HypervisorEvent x6)) (exec_C \<Gamma> handleHypervisorEvent_C) proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) \<lbrace>True\<rbrace> [] (callKernel (HypervisorEvent x6)) handleHypervisorEvent_C proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q158 x6) (?Q'158 x6) [] (callKernel (HypervisorEvent x6)) handleHypervisorEvent_C
 2. \<And>x6 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6; \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_running' s \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ?Q158 x6 s
 3. \<And>x6 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'158 x6 proof (prove)
goal (2 subgoals):
 1. \<And>x6 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6; \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_running' s \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple) s
 2. \<And>x6 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>x6 s. \<lbrakk>no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> ct_running' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (callKernel (HypervisorEvent x6)); e = HypervisorEvent x6; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal:
No subgoals!