theory Noninterference

lemma kernel_call_A_if_partitionIntegrity:
  "\<lbrakk> ((a, b), x, aa, ba) \<in> kernel_call_A_if e; e \<noteq> Interrupt;
     ct_active b; Invs b; scheduler_action b = resume_cur_thread \<rbrakk>
     \<Longrightarrow> partitionIntegrity (current_aag b) b ba" apply (clarsimp simp: kernel_call_A_if_def) apply (erule use_valid) apply (wp kernel_entry_if_partitionIntegrity) apply (clarsimp simp: partitionIntegrity_refl Invs_def silc_inv_refl) apply (simp add: guarded_pas_domain_def current_aag_def active_from_running schact_is_rct_def) apply (erule impE) apply (rule ct_active_cur_thread_not_idle_thread, simp add: invs_valid_idle) apply simp apply (simp add: the_subject_of_aag_domain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> kernel_call_A_if e; e \<noteq> Interrupt; ct_active b; Invs b; scheduler_action b = resume_cur_thread\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; Invs b; scheduler_action b = resume_cur_thread; ((r, aa), ba) \<in> fst (kernel_entry_if e a b); x = (r = Inl ())\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; Invs b; scheduler_action b = resume_cur_thread; x = (r = Inl ())\<rbrakk> \<Longrightarrow> \<lbrace>?P5 r\<rbrace> kernel_entry_if e a \<lbrace>\<lambda>a. partitionIntegrity (current_aag b) b\<rbrace>
 2. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; Invs b; scheduler_action b = resume_cur_thread; x = (r = Inl ())\<rbrakk> \<Longrightarrow> ?P5 r b proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; Invs b; scheduler_action b = resume_cur_thread; x = (r = Inl ())\<rbrakk> \<Longrightarrow> (silc_inv (current_aag b) b and pas_refined (current_aag b) and einvs and schact_is_rct and is_subject (current_aag b) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (current_aag b)) (?st'9 r) and guarded_pas_domain (current_aag b) and (\<lambda>s. e \<noteq> Interrupt \<and> ct_active s) and (=) b) b proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (current_aag b) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (current_aag b) b; guarded_pas_domain (current_aag b) b; idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b\<rbrakk> \<Longrightarrow> schact_is_rct b \<and> is_subject (current_aag b) (cur_thread b) \<and> domain_sep_inv False (?st'9 r) b proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; cur_thread b \<noteq> idle_thread b \<longrightarrow> pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b)) \<and> domain_sep_inv False (?st'9 r) b proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b\<rbrakk> \<Longrightarrow> cur_thread b \<noteq> idle_thread b
 2. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b)\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b)) \<and> domain_sep_inv False (?st'9 r) b proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b\<rbrakk> \<Longrightarrow> ct_active b
 2. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b)\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b)) \<and> domain_sep_inv False (?st'9 r) b proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>e \<noteq> Interrupt; ct_active b; scheduler_action b = resume_cur_thread; x = (r = Inl ()); invs b; valid_list b; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); only_timer_irq_inv timer_irq s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; domain_sep_inv False s0_internal b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; idle_equiv s0_internal b; valid_domain_list b; valid_vspace_objs_if b; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b)\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b)) \<and> domain_sep_inv False (?st'9 r) b proof (prove)
goal:
No subgoals!