theory KHeap_DP

lemma delete_cap_simple_wp:
 "\<lbrace>\<lambda>s. <ptr  \<mapsto>c cap  \<and>* R> s \<and> \<not> ep_related_cap cap\<rbrace>
    delete_cap_simple ptr
  \<lbrace>\<lambda>_. < ptr  \<mapsto>c NullCap \<and>* R>\<rbrace>" apply (clarsimp simp: delete_cap_simple_def is_final_cap_def) apply (wp unless_wp always_empty_wp fast_finalise_cap_non_ep_wp) apply clarsimp apply (frule opt_cap_sep_imp) apply (clarsimp, rule conjI) apply clarsimp apply (metis reset_cap_asid_simps2(1)) apply clarsimp apply (rule conjI) apply sep_solve apply (metis reset_cap_asid_ep_related_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (ptr \<mapsto>c cap \<and>* R) s \<and> \<not> ep_related_cap cap\<rbrace> delete_cap_simple ptr \<lbrace>\<lambda>_. cdl.lift (ptr \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (ptr \<mapsto>c cap \<and>* R) s \<and> \<not> ep_related_cap cap\<rbrace> do cap <- get_cap ptr;
unless (cap = NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
always_empty_slot ptr
od)
od \<lbrace>\<lambda>_. cdl.lift (ptr \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (ptr \<mapsto>c cap \<and>* R) s \<and> \<not> ep_related_cap cap \<Longrightarrow> opt_cap ptr s \<noteq> None \<longrightarrow> (if the (opt_cap ptr s) = NullCap then cdl.lift (ptr \<mapsto>c NullCap \<and>* R) else cdl.lift (ptr \<mapsto>c - \<and>* R) and K (\<not> ep_related_cap (the (opt_cap ptr s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap\<rbrakk> \<Longrightarrow> (the (opt_cap ptr s) = NullCap \<longrightarrow> (\<exists>y. opt_cap ptr s = Some y) \<longrightarrow> cdl.lift (ptr \<mapsto>c NullCap \<and>* R) s) \<and> (the (opt_cap ptr s) \<noteq> NullCap \<longrightarrow> (\<exists>y. opt_cap ptr s = Some y) \<longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> \<not> ep_related_cap (the (opt_cap ptr s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; \<exists>cap'. opt_cap ptr s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> (the (opt_cap ptr s) = NullCap \<longrightarrow> (\<exists>y. opt_cap ptr s = Some y) \<longrightarrow> cdl.lift (ptr \<mapsto>c NullCap \<and>* R) s) \<and> (the (opt_cap ptr s) \<noteq> NullCap \<longrightarrow> (\<exists>y. opt_cap ptr s = Some y) \<longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> \<not> ep_related_cap (the (opt_cap ptr s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> cap' = NullCap \<longrightarrow> cdl.lift (ptr \<mapsto>c NullCap \<and>* R) s
 2. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> \<not> ep_related_cap cap' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some NullCap; NullCap = reset_cap_asid cap\<rbrakk> \<Longrightarrow> cdl.lift (ptr \<mapsto>c NullCap \<and>* R) s
 2. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> \<not> ep_related_cap cap' proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> cap' \<noteq> NullCap \<longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> \<not> ep_related_cap cap' proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap; cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> \<not> ep_related_cap cap' proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap; cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (ptr \<mapsto>c - \<and>* R) s
 2. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap; cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<not> ep_related_cap cap' proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; opt_cap ptr s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap; cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<not> ep_related_cap cap' proof (prove)
goal:
No subgoals!