kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma ethread_set_not_queued_valid_sched:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>valid_sched and not_queued 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_domain_switch_in_cur_domain ethread_set_not_domain_ct_in_cur_domain ethread_set_not_domain_valid_blocked ethread_set_valid_idle_etcb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>valid_sched and not_queued tptr\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_dequeue_not_queued:
  "\<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>_. not_queued tptr\<rbrace>" apply (simp add: tcb_sched_action_def | wp)+ apply (clarsimp simp: etcb_at_def tcb_sched_dequeue_def not_queued_def
                        valid_queues_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>_. not_queued tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. not_queued_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_dequeue tptr (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) tptr) tptr s) tptr s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ct_in_state_def2: "ct_in_state test s = st_tcb_at test (cur_thread s) s" by (simp add: ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_state test s = st_tcb_at test (cur_thread s) s
theory DetSchedSchedule_AI

lemma set_mcpriority_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> set_mcpriority tptr prio \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: set_mcpriority_def thread_set_not_state_valid_sched)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> set_mcpriority tptr prio \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma set_nonmember_if_cong: "(a \<notin> set (if P then x else y)) = (if P then a \<notin> set x else a \<notin> set y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<notin> set (if P then x else y)) = (if P then a \<notin> set x else a \<notin> set y)
theory DetSchedSchedule_AI

lemma set_scheduler_action_swt_weak_valid_sched_except:
  "\<lbrace>valid_sched_except_blocked and valid_blocked_except t and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace>
     set_scheduler_action (switch_thread t)
   \<lbrace>\<lambda>_.valid_sched\<rbrace>" apply (simp add: set_scheduler_action_def) apply wp apply (force simp: valid_sched_def ct_not_in_q_def
                     valid_sched_action_def weak_valid_sched_action_def
                     in_cur_domain_def ct_in_cur_domain_def switch_in_cur_domain_def
                     valid_blocked_except_def simple_sched_action_def
                     valid_blocked_2_def is_activatable_2_def valid_idle_etcb_def
              split: scheduler_action.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_except_blocked and valid_blocked_except t and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace> set_scheduler_action (switch_thread t) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_except_blocked and valid_blocked_except t and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace> modify (scheduler_action_update (\<lambda>_. switch_thread t)) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched_except_blocked and valid_blocked_except t and st_tcb_at runnable t and in_cur_domain t and simple_sched_action) s \<Longrightarrow> valid_sched (scheduler_action_update (\<lambda>_. switch_thread t) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_swt_weak_valid_sched:
  "\<lbrace>valid_sched and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace>
     set_scheduler_action (switch_thread t)
   \<lbrace>\<lambda>_.valid_sched\<rbrace>" apply (simp add: set_scheduler_action_def) apply wp apply (clarsimp simp: valid_sched_def ct_not_in_q_def valid_sched_action_def weak_valid_sched_action_def
                        in_cur_domain_def ct_in_cur_domain_def switch_in_cur_domain_def valid_blocked_def
                        simple_sched_action_def
                 split: scheduler_action.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace> set_scheduler_action (switch_thread t) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace> modify (scheduler_action_update (\<lambda>_. switch_thread t)) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched and st_tcb_at runnable t and in_cur_domain t and simple_sched_action) s \<Longrightarrow> valid_sched (scheduler_action_update (\<lambda>_. switch_thread t) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_sched_action_cnt_not_cur_thread[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>" apply (simp add: set_scheduler_action_def | wp)+ apply (simp add: not_cur_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. not_cur_thread_2 t choose_new_thread (cur_thread s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma reschedule_required_not_cur_thread[wp]:
  "\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>" by (simp add: reschedule_required_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>
theory DetSchedSchedule_AI

lemma set_priority_valid_sched[wp]:
  "\<lbrace>valid_sched and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> set_priority tptr prio \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (rule hoare_pre) apply (simp add: set_priority_def thread_set_priority_def) apply (wp gts_wp hoare_vcg_if_lift ethread_set_not_queued_valid_queues hoare_vcg_all_lift
             tcb_dequeue_not_queued hoare_vcg_imp_lift hoare_vcg_disj_lift
             tcb_sched_action_enqueue_valid_blocked
             ethread_set_not_domain_valid_sched_action
             ethread_set_not_domain_ct_in_cur_domain
             ethread_set_not_domain_valid_blocked_except
             ethread_set_not_queued_valid_sched
             tcb_sched_action_dequeue_valid_blocked_except
             tcb_sched_action_dequeue_valid_sched_not_runnable
             reschedule_required_valid_sched_cur_thread ethread_set_valid_idle_etcb
             possible_switch_to_valid_sched_except
          | simp add: ct_in_state_def2[symmetric])+ apply (auto simp: valid_sched_def valid_sched_action_def st_tcb_at_def obj_at_def not_cur_thread_def split: thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> set_priority tptr prio \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_priority tptr prio \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>s. (valid_sched and (\<lambda>s. tptr \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- tcb_sched_action tcb_sched_dequeue tptr;
y <- ethread_set (tcb_priority_update (\<lambda>_. prio)) tptr;
ts <- get_thread_state tptr;
when (runnable ts) (do cur <- gets cur_thread;
if tptr = cur then reschedule_required else possible_switch_to tptr
od)
od \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>s. (valid_sched and (\<lambda>s. tptr \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<and> tptr \<noteq> idle_thread s \<Longrightarrow> \<forall>x. st_tcb_at ((=) x) tptr s \<longrightarrow> (runnable x \<longrightarrow> (tptr = cur_thread s \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s) \<and> (tptr = cur_thread s \<or> 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_idle_etcb s \<and> valid_blocked s \<and> st_tcb_at runnable tptr s \<and> not_cur_thread tptr s)) \<and> (runnable x \<or> st_tcb_at (\<lambda>st. st \<noteq> Running \<and> st \<noteq> Restart) tptr s \<and> valid_queues s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma rec_del_idle_thread[wp]:
  "\<lbrace>\<lambda>(s:: det_ext state). P (idle_thread s)\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>" apply (rule rec_del_preservation) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s sl1 sl2. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> cap_swap_for_delete sl1 sl2 \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>
 2. \<And>s sl cap. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> set_cap sl cap \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>
 3. \<And>s sl opt. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> empty_slot sl opt \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>
 4. \<And>s cap fin. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>
 5. \<And>s. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> preemption_point \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma possible_switch_to_valid_sched:
  "\<lbrace>valid_sched and st_tcb_at runnable target and not_cur_thread target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
     possible_switch_to target \<lbrace>\<lambda>rv. valid_sched\<rbrace>" unfolding possible_switch_to_def apply (wpsimp wp: reschedule_required_valid_blocked set_scheduler_action_swt_weak_valid_sched
         | strengthen valid_blocked_valid_blocked_except)+ by (fastforce simp: etcb_at'_def not_cur_thread_2_def valid_sched_def valid_sched_action_def
                      in_cur_domain_def ct_in_cur_domain_2_def valid_blocked_def
                      valid_blocked_except_def
                split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at runnable target and not_cur_thread target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace> possible_switch_to target \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at runnable target and not_cur_thread target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace> do cur_dom <- gets cur_domain;
target_dom <- ethread_get tcb_domain target;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue target else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue target
od else set_scheduler_action $ switch_thread target
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_sched s; st_tcb_at runnable target s; not_cur_thread target s; target \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. (tcb_domain t \<noteq> cur_domain s \<longrightarrow> 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_idle_etcb s \<and> valid_blocked_except target s) \<and> (tcb_domain t = cur_domain s \<longrightarrow> (scheduler_action s \<noteq> resume_cur_thread \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> weak_valid_sched_action s \<and> valid_idle_etcb s \<and> valid_blocked s) \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> in_cur_domain target s))) target s
theory DetSchedSchedule_AI

lemma set_thread_state_not_cur_thread[wp]:
  "\<lbrace>not_cur_thread thread\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>rv. not_cur_thread thread\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_def set_thread_state_ext_def set_object_def get_object_def |
         wp gts_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_cur_thread thread\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>rv. not_cur_thread thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_cur_thread thread\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>rv. not_cur_thread thread\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma as_user_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> as_user tptr f \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def) apply (wp | wpc)+ apply clarsimp by (fastforce simp: valid_sched_def valid_etcbs_def valid_queues_def
                      valid_sched_action_def is_activatable_def
                      weak_valid_sched_action_def st_tcb_at_kh_if_split
                      st_tcb_def2 valid_blocked_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> as_user tptr f \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do tcb <- gets_the (get_tcb tptr);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- do 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 (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return a
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb tptr s))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_sched (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb tptr s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>valid_sched s; (x, xa) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb tptr s = Some y; kheap s tptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (\<lambda>a. if a = tptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap s a) (cur_thread s) (idle_thread s)
theory DetSchedSchedule_AI

lemma runnable_eq_active: "runnable = active" apply (rule ext) apply (case_tac st, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. runnable = active proof (prove)
goal (1 subgoal):
 1. \<And>st. runnable st = active st proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma handle_yield_valid_sched[wp]:
  "\<lbrace>valid_sched and ct_active\<rbrace> handle_yield \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: handle_yield_def | wp tcb_sched_action_append_valid_blocked tcb_sched_action_dequeue_valid_blocked_except reschedule_required_valid_sched)+ apply (clarsimp simp: valid_sched_def ct_in_state_def valid_sched_action_def
                        runnable_eq_active) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and ct_active\<rbrace> handle_yield \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<and> ct_active s \<Longrightarrow> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) 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 reschedule_required_switch_valid_sched:
  "\<lbrace>valid_etcbs and valid_queues and weak_valid_sched_action and (\<lambda>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False) and valid_idle_etcb\<rbrace>
    reschedule_required
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: valid_sched_def | wp reschedule_required_switch_valid_blocked | force)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs and valid_queues and weak_valid_sched_action and (\<lambda>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False) and valid_idle_etcb\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma set_simple_ko_valid_sched_action[wp]:
  "\<lbrace>valid_sched_action\<rbrace> set_simple_ko f ptr ntfn \<lbrace>\<lambda>rv. valid_sched_action\<rbrace>" by (wp hoare_drop_imps valid_sched_action_lift | simp add: set_simple_ko_def)+

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

lemma transfer_caps_not_cur_thread[wp]:
  "\<lbrace>not_cur_thread t\<rbrace> transfer_caps info caps ep recv recv_buf
   \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>" by (simp add: transfer_caps_def | wp transfer_caps_loop_pres | wpc)+

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

lemma set_thread_state_runnable_valid_sched:
  "\<lbrace>valid_sched and st_tcb_at runnable ref and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def | wp set_thread_state_runnable_valid_queues
                                        set_thread_state_runnable_valid_sched_action
                                        set_thread_state_runnable_valid_blocked)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at runnable ref and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma update_waiting_ntfn_valid_sched[wp]:
  "\<lbrace> \<lambda>s. valid_sched s \<and> hd queue \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd queue \<noteq> cur_thread s)\<rbrace> update_waiting_ntfn ntfnptr queue badge val \<lbrace> \<lambda>_. valid_sched \<rbrace>" apply (simp add: update_waiting_ntfn_def) apply (wp sts_st_tcb_at' possible_switch_to_valid_sched_except
            set_thread_state_runnable_valid_sched
            set_thread_state_runnable_valid_queues
            set_thread_state_runnable_valid_sched_action
            set_thread_state_valid_blocked_except
            | clarsimp)+ apply (clarsimp simp add: valid_sched_def not_cur_thread_def ct_not_in_q_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_sched s \<and> hd queue \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd queue \<noteq> cur_thread s)\<rbrace> update_waiting_ntfn ntfnptr queue badge val \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_sched s \<and> hd queue \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd queue \<noteq> cur_thread s)\<rbrace> do y <- assert (queue \<noteq> []);
y <- set_notification ntfnptr \<lparr>ntfn_obj = case tl queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl queue), ntfn_bound_tcb = badge\<rparr>;
y <- set_thread_state (hd queue) Running;
y <- as_user (hd queue) (setRegister badge_register val);
possible_switch_to (hd queue)
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_sched s; hd queue \<noteq> idle_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> hd queue \<noteq> cur_thread s; queue \<noteq> []\<rbrakk> \<Longrightarrow> 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_idle_etcb s \<and> valid_blocked s \<and> not_cur_thread (hd queue) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma timer_tick_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> timer_tick \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: timer_tick_def crunch_simps thread_set_time_slice_def
                   trans_state_update'[symmetric] ethread_set_def set_eobject_def
           | wp gts_wp reschedule_required_valid_sched tcb_sched_action_append_valid_blocked
           | wpc | rule hoare_strengthen_post, rule dec_domain_time_valid_sched,
                                      simp add: valid_sched_def valid_sched_action_def)+ by (fastforce simp: valid_sched_def valid_etcbs_def valid_queues_def pred_tcb_weakenE
         valid_sched_action_def weak_valid_sched_action_def etcb_at_def is_etcb_at_def
         get_etcb_def in_cur_domain_def ct_in_cur_domain_2_def switch_in_cur_domain_def
         valid_idle_etcb_2_def
         split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> timer_tick \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> st_tcb_at ((=) Running) (cur_thread s) s \<longrightarrow> etcb_at (\<lambda>t. (Suc 0 < tcb_time_slice t \<longrightarrow> (\<exists>y. get_etcb (cur_thread s) s = Some y) \<longrightarrow> valid_sched_2 (ready_queues s) (\<lambda>a. if a = cur_thread s then Some (the (get_etcb (cur_thread s) s)\<lparr>tcb_time_slice := tcb_time_slice t - Suc 0\<rparr>) else ekheap s a) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) \<and> (\<not> Suc 0 < tcb_time_slice t \<longrightarrow> (\<exists>y. get_etcb (cur_thread s) s = Some y) \<longrightarrow> valid_etcbs_2 (\<lambda>a. if a = cur_thread s then Some (the (get_etcb (cur_thread s) s)\<lparr>tcb_time_slice := timeSlice\<rparr>) else ekheap s a) (kheap s) \<and> valid_queues_2 (ready_queues s) (\<lambda>a. if a = cur_thread s then Some (the (get_etcb (cur_thread s) s)\<lparr>tcb_time_slice := timeSlice\<rparr>) else ekheap s a) (kheap s) \<and> st_tcb_at runnable (cur_thread s) s \<and> weak_valid_sched_action_2 (scheduler_action s) (\<lambda>a. if a = cur_thread s then Some (the (get_etcb (cur_thread s) s)\<lparr>tcb_time_slice := timeSlice\<rparr>) else ekheap s a) (kheap s) \<and> valid_blocked_except (cur_thread s) s \<and> valid_idle_etcb_2 (\<lambda>a. if a = cur_thread s then Some (the (get_etcb (cur_thread s) s)\<lparr>tcb_time_slice := timeSlice\<rparr>) else ekheap s a))) (cur_thread s) s