theory SyscallArgs_C

lemma threadGet_tcbIpcBuffer_ccorres [corres]:
  "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs
           (threadGet tcbIPCBuffer tptr)
           (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr tptr\<rbrace>
               (\<acute>w_bufferPtr :==
                  h_val (hrs_mem \<acute>t_hrs)
                   (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::word32 ptr)))" apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return2) apply (rule ccorres_pre_threadGet) apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and
                   P'="{s'. \<exists>ctcb.
          cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and>
                 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (clarsimp simp: return_def typ_heap_simps') apply (clarsimp simp: obj_at'_def ctcb_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs (threadGet tcbIPCBuffer tptr) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr} (\<acute>w_bufferPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])))) proof (prove)
goal (2 subgoals):
 1. ccorres (=) w_bufferPtr_' ?Q ?Q' hs (threadGet tcbIPCBuffer tptr) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr} (\<acute>w_bufferPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres (=) w_bufferPtr_' ?Q ?Q' hs (threadGet tcbIPCBuffer tptr >>= return) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr} (\<acute>w_bufferPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>x. ccorres (=) w_bufferPtr_' (?P5 x) (?P'5 x) hs (return x) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr} (\<acute>w_bufferPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb tptr s \<longrightarrow> ?P5 (tcbIPCBuffer tcb) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'5 (tcbIPCBuffer tcb)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr \<sigma> \<and> s \<in> {s'. \<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> tcbIPCBuffer_C ctcb = x} \<and> (\<sigma>, s) \<in> rf_sr} Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr} (\<acute>w_bufferPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C'']))) {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rv = w_bufferPtr_' s}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb tptr s \<longrightarrow> obj_at' (\<lambda>tcba. tcbIPCBuffer tcba = tcbIPCBuffer tcb) tptr s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> tcbIPCBuffer_C ctcb = tcbIPCBuffer tcb}} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma>. {s. obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr \<sigma> \<and> s \<in> {s'. \<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> tcbIPCBuffer_C ctcb = x} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr \<and> (\<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', w_bufferPtr_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C'']))) s) \<in> rf_sr \<and> rv = h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb tptr s \<longrightarrow> obj_at' (\<lambda>tcba. tcbIPCBuffer tcba = tcbIPCBuffer tcb) tptr s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> tcbIPCBuffer_C ctcb = tcbIPCBuffer tcb}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa ctcb. \<lbrakk>obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = tcbIPCBuffer_C ctcb) tptr \<sigma>; (\<sigma>, xa) \<in> rf_sr; cslift xa (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb\<rbrakk> \<Longrightarrow> xa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tptr \<and> (\<exists>x\<in>fst (return (tcbIPCBuffer_C ctcb) \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr \<and> rv = h_val (hrs_mem (t_hrs_' (globals xa))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb tptr s \<longrightarrow> obj_at' (\<lambda>tcba. tcbIPCBuffer tcba = tcbIPCBuffer tcb) tptr s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> tcbIPCBuffer_C ctcb = tcbIPCBuffer tcb}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' tptr s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb tptr s \<longrightarrow> obj_at' (\<lambda>tcba. tcbIPCBuffer tcba = tcbIPCBuffer tcb) tptr s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> tcbIPCBuffer_C ctcb = tcbIPCBuffer tcb}} proof (prove)
goal:
No subgoals!