theory Ipc_R

lemma handleDoubleFault_corres:
  "corres dc (tcb_at thread)
             (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
             (handle_double_fault thread f ft)
             (handleDoubleFault thread f' ft')" apply (simp add: handle_double_fault_def handleDoubleFault_def) apply (rule corres_guard_imp) apply (subst bind_return [symmetric],
           rule corres_underlying_split [OF setThreadState_corres]) apply simp apply (rule corres_noop2) apply (simp add: exs_valid_def return_def) apply (rule hoare_eq_P) apply wp apply (rule asUser_inv) apply (rule getRestartPC_inv) apply (wp no_fail_getRestartPC)+ apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at thread) (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (handle_double_fault thread f ft) (handleDoubleFault thread f' ft') proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at thread) (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (set_thread_state thread Structures_A.thread_state.Inactive) (do y <- setThreadState Structures_H.thread_state.Inactive thread;
faultPC <- asUser thread getRestartPC;
return ()
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (set_thread_state thread Structures_A.thread_state.Inactive) (do y <- setThreadState Structures_H.thread_state.Inactive thread;
faultPC <- asUser thread getRestartPC;
return ()
od)
 2. \<And>s. tcb_at thread s \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. thread_state_relation Structures_A.thread_state.Inactive Structures_H.thread_state.Inactive
 2. \<And>rv y. dc rv y \<Longrightarrow> corres dc (?Q7 rv) (?Q'7 y) (return rv) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 3. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 4. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 5. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 6. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (5 subgoals):
 1. \<And>rv y. dc rv y \<Longrightarrow> corres dc (?Q7 rv) (?Q'7 y) (return rv) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 2. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 3. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 4. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 5. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (8 subgoals):
 1. \<And>rv y s. \<lbrakk>dc rv y; ?Q7 rv s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> return rv \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>rv y s. \<lbrakk>dc rv y; ?Q'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do faultPC <- asUser thread getRestartPC;
return ()
od \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q7 rv) (return rv)
 4. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q'7 y) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 5. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 6. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 7. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 8. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (7 subgoals):
 1. \<And>rv y s. \<lbrakk>dc rv y; ?Q'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do faultPC <- asUser thread getRestartPC;
return ()
od \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q7 rv) (return rv)
 3. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q'7 y) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 4. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 5. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 6. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 7. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (7 subgoals):
 1. \<And>rv y s P. \<lbrakk>dc rv y; ?Q'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do faultPC <- asUser thread getRestartPC;
return ()
od \<lbrace>\<lambda>r. P\<rbrace>
 2. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q7 rv) (return rv)
 3. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q'7 y) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 4. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 5. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 6. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 7. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (7 subgoals):
 1. \<And>rv y s P. \<lbrakk>dc rv y; ?Q'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>faultPC. P\<rbrace>
 2. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q7 rv) (return rv)
 3. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q'7 y) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 4. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 5. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 6. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 7. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (7 subgoals):
 1. \<And>rv y s P Pa. \<lbrakk>dc rv y; ?Q'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> getRestartPC \<lbrace>\<lambda>faultPC. Pa\<rbrace>
 2. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q7 rv) (return rv)
 3. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q'7 y) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 4. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 5. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 6. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 7. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (6 subgoals):
 1. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q7 rv) (return rv)
 2. \<And>rv y. \<lbrakk>dc rv y; True\<rbrakk> \<Longrightarrow> no_fail (?Q'7 y) (do faultPC <- asUser thread getRestartPC;
return ()
od)
 3. \<lbrace>tcb_at thread\<rbrace> set_thread_state thread Structures_A.thread_state.Inactive \<lbrace>?Q7\<rbrace>
 4. \<lbrace>tcb_at' thread\<rbrace> setThreadState Structures_H.thread_state.Inactive thread \<lbrace>?Q'7\<rbrace>
 5. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 6. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at thread s \<Longrightarrow> tcb_at thread s
 2. \<And>s. (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> tcb_at' thread s proof (prove)
goal:
No subgoals!