kings-crown/FVELER_Isabelle huggingface dataset:
theory Orphanage

lemma setCTE_almost_no_orphans [wp]:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<rbrace>
   setCTE p cte
   \<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>" unfolding almost_no_orphans_disj all_queued_tcb_ptrs_def apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift setCTE_typ_at' setCTE_pred_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>almost_no_orphans tcb_ptr\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ptr. ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. \<forall>ptr. ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma asUser_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   asUser thread f
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding no_orphans_disj all_queued_tcb_ptrs_def apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> asUser thread f \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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\<rbrace> asUser thread f \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma threadSet_almost_no_orphans:
  "\<forall>tcb. \<not> is_active_thread_state (tcbState tcb) \<longrightarrow> \<not> is_active_thread_state (tcbState (F tcb)) \<Longrightarrow>
   \<lbrace> \<lambda>s. almost_no_orphans ptr s \<rbrace>
   threadSet F tptr
   \<lbrace> \<lambda>rv s. almost_no_orphans ptr s \<rbrace>" unfolding almost_no_orphans_disj all_queued_tcb_ptrs_def apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift threadSet_st_tcb_at2 | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>tcb. \<not> is_active_thread_state (tcbState tcb) \<longrightarrow> \<not> is_active_thread_state (tcbState (F tcb)) \<Longrightarrow> \<lbrace>almost_no_orphans ptr\<rbrace> threadSet F tptr \<lbrace>\<lambda>rv. almost_no_orphans ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>tcb. \<not> is_active_thread_state (tcbState tcb) \<longrightarrow> \<not> is_active_thread_state (tcbState (F tcb)) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>ptra. ptra = ksCurThread s \<or> ptra \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT ptra s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptra s \<or> ptra = ptr \<or> ksSchedulerAction s = SwitchToThread ptra\<rbrace> threadSet F tptr \<lbrace>\<lambda>rv s. \<forall>ptra. ptra = ksCurThread s \<or> ptra \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT ptra s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptra s \<or> ptra = ptr \<or> ksSchedulerAction s = SwitchToThread ptra\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setQueue_no_orphans_enq:
  "\<lbrace> \<lambda>s. no_orphans s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<rbrace>
   setQueue d prio qs
   \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" unfolding setQueue_def apply wp apply (clarsimp simp: no_orphans_def all_queued_tcb_ptrs_def
                  split: if_split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs\<rbrace> setQueue d prio qs \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, prio), qs)]\<rparr>) \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<Longrightarrow> no_orphans (s\<lparr>ksReadyQueues := ksReadyQueues s aLU [((d, prio), qs)]\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb_ptr. \<lbrakk>\<forall>tcb_ptr. tcb_ptr \<in> all_active_tcb_ptrs s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr; set (ksReadyQueues s (d, prio)) \<subseteq> set qs; tcb_ptr \<in> all_active_tcb_ptrs s; tcb_ptr \<noteq> ksCurThread s; sch_act_not tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>a b. (a = d \<and> b = prio \<longrightarrow> tcb_ptr \<in> set qs) \<and> ((a = d \<longrightarrow> b \<noteq> prio) \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (a, b))) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setQueue_almost_no_orphans_enq:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<and> tcb_ptr \<in> set qs \<rbrace>
   setQueue d prio qs
   \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" unfolding setQueue_def apply wp apply (clarsimp simp: no_orphans_def almost_no_orphans_def all_queued_tcb_ptrs_def
                  split: if_split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<and> tcb_ptr \<in> set qs\<rbrace> setQueue d prio qs \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<and> tcb_ptr \<in> set qs\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, prio), qs)]\<rparr>) \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<and> tcb_ptr \<in> set qs \<Longrightarrow> no_orphans (s\<lparr>ksReadyQueues := ksReadyQueues s aLU [((d, prio), qs)]\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb_ptra. \<lbrakk>\<forall>ptr. ptr \<in> all_active_tcb_ptrs s \<longrightarrow> ptr = tcb_ptr \<or> ptr = ksCurThread s \<or> (\<exists>a b. ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread ptr; set (ksReadyQueues s (d, prio)) \<subseteq> set qs; tcb_ptr \<in> set qs; tcb_ptra \<in> all_active_tcb_ptrs s; tcb_ptra \<noteq> ksCurThread s; sch_act_not tcb_ptra s\<rbrakk> \<Longrightarrow> \<exists>a b. (a = d \<and> b = prio \<longrightarrow> tcb_ptra \<in> set qs) \<and> ((a = d \<longrightarrow> b \<noteq> prio) \<longrightarrow> tcb_ptra \<in> set (ksReadyQueues s (a, b))) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setQueue_almost_no_orphans_enq_lift:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<rbrace>
   setQueue d prio qs
   \<lbrace> \<lambda>_ s. almost_no_orphans tcb_ptr s \<rbrace>" unfolding setQueue_def apply wp apply (clarsimp simp: almost_no_orphans_def all_queued_tcb_ptrs_def
                  split: if_split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs\<rbrace> setQueue d prio qs \<lbrace>\<lambda>_. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, prio), qs)]\<rparr>) \<lbrace>\<lambda>_. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. almost_no_orphans tcb_ptr s \<and> set (ksReadyQueues s (d, prio)) \<subseteq> set qs \<Longrightarrow> almost_no_orphans tcb_ptr (s\<lparr>ksReadyQueues := ksReadyQueues s aLU [((d, prio), qs)]\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ptr. \<lbrakk>\<forall>ptr. ptr \<in> all_active_tcb_ptrs s \<longrightarrow> ptr = tcb_ptr \<or> ptr = ksCurThread s \<or> (\<exists>a b. ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread ptr; set (ksReadyQueues s (d, prio)) \<subseteq> set qs; ptr \<in> all_active_tcb_ptrs s; ptr \<noteq> tcb_ptr; ptr \<noteq> ksCurThread s; sch_act_not ptr s\<rbrakk> \<Longrightarrow> \<exists>a b. (a = d \<and> b = prio \<longrightarrow> ptr \<in> set qs) \<and> ((a = d \<longrightarrow> b \<noteq> prio) \<longrightarrow> ptr \<in> set (ksReadyQueues s (a, b))) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedEnqueue_no_orphans[wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   tcbSchedEnqueue tcb_ptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding tcbSchedEnqueue_def apply (wp setQueue_no_orphans_enq threadSet_no_orphans | clarsimp simp: unless_def)+ apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+ apply (drule obj_at_ko_at') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> tcbSchedEnqueue tcb_ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do queued <- threadGet tcbQueued tcb_ptr;
unless queued $ do tdom <- threadGet tcbDomain tcb_ptr;
prio <- threadGet tcbPriority tcb_ptr;
queue <- getQueue tdom prio;
setQueue tdom prio $ tcb_ptr # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) tcb_ptr
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'29 False tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>rv s. set (ksReadyQueues s (tdom, rv)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tdom, rv)))\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>\<lambda>tdom s. no_orphans s \<and> ?P'29 queued tdom s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then no_orphans else ?Q3 queued\<rbrace>
 4. \<And>s. no_orphans s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; tcb_at' tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> set (ksReadyQueues s (tcbDomain t, tcbPriority ta)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; \<exists>ko. ko_at' ko tcb_ptr s \<and> True\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> set (ksReadyQueues s (tcbDomain t, tcbPriority ta)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedAppend_no_orphans[wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   tcbSchedAppend tcb_ptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding tcbSchedAppend_def apply (wp setQueue_no_orphans_enq threadSet_no_orphans | clarsimp simp: unless_def)+ apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+ apply (drule obj_at_ko_at') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> tcbSchedAppend tcb_ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do queued <- threadGet tcbQueued tcb_ptr;
unless queued $ do tdom <- threadGet tcbDomain tcb_ptr;
prio <- threadGet tcbPriority tcb_ptr;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [tcb_ptr];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) tcb_ptr
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'29 False tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>rv s. set (ksReadyQueues s (tdom, rv)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tdom, rv)))\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>\<lambda>tdom s. no_orphans s \<and> ?P'29 queued tdom s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then no_orphans else ?Q3 queued\<rbrace>
 4. \<And>s. no_orphans s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; tcb_at' tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> set (ksReadyQueues s (tcbDomain t, tcbPriority ta)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; \<exists>ko. ko_at' ko tcb_ptr s \<and> True\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> set (ksReadyQueues s (tcbDomain t, tcbPriority ta)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma ko_at_obj_at':
  "ko_at' ko p s \<and> P ko \<Longrightarrow> obj_at' P p s" unfolding  obj_at'_def apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko p s \<and> P ko \<Longrightarrow> obj_at' P p s proof (prove)
goal (1 subgoal):
 1. (\<exists>koa obj. ksPSpace s p = Some koa \<and> is_aligned p (objBitsKO koa) \<and> fst (projectKO koa s) = {(obj, s)} \<and> obj = ko \<and> ps_clear p (objBitsKO koa) s) \<and> P ko \<Longrightarrow> \<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma queued_in_queue:
  "\<lbrakk>valid_queues' s; ko_at' tcb tcb_ptr s; tcbQueued tcb\<rbrakk> \<Longrightarrow>
   \<exists> p. tcb_ptr \<in> set (ksReadyQueues s p)" unfolding valid_queues'_def apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) apply (drule_tac x="tcb_ptr" in spec) apply (drule mp) apply (rule ko_at_obj_at') apply (auto simp: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues' s; ko_at' tcb tcb_ptr s; tcbQueued tcb\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ko_at' tcb tcb_ptr s; tcbQueued tcb\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb; \<forall>p t. obj_at' (inQ (tcbDomain tcb) p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain tcb, p))\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb; \<forall>t. obj_at' (inQ (tcbDomain tcb) (tcbPriority tcb)) t s \<longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb))\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb; obj_at' (inQ (tcbDomain tcb) (tcbPriority tcb)) tcb_ptr s \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb))\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb\<rbrakk> \<Longrightarrow> obj_at' (inQ (tcbDomain tcb) (tcbPriority tcb)) tcb_ptr s
 2. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb; tcb_ptr \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb))\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb\<rbrakk> \<Longrightarrow> ko_at' ?ko9 tcb_ptr s \<and> inQ (tcbDomain tcb) (tcbPriority tcb) ?ko9
 2. \<lbrakk>ko_at' tcb tcb_ptr s; tcbQueued tcb; tcb_ptr \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb))\<rbrakk> \<Longrightarrow> \<exists>p. tcb_ptr \<in> set (ksReadyQueues s p) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedEnqueue_almost_no_orphans_lift:
  "\<lbrace> \<lambda>s. almost_no_orphans ptr s \<rbrace>
   tcbSchedEnqueue tcb_ptr
   \<lbrace> \<lambda>rv s. almost_no_orphans ptr s \<rbrace>" unfolding tcbSchedEnqueue_def apply (wp setQueue_almost_no_orphans_enq_lift threadSet_almost_no_orphans | clarsimp simp: unless_def)+ apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+ apply (drule obj_at_ko_at') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>almost_no_orphans ptr\<rbrace> tcbSchedEnqueue tcb_ptr \<lbrace>\<lambda>rv. almost_no_orphans ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>almost_no_orphans ptr\<rbrace> do queued <- threadGet tcbQueued tcb_ptr;
unless queued $ do tdom <- threadGet tcbDomain tcb_ptr;
prio <- threadGet tcbPriority tcb_ptr;
queue <- getQueue tdom prio;
setQueue tdom prio $ tcb_ptr # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) tcb_ptr
od
od \<lbrace>\<lambda>rv. almost_no_orphans ptr\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'29 False tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>rv s. set (ksReadyQueues s (tdom, rv)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tdom, rv)))\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>\<lambda>tdom s. almost_no_orphans ptr s \<and> ?P'29 queued tdom s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then almost_no_orphans ptr else ?Q3 queued\<rbrace>
 4. \<And>s. almost_no_orphans ptr s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>almost_no_orphans ptr s; tcb_at' tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> set (ksReadyQueues s (tcbDomain t, tcbPriority ta)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>almost_no_orphans ptr s; \<exists>ko. ko_at' ko tcb_ptr s \<and> True\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> set (ksReadyQueues s (tcbDomain t, tcbPriority ta)) \<subseteq> insert tcb_ptr (set (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma ssa_no_orphans:
  "\<lbrace> \<lambda>s. no_orphans s \<and>
     (\<forall>t. sch_act_not t s \<or> t : all_queued_tcb_ptrs s \<or> ksCurThread s = t) \<rbrace>
   setSchedulerAction sa
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setSchedulerAction_def no_orphans_disj all_queued_tcb_ptrs_def apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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) \<and> (\<forall>t. sch_act_not t s \<or> t \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksCurThread s = t)\<rbrace> modify (ksSchedulerAction_update (\<lambda>_. sa)) \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<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) \<and> (\<forall>t. sch_act_not t s \<or> t \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ksCurThread s = t) \<Longrightarrow> \<forall>tcb_ptr. tcb_ptr = ksCurThread (s\<lparr>ksSchedulerAction := sa\<rparr>) \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (s\<lparr>ksSchedulerAction := sa\<rparr>) priority)} \<or> \<not> typ_at' TCBT tcb_ptr (s\<lparr>ksSchedulerAction := sa\<rparr>) \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr (s\<lparr>ksSchedulerAction := sa\<rparr>) \<or> ksSchedulerAction (s\<lparr>ksSchedulerAction := sa\<rparr>) = SwitchToThread tcb_ptr proof (prove)
goal:
No subgoals!