theory CSpace_C

lemma cteInsert_ccorres_mdb_helper:
  "\<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = (newCapIsRevocable :: word32); srcSlot = Ptr src\<rbrakk>
       \<Longrightarrow> ccorres cmdbnode_relation newMDB_' (K (is_aligned src 3))
           UNIV hs
           (return
             (mdbFirstBadged_update (\<lambda>_. rvc)
               (mdbRevocable_update (\<lambda>_. rvc)
                 (mdbPrev_update (\<lambda>_. src) rva))))
           (\<acute>newMDB :== CALL mdb_node_set_mdbPrev(srcMDB,
            ptr_val srcSlot);;
            \<acute>newMDB :== CALL mdb_node_set_mdbRevocable(\<acute>newMDB,
            newCapIsRevocable);;
            \<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged(\<acute>newMDB,
            newCapIsRevocable))" apply (rule ccorres_from_vcg) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def mask_Suc_0) apply (simp add: cmdbnode_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = newCapIsRevocable; srcSlot = PTR('a) src\<rbrakk> \<Longrightarrow> ccorres cmdbnode_relation newMDB_' (K (is_aligned src 3)) UNIV hs (return (mdbFirstBadged_update (\<lambda>_. rvc) (mdbRevocable_update (\<lambda>_. rvc) (mdbPrev_update (\<lambda>_. src) rva)))) (\<acute>newMDB :== CALL mdb_node_set_mdbPrev_'proc(srcMDB,ptr_val srcSlot);;
\<acute>newMDB :== CALL mdb_node_set_mdbRevocable_'proc(\<acute>newMDB,newCapIsRevocable);;
\<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged_'proc(\<acute>newMDB,newCapIsRevocable)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = newCapIsRevocable; srcSlot = PTR('a) src\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. K (is_aligned src 3) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>newMDB :== CALL mdb_node_set_mdbPrev_'proc(srcMDB,ptr_val srcSlot);;
\<acute>newMDB :== CALL mdb_node_set_mdbRevocable_'proc(\<acute>newMDB,newCapIsRevocable);;
\<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged_'proc(\<acute>newMDB,newCapIsRevocable) {s. \<exists>(rv, \<sigma>')\<in>fst (return (mdbFirstBadged_update (\<lambda>_. rvc) (mdbRevocable_update (\<lambda>_. rvc) (mdbPrev_update (\<lambda>_. src) rva))) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> cmdbnode_relation rv (newMDB_' s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = newCapIsRevocable; srcSlot = PTR('a) src\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. K (is_aligned src 3) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>newMDB :== CALL mdb_node_set_mdbPrev_'proc(srcMDB,ptr_val srcSlot);;
\<acute>newMDB :== CALL mdb_node_set_mdbRevocable_'proc(\<acute>newMDB,newCapIsRevocable);;
\<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged_'proc(\<acute>newMDB,newCapIsRevocable) {s. \<exists>(rv, \<sigma>')\<in>fst (return (mdbFirstBadged_update (\<lambda>_. rvc) (mdbRevocable_update (\<lambda>_. rvc) (mdbPrev_update (\<lambda>_. src) rva))) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> cmdbnode_relation rv (newMDB_' s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = newCapIsRevocable; srcSlot = PTR('a) src\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'4 \<sigma>) \<acute>newMDB :== CALL mdb_node_set_mdbPrev_'proc(srcMDB,ptr_val srcSlot);;
\<acute>newMDB :== CALL mdb_node_set_mdbRevocable_'proc(\<acute>newMDB,newCapIsRevocable);;
\<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged_'proc(\<acute>newMDB,newCapIsRevocable) {s. \<exists>(rv, \<sigma>')\<in>fst (return (mdbFirstBadged_update (\<lambda>_. rvc) (mdbRevocable_update (\<lambda>_. rvc) (mdbPrev_update (\<lambda>_. src) rva))) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> cmdbnode_relation rv (newMDB_' s)}
 2. \<And>\<sigma>. \<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = newCapIsRevocable; srcSlot = PTR('a) src\<rbrakk> \<Longrightarrow> {s. K (is_aligned src 3) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'4 \<sigma> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = newCapIsRevocable; srcSlot = PTR('a) src\<rbrakk> \<Longrightarrow> {s. K (is_aligned src 3) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = mdb_node_lift srcMDB\<lparr>mdbPrev_CL := ptr_val srcSlot && ~~ mask 3\<rparr> \<longrightarrow> (\<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = mdb_node_lift srcMDB\<lparr>mdbPrev_CL := ptr_val srcSlot && ~~ mask 3, mdbRevocable_CL := newCapIsRevocable && mask 1\<rparr> \<longrightarrow> (\<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = mdb_node_lift srcMDB\<lparr>mdbPrev_CL := ptr_val srcSlot && ~~ mask 3, mdbRevocable_CL := newCapIsRevocable && mask 1, mdbFirstBadged_CL := newCapIsRevocable && mask 1\<rparr> \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (mdbFirstBadged_update (\<lambda>_. rvc) (mdbRevocable_update (\<lambda>_. rvc) (mdbPrev_update (\<lambda>_. src) rva))) \<sigma>). (\<sigma>', newMDB_'_update (\<lambda>_. ret__struct_mdb_node_C_' t) s) \<in> rf_sr \<and> cmdbnode_relation rv (ret__struct_mdb_node_C_' t))))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t ta tb. \<lbrakk>cmdbnode_relation rva srcMDB; srcSlot = PTR('a) src; newCapIsRevocable = from_bool rvc; is_aligned src 3; (\<sigma>, x) \<in> rf_sr; mdb_node_lift (ret__struct_mdb_node_C_' t) = mdb_node_lift srcMDB\<lparr>mdbPrev_CL := src\<rparr>; mdb_node_lift (ret__struct_mdb_node_C_' ta) = mdb_node_lift srcMDB\<lparr>mdbPrev_CL := src, mdbRevocable_CL := from_bool rvc\<rparr>; mdb_node_lift (ret__struct_mdb_node_C_' tb) = mdb_node_lift srcMDB\<lparr>mdbPrev_CL := src, mdbRevocable_CL := from_bool rvc, mdbFirstBadged_CL := from_bool rvc\<rparr>\<rbrakk> \<Longrightarrow> cmdbnode_relation (mdbFirstBadged_update (\<lambda>_. rvc) (mdbRevocable_update (\<lambda>_. rvc) (mdbPrev_update (\<lambda>_. src) rva))) (ret__struct_mdb_node_C_' tb) proof (prove)
goal:
No subgoals!