kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_R

lemma not_tcbQueued_not_ksQ:
  fixes s
  assumes "invs' s"
      and "obj_at' (Not \<circ> tcbQueued) t s"
  shows "\<forall>d p. t \<notin> set (ksReadyQueues s (d, p))" apply (insert assms) apply (clarsimp simp add: invs'_def valid_state'_def) apply (drule(1) valid_queues_not_tcbQueued_not_ksQ) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (Not \<circ> tcbQueued) t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (Not \<circ> tcbQueued) t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; t \<in> set (ksReadyQueues s (d, p)); \<forall>d p. t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma ct_not_ksQ:
  "\<lbrakk> invs' s; ksSchedulerAction s = ResumeCurrentThread \<rbrakk>
   \<Longrightarrow> \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)" apply (clarsimp simp: invs'_def valid_state'_def ct_not_inQ_def) apply (frule(1) valid_queues_not_tcbQueued_not_ksQ) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ksSchedulerAction s = ResumeCurrentThread; valid_pspace' s; ct_in_state' activatable' s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksCurThread s \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ksSchedulerAction s = ResumeCurrentThread; valid_pspace' s; ct_in_state' activatable' s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksCurThread s \<in> set (ksReadyQueues s (a, b)); \<forall>d p. ksCurThread s \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma bitmapQ_from_bitmap_lookup:
  "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ;
     valid_bitmapQ s ; bitmapQ_no_L1_orphans s
     \<rbrakk>
   \<Longrightarrow> bitmapQ d (lookupBitmapPriority d s) s" apply (simp add: bitmapQ_lookupBitmapPriority_simp) apply (drule word_log2_nth_same) apply (drule (1) bitmapQ_no_L1_orphansD) apply (fastforce dest!: word_log2_nth_same
                   simp: word_ao_dist lookupBitmapPriority_def word_size numPriorities_def
                         wordBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d \<noteq> 0; valid_bitmapQ s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> bitmapQ d (lookupBitmapPriority d s) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d \<noteq> 0; valid_bitmapQ s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d)\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma lookupBitmapPriority_obj_at':
  "\<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; valid_queues_no_bitmap s; valid_bitmapQ s;
         bitmapQ_no_L1_orphans s\<rbrakk>
        \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState)
             (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s" apply (drule (2) bitmapQ_from_bitmap_lookup) apply (simp add: valid_bitmapQ_bitmapQ_simp) apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)", simp) apply (clarsimp, rename_tac t ts) apply (drule cons_set_intro) apply (drule (2) valid_queues_no_bitmap_objD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s\<rbrakk> \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []\<rbrakk> \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list\<rbrakk> \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>t ts. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = t # ts\<rbrakk> \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) t s proof (prove)
goal (1 subgoal):
 1. \<And>t ts. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrakk> \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) t s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma bitmapL1_zero_ksReadyQueues:
  "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk>
   \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d,p) = [])" apply (cases "ksReadyQueuesL1Bitmap s d = 0") apply (force simp add: bitmapQ_def valid_bitmapQ_def) apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d, p) = []) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d = 0\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d, p) = [])
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d, p) = []) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d, p) = []) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma prioToL1Index_le_mask:
  "\<lbrakk> prioToL1Index p = prioToL1Index p' ; p && mask wordRadix \<le> p' && mask wordRadix \<rbrakk>
   \<Longrightarrow> p \<le> p'" unfolding prioToL1Index_def apply (simp add: wordRadix_def word_le_nat_alt[symmetric]) apply (drule shiftr_eq_neg_mask_eq) apply (metis add.commute word_and_le2 word_plus_and_or_coroll2 word_plus_mono_left) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prioToL1Index p = prioToL1Index p'; p && mask wordRadix \<le> p' && mask wordRadix\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(fromIntegral $ p `~shiftR~` wordRadix) = (fromIntegral $ p' `~shiftR~` wordRadix); p && mask wordRadix \<le> p' && mask wordRadix\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p >> 5 = p' >> 5; p && mask 5 \<le> p' && mask 5\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p && mask 5 \<le> p' && mask 5; p && ~~ mask 5 = p' && ~~ mask 5\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma prioToL1Index_le_index:
  "\<lbrakk> prioToL1Index p \<le> prioToL1Index p' ; prioToL1Index p \<noteq> prioToL1Index p' \<rbrakk>
   \<Longrightarrow> p \<le> p'" unfolding prioToL1Index_def apply (simp add: wordRadix_def word_le_nat_alt[symmetric]) apply (erule (1) le_shiftr') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prioToL1Index p \<le> prioToL1Index p'; prioToL1Index p \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(fromIntegral $ p `~shiftR~` wordRadix) \<le> (fromIntegral $ p' `~shiftR~` wordRadix); (fromIntegral $ p `~shiftR~` wordRadix) \<noteq> (fromIntegral $ p' `~shiftR~` wordRadix)\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p >> 5 \<le> p' >> 5; p >> 5 \<noteq> p' >> 5\<rbrakk> \<Longrightarrow> p \<le> p' proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma bitmapQ_ksReadyQueuesI:
  "\<lbrakk> bitmapQ d p s ; valid_bitmapQ s \<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p) \<noteq> []" unfolding valid_bitmapQ_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bitmapQ d p s; valid_bitmapQ s\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bitmapQ d p s; \<forall>d p. bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p) \<noteq> []
theory Schedule_R

lemma getReadyQueuesL2Bitmap_inv[wp]:
  "\<lbrace> P \<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>_. P\<rbrace>" unfolding getReadyQueuesL2Bitmap_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, i)) \<lbrace>\<lambda>_. P\<rbrace>
theory Schedule_R

lemma switchToIdleThread_invs_no_cicd':
  "\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (clarsimp simp: Thread_H.switchToIdleThread_def ARM_H.switchToIdleThread_def) apply (wp setCurThread_invs_no_cicd'_idle_thread setVMRoot_invs_no_cicd') apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_idle'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do thread <- getIdleThread;
y <- getIdleThread >>= setVMRoot;
setCurThread thread
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> ksIdleThread s = ksIdleThread s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma setCurThread_const:
  "\<lbrace>\<lambda>_. P t \<rbrace> setCurThread t \<lbrace>\<lambda>_ s. P (ksCurThread s) \<rbrace>" by (simp add: setCurThread_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. P t\<rbrace> setCurThread t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
theory Schedule_R

lemma switchToIdleThread_curr_is_idle:
  "\<lbrace>\<top>\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s\<rbrace>" apply (rule hoare_weaken_pre) apply (wps switchToIdleThread_it) apply (simp add: Thread_H.switchToIdleThread_def) apply (wp setCurThread_const) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s'. ksCurThread s' = ksIdleThread prev_s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?P3 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> do thread <- getIdleThread;
y <- Arch.switchToIdleThread;
setCurThread thread
od \<lbrace>\<lambda>rv s'. ksCurThread s' = ksIdleThread prev_s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ksIdleThread s = ksIdleThread s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma chooseThread_it[wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>" supply if_split[split del] by (wpsimp simp: chooseThread_def curDomain_def bitmap_fun_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
theory Schedule_R

lemma threadGet_inv [wp]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: threadGet_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> liftM f (getObject t) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma corres_assert_assume_r:
  "corres dc P Q f (g ())
  \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)" by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc P Q f (g ()) \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)
theory Schedule_R

lemma thread_get_exs_valid[wp]:
  "tcb_at t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> thread_get f t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" apply (clarsimp simp: get_thread_state_def  assert_opt_def fail_def
             thread_get_def gets_the_def exs_valid_def gets_def
             get_def bind_def return_def split: option.splits) apply (erule get_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> thread_get f t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> \<exists>y. get_tcb t s = Some y proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)" by (simp add: curDomain_def state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets cur_domain) curDomain
theory Schedule_R

lemma curDomain_corres':
  "corres (=) \<top> (\<lambda>s. ksCurDomain s \<le> maxDomain)
    (gets cur_domain) (if 1 < numDomains then curDomain else return 0)" apply (case_tac "1 < numDomains"; simp) apply (rule corres_guard_imp[OF curDomain_corres]; solves simp) 
  (* if we have only one domain, then we are in it *)
   apply (clarsimp simp: return_def simpler_gets_def bind_def maxDomain_def
                        state_relation_def corres_underlying_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>s. ksCurDomain s \<le> maxDomain) (gets cur_domain) (if 1 < numDomains then curDomain else return 0) proof (prove)
goal (2 subgoals):
 1. Suc 0 < numDomains \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>s. ksCurDomain s \<le> maxDomain) (gets cur_domain) curDomain
 2. \<not> Suc 0 < numDomains \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>s. ksCurDomain s \<le> maxDomain) (gets cur_domain) (return 0) proof (prove)
goal (1 subgoal):
 1. \<not> Suc 0 < numDomains \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>s. ksCurDomain s \<le> maxDomain) (gets cur_domain) (return 0) proof (prove)
goal (1 subgoal):
 1. \<not> Suc 0 < numDomains \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>s. ksCurDomain s \<le> maxDomain) (gets cur_domain) (return 0) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma lookupBitmapPriority_Max_eqI:
  "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
   \<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})" apply (rule Max_eqI[simplified eq_commute]; simp) apply (fastforce simp: bitmapL1_highest_lookup valid_bitmapQ_bitmapQ_simp) apply (metis valid_bitmapQ_bitmapQ_simp bitmapQ_from_bitmap_lookup) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> lookupBitmapPriority d s = Max {prio. ksReadyQueues s (d, prio) \<noteq> []} proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; ksReadyQueues s (d, y) \<noteq> []\<rbrakk> \<Longrightarrow> y \<le> lookupBitmapPriority d s
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, lookupBitmapPriority d s) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, lookupBitmapPriority d s) \<noteq> [] proof (prove)
goal:
No subgoals!