theory Ipc_R

lemma makeFaultMessage_corres:
  "corres (=) (tcb_at t) (tcb_at' t)
     (make_fault_msg ft t)
     (makeFaultMessage (fault_map ft) t)" apply (cases ft, simp_all add: makeFaultMessage_def split del: if_split) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF asUser_getRestartPC_corres]) apply (rule corres_trivial, simp add: fromEnum_def enum_bool) apply (wp | simp)+ apply (simp add: ARM_H.syscallMessage_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF asUser_mapM_getRegister_corres]) apply (rule corres_trivial, simp) apply (wp | simp)+ apply (simp add: ARM_H.exceptionMessage_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF asUser_mapM_getRegister_corres]) apply (rule corres_trivial, simp) apply (wp | simp)+ apply (rule makeArchFaultMessage_corres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (make_fault_msg ft t) (makeFaultMessage (fault_map ft) t) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do pc <- as_user t getRestartPC;
return (1, pc # x11 # (if x12 then 1 else 0) # msg_from_lookup_failure x13)
od) (do pc <- asUser t getRestartPC;
return (1, pc # x11 # word_of_nat (fromEnum x12) # msg_from_lookup_failure x13)
od)
 2. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.syscallMessage);
return (2, msg @ [x2])
od)
 3. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 4. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> corres (=) (?Q2 x11 x12 x13) (?Q'2 x11 x12 x13) (do pc <- as_user t getRestartPC;
return (1, pc # x11 # (if x12 then 1 else 0) # msg_from_lookup_failure x13)
od) (do pc <- asUser t getRestartPC;
return (1, pc # x11 # word_of_nat (fromEnum x12) # msg_from_lookup_failure x13)
od)
 2. \<And>x11 x12 x13 s. \<lbrakk>ft = ExceptionTypes_A.fault.CapFault x11 x12 x13; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q2 x11 x12 x13 s
 3. \<And>x11 x12 x13 s. \<lbrakk>ft = ExceptionTypes_A.fault.CapFault x11 x12 x13; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'2 x11 x12 x13 s
 4. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.syscallMessage);
return (2, msg @ [x2])
od)
 5. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 6. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 pc. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> corres (=) (?R6 x11 x12 x13 pc) (?R'6 x11 x12 x13 pc) (return (1, pc # x11 # (if x12 then 1 else 0) # msg_from_lookup_failure x13)) (return (1, pc # x11 # word_of_nat (fromEnum x12) # msg_from_lookup_failure x13))
 2. \<And>x11 x12 x13. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> \<lbrace>?Q6 x11 x12 x13\<rbrace> as_user t getRestartPC \<lbrace>?R6 x11 x12 x13\<rbrace>
 3. \<And>x11 x12 x13. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> \<lbrace>?Q'6 x11 x12 x13\<rbrace> asUser t getRestartPC \<lbrace>?R'6 x11 x12 x13\<rbrace>
 4. \<And>x11 x12 x13 s. \<lbrakk>ft = ExceptionTypes_A.fault.CapFault x11 x12 x13; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q6 x11 x12 x13) s
 5. \<And>x11 x12 x13 s. \<lbrakk>ft = ExceptionTypes_A.fault.CapFault x11 x12 x13; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'6 x11 x12 x13) s
 6. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.syscallMessage);
return (2, msg @ [x2])
od)
 7. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 8. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> \<lbrace>?Q6 x11 x12 x13\<rbrace> as_user t getRestartPC \<lbrace>\<lambda>pc _. True\<rbrace>
 2. \<And>x11 x12 x13. ft = ExceptionTypes_A.fault.CapFault x11 x12 x13 \<Longrightarrow> \<lbrace>?Q'6 x11 x12 x13\<rbrace> asUser t getRestartPC \<lbrace>\<lambda>pc _. True\<rbrace>
 3. \<And>x11 x12 x13 s. \<lbrakk>ft = ExceptionTypes_A.fault.CapFault x11 x12 x13; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q6 x11 x12 x13) s
 4. \<And>x11 x12 x13 s. \<lbrakk>ft = ExceptionTypes_A.fault.CapFault x11 x12 x13; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'6 x11 x12 x13) s
 5. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.syscallMessage);
return (2, msg @ [x2])
od)
 6. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 7. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (3 subgoals):
 1. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.syscallMessage);
return (2, msg @ [x2])
od)
 2. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 3. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (3 subgoals):
 1. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od)
 2. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 3. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (5 subgoals):
 1. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (?Q24 x2) (?Q'24 x2) (do msg <- as_user t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od) (do msg <- asUser t (mapM getRegister MachineExports.syscallMessage);
return (2, msg @ [x2])
od)
 2. \<And>x2 s. \<lbrakk>ft = ExceptionTypes_A.fault.UnknownSyscallException x2; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q24 x2 s
 3. \<And>x2 s. \<lbrakk>ft = ExceptionTypes_A.fault.UnknownSyscallException x2; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'24 x2 s
 4. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 5. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (7 subgoals):
 1. \<And>x2 msg. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> corres (=) (?R28 x2 msg) (?R'28 x2 msg) (return (2, msg @ [x2])) (return (2, msg @ [x2]))
 2. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q28 x2\<rbrace> as_user t (mapM getRegister MachineExports.syscallMessage) \<lbrace>?R28 x2\<rbrace>
 3. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q'28 x2\<rbrace> asUser t (mapM getRegister MachineExports.syscallMessage) \<lbrace>?R'28 x2\<rbrace>
 4. \<And>x2 s. \<lbrakk>ft = ExceptionTypes_A.fault.UnknownSyscallException x2; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q28 x2) s
 5. \<And>x2 s. \<lbrakk>ft = ExceptionTypes_A.fault.UnknownSyscallException x2; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'28 x2) s
 6. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 7. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (6 subgoals):
 1. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q28 x2\<rbrace> as_user t (mapM getRegister MachineExports.syscallMessage) \<lbrace>\<lambda>msg _. True\<rbrace>
 2. \<And>x2. ft = ExceptionTypes_A.fault.UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q'28 x2\<rbrace> asUser t (mapM getRegister MachineExports.syscallMessage) \<lbrace>\<lambda>msg _. True\<rbrace>
 3. \<And>x2 s. \<lbrakk>ft = ExceptionTypes_A.fault.UnknownSyscallException x2; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q28 x2) s
 4. \<And>x2 s. \<lbrakk>ft = ExceptionTypes_A.fault.UnknownSyscallException x2; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'28 x2) s
 5. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 6. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 2. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 2. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (?Q45 x31 x32) (?Q'45 x31 x32) (do msg <- as_user t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od) (do msg <- asUser t (mapM getRegister MachineExports.exceptionMessage);
return (3, msg @ [x31, x32])
od)
 2. \<And>x31 x32 s. \<lbrakk>ft = ExceptionTypes_A.fault.UserException x31 x32; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q45 x31 x32 s
 3. \<And>x31 x32 s. \<lbrakk>ft = ExceptionTypes_A.fault.UserException x31 x32; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'45 x31 x32 s
 4. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 msg. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> corres (=) (?R49 x31 x32 msg) (?R'49 x31 x32 msg) (return (3, msg @ [x31, x32])) (return (3, msg @ [x31, x32]))
 2. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> \<lbrace>?Q49 x31 x32\<rbrace> as_user t (mapM getRegister MachineExports.exceptionMessage) \<lbrace>?R49 x31 x32\<rbrace>
 3. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> \<lbrace>?Q'49 x31 x32\<rbrace> asUser t (mapM getRegister MachineExports.exceptionMessage) \<lbrace>?R'49 x31 x32\<rbrace>
 4. \<And>x31 x32 s. \<lbrakk>ft = ExceptionTypes_A.fault.UserException x31 x32; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q49 x31 x32) s
 5. \<And>x31 x32 s. \<lbrakk>ft = ExceptionTypes_A.fault.UserException x31 x32; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'49 x31 x32) s
 6. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> \<lbrace>?Q49 x31 x32\<rbrace> as_user t (mapM getRegister MachineExports.exceptionMessage) \<lbrace>\<lambda>msg _. True\<rbrace>
 2. \<And>x31 x32. ft = ExceptionTypes_A.fault.UserException x31 x32 \<Longrightarrow> \<lbrace>?Q'49 x31 x32\<rbrace> asUser t (mapM getRegister MachineExports.exceptionMessage) \<lbrace>\<lambda>msg _. True\<rbrace>
 3. \<And>x31 x32 s. \<lbrakk>ft = ExceptionTypes_A.fault.UserException x31 x32; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q49 x31 x32) s
 4. \<And>x31 x32 s. \<lbrakk>ft = ExceptionTypes_A.fault.UserException x31 x32; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'49 x31 x32) s
 5. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal (1 subgoal):
 1. \<And>x4. ft = ExceptionTypes_A.fault.ArchFault x4 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg x4 t) (makeArchFaultMessage (arch_fault_map x4) t) proof (prove)
goal:
No subgoals!