theory Syscall_C

lemma handleDoubleFault_ccorres:
  "ccorres dc xfdc (invs' and  tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and
        sch_act_not tptr and (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p)))
      (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr})
      [] (handleDoubleFault tptr ex1 ex2)
         (Call handleDoubleFault_'proc)" apply (cinit lift: tptr_') apply (subst ccorres_seq_skip'[symmetric]) apply (ctac (no_vcg)) apply (rule ccorres_symb_exec_l) apply (rule ccorres_return_Skip) apply (wp asUser_inv getRestartPC_inv)+ apply (rule empty_fail_asUser) apply (simp add: getRestartPC_def) apply wp apply clarsimp apply (simp add: ThreadState_Inactive_def) apply (fastforce simp: valid_tcb_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p))) (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>) [] (handleDoubleFault tptr ex1 ex2) (Call handleDoubleFault_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> ccorres dc xfdc (?Q31 tptra) (?Q'31 tptra) [SKIP] (do y <- setThreadState Structures_H.thread_state.Inactive tptr;
faultPC <- asUser tptr getRestartPC;
return ()
od) (CALL setThreadState_'proc(tptra,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive))
 2. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q31 tptra s \<and> s' \<in> ?Q'31 tptra proof (prove)
goal (2 subgoals):
 1. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> ccorres dc xfdc (?Q38 tptra tptra) (?Q'38 tptra tptra) [SKIP] (do y <- setThreadState Structures_H.thread_state.Inactive tptr;
faultPC <- asUser tptr getRestartPC;
return ()
od) (CALL setThreadState_'proc(tptra,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive);;
SKIP)
 2. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q38 tptra tptra s \<and> s' \<in> ?Q'38 tptra tptra proof (prove)
goal (3 subgoals):
 1. \<And>tptra rv xfdca. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q42 tptra rv) (?Q'42 tptra rv xfdca) [SKIP] (do faultPC <- asUser tptr getRestartPC;
return ()
od) SKIP
 2. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> \<lbrace>?R52 tptra tptra\<rbrace> setThreadState Structures_H.thread_state.Inactive tptr \<lbrace>?Q42 tptra\<rbrace>
 3. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R52 tptra tptra) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'49 tptra tptra t rv}
flex-flex pairs:
\<lambda>tptra. ?Q'49 tptra tptra \<equiv>\<^sup>? \<lambda>tptra t rv. ?Q'42 tptra rv (xfdc t) proof (prove)
goal (6 subgoals):
 1. \<And>tptra rv xfdca faultPC. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q78 tptra rv xfdca faultPC) (?Q'78 tptra rv xfdca faultPC) [SKIP] (return ()) SKIP
 2. \<And>tptra rv xfdc s. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> asUser tptr getRestartPC \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptra rv xfdc. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 tptra rv\<rbrace> asUser tptr getRestartPC \<lbrace>?Q78 tptra rv xfdc\<rbrace>
 4. \<And>tptra rv xfdc. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> empty_fail (asUser tptr getRestartPC)
 5. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> \<lbrace>?R52 tptra tptra\<rbrace> setThreadState Structures_H.thread_state.Inactive tptr \<lbrace>?Q42 tptra\<rbrace>
 6. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R52 tptra tptra) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q84 tptra tptra t rv rva s \<longrightarrow> s' \<in> ?Q'83 tptra tptra t rv rva}}
flex-flex pairs:
\<lambda>tptra. ?Q84 tptra tptra \<equiv>\<^sup>? \<lambda>tptra t rv. ?Q78 tptra rv (xfdc t)
\<lambda>tptra. ?Q'83 tptra tptra \<equiv>\<^sup>? \<lambda>tptra t rv. ?Q'78 tptra rv (xfdc t) proof (prove)
goal (5 subgoals):
 1. \<And>tptra rv xfdc s. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> asUser tptr getRestartPC \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>tptra rv xfdc. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 tptra rv\<rbrace> asUser tptr getRestartPC \<lbrace>\<lambda>faultPC _. True\<rbrace>
 3. \<And>tptra rv xfdc. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> empty_fail (asUser tptr getRestartPC)
 4. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> \<lbrace>?R52 tptra tptra\<rbrace> setThreadState Structures_H.thread_state.Inactive tptr \<lbrace>?Q42 tptra\<rbrace>
 5. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R52 tptra tptra) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> True \<longrightarrow> s' \<in> UNIV}} proof (prove)
goal (3 subgoals):
 1. \<And>tptra rv xfdc. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> empty_fail (asUser tptr getRestartPC)
 2. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> \<lbrace>?R52 tptra tptra\<rbrace> setThreadState Structures_H.thread_state.Inactive tptr \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R52 tptra tptra) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> True \<longrightarrow> s' \<in> UNIV}} proof (prove)
goal (3 subgoals):
 1. \<And>tptra rv xfdc. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; dc rv xfdc\<rbrakk> \<Longrightarrow> empty_fail getRestartPC
 2. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> \<lbrace>?R52 tptra tptra\<rbrace> setThreadState Structures_H.thread_state.Inactive tptr \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R52 tptra tptra) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> True \<longrightarrow> s' \<in> UNIV}} proof (prove)
goal (2 subgoals):
 1. \<And>tptra. tptra = tcb_ptr_to_ctcb_ptr tptr \<Longrightarrow> \<lbrace>?R52 tptra tptra\<rbrace> setThreadState Structures_H.thread_state.Inactive tptr \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R52 tptra tptra) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> True \<longrightarrow> s' \<in> UNIV}} proof (prove)
goal (1 subgoal):
 1. \<And>tptra s s'. \<lbrakk>tptra = tcb_ptr_to_ctcb_ptr tptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not tptr and (\<lambda>s. \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' tptr a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Inactive a \<and> (ksSchedulerAction a = SwitchToThread tptr \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (\<forall>p. tptr \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. True)) s \<and> s' \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tptra) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr tptr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> True \<longrightarrow> s' \<in> UNIV}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; tcb_at' tptr s; weak_sch_act_wf (ksSchedulerAction s) s; sch_act_not tptr s; \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Inactive s \<and> sch_act_wf (ksSchedulerAction s) s \<and> SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; tcb_at' tptr s; weak_sch_act_wf (ksSchedulerAction s) s; sch_act_not tptr s; \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Inactive s \<and> sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!