theory IpcCancel_R

lemma (in delete_one) cancelIPC_ReplyCap_corres:
  "corres dc (einvs  and st_tcb_at awaiting_reply t)
             (invs' and st_tcb_at' awaiting_reply' t)
      (reply_cancel_ipc t)
      (do y \<leftarrow> threadSet (\<lambda>tcb. tcb \<lparr> tcbFault := None \<rparr>) t;
          slot \<leftarrow> getThreadReplySlot t;
          callerCap \<leftarrow> liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
          when (callerCap \<noteq> nullPointer) (do
              y \<leftarrow> stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap
                                                             \<and> \<not> capReplyMaster cap))
                  [];
              cteDeleteOne callerCap
          od)
       od)" proof - interpret Arch .  (*FIXME: arch_split*)
   show ?thesis apply (simp add: reply_cancel_ipc_def getThreadReplySlot_def
                   locateSlot_conv liftM_def tcbReplySlot_def
              del: split_paired_Ex) apply (rule_tac Q="\<lambda>_. invs and valid_list and valid_sched and st_tcb_at awaiting_reply t"
              and Q'="\<lambda>_. invs' and st_tcb_at' awaiting_reply' t"
               in corres_underlying_split) apply (rule corres_guard_imp) apply (rule threadset_corresT) apply (simp add: tcb_relation_def fault_rel_optionation_def) apply (simp add: tcb_cap_cases_def) apply (simp add: tcb_cte_cases_def) apply (simp add: exst_same_def) apply (clarsimp simp: st_tcb_at_tcb_at) apply clarsimp defer apply (wp thread_set_invs_trivial thread_set_no_change_tcb_state
              threadSet_invs_trivial threadSet_pred_tcb_no_state thread_set_not_state_valid_sched
         | fastforce simp: tcb_cap_cases_def inQ_def
         | wp (once) sch_act_simple_lift)+ apply (rule corres_underlying_split) apply (rule corres_guard_imp) apply (rule get_cap_corres [where cslot_ptr="(t, tcb_cnode_index 2)",
                                          simplified cte_map_tcb_2 cte_index_repair_sym]) apply (clarsimp dest!: st_tcb_at_tcb_at
                             tcb_at_cte_at [where ref="tcb_cnode_index 2"]) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) defer apply (rule hoare_vcg_conj_lift [OF get_cap_inv get_cap_cte_wp_at, simplified]) apply (rule hoare_vcg_conj_lift [OF getCTE_inv getCTE_cte_wp_at, simplified]) apply (rename_tac cte) apply (rule corres_symb_exec_l [OF _ _ gets_sp]) apply (rule_tac F="\<exists>r. cap = cap.ReplyCap t True r \<and>
                       cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r)" in corres_req) apply (fastforce simp: cte_wp_at_caps_of_state is_cap_simps
                     dest!: st_tcb_at_reply_cap_valid) apply (rule_tac F="(descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer)"
                 in corres_req) apply (fastforce simp: st_tcb_at_tcb_at cte_wp_at_ctes_of st_tcb_def2 cte_index_repair
                     dest: reply_descendants_of_mdbNext) apply (elim exE) apply (case_tac "descs = {}", simp add: when_def) apply (rule_tac F="\<exists>sl. descs = {sl}" in corres_req) apply (fastforce intro: st_tcb_at_tcb_at dest: reply_master_one_descendant) apply (erule exE, frule singleton_eqD) apply (rule_tac F="mdbNext (cteMDBNode cte) = cte_map sl" in corres_req) apply (clarsimp dest!: st_tcb_at_tcb_at) apply (fastforce simp: cte_wp_at_ctes_of cte_level_bits_def
                    elim!: reply_mdbNext_is_descendantD) apply (simp add: when_def getSlotCap_def capHasProperty_def
                del: split_paired_Ex) apply (rule corres_guard_imp) apply (rule_tac P'="\<lambda>s. \<exists>r'. cte_wp_at ((=) (cap.ReplyCap t False r')) sl s"
                   in corres_stateAssert_implied [OF delete_one_corres]) apply (fastforce dest: pspace_relation_cte_wp_at
                            state_relation_pspace_relation
                      simp: cte_wp_at_ctes_of isCap_simps) apply (fastforce simp: invs_def valid_state_def valid_mdb_def reply_mdb_def
                           reply_masters_mdb_def cte_wp_at_caps_of_state
                           can_fast_finalise_def) apply (fastforce simp: valid_mdb'_def valid_mdb_ctes_def
                          cte_wp_at_ctes_of nullPointer_def
                    elim: valid_dlistEn dest: invs_mdb') apply (simp add: exs_valid_def gets_def get_def return_def bind_def
               del: split_paired_Ex split_paired_All) apply (wp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (reply_cancel_ipc t) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) proof (state)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (reply_cancel_ipc t) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) proof (prove)
goal:
No subgoals! proof (state)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (reply_cancel_ipc t) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) proof (state)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (reply_cancel_ipc t) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (reply_cancel_ipc t) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od) proof (prove)
goal (4 subgoals):
 1. corres ?r'1 (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (thread_set (tcb_fault_update (\<lambda>_. None)) t) (threadSet (tcbFault_update (\<lambda>_. None)) t)
 2. \<And>rv rv'. ?r'1 rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 3. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 4. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (6 subgoals):
 1. corres ?r'1 ?Q3 ?Q'3 (thread_set (tcb_fault_update (\<lambda>_. None)) t) (threadSet (tcbFault_update (\<lambda>_. None)) t)
 2. \<And>s. (einvs and st_tcb_at awaiting_reply t) s \<Longrightarrow> ?Q3 s
 3. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> ?Q'3 s
 4. \<And>rv rv'. ?r'1 rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 5. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 6. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_fault := None\<rparr>) (tcbFault_update (\<lambda>_. None) tcb')
 2. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_fault := None\<rparr>) = getF tcb
 3. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbFault_update (\<lambda>_. None) tcb) = getF tcb
 4. \<And>tcb'. exst_same tcb' (tcbFault_update (\<lambda>_. None) tcb')
 5. \<And>s. (einvs and st_tcb_at awaiting_reply t) s \<Longrightarrow> tcb_at t s
 6. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> tcb_at' t s
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 8. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 9. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_fault := None\<rparr>) = getF tcb
 2. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbFault_update (\<lambda>_. None) tcb) = getF tcb
 3. \<And>tcb'. exst_same tcb' (tcbFault_update (\<lambda>_. None) tcb')
 4. \<And>s. (einvs and st_tcb_at awaiting_reply t) s \<Longrightarrow> tcb_at t s
 5. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> tcb_at' t s
 6. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 7. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 8. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbFault_update (\<lambda>_. None) tcb) = getF tcb
 2. \<And>tcb'. exst_same tcb' (tcbFault_update (\<lambda>_. None) tcb')
 3. \<And>s. (einvs and st_tcb_at awaiting_reply t) s \<Longrightarrow> tcb_at t s
 4. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> tcb_at' t s
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 6. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 7. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tcb'. exst_same tcb' (tcbFault_update (\<lambda>_. None) tcb')
 2. \<And>s. (einvs and st_tcb_at awaiting_reply t) s \<Longrightarrow> tcb_at t s
 3. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> tcb_at' t s
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 5. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 6. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. (einvs and st_tcb_at awaiting_reply t) s \<Longrightarrow> tcb_at t s
 2. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> tcb_at' t s
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 4. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 5. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. (invs' and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> tcb_at' t s
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 3. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 4. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od)
 2. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 3. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. einvs and st_tcb_at awaiting_reply t\<rbrace>
 2. \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs' and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (do cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (do x <- getCTE (t + 2 ^ cte_level_bits * 2);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres (?r'207 rv rv') (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (get_cap (t, tcb_cnode_index 2)) (getCTE (t + 2 ^ cte_level_bits * 2))
 2. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; ?r'207 rv rv' cap rv'a\<rbrakk> \<Longrightarrow> corres dc (?Q207 rv rv' cap) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od))
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?Q207 rv rv'\<rbrace>
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres (?r'207 rv rv') (?Q212 rv rv') (?Q'212 rv rv') (get_cap (t, tcb_cnode_index 2)) (getCTE (t + 2 ^ cte_level_bits * 2))
 2. \<And>rv rv' s. \<lbrakk>dc rv rv'; (einvs and st_tcb_at awaiting_reply t) s\<rbrakk> \<Longrightarrow> ?Q212 rv rv' s
 3. \<And>rv rv' s. \<lbrakk>dc rv rv'; (invs' and st_tcb_at' awaiting_reply' t) s\<rbrakk> \<Longrightarrow> ?Q'212 rv rv' s
 4. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; ?r'207 rv rv' cap rv'a\<rbrakk> \<Longrightarrow> corres dc (?Q207 rv rv' cap) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od))
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?Q207 rv rv'\<rbrace>
 6. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' s. \<lbrakk>dc rv rv'; (einvs and st_tcb_at awaiting_reply t) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s
 2. \<And>rv rv' s. \<lbrakk>dc rv rv'; (invs' and st_tcb_at' awaiting_reply' t) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 3. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; cap_relation cap (cteCap rv'a)\<rbrakk> \<Longrightarrow> corres dc (?Q207 rv rv' cap) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od))
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?Q207 rv rv'\<rbrace>
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' s. \<lbrakk>dc rv rv'; (invs' and st_tcb_at' awaiting_reply' t) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 2. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; cap_relation cap (cteCap rv'a)\<rbrakk> \<Longrightarrow> corres dc (?Q207 rv rv' cap) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od))
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?Q207 rv rv'\<rbrace>
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; cap_relation cap (cteCap rv'a)\<rbrakk> \<Longrightarrow> corres dc (?Q207 rv rv' cap) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od))
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?Q207 rv rv'\<rbrace>
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>einvs and st_tcb_at awaiting_reply t\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?Q207 rv rv'\<rbrace>
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace>
 3. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; cap_relation cap (cteCap rv'a)\<rbrakk> \<Longrightarrow> corres dc (?Q207 rv rv' cap) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od)) proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>invs' and st_tcb_at' awaiting_reply' t\<rbrace> getCTE (t + 2 ^ cte_level_bits * 2) \<lbrace>?Q'207 rv rv'\<rbrace>
 2. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; cap_relation cap (cteCap rv'a)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (?Q'207 rv rv' rv'a) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od)) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' cap rv'a. \<lbrakk>dc rv rv'; cap_relation cap (cteCap rv'a)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = rv'a) (t + 2 ^ cte_level_bits * 2) s) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode rv'a) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode rv'a)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode rv'a))
od)) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (do descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)
od) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' cap cte descs s s'. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (s, s') \<in> state_relation; ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) s; (invs' and st_tcb_at' awaiting_reply' t) s' \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s'\<rbrakk> \<Longrightarrow> \<exists>r. cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r)
 2. \<And>rv rv' cap cte descs. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); \<exists>r. cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r)\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 3. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); \<exists>r. cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r)\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' cap cte descs s s'. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); \<exists>r. cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); (s, s') \<in> state_relation; ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) s; (invs' and st_tcb_at' awaiting_reply' t) s' \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s'\<rbrakk> \<Longrightarrow> (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer)
 2. \<And>rv rv' cap cte descs. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); \<exists>r. cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer)\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 3. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); \<exists>r. cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer)\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs r. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r)\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs r. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' cap cte descs r s s'. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; (s, s') \<in> state_relation; ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) s; (invs' and st_tcb_at' awaiting_reply' t) s' \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s'\<rbrakk> \<Longrightarrow> \<exists>sl. descs = {sl}
 2. \<And>rv rv' cap cte descs r. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; \<exists>sl. descs = {sl}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 3. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs r. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; \<exists>sl. descs = {sl}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs r sl. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; descs = {sl}; sl \<in> descs\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' cap cte descs r sl s s'. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; descs = {sl}; sl \<in> descs; (s, s') \<in> state_relation; ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) s; (invs' and st_tcb_at' awaiting_reply' t) s' \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl
 2. \<And>rv rv' cap cte descs r sl. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; descs = {sl}; sl \<in> descs; mdbNext (cteMDBNode cte) = cte_map sl\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 3. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (4 subgoals):
 1. \<And>cte r a b s s'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); (s, s') \<in> state_relation; invs s; invs' s'; valid_list s; st_tcb_at' awaiting_reply' t s'; cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s'; valid_sched s; tcb_at t s; cte_wp_at (\<lambda>c. c = cap.ReplyCap t True r) (t, tcb_cnode_index 2) s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map (a, b)
 2. \<And>rv rv' cap cte descs r sl. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; descs = {sl}; sl \<in> descs; mdbNext (cteMDBNode cte) = cte_map sl\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 3. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cap cte descs r sl. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer); cap = cap.ReplyCap t True r \<and> cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs \<noteq> {}; descs = {sl}; sl \<in> descs; mdbNext (cteMDBNode cte) = cte_map sl\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) and (\<lambda>s. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = descs)) (\<lambda>s. (invs' and st_tcb_at' awaiting_reply' t) s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (when (descs \<noteq> {}) (do y <- assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od)) (when (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode cte)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode cte))
od))
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>cte descs r sl. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (\<lambda>c. c = cap.ReplyCap t True r) (t, tcb_cnode_index 2) s) and (\<lambda>s. descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl})) (\<lambda>s. invs' s \<and> st_tcb_at' awaiting_reply' t s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s) (cap_delete_one sl) (do y <- stateAssert (cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<and> \<not> capReplyMaster (cteCap c)) (cte_map sl)) [];
cteDeleteOne (cte_map sl)
od)
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (5 subgoals):
 1. \<And>cte descs r sl. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl\<rbrakk> \<Longrightarrow> corres dc (?Q454 cte descs r sl) (?Q'454 cte descs r sl) (cap_delete_one sl) (do y <- stateAssert (cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<and> \<not> capReplyMaster (cteCap c)) (cte_map sl)) [];
cteDeleteOne (cte_map sl)
od)
 2. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; ((\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (\<lambda>c. c = cap.ReplyCap t True r) (t, tcb_cnode_index 2) s) and (\<lambda>s. descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl})) s\<rbrakk> \<Longrightarrow> ?Q454 cte descs r sl s
 3. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; invs' s \<and> st_tcb_at' awaiting_reply' t s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s\<rbrakk> \<Longrightarrow> ?Q'454 cte descs r sl s
 4. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (5 subgoals):
 1. \<And>cte descs r sl s s'. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; (s, s') \<in> state_relation; (einvs and cte_wp_at can_fast_finalise sl) s; \<exists>r'. cte_wp_at ((=) (cap.ReplyCap t False r')) sl s; (invs' and cte_wp_at' (\<lambda>_. True) (cte_map sl)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<and> \<not> capReplyMaster (cteCap c)) (cte_map sl) s'
 2. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; ((\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (\<lambda>c. c = cap.ReplyCap t True r) (t, tcb_cnode_index 2) s) and (\<lambda>s. descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl})) s\<rbrakk> \<Longrightarrow> (einvs and cte_wp_at can_fast_finalise sl and (\<lambda>s. \<exists>r'. cte_wp_at ((=) (cap.ReplyCap t False r')) sl s)) s
 3. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; invs' s \<and> st_tcb_at' awaiting_reply' t s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map sl)) s
 4. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (4 subgoals):
 1. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; ((\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (\<lambda>c. c = cap.ReplyCap t True r) (t, tcb_cnode_index 2) s) and (\<lambda>s. descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl})) s\<rbrakk> \<Longrightarrow> (einvs and cte_wp_at can_fast_finalise sl and (\<lambda>s. \<exists>r'. cte_wp_at ((=) (cap.ReplyCap t False r')) sl s)) s
 2. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; invs' s \<and> st_tcb_at' awaiting_reply' t s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map sl)) s
 3. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (3 subgoals):
 1. \<And>cte descs r sl s. \<lbrakk>cte_map sl \<noteq> nullPointer; cteCap cte = capability.ReplyCap t True (AllowGrant \<in> r); descs = {sl}; mdbNext (cteMDBNode cte) = cte_map sl; invs' s \<and> st_tcb_at' awaiting_reply' t s \<and> cte_wp_at' (\<lambda>c. c = cte) (t + 2 ^ cte_level_bits * 2) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map sl)) s
 2. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' cap cte s. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' cap cte. \<lbrakk>dc rv rv'; cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (einvs and st_tcb_at awaiting_reply t) s \<and> cte_wp_at (\<lambda>c. c = cap) (t, tcb_cnode_index 2) s) (gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt)) proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (einvs and st_tcb_at awaiting_reply t) (invs' and st_tcb_at' awaiting_reply' t) (reply_cancel_ipc t) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od)

goal:
No subgoals!