kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma cancel_badged_sends_valid_sched[wp]:
  shows
  "\<lbrace>valid_sched\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: cancel_badged_sends_def) apply (wp hoare_drop_imps reschedule_required_valid_sched | wpc | 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_badged_sends epptr badge \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do ep <- get_endpoint epptr;
case ep of SendEP queue \<Rightarrow> do set_endpoint epptr IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
set_endpoint epptr ep';
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 cap_revoke_valid_sched[wp]:
  "\<lbrace>valid_sched and simple_sched_action\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (rule hoare_strengthen_post) apply (rule validE_valid, rule cap_revoke_preservation) apply (wpsimp wp: preemption_point_inv')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_sched and simple_sched_action\<rbrace> cap_revoke slot \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> valid_sched s proof (prove)
goal (3 subgoals):
 1. \<And>s p. \<lbrace>valid_sched and simple_sched_action\<rbrace> cap_delete p \<lbrace>\<lambda>_. valid_sched and simple_sched_action\<rbrace>
 2. \<And>s. \<lbrace>valid_sched and simple_sched_action\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_sched and simple_sched_action\<rbrace>
 3. \<And>rv s. (valid_sched and simple_sched_action) s \<Longrightarrow> valid_sched s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma cap_revoke_simple_sched_action[wp]:
  "\<lbrace>simple_sched_action\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>" by (wp cap_revoke_preservation preemption_point_inv' | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>simple_sched_action\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma thread_set_state_eq_valid_queues:
  "(\<And>x. tcb_state (f x) = ts) \<Longrightarrow>
   \<lbrace>valid_queues and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_queues\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (fastforce simp: valid_queues_def st_tcb_at_kh_if_split st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_queues and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_queues and st_tcb_at ((=) ts) tptr\<rbrace> do tcb <- gets_the (get_tcb tptr);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh tptr = Some y);
return (the (kh tptr))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_state (f x) = ts; (valid_queues and st_tcb_at ((=) ts) tptr) s\<rbrakk> \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_queues (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f (the (get_tcb tptr s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_state_eq_valid_sched_action:
  "(\<And>x. tcb_state (f x) = ts) \<Longrightarrow>
   \<lbrace>valid_sched_action and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_sched_action\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (fastforce simp: valid_sched_action_def weak_valid_sched_action_def
                         is_activatable_def st_tcb_at_kh_if_split st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_sched_action and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_sched_action and st_tcb_at ((=) ts) tptr\<rbrace> do tcb <- gets_the (get_tcb tptr);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh tptr = Some y);
return (the (kh tptr))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_state (f x) = ts; (valid_sched_action and st_tcb_at ((=) ts) tptr) s\<rbrakk> \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_sched_action (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f (the (get_tcb tptr s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_state_eq_ct_in_cur_domain:
  "(\<And>x. tcb_state (f x) = ts) \<Longrightarrow>
   \<lbrace>ct_in_cur_domain and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. ct_in_cur_domain\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (fastforce simp: ct_in_cur_domain_def st_tcb_at_kh_if_split st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>ct_in_cur_domain and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>ct_in_cur_domain and st_tcb_at ((=) ts) tptr\<rbrace> do tcb <- gets_the (get_tcb tptr);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh tptr = Some y);
return (the (kh tptr))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_state (f x) = ts; (ct_in_cur_domain and st_tcb_at ((=) ts) tptr) s\<rbrakk> \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> ct_in_cur_domain (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f (the (get_tcb tptr s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_state_eq_valid_blocked:
  "(\<And>x. tcb_state (f x) = ts) \<Longrightarrow>
   \<lbrace>valid_blocked and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_blocked\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (fastforce simp: valid_blocked_def st_tcb_at_kh_if_split st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_blocked and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_blocked and st_tcb_at ((=) ts) tptr\<rbrace> do tcb <- gets_the (get_tcb tptr);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh tptr = Some y);
return (the (kh tptr))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_state (f x) = ts; (valid_blocked and st_tcb_at ((=) ts) tptr) s\<rbrakk> \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_blocked (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f (the (get_tcb tptr s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_state_eq_valid_sched:
  "(\<And>x. tcb_state (f x) = ts) \<Longrightarrow>
   \<lbrace>valid_sched and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: valid_sched_def) apply (wp thread_set_state_eq_valid_queues thread_set_state_eq_valid_blocked thread_set_state_eq_valid_sched_action thread_set_state_eq_ct_in_cur_domain | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>valid_sched and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_state (f x) = ts) \<Longrightarrow> \<lbrace>(\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and st_tcb_at ((=) ts) tptr\<rbrace> thread_set f tptr \<lbrace>\<lambda>rv s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_switch_switch_in_cur_domain:
  "\<lbrace>switch_in_cur_domain and (\<lambda>s. scheduler_action s \<noteq> switch_thread tptr)\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: switch_in_cur_domain_def in_cur_domain_def is_etcb_at_def etcb_at_def get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain and (\<lambda>s. scheduler_action s \<noteq> switch_thread tptr)\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. switch_in_cur_domain s \<and> scheduler_action s \<noteq> switch_thread tptr \<Longrightarrow> (\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (\<lambda>a. if a = tptr then Some (f (the (get_etcb tptr s))) else ekheap s a) (cur_domain s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_valid_blocked:
  "\<lbrace>valid_blocked\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked\<rbrace>" by (wp valid_blocked_lift | simp add: ethread_set_def set_eobject_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked\<rbrace>
theory DetSchedSchedule_AI

lemma ethread_set_inactive_valid_idle_etcb:
  notes valid_idle_etcb_lift[wp del]
  shows
  "\<lbrace>valid_idle_etcb and valid_idle and st_tcb_at inactive tptr\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>" apply(simp add: ethread_set_def set_eobject_def) apply wp apply(clarsimp simp: get_etcb_def valid_idle_etcb_def etcb_at'_def valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle_etcb and valid_idle and st_tcb_at inactive tptr\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle_etcb and valid_idle and st_tcb_at inactive tptr\<rbrace> do tcb <- gets_the (get_etcb tptr);
es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(tptr \<mapsto> f tcb)) es)
od \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_idle_etcb and valid_idle and st_tcb_at inactive tptr) s \<Longrightarrow> get_etcb tptr s \<noteq> None \<longrightarrow> valid_idle_etcb (ekheap_update (\<lambda>_. (ekheap s)(tptr \<mapsto> f (the (get_etcb tptr s)))) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_inactive_valid_sched:
  "\<lbrace>valid_sched and valid_idle and st_tcb_at inactive tptr\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def valid_sched_action_def | wp ethread_set_not_queued_valid_queues ethread_set_not_switch_switch_in_cur_domain ethread_set_not_cur_ct_in_cur_domain ethread_set_valid_blocked ethread_set_inactive_valid_idle_etcb)+ apply (force simp: valid_idle_def st_tcb_at_def obj_at_def not_cur_thread_def
                           is_activatable_def weak_valid_sched_action_def valid_queues_def
                           not_queued_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_idle and st_tcb_at inactive tptr\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> st_tcb_at inactive tptr s \<Longrightarrow> not_queued tptr s \<and> scheduler_action s \<noteq> switch_thread tptr \<and> not_cur_thread tptr s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_not_idle_valid_idle:
  "\<lbrace>valid_idle and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
     thread_set f tptr \<lbrace>\<lambda>_. valid_idle\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def, wp) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_idle and (\<lambda>s. tptr \<noteq> idle_thread s)) s \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_idle (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f (the (get_tcb tptr s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_st_tcb_at:
  "(\<And>x. P (tcb_state (f x)))
  \<Longrightarrow> \<lbrace>\<top>\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. st_tcb_at P tptr\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def, wp) apply (clarsimp simp: valid_idle_def st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. P (tcb_state (f x))) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. st_tcb_at P tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. P (tcb_state (f x)); True\<rbrakk> \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> st_tcb_at P tptr (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (f (the (get_tcb tptr s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma transfer_caps_valid_sched:
  "\<lbrace>valid_sched\<rbrace> transfer_caps info caps ep recv recv_buf \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: transfer_caps_def | wp transfer_caps_loop_pres | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> transfer_caps info caps ep recv recv_buf \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma thread_set_ct_active_wp:
  "\<lbrace> ct_active \<rbrace> thread_set (tcb_fault_update u) t \<lbrace>\<lambda>rv. ct_active \<rbrace>" by (wp ct_in_state_thread_state_lift thread_set_no_change_tcb_state, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> thread_set (tcb_fault_update u) t \<lbrace>\<lambda>rv. ct_active\<rbrace>
theory DetSchedSchedule_AI

lemma set_thread_state_not_queued_valid_queues:
  "\<lbrace>valid_queues and not_queued thread\<rbrace>
      set_thread_state thread ts
   \<lbrace>\<lambda>rv. valid_queues\<rbrace>" apply (simp add: set_thread_state_def) apply (wp | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (fastforce simp: valid_queues_def st_tcb_at_kh_if_split not_queued_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and not_queued thread\<rbrace> set_thread_state thread ts \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and not_queued thread\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<and> not_queued thread s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> (\<exists>y. kheap s thread = Some y) \<longrightarrow> a_type (the (kheap s thread)) = ATCB \<longrightarrow> valid_queues_2 (ready_queues s) (ekheap s) (\<lambda>a. if a = thread then Some (TCB (the (get_tcb thread s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_is_activatable'[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. is_activatable (t s) s\<rbrace>" apply (wp set_scheduler_action_wp) apply (simp add: is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. is_activatable (t s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> is_activatable (t (scheduler_action_update (\<lambda>_. choose_new_thread) s)) (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_switch_in_cur_domain[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>" by (simp add: set_scheduler_action_def, wp, simp)

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

lemma set_thread_state_sched_act_not_valid_sched:
  "\<lbrace>valid_sched and scheduler_act_not thread
      and not_queued thread and K (\<not> runnable ts)\<rbrace>
     set_thread_state thread ts
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (simp add: valid_sched_def |
      wp set_thread_state_not_queued_valid_queues
                                    set_thread_state_not_runnable_valid_blocked
         set_thread_state_sched_act_not_valid_sched_action)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable ts)\<rbrace> set_thread_state thread ts \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma setup_caller_cap_sched_act_not_valid_sched:
  "\<lbrace>valid_sched and scheduler_act_not sender and not_queued sender\<rbrace>
     setup_caller_cap sender receiver grant
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (auto simp: setup_caller_cap_def
     | wp set_thread_state_sched_act_not_valid_sched)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and scheduler_act_not sender and not_queued sender\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma possible_switch_to_sched_act_not[wp]:
  "\<lbrace>K(t \<noteq> target) and scheduler_act_not t\<rbrace>
     possible_switch_to target
   \<lbrace>\<lambda>_. scheduler_act_not t\<rbrace>" apply (simp add: possible_switch_to_def reschedule_required_def
                   set_scheduler_action_def tcb_sched_action_def
              split del: if_split
        | wp | wpc)+ apply (clarsimp simp: etcb_at_def scheduler_act_not_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (t \<noteq> target) and scheduler_act_not t\<rbrace> possible_switch_to target \<lbrace>\<lambda>_. scheduler_act_not t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. t \<noteq> target \<and> scheduler_act_not t s \<Longrightarrow> etcb_at (\<lambda>ta. tcb_domain ta = cur_domain s \<longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> scheduler_act_not_2 (switch_thread target) t) target s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_ready_queues[wp]:
  "\<lbrace>\<lambda>s :: det_state. P (ready_queues s)\<rbrace>
    set_thread_state thread ts
   \<lbrace>\<lambda>r s. P (ready_queues s)\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def[abs_def] reschedule_required_def
                   set_scheduler_action_def set_object_def get_object_def) apply (wp | wpc | simp add: tcb_sched_action_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> set_thread_state thread ts \<lbrace>\<lambda>r s. P (ready_queues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>r s. P (ready_queues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh thread = Some y);
return (the (kh thread))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od;
ts <- get_thread_state thread;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = thread \<and> action = resume_cur_thread) (modify (scheduler_action_update (\<lambda>_. choose_new_thread)))
od \<lbrace>\<lambda>r s. P (ready_queues s)\<rbrace> proof (prove)
goal:
No subgoals!