theory VSpace_R

lemma handleVMFault_corres:
  "corres (fr \<oplus> dc) (tcb_at thread) (tcb_at' thread)
          (handle_vm_fault thread fault) (handleVMFault thread fault)" apply (simp add: ARM_H.handleVMFault_def) apply corres_cases apply simp apply (rule corres_splitEE) apply simp apply (rule corres_machine_op [where r="(=)"]) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_getFAR) apply (rule corres_splitEE) apply simp apply (rule corres_machine_op [where r="(=)"]) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_getDFSR) apply (rule corres_trivial, simp add: arch_fault_map_def) apply wpsimp+ apply (rule corres_splitEE) apply simp apply (rule asUser_corres') apply (rule corres_no_failI [where R="(=)"]) apply (rule no_fail_getRestartPC) apply fastforce apply (rule corres_splitEE) apply simp apply (rule corres_machine_op [where r="(=)"]) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_getIFSR) apply (rule corres_trivial, simp add: arch_fault_map_def) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (fr \<oplus> dc) (tcb_at thread) (tcb_at' thread) (handle_vm_fault thread fault) (handleVMFault thread fault) proof (prove)
goal (1 subgoal):
 1. corres (fr \<oplus> dc) (tcb_at thread) (tcb_at' thread) (handle_vm_fault thread fault) (case fault of 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 | 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) proof (prove)
goal (4 subgoals):
 1. fault = ARMDataAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'23 ?Q23 (handle_vm_fault thread fault) (doE addr <- withoutFailure $ doMachineOp getFAR;
fault <- withoutFailure $ doMachineOp getDFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault addr [0, fault && mask 14]
odE)
 2. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 3. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ?Q'23 s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 4. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ?Q23 s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (4 subgoals):
 1. fault = ARMDataAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'23 ?Q23 (doE addr <- liftE (do_machine_op getFAR);
fault <- liftE (do_machine_op getDFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, fault && mask 14]))
odE) (doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE)
 2. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 3. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ?Q'23 s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 4. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ?Q23 s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (7 subgoals):
 1. fault = ARMDataAbort \<Longrightarrow> corres (fr \<oplus> ?r'38) ?P38 ?P'38 (liftE (do_machine_op getFAR)) (liftE (doMachineOp getFAR))
 2. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; ?r'38 addr addra\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R38 addr) (?R'38 addra) (doE fault <- liftE (do_machine_op getDFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, fault && mask 14]))
odE)
 3. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?R38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>?R'38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> (?P38 and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> (?P'38 and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (7 subgoals):
 1. fault = ARMDataAbort \<Longrightarrow> corres ?r'38 ?P38 ?P'38 (do_machine_op getFAR) (doMachineOp getFAR)
 2. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; ?r'38 addr addra\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R38 addr) (?R'38 addra) (doE fault <- liftE (do_machine_op getDFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, fault && mask 14]))
odE)
 3. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?R38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>?R'38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> (?P38 and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> (?P'38 and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (7 subgoals):
 1. fault = ARMDataAbort \<Longrightarrow> corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) getFAR getFAR
 2. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R38 addr) (?R'38 addra) (doE fault <- liftE (do_machine_op getDFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, fault && mask 14]))
odE)
 3. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?R38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>?R'38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (7 subgoals):
 1. \<lbrakk>fault = ARMDataAbort; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) getFAR
 2. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R38 addr) (?R'38 addra) (doE fault <- liftE (do_machine_op getDFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, fault && mask 14]))
odE)
 3. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?R38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>?R'38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (6 subgoals):
 1. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R38 addr) (?R'38 addra) (doE fault <- liftE (do_machine_op getDFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, fault && mask 14]))
odE)
 2. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?R38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>?R'38\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (9 subgoals):
 1. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> corres (fr \<oplus> ?r'50 addr addra) (?P51 addr) (?P'53 addra) (liftE (do_machine_op getDFSR)) (liftE (doMachineOp getDFSR))
 2. \<And>addr addra faulta faultaa. \<lbrakk>fault = ARMDataAbort; addr = addra; ?r'50 addr addra faulta faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R50 addr addra faulta) (?R'50 addr addra faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, faultaa && mask 14])))
 3. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 addr\<rbrace> liftE (do_machine_op getDFSR) \<lbrace>?R50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 addra\<rbrace> liftE (doMachineOp getDFSR) \<lbrace>?R'50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>\<lambda>addr. ?P51 addr and ?Q52 addr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>\<lambda>addra. ?P'53 addra and ?Q'54 addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 9. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (9 subgoals):
 1. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> corres (?r'50 addra addra) (?P51 addra) (?P'53 addra) (do_machine_op getDFSR) (doMachineOp getDFSR)
 2. \<And>addr addra faulta faultaa. \<lbrakk>fault = ARMDataAbort; addr = addra; ?r'50 addr addra faulta faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R50 addr addra faulta) (?R'50 addr addra faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, faultaa && mask 14])))
 3. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 addr\<rbrace> liftE (do_machine_op getDFSR) \<lbrace>?R50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 addra\<rbrace> liftE (doMachineOp getDFSR) \<lbrace>?R'50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>\<lambda>addr. ?P51 addr and ?Q52 addr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>\<lambda>addra. ?P'53 addra and ?Q'54 addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 9. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (9 subgoals):
 1. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) getDFSR getDFSR
 2. \<And>addr addra faulta faultaa. \<lbrakk>fault = ARMDataAbort; addr = addra; faulta = faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R50 addr addra faulta) (?R'50 addr addra faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, faultaa && mask 14])))
 3. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 addr\<rbrace> liftE (do_machine_op getDFSR) \<lbrace>?R50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 addra\<rbrace> liftE (doMachineOp getDFSR) \<lbrace>?R'50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>\<lambda>addr. (\<lambda>a. True) and ?Q52 addr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>\<lambda>addra. (\<lambda>a. True) and ?Q'54 addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 9. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (9 subgoals):
 1. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) getDFSR
 2. \<And>addr addra faulta faultaa. \<lbrakk>fault = ARMDataAbort; addr = addra; faulta = faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R50 addr addra faulta) (?R'50 addr addra faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, faultaa && mask 14])))
 3. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 addr\<rbrace> liftE (do_machine_op getDFSR) \<lbrace>?R50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 addra\<rbrace> liftE (doMachineOp getDFSR) \<lbrace>?R'50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>\<lambda>addr. (\<lambda>a. True) and ?Q52 addr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>\<lambda>addra. (\<lambda>a. True) and ?Q'54 addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 9. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (8 subgoals):
 1. \<And>addr addra faulta faultaa. \<lbrakk>fault = ARMDataAbort; addr = addra; faulta = faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R50 addr addra faulta) (?R'50 addr addra faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault addr [0, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addra [0, faultaa && mask 14])))
 2. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 addr\<rbrace> liftE (do_machine_op getDFSR) \<lbrace>?R50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 addra\<rbrace> liftE (doMachineOp getDFSR) \<lbrace>?R'50 addr addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>\<lambda>addr. (\<lambda>a. True) and ?Q52 addr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>\<lambda>addra. (\<lambda>a. True) and ?Q'54 addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (7 subgoals):
 1. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 addr\<rbrace> liftE (do_machine_op getDFSR) \<lbrace>\<lambda>fault _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>addr addra. \<lbrakk>fault = ARMDataAbort; addr = addra\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 addra\<rbrace> liftE (doMachineOp getDFSR) \<lbrace>\<lambda>faulta _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q38\<rbrace> liftE (do_machine_op getFAR) \<lbrace>\<lambda>addr. (\<lambda>a. True) and ?Q52 addr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMDataAbort \<Longrightarrow> \<lbrace>?Q'38\<rbrace> liftE (doMachineOp getFAR) \<lbrace>\<lambda>addra. (\<lambda>a. True) and ?Q'54 addra\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (handle_vm_fault thread fault) (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)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q38) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and ?Q'38) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (3 subgoals):
 1. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> dc) ?Q'15 ?Q15 (doE pc <- liftE (as_user thread getRestartPC);
fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE pc <- liftE (asUser thread getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE)
 2. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q'15 s)
 3. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> ?Q15 s') proof (prove)
goal (6 subgoals):
 1. fault = ARMPrefetchAbort \<Longrightarrow> corres (fr \<oplus> ?r'104) ?P104 ?P'104 (liftE (as_user thread getRestartPC)) (liftE (asUser thread getRestartPC))
 2. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; ?r'104 pc pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R104 pc) (?R'104 pca) (doE fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, fault && mask 14]))
odE)
 3. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?R104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>?R'104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (?P104 and ?Q104) s)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (?P'104 and ?Q'104) s') proof (prove)
goal (6 subgoals):
 1. fault = ARMPrefetchAbort \<Longrightarrow> corres ?r'104 ?P104 ?P'104 (as_user thread getRestartPC) (asUser thread getRestartPC)
 2. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; ?r'104 pc pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R104 pc) (?R'104 pca) (doE fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, fault && mask 14]))
odE)
 3. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?R104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>?R'104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (?P104 and ?Q104) s)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (?P'104 and ?Q'104) s') proof (prove)
goal (6 subgoals):
 1. fault = ARMPrefetchAbort \<Longrightarrow> corres_underlying Id False True ?r'104 (\<lambda>_. True) (\<lambda>_. True) getRestartPC getRestartPC
 2. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; ?r'104 pc pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R104 pc) (?R'104 pca) (doE fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, fault && mask 14]))
odE)
 3. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?R104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>?R'104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (7 subgoals):
 1. \<lbrakk>fault = ARMPrefetchAbort; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) getRestartPC
 2. fault = ARMPrefetchAbort \<Longrightarrow> \<forall>(s, s')\<in>Id. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (getRestartPC s'). \<exists>(r, t)\<in>fst (getRestartPC s). (t, t') \<in> Id \<and> r = r')
 3. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R104 pc) (?R'104 pca) (doE fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, fault && mask 14]))
odE)
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?R104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>?R'104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (6 subgoals):
 1. fault = ARMPrefetchAbort \<Longrightarrow> \<forall>(s, s')\<in>Id. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (getRestartPC s'). \<exists>(r, t)\<in>fst (getRestartPC s). (t, t') \<in> Id \<and> r = r')
 2. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R104 pc) (?R'104 pca) (doE fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, fault && mask 14]))
odE)
 3. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?R104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>?R'104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (5 subgoals):
 1. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R104 pc) (?R'104 pca) (doE fault <- liftE (do_machine_op getIFSR);
throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, fault && mask 14]))
odE) (doE fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, fault && mask 14]))
odE)
 2. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?R104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>?R'104\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (8 subgoals):
 1. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> corres (fr \<oplus> ?r'153 pc pca) (?P154 pc) (?P'156 pca) (liftE (do_machine_op getIFSR)) (liftE (doMachineOp getIFSR))
 2. \<And>pc pca faulta faultaa. \<lbrakk>fault = ARMPrefetchAbort; pc = pca; ?r'153 pc pca faulta faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R153 pc pca faulta) (?R'153 pc pca faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, faultaa && mask 14])))
 3. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q155 pc\<rbrace> liftE (do_machine_op getIFSR) \<lbrace>?R153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 pca\<rbrace> liftE (doMachineOp getIFSR) \<lbrace>?R'153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>\<lambda>pc. ?P154 pc and ?Q155 pc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>\<lambda>pca. ?P'156 pca and ?Q'157 pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (8 subgoals):
 1. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> corres (?r'153 pca pca) (?P154 pca) (?P'156 pca) (do_machine_op getIFSR) (doMachineOp getIFSR)
 2. \<And>pc pca faulta faultaa. \<lbrakk>fault = ARMPrefetchAbort; pc = pca; ?r'153 pc pca faulta faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R153 pc pca faulta) (?R'153 pc pca faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, faultaa && mask 14])))
 3. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q155 pc\<rbrace> liftE (do_machine_op getIFSR) \<lbrace>?R153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 pca\<rbrace> liftE (doMachineOp getIFSR) \<lbrace>?R'153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>\<lambda>pc. ?P154 pc and ?Q155 pc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>\<lambda>pca. ?P'156 pca and ?Q'157 pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (8 subgoals):
 1. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) getIFSR getIFSR
 2. \<And>pc pca faulta faultaa. \<lbrakk>fault = ARMPrefetchAbort; pc = pca; faulta = faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R153 pc pca faulta) (?R'153 pc pca faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, faultaa && mask 14])))
 3. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q155 pc\<rbrace> liftE (do_machine_op getIFSR) \<lbrace>?R153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 pca\<rbrace> liftE (doMachineOp getIFSR) \<lbrace>?R'153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>\<lambda>pc. (\<lambda>a. True) and ?Q155 pc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>\<lambda>pca. (\<lambda>a. True) and ?Q'157 pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (8 subgoals):
 1. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) getIFSR
 2. \<And>pc pca faulta faultaa. \<lbrakk>fault = ARMPrefetchAbort; pc = pca; faulta = faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R153 pc pca faulta) (?R'153 pc pca faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, faultaa && mask 14])))
 3. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q155 pc\<rbrace> liftE (do_machine_op getIFSR) \<lbrace>?R153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 pca\<rbrace> liftE (doMachineOp getIFSR) \<lbrace>?R'153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>\<lambda>pc. (\<lambda>a. True) and ?Q155 pc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>\<lambda>pca. (\<lambda>a. True) and ?Q'157 pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 8. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (7 subgoals):
 1. \<And>pc pca faulta faultaa. \<lbrakk>fault = ARMPrefetchAbort; pc = pca; faulta = faultaa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R153 pc pca faulta) (?R'153 pc pca faultaa) (throwError (ExceptionTypes_A.fault.ArchFault (ARM_A.VMFault pc [1, faulta && mask 14]))) (throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pca [1, faultaa && mask 14])))
 2. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q155 pc\<rbrace> liftE (do_machine_op getIFSR) \<lbrace>?R153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 pca\<rbrace> liftE (doMachineOp getIFSR) \<lbrace>?R'153 pc pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>\<lambda>pc. (\<lambda>a. True) and ?Q155 pc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>\<lambda>pca. (\<lambda>a. True) and ?Q'157 pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 7. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal (6 subgoals):
 1. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q155 pc\<rbrace> liftE (do_machine_op getIFSR) \<lbrace>\<lambda>fault _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>pc pca. \<lbrakk>fault = ARMPrefetchAbort; pc = pca\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 pca\<rbrace> liftE (doMachineOp getIFSR) \<lbrace>\<lambda>faulta _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q104\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>\<lambda>pc. (\<lambda>a. True) and ?Q155 pc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q'104\<rbrace> liftE (asUser thread getRestartPC) \<lbrace>\<lambda>pca. (\<lambda>a. True) and ?Q'157 pca\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s) \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at thread and ?Q104) s)
 6. \<And>s s'. \<lbrakk>tcb_at thread s; tcb_at' thread s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (fault = ARMDataAbort \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s') \<and> (fault = ARMPrefetchAbort \<longrightarrow> (tcb_at' thread and ?Q'104) s') proof (prove)
goal:
No subgoals!