theory Ipc_R

lemma cteDeleteOne_reply_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p and
    cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot\<rbrace>
   cteDeleteOne slot
   \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp add: cteDeleteOne_def ex_nonz_cap_to'_def unless_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (rule hoare_assume_pre) apply (subgoal_tac "isReplyCap (cteCap cte)") apply (wp hoare_vcg_ex_lift emptySlot_cte_wp_cap_other isFinalCapability_inv
        | clarsimp simp: finaliseCap_def isCap_simps | simp
        | wp (once) hoare_drop_imps)+ apply (fastforce simp: cte_wp_at_ctes_of) apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)) s \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte s. \<lbrakk>(cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)) s; isReplyCap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace>
 2. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)) s \<Longrightarrow> isReplyCap (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>cte s sa v0 v1 v2 cref crefa. \<lbrakk>cteCap cte = capability.ReplyCap v0 v1 v2; cte_wp_at' (\<lambda>c. c = cte) slot s; cte_wp_at' (\<lambda>c. c = cte) slot sa; cte_wp_at' (\<lambda>c. \<exists>v0 v1 v2. cteCap c = capability.ReplyCap v0 v1 v2) slot s; cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s; cte_wp_at' (\<lambda>c. \<exists>v0 v1 v2. cteCap c = capability.ReplyCap v0 v1 v2) slot sa; cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) crefa sa\<rbrakk> \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) x sa \<and> x \<noteq> slot
 2. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)) s \<Longrightarrow> isReplyCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) slot and ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c)) slot)) s \<Longrightarrow> isReplyCap (cteCap cte) proof (prove)
goal:
No subgoals!