kings-crown/FVELER_Isabelle huggingface dataset:
theory EmptyFail_H

lemma spec_empty_fail_unlessE':
  "\<lbrakk> \<not> P \<Longrightarrow> spec_empty_fail f s \<rbrakk> \<Longrightarrow> spec_empty_fail (unlessE P f) s" by (simp add:unlessE_def spec_empty_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> spec_empty_fail f s) \<Longrightarrow> spec_empty_fail (unlessE P f) s
theory EmptyFail_H

lemma cteRevoke_spec_empty_fail:
  notes spec_empty_fail_bindE'[wp_split]
  shows "spec_empty_fail (cteRevoke p) s" proof (induct rule: cteRevoke.induct) case (1 p s) show ?case apply (simp add: cteRevoke.simps) apply (wp spec_empty_whenE' spec_empty_fail_unlessE' | rule drop_spec_empty_fail, wp)+ apply (rule 1, auto simp add: in_monad) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (cteRevoke p) s 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> spec_empty_fail (cteRevoke p) std) \<Longrightarrow> spec_empty_fail (cteRevoke p) s 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> spec_empty_fail (cteRevoke p) ?std

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> spec_empty_fail (cteRevoke p) std) \<Longrightarrow> spec_empty_fail (cteRevoke p) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (cteRevoke p) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (doE cte <- liftE (getCTE p);
unlessE (cteCap cte = capability.NullCap \<or> mdbNext (cteMDBNode cte) = nullPointer) (doE nextCTE <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte nextCTE) (doE y <- cteDelete (mdbNext (cteMDBNode cte)) True;
y <- preemptionPoint;
cteRevoke p
odE)
odE)
odE) s proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b xc s'c. \<lbrakk>(Inr x, s') \<in> fst (liftE (getCTE p) s); \<not> (cteCap x = capability.NullCap \<or> mdbNext (cteMDBNode x) = nullPointer); (Inr xa, s'a) \<in> fst (liftE (getCTE (mdbNext (cteMDBNode x))) s'); isMDBParentOf x xa; (Inr xb, s'b) \<in> fst (cteDelete (mdbNext (cteMDBNode x)) True s'a); (Inr xc, s'c) \<in> fst (preemptionPoint s'b)\<rbrakk> \<Longrightarrow> spec_empty_fail (cteRevoke p) s'c proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (cteRevoke p) s

goal:
No subgoals!
theory EmptyFail_H

lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]:
  "\<lbrakk>empty_fail a; \<And>x. empty_fail (b x); \<And>x. empty_fail (c x);
    \<And>x. empty_fail (d x); \<And>x. empty_fail (e x)\<rbrakk>
   \<Longrightarrow> empty_fail (syscall a b c d e)" apply (simp add:syscall_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail a; \<And>x. empty_fail (b x); \<And>x. empty_fail (c x); \<And>x. empty_fail (d x); \<And>x. empty_fail (e x)\<rbrakk> \<Longrightarrow> empty_fail (Syscall_H.syscall a b c d e) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail a; \<And>x. empty_fail (b x); \<And>x. empty_fail (c x); \<And>x. empty_fail (d x); \<And>x. empty_fail (e x)\<rbrakk> \<Longrightarrow> empty_fail (doE rFault <- liftE a;
case rFault of Inl f \<Rightarrow> withoutPreemption $ b f | Inr a \<Rightarrow> doE rError <- withoutPreemption $ runExceptT $ c a;
case rError of Inl e \<Rightarrow> withoutPreemption $ d e | Inr b \<Rightarrow> e b
odE
odE) proof (prove)
goal:
No subgoals!
theory EmptyFail_H

lemma catchError_empty_fail[intro!, wp, simp]:
  "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catchError f g)" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>x. empty_fail (g x)\<rbrakk> \<Longrightarrow> empty_fail (catchError f g)
theory EmptyFail_H

lemma ThreadDecls_H_schedule_empty_fail[intro!, wp, simp]:
  "empty_fail schedule" apply (simp add: schedule_def) apply (clarsimp simp: scheduleChooseNewThread_def split: if_split | wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail ThreadDecls_H.schedule proof (prove)
goal (1 subgoal):
 1. empty_fail (do curThread <- getCurThread;
action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma st_tcb_at_neg':
  "(st_tcb_at' (\<lambda> ts. \<not> P ts) t s) = (tcb_at' t s \<and> \<not> st_tcb_at' P t s)" by (auto simp: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' (\<lambda>ts. \<not> P ts) t s = (tcb_at' t s \<and> \<not> st_tcb_at' P t s)
theory Orphanage

lemma st_tcb_at_neg2:
  "(\<not> st_tcb_at' P t s) = (st_tcb_at' (\<lambda> ts. \<not> P ts) t s \<or> \<not> tcb_at' t s)" by (auto simp: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> st_tcb_at' P t s) = (st_tcb_at' (\<lambda>ts. \<not> P ts) t s \<or> \<not> tcb_at' t s)
theory Orphanage

lemma st_tcb_at_double_neg':
  "(st_tcb_at' (\<lambda> ts. \<not> P ts \<and> \<not> Q ts) t s) =
   ((st_tcb_at' (\<lambda> ts. \<not> P ts) t s) \<and> (st_tcb_at' (\<lambda> ts. \<not> Q ts) t s))" apply (auto simp: pred_tcb_at'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' (\<lambda>ts. \<not> P ts \<and> \<not> Q ts) t s = (st_tcb_at' (\<lambda>ts. \<not> P ts) t s \<and> st_tcb_at' (\<lambda>ts. \<not> Q ts) t s) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma no_orphans_disj:
   "no_orphans = (\<lambda> s.
           \<forall> tcb_ptr. tcb_ptr = ksCurThread s \<or>
                      tcb_ptr : all_queued_tcb_ptrs s \<or>
                      \<not> typ_at' TCBT tcb_ptr s \<or>
                      st_tcb_at' (\<lambda> state. \<not> is_active_thread_state state) tcb_ptr s \<or>
                      ksSchedulerAction s = SwitchToThread tcb_ptr)" apply clarsimp apply (rule ext) apply (unfold no_orphans_def all_active_tcb_ptrs_def
                is_active_tcb_ptr_def st_tcb_at_neg' typ_at_tcb') apply (auto intro: pred_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans = (\<lambda>s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> all_queued_tcb_ptrs s \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) proof (prove)
goal (1 subgoal):
 1. no_orphans = (\<lambda>s. \<forall>tcb_ptr. typ_at' TCBT tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> all_queued_tcb_ptrs s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s = (\<forall>tcb_ptr. typ_at' TCBT tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> all_queued_tcb_ptrs s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> all_queued_tcb_ptrs s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) = (\<forall>tcb_ptr. tcb_at' tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> all_queued_tcb_ptrs s \<or> tcb_at' tcb_ptr s \<and> \<not> st_tcb_at' is_active_thread_state tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma st_tcb_at'_all_active_tcb_ptrs_lift:
  assumes "\<And>P P' t. \<lbrace>\<lambda>s. P (st_tcb_at' P' t s)\<rbrace> f \<lbrace>\<lambda>rv s. P (st_tcb_at' P' t s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (t \<in> all_active_tcb_ptrs s)\<rbrace> f \<lbrace>\<lambda>_ s. P (t \<in> all_active_tcb_ptrs s)\<rbrace>" by (clarsimp simp: all_active_tcb_ptrs_def)
     (rule st_tcb_at'_is_active_tcb_ptr_lift [OF assms])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (t \<in> all_active_tcb_ptrs s)\<rbrace> f \<lbrace>\<lambda>_ s. P (t \<in> all_active_tcb_ptrs s)\<rbrace>
theory Orphanage

lemma ksQ_all_queued_tcb_ptrs_lift:
  assumes "\<And>P p. \<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> f \<lbrace>\<lambda>rv s. P (ksReadyQueues s p)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (t \<in> all_queued_tcb_ptrs s)\<rbrace> f \<lbrace>\<lambda>_ s. P (t \<in> all_queued_tcb_ptrs s)\<rbrace>" apply (clarsimp simp: all_queued_tcb_ptrs_def) apply (rule_tac P=P in P_bool_lift) apply (wp hoare_vcg_ex_lift assms) apply (clarsimp) apply (wp hoare_vcg_all_lift assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (t \<in> all_queued_tcb_ptrs s)\<rbrace> f \<lbrace>\<lambda>_ s. P (t \<in> all_queued_tcb_ptrs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (\<exists>a b. t \<in> set (ksReadyQueues s (a, b)))\<rbrace> f \<lbrace>\<lambda>_ s. P (\<exists>a b. t \<in> set (ksReadyQueues s (a, b)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<exists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace> f \<lbrace>\<lambda>r s. \<exists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace>
 2. \<lbrace>\<lambda>s. \<nexists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace> f \<lbrace>\<lambda>r s. \<nexists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<nexists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace> f \<lbrace>\<lambda>r s. \<nexists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))\<rbrace> f \<lbrace>\<lambda>r s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma no_orphans_strg_almost:
   "no_orphans s \<longrightarrow> almost_no_orphans tcb_ptr s" unfolding no_orphans_def almost_no_orphans_def apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans s \<longrightarrow> almost_no_orphans tcb_ptr s proof (prove)
goal (1 subgoal):
 1. (\<forall>tcb_ptr. tcb_ptr \<in> all_active_tcb_ptrs s \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> all_queued_tcb_ptrs s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<longrightarrow> (\<forall>ptr. ptr = tcb_ptr \<or> (ptr \<in> all_active_tcb_ptrs s \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> ksSchedulerAction s = SwitchToThread ptr)) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma almost_no_orphans_disj:
   "almost_no_orphans tcb_ptr = (\<lambda> s.
           \<forall> ptr. ptr = ksCurThread s \<or>
                  ptr : all_queued_tcb_ptrs s \<or>
                  \<not> typ_at' TCBT ptr s \<or>
                  st_tcb_at' (\<lambda> thread_state. \<not> is_active_thread_state thread_state) ptr s \<or>
                  ptr = tcb_ptr \<or>
                  ksSchedulerAction s = SwitchToThread ptr)" apply clarsimp apply (rule ext) apply (unfold almost_no_orphans_def all_active_tcb_ptrs_def
                is_active_tcb_ptr_def st_tcb_at_neg' typ_at_tcb') apply (auto intro: pred_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. almost_no_orphans tcb_ptr = (\<lambda>s. \<forall>ptr. ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> \<not> typ_at' TCBT ptr s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr s \<or> ptr = tcb_ptr \<or> ksSchedulerAction s = SwitchToThread ptr) proof (prove)
goal (1 subgoal):
 1. almost_no_orphans tcb_ptr = (\<lambda>s. \<forall>ptr. typ_at' TCBT ptr s \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr s \<or> ptr = tcb_ptr \<or> ksSchedulerAction s = SwitchToThread ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. almost_no_orphans tcb_ptr s = (\<forall>ptr. typ_at' TCBT ptr s \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr s \<or> ptr = tcb_ptr \<or> ksSchedulerAction s = SwitchToThread ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>ptr. ptr = tcb_ptr \<or> (ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> ksSchedulerAction s = SwitchToThread ptr)) = (\<forall>ptr. tcb_at' ptr s \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> tcb_at' ptr s \<and> \<not> st_tcb_at' is_active_thread_state ptr s \<or> ptr = tcb_ptr \<or> ksSchedulerAction s = SwitchToThread ptr) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma no_orphans_update_simps[simp]:
  "no_orphans (gsCNodes_update f s) = no_orphans s"
  "no_orphans (gsUserPages_update g s) = no_orphans s"
  "no_orphans (gsUntypedZeroRanges_update h s) = no_orphans s" by (simp_all add: no_orphans_def all_active_tcb_ptrs_def
                    is_active_tcb_ptr_def all_queued_tcb_ptrs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans (gsCNodes_update f s) = no_orphans s &&& no_orphans (gsUserPages_update g s) = no_orphans s &&& no_orphans (gsUntypedZeroRanges_update h s) = no_orphans s
theory Orphanage

lemma no_orphans_ksReadyQueuesL1Bitmap_update[simp]:
  "no_orphans (ksReadyQueuesL1Bitmap_update f s) = no_orphans s" unfolding no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans (ksReadyQueuesL1Bitmap_update f s) = no_orphans s proof (prove)
goal (1 subgoal):
 1. (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (ksReadyQueuesL1Bitmap_update f s)} \<longrightarrow> tcb_ptr = ksCurThread (ksReadyQueuesL1Bitmap_update f s) \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (ksReadyQueuesL1Bitmap_update f s) priority)} \<or> ksSchedulerAction (ksReadyQueuesL1Bitmap_update f s) = SwitchToThread tcb_ptr) = (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksSchedulerAction s = SwitchToThread tcb_ptr)
theory Orphanage

lemma no_orphans_ksReadyQueuesL2Bitmap_update[simp]:
  "no_orphans (ksReadyQueuesL2Bitmap_update f s) = no_orphans s" unfolding no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans (ksReadyQueuesL2Bitmap_update f s) = no_orphans s proof (prove)
goal (1 subgoal):
 1. (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (ksReadyQueuesL2Bitmap_update f s)} \<longrightarrow> tcb_ptr = ksCurThread (ksReadyQueuesL2Bitmap_update f s) \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (ksReadyQueuesL2Bitmap_update f s) priority)} \<or> ksSchedulerAction (ksReadyQueuesL2Bitmap_update f s) = SwitchToThread tcb_ptr) = (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksSchedulerAction s = SwitchToThread tcb_ptr)
theory Orphanage

lemma no_orphans_ksIdle[simp]:
   "no_orphans (ksIdleThread_update f s) = no_orphans s" unfolding no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans (ksIdleThread_update f s) = no_orphans s proof (prove)
goal (1 subgoal):
 1. (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (ksIdleThread_update f s)} \<longrightarrow> tcb_ptr = ksCurThread (ksIdleThread_update f s) \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (ksIdleThread_update f s) priority)} \<or> ksSchedulerAction (ksIdleThread_update f s) = SwitchToThread tcb_ptr) = (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma no_orphans_ksWorkUnits [simp]:
   "no_orphans (ksWorkUnitsCompleted_update f s) = no_orphans s" unfolding no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans (ksWorkUnitsCompleted_update f s) = no_orphans s proof (prove)
goal (1 subgoal):
 1. (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (ksWorkUnitsCompleted_update f s)} \<longrightarrow> tcb_ptr = ksCurThread (ksWorkUnitsCompleted_update f s) \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (ksWorkUnitsCompleted_update f s) priority)} \<or> ksSchedulerAction (ksWorkUnitsCompleted_update f s) = SwitchToThread tcb_ptr) = (\<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma no_orphans_irq_state_independent[intro!, simp]:
  "no_orphans (s \<lparr>ksMachineState := ksMachineState s \<lparr> irq_state := f (irq_state (ksMachineState s)) \<rparr> \<rparr>)
   = no_orphans s" by (simp add: no_orphans_def all_active_tcb_ptrs_def
                all_queued_tcb_ptrs_def is_active_tcb_ptr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = no_orphans s
theory Orphanage

lemma almost_no_orphans_ksReadyQueuesL1Bitmap_update[simp]:
  "almost_no_orphans t (ksReadyQueuesL1Bitmap_update f s) = almost_no_orphans t s" unfolding almost_no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. almost_no_orphans t (ksReadyQueuesL1Bitmap_update f s) = almost_no_orphans t s proof (prove)
goal (1 subgoal):
 1. (\<forall>ptr. ptr = t \<or> (ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (ksReadyQueuesL1Bitmap_update f s)} \<longrightarrow> ptr = ksCurThread (ksReadyQueuesL1Bitmap_update f s) \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (ksReadyQueuesL1Bitmap_update f s) priority)} \<or> ksSchedulerAction (ksReadyQueuesL1Bitmap_update f s) = SwitchToThread ptr)) = (\<forall>ptr. ptr = t \<or> (ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksSchedulerAction s = SwitchToThread ptr))
theory Orphanage

lemma almost_no_orphans_ksReadyQueuesL2Bitmap_update[simp]:
  "almost_no_orphans t (ksReadyQueuesL2Bitmap_update f s) = almost_no_orphans t s" unfolding almost_no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. almost_no_orphans t (ksReadyQueuesL2Bitmap_update f s) = almost_no_orphans t s proof (prove)
goal (1 subgoal):
 1. (\<forall>ptr. ptr = t \<or> (ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (ksReadyQueuesL2Bitmap_update f s)} \<longrightarrow> ptr = ksCurThread (ksReadyQueuesL2Bitmap_update f s) \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (ksReadyQueuesL2Bitmap_update f s) priority)} \<or> ksSchedulerAction (ksReadyQueuesL2Bitmap_update f s) = SwitchToThread ptr)) = (\<forall>ptr. ptr = t \<or> (ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s} \<longrightarrow> ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksSchedulerAction s = SwitchToThread ptr))
theory Orphanage

lemma all_active_tcb_ptrs_queue [simp]:
  "all_active_tcb_ptrs (ksReadyQueues_update f s) = all_active_tcb_ptrs s" by (clarsimp simp: all_active_tcb_ptrs_def is_active_tcb_ptr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_active_tcb_ptrs (ksReadyQueues_update f s) = all_active_tcb_ptrs s
theory Orphanage

lemma setCTE_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   setCTE p cte
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (rule no_orphans_lift) apply (wp setCTE_typ_at' setCTE_pred_tcb_at')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tcb_ptr. \<lbrace>\<lambda>s. \<not> typ_at' TCBT tcb_ptr s\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. \<not> typ_at' TCBT tcb_ptr s\<rbrace>
 2. \<And>tcb_ptr. \<lbrace>\<lambda>s. tcb_ptr = ksCurThread s\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. tcb_ptr = ksCurThread s\<rbrace>
 3. \<And>P pa. \<lbrace>st_tcb_at' P pa\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. st_tcb_at' P pa\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!