theory CSpace_C

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

     (IF mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0
      THEN
          Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr)\<rbrace>
               (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr
                                                           \<rightarrow>[''cteMDBNode_C'']),
                                 v32_' := ptr_val slotc |))
                mdb_node_ptr_set_mdbNext_'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 mdbPrev_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_mdbNext)
                   \<comment> \<open>-- ccorres_call generates 4 subgoals, the 3 last being solved by simp\<close>
   \<comment> \<open>***cond False: ptr = 0***\<close> apply (ctac ccorres: ccorres_updateMDB_skip)

  \<comment> \<open>instanciate generalized preconditions\<close> apply (case_tac "mdbPrev_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: cte_wp_at_ctes_of cmdbnode_relation_def) 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 (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) UNIV hs (updateMDB (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) (IF mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) (IF mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_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 (mdbPrev 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>mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) SKIP
 4. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbPrev 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>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) SKIP
 4. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev ?n14 \<noteq> 0 \<longrightarrow> ?Pt3 s) and (\<lambda>s. \<not> mdbPrev ?n14 \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) SKIP
 3. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> ?Pt3 s) and (\<lambda>s. \<not> mdbPrev mdba \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) SKIP
 3. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> (mdbPrev mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev mdba) s) \<longrightarrow> ?G16 s) and (\<lambda>s. \<not> mdbPrev mdba \<noteq> 0 \<longrightarrow> ?Pf3 s)) s \<and> s' \<in> ?Rt3 \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) SKIP
 2. \<And>s s'. \<lbrakk>slotc = PTR('a) slota; cmdbnode_relation mdba mdbc; (s, s') \<in> rf_sr; is_aligned (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> (mdbPrev mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev mdba) s) \<longrightarrow> ((\<lambda>_. mdbPrev mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbPrev 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 (mdbPrev_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbPrev mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> ?Rf3 \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> (mdbPrev mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev mdba) s) \<longrightarrow> ((\<lambda>_. mdbPrev mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbPrev mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbPrev mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbPrev mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV; mdbPrev_CL (mdb_node_lift mdbc) = 0\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> (mdbPrev mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev mdba) s) \<longrightarrow> ((\<lambda>_. mdbPrev mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbPrev mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbPrev mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbPrev mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV; mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> (mdbPrev mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev mdba) s) \<longrightarrow> ((\<lambda>_. mdbPrev mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbPrev mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbPrev mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbPrev mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbPrev_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 (mdbPrev mdba) 3 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3); s' \<in> UNIV; mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdbPrev mdba \<noteq> 0 \<longrightarrow> (mdbPrev mdba \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev mdba) s) \<longrightarrow> ((\<lambda>_. mdbPrev mdba \<noteq> 0 \<and> (slota \<noteq> 0 \<longrightarrow> is_aligned slota 3)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))))) s) and (\<lambda>s. \<not> mdbPrev mdba \<noteq> 0 \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. mdbPrev mdba = 0)) s)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. ptr_val slotc) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdbc))\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr (mdbPrev mdba)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slota\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> \<union> UNIV \<inter> - \<lbrace>mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0\<rbrace> proof (prove)
goal:
No subgoals!