theory Finalise_R

lemma emptySlot_valid_irq_handlers'[wp]:
  "\<lbrace>\<lambda>s. valid_irq_handlers' s
          \<and> (\<forall>sl'. info \<noteq> NullCap \<longrightarrow> sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)\<rbrace>
     emptySlot sl info
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: emptySlot_def case_Null_If) apply (wp | wpc)+ apply (unfold valid_irq_handlers'_def irq_issued'_def) apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of
          | wps clearUntypedFreeIndex_ksInterruptState)+ apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of ran_def modify_map_def
                 split: option.split) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (\<forall>sl'. info \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)\<rbrace> emptySlot sl info \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (info \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info))\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion info
od
od \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y newCTE ya yb yc. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B11 y newCTE ya yb yc\<rbrace> updateMDB sl (const nullMDBNode) \<lbrace>\<lambda>yd s. valid_irq_handlers' s \<and> (info \<noteq> capability.NullCap \<longrightarrow> info \<notin> ran (cteCaps_of s))\<rbrace>
 2. \<And>y newCTE ya yb. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B10 y newCTE ya yb\<rbrace> updateCap sl capability.NullCap \<lbrace>?B11 y newCTE ya yb\<rbrace>
 3. \<And>y newCTE ya. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B9 y newCTE ya\<rbrace> updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb)) \<lbrace>?B10 y newCTE ya\<rbrace>
 4. \<And>y newCTE. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?R7 y newCTE\<rbrace> updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE))) \<lbrace>?B9 y newCTE\<rbrace>
 5. \<And>y. \<lbrace>?B5 y\<rbrace> getCTE sl \<lbrace>\<lambda>newCTE s. (cteCap newCTE = capability.NullCap \<longrightarrow> valid_irq_handlers' s) \<and> (cteCap newCTE \<noteq> capability.NullCap \<longrightarrow> ?R7 y newCTE s)\<rbrace>
 6. \<lbrace>?Q4\<rbrace> clearUntypedFreeIndex sl \<lbrace>?B5\<rbrace>
 7. \<And>s. valid_irq_handlers' s \<and> (info \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)) \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>y newCTE ya yb yc. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B11 y newCTE ya yb yc\<rbrace> updateMDB sl (const nullMDBNode) \<lbrace>\<lambda>yd s. (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> (info \<noteq> capability.NullCap \<longrightarrow> info \<notin> ran (cteCaps_of s))\<rbrace>
 2. \<And>y newCTE ya yb. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B10 y newCTE ya yb\<rbrace> updateCap sl capability.NullCap \<lbrace>?B11 y newCTE ya yb\<rbrace>
 3. \<And>y newCTE ya. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B9 y newCTE ya\<rbrace> updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb)) \<lbrace>?B10 y newCTE ya\<rbrace>
 4. \<And>y newCTE. cteCap newCTE \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?R7 y newCTE\<rbrace> updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE))) \<lbrace>?B9 y newCTE\<rbrace>
 5. \<And>y. \<lbrace>?B5 y\<rbrace> getCTE sl \<lbrace>\<lambda>newCTE s. (cteCap newCTE = capability.NullCap \<longrightarrow> (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)) \<and> (cteCap newCTE \<noteq> capability.NullCap \<longrightarrow> ?R7 y newCTE s)\<rbrace>
 6. \<lbrace>?Q4\<rbrace> clearUntypedFreeIndex sl \<lbrace>?B5\<rbrace>
 7. \<And>s. (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> (info \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)) \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> (info \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)) \<Longrightarrow> case cteCaps_of s sl of None \<Rightarrow> True | Some cap \<Rightarrow> (cap = capability.NullCap \<longrightarrow> (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (\<forall>cap\<in>ran (modify_map (cteCaps_of s) sl (K capability.NullCap)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> (info \<noteq> capability.NullCap \<longrightarrow> info \<notin> ran (modify_map (cteCaps_of s) sl (K capability.NullCap)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a irq z. \<lbrakk>\<forall>cap. (\<exists>a z. ctes_of s a = Some z \<and> cteCap z = cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); info \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> sl \<longrightarrow> (\<forall>z. ctes_of s sl' = Some z \<longrightarrow> cteCap z \<noteq> info)); ctes_of s sl = Some x2; cteCap x2 \<noteq> capability.NullCap; a \<noteq> sl; ctes_of s a = Some z; cteCap z = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!