kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF

lemma big_step_adt_Step_system:
  "Init_inv_Fin_system C s0 \<Longrightarrow> Step_system (big_step_adt C R exmap) s0" apply (rule Init_Fin_system_Step_system) apply (rule Init_inv_Fin_system_Init_Fin_system) apply (rule big_step_adt_Init_inv_Fin_system) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system C s0 \<Longrightarrow> Step_system (big_step_adt C R exmap) s0 proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system C s0 \<Longrightarrow> Init_Fin_system (big_step_adt C R exmap) s0 proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system C s0 \<Longrightarrow> Init_inv_Fin_system (big_step_adt C R exmap) s0 proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system C s0 \<Longrightarrow> Init_inv_Fin_system C s0 proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma big_step_adt_enabled_Step_system:
  assumes single_event: "\<forall>(x::'b) (y::'b). x = y"
  assumes nrefl: "\<And>s. \<not> R s s"
  assumes ifsw: "Init_Fin_serial_weak A s0 I"
  assumes iifs: "Init_inv_Fin_system A s0"
  assumes rt: "rel_terminate A s0 R I measuref"
  shows "enabled_Step_system (big_step_adt A R (examp::('a list \<Rightarrow> 'b))) s0" using assms by (simp add: enabled_Step_system_def big_step_adt_Step_system big_step_adt_enabled_system)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enabled_Step_system (big_step_adt A R examp) s0 proof (prove)
using this:
\<forall>x y. x = y
\<not> R ?s ?s
Init_Fin_serial_weak A s0 I
Init_inv_Fin_system A s0
rel_terminate A s0 R I measuref

goal (1 subgoal):
 1. enabled_Step_system (big_step_adt A R examp) s0
theory ADT_IF

lemma no_irq_user_memory_update[simp]:
  "no_irq (user_memory_update a)" by (wpsimp simp: no_irq_def user_memory_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (user_memory_update a)
theory ADT_IF

lemma no_irq_device_memory_update[simp]:
  "no_irq (device_memory_update a)" by (wpsimp simp: no_irq_def device_memory_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (device_memory_update a)
theory ADT_IF

lemma thread_set_tcb_context_update_ct_active[wp]:
  "thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>ct_active\<rbrace>" apply (simp add: thread_set_def ct_in_state_def | wp set_object_wp)+ apply (clarsimp simp: st_tcb_at_def obj_at_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_. ct_active\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at active (cur_thread s) s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> st_tcb_at active (cur_thread s) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set f) (the (get_tcb t s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma thread_set_tcb_context_update_not_ct_active[wp]:
  "thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>s. \<not> ct_active s\<rbrace>" apply (simp add: thread_set_def ct_in_state_def | wp set_object_wp)+ apply (clarsimp simp: st_tcb_at_def obj_at_def get_tcb_def
                 split: kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> ct_active s\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. \<not> ct_active s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> st_tcb_at active (cur_thread s) s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> st_tcb_at active (cur_thread s) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set f) (the (get_tcb t s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma kernel_entry_if_invs:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. invs\<rbrace>" unfolding kernel_entry_if_def by (wpsimp wp: thread_set_invs_trivial hoare_weak_lift_imp
           simp: arch_tcb_update_aux2 ran_tcb_cap_cases)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc)
od \<lbrace>\<lambda>_. invs\<rbrace>
theory ADT_IF

lemma kernel_entry_if_globals_equiv:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st
         and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (simp add: kernel_entry_if_def) apply (wp hoare_weak_lift_imp handle_event_globals_equiv
            thread_set_invs_trivial thread_set_context_globals_equiv
         | simp add: ran_tcb_cap_cases arch_tcb_update_aux2)+ apply (clarsimp simp: cur_thread_idle) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> globals_equiv st s \<and> (ct_idle s \<longrightarrow> tc = idle_context s) \<Longrightarrow> cur_thread s = idle_thread s \<longrightarrow> tc = idle_context s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma thread_set_tcb_context_update_domain_sep_inv[wp]:
  "thread_set (tcb_arch_update f) t \<lbrace>domain_sep_inv irqs st\<rbrace>" by (wp domain_sep_inv_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> thread_set (tcb_arch_update f) t \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory ADT_IF

lemma kernel_entry_silc_inv[wp]:
  "\<lbrace>silc_inv aag st and einvs and simple_sched_action and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)
                    and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
                    and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
   kernel_entry_if ev tc
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding kernel_entry_if_def by (wpsimp simp: ran_tcb_cap_cases arch_tcb_update_aux2
               wp: hoare_weak_lift_imp handle_event_silc_inv thread_set_silc_inv thread_set_invs_trivial
                   thread_set_not_state_valid_sched thread_set_pas_refined
      | wp (once) hoare_vcg_imp_lift | force)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event ev;
return (r, tc)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory ADT_IF

lemma kernel_entry_pas_refined[wp]:
  "\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st
                    and einvs and schact_is_rct
                    and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
                    and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   kernel_entry_if ev tc
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" unfolding kernel_entry_if_def by (wpsimp simp: ran_tcb_cap_cases schact_is_rct_def arch_tcb_update_aux2
               wp: hoare_weak_lift_imp handle_event_pas_refined thread_set_pas_refined
                   guarded_pas_domain_lift thread_set_invs_trivial thread_set_not_state_valid_sched
      | force)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event ev;
return (r, tc)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ADT_IF

lemma kernel_entry_if_valid_sched:
  "\<lbrace>valid_sched and invs and (ct_active or ct_idle)
                and (\<lambda>s. (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> scheduler_action s = resume_cur_thread)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (wpsimp simp: kernel_entry_if_def ran_tcb_cap_cases arch_tcb_update_aux2
               wp: handle_event_valid_sched thread_set_invs_trivial hoare_vcg_disj_lift
                   thread_set_no_change_tcb_state ct_in_state_thread_state_lift
                   thread_set_not_state_valid_sched hoare_weak_lift_imp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and (ct_active or ct_idle) and (\<lambda>s. (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> scheduler_action s = resume_cur_thread)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory ADT_IF

lemma kernel_entry_if_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" by (simp add: kernel_entry_if_def ran_tcb_cap_cases arch_tcb_update_aux2
      | wp handle_event_irq_masks thread_set_invs_trivial | force)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory ADT_IF

lemma activate_thread_guarded_pas_domain[wp]:
  "activate_thread \<lbrace>guarded_pas_domain aag\<rbrace>" by (rule guarded_pas_domain_lift; wp activate_thread_cur_thread)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag\<rbrace> activate_thread \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>
theory ADT_IF

lemma kernel_entry_if_guarded_pas_domain:
  "kernel_entry_if e tc \<lbrace>guarded_pas_domain aag\<rbrace>" apply (simp add: kernel_entry_if_def) apply (wp guarded_pas_domain_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc)
od \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma handle_preemption_if_invs:
  "handle_preemption_if tc \<lbrace>invs\<rbrace>" by (simp add: handle_preemption_if_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. invs\<rbrace>
theory ADT_IF

lemma handle_preemption_if_domain_sep_inv:
  "handle_preemption_if e \<lbrace>domain_sep_inv irqs st\<rbrace>" by (simp add: handle_preemption_if_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> handle_preemption_if e \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory ADT_IF

lemma handle_preemption_if_silc_inv[wp]:
  "handle_preemption_if tc \<lbrace>silc_inv aag st\<rbrace>" apply (simp add: handle_preemption_if_def) apply (wp handle_interrupt_silc_inv do_machine_op_silc_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do irq <- do_machine_op (getActiveIRQ True);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return tc
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma handle_preemption_if_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   handle_preemption_if tc
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wpsimp wp: handle_interrupt_pas_refined getActiveIRQ_wp hoare_drop_imps
           simp: handle_preemption_if_def if_fun_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ADT_IF

lemma handle_preemption_if_guarded_pas_domain[wp]:
  "handle_preemption_if tc \<lbrace>guarded_pas_domain aag\<rbrace>" by (rule guarded_pas_domain_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>
theory ADT_IF

lemma schedule_if_invs[wp]:
  "schedule_if tc \<lbrace>invs\<rbrace>" by (simp add: schedule_if_def | wp | rule hoare_strengthen_post[OF activate_invs])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule_if tc \<lbrace>\<lambda>_. invs\<rbrace>
theory ADT_IF

lemma guarded_pas_domain_arch_state_update[simp]:
  "guarded_pas_domain aag (s\<lparr>arch_state := x\<rparr>) = guarded_pas_domain aag s" by (simp add: guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain aag (s\<lparr>arch_state := x\<rparr>) = guarded_pas_domain aag s
theory ADT_IF

lemma switch_to_thread_guarded_pas_domain:
  "\<lbrace>\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)\<rbrace>
   switch_to_thread t
   \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" apply (simp add: switch_to_thread_def) apply (wp modify_wp hoare_drop_imps| simp add: guarded_pas_domain_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma guarded_pas_domain_machine_state_update[simp]:
  "guarded_pas_domain aag (s\<lparr>machine_state := x\<rparr>) = guarded_pas_domain aag s" by (simp add: guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain aag (s\<lparr>machine_state := x\<rparr>) = guarded_pas_domain aag s
theory ADT_IF

lemma switch_to_idle_thread_guarded_pas_domain[wp]:
  "\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" apply (simp add: switch_to_idle_thread_def bind_assoc double_gets_drop_regets) apply (wp modify_wp dmo_wp hoare_vcg_imp_lift | wp (once) | simp add: guarded_pas_domain_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma schedule_if_ct_running_or_ct_idle[wp]:
  "\<lbrace>invs\<rbrace> schedule_if tc \<lbrace>\<lambda>_ s. ct_running s \<or> ct_idle s\<rbrace>" apply (simp add: schedule_if_def | wp)+ apply (rule hoare_strengthen_post[OF activate_invs] | simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule_if tc \<lbrace>\<lambda>_ s. ct_running s \<or> ct_idle s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> activate_thread \<lbrace>\<lambda>ya a. ct_running a \<or> ct_idle a\<rbrace>
 2. \<lbrace>?Q\<rbrace> schedule \<lbrace>?B1\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma schedule_if_guarded_pas_domain[wp]:
  "\<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<rbrace>
   schedule_if tc
   \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" apply (simp add: schedule_if_def) apply (wp schedule_guarded_pas_domain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<rbrace> schedule_if tc \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<rbrace> do y <- schedule;
y <- activate_thread;
return tc
od \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma activate_thread_scheduler_action[wp]:
  "activate_thread \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>" apply (simp add: activate_thread_def | wp set_thread_state_scheduler_action gts_wp | wpc)+ apply (fastforce elim: st_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> activate_thread \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (scheduler_action s) \<Longrightarrow> st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma schedule_if_scheduler_action[wp]:
  "\<lbrace>\<top>\<rbrace> schedule_if tc \<lbrace>\<lambda>_ s. scheduler_action s = resume_cur_thread\<rbrace>" apply (simp add: schedule_if_def | wp | wpc)+ apply (simp add: schedule_def schedule_choose_new_thread_def split del: if_split | wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> schedule_if tc \<lbrace>\<lambda>_ s. scheduler_action s = resume_cur_thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> schedule \<lbrace>\<lambda>y s. scheduler_action s = resume_cur_thread\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma do_user_op_if_only_timer_irq_inv[wp]:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>
   do_user_op_if uop tc
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (rule hoare_pre) apply (wp only_timer_irq_inv_pres | simp | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>
 2. \<And>s. only_timer_irq_inv irq st s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma kernel_entry_if_only_timer_irq_inv:
  "\<lbrace>only_timer_irq_inv irq st and einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" by (wp only_timer_irq_inv_pres kernel_entry_if_irq_masks kernel_entry_if_domain_sep_inv
       | simp | blast)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st and einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>
theory ADT_IF

lemma check_active_irq_if_wp:
  "\<lbrace>\<lambda>s. P ((irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))),tc)
          (s\<lparr>machine_state := (machine_state s\<lparr>irq_state := irq_state (machine_state s) + 1\<rparr>)\<rparr>)\<rbrace>
   check_active_irq_if tc
   \<lbrace>P\<rbrace>" by (wpsimp wp: dmo_getActiveIRQ_wp simp: check_active_irq_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)), tc) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state (machine_state s) + 1\<rparr>\<rparr>)\<rbrace> check_active_irq_if tc \<lbrace>P\<rbrace>
theory ADT_IF

lemma handle_preemption_if_only_timer_irq_inv[wp]:
  "handle_preemption_if tc \<lbrace>only_timer_irq_inv irq st\<rbrace>" by (wp only_timer_irq_inv_pres handle_preemption_if_irq_masks handle_preemption_if_domain_sep_inv
      | simp | blast)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>
theory ADT_IF

lemma schedule_if_only_timer_irq_inv[wp]:
  "schedule_if tc \<lbrace>only_timer_irq_inv irq st\<rbrace>" by (wp only_timer_irq_inv_pres schedule_if_irq_masks | blast)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> schedule_if tc \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>
theory ADT_IF

lemma schedule_if_domain_time_nonzero:
  "\<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
   schedule_if tc
   \<lbrace>\<lambda>_ s. domain_time s \<noteq> 0\<rbrace>" apply (rule hoare_strengthen_post[OF schedule_if_domain_time_nonzero']) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> schedule_if tc \<lbrace>\<lambda>_ s. domain_time s \<noteq> 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. 0 < domain_time s \<Longrightarrow> domain_time s \<noteq> 0 proof (prove)
goal:
No subgoals!