theory Arch_IF

lemma equiv_but_for_affects_equiv:
  "\<lbrakk> pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s' \<rbrakk>
     \<Longrightarrow> affects_equiv aag l s s'" apply (subst affects_equiv_def2) apply (clarsimp simp: labels_are_invisible_def equiv_but_for_labels_def aag_can_affect_label_def) apply (rule states_equiv_forI) apply (fastforce intro!: equiv_forI elim!: states_equiv_forE equiv_forD)+ apply (fastforce simp: equiv_asids_def elim!: states_equiv_forE elim!: equiv_forD) apply (clarsimp simp: equiv_for_def states_equiv_for_def disjoint_iff_not_equal) apply (metis pas_domains_distinct_inj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> affects_equiv aag l s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l) (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) l) (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) l \<noteq> {}) s s' proof (prove)
goal (10 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) kheap s s'
 2. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) (machine_state s) (machine_state s')
 3. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) \<circ> fst) cdt s s'
 4. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) ekheap s s'
 5. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) \<circ> fst) cdt_list s s'
 6. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l) \<circ> fst) is_original_cap s s'
 7. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l) interrupt_states s s'
 8. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l) interrupt_irq_node s s'
 9. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) l) s s'
 10. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) l \<noteq> {}) ready_queues s s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) l) s s'
 2. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) l \<noteq> {}) ready_queues s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<and> pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) l \<noteq> {}) ready_queues s s' proof (prove)
goal (1 subgoal):
 1. \<And>x xa d. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (\<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> kheap s x = kheap s' x; \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x; \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> device_state (machine_state s) x = device_state (machine_state s') x; \<forall>a. pasObjectAbs aag a \<notin> L \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt s' (a, b)); \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> ekheap s x = ekheap s' x; \<forall>a. pasObjectAbs aag a \<notin> L \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list s' (a, b)); \<forall>a. pasObjectAbs aag a \<notin> L \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap s' (a, b)); \<forall>x. pasIRQAbs aag x \<notin> L \<longrightarrow> interrupt_states s x = interrupt_states s' x; \<forall>x. pasIRQAbs aag x \<notin> L \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x; \<forall>x. (\<forall>l\<in>pasDomainAbs aag x. l \<notin> L) \<longrightarrow> ready_queues s x = ready_queues s' x; equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) s s'; xa \<in> pasDomainAbs aag x; xa \<in> subjectReads (pasPolicy aag) l; subject_can_affect_label_directly aag d; d \<in> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> ready_queues s x = ready_queues s' x proof (prove)
goal:
No subgoals!