theory Syscall_R

lemma deleteCallerCap_corres:
  "corres dc (einvs and tcb_at t) (invs' and tcb_at' t)
     (delete_caller_cap t)
     (deleteCallerCap t)" apply (simp add: delete_caller_cap_def deleteCallerCap_def
                   getThreadCallerSlot_map) apply (rule corres_guard_imp) apply (rule_tac P'="cte_at' (cte_map (t, tcb_cnode_index 3))" in corres_symb_exec_r_conj) apply (rule_tac F="isReplyCap rv \<or> rv = capability.NullCap"
             and P="cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3)
                 and einvs"
             and P'="invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv)
                 (cte_map (t, tcb_cnode_index 3))" in corres_req) apply (clarsimp simp: cte_wp_at_caps_of_state state_relation_def) apply (drule caps_of_state_cteD) apply (drule(1) pspace_relation_cte_wp_at, clarsimp+) apply (clarsimp simp: cte_wp_at_ctes_of is_reply_cap_relation cap_relation_NullCapI) apply simp apply (rule corres_guard_imp, rule cap_delete_one_corres) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) apply (auto simp: can_fast_finalise_def)[1] apply (clarsimp simp: cte_wp_at_ctes_of) apply ((wp getCTE_wp')+ | simp add: getSlotCap_def)+ apply clarsimp apply (frule tcb_at_cte_at[where ref="tcb_cnode_index 3"]) apply clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule tcb_cap_valid_caps_of_stateD, clarsimp) apply (drule(1) tcb_cnode_index_3_reply_or_null) apply (auto simp: can_fast_finalise_def is_cap_simps
              intro: tcb_at_cte_at_map tcb_at_cte_at)[1] apply clarsimp apply (frule_tac offs="tcb_cnode_index 3" in tcb_at_cte_at_map) apply (simp add: tcb_cap_cases_def) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (delete_caller_cap t) (deleteCallerCap t) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (cap_delete_one (t, tcb_cnode_index 3)) (do callerCap <- getSlotCap (cte_map (t, tcb_cnode_index 3));
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (cap_delete_one (t, tcb_cnode_index 3)) (do callerCap <- getSlotCap (cte_map (t, tcb_cnode_index 3));
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. corres dc ?Q (?R'4 rv) (cap_delete_one (t, tcb_cnode_index 3)) (do y <- assert (isReplyCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 2. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>?R'4\<rbrace>
 3. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> ?Q s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s s'. \<lbrakk>(s, s') \<in> state_relation; (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) s'\<rbrakk> \<Longrightarrow> isReplyCap rv \<or> rv = capability.NullCap
 2. \<And>rv. isReplyCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) (cap_delete_one (t, tcb_cnode_index 3)) (do y <- assert (isReplyCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 3. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 4. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s s' cap. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs' s'; cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3)) s'; ekheap_relation (ekheap s) (ksPSpace s'); invs s; caps_of_state s (t, tcb_cnode_index 3) = Some cap; is_reply_cap cap \<or> cap = cap.NullCap; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (ksCurDomain s') (kheap s) (ksCurThread s') (ksIdleThread s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; rv \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> isReplyCap rv
 2. \<And>rv. isReplyCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) (cap_delete_one (t, tcb_cnode_index 3)) (do y <- assert (isReplyCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 3. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 4. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s s' cap. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs' s'; cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3)) s'; ekheap_relation (ekheap s) (ksPSpace s'); invs s; is_reply_cap cap \<or> cap = cap.NullCap; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (ksCurDomain s') (kheap s) (ksCurThread s') (ksIdleThread s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; rv \<noteq> capability.NullCap; cte_wp_at ((=) cap) (t, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> isReplyCap rv
 2. \<And>rv. isReplyCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) (cap_delete_one (t, tcb_cnode_index 3)) (do y <- assert (isReplyCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 3. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 4. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s s' cap. \<lbrakk>invs' s'; cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3)) s'; ekheap_relation (ekheap s) (ksPSpace s'); invs s; is_reply_cap cap \<or> cap = cap.NullCap; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (ksCurDomain s') (kheap s) (ksCurThread s') (ksIdleThread s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; rv \<noteq> capability.NullCap; cte_wp_at ((=) cap) (t, tcb_cnode_index 3) s; cte_wp_at' (\<lambda>cte. cap_relation cap (cteCap cte)) (cte_map (t, tcb_cnode_index 3)) s'\<rbrakk> \<Longrightarrow> isReplyCap rv
 2. \<And>rv. isReplyCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) (cap_delete_one (t, tcb_cnode_index 3)) (do y <- assert (isReplyCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 3. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 4. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. isReplyCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) (cap_delete_one (t, tcb_cnode_index 3)) (do y <- assert (isReplyCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od)
 2. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 3. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. isReplyCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) (cap_delete_one (t, tcb_cnode_index 3)) (cteDeleteOne (cte_map (t, tcb_cnode_index 3)))
 2. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 3. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s. \<lbrakk>isReplyCap rv \<or> rv = capability.NullCap; (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s\<rbrakk> \<Longrightarrow> (einvs and cte_wp_at can_fast_finalise (t, tcb_cnode_index 3)) s
 2. \<And>rv s. \<lbrakk>isReplyCap rv \<or> rv = capability.NullCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3))) s
 3. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 4. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s cap. \<lbrakk>isReplyCap rv \<or> rv = capability.NullCap; invs s; caps_of_state s (t, tcb_cnode_index 3) = Some cap; (\<exists>x R. cap = cap.ReplyCap x False R) \<or> cap = cap.NullCap; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 2. \<And>rv s. \<lbrakk>isReplyCap rv \<or> rv = capability.NullCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3))) s
 3. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 4. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>isReplyCap rv \<or> rv = capability.NullCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3))) s
 2. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 3. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'4\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (t, tcb_cnode_index 3))\<rbrace>
 2. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s'\<rbrace> getSlotCap (cte_map (t, tcb_cnode_index 3)) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 3. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s') (getSlotCap (cte_map (t, tcb_cnode_index 3)))
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) and einvs) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<Longrightarrow> cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs s; valid_list s; valid_sched s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>invs s; valid_list s; valid_sched s; tcb_at t s\<rbrakk> \<Longrightarrow> tcb_cnode_index 3 \<in> dom tcb_cap_cases
 2. \<And>s. \<lbrakk>invs s; valid_list s; valid_sched s; tcb_at t s; cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs s; valid_list s; valid_sched s; tcb_at t s; cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_reply_cap cap \<or> cap = cap.NullCap) (t, tcb_cnode_index 3) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; valid_list s; valid_sched s; tcb_at t s; caps_of_state s (t, tcb_cnode_index 3) = Some cap; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> is_reply_cap cap
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; valid_list s; valid_sched s; tcb_at t s; caps_of_state s (t, tcb_cnode_index 3) = Some cap; cap \<noteq> cap.NullCap; tcb_cap_valid cap (t, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> is_reply_cap cap
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; valid_list s; valid_sched s; caps_of_state s (t, tcb_cnode_index 3) = Some cap; cap \<noteq> cap.NullCap; tcb_cap_valid cap (t, tcb_cnode_index 3) s; is_reply_cap cap \<or> cap = cap.NullCap\<rbrakk> \<Longrightarrow> is_reply_cap cap
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) and (\<lambda>s. invs' s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; tcb_at' t s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs' s; tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_cnode_index 3 \<in> dom tcb_cap_cases
 2. \<And>s. \<lbrakk>invs' s; tcb_at' t s; cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; tcb_at' t s; cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s \<and> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (cte_map (t, tcb_cnode_index 3)) s) proof (prove)
goal:
No subgoals!