theory IpcCancel_AI

lemma reply_cancel_ipc_invs:
  assumes delete: "\<And>p. \<lbrace>invs and emptyable p\<rbrace>
                        (cap_delete_one p :: (unit,'z::state_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>"
  shows           "\<lbrace>invs\<rbrace> (reply_cancel_ipc t :: (unit,'z::state_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: reply_cancel_ipc_def) apply (wp delete) apply (rule_tac Q="\<lambda>rv. invs" in hoare_post_imp) apply (fastforce simp: emptyable_def dest: reply_slot_not_descendant) apply (wp thread_set_invs_trivial) apply (auto simp: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> 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>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>y s. (if (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s \<noteq> {} then \<lambda>sa. (\<exists>a b. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = {(a, b)}) \<longrightarrow> (\<forall>x\<in>(descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s. (invs and emptyable x) sa) else invs) s\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. invs s \<Longrightarrow> (if (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s \<noteq> {} then \<lambda>sa. (\<exists>a b. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = {(a, b)}) \<longrightarrow> (\<forall>x\<in>(descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s. (invs and emptyable x) sa) else invs) s
 2. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_fault := None\<rparr>) = getF tcb
 2. \<And>tcb. tcb_state (tcb\<lparr>tcb_fault := None\<rparr>) = tcb_state tcb
 3. \<And>tcb. tcb_bound_notification (tcb\<lparr>tcb_fault := None\<rparr>) = tcb_bound_notification tcb
 4. \<And>tcb. tcb_iarch (tcb\<lparr>tcb_fault := None\<rparr>) = tcb_iarch tcb
 5. \<And>tcb. tcb_ipc_buffer (tcb\<lparr>tcb_fault := None\<rparr>) = tcb_ipc_buffer tcb \<or> tcb_ipc_buffer (tcb\<lparr>tcb_fault := None\<rparr>) = 0
 6. \<And>tcb. tcb_fault_handler (tcb\<lparr>tcb_fault := None\<rparr>) \<noteq> tcb_fault_handler tcb \<longrightarrow> length (tcb_fault_handler (tcb\<lparr>tcb_fault := None\<rparr>)) = word_bits
 7. \<And>tcb. tcb_fault (tcb\<lparr>tcb_fault := None\<rparr>) \<noteq> tcb_fault tcb \<longrightarrow> (case tcb_fault (tcb\<lparr>tcb_fault := None\<rparr>) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)
 8. \<And>tcb. tcb_arch_ref (tcb\<lparr>tcb_fault := None\<rparr>) = tcb_arch_ref tcb
 9. \<And>s. invs s \<Longrightarrow> invs s proof (prove)
goal:
No subgoals!