theory CSpace_R

lemma setupReplyMaster_corres:
  "corres dc (einvs and tcb_at t) (invs' and tcb_at' t)
       (setup_reply_master t) (setupReplyMaster t)" apply (simp add: setupReplyMaster_def setup_reply_master_def) apply (simp add: locateSlot_conv tcbReplySlot_def objBits_def objBitsKO_def) apply (simp add: nullMDBNode_def, fold initMDBNode_def) apply (rule_tac F="t + 2*2^cte_level_bits = cte_map (t, tcb_cnode_index 2)" in corres_req) apply (clarsimp simp: tcb_cnode_index_def2 cte_map_nat_to_cref word_bits_def cte_level_bits_def) apply (clarsimp simp: cte_level_bits_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_when) apply fastforce apply (rule_tac P'="einvs and tcb_at t" in corres_stateAssert_implied) apply (rule create_reply_master_corres; simp) apply (subgoal_tac "\<exists>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s'
                              \<and> cteCap cte = capability.NullCap") apply (fastforce dest: pspace_relation_no_reply_caps
                             state_relation_pspace_relation) apply (clarsimp simp: cte_map_def tcb_cnode_index_def cte_wp_at_ctes_of) apply (rule_tac Q="\<lambda>rv. einvs and tcb_at t and
                             cte_wp_at ((=) rv) (t, tcb_cnode_index 2)"
                  in hoare_strengthen_post) apply (wp hoare_drop_imps get_cap_wp) apply (clarsimp simp: invs_def valid_state_def elim!: cte_wp_at_weakenE) apply (rule_tac Q="\<lambda>rv. valid_pspace' and valid_mdb' and
                            cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))"
                 in hoare_strengthen_post) apply (wp hoare_drop_imps getCTE_wp') apply (rename_tac rv s) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) apply (case_tac rv, fastforce elim: valid_nullcapsE) apply (fastforce elim: tcb_at_cte_at) apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (setup_reply_master t) (setupReplyMaster t) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do slot <- locateSlotTCB t tcbReplySlot;
oldCTE <- getCTE slot;
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE slot (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do oldCTE <- getCTE (t + 2 ^ cte_level_bits * 2);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * 2) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do oldCTE <- getCTE (t + 2 ^ cte_level_bits * 2);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * 2) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; (einvs and tcb_at t) s; (invs' and tcb_at' t) s'\<rbrakk> \<Longrightarrow> t + 2 * 2 ^ cte_level_bits = cte_map (t, tcb_cnode_index 2)
 2. t + 2 * 2 ^ cte_level_bits = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do oldCTE <- getCTE (t + 2 ^ cte_level_bits * 2);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * 2) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
od) proof (prove)
goal (1 subgoal):
 1. t + 2 * 2 ^ cte_level_bits = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do oldCTE <- getCTE (t + 2 ^ cte_level_bits * 2);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * 2) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
od) proof (prove)
goal (1 subgoal):
 1. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do oldCTE <- getCTE (cte_map (t, tcb_cnode_index 2));
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (cte_map (t, tcb_cnode_index 2)) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
od) proof (prove)
goal (3 subgoals):
 1. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> corres dc ?Q2 ?Q'2 (do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od) (do oldCTE <- getCTE (cte_map (t, tcb_cnode_index 2));
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (cte_map (t, tcb_cnode_index 2)) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
od)
 2. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q'2 s' proof (prove)
goal (5 subgoals):
 1. \<And>old_cap rv'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv')\<rbrakk> \<Longrightarrow> corres dc (?R6 old_cap) (?R'6 rv') (when (old_cap = cap.NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)) (when (cteCap rv' = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (cte_map (t, tcb_cnode_index 2)) (CTE (capability.ReplyCap t True True) initMDBNode)
od))
 2. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?R6\<rbrace>
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>?R'6\<rbrace>
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (6 subgoals):
 1. \<And>old_cap rv'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv')\<rbrakk> \<Longrightarrow> (old_cap = cap.NullCap) = (cteCap rv' = capability.NullCap)
 2. \<And>old_cap rv'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv')\<rbrakk> \<Longrightarrow> corres dc (?P13 old_cap) (?P'15 rv') (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (cte_map (t, tcb_cnode_index 2)) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> ?P13 old_cap x\<rbrace>
 4. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> ?P'15 rv' x\<rbrace>
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 6. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (5 subgoals):
 1. \<And>old_cap rv'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv')\<rbrakk> \<Longrightarrow> corres dc (?P13 old_cap) (?P'15 rv') (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (cte_map (t, tcb_cnode_index 2)) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
 2. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> ?P13 old_cap x\<rbrace>
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> ?P'15 rv' x\<rbrace>
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (6 subgoals):
 1. \<And>old_cap rv'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv')\<rbrakk> \<Longrightarrow> corres dc (?P23 old_cap) (?P'15 rv') (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (cap.ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od) (setCTE (cte_map (t, tcb_cnode_index 2)) (CTE (capability.ReplyCap t True True) initMDBNode))
 2. \<And>old_cap rv' s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv'); (s, s') \<in> state_relation; ?P23 old_cap s; (einvs and tcb_at t) s; ?P'15 rv' s'\<rbrakk> \<Longrightarrow> noReplyCapsFor t s'
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> (?P23 old_cap and (einvs and tcb_at t)) x\<rbrace>
 4. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> ?P'15 rv' x\<rbrace>
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 6. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (5 subgoals):
 1. \<And>old_cap rv' s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv'); (s, s') \<in> state_relation; (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list) s; (einvs and tcb_at t) s; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s'\<rbrakk> \<Longrightarrow> noReplyCapsFor t s'
 2. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list and (einvs and tcb_at t)) x\<rbrace>
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (6 subgoals):
 1. \<And>old_cap rv' s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv'); (s, s') \<in> state_relation; (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list) s; (einvs and tcb_at t) s; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s'; \<exists>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s' \<and> cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> noReplyCapsFor t s'
 2. \<And>old_cap rv' s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv'); (s, s') \<in> state_relation; (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list) s; (einvs and tcb_at t) s; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s'\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s' \<and> cteCap cte = capability.NullCap
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list and (einvs and tcb_at t)) x\<rbrace>
 4. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 6. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (5 subgoals):
 1. \<And>old_cap rv' s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); cap_relation old_cap (cteCap rv'); (s, s') \<in> state_relation; (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list) s; (einvs and tcb_at t) s; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s'\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s' \<and> cteCap cte = capability.NullCap
 2. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list and (einvs and tcb_at t)) x\<rbrace>
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (4 subgoals):
 1. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>old_cap x. old_cap = cap.NullCap \<longrightarrow> (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list and (einvs and tcb_at t)) x\<rbrace>
 2. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (5 subgoals):
 1. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q6\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>\<lambda>rv. einvs and tcb_at t and cte_wp_at ((=) rv) (t, tcb_cnode_index 2)\<rbrace>
 2. \<And>rv s. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t and cte_wp_at ((=) rv) (t, tcb_cnode_index 2)) s\<rbrakk> \<Longrightarrow> rv = cap.NullCap \<longrightarrow> (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list and (einvs and tcb_at t)) s
 3. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and ?Q6) s
 5. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t and cte_wp_at ((=) rv) (t, tcb_cnode_index 2)) s\<rbrakk> \<Longrightarrow> rv = cap.NullCap \<longrightarrow> (cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 2) and valid_pspace and valid_mdb and valid_list and (einvs and tcb_at t)) s
 2. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (3 subgoals):
 1. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv' x. cteCap rv' = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') x\<rbrace>
 2. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (4 subgoals):
 1. t + 0x20 = cte_map (t, tcb_cnode_index 2) \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCTE (cte_map (t, tcb_cnode_index 2)) \<lbrace>\<lambda>rv. valid_pspace' and valid_mdb' and cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))\<rbrace>
 2. \<And>rv s. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (valid_pspace' and valid_mdb' and cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))) s\<rbrakk> \<Longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 4. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'6) s' proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (valid_pspace' and valid_mdb' and cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))) s\<rbrakk> \<Longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s
 2. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s \<longrightarrow> (valid_pspace' and valid_mdb' and cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2))) s)) s' proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (valid_pspace' and valid_mdb' and cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))) s\<rbrakk> \<Longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<and> mdbPrev (cteMDBNode c) = 0) (cte_map (t, tcb_cnode_index 2)) and valid_mdb' and valid_pspace') s
 2. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s \<longrightarrow> (valid_pspace' and valid_mdb' and cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2))) s)) s' proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); valid_pspace' s; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s (cte_map (t, tcb_cnode_index 2)) = Some rv; cteCap rv = capability.NullCap\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode rv) = 0
 2. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 3. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s \<longrightarrow> (valid_pspace' and valid_mdb' and cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2))) s)) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (einvs and tcb_at t and cte_wp_at ((=) cap) (t, tcb_cnode_index 2)) s)) s
 2. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s \<longrightarrow> (valid_pspace' and valid_mdb' and cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2))) s)) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>t + 0x20 = cte_map (t, tcb_cnode_index 2); (einvs and tcb_at t) s; (invs' and tcb_at' t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2)) s \<longrightarrow> (valid_pspace' and valid_mdb' and cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 2))) s)) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>of_bl (tcb_cnode_index 2) * 2 ^ cte_level_bits = 0x20; (s, s') \<in> state_relation; invs s; invs' s'; tcb_at' t s'; valid_list s; valid_sched s; tcb_at t s\<rbrakk> \<Longrightarrow> pspace_aligned' s' \<and> pspace_distinct' s' \<and> ((\<exists>cte. cte_wp_at' ((=) cte) (t + 0x20) s') \<longrightarrow> valid_pspace' s' \<and> valid_mdb' s') proof (prove)
goal:
No subgoals!