theory Finalise_C

lemma updateRestartPC_ccorres:
  "ccorres dc xfdc (tcb_at' thread) \<lbrace> \<acute>tcb = tcb_ptr_to_ctcb_ptr thread \<rbrace> hs
     (updateRestartPC thread) (Call updateRestartPC_'proc)" apply (cinit lift: tcb_') apply (subst asUser_bind_distrib; (wp add: empty_fail_getRegister)?) apply (ctac (no_vcg) add: getRegister_ccorres) apply (ctac (no_vcg) add: setRegister_ccorres) apply wpsimp+ apply (simp add: ARM_H.faultRegister_def ARM_H.nextInstructionRegister_def
                   ARM.faultRegister_def ARM.nextInstructionRegister_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr thread\<rbrace> hs (updateRestartPC thread) (Call updateRestartPC_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q56 tcb) (?Q'56 tcb) (SKIP # hs) (asUser thread (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister)) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb,SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP);;
CALL setRegister_'proc(tcb,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP,\<acute>ret__unsigned_long))
 2. \<And>tcb s s'. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q56 tcb s \<and> s' \<in> ?Q'56 tcb proof (prove)
goal (2 subgoals):
 1. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q63 tcb tcb) (?Q'63 tcb tcb) (SKIP # hs) (do rv <- asUser thread (getRegister Thread_H.nextInstructionRegister);
asUser thread (setRegister Thread_H.faultRegister rv)
od) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb,SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP);;
CALL setRegister_'proc(tcb,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP,\<acute>ret__unsigned_long))
 2. \<And>tcb s s'. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q63 tcb tcb s \<and> s' \<in> ?Q'63 tcb tcb proof (prove)
goal (3 subgoals):
 1. \<And>tcb rv ret__unsigned_long. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr thread; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q75 tcb rv) (?Q'75 tcb rv ret__unsigned_long) (SKIP # hs) (asUser thread (setRegister Thread_H.faultRegister rv)) (CALL setRegister_'proc(tcb,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP,ret__unsigned_long))
 2. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R86 tcb tcb\<rbrace> asUser thread (getRegister Thread_H.nextInstructionRegister) \<lbrace>?Q75 tcb\<rbrace>
 3. \<And>tcb s s'. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R86 tcb tcb) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP) (thread_'_update (\<lambda>_. tcb) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Thread_H.nextInstructionRegister\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'83 tcb tcb t rv}
flex-flex pairs:
\<lambda>tcb. ?Q'83 tcb tcb \<equiv>\<^sup>? \<lambda>tcb t rv. ?Q'75 tcb rv (ret__unsigned_long_' t) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R86 tcb tcb\<rbrace> asUser thread (getRegister Thread_H.nextInstructionRegister) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>tcb s s'. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R86 tcb tcb) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP) (thread_'_update (\<lambda>_. tcb) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Thread_H.nextInstructionRegister\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. w_'_update (\<lambda>_. ret__unsigned_long_' t) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) (thread_'_update (\<lambda>_. tcb) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Thread_H.faultRegister\<rbrace> \<inter> \<lbrace>\<acute>w = rv\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s\<rbrakk> \<Longrightarrow> s' \<in> (if SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP = register_from_H Thread_H.nextInstructionRegister then UNIV else {}) \<and> (\<forall>t. s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> (if SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP = register_from_H Thread_H.faultRegister then UNIV else {})) proof (prove)
goal:
No subgoals!