theory CSpace_C

lemma (in kernel_m) updateMDB_set_mdbPrev:
 "ccorres dc xfdc
     ( \<lambda>s. is_aligned ptr 3 \<and> (slota\<noteq>0 \<longrightarrow> is_aligned slota 3))
     {s. slotc = slota } hs
      (updateMDB ptr (mdbPrev_update (\<lambda>_. slota)))

      (IF ptr \<noteq> 0
       THEN
          Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr ptr:: cte_C ptr)\<rbrace>
               (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr ptr:: cte_C ptr
                                                          \<rightarrow>[''cteMDBNode_C'']),
                                 v32_' := slotc |))
                mdb_node_ptr_set_mdbPrev_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a)))
      FI)" apply (rule ccorres_guard_imp2) \<comment> \<open>replace preconditions by schematics\<close>
  \<comment> \<open>Main Goal\<close> apply (rule ccorres_Cond_rhs) apply (rule ccorres_updateMDB_cte_at) apply (ctac add: ccorres_updateMDB_set_mdbPrev) apply (ctac ccorres: ccorres_updateMDB_skip) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. is_aligned ptr 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) \<lbrace>slotc = slota\<rbrace> hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) (IF ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ptr} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C'']),slotc))
FI) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?Q' hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) (IF ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ptr} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C'']),slotc))
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> \<lbrace>slotc = slota\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ptr \<noteq> 0 \<Longrightarrow> ccorres dc xfdc ?Q3 ?S3 hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ptr} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C'']),slotc)))
 2. \<not> ptr \<noteq> 0 \<Longrightarrow> ccorres dc xfdc ?R3 ?T3 hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) SKIP
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> \<lbrace>slotc = slota\<rbrace>\<rbrakk> \<Longrightarrow> ((ptr \<noteq> 0 \<longrightarrow> ?Q3 s) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> ?R3 s)) \<and> s' \<in> {s. (ptr \<noteq> 0 \<longrightarrow> s \<in> ?S3) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> s \<in> ?T3)} proof (prove)
goal (3 subgoals):
 1. ptr \<noteq> 0 \<Longrightarrow> ccorres dc xfdc ?G6 ?S3 hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ptr} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C'']),slotc)))
 2. \<not> ptr \<noteq> 0 \<Longrightarrow> ccorres dc xfdc ?R3 ?T3 hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) SKIP
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> \<lbrace>slotc = slota\<rbrace>\<rbrakk> \<Longrightarrow> ((ptr \<noteq> 0 \<longrightarrow> (ptr \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s) \<longrightarrow> ?G6 s) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> ?R3 s)) \<and> s' \<in> {s. (ptr \<noteq> 0 \<longrightarrow> s \<in> ?S3) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> s \<in> ?T3)} proof (prove)
goal (2 subgoals):
 1. \<not> ptr \<noteq> 0 \<Longrightarrow> ccorres dc xfdc ?R3 ?T3 hs (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) SKIP
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> \<lbrace>slotc = slota\<rbrace>\<rbrakk> \<Longrightarrow> ((ptr \<noteq> 0 \<longrightarrow> (ptr \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s) \<longrightarrow> ((\<lambda>_. ptr \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ptr))) s) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> ?R3 s)) \<and> s' \<in> {s. (ptr \<noteq> 0 \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace>) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> s \<in> ?T3)} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> \<lbrace>slotc = slota\<rbrace>\<rbrakk> \<Longrightarrow> ((ptr \<noteq> 0 \<longrightarrow> (ptr \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s) \<longrightarrow> ((\<lambda>_. ptr \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ptr))) s) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. ptr = 0)) s)) \<and> s' \<in> {s. (ptr \<noteq> 0 \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr ptr\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace>) \<and> (\<not> ptr \<noteq> 0 \<longrightarrow> s \<in> UNIV)} proof (prove)
goal:
No subgoals!