kings-crown/FVELER_Isabelle huggingface dataset:
theory Orphanage

lemma ssa_almost_no_orphans:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and>
     (\<forall>t. sch_act_not t s \<or> t : all_queued_tcb_ptrs s \<or> ksCurThread s = t) \<rbrace>
   setSchedulerAction (SwitchToThread tcb_ptr)
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setSchedulerAction_def no_orphans_disj almost_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. almost_no_orphans tcb_ptr s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)\<rbrace> setSchedulerAction (SwitchToThread tcb_ptr) \<lbrace>\<lambda>rv. no_orphans\<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) \<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>_. SwitchToThread tcb_ptr)) \<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>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) \<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_ptra. tcb_ptra = ksCurThread (s\<lparr>ksSchedulerAction := SwitchToThread tcb_ptr\<rparr>) \<or> tcb_ptra \<in> {tcb_ptra. \<exists>priority. tcb_ptra \<in> set (ksReadyQueues (s\<lparr>ksSchedulerAction := SwitchToThread tcb_ptr\<rparr>) priority)} \<or> \<not> typ_at' TCBT tcb_ptra (s\<lparr>ksSchedulerAction := SwitchToThread tcb_ptr\<rparr>) \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptra (s\<lparr>ksSchedulerAction := SwitchToThread tcb_ptr\<rparr>) \<or> ksSchedulerAction (s\<lparr>ksSchedulerAction := SwitchToThread tcb_ptr\<rparr>) = SwitchToThread tcb_ptra proof (prove)
goal:
No subgoals!
theory Orphanage

lemma ssa_almost_no_orphans_lift [wp]:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr 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. almost_no_orphans tcb_ptr s \<rbrace>" unfolding setSchedulerAction_def almost_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. almost_no_orphans tcb_ptr 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. 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) \<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>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 (1 subgoal):
 1. \<And>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) \<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>ptr. ptr = ksCurThread (s\<lparr>ksSchedulerAction := sa\<rparr>) \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (s\<lparr>ksSchedulerAction := sa\<rparr>) priority)} \<or> \<not> typ_at' TCBT ptr (s\<lparr>ksSchedulerAction := sa\<rparr>) \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr (s\<lparr>ksSchedulerAction := sa\<rparr>) \<or> ptr = tcb_ptr \<or> ksSchedulerAction (s\<lparr>ksSchedulerAction := sa\<rparr>) = SwitchToThread ptr proof (prove)
goal:
No subgoals!
theory Orphanage

lemma activateThread_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> ct_in_state' activatable' s \<and> invs' s \<rbrace>
   activateThread
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding activateThread_def apply (wp gts_wp' setThreadState_isRestart_no_orphans | wpc | clarsimp)+ apply (auto simp: ct_in_state'_def pred_tcb_at'_def obj_at'_def isRestart_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> ct_in_state' activatable' s \<and> invs' s\<rbrace> activateThread \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> ct_in_state' activatable' s \<and> invs' s\<rbrace> do thread <- getCurThread;
state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; ct_in_state' activatable' s; invs' s; st_tcb_at' ((=) Structures_H.thread_state.Restart) (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' isRestart (ksCurThread s) s \<and> valid_queues' s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setQueue_no_orphans_deq:
  "\<lbrace> \<lambda>s. \<exists> tcb_ptr. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s \<and>
        queue = [x\<leftarrow>((ksReadyQueues s) (d, priority)). x \<noteq> tcb_ptr] \<rbrace>
   setQueue d priority queue
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setQueue_def apply (wp | clarsimp)+ apply (fastforce simp: no_orphans_def all_queued_tcb_ptrs_def
                        all_active_tcb_ptrs_def is_active_tcb_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>tcb_ptr. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))\<rbrace> setQueue d priority queue \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>tcb_ptr. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, priority), queue)]\<rparr>) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcb_ptr. \<lbrakk>no_orphans s; \<not> is_active_tcb_ptr tcb_ptr s; queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))\<rbrakk> \<Longrightarrow> no_orphans (s\<lparr>ksReadyQueues := \<lambda>a. if a = (d, priority) then filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority)) else ksReadyQueues s a\<rparr>) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setQueue_almost_no_orphans_deq [wp]:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and>
        queue = [x\<leftarrow>((ksReadyQueues s) (d, priority)). x \<noteq> tcb_ptr] \<rbrace>
   setQueue d priority queue
   \<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>" unfolding setQueue_def apply (wp | clarsimp)+ apply (fastforce simp: almost_no_orphans_def all_queued_tcb_ptrs_def
                        all_active_tcb_ptrs_def is_active_tcb_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))\<rbrace> setQueue d priority queue \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, priority), queue)]\<rparr>) \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>almost_no_orphans tcb_ptr s; queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))\<rbrakk> \<Longrightarrow> almost_no_orphans tcb_ptr (s\<lparr>ksReadyQueues := \<lambda>a. if a = (d, priority) then filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority)) else ksReadyQueues s a\<rparr>) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedDequeue_almost_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   tcbSchedDequeue thread
   \<lbrace> \<lambda>rv s. almost_no_orphans thread s \<rbrace>" unfolding tcbSchedDequeue_def apply (wp threadSet_almost_no_orphans | simp cong: if_cong)+ apply (simp add:no_orphans_strg_almost cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>rv. almost_no_orphans thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do queued <- threadGet tcbQueued thread;
when queued $ do tdom <- threadGet tcbDomain thread;
prio <- threadGet tcbPriority thread;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> thread) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) thread
od
od \<lbrace>\<lambda>rv. almost_no_orphans thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<Longrightarrow> almost_no_orphans thread s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma switchToIdleThread_no_orphans' [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and>
          (is_active_tcb_ptr (ksCurThread s) s
             \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<rbrace>
   switchToIdleThread
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding switchToIdleThread_def setCurThread_def ARM_H.switchToIdleThread_def apply (simp add: no_orphans_disj all_queued_tcb_ptrs_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_disj_lift
       | clarsimp)+ apply (auto simp: no_orphans_disj all_queued_tcb_ptrs_def is_active_tcb_ptr_def
                    st_tcb_at_neg' tcb_at_typ_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> do thread <- getIdleThread;
getIdleThread >>= setVMRoot;
modify (ksCurThread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>tcb_ptr. typ_at' TCBT tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> (\<exists>a b. ksCurThread s \<in> set (ksReadyQueues s (a, b))))\<rbrace> do thread <- getIdleThread;
y <- getIdleThread >>= setVMRoot;
modify (ksCurThread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. typ_at' TCBT tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<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 x. \<lbrakk>\<forall>tcb_ptr. typ_at' TCBT tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr; is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> (\<exists>a b. ksCurThread s \<in> set (ksReadyQueues s (a, b))); typ_at' TCBT x s; x \<noteq> ksIdleThread s; \<forall>a b. x \<notin> set (ksReadyQueues s (a, b)); sch_act_not x s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) x s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma ArchThreadDecls_H_switchToThread_all_queued_tcb_ptrs [wp]:
  "\<lbrace> \<lambda>s. P (all_queued_tcb_ptrs s) \<rbrace>
   Arch.switchToThread tcb_ptr
   \<lbrace> \<lambda>rv s. P (all_queued_tcb_ptrs s) \<rbrace>" unfolding ARM_H.switchToThread_def all_queued_tcb_ptrs_def apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (all_queued_tcb_ptrs s)\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s. P (all_queued_tcb_ptrs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)}\<rbrace> do setVMRoot tcb_ptr;
doMachineOp $ ARM.clearExMonitor
od \<lbrace>\<lambda>rv s. P {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)}\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setCurThread_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and>
         (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s : all_queued_tcb_ptrs s) \<rbrace>
   setCurThread newThread
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setCurThread_def apply (wp | clarsimp)+ apply (unfold no_orphans_def all_queued_tcb_ptrs_def
                all_active_tcb_ptrs_def is_active_tcb_ptr_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> setCurThread newThread \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> modify (ksCurThread_update (\<lambda>_. newThread)) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s\<rbrakk> \<Longrightarrow> no_orphans (s\<lparr>ksCurThread := newThread\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<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; st_tcb_at' is_active_thread_state (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)}\<rbrakk> \<Longrightarrow> \<forall>tcb_ptr. tcb_ptr \<in> {tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr (s\<lparr>ksCurThread := newThread\<rparr>)} \<longrightarrow> tcb_ptr = ksCurThread (s\<lparr>ksCurThread := newThread\<rparr>) \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues (s\<lparr>ksCurThread := newThread\<rparr>) priority)} \<or> ksSchedulerAction (s\<lparr>ksCurThread := newThread\<rparr>) = SwitchToThread tcb_ptr proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedDequeue_all_active_tcb_ptrs[wp]:
  "\<lbrace>\<lambda>s. P (t' \<in> all_active_tcb_ptrs s)\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. P (t' \<in> all_active_tcb_ptrs s)\<rbrace>" by (clarsimp simp: all_active_tcb_ptrs_def is_active_tcb_ptr_def) wp

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

lemma setCurThread_almost_no_orphans:
  "\<lbrace>\<lambda>s. almost_no_orphans t s \<and>
          (ksCurThread s \<noteq> t \<longrightarrow>
             ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow>
             ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace>
   setCurThread t \<lbrace>\<lambda>_. no_orphans\<rbrace>" unfolding setCurThread_def apply wp apply (fastforce simp: almost_no_orphans_def
                        no_orphans_def
                        all_queued_tcb_ptrs_def
                        all_active_tcb_ptrs_def
                        is_active_tcb_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans t s \<and> (ksCurThread s \<noteq> t \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> setCurThread t \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans t s \<and> (ksCurThread s \<noteq> t \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. almost_no_orphans t s \<and> (ksCurThread s \<noteq> t \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> no_orphans (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedEnqueue_inQueue_eq:
  "\<lbrace> valid_queues' and K (tcb_ptr = tcb_ptr') \<rbrace>
   tcbSchedEnqueue tcb_ptr
   \<lbrace> \<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s \<rbrace>" apply (rule hoare_gen_asm, simp) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and K (tcb_ptr = tcb_ptr')\<rbrace> tcbSchedEnqueue tcb_ptr \<lbrace>\<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. tcb_ptr = tcb_ptr' \<Longrightarrow> \<lbrace>valid_queues'\<rbrace> tcbSchedEnqueue tcb_ptr' \<lbrace>\<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedAppend_inQueue_eq:
  "\<lbrace> valid_queues' and K (tcb_ptr = tcb_ptr') \<rbrace>
   tcbSchedAppend tcb_ptr
   \<lbrace> \<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s \<rbrace>" apply (rule hoare_gen_asm, simp) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and K (tcb_ptr = tcb_ptr')\<rbrace> tcbSchedAppend tcb_ptr \<lbrace>\<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. tcb_ptr = tcb_ptr' \<Longrightarrow> \<lbrace>valid_queues'\<rbrace> tcbSchedAppend tcb_ptr' \<lbrace>\<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setQueue_deq_not_empty:
  "\<lbrace> \<lambda>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and>
         (\<exists>tcb_ptr. \<not> st_tcb_at' P tcb_ptr s \<and>
                    queue = [x\<leftarrow>((ksReadyQueues s) (d, priority)). x \<noteq> tcb_ptr]) \<rbrace>
   setQueue d priority queue
   \<lbrace> \<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s \<rbrace>" unfolding setQueue_def apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> (\<exists>tcb_ptr. \<not> st_tcb_at' P tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority)))\<rbrace> setQueue d priority queue \<lbrace>\<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> (\<exists>tcb_ptr. \<not> st_tcb_at' P tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority)))\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, priority), queue)]\<rparr>) \<lbrace>\<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> (\<exists>tcb_ptr. \<not> st_tcb_at' P tcb_ptr s \<and> queue = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (d, priority))) \<Longrightarrow> \<exists>tcb. tcb \<in> set (ksReadyQueues (s\<lparr>ksReadyQueues := ksReadyQueues s aLU [((d, priority), queue)]\<rparr>) p) \<and> st_tcb_at' P tcb (s\<lparr>ksReadyQueues := ksReadyQueues s aLU [((d, priority), queue)]\<rparr>) proof (prove)
goal:
No subgoals!
theory Orphanage

lemma hoare_neg_imps:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda> rv s. \<not> R rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>" by (auto simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not> R rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>
theory Orphanage

lemma setCurThread_ct [wp]:
  "\<lbrace> \<top> \<rbrace>
   setCurThread tcb_ptr
   \<lbrace> \<lambda>rv s. ksCurThread s = tcb_ptr \<rbrace>" unfolding setCurThread_def apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> setCurThread tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s = tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> modify (ksCurThread_update (\<lambda>_. tcb_ptr)) \<lbrace>\<lambda>rv s. ksCurThread s = tcb_ptr\<rbrace> proof (prove)
goal:
No subgoals!