theory CSpace_C

lemma updateMDB_mdbNext_set_mdbPrev:
 "\<lbrakk> slotc = Ptr slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow>
  ccorres dc xfdc
     ( \<lambda>s. is_aligned (mdbNext mdba) 3 \<and> (slota\<noteq>0\<longrightarrow>is_aligned slota 3))
     UNIV hs
      (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota)))

      (IF mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0
       THEN
          Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr (mdbNext_CL (mdb_node_lift mdbc)) :: cte_C ptr)\<rbrace>
               (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbNext_CL (mdb_node_lift mdbc)):: cte_C ptr
                                                          \<rightarrow>[''cteMDBNode_C'']),
                                 v32_' := ptr_val 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_both [where R="\<lambda>_.True", simplified])  \<comment> \<open>generates 3 subgoals (one for 'then', one for 'else')\<close>
   \<comment> \<open>***instanciate the condition***\<close> apply (rule mdbNext_not_zero_eq) apply assumption
   \<comment> \<open>***cond True: ptr \<noteq> 0***\<close> apply (rule ccorres_updateMDB_cte_at) apply (ctac add: ccorres_updateMDB_set_mdbPrev) apply (ctac ccorres: ccorres_updateMDB_skip)
  \<comment> \<open>instanciate generalized preconditions\<close> apply (case_tac "mdbNext_CL (mdb_node_lift mdbc)=0")

  \<comment> \<open>Next is zero\<close> apply (clarsimp simp: cmdbnode_relation_def)

  \<comment> \<open>Next is not zero\<close> apply (clarsimp simp: cmdbnode_relation_def cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>s. is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) UNIV hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) (IF mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C'']),ptr_val slotc))
FI) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) (IF mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C'']),ptr_val slotc))
FI)
 2. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<longrightarrow> ?P3 s = (s' \<in> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace>)
 2. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pt3 ?Rt3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C'']),ptr_val slotc)))
 3. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pf3 ?Rf3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) SKIP
 4. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. ?P3 s \<longrightarrow> ?Pt3 s) and (\<lambda>s. \<not> ?P3 s \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> cmdbnode_relation ?n14 mdbc
 2. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pt3 ?Rt3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C'']),ptr_val slotc)))
 3. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pf3 ?Rf3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) SKIP
 4. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext ?n14 \<noteq> 0 \<longrightarrow> ?Pt3 s) and (\<lambda>s. \<not> mdbNext ?n14 \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pt3 ?Rt3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C'']),ptr_val slotc)))
 2. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pf3 ?Rf3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) SKIP
 3. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> ?Pt3 s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?G16 ?Rt3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C'']),ptr_val slotc)))
 2. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pf3 ?Rf3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) SKIP
 3. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> (mdbNext mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext mdba) s) \<longrightarrow> ?G16 s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Pf3 ?Rf3 hs (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) SKIP
 2. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> (mdbNext mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext mdba) s) \<longrightarrow> ((\<lambda>_. mdbNext mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbNext mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> (mdbNext mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext mdba) s) \<longrightarrow> ((\<lambda>_. mdbNext mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbNext mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbNext mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV; mdbNext_CL (mdb_node_lift mdbc) = 0\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> (mdbNext mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext mdba) s) \<longrightarrow> ((\<lambda>_. mdbNext mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbNext mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbNext mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace>
 2. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV; mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> (mdbNext mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext mdba) s) \<longrightarrow> ((\<lambda>_. mdbNext mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbNext mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbNext mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbNext mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV; mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbNext mdba \<noteq> 0 \<longrightarrow> (mdbNext mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext mdba) s) \<longrightarrow> ((\<lambda>_. mdbNext mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbNext mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbNext mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbNext mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal:
No subgoals!