theory ArchScheduler_IF

lemma ackInterrupt_reads_respects_scheduler[Scheduler_IF_assms]:
  "reads_respects_scheduler aag l \<top> (do_machine_op (ackInterrupt irq))" apply (rule reads_respects_scheduler_unobservable) apply (rule scheduler_equiv_lift) apply (simp add:  globals_equiv_scheduler_def[abs_def] idle_equiv_def) apply (rule hoare_pre) apply wps apply (wp dmo_wp ackInterrupt_irq_masks | simp add:no_irq_def)+ apply clarsimp 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 wps apply (wp dmo_wp | simp add: arch_scheduler_affects_equiv_def ackInterrupt_def)+ apply (wp mol_exclusive_state) apply (simp add: arch_scheduler_affects_equiv_def) 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 (ackInterrupt irq)) proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>scheduler_equiv aag st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>sta. \<lbrace>?Q10 sta\<rbrace> do_machine_op (ackInterrupt irq) \<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>sta 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)) \<Longrightarrow> ?Q10 sta s
 3. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 5. \<And>st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 7. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 8. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>sta prev_s. \<lbrace>?P13 sta prev_s\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>rv s'. arch_globals_equiv_scheduler (kheap sta) (kheap prev_s) (arch_state sta) (arch_state prev_s) \<and> idle_thread sta = idle_thread prev_s \<and> (\<forall>tcb. kheap sta (idle_thread sta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap prev_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) prev_s \<and> dom (device_state (machine_state sta)) = dom (device_state (machine_state s'))\<rbrace>
 2. \<And>sta 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)) \<Longrightarrow> ?P13 sta s s
 3. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 5. \<And>st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 7. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 8. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>sta 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)) \<Longrightarrow> tcb_at (idle_thread s) sta = tcb_at (idle_thread s) s
 2. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 2. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 5. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 6. \<And>st. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 7. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op (ackInterrupt irq) \<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 (ackInterrupt irq) \<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 (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 7. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>P Q R S sta. \<lbrace>?Q91 P Q R S sta\<rbrace> do_machine_op (ackInterrupt irq) \<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> ?Q91 P Q R S sta s
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 7. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 8. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>P Q R S sta prev_s. \<lbrace>?P94 P Q R S sta prev_s\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>rv s'. (\<forall>x. P x \<longrightarrow> kheap sta x = kheap prev_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 prev_s (a, b))) \<and> (\<forall>x. P x \<longrightarrow> ekheap sta x = ekheap prev_s x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list sta (a, b) = cdt_list prev_s (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap sta (a, b) = is_original_cap prev_s (a, b))) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_states sta x = interrupt_states prev_s x) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_irq_node sta x = interrupt_irq_node prev_s x) \<and> (\<forall>x. S x \<longrightarrow> ready_queues sta x = ready_queues prev_s x) \<and> (\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> asid_table sta (asid_high_bits_of asid) = asid_table prev_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 prev_s \<and> (\<forall>asid_pool asid_pool'. kheap sta pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap prev_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> ?P94 P Q R S sta s s
 3. \<And>st P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 4. \<And>st P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
 6. \<And>st P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (work_units_completed s)\<rbrace>
 7. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 8. \<And>st. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrace>?P168 st s\<rbrace> machine_op_lift (ackInterrupt_impl irq) \<lbrace>\<lambda>a b. exclusive_state (machine_state st) = exclusive_state b\<rbrace>
 2. \<And>st s. arch_scheduler_affects_equiv st s \<Longrightarrow> ?P168 st s (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>st s. arch_scheduler_affects_equiv st s \<Longrightarrow> exclusive_state (machine_state st) = exclusive_state (machine_state s) proof (prove)
goal:
No subgoals!