kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchSyscall_IF

lemma handle_vm_fault_globals_equiv[Syscall_IF_assms]:
  "\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
   handle_vm_fault thread vmfault_type
   \<lbrace>\<lambda>r. globals_equiv st\<rbrace>" apply (cases vmfault_type) apply (wp dmo_no_mem_globals_equiv | simp add: getDFSR_def getFAR_def getIFSR_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>r. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>r. globals_equiv st\<rbrace>
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>r. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_IF

lemma arch_activate_idle_thread_reads_respects[Syscall_IF_assms, wp]:
  "reads_respects aag l \<top> (arch_activate_idle_thread t)" unfolding arch_activate_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (arch_activate_idle_thread t) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (return ())
theory Scheduler_IF

lemma globals_equiv_from_scheduler:
  "\<lbrakk> globals_equiv_scheduler s s'; scheduler_globals_frame_equiv s s'; cur_thread s = cur_thread s';
     cur_thread s \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv s s' \<rbrakk>
     \<Longrightarrow> globals_equiv s s'" by (clarsimp simp: globals_equiv_scheduler_def scheduler_globals_frame_equiv_def
                     globals_equiv_def arch_globals_equiv_from_scheduler)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_equiv_scheduler s s'; scheduler_globals_frame_equiv s s'; cur_thread s = cur_thread s'; cur_thread s \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv s s'\<rbrakk> \<Longrightarrow> globals_equiv s s'
theory Scheduler_IF

lemma globals_equiv_scheduler_sym[elim]:
  "globals_equiv_scheduler s s' \<Longrightarrow> globals_equiv_scheduler s' s" by (auto simp: globals_equiv_scheduler_def idle_equiv_sym arch_globals_equiv_scheduler_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv_scheduler s s' \<Longrightarrow> globals_equiv_scheduler s' s
theory Scheduler_IF

lemma globals_equiv_scheduler_trans[elim]:
  "\<lbrakk> globals_equiv_scheduler s s'; globals_equiv_scheduler s' s'' \<rbrakk>
     \<Longrightarrow> globals_equiv_scheduler s s''" unfolding globals_equiv_scheduler_def by (fastforce elim: arch_globals_equiv_scheduler_trans idle_equiv_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s') \<and> idle_equiv s s' \<and> dom (device_state (machine_state s)) = dom (device_state (machine_state s')); arch_globals_equiv_scheduler (kheap s') (kheap s'') (arch_state s') (arch_state s'') \<and> idle_equiv s' s'' \<and> dom (device_state (machine_state s')) = dom (device_state (machine_state s''))\<rbrakk> \<Longrightarrow> arch_globals_equiv_scheduler (kheap s) (kheap s'') (arch_state s) (arch_state s'') \<and> idle_equiv s s'' \<and> dom (device_state (machine_state s)) = dom (device_state (machine_state s''))
theory Scheduler_IF

lemma scheduler_globals_frame_equiv_refl:
  "scheduler_globals_frame_equiv s s" by (simp add: scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_globals_frame_equiv s s
theory Scheduler_IF

lemma scheduler_globals_frame_equiv_sym[elim]:
  "scheduler_globals_frame_equiv s s' \<Longrightarrow> scheduler_globals_frame_equiv s' s" by (simp add: scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_globals_frame_equiv s s' \<Longrightarrow> scheduler_globals_frame_equiv s' s
theory Scheduler_IF

lemma scheduler_globals_frame_equiv_trans[elim]:
  "\<lbrakk> scheduler_globals_frame_equiv s s'; scheduler_globals_frame_equiv s' s'' \<rbrakk>
     \<Longrightarrow> scheduler_globals_frame_equiv s s''" by (simp add: scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_globals_frame_equiv s s'; scheduler_globals_frame_equiv s' s''\<rbrakk> \<Longrightarrow> scheduler_globals_frame_equiv s s''
theory Scheduler_IF

lemma preserves_equivalence_2_weak:
  assumes A: "(u,b) \<in> fst (f s)"
  assumes B: "(u',ba) \<in> fst (g t)"
  assumes R_preserved: "\<And>st. \<lbrace>P and R st\<rbrace> f \<lbrace>\<lambda>_. R st\<rbrace>"
  assumes R_preserved': "\<And>st. \<lbrace>S and R st\<rbrace> g \<lbrace>\<lambda>_. R st\<rbrace>"
  assumes R_sym: "\<forall>s s'. R s s' \<longrightarrow> R s' s"
  assumes R_trans: "\<forall>s s' s''. R s s' \<longrightarrow> R s' s'' \<longrightarrow> R s s''"
  shows "\<lbrakk> R s t; P s; S t \<rbrakk> \<Longrightarrow> R b ba" apply (insert A B) apply (drule use_valid[OF _ R_preserved]) apply simp apply (rule R_sym[rule_format]) apply assumption apply (drule use_valid[OF _ R_preserved']) apply simp apply (metis R_trans R_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s t; P s; S t\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s t; P s; S t; (u, b) \<in> fst (f s); (u', ba) \<in> fst (g t)\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t)\<rbrakk> \<Longrightarrow> (P and R ?st2) s
 2. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t); R ?st2 b\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t)\<rbrakk> \<Longrightarrow> R ?st2 s
 2. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t); R ?st2 b\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t)\<rbrakk> \<Longrightarrow> R s ?st2
 2. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t); R ?st2 b\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s t; P s; S t; (u', ba) \<in> fst (g t); R t b\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R s t; P s; S t; R t b\<rbrakk> \<Longrightarrow> (S and R ?st7) t
 2. \<lbrakk>R s t; P s; S t; R t b; R ?st7 ba\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s t; P s; S t; R t b; R s ba\<rbrakk> \<Longrightarrow> R b ba proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma preserves_equivalence_weak:
  assumes A: "(u,b) \<in> fst (f s)"
  assumes B: "(u',ba) \<in> fst (f t)"
  assumes R_preserved: "\<And>st. \<lbrace>P and R st\<rbrace> f \<lbrace>\<lambda>_. R st\<rbrace>"
  assumes R_sym: "\<forall>s s'. R s s' \<longrightarrow> R s' s"
  assumes R_trans: "\<forall>s s' s''. R s s' \<longrightarrow> R s' s'' \<longrightarrow> R s s''"
  shows "\<lbrakk> R s t; P s; P t \<rbrakk> \<Longrightarrow> R b ba" using assms by (blast intro: preserves_equivalence_2_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s t; P s; P t\<rbrakk> \<Longrightarrow> R b ba proof (prove)
using this:
(u, b) \<in> fst (f s)
(u', ba) \<in> fst (f t)
\<lbrace>P and R ?st\<rbrace> f \<lbrace>\<lambda>_. R ?st\<rbrace>
\<forall>s s'. R s s' \<longrightarrow> R s' s
\<forall>s s' s''. R s s' \<longrightarrow> R s' s'' \<longrightarrow> R s s''

goal (1 subgoal):
 1. \<lbrakk>R s t; P s; P t\<rbrakk> \<Longrightarrow> R b ba
theory Scheduler_IF

lemma scheduler_equiv_sym[elim]:
  "scheduler_equiv aag s s' \<Longrightarrow> scheduler_equiv aag s' s" by (simp add: scheduler_equiv_def domain_fields_equiv_def
                globals_equiv_scheduler_sym silc_dom_equiv_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_equiv aag s s' \<Longrightarrow> scheduler_equiv aag s' s
theory Scheduler_IF

lemma idle_equiv_machine_state_update[simp]:
  "idle_equiv st (s\<lparr>machine_state := x\<rparr>) = idle_equiv st s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv st (s\<lparr>machine_state := x\<rparr>) = idle_equiv st s
theory Scheduler_IF

lemma idle_equiv_machine_state_update'[simp]:
  "idle_equiv (st\<lparr>machine_state := x\<rparr>) s = idle_equiv st s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv (st\<lparr>machine_state := x\<rparr>) s = idle_equiv st s
theory Scheduler_IF

lemma idle_equiv_cur_thread_update'[simp]:
  "idle_equiv (st\<lparr>cur_thread := x\<rparr>) s = idle_equiv st s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv (st\<lparr>cur_thread := x\<rparr>) s = idle_equiv st s
theory Scheduler_IF

lemma silc_dom_equiv_scheduler_action_update[simp]:
  "silc_dom_equiv aag st (s\<lparr>scheduler_action := x\<rparr>) = silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag st (scheduler_action_update (\<lambda>_. x) s) = silc_dom_equiv aag st s
theory Scheduler_IF

lemma idle_equiv_scheduler_action_update[simp]:
  "idle_equiv (scheduler_action_update f st) s = idle_equiv st s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv (scheduler_action_update f st) s = idle_equiv st s
theory Scheduler_IF

lemma idle_equiv_scheduler_action_update'[simp]:
  "idle_equiv st (scheduler_action_update f s) = idle_equiv st s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv st (scheduler_action_update f s) = idle_equiv st s
theory Scheduler_IF

lemma scheduler_globals_frame_equiv_cur_thread_update[simp]:
  "scheduler_globals_frame_equiv st (s\<lparr>cur_thread := x\<rparr>) = scheduler_globals_frame_equiv st s" by (simp add: scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_globals_frame_equiv st (s\<lparr>cur_thread := x\<rparr>) = scheduler_globals_frame_equiv st s
theory Scheduler_IF

lemma scheduler_globals_frame_equiv_ready_queues_update[simp]:
  "scheduler_globals_frame_equiv st (s\<lparr>ready_queues := x\<rparr>) = scheduler_globals_frame_equiv st s" by (simp add: scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_globals_frame_equiv st (ready_queues_update (\<lambda>_. x) s) = scheduler_globals_frame_equiv st s
theory Scheduler_IF

lemma scheduler_globals_frame_equiv_ready_queues_update'[simp]:
  "scheduler_globals_frame_equiv (st\<lparr>ready_queues := x\<rparr>) s = scheduler_globals_frame_equiv st s" by (simp add: scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_globals_frame_equiv (ready_queues_update (\<lambda>_. x) st) s = scheduler_globals_frame_equiv st s
theory Scheduler_IF

lemma silc_dom_equiv_cur_thread_update[simp]:
  "silc_dom_equiv aag st (s\<lparr>cur_thread := x\<rparr>) = silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag st (s\<lparr>cur_thread := x\<rparr>) = silc_dom_equiv aag st s
theory Scheduler_IF

lemma silc_dom_equiv_ready_queues_update[simp]:
  "silc_dom_equiv aag st (s\<lparr>ready_queues := x\<rparr>) = silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag st (ready_queues_update (\<lambda>_. x) s) = silc_dom_equiv aag st s
theory Scheduler_IF

lemma silc_dom_equiv_ready_queues_update'[simp]:
  "silc_dom_equiv aag (st\<lparr>ready_queues := x\<rparr>) s = silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag (ready_queues_update (\<lambda>_. x) st) s = silc_dom_equiv aag st s
theory Scheduler_IF

lemma silc_dom_equiv_cur_thread_update'[simp]:
  "silc_dom_equiv aag (st\<lparr>cur_thread := x\<rparr>) s = silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag (st\<lparr>cur_thread := x\<rparr>) s = silc_dom_equiv aag st s
theory Scheduler_IF

lemma tcb_domain_wellformed:
  "\<lbrakk> pas_refined aag s; ekheap s t = Some a \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain a)" apply (clarsimp simp add: pas_refined_def tcb_domain_map_wellformed_aux_def) apply (drule_tac x="(t,tcb_domain a)" in bspec) apply (rule domtcbs) apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; ekheap s t = Some a\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ekheap s t = Some a; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ekheap s t = Some a; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (t, tcb_domain a) \<in> domains_of_state s
 2. \<lbrakk>ekheap s t = Some a; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (t, tcb_domain a) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ekheap s t = Some a; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> ekheap s t = Some ?etcb16
 2. \<lbrakk>ekheap s t = Some a; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> tcb_domain a = tcb_domain ?etcb16
 3. \<lbrakk>ekheap s t = Some a; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (t, tcb_domain a) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain a) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma silc_dom_equiv_trans_state[simp]:
  "silc_dom_equiv aag st (trans_state f s) = silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag st (trans_state f s) = silc_dom_equiv aag st s
theory Scheduler_IF

lemma (in is_extended') silc_dom_equiv[wp]:
  "I (silc_dom_equiv aag st)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>
theory Scheduler_IF

lemma set_scheduler_action_rev_scheduler[wp]:
  "reads_respects_scheduler aag l \<top> (set_scheduler_action a)" apply (clarsimp simp: set_scheduler_action_def) apply (rule ev_modify) by (clarsimp simp: scheduler_affects_equiv_def scheduler_equiv_def states_equiv_for_def
                     equiv_asids_def domain_fields_equiv_def globals_equiv_scheduler_def
                     silc_dom_equiv_def scheduler_globals_frame_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (set_scheduler_action a) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (modify (scheduler_action_update (\<lambda>_. a))) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; True; scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag (scheduler_action_update (\<lambda>_. a) s) (scheduler_action_update (\<lambda>_. a) t) \<and> scheduler_affects_equiv aag l (scheduler_action_update (\<lambda>_. a) s) (scheduler_action_update (\<lambda>_. a) t)
theory Scheduler_IF

lemma globals_equiv_scheduler_cur_thread_update[simp]:
  "globals_equiv_scheduler st (s\<lparr>cur_thread := x\<rparr>) = globals_equiv_scheduler st s" by (simp add: globals_equiv_scheduler_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv_scheduler st (s\<lparr>cur_thread := x\<rparr>) = globals_equiv_scheduler st s
theory Scheduler_IF

lemma globals_equiv_scheduler_trans_state_update[simp]:
  "globals_equiv_scheduler st (trans_state f s) = globals_equiv_scheduler st s" by (simp add: globals_equiv_scheduler_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv_scheduler st (trans_state f s) = globals_equiv_scheduler st s
theory Scheduler_IF

lemma states_equiv_for_cur_thread_update[simp]:
  "states_equiv_for P Q R S s (s'\<lparr>cur_thread := x\<rparr>) = states_equiv_for P Q R S s s'" by (simp add: states_equiv_for_def equiv_for_def equiv_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S s (s'\<lparr>cur_thread := x\<rparr>) = states_equiv_for P Q R S s s'
theory Scheduler_IF

lemma scheduler_equiv_ready_queues_update[simp]:
  "scheduler_equiv aag (st\<lparr>ready_queues := x\<rparr>) s = scheduler_equiv aag st s" by (simp add: scheduler_equiv_def domain_fields_equiv_def
                globals_equiv_scheduler_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_equiv aag (ready_queues_update (\<lambda>_. x) st) s = scheduler_equiv aag st s
theory Scheduler_IF

lemma scheduler_equiv_ready_queues_update'[simp]:
  "scheduler_equiv aag st (s\<lparr>ready_queues := x\<rparr>) = scheduler_equiv aag st s" by (simp add: scheduler_equiv_def domain_fields_equiv_def
                globals_equiv_scheduler_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_equiv aag st (ready_queues_update (\<lambda>_. x) s) = scheduler_equiv aag st s
theory Scheduler_IF

lemma get_tcb_queue_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l (K(pasDomainAbs aag rv \<inter> reads_scheduler aag l \<noteq> {}))
                            (get_tcb_queue rv rva)" apply (rule gen_asm_ev) apply (simp add: get_tcb_queue_def) apply (subst gets_apply) apply (wp gets_apply_ev) apply (force simp: scheduler_affects_equiv_def states_equiv_for_def
                     equiv_for_def disjoint_iff_not_equal) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (K (pasDomainAbs aag rv \<inter> reads_scheduler aag l \<noteq> {})) (get_tcb_queue rv rva) proof (prove)
goal (1 subgoal):
 1. pasDomainAbs aag rv \<inter> reads_scheduler aag l \<noteq> {} \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (get_tcb_queue rv rva) proof (prove)
goal (1 subgoal):
 1. pasDomainAbs aag rv \<inter> reads_scheduler aag l \<noteq> {} \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do queues <- gets ready_queues;
return (queues rv rva)
od) proof (prove)
goal (1 subgoal):
 1. pasDomainAbs aag rv \<inter> reads_scheduler aag l \<noteq> {} \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do a <- gets_apply ready_queues rv;
return (a rva)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasDomainAbs aag rv \<inter> reads_scheduler aag l \<noteq> {}; True\<rbrakk> \<Longrightarrow> K (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> ready_queues s rv = ready_queues t rv) s proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma ethread_get_when_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l (K (b \<longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l))
    (ethread_get_when b f t)" apply (simp add: ethread_get_when_def) apply (rule conjI; clarsimp) using ethread_get_reads_respects_scheduler apply fastforce apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (K (b \<longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l)) (ethread_get_when b f t) proof (prove)
goal (1 subgoal):
 1. (b \<longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. pasObjectAbs aag t \<in> reads_scheduler aag l) (ethread_get f t)) \<and> (\<not> b \<longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. True) (return undefined)) proof (prove)
goal (2 subgoals):
 1. b \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. pasObjectAbs aag t \<in> reads_scheduler aag l) (ethread_get f t)
 2. \<not> b \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. True) (return undefined) proof (prove)
using this:
equiv_valid_inv (scheduler_equiv ?aag) (scheduler_affects_equiv ?aag ?l) (K (pasObjectAbs ?aag ?t \<in> reads_scheduler ?aag ?l)) (ethread_get ?f ?t)

goal (2 subgoals):
 1. b \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. pasObjectAbs aag t \<in> reads_scheduler aag l) (ethread_get f t)
 2. \<not> b \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. True) (return undefined) proof (prove)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>y. True) (return undefined) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma globals_frame_equiv_as_states_equiv:
  "scheduler_globals_frame_equiv st s =
   states_equiv_for (\<lambda>x. x \<in> scheduler_affects_globals_frame s) \<bottom> \<bottom> \<bottom>
                    (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s" by (simp add: states_equiv_for_def equiv_for_def scheduler_globals_frame_equiv_def equiv_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_globals_frame_equiv st s = states_equiv_for (\<lambda>x. x \<in> {}) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s