theory CSpace_R

lemma setupReplyMaster_global_refs[wp]:
  "\<lbrace>\<lambda>s. valid_global_refs' s \<and> thread \<notin> global_refs' s \<and> tcb_at' thread s
      \<and> ex_nonz_cap_to' thread s \<and> valid_objs' s\<rbrace>
    setupReplyMaster thread
   \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (wp getCTE_wp') apply (clarsimp simp: capRange_def cte_wp_at_ctes_of objBits_simps) apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (rename_tac "prev_cte") apply (case_tac prev_cte, simp) apply (frule(1) ctes_of_valid_cap') apply (drule(1) valid_global_refsD_with_objSize)+ apply (clarsimp simp: valid_cap'_def objBits_simps obj_at'_def projectKOs
                 split: capability.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_refs' s \<and> thread \<notin> global_refs' s \<and> tcb_at' thread s \<and> ex_nonz_cap_to' thread s \<and> valid_objs' s\<rbrace> setupReplyMaster thread \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_refs' s \<and> thread \<notin> global_refs' s \<and> tcb_at' thread s \<and> ex_nonz_cap_to' thread s \<and> valid_objs' s\<rbrace> do oldCTE <- getCTE (thread + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor thread) [];
setCTE (thread + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap thread True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs' s \<and> thread \<notin> global_refs' s \<and> tcb_at' thread s \<and> ex_nonz_cap_to' thread s \<and> valid_objs' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (thread + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (if cteCap cte = capability.NullCap then \<lambda>s. noReplyCapsFor thread s \<longrightarrow> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (cteCap (CTE (capability.ReplyCap thread True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))) = {}) and (\<lambda>s. 2 ^ capBits (cteCap (CTE (capability.ReplyCap thread True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))) \<le> gsMaxObjectSize s)) s else valid_global_refs') s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_global_refs' s; thread \<notin> global_refs' s; tcb_at' thread s; ex_nonz_cap_to' thread s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (thread + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor thread s\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea. \<lbrakk>valid_global_refs' s; thread \<notin> global_refs' s; tcb_at' thread s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (thread + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor thread s; ctes_of s cref = Some ctea; thread \<in> zobj_refs' (cteCap ctea)\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref prev_cte. \<lbrakk>valid_global_refs' s; thread \<notin> global_refs' s; tcb_at' thread s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (thread + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor thread s; ctes_of s cref = Some prev_cte; thread \<in> zobj_refs' (cteCap prev_cte)\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref prev_cte x1 x2. \<lbrakk>valid_global_refs' s; thread \<notin> global_refs' s; tcb_at' thread s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (thread + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor thread s; ctes_of s cref = Some (CTE x1 x2); thread \<in> zobj_refs' x1; prev_cte = CTE x1 x2\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref prev_cte x1 x2. \<lbrakk>valid_global_refs' s; thread \<notin> global_refs' s; tcb_at' thread s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (thread + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor thread s; ctes_of s cref = Some (CTE x1 x2); thread \<in> zobj_refs' x1; prev_cte = CTE x1 x2; valid_cap' x1 s\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref prev_cte x1 x2. \<lbrakk>valid_global_refs' s; thread \<notin> global_refs' s; tcb_at' thread s; valid_objs' s; cteCap cte = capability.NullCap; noReplyCapsFor thread s; thread \<in> zobj_refs' x1; prev_cte = CTE x1 x2; valid_cap' x1 s; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s; kernel_data_refs \<inter> capRange (cteCap (CTE x1 x2)) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap (CTE x1 x2)) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!