kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma set_thread_state_Restart_valid_sched:
  "\<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace>
     set_thread_state ct Restart \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (rule set_thread_state_active_valid_sched) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace> set_thread_state ct Restart \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma simple_sched_action_sched_act_not[simp]:
  "simple_sched_action s \<Longrightarrow> scheduler_act_not t s" by (fastforce simp: simple_sched_action_def scheduler_act_not_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple_sched_action s \<Longrightarrow> scheduler_act_not t s
theory DetSchedSchedule_AI

lemma ethread_set_not_activatable_valid_idle_etcb:
  "\<lbrace>valid_idle_etcb and valid_idle and st_tcb_at (\<lambda>ts. \<not> activatable ts) 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 (\<lambda>ts. \<not> activatable ts) 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 (\<lambda>ts. \<not> runnable ts \<and> ts \<noteq> IdleThreadState) 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 (\<lambda>ts. \<not> runnable ts \<and> ts \<noteq> IdleThreadState) 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_not_activatable_valid_sched:
  "\<lbrace>valid_sched and valid_idle and st_tcb_at (\<lambda>ts. \<not> activatable ts) 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_not_activatable_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 split: thread_state.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_idle and st_tcb_at (\<lambda>ts. \<not> activatable ts) 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 (\<lambda>ts. \<not> runnable ts \<and> ts \<noteq> IdleThreadState) 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 ethread_set_not_idle_valid_idle_etcb:
  "\<lbrace>valid_idle_etcb and valid_idle and (\<lambda>s. tptr \<noteq> idle_thread s)\<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 st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle_etcb and valid_idle and (\<lambda>s. tptr \<noteq> idle_thread s)\<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 (\<lambda>s. tptr \<noteq> idle_thread s)\<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 (\<lambda>s. tptr \<noteq> idle_thread s)) 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_not_idle_valid_sched:
  "\<lbrace>valid_sched and simple_sched_action and not_queued tptr and (\<lambda>s. tptr \<noteq> cur_thread s) and (\<lambda>s. tptr \<noteq> idle_thread s) and valid_idle\<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_not_idle_valid_idle_etcb)+ apply (force simp: simple_sched_action_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 split: thread_state.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action and not_queued tptr and (\<lambda>s. tptr \<noteq> cur_thread s) and (\<lambda>s. tptr \<noteq> idle_thread s) and valid_idle\<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> simple_sched_action s \<and> not_queued tptr s \<and> tptr \<noteq> cur_thread s \<and> tptr \<noteq> idle_thread s \<and> valid_idle s \<Longrightarrow> scheduler_action s \<noteq> switch_thread tptr \<and> not_cur_thread tptr s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_valid_blocked_except:
  "\<lbrace>valid_blocked_except t\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked_except t\<rbrace>" by (wp valid_blocked_except_lift | simp add: ethread_set_def set_eobject_def)+

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

lemma idle_not_reply_cap:
  "\<lbrakk> valid_idle s; valid_reply_caps s; cte_wp_at (is_reply_cap_to r) p s \<rbrakk> \<Longrightarrow> r \<noteq> idle_thread s" apply (drule_tac p=p in valid_reply_caps_of_stateD',assumption) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_reply_caps s; cte_wp_at (is_reply_cap_to r) p s\<rbrakk> \<Longrightarrow> r \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; cte_wp_at (is_reply_cap_to r) p s; st_tcb_at awaiting_reply r s\<rbrakk> \<Longrightarrow> r \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma idle_not_reply_cap':
  "\<lbrakk> valid_idle s; valid_reply_caps s; cte_wp_at ((=) (ReplyCap r False R)) p s \<rbrakk>
   \<Longrightarrow> r \<noteq> idle_thread s" apply (simp add: cte_wp_at_caps_of_state) apply (drule_tac p=p in valid_reply_caps_of_stateD,assumption) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_reply_caps s; cte_wp_at ((=) (ReplyCap r False R)) p s\<rbrakk> \<Longrightarrow> r \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_reply_caps s; caps_of_state s p = Some (ReplyCap r False R)\<rbrakk> \<Longrightarrow> r \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; caps_of_state s p = Some (ReplyCap r False R); st_tcb_at awaiting_reply r s\<rbrakk> \<Longrightarrow> r \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma valid_sched_ct_not_queued:
  "\<lbrakk>valid_sched s; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow>
    not_queued (cur_thread s) s" by (fastforce simp: valid_sched_def ct_not_in_q_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_sched s; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> ct_not_queued s
theory DetSchedSchedule_AI

lemma handle_reply_valid_sched:
  "\<lbrace>valid_sched and ct_active and invs\<rbrace> handle_reply \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: handle_reply_def) apply (wp get_cap_wp | wpc | clarsimp)+ apply (auto simp: invs_valid_objs idle_not_reply_cap' invs_valid_idle invs_valid_reply_caps is_reply_cap_to_def | erule cte_wp_at_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and ct_active and invs\<rbrace> handle_reply \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and ct_active and invs\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>valid_sched s; ct_active s; invs s; cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> valid_objs s \<and> cte_wp_at (is_reply_cap_to (?t'99 (cur_thread s) (ReplyCap x False xb) x False xb)) (cur_thread s, tcb_cnode_index 3) s \<and> x \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

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

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

lemma do_reply_transfer_not_queued[wp]:
  "\<lbrace>not_queued t and invs and st_tcb_at active t and scheduler_act_not t and
    K(receiver \<noteq> t)\<rbrace>
     do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. not_queued t\<rbrace>" apply (simp add: do_reply_transfer_def) apply (wp cap_delete_one_not_queued hoare_vcg_if_lift | wpc |
         clarsimp split del: if_split | wp (once) hoare_drop_imps)+ apply (simp add: invs_def valid_state_def valid_pspace_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_queued t and invs and st_tcb_at active t and scheduler_act_not t and K (receiver \<noteq> t)\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. not_queued t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_queued t and invs and st_tcb_at active t and scheduler_act_not t and (\<lambda>y. receiver \<noteq> t)\<rbrace> do state <- get_thread_state receiver;
y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
possible_switch_to receiver
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od)
od \<lbrace>\<lambda>_. not_queued t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>not_queued t s; invs s; st_tcb_at active t s; scheduler_act_not t s; receiver \<noteq> t\<rbrakk> \<Longrightarrow> valid_objs s \<and> valid_mdb s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> sym_refs (state_refs_of s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma do_reply_transfer_schedact_not[wp]:
  "\<lbrace>scheduler_act_not t and K(receiver \<noteq> t)\<rbrace>
     do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. scheduler_act_not t\<rbrace>" apply (simp add: do_reply_transfer_def) apply (wp hoare_vcg_if_lift | wpc | clarsimp split del: if_split |
         wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_act_not t and K (receiver \<noteq> t)\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. scheduler_act_not t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_act_not t and (\<lambda>y. receiver \<noteq> t)\<rbrace> do state <- get_thread_state receiver;
y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
possible_switch_to receiver
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od)
od \<lbrace>\<lambda>_. scheduler_act_not t\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma assert_false:"\<lbrace>\<lambda>s. \<not> P\<rbrace> assert P \<lbrace>\<lambda>_ _. False\<rbrace>" apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> P\<rbrace> assert P \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> P \<Longrightarrow> P \<longrightarrow> False proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma do_reply_transfer_ct_not_queued[wp]:
  "\<lbrace>ct_not_queued and invs and ct_active and scheduler_act_sane\<rbrace>
     do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. ct_not_queued\<rbrace>" apply (rule do_reply_transfer_add_assert) apply (rule hoare_pre) apply (wp ct_not_queued_lift) apply (clarsimp simp add: ct_in_state_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_queued and invs and ct_active and scheduler_act_sane\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. ct_not_queued\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at awaiting_reply receiver and (ct_not_queued and invs and ct_active and scheduler_act_sane)\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. ct_not_queued\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. ct_not_queued\<rbrace>
 2. \<And>s. (st_tcb_at awaiting_reply receiver and (ct_not_queued and invs and ct_active and scheduler_act_sane)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at awaiting_reply receiver and (ct_not_queued and invs and ct_active and scheduler_act_sane)) s \<Longrightarrow> (not_queued (cur_thread s) and invs and st_tcb_at active (cur_thread s) and scheduler_act_not (cur_thread s) and K (receiver \<noteq> cur_thread s)) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma do_reply_transfer_scheduler_act_sane[wp]:
  "\<lbrace>scheduler_act_sane and ct_active\<rbrace>
     do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. scheduler_act_sane\<rbrace>" apply (rule do_reply_transfer_add_assert) apply (rule hoare_pre) apply (wp sch_act_sane_lift) apply (clarsimp simp add: ct_in_state_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_act_sane and ct_active\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. scheduler_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at awaiting_reply receiver and (scheduler_act_sane and ct_active)\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. scheduler_act_sane\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. scheduler_act_sane\<rbrace>
 2. \<And>s. (st_tcb_at awaiting_reply receiver and (scheduler_act_sane and ct_active)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at awaiting_reply receiver and (scheduler_act_sane and ct_active)) s \<Longrightarrow> (scheduler_act_not (cur_thread s) and K (receiver \<noteq> cur_thread s)) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma handle_interrupt_valid_sched[wp]:
  "\<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace>
  handle_interrupt irq \<lbrace>\<lambda>rv. valid_sched\<rbrace>" unfolding handle_interrupt_def by (wpsimp wp: get_cap_wp hoare_drop_imps hoare_vcg_all_lift|rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace> handle_interrupt irq \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- get_irq_state irq;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op $ ackInterrupt irq
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma set_scheduler_action_switch_not_cur_thread [wp]:
  "\<lbrace>\<lambda>s. True\<rbrace> set_scheduler_action (switch_thread target) \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>" unfolding set_scheduler_action_def by wp (simp add: not_cur_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> set_scheduler_action (switch_thread target) \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> modify (scheduler_action_update (\<lambda>_. switch_thread target)) \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>
theory DetSchedSchedule_AI

lemma possible_switch_to_not_cur_thread [wp]:
  "\<lbrace>not_cur_thread t\<rbrace> possible_switch_to target \<lbrace>\<lambda>_. not_cur_thread t\<rbrace>" unfolding possible_switch_to_def apply (rule hoare_pre) apply (wp hoare_vcg_imp_lift|wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_cur_thread t\<rbrace> possible_switch_to target \<lbrace>\<lambda>_. not_cur_thread t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_cur_thread t\<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>_. not_cur_thread t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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>_. not_cur_thread t\<rbrace>
 2. \<And>s. not_cur_thread t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. not_cur_thread t s \<Longrightarrow> etcb_at (\<lambda>ta. (\<not> tcb_domain ta \<noteq> cur_domain s \<or> not_cur_thread t s) \<and> (\<not> \<not> tcb_domain ta \<noteq> cur_domain s \<or> (\<not> scheduler_action s \<noteq> resume_cur_thread \<or> True) \<and> (\<not> \<not> scheduler_action s \<noteq> resume_cur_thread \<or> True))) target s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma schedule_valid_list[wp]: "\<lbrace>valid_list\<rbrace> Schedule_A.schedule \<lbrace>\<lambda>_. valid_list\<rbrace>" apply (simp add: Schedule_A.schedule_def) apply (wp add: tcb_sched_action_valid_list gts_wp hoare_drop_imps
            del: ethread_get_wp
         | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> schedule \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma call_kernel_valid_list[wp]: "\<lbrace>valid_list\<rbrace> call_kernel e \<lbrace>\<lambda>_. valid_list\<rbrace>" apply (simp add: call_kernel_def) by (wp | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> call_kernel e \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do y <- handle_event e <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_. valid_list\<rbrace>