theory Ipc_DR

lemma dcorres_handle_fault_reply:
  "dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and  valid_etcbs)
   (corrupt_tcb_intent y)
   (handle_fault_reply a y mi mrs)" unfolding arch_get_sanitise_register_info_def apply (case_tac a) apply (simp_all) apply (rule dummy_corrupt_tcb_intent_corres)+ apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r) apply (rule corres_split[OF corrupt_tcb_intent_as_user_corres corres_trivial[OF corres_free_return]]) apply (wp|clarsimp simp: arch_get_sanitise_register_info_def)+ apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split[OF corrupt_tcb_intent_as_user_corres corres_trivial[OF corres_free_return]]) apply (wp|clarsimp)+ apply (rule dcorres_handle_arch_fault_reply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_fault_reply a y mi mrs) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_fault_reply a y mi mrs) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. a = CapFault x11 x12 x13 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_fault_reply a y mi mrs)
 2. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_fault_reply a y mi mrs)
 3. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_fault_reply a y mi mrs)
 4. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_fault_reply a y mi mrs) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. a = CapFault x11 x12 x13 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (return True)
 2. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) syscallMessage mrs);
return (mi = 0)
od)
 3. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) exceptionMessage mrs);
return (mi = 0)
od)
 4. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (3 subgoals):
 1. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) syscallMessage mrs);
return (mi = 0)
od)
 2. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) exceptionMessage mrs);
return (mi = 0)
od)
 3. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (3 subgoals):
 1. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y >>= return) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) syscallMessage mrs);
return (mi = 0)
od)
 2. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) exceptionMessage mrs);
return (mi = 0)
od)
 3. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (5 subgoals):
 1. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> dcorres dc (?Q5 x2) (?Q'5 x2) (corrupt_tcb_intent y >>= return) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) syscallMessage mrs);
return (mi = 0)
od)
 2. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; True\<rbrakk> \<Longrightarrow> ?Q5 x2 s
 3. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'5 x2 s
 4. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) exceptionMessage mrs);
return (mi = 0)
od)
 5. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (8 subgoals):
 1. \<And>x2 t. a = UnknownSyscallException x2 \<Longrightarrow> dcorres dc (?Q5 x2) (?Q'9 x2 t) (corrupt_tcb_intent y >>= return) (do y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) syscallMessage mrs);
return (mi = 0)
od)
 2. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q'5 x2\<rbrace> arch_get_sanitise_register_info y \<lbrace>?Q'9 x2\<rbrace>
 3. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; ?Q'5 x2 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> arch_get_sanitise_register_info y \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>x2. \<lbrakk>a = UnknownSyscallException x2; False\<rbrakk> \<Longrightarrow> no_fail (?Q'5 x2) (arch_get_sanitise_register_info y)
 5. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; True\<rbrakk> \<Longrightarrow> ?Q5 x2 s
 6. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'5 x2 s
 7. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) exceptionMessage mrs);
return (mi = 0)
od)
 8. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (9 subgoals):
 1. \<And>x2 t. a = UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q20 x2\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>x2 t. a = UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q'14 x2 t\<rbrace> as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) syscallMessage mrs) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> \<lbrace>?Q'5 x2\<rbrace> arch_get_sanitise_register_info y \<lbrace>\<lambda>t. valid_idle and not_idle_thread y and valid_etcbs and ?Q'14 x2 t\<rbrace>
 4. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; ?Q'5 x2 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> arch_get_sanitise_register_info y \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>x2. \<lbrakk>a = UnknownSyscallException x2; False\<rbrakk> \<Longrightarrow> no_fail (?Q'5 x2) (arch_get_sanitise_register_info y)
 6. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q20 x2) s
 7. \<And>x2 s. \<lbrakk>a = UnknownSyscallException x2; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'5 x2 s
 8. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do t <- arch_get_sanitise_register_info y;
y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t r v)) exceptionMessage mrs);
return (mi = 0)
od)
 9. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) exceptionMessage mrs);
return (mi = 0)
od)
 2. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y >>= return) (do y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) exceptionMessage mrs);
return (mi = 0)
od)
 2. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> dcorres dc (?Q45 x31 x32) (?Q'45 x31 x32) (corrupt_tcb_intent y >>= return) (do y <- as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) exceptionMessage mrs);
return (mi = 0)
od)
 2. \<And>x31 x32 s. \<lbrakk>a = UserException x31 x32; True\<rbrakk> \<Longrightarrow> ?Q45 x31 x32 s
 3. \<And>x31 x32 s. \<lbrakk>a = UserException x31 x32; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'45 x31 x32 s
 4. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> \<lbrace>?Q49 x31 x32\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> \<lbrace>?Q'49 x31 x32\<rbrace> as_user y (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) exceptionMessage mrs) \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>x31 x32 s. \<lbrakk>a = UserException x31 x32; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q49 x31 x32) s
 4. \<And>x31 x32 s. \<lbrakk>a = UserException x31 x32; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread y and valid_etcbs and ?Q'49 x31 x32) s
 5. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal (1 subgoal):
 1. \<And>x4. a = ArchFault x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply x4 y mi mrs) proof (prove)
goal:
No subgoals!