theory Finalise_IF

lemma get_irq_slot_reads_respects:
  "reads_respects aag l (K (is_subject_irq aag irq)) (get_irq_slot irq)" unfolding get_irq_slot_def apply (rule equiv_valid_guard_imp) apply (rule gets_ev) apply (simp add: reads_equiv_def states_equiv_for_def equiv_for_def affects_equiv_def) apply (drule aag_can_read_irq_self) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject_irq aag irq)) (get_irq_slot irq) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject_irq aag irq)) (gets (\<lambda>st. (interrupt_irq_node st irq, []))) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (gets (\<lambda>st. (interrupt_irq_node st irq, [])))
 2. \<And>s. K (is_subject_irq aag irq) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (is_subject_irq aag irq) s \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> (interrupt_irq_node s irq, []) = (interrupt_irq_node t irq, []) proof (prove)
goal (1 subgoal):
 1. is_subject_irq aag irq \<Longrightarrow> \<forall>s t. (aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> kheap s x = kheap t x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b))) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> ekheap s x = ekheap t x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b))) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap t (a, b))) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_states s x = interrupt_states t x) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x) \<and> (\<forall>x. d \<in> pasDomainAbs aag x \<longrightarrow> ready_queues s x = ready_queues t x) \<and> equiv_asids (\<lambda>x. d = pasASIDAbs aag x) s t) \<and> cur_thread s = cur_thread t \<and> cur_domain s = cur_domain t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> equiv_irq_state (machine_state s) (machine_state t) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> kheap s x = kheap t x) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x) \<and> (\<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b))) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> ekheap s x = ekheap t x) \<and> (\<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b))) \<and> (\<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap t (a, b))) \<and> (\<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_states s x = interrupt_states t x) \<and> (\<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x) \<and> (\<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> ready_queues s x = ready_queues t x) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) l) s t \<longrightarrow> interrupt_irq_node s irq = interrupt_irq_node t irq) \<and> (\<not> aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> kheap s x = kheap t x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b))) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> ekheap s x = ekheap t x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b))) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap t (a, b))) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_states s x = interrupt_states t x) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x) \<and> (\<forall>x. d \<in> pasDomainAbs aag x \<longrightarrow> ready_queues s x = ready_queues t x) \<and> equiv_asids (\<lambda>x. d = pasASIDAbs aag x) s t) \<and> cur_thread s = cur_thread t \<and> cur_domain s = cur_domain t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> equiv_irq_state (machine_state s) (machine_state t) \<longrightarrow> interrupt_irq_node s irq = interrupt_irq_node t irq) proof (prove)
goal (1 subgoal):
 1. aag_can_read_irq aag irq \<Longrightarrow> \<forall>s t. (aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> kheap s x = kheap t x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b))) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> ekheap s x = ekheap t x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b))) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap t (a, b))) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_states s x = interrupt_states t x) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x) \<and> (\<forall>x. d \<in> pasDomainAbs aag x \<longrightarrow> ready_queues s x = ready_queues t x) \<and> equiv_asids (\<lambda>x. d = pasASIDAbs aag x) s t) \<and> cur_thread s = cur_thread t \<and> cur_domain s = cur_domain t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> equiv_irq_state (machine_state s) (machine_state t) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> kheap s x = kheap t x) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x) \<and> (\<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b))) \<and> (\<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> ekheap s x = ekheap t x) \<and> (\<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b))) \<and> (\<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap t (a, b))) \<and> (\<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_states s x = interrupt_states t x) \<and> (\<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x) \<and> (\<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> ready_queues s x = ready_queues t x) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) l) s t \<longrightarrow> interrupt_irq_node s irq = interrupt_irq_node t irq) \<and> (\<not> aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> kheap s x = kheap t x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b))) \<and> (\<forall>x. d = pasObjectAbs aag x \<longrightarrow> ekheap s x = ekheap t x) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b))) \<and> (\<forall>a. d = pasObjectAbs aag a \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap t (a, b))) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_states s x = interrupt_states t x) \<and> (\<forall>x. d = pasIRQAbs aag x \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x) \<and> (\<forall>x. d \<in> pasDomainAbs aag x \<longrightarrow> ready_queues s x = ready_queues t x) \<and> equiv_asids (\<lambda>x. d = pasASIDAbs aag x) s t) \<and> cur_thread s = cur_thread t \<and> cur_domain s = cur_domain t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> equiv_irq_state (machine_state s) (machine_state t) \<longrightarrow> interrupt_irq_node s irq = interrupt_irq_node t irq) proof (prove)
goal:
No subgoals!