theory Noninterference

lemma cur_thread_update_reads_respects_g':
  "equiv_valid (reads_equiv_g aag)
               (\<lambda>s s'. affects_equiv aag l s s' \<and>
                       arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
               (affects_equiv aag l) \<top> (modify (cur_thread_update (\<lambda>_. t)))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) apply (clarsimp simp: reads_equiv_g_def reads_equiv_def2
                        affects_equiv_def2 globals_equiv_def idle_equiv_def) apply (fastforce intro: states_equiv_for_sym
                    dest: arch_globals_equiv_strengthener_thread_independent) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (affects_equiv aag l) (\<lambda>_. True) (modify (cur_thread_update (\<lambda>_. t))) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (affects_equiv aag l) (=) (\<lambda>_. True) (modify (cur_thread_update (\<lambda>_. t))) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>reads_equiv_g aag s ta; affects_equiv aag l s ta \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state ta); True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv_g aag (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) \<and> affects_equiv aag l (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s ta; 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 ta; arch_globals_equiv_strengthener (machine_state s) (machine_state ta); cur_domain s = cur_domain ta; scheduler_action s = scheduler_action ta; work_units_completed s = work_units_completed ta; equiv_irq_state (machine_state s) (machine_state ta); arch_globals_equiv (cur_thread ta) (idle_thread ta) (kheap s) (kheap ta) (arch_state s) (arch_state ta) (machine_state s) (machine_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; cur_thread s = cur_thread ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta))\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) (s\<lparr>cur_thread := t\<rparr>) ta \<and> arch_globals_equiv t (idle_thread ta) (kheap s) (kheap ta) (arch_state s) (arch_state ta) (machine_state s) (machine_state ta) \<and> 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\<lparr>cur_thread := t\<rparr>) ta proof (prove)
goal:
No subgoals!