theory Finalise_R

lemma cteDeleteOne_ct_not_ksQ:
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   cteDeleteOne slot
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: cteDeleteOne_def unless_def split_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (case_tac "\<forall>final. finaliseCap (cteCap cte) final True = fail") apply (simp add: finaliseCapTrue_standin_simple_def) apply wp apply (clarsimp) apply (wp emptySlot_cteCaps_of hoare_lift_Pf2 [OF emptySlot_ksRQ emptySlot_ct]) apply (simp add: cteCaps_of_def) apply (wp (once) hoare_drop_imps) apply (wp finaliseCapTrue_standin_ct_not_ksQ isFinalCapability_inv)+ apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<forall>final. global.finaliseCap (cteCap cte) final True = fail \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>cte. \<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail) \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<forall>final. global.finaliseCap (cteCap cte) final True = fail \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
fail
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>cte. \<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail) \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte s. \<lbrakk>\<forall>final. global.finaliseCap (cteCap cte) final True = fail; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (if cteCap cte \<noteq> capability.NullCap then \<lambda>s. True else (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s
 2. \<And>cte. \<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail) \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail) \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte final. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B18 cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>\<lambda>pa s. capRemovable (fst pa) slot \<and> snd pa = capability.NullCap \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>cte. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 cte\<rbrace> isFinalCapability cte \<lbrace>?B18 cte\<rbrace>
 3. \<And>cte s. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (if cteCap cte \<noteq> capability.NullCap then ?Q17 cte else (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s proof (prove)
goal (3 subgoals):
 1. \<And>cte final. \<lbrakk>\<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B18 cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>\<lambda>pa s. capRemovable (fst pa) slot \<and> snd pa = capability.NullCap \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>cte. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 cte\<rbrace> isFinalCapability cte \<lbrace>?B18 cte\<rbrace>
 3. \<And>cte s. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (if cteCap cte \<noteq> capability.NullCap then ?Q17 cte else (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s proof (prove)
goal (3 subgoals):
 1. \<And>cte final. \<lbrakk>\<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B18 cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>cte. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 cte\<rbrace> isFinalCapability cte \<lbrace>?B18 cte\<rbrace>
 3. \<And>cte s. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (if cteCap cte \<noteq> capability.NullCap then ?Q17 cte else (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s proof (prove)
goal (1 subgoal):
 1. \<And>cte s. \<lbrakk>\<not> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail); (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (if cteCap cte \<noteq> capability.NullCap then invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) else (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s proof (prove)
goal:
No subgoals!