theory ArchFinalise_IF

lemma set_tcb_queue_reads_respects[Finalise_IF_assms, wp]:
  "reads_respects aag l \<top> (set_tcb_queue d prio queue)" unfolding equiv_valid_def2 equiv_valid_2_def apply (clarsimp simp: set_tcb_queue_def bind_def modify_def put_def get_def) apply (rule conjI) apply (rule reads_equiv_ready_queues_update, assumption) apply (fastforce simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def) apply (rule affects_equiv_ready_queues_update, assumption) apply (clarsimp simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def
                        equiv_asids_def equiv_asid_def) apply (rule ext) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_tcb_queue d prio queue) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue d prio queue s). \<forall>(rvb, t')\<in>fst (set_tcb_queue d prio queue t). rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t') proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t) \<and> affects_equiv aag l (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t)
 2. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> affects_equiv aag l (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_domain aag) id (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p)
 2. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> affects_equiv aag l (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> affects_equiv aag l (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_affect_domain aag l) id (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) proof (prove)
goal (1 subgoal):
 1. \<And>s t x. \<lbrakk>\<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> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr t \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)))); cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); aag_can_affect_label aag l; pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) l \<noteq> {}; \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> kheap s x = kheap t x; \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x; \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x; \<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b)); \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> ekheap s x = ekheap t x; \<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b)); \<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)); \<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_states s x = interrupt_states t x; \<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> ready_queues s x = ready_queues t x; \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> subjectReads (pasPolicy aag) l \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr t \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> (\<lambda>p. if x = d \<and> p = prio then queue else ready_queues s x p) = (\<lambda>p. if x = d \<and> p = prio then queue else ready_queues t x p) proof (prove)
goal (1 subgoal):
 1. \<And>s t x p. \<lbrakk>\<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> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr t \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)))); cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); aag_can_affect_label aag l; pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) l \<noteq> {}; \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> kheap s x = kheap t x; \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state t) x; \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> device_state (machine_state s) x = device_state (machine_state t) x; \<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt t (a, b)); \<forall>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> ekheap s x = ekheap t x; \<forall>a. pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) l \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list t (a, b)); \<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)); \<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_states s x = interrupt_states t x; \<forall>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) l \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> subjectReads (pasPolicy aag) l) \<longrightarrow> ready_queues s x = ready_queues t x; \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> subjectReads (pasPolicy aag) l \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr t \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> (if x = d \<and> p = prio then queue else ready_queues s x p) = (if x = d \<and> p = prio then queue else ready_queues t x p) proof (prove)
goal:
No subgoals!