theory ArchScheduler_IF

lemma dmo_resetTimer_reads_respects_scheduler[Scheduler_IF_assms]:
  "reads_respects_scheduler aag l \<top> (do_machine_op resetTimer)" apply (rule reads_respects_scheduler_unobservable) apply (rule scheduler_equiv_lift) apply (simp add: globals_equiv_scheduler_def[abs_def]  idle_equiv_def) apply (wpsimp wp: dmo_wp) apply ((wp silc_dom_lift dmo_wp | simp)+)[5] apply (rule scheduler_affects_equiv_unobservable) apply (simp add: states_equiv_for_def[abs_def] equiv_for_def equiv_asids_def equiv_asid_def) apply (rule hoare_pre) apply (wp  | simp add: arch_scheduler_affects_equiv_def | wp dmo_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do_machine_op resetTimer) proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>scheduler_equiv aag st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>st sta. \<lbrace>globals_equiv_scheduler sta\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>sta. \<lbrace>\<lambda>s'. arch_globals_equiv_scheduler (kheap sta) (kheap s') (arch_state sta) (arch_state s') \<and> idle_thread sta = idle_thread s' \<and> (\<forall>tcb. kheap sta (idle_thread sta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap s' (idle_thread sta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> tcb_at (idle_thread sta) sta = tcb_at (idle_thread sta) s' \<and> dom (device_state (machine_state sta)) = dom (device_state (machine_state s'))\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s'. arch_globals_equiv_scheduler (kheap sta) (kheap s') (arch_state sta) (arch_state s') \<and> idle_thread sta = idle_thread s' \<and> (\<forall>tcb. kheap sta (idle_thread sta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap s' (idle_thread sta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> tcb_at (idle_thread sta) sta = tcb_at (idle_thread sta) s' \<and> dom (device_state (machine_state sta)) = dom (device_state (machine_state s'))\<rbrace>
 2. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 2. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 3. \<And>st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 5. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 6. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>st P Q R S sta. \<lbrace>states_equiv_for P Q R S sta\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. states_equiv_for P Q R S sta\<rbrace>
 2. \<And>st P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 7. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>P Q R S sta. \<lbrace>\<lambda>s'. (\<forall>x. P x \<longrightarrow> kheap sta x = kheap s' x) \<and> (\<forall>x. P x \<longrightarrow> underlying_memory (machine_state sta) x = underlying_memory (machine_state s') x) \<and> (\<forall>x. P x \<longrightarrow> device_state (machine_state sta) x = device_state (machine_state s') x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt sta (a, b) = cdt s' (a, b))) \<and> (\<forall>x. P x \<longrightarrow> ekheap sta x = ekheap s' x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list sta (a, b) = cdt_list s' (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap sta (a, b) = is_original_cap s' (a, b))) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_states sta x = interrupt_states s' x) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_irq_node sta x = interrupt_irq_node s' x) \<and> (\<forall>x. S x \<longrightarrow> ready_queues sta x = ready_queues s' x) \<and> (\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> asid_table sta (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table sta (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr sta = typ_at (AArch AASIDPool) pool_ptr s' \<and> (\<forall>asid_pool asid_pool'. kheap sta pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s'. (\<forall>x. P x \<longrightarrow> kheap sta x = kheap s' x) \<and> (\<forall>x. P x \<longrightarrow> underlying_memory (machine_state sta) x = underlying_memory (machine_state s') x) \<and> (\<forall>x. P x \<longrightarrow> device_state (machine_state sta) x = device_state (machine_state s') x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt sta (a, b) = cdt s' (a, b))) \<and> (\<forall>x. P x \<longrightarrow> ekheap sta x = ekheap s' x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list sta (a, b) = cdt_list s' (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap sta (a, b) = is_original_cap s' (a, b))) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_states sta x = interrupt_states s' x) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_irq_node sta x = interrupt_irq_node s' x) \<and> (\<forall>x. S x \<longrightarrow> ready_queues sta x = ready_queues s' x) \<and> (\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> asid_table sta (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table sta (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr sta = typ_at (AArch AASIDPool) pool_ptr s' \<and> (\<forall>asid_pool asid_pool'. kheap sta pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))\<rbrace>
 2. \<And>st P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 7. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>P Q R S sta. \<lbrace>?Q88 P Q R S sta\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s'. (\<forall>x. P x \<longrightarrow> kheap sta x = kheap s' x) \<and> (\<forall>x. P x \<longrightarrow> underlying_memory (machine_state sta) x = underlying_memory (machine_state s') x) \<and> (\<forall>x. P x \<longrightarrow> device_state (machine_state sta) x = device_state (machine_state s') x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt sta (a, b) = cdt s' (a, b))) \<and> (\<forall>x. P x \<longrightarrow> ekheap sta x = ekheap s' x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list sta (a, b) = cdt_list s' (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap sta (a, b) = is_original_cap s' (a, b))) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_states sta x = interrupt_states s' x) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_irq_node sta x = interrupt_irq_node s' x) \<and> (\<forall>x. S x \<longrightarrow> ready_queues sta x = ready_queues s' x) \<and> (\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> asid_table sta (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table sta (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr sta = typ_at (AArch AASIDPool) pool_ptr s' \<and> (\<forall>asid_pool asid_pool'. kheap sta pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))\<rbrace>
 2. \<And>P Q R S sta s. (\<forall>x. P x \<longrightarrow> kheap sta x = kheap s x) \<and> (\<forall>x. P x \<longrightarrow> underlying_memory (machine_state sta) x = underlying_memory (machine_state s) x) \<and> (\<forall>x. P x \<longrightarrow> device_state (machine_state sta) x = device_state (machine_state s) x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt sta (a, b) = cdt s (a, b))) \<and> (\<forall>x. P x \<longrightarrow> ekheap sta x = ekheap s x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list sta (a, b) = cdt_list s (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap sta (a, b) = is_original_cap s (a, b))) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_states sta x = interrupt_states s x) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_irq_node sta x = interrupt_irq_node s x) \<and> (\<forall>x. S x \<longrightarrow> ready_queues sta x = ready_queues s x) \<and> (\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> asid_table sta (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table sta (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr sta = typ_at (AArch AASIDPool) pool_ptr s \<and> (\<forall>asid_pool asid_pool'. kheap sta pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)))) \<Longrightarrow> ?Q88 P Q R S sta s
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 7. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 8. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal:
No subgoals!