theory CNodeInv_R

lemma cteRevoke_preservation':
  assumes x: "\<And>ptr. \<lbrace>P\<rbrace> cteDelete ptr True \<lbrace>\<lambda>rv. P\<rbrace>"
  assumes y: "\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s"
  assumes irq: "irq_state_independent_H P"
  shows      "s \<turnstile> \<lbrace>P\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>" proof (induct rule: cteRevoke.induct) case (1 p s') show ?case apply (subst cteRevoke.simps) apply (wp "1.hyps") apply (wp x y preemptionPoint_inv hoare_drop_imps irq | clarsimp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>p s. (\<And>rv st rva sta rvb stb rvc stc rvd std. \<lbrakk>(Inr rv, st) \<in> fst ((withoutPreemption $ getCTE p) s); (Inr rva, sta) \<in> fst (returnOk (mdbNext $ cteMDBNode rv) st); \<not> ((isNullCap $ cteCap rv) \<or> rva = nullPointer); (Inr rvb, stb) \<in> fst ((withoutPreemption $ getCTE rva) sta); rv `~isMDBParentOf~` rvb; (Inr rvc, stc) \<in> fst (cteDelete rva True stb); (Inr rvd, std) \<in> fst (preemptionPoint stc)\<rbrakk> \<Longrightarrow> std \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((withoutPreemption $ getCTE p) s'); (Inr ?rva, ?sta) \<in> fst (returnOk (mdbNext $ cteMDBNode ?rv) ?st); \<not> ((isNullCap $ cteCap ?rv) \<or> ?rva = nullPointer); (Inr ?rvb, ?stb) \<in> fst ((withoutPreemption $ getCTE ?rva) ?sta); ?rv `~isMDBParentOf~` ?rvb; (Inr ?rvc, ?stc) \<in> fst (cteDelete ?rva True ?stb); (Inr ?rvd, ?std) \<in> fst (preemptionPoint ?stc)\<rbrakk> \<Longrightarrow> ?std \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>

goal (1 subgoal):
 1. \<And>p s. (\<And>rv st rva sta rvb stb rvc stc rvd std. \<lbrakk>(Inr rv, st) \<in> fst ((withoutPreemption $ getCTE p) s); (Inr rva, sta) \<in> fst (returnOk (mdbNext $ cteMDBNode rv) st); \<not> ((isNullCap $ cteCap rv) \<or> rva = nullPointer); (Inr rvb, stb) \<in> fst ((withoutPreemption $ getCTE rva) sta); rv `~isMDBParentOf~` rvb; (Inr rvc, stc) \<in> fst (cteDelete rva True stb); (Inr rvd, std) \<in> fst (preemptionPoint stc)\<rbrakk> \<Longrightarrow> std \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>P\<rbrace> doE cte <- withoutPreemption $ getCTE p;
nextPtr <- returnOk (mdbNext $ cteMDBNode cte);
unlessE ((isNullCap $ cteCap cte) \<or> nextPtr = nullPointer) $ doE nextCTE <- withoutPreemption $ getCTE nextPtr;
whenE (cte `~isMDBParentOf~` nextCTE) $ doE cteDelete nextPtr True;
preemptionPoint;
cteRevoke p
odE
odE
odE \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE p) s'); (Inr rva, s''a) \<in> fst (returnOk (mdbNext $ cteMDBNode rv) s''); \<not> ((isNullCap $ cteCap rv) \<or> rva = nullPointer); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE rva) s''a); rv `~isMDBParentOf~` rvb; (Inr rvc, s''c) \<in> fst (cteDelete rva True s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc\<rbrace> preemptionPoint \<lbrace>\<lambda>rvd. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE p) s'); (Inr rva, s''a) \<in> fst (returnOk (mdbNext $ cteMDBNode rv) s''); \<not> ((isNullCap $ cteCap rv) \<or> rva = nullPointer); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE rva) s''a); rv `~isMDBParentOf~` rvb\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P12 rv s'' rva s''a rvb\<rbrace> cteDelete rva True \<lbrace>?B13 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE p) s'); (Inr rva, s''a) \<in> fst (returnOk (mdbNext $ cteMDBNode rv) s''); \<not> ((isNullCap $ cteCap rv) \<or> rva = nullPointer)\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?P7 rv s'' rva\<rbrace> withoutPreemption $ getCTE rva \<lbrace>\<lambda>a b. (rv `~isMDBParentOf~` a \<longrightarrow> ?P12 rv s'' rva s''a a b) \<and> (\<not> rv `~isMDBParentOf~` a \<longrightarrow> P b)\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>rv s''. (Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE p) s') \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> returnOk (mdbNext $ cteMDBNode rv) \<lbrace>\<lambda>a b. ((isNullCap $ cteCap rv) \<or> a = nullPointer \<longrightarrow> P b) \<and> (\<not> ((isNullCap $ cteCap rv) \<or> a = nullPointer) \<longrightarrow> ?P7 rv s'' a b)\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. s' \<turnstile> \<lbrace>P\<rbrace> withoutPreemption $ getCTE p \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>P\<rbrace> cteRevoke p \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>

goal:
No subgoals!