theory CSpace_R

lemma setupReplyMaster_urz[wp]:
  "\<lbrace>untyped_ranges_zero' and valid_mdb' and valid_objs'\<rbrace>
    setupReplyMaster t
  \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (rule hoare_pre) apply (wp untyped_ranges_zero_lift getCTE_wp' | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of fun_upd_def[symmetric]) apply (subst untyped_ranges_zero_fun_upd, assumption, simp_all) apply (clarsimp simp: cteCaps_of_def untypedZeroRange_def Let_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_mdb' and valid_objs'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_mdb' and valid_objs'\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and valid_mdb' and valid_objs') s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero' s \<and> valid_mdb' s \<and> valid_objs' s \<Longrightarrow> \<forall>cte. cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> noReplyCapsFor t s \<longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = t + 2 ^ cte_level_bits * tcbReplySlot then Some (capability.ReplyCap t True True) else cteCaps_of s a) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>untyped_ranges_zero' s; valid_mdb' s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(t + 2 ^ cte_level_bits * tcbReplySlot \<mapsto> capability.ReplyCap t True True)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>untyped_ranges_zero' s; valid_mdb' s; valid_objs' s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; noReplyCapsFor t s; set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (t + 2 ^ cte_level_bits * tcbReplySlot)) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (t + 2 ^ cte_level_bits * tcbReplySlot)) \<union> set_option (untypedZeroRange (capability.ReplyCap t True True)) proof (prove)
goal:
No subgoals!