theory TcbAcc_C

lemma getRestartPC_ccorres [corres]:
  "ccorres (=) ret__unsigned_long_' \<top> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> []
           (asUser thread getRestartPC) (Call getRestartPC_'proc)" unfolding getRestartPC_def apply (cinit') apply (rule ccorres_add_return2, ctac) apply (rule ccorres_return_C, simp+)[1] apply wp apply vcg apply (simp add: scast_id) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (=) ret__unsigned_long_' (\<lambda>_. True) \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> [] (asUser thread getRestartPC) (Call getRestartPC_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (=) ret__unsigned_long_' (\<lambda>_. True) \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> [] (asUser thread (getRegister register.FaultIP)) (Call getRestartPC_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres (=) ret__unsigned_long_' ?Q10 ?Q'10 [SKIP] (asUser thread (getRegister register.FaultIP)) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ?Q10 s \<and> s' \<in> ?Q'10 proof (prove)
goal (4 subgoals):
 1. \<And>rv ret__unsigned_long. rv = ret__unsigned_long \<Longrightarrow> ccorres (=) ret__unsigned_long_' (?Q20 rv) (?Q'20 rv ret__unsigned_long) [SKIP] (return rv) (return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long))
 2. \<lbrace>?R20\<rbrace> asUser thread (getRegister register.FaultIP) \<lbrace>?Q20\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'20 \<acute>ret__unsigned_long :== CALL getRegister_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'20 rv (ret__unsigned_long_' s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R20) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) (thread_'_update (\<lambda>_. thread_' s) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H register.FaultIP\<rbrace>} \<inter> ?R'20 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R20\<rbrace> asUser thread (getRegister register.FaultIP) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'20 \<acute>ret__unsigned_long :== CALL getRegister_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> \<lbrace>rv = \<^bsup>s\<^esup>ret__unsigned_long\<rbrace>}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R20) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) (thread_'_update (\<lambda>_. thread_' s) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H register.FaultIP\<rbrace>} \<inter> ?R'20 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'20 \<acute>ret__unsigned_long :== CALL getRegister_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> \<lbrace>rv = \<^bsup>s\<^esup>ret__unsigned_long\<rbrace>}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) (thread_'_update (\<lambda>_. thread_' s) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H register.FaultIP\<rbrace>} \<inter> ?R'20 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP) (thread_'_update (\<lambda>_. thread_' s) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H register.FaultIP\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!