kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma getQueue_corres: "corres (=) \<top> \<top> (get_tcb_queue qdom prio) (getQueue qdom prio)" apply (clarsimp simp add: getQueue_def state_relation_def ready_queues_relation_def get_tcb_queue_def gets_def) apply (fold gets_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (get_tcb_queue qdom prio) (getQueue qdom prio) proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> (\<forall>d p. ready_queues s d p = ksReadyQueues s' (d, p)) \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'} False True (=) (\<lambda>_. True) (\<lambda>_. True) (do s <- get;
return (ready_queues s qdom prio)
od) (do s <- get;
return (ksReadyQueues s (qdom, prio))
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> (\<forall>d p. ready_queues s d p = ksReadyQueues s' (d, p)) \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'} False True (=) (\<lambda>_. True) (\<lambda>_. True) (gets (\<lambda>s. ready_queues s qdom prio)) (gets (\<lambda>s. ksReadyQueues s (qdom, prio))) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma no_fail_return:
  "no_fail x (return y)" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail x (return y)
theory TcbAcc_R

lemma addToBitmap_noop_corres:
  "corres dc \<top> \<top> (return ()) (addToBitmap d p)" unfolding addToBitmap_def modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
            modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def by (rule corres_noop)
     (wp | simp add: state_relation_def | rule no_fail_pre)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (addToBitmap d p) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od)
theory TcbAcc_R

lemma addToBitmap_if_null_noop_corres: (* used this way in Haskell code *)
  "corres dc \<top> \<top> (return ()) (if null queue then addToBitmap d p else return ())" by (cases "null queue", simp_all add: addToBitmap_noop_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (if null queue then addToBitmap d p else return ())
theory TcbAcc_R

lemma removeFromBitmap_corres_noop:
  "corres dc \<top> \<top> (return ()) (removeFromBitmap tdom prioa)" unfolding removeFromBitmap_def by (rule corres_noop)
     (wp | simp add: bitmap_fun_defs state_relation_def | rule no_fail_pre)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (removeFromBitmap tdom prioa) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do l1index <- return (prioToL1Index prioa);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prioa && mask wordRadix));
modifyReadyQueuesL2Bitmap tdom l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap tdom l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap tdom $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od)
theory TcbAcc_R

lemma weak_sch_act_wf_updateDomainTime[simp]:
  "weak_sch_act_wf m (ksDomainTime_update f s) = weak_sch_act_wf m s" by (simp add:weak_sch_act_wf_def tcb_in_cur_domain'_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_sch_act_wf m (ksDomainTime_update f s) = weak_sch_act_wf m s
theory TcbAcc_R

lemma setSchedulerAction_corres:
  "sched_act_relation sa sa'
    \<Longrightarrow> corres dc \<top> \<top> (set_scheduler_action sa) (setSchedulerAction sa')" apply (simp add: setSchedulerAction_def set_scheduler_action_def) apply (rule corres_no_failI) apply wp apply (clarsimp simp: in_monad simpler_modify_def state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sched_act_relation sa sa' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (set_scheduler_action sa) (setSchedulerAction sa') proof (prove)
goal (1 subgoal):
 1. sched_act_relation sa sa' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (modify (scheduler_action_update (\<lambda>_. sa))) (modify (ksSchedulerAction_update (\<lambda>_. sa'))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sched_act_relation sa sa'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (modify (ksSchedulerAction_update (\<lambda>_. sa')))
 2. sched_act_relation sa sa' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (modify (ksSchedulerAction_update (\<lambda>_. sa')) s'). \<exists>(r, t)\<in>fst (modify (scheduler_action_update (\<lambda>_. sa)) s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. sched_act_relation sa sa' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (modify (ksSchedulerAction_update (\<lambda>_. sa')) s'). \<exists>(r, t)\<in>fst (modify (scheduler_action_update (\<lambda>_. sa)) s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma getSchedulerAction_corres:
  "corres sched_act_relation \<top> \<top> (gets scheduler_action) getSchedulerAction" apply (simp add: getSchedulerAction_def) apply (clarsimp simp: state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres sched_act_relation (\<lambda>_. True) (\<lambda>_. True) (gets scheduler_action) getSchedulerAction proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> sched_act_relation (scheduler_action s) (ksSchedulerAction s') proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma weak_sch_act_wf_lift:
  assumes pre: "\<And>P. \<lbrace>\<lambda>s. P (sa s)\<rbrace> f \<lbrace>\<lambda>rv s. P (sa s)\<rbrace>"
               "\<And>t. \<lbrace>st_tcb_at' runnable' t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace>"
               "\<And>t. \<lbrace>tcb_in_cur_domain' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_in_cur_domain' t\<rbrace>"
  shows "\<lbrace>\<lambda>s. weak_sch_act_wf (sa s) s\<rbrace> f \<lbrace>\<lambda>rv s. weak_sch_act_wf (sa s) s\<rbrace>" apply (simp only: weak_sch_act_wf_def imp_conv_disj) apply (intro hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_disj_lift pre | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (sa s) s\<rbrace> f \<lbrace>\<lambda>rv s. weak_sch_act_wf (sa s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. sa s \<noteq> SwitchToThread t \<or> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>t. sa s \<noteq> SwitchToThread t \<or> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
    asUser t m \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp weak_sch_act_wf_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> asUser t m \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma doMachineOp_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
     doMachineOp m \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (simp add: doMachineOp_def split_def tcb_in_cur_domain'_def | wp weak_sch_act_wf_lift)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma weak_sch_act_wf_setQueue[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>
    setQueue qdom prio queue
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>" by (simp add: setQueue_def weak_sch_act_wf_def tcb_in_cur_domain'_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> setQueue qdom prio queue \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma threadSet_tcbDomain_triv:
  assumes "\<And>tcb. tcbDomain (f tcb) = tcbDomain tcb"
  shows   "\<lbrace>tcb_in_cur_domain' t'\<rbrace> threadSet f t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace>" apply (simp add: tcb_in_cur_domain'_def) apply (rule_tac f="ksCurDomain" in hoare_lift_Pf) apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | simp add: assms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> threadSet f t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> threadSet f t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma removeFromBitmap_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" unfolding removeFromBitmap_def by (simp add: bitmap_fun_defs|wp setObject_nosch)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
modifyReadyQueuesL2Bitmap d l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap d l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap d $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
theory TcbAcc_R

lemma addToBitmap_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" unfolding addToBitmap_def by (simp add: bitmap_fun_defs|wp setObject_nosch)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
modifyReadyQueuesL1Bitmap d (\<lambda>w. w || HaskellLib_H.bit l1index);
modifyReadyQueuesL2Bitmap d l1indexInverted (\<lambda>w. w || HaskellLib_H.bit l2bit)
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
theory TcbAcc_R

lemma removeFromBitmap_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace>" unfolding tcb_in_cur_domain'_def removeFromBitmap_def apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf) apply (wp setObject_cte_obj_at_tcb' | simp add: bitmap_fun_defs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> do l1index <- return (prioToL1Index prio);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prio && mask wordRadix));
modifyReadyQueuesL2Bitmap tdom l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap tdom l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap tdom $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>ya s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace> do l1index <- return (prioToL1Index prio);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prio && mask wordRadix));
modifyReadyQueuesL2Bitmap tdom l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap tdom l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap tdom $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> do l1index <- return (prioToL1Index prio);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prio && mask wordRadix));
modifyReadyQueuesL2Bitmap tdom l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap tdom l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap tdom $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma addToBitmap_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace>" unfolding tcb_in_cur_domain'_def addToBitmap_def apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf) apply (wp setObject_cte_obj_at_tcb' | simp add: bitmap_fun_defs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> do l1index <- return (prioToL1Index prio);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prio && mask wordRadix));
modifyReadyQueuesL1Bitmap tdom (\<lambda>w. w || HaskellLib_H.bit l1index);
modifyReadyQueuesL2Bitmap tdom l1indexInverted (\<lambda>w. w || HaskellLib_H.bit l2bit)
od \<lbrace>\<lambda>ya s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace> do l1index <- return (prioToL1Index prio);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prio && mask wordRadix));
modifyReadyQueuesL1Bitmap tdom (\<lambda>w. w || HaskellLib_H.bit l1index);
modifyReadyQueuesL2Bitmap tdom l1indexInverted (\<lambda>w. w || HaskellLib_H.bit l2bit)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> do l1index <- return (prioToL1Index prio);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral prio && mask wordRadix));
modifyReadyQueuesL1Bitmap tdom (\<lambda>w. w || HaskellLib_H.bit l1index);
modifyReadyQueuesL2Bitmap tdom l1indexInverted (\<lambda>w. w || HaskellLib_H.bit l2bit)
od \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedDequeue_weak_sch_act_wf[wp]:
  "\<lbrace> \<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace> tcbSchedDequeue a \<lbrace> \<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>" apply (simp add: tcbSchedDequeue_def) apply (wp threadSet_weak_sch_act_wf removeFromBitmap_weak_sch_act_wf | simp add: crunch_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedDequeue a \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do queued <- threadGet tcbQueued a;
when queued (do tdom <- threadGet tcbDomain a;
prio <- threadGet tcbPriority a;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> a) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> a) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) a
od)
od \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gets_the_exec: "f s \<noteq> None \<Longrightarrow>  (do x \<leftarrow> gets_the f; g x od) s = g (the (f s)) s" apply (clarsimp simp add: gets_the_def bind_def gets_def get_def
                   return_def assert_opt_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f s \<noteq> None \<Longrightarrow> (gets_the f >>= g) s = g (the (f s)) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma thread_get_test: "do cur_ts \<leftarrow> get_thread_state cur; g (test cur_ts) od =
       do t \<leftarrow> (thread_get (\<lambda>tcb. test (tcb_state tcb)) cur); g t od" apply (simp add: get_thread_state_def thread_get_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do cur_ts <- get_thread_state cur;
g (test cur_ts)
od = thread_get (\<lambda>tcb. test (tcb_state tcb)) cur >>= g proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_corres:
  "corres dc
          (tcb_at t)
          (tcb_at' t)
          (set_bound_notification t ntfn) (setBoundNotification ntfn t)" apply (simp add: set_bound_notification_def setBoundNotification_def) apply (subst thread_set_def[simplified, symmetric]) apply (rule threadset_corres, simp_all add:tcb_relation_def exst_same_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (set_bound_notification t ntfn) (setBoundNotification ntfn t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od) (threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) t) (threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_valid_objs':
  "\<lbrace>valid_objs' and valid_tcb_state' st\<rbrace>
  setThreadState st t
  \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (simp add: setThreadState_def setQueue_def isRunnable_def isStopped_def) apply (wp threadSet_valid_objs') apply (simp add: valid_tcb'_def tcb_cte_cases_def) apply (wp threadSet_valid_objs' | simp)+ apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_tcb_state' st\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
state <- getThreadState t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (if \<not> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then valid_objs' else valid_objs') s\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_objs' and valid_tcb_state' st) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> getThreadState t \<lbrace>\<lambda>state. valid_objs'\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_objs' and valid_tcb_state' st) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> valid_tcb_state' st s \<Longrightarrow> \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. st) tcb) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma ssa_wp[wp]:
  "\<lbrace>\<lambda>s. P (s \<lparr>ksSchedulerAction := sa\<rparr>)\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>_. P\<rbrace>" by (wpsimp simp: setSchedulerAction_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>ksSchedulerAction := sa\<rparr>)\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>_. P\<rbrace>