theory VSpace_C

lemma handleVMFault_ccorres:
  "ccorres ((\<lambda>a ex v. ex = scast EXCEPTION_FAULT \<and> (\<exists>vf.
                      a = ArchFault (VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and>
                      errfault v = Some (SeL4_Fault_VMFault vf))) \<currency>
           (\<lambda>_. \<bottom>))
           (liftxf errstate id (K ()) ret__unsigned_long_')
           \<top>
           (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_fault_type_from_H vm_fault\<rbrace>)
          []
           (handleVMFault thread vm_fault)
           (Call handleVMFault_'proc)" apply (cinit lift: vm_faultType_') apply wpc apply (simp add: vm_fault_type_from_H_def Kernel_C.ARMDataAbort_def Kernel_C.ARMPrefetchAbort_def) apply (simp add: ccorres_cond_univ_iff) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply (ctac (no_vcg) add: getFAR_ccorres pre: ccorres_liftE_Seq) apply (ctac (no_vcg) add: getDFSR_ccorres pre: ccorres_liftE_Seq) apply clarsimp apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (clarsimp simp add: throwError_def throw_def return_def) apply (rule conseqPre) apply vcg apply (clarsimp simp: errstate_def) apply (clarsimp simp: EXCEPTION_FAULT_def EXCEPTION_NONE_def) apply (simp add: seL4_Fault_VMFault_lift) apply wp+ apply (simp add: vm_fault_type_from_H_def Kernel_C.ARMDataAbort_def Kernel_C.ARMPrefetchAbort_def) apply (simp add: ccorres_cond_univ_iff ccorres_cond_empty_iff) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply (ctac (no_vcg) pre: ccorres_liftE_Seq) apply (ctac (no_vcg) add: getIFSR_ccorres pre: ccorres_liftE_Seq) apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (clarsimp simp add: throwError_def throw_def return_def) apply (rule conseqPre) apply vcg apply (clarsimp simp: errstate_def) apply (clarsimp simp: EXCEPTION_FAULT_def EXCEPTION_NONE_def) apply (simp add: seL4_Fault_VMFault_lift) apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_fault_type_from_H vm_fault\<rbrace>) [] (handleVMFault thread vm_fault) (Call handleVMFault_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>vm_faultType. vm_faultType = vm_fault_type_from_H vm_fault \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q571 vm_faultType) (?Q'571 vm_faultType) [SKIP] (case vm_fault of vmfault_type.ARMDataAbort \<Rightarrow> doE addr <- withoutFailure $ doMachineOp getFAR;
fault <- withoutFailure $ doMachineOp getDFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault addr [0, fault && mask 14]
odE | vmfault_type.ARMPrefetchAbort \<Rightarrow> doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ?Q571 vm_faultType s \<and> s' \<in> ?Q'571 vm_faultType proof (prove)
goal (3 subgoals):
 1. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMDataAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R582 vm_faultType) (?R''582 vm_faultType) [SKIP] (doE addr <- withoutFailure $ doMachineOp getFAR;
fault <- withoutFailure $ doMachineOp getDFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault addr [0, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 2. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ?R582 vm_faultType s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> ?R''582 vm_faultType} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (3 subgoals):
 1. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R582 0) (?R''582 0) [SKIP] (doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE) (Cond UNIV (lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)) (Cond {} (lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc();;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)) (Guard DontReach {} SKIP)))
 2. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ?R582 vm_faultType s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> ?R''582 vm_faultType} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (3 subgoals):
 1. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R582 0) (?R''582 0) [SKIP] (doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE) (lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))
 2. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ?R582 vm_faultType s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> ?R''582 vm_faultType} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (3 subgoals):
 1. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R582 0) (?R''582 0) [SKIP] (doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE) (lvar_nondet_init addr_' addr_'_update;;
(lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
(\<acute>addr :== CALL getFAR_'proc();;
(\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))))))
 2. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ?R582 vm_faultType s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> ?R''582 vm_faultType} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (3 subgoals):
 1. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R582 0) (?G'606 0) [SKIP] (doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE) (lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
(\<acute>addr :== CALL getFAR_'proc();;
(\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)))))
 2. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ?R582 vm_faultType s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> ?G'606 vm_faultType}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (3 subgoals):
 1. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R582 0) (?G'619 0) [SKIP] (doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE) (\<acute>addr :== CALL getFAR_'proc();;
(\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))))
 2. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ?R582 vm_faultType s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> ?G'619 vm_faultType}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (4 subgoals):
 1. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q631 rv) (?Q'631 rv addr) [SKIP] (doE fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault rv [0, fault && mask 14]))
odE) (\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)))
 2. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>?Q631\<rbrace>
 3. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'637 vm_faultType t rv}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType}
flex-flex pairs:
?Q'637 0 \<equiv>\<^sup>? \<lambda>t rv. ?Q'631 rv (ret__unsigned_long_' t) proof (prove)
goal (5 subgoals):
 1. \<And>rv addr rva fault___unsigned_long. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr; rva = fault___unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q749 rv addr rva) (?Q'749 rv addr rva fault___unsigned_long) [SKIP] (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault rv [0, rva && mask 14]))) (\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(addr,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>?Q749 rv addr\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. rva = ret__unsigned_long_' ta \<longrightarrow> s'\<lparr>globals := globals ta, fault___unsigned_long_' := ret__unsigned_long_' ta\<rparr> \<in> ?Q'759 vm_faultType t rv ta rva}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType}
flex-flex pairs:
?Q'759 0 \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'749 rv (ret__unsigned_long_' t) rva (ret__unsigned_long_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>addr fault___unsigned_long. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q749 addr addr fault___unsigned_long) (?Q'749 addr addr fault___unsigned_long fault___unsigned_long) [SKIP] (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault___unsigned_long && mask 14]))) (\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(addr,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>?Q749 rv addr\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. rva = ret__unsigned_long_' ta \<longrightarrow> s'\<lparr>globals := globals ta, fault___unsigned_long_' := ret__unsigned_long_' ta\<rparr> \<in> ?Q'759 vm_faultType t rv ta rva}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType}
flex-flex pairs:
?Q'759 0 \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'749 rv (ret__unsigned_long_' t) rva (ret__unsigned_long_' ta) proof (prove)
goal (5 subgoals):
 1. \<And>addr fault___unsigned_long. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(addr,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) {},{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault___unsigned_long && mask 14])) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (5 subgoals):
 1. \<And>addr fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} \<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(addr,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) {},{s. (\<sigma>, s) \<in> rf_sr \<and> ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ret__unsigned_long_' s = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. addr = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 0 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (current_fault_' (globals s)) = Some (SeL4_Fault_VMFault vf))}
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (6 subgoals):
 1. \<And>addr fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<Gamma>\<turnstile> (?P'842 addr fault___unsigned_long \<sigma>) \<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(addr,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) {},{s. (\<sigma>, s) \<in> rf_sr \<and> ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ret__unsigned_long_' s = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. addr = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 0 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (current_fault_' (globals s)) = Some (SeL4_Fault_VMFault vf))}
 2. \<And>addr fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'842 addr fault___unsigned_long \<sigma>
 3. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 4. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 5. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 6. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (5 subgoals):
 1. \<And>addr fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>t. seL4_Fault_VMFault_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>seL4_Fault_VMFault_CL.address_CL = addr && mask 32, FSR_CL = fault___unsigned_long && mask 14, instructionFault_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<longrightarrow> (\<sigma>, globals_update (current_fault_'_update (\<lambda>_. ret__struct_seL4_Fault_C_' t)) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> (\<exists>vf. addr = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 0 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_VMFault vf))}
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (5 subgoals):
 1. \<And>addr fault___unsigned_long \<sigma> x t. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; (\<sigma>, x) \<in> rf_sr; seL4_Fault_VMFault_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>seL4_Fault_VMFault_CL.address_CL = addr, FSR_CL = fault___unsigned_long && mask 14, instructionFault_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault\<rbrakk> \<Longrightarrow> EXCEPTION_FAULT \<noteq> EXCEPTION_NONE \<and> (\<exists>vf. addr = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 0 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_VMFault vf))
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (5 subgoals):
 1. \<And>addr fault___unsigned_long \<sigma> x t. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; (\<sigma>, x) \<in> rf_sr; seL4_Fault_VMFault_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>seL4_Fault_VMFault_CL.address_CL = addr, FSR_CL = fault___unsigned_long && mask 14, instructionFault_CL = SCAST(32 signed \<rightarrow> 32) false\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault\<rbrakk> \<Longrightarrow> \<exists>vf. addr = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 0 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_VMFault vf)
 2. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 4. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (4 subgoals):
 1. \<And>rv addr. \<lbrakk>vm_fault = vmfault_type.ARMDataAbort; rv = addr\<rbrakk> \<Longrightarrow> \<lbrace>?R756 rv\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>a b. True\<rbrace>
 2. vm_fault = vmfault_type.ARMDataAbort \<Longrightarrow> \<lbrace>?R640 0\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R756 a\<rbrace>
 3. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and ?R640 vm_faultType) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (2 subgoals):
 1. \<And>vm_faultType. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; vm_fault = vmfault_type.ARMPrefetchAbort\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 vm_faultType) (?R''581 vm_faultType) [SKIP] (doE pc <- withoutFailure $ asUser thread $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE) (IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMDataAbort THEN
  lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>addr,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  IF vm_faultType = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMPrefetchAbort THEN
  lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>thread);;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>pc,UCAST(32 \<rightarrow> 32) \<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (2 subgoals):
 1. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 1) (?R''581 1) [SKIP] (doE pc <- liftE (asUser thread getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE) (Cond {} (lvar_nondet_init addr_' addr_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>addr :== CALL getFAR_'proc();;
\<acute>fault___unsigned_long :== CALL getDFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>addr,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) false);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)) (Cond UNIV (lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc();;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)) (Guard DontReach {} SKIP)))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (2 subgoals):
 1. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 1) (?R''581 1) [SKIP] (doE pc <- liftE (asUser thread getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE) (lvar_nondet_init pc_' pc_'_update;;
lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
\<acute>pc :== CALL getRestartPC_'proc();;
\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (2 subgoals):
 1. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 1) (?R''581 1) [SKIP] (doE pc <- liftE (asUser thread getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE) (lvar_nondet_init pc_' pc_'_update;;
(lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
(\<acute>pc :== CALL getRestartPC_'proc();;
(\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> ?R''581 vm_faultType} proof (prove)
goal (2 subgoals):
 1. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 1) (?G'892 1) [SKIP] (doE pc <- liftE (asUser thread getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE) (lvar_nondet_init fault___unsigned_long_' fault___unsigned_long_'_update;;
(\<acute>pc :== CALL getRestartPC_'proc();;
(\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> ?G'892 vm_faultType}} proof (prove)
goal (2 subgoals):
 1. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?R581 1) (?G'905 1) [SKIP] (doE pc <- liftE (asUser thread getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE) (\<acute>pc :== CALL getRestartPC_'proc();;
(\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(\<acute>pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))))
 2. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ?R581 vm_faultType s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> ?G'905 vm_faultType}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q918 rv) (?Q'918 rv pc) [SKIP] (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault rv [1, fault && mask 14]))
odE) (\<acute>fault___unsigned_long :== CALL getIFSR_'proc();;
(\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(pc,\<acute>fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT)))
 2. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>?Q918\<rbrace>
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'925 vm_faultType t rv}}}}
flex-flex pairs:
?Q'925 1 \<equiv>\<^sup>? \<lambda>t rv. ?Q'918 rv (ret__unsigned_long_' t) proof (prove)
goal (4 subgoals):
 1. \<And>rv pc rva fault___unsigned_long. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc; rva = fault___unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1038 rv pc rva) (?Q'1038 rv pc rva fault___unsigned_long) [SKIP] (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault rv [1, rva && mask 14]))) (\<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(pc,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT))
 2. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>?Q1038 rv pc\<rbrace>
 3. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. rva = ret__unsigned_long_' ta \<longrightarrow> s'\<lparr>globals := globals ta, fault___unsigned_long_' := ret__unsigned_long_' ta\<rparr> \<in> ?Q'1048 vm_faultType t rv ta rva}}}}}
flex-flex pairs:
?Q'1048 1 \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'1038 rv (ret__unsigned_long_' t) rva (ret__unsigned_long_' ta) proof (prove)
goal (4 subgoals):
 1. \<And>rv pc rva fault___unsigned_long. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc; rva = fault___unsigned_long\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(pc,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) {},{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault rv [1, rva && mask 14])) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((\<lambda>a ex v. ex = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. a = Fault_H.fault.ArchFault (ARM_H.VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> (\<lambda>_ _. False)) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (4 subgoals):
 1. \<And>pc fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} \<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(pc,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) {},{s. (\<sigma>, s) \<in> rf_sr \<and> ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ret__unsigned_long_' s = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. pc = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 1 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (current_fault_' (globals s)) = Some (SeL4_Fault_VMFault vf))}
 2. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (5 subgoals):
 1. \<And>pc fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<Gamma>\<turnstile> (?P'1129 pc fault___unsigned_long \<sigma>) \<acute>current_fault :== CALL seL4_Fault_VMFault_new_'proc(pc,fault___unsigned_long,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT) {},{s. (\<sigma>, s) \<in> rf_sr \<and> ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ret__unsigned_long_' s = SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<and> (\<exists>vf. pc = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 1 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (current_fault_' (globals s)) = Some (SeL4_Fault_VMFault vf))}
 2. \<And>pc fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'1129 pc fault___unsigned_long \<sigma>
 3. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 4. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 5. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (4 subgoals):
 1. \<And>pc fault___unsigned_long \<sigma>. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>t. seL4_Fault_VMFault_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>seL4_Fault_VMFault_CL.address_CL = pc && mask 32, FSR_CL = fault___unsigned_long && mask 14, instructionFault_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1\<rparr> \<and> seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<longrightarrow> (\<sigma>, globals_update (current_fault_'_update (\<lambda>_. ret__struct_seL4_Fault_C_' t)) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> SCAST(32 signed \<rightarrow> 32) EXCEPTION_FAULT \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> (\<exists>vf. pc = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 1 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_VMFault vf))}
 2. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (4 subgoals):
 1. \<And>pc fault___unsigned_long \<sigma> x t. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; (\<sigma>, x) \<in> rf_sr; seL4_Fault_VMFault_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>seL4_Fault_VMFault_CL.address_CL = pc, FSR_CL = fault___unsigned_long && mask 14, instructionFault_CL = SCAST(32 signed \<rightarrow> 32) true\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault\<rbrakk> \<Longrightarrow> EXCEPTION_FAULT \<noteq> EXCEPTION_NONE \<and> (\<exists>vf. pc = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 1 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_VMFault vf))
 2. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (4 subgoals):
 1. \<And>pc fault___unsigned_long \<sigma> x t. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; (\<sigma>, x) \<in> rf_sr; seL4_Fault_VMFault_lift (ret__struct_seL4_Fault_C_' t) = \<lparr>seL4_Fault_VMFault_CL.address_CL = pc, FSR_CL = fault___unsigned_long && mask 14, instructionFault_CL = SCAST(32 signed \<rightarrow> 32) true\<rparr>; seL4_Fault_get_tag (ret__struct_seL4_Fault_C_' t) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault\<rbrakk> \<Longrightarrow> \<exists>vf. pc = seL4_Fault_VMFault_CL.address_CL vf \<and> instructionFault_CL vf = 1 \<and> fault___unsigned_long && mask 14 = FSR_CL vf \<and> seL4_Fault_lift (ret__struct_seL4_Fault_C_' t) = Some (SeL4_Fault_VMFault vf)
 2. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 3. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 4. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv pc. \<lbrakk>vm_fault = vmfault_type.ARMPrefetchAbort; rv = pc\<rbrakk> \<Longrightarrow> \<lbrace>?R1045 rv\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>a b. True\<rbrace>
 2. vm_fault = vmfault_type.ARMPrefetchAbort \<Longrightarrow> \<lbrace>?R928 1\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1045 a\<rbrace>
 3. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and ?R928 vm_faultType) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal (1 subgoal):
 1. \<And>vm_faultType s s'. \<lbrakk>vm_faultType = vm_fault_type_from_H vm_fault; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s) \<and> (vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> True)) s)) \<and> s' \<in> {s. vm_fault = vmfault_type.ARMDataAbort \<longrightarrow> s \<in> {s. \<forall>v. addr_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> addr_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} \<inter> {s. vm_fault = vmfault_type.ARMPrefetchAbort \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. \<forall>v. s\<lparr>fault___unsigned_long_' := v\<rparr> \<in> {s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> pc_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, fault___unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}}}} proof (prove)
goal:
No subgoals!