theory ADT_H

lemma absExst_correct:
  assumes invs: "einvs s" and invs': "invs' s'"
  assumes rel: "(s, s') \<in> state_relation"
  shows "absExst s' = exst s" apply (rule det_ext.equality) using rel invs invs' apply (simp_all add: absExst_def absSchedulerAction_correct absEkheap_correct
                           absCDTList_correct[THEN fun_cong] state_relation_def invs_def valid_state_def
                           ready_queues_relation_def invs'_def valid_state'_def
                           valid_pspace_def valid_sched_def valid_pspace'_def curry_def fun_eq_iff) apply (fastforce simp: absEkheap_correct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absExst s' = exst s proof (prove)
goal (10 subgoals):
 1. work_units_completed_internal (absExst s') = work_units_completed s
 2. scheduler_action_internal (absExst s') = scheduler_action s
 3. ekheap_internal (absExst s') = ekheap s
 4. domain_list_internal (absExst s') = domain_list s
 5. domain_index_internal (absExst s') = domain_index s
 6. cur_domain_internal (absExst s') = cur_domain s
 7. domain_time_internal (absExst s') = domain_time s
 8. ready_queues_internal (absExst s') = ready_queues s
 9. cdt_list_internal (absExst s') = cdt_list s
 10. det_ext.more (absExst s') = det_ext.more (exst s) proof (prove)
using this:
(s, s') \<in> state_relation
einvs s
invs' s'

goal (10 subgoals):
 1. work_units_completed_internal (absExst s') = work_units_completed s
 2. scheduler_action_internal (absExst s') = scheduler_action s
 3. ekheap_internal (absExst s') = ekheap s
 4. domain_list_internal (absExst s') = domain_list s
 5. domain_index_internal (absExst s') = domain_index s
 6. cur_domain_internal (absExst s') = cur_domain s
 7. domain_time_internal (absExst s') = domain_time s
 8. ready_queues_internal (absExst s') = ready_queues s
 9. cdt_list_internal (absExst s') = cdt_list s
 10. det_ext.more (absExst s') = det_ext.more (exst s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> (\<forall>d p. ready_queues s d p = ksReadyQueues s' (d, p)) \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_list s \<and> valid_etcbs s \<and> DetSchedInvs_AI.valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (scheduler_action s) (ksCurThread s') \<and> valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) (ksCurThread s') (ksCurDomain s') \<and> ct_in_cur_domain_2 (ksCurThread s') (ksIdleThread s') (scheduler_action s) (ksCurDomain s') (ekheap s) \<and> valid_blocked_2 (ready_queues s) (kheap s) (scheduler_action s) (ksCurThread s') \<and> valid_idle_etcb s; valid_objs' s' \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> no_0_obj' s' \<and> valid_mdb' s' \<and> sch_act_wf (ksSchedulerAction s') s' \<and> Invariants_H.valid_queues s' \<and> sym_refs (state_refs_of' s') \<and> if_live_then_nonz_cap' s' \<and> if_unsafe_then_cap' s' \<and> valid_idle' s' \<and> valid_global_refs' s' \<and> valid_arch_state' s' \<and> valid_irq_node' (irq_node' s') s' \<and> valid_irq_handlers' s' \<and> valid_irq_states' s' \<and> valid_machine_state' s' \<and> irqs_masked' s' \<and> valid_queues' s' \<and> ct_not_inQ s' \<and> ct_idle_or_in_cur_domain' s' \<and> valid_pde_mappings' s' \<and> pspace_domain_valid s' \<and> ksCurDomain s' \<le> maxDomain \<and> ksDomSchedule s' \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s'). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s' \<and> cur_tcb' s'\<rbrakk> \<Longrightarrow> \<forall>x. absEkheap (ksPSpace s') x = ekheap s x proof (prove)
goal:
No subgoals!