theory CNodeInv_R

lemma cteRevoke_IRQInactive':
  "s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke x
  \<lbrace>\<lambda>_. \<top>\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" proof (induct rule: cteRevoke.induct) case (1 p s') show ?case apply (subst cteRevoke.simps) apply (wp "1.hyps" unlessE_wp whenE_wp preemptionPoint_IRQInactive_spec
              cteDelete_IRQInactive cteDelete_irq_states' getCTE_wp')+ apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>valid_irq_states'\<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>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> ((isNullCap $ cteCap cte) \<or> (mdbNext $ cteMDBNode cte) = nullPointer \<longrightarrow> True) \<and> (\<not> ((isNullCap $ cteCap cte) \<or> (mdbNext $ cteMDBNode cte) = nullPointer) \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) (mdbNext $ cteMDBNode cte) s \<longrightarrow> (cte `~isMDBParentOf~` ctea \<longrightarrow> valid_irq_states' s \<and> valid_irq_states' s) \<and> (\<not> cte `~isMDBParentOf~` ctea \<longrightarrow> True))) proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke p \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>

goal:
No subgoals!