theory Noninterference

lemma activate_thread_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct pas"
  shows "reads_respects_g pas (l :: 'a subject_label)
           ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) and invs)
           activate_thread" apply (simp add: activate_thread_def) apply (wp set_thread_state_runnable_reads_respects_g as_user_reads_respects_g
            get_thread_state_reads_respects_g gts_wp
         | wpc | simp add: det_setNextPC)+ apply (clarsimp cong: conj_cong) apply (rule conjI) apply (blast intro: requiv_g_cur_thread_eq) apply (frule invs_valid_idle) apply simp apply (rule conjI) apply blast apply (rule impI) apply (clarsimp simp: pred_tcb_at_def obj_at_def valid_idle_def) apply (fastforce simp: det_getRestartPC) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv pas l) pas ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) and invs) activate_thread proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv pas l) pas ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) and invs) (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) \<and> invs s \<Longrightarrow> (\<forall>s t. reads_equiv_g pas s t \<and> affects_equiv pas l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> valid_idle s \<and> (is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC \<and> is_subject pas (cur_thread s) \<and> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> is_subject pas (cur_thread s) \<and> valid_arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_g pas s t \<and> affects_equiv pas l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> valid_idle s \<and> (is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv_g pas s t \<and> affects_equiv pas l s t \<longrightarrow> cur_thread s = cur_thread t
 2. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s \<and> (is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s; valid_idle s\<rbrakk> \<Longrightarrow> (is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s; valid_idle s\<rbrakk> \<Longrightarrow> is_subject pas (cur_thread s) \<or> cur_thread s = idle_thread s
 2. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s; valid_idle s\<rbrakk> \<Longrightarrow> st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s; valid_idle s\<rbrakk> \<Longrightarrow> st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s); invs s; valid_idle s; st_tcb_at ((=) Restart) (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> det getRestartPC proof (prove)
goal (1 subgoal):
 1. \<And>s tcb tcba. \<lbrakk>cur_thread s \<noteq> idle_thread_ptr \<longrightarrow> is_subject pas (cur_thread s); invs s; idle_thread s = idle_thread_ptr; kheap s (cur_thread s) = Some (TCB tcb); kheap s idle_thread_ptr = Some (TCB tcba); Restart = tcb_state tcb; idle (tcb_state tcba); tcb_bound_notification tcba = None; valid_arch_idle (tcb_iarch tcba)\<rbrakk> \<Longrightarrow> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread_ptr \<and> det getRestartPC proof (prove)
goal:
No subgoals!