theory Noninterference

lemma do_user_op_A_if_partitionIntegrity:
  "((a, b), x, aa, ba) \<in> do_user_op_A_if uop \<Longrightarrow> ct_running b \<Longrightarrow> Invs b
   \<Longrightarrow> partitionIntegrity (current_aag b) b ba" apply (simp add: do_user_op_A_if_def) apply (erule use_valid) apply (wp do_user_op_if_partitionIntegrity) apply (simp add: partitionIntegrity_refl) apply (simp add: Invs_def) apply (clarsimp simp: guarded_pas_domain_def current_aag_def) apply (erule impE) apply (erule ct_running_not_idle) apply (simp add: invs_valid_idle) 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> do_user_op_A_if uop; ct_running b; Invs b\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((x, aa), ba) \<in> fst (do_user_op_if uop a b); ct_running b; Invs b\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ct_running b; Invs b\<rbrakk> \<Longrightarrow> \<lbrace>?P\<rbrace> do_user_op_if uop a \<lbrace>\<lambda>a. partitionIntegrity (current_aag b) b\<rbrace>
 2. \<lbrakk>ct_running b; Invs b\<rbrakk> \<Longrightarrow> ?P b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_running b; Invs b\<rbrakk> \<Longrightarrow> (partitionIntegrity (current_aag b) b and pas_refined (current_aag b) and invs and is_subject (current_aag b) \<circ> cur_thread) b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_running b; Invs b\<rbrakk> \<Longrightarrow> pas_refined (current_aag b) b \<and> invs b \<and> is_subject (current_aag b) (cur_thread b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_running b; invs b \<and> valid_list b \<and> valid_sched b \<and> only_timer_irq_inv timer_irq s0_internal b \<and> silc_inv (current_aag b) s0_internal b \<and> domain_sep_inv False s0_internal b \<and> pas_refined (current_aag b) b \<and> guarded_pas_domain (current_aag b) b \<and> idle_equiv s0_internal b \<and> valid_domain_list b \<and> valid_vspace_objs_if b\<rbrakk> \<Longrightarrow> is_subject (current_aag b) (cur_thread b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_running b; invs b; valid_list b; valid_sched 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)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ct_running b; invs b; valid_list b; valid_sched 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. \<lbrakk>ct_running b; invs b; valid_list b; valid_sched 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)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs b; valid_list b; valid_sched 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> valid_idle b
 2. \<lbrakk>ct_running b; invs b; valid_list b; valid_sched 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)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_running b; invs b; valid_list b; valid_sched 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)) proof (prove)
goal:
No subgoals!