kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma next_domain_valid_sched_action:
  "\<lbrace>\<lambda>s. scheduler_action s = choose_new_thread\<rbrace> next_domain \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def) apply wp apply (clarsimp simp: Let_def valid_sched_action_def weak_valid_sched_action_def
                        get_etcb_def etcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. scheduler_action s = choose_new_thread\<rbrace> next_domain \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. scheduler_action s = choose_new_thread\<rbrace> modify (\<lambda>s. let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s) \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. scheduler_action s = choose_new_thread \<Longrightarrow> valid_sched_action (let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_in_cur_domain:
  "\<lbrace>in_cur_domain thread\<rbrace>
    tcb_sched_action tcb_sched_dequeue thread
  \<lbrace>\<lambda>_. in_cur_domain thread\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (simp add: etcb_at_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_cur_domain thread\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. in_cur_domain thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_cur_domain thread\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_dequeue thread queue)
od \<lbrace>\<lambda>_. in_cur_domain thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. in_cur_domain thread s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. in_cur_domain thread (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma switch_to_thread_cur_in_cur_domain[wp]:
  "\<lbrace>in_cur_domain t\<rbrace>
    switch_to_thread t
   \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s\<rbrace>" apply (simp add: switch_to_thread_def | wp tcb_sched_action_dequeue_in_cur_domain)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_cur_domain t\<rbrace> switch_to_thread t \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_enqueue_cur_ct_in_q:
  "\<lbrace>\<lambda>s. cur = cur_thread s\<rbrace> tcb_sched_action tcb_sched_enqueue cur \<lbrace>\<lambda>_. ct_in_q\<rbrace>" apply (simp add: tcb_sched_action_def | wp)+ apply (force simp: etcb_at_def ct_in_q_def tcb_sched_enqueue_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cur = cur_thread s\<rbrace> tcb_sched_action tcb_sched_enqueue cur \<lbrace>\<lambda>_. ct_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cur = cur_thread s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_in_q (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue (cur_thread s) (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) (cur_thread s) s) (cur_thread s) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_enqueue_ct_in_q:
  "\<lbrace> ct_in_q \<rbrace> tcb_sched_action tcb_sched_enqueue cur \<lbrace>\<lambda>_. ct_in_q\<rbrace>" apply (simp add: tcb_sched_action_def | wp)+ apply (force simp: etcb_at_def ct_in_q_def tcb_sched_enqueue_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_q\<rbrace> tcb_sched_action tcb_sched_enqueue cur \<lbrace>\<lambda>_. ct_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_q s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_in_q (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue cur (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) cur s) cur s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_append_ct_in_q:
  "\<lbrace> ct_in_q \<rbrace> tcb_sched_action tcb_sched_append cur \<lbrace>\<lambda>_. ct_in_q\<rbrace>" apply (simp add: tcb_sched_action_def | wp)+ apply (force simp: etcb_at_def ct_in_q_def tcb_sched_append_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_q\<rbrace> tcb_sched_action tcb_sched_append cur \<lbrace>\<lambda>_. ct_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_q s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_in_q (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append cur (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) cur s) cur s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_switch_thread_valid_blocked:
  "\<lbrace>valid_blocked and (\<lambda>s. scheduler_action s = switch_thread (cur_thread s))\<rbrace>
   set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: valid_blocked_def, wp set_scheduler_action_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and (\<lambda>s. scheduler_action s = switch_thread (cur_thread s))\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)) and (\<lambda>s. scheduler_action s = switch_thread (cur_thread s))) s \<Longrightarrow> \<forall>t. not_queued t (scheduler_action_update (\<lambda>_. resume_cur_thread) s) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t (scheduler_action_update (\<lambda>_. resume_cur_thread) s) \<longrightarrow> t \<noteq> cur_thread (scheduler_action_update (\<lambda>_. resume_cur_thread) s) \<longrightarrow> scheduler_action (scheduler_action_update (\<lambda>_. resume_cur_thread) s) \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_switch_thread_valid_sched:
  "\<lbrace>valid_sched and ct_not_queued
          and (\<lambda>s. st_tcb_at activatable (cur_thread s) s)
          and (\<lambda>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s)
          and (\<lambda>s. scheduler_action s = switch_thread (cur_thread s))\<rbrace>
     set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_.valid_sched\<rbrace>" by (simp add: valid_sched_def | wp set_scheduler_action_rct_switch_thread_valid_blocked | force)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and ct_not_queued and (\<lambda>s. st_tcb_at activatable (cur_thread s) s) and (\<lambda>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s) and (\<lambda>s. scheduler_action s = switch_thread (cur_thread s))\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma choose_thread_ct_not_queued:
  "\<lbrace> valid_queues and valid_idle and valid_etcbs \<rbrace> choose_thread \<lbrace>\<lambda>_. ct_not_queued \<rbrace>" by (wpsimp simp: choose_thread_def wp: guarded_switch_to_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and valid_idle and valid_etcbs\<rbrace> choose_thread \<lbrace>\<lambda>_. ct_not_queued\<rbrace>
theory DetSchedSchedule_AI

lemma choose_thread_ct_activatable:
  "\<lbrace> valid_queues and valid_idle \<rbrace> choose_thread \<lbrace>\<lambda>_ s.  st_tcb_at activatable (cur_thread s) s \<rbrace>" apply (wpsimp simp: choose_thread_def
                wp: guarded_switch_to_lift stit_activatable'[simplified ct_in_state_def]
                    stt_activatable[simplified ct_in_state_def]) apply (fastforce dest!: next_thread_queued
                   simp: next_thread_def valid_queues_def is_activatable_def in_cur_domain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and valid_idle\<rbrace> choose_thread \<lbrace>\<lambda>_ s. st_tcb_at activatable (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>valid_queues s; valid_idle s; ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma valid_sched_action_from_choose_thread:
  "scheduler_action s = choose_new_thread \<Longrightarrow> valid_sched_action s" unfolding valid_sched_action_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_action s = choose_new_thread \<Longrightarrow> valid_sched_action s proof (prove)
goal (1 subgoal):
 1. scheduler_action s = choose_new_thread \<Longrightarrow> is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s
theory DetSchedSchedule_AI

lemma ct_in_q_scheduler_action_update_id[simp]:
  "ct_in_q (scheduler_action_update f s) = ct_in_q s" by (simp add: ct_in_q_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_q (scheduler_action_update f s) = ct_in_q s
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_simple[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. simple_sched_action \<rbrace>" by (wpsimp wp: set_scheduler_action_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. simple_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma set_scheduler_action_obvious[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action a \<lbrace>\<lambda>_ s. scheduler_action s = a\<rbrace>" by (wpsimp wp: set_scheduler_action_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action a \<lbrace>\<lambda>_ s. scheduler_action s = a\<rbrace>
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_valid_sched:
  "\<lbrace>valid_sched and (\<lambda>s. scheduler_action s = switch_thread t \<and>
      (\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace>
   set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (wpsimp simp: valid_sched_def wp: set_scheduler_action_cnt_valid_blocked'[where t=t])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and (\<lambda>s. scheduler_action s = switch_thread t \<and> (\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma append_thread_queued:
  "\<lbrace>\<top>\<rbrace>
     tcb_sched_action tcb_sched_append thread
   \<lbrace>\<lambda>_ s. (\<exists>d prio. thread \<in> set (ready_queues s d prio))\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (fastforce simp: etcb_at_def tcb_sched_append_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_ s. \<exists>d prio. thread \<in> set (ready_queues s d prio)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append thread queue)
od \<lbrace>\<lambda>_ s. \<exists>d prio. thread \<in> set (ready_queues s d prio)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. \<exists>d prio. thread \<in> set (ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s) d prio)) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma schedule_choose_new_thread_valid_sched:
  "\<lbrace> valid_idle and valid_etcbs and valid_idle_etcb and valid_queues and valid_blocked
     and (\<lambda>s. scheduler_action s = choose_new_thread)
     and ct_in_q \<rbrace>
   schedule_choose_new_thread
   \<lbrace>\<lambda>_. valid_sched \<rbrace>" unfolding schedule_choose_new_thread_def apply (wpsimp wp_del: when_wp
                 wp: set_scheduler_action_rct_valid_sched choose_thread_ct_not_queued
                     choose_thread_ct_activatable choose_thread_cur_dom_or_idle
                     hoare_vcg_disj_lift)+ apply (wpsimp wp: next_domain_valid_sched_action next_domain_valid_etcbs
                      next_domain_valid_queues next_domain_valid_blocked next_domain_ct_in_q)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_etcbs and valid_idle_etcb and valid_queues and valid_blocked and (\<lambda>s. scheduler_action s = choose_new_thread) and ct_in_q\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_etcbs and valid_idle_etcb and valid_queues and valid_blocked and (\<lambda>s. scheduler_action s = choose_new_thread) and ct_in_q\<rbrace> do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q22 (ds_id 0)\<rbrace> next_domain \<lbrace>\<lambda>x s. valid_sched_action s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_queues s \<and> valid_blocked s \<and> ct_in_q s \<and> valid_idle_etcb s \<and> valid_queues s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_queues s \<and> valid_idle s \<and> valid_queues s \<and> simple_sched_action s\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets domain_time \<lbrace>\<lambda>dom_time. if dom_time = 0 then ?Q22 dom_time else (\<lambda>s. valid_sched_action s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_queues s \<and> valid_blocked s \<and> ct_in_q s \<and> valid_idle_etcb s \<and> (valid_queues and valid_idle and valid_etcbs) s \<and> (valid_queues and valid_idle) s \<and> valid_queues s \<and> simple_sched_action s)\<rbrace>
 3. \<And>s. (valid_idle and valid_etcbs and valid_idle_etcb and valid_queues and valid_blocked and (\<lambda>s. scheduler_action s = choose_new_thread) and ct_in_q) s \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_simple_ko_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_valid_queues[wp]:
  "\<lbrace>valid_queues\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_queues\<rbrace>" by (wp hoare_drop_imps valid_queues_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_queues\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_weak_valid_sched_action[wp]:
  "\<lbrace>weak_valid_sched_action\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>" by (wp hoare_drop_imps weak_valid_sched_action_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_switch_in_cur_domain[wp]:
  "\<lbrace>switch_in_cur_domain\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. switch_in_cur_domain\<rbrace>" by (wp hoare_drop_imps switch_in_cur_domain_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. switch_in_cur_domain\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_ct_in_cur_domain[wp]:
  "\<lbrace>ct_in_cur_domain\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" by (wp hoare_drop_imps ct_in_cur_domain_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_cur_domain\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (wp hoare_drop_imps valid_sched_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_valid_blocked[wp]:
  "\<lbrace>valid_blocked\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_blocked\<rbrace>" by (wp hoare_drop_imps valid_blocked_lift | simp add: set_simple_ko_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. valid_blocked\<rbrace>
theory DetSchedSchedule_AI

lemma cancel_all_ipc_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: cancel_all_ipc_def) apply (wp mapM_x_wp' set_thread_state_runnable_valid_queues sts_st_tcb_at' hoare_drop_imps
          set_thread_state_runnable_weak_valid_sched_action hoare_vcg_all_lift
          set_thread_state_valid_blocked_except
          tcb_sched_action_enqueue_valid_blocked
          reschedule_required_valid_sched
     | wpc
     | rule subset_refl | simp)+ apply (simp_all add: valid_sched_def valid_sched_action_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint epptr IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> valid_etcbs s \<and> valid_queues s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma cancel_all_signals_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: cancel_all_signals_def) apply (wp mapM_x_wp' set_thread_state_runnable_valid_queues sts_st_tcb_at' hoare_drop_imps
          set_thread_state_runnable_weak_valid_sched_action hoare_vcg_all_lift
          set_thread_state_valid_blocked_except
          tcb_sched_action_enqueue_valid_blocked
          reschedule_required_valid_sched
       | wpc
       | rule subset_refl | simp)+ apply (simp_all add: valid_sched_def valid_sched_action_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> valid_etcbs s \<and> valid_queues s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" by (wp hoare_drop_imps valid_etcbs_lift | simp add: thread_set_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>
theory DetSchedSchedule_AI

lemma thread_set_valid_queues:
  "(\<And>x. tcb_state (f x) = tcb_state x) \<Longrightarrow>
    \<lbrace>valid_queues\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_queues\<rbrace>" by (wp hoare_drop_imps valid_queues_lift thread_set_no_change_tcb_state |
      simp add: thread_set_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = tcb_state x) \<Longrightarrow> \<lbrace>valid_queues\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_queues\<rbrace>
theory DetSchedSchedule_AI

lemma thread_set_weak_valid_sched_action:
  "(\<And>x. tcb_state (f x) = tcb_state x) \<Longrightarrow>
   \<lbrace>weak_valid_sched_action\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>" by (wp hoare_drop_imps weak_valid_sched_action_lift thread_set_no_change_tcb_state
        | simp add: thread_set_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = tcb_state x) \<Longrightarrow> \<lbrace>weak_valid_sched_action\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma thread_set_not_state_valid_sched:
  "(\<And>x. tcb_state (f x) = tcb_state x) \<Longrightarrow>
   \<lbrace>valid_sched\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (wp hoare_drop_imps valid_sched_lift thread_set_no_change_tcb_state |
      simp add: thread_set_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = tcb_state x) \<Longrightarrow> \<lbrace>valid_sched\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>