theory Noninterference

lemma switch_to_thread_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_g aag (l :: 'a subject_label)
                          (pas_refined aag and (\<lambda>s. is_subject aag t)) (switch_to_thread t)" apply (simp add: switch_to_thread_def) apply (subst bind_assoc[symmetric]) apply (rule equiv_valid_guard_imp) apply (rule bind_ev) apply (wp bind_ev_general cur_thread_update_reads_respects_g'
               tcb_sched_action_reads_respects_g' arch_switch_to_thread_reads_respects_g') apply (simp add: equiv_valid_def2) apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (rule assert_ev2 | simp)+ apply (rule equiv_valid_rv_trivial, wp+) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and (\<lambda>s. is_subject aag t)) (switch_to_thread t) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and (\<lambda>s. is_subject aag t)) (do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and (\<lambda>s. is_subject aag t)) (do y <- do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od;
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (do y <- do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od;
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od)
 2. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q3 rv) (do y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od)
 2. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'3 (do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od)
 3. \<lbrace>?P''3\<rbrace> do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od \<lbrace>?Q3\<rbrace>
 4. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'3 (do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od)
 2. \<lbrace>?P''3\<rbrace> do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od \<lbrace>\<lambda>rv s. is_subject aag t \<and> pas_refined aag s \<and> True\<rbrace>
 3. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (=) ?P'3 (do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od)
 2. \<lbrace>?P''3\<rbrace> do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od \<lbrace>\<lambda>rv s. is_subject aag t \<and> pas_refined aag s \<and> True\<rbrace>
 3. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q20 rv) (?Q'20 rv') (assert (\<exists>y. get_tcb t rv = Some y)) (assert (\<exists>y. get_tcb t rv' = Some y))
 2. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>_ _. True) ?P20 get
 3. \<lbrace>?S20\<rbrace> get \<lbrace>?Q20\<rbrace>
 4. \<lbrace>?S20\<rbrace> get \<lbrace>?Q'20\<rbrace>
 5. \<lbrace>?P''3\<rbrace> do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od \<lbrace>\<lambda>rv s. is_subject aag t \<and> pas_refined aag s \<and> True\<rbrace>
 6. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> (?P20 s \<and> ?S20 s) \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>_ _. True) ?P20 get
 2. \<lbrace>?S20\<rbrace> get \<lbrace>?Q20\<rbrace>
 3. \<lbrace>?S20\<rbrace> get \<lbrace>?Q'20\<rbrace>
 4. \<lbrace>?P''3\<rbrace> do state <- get;
assert (\<exists>y. get_tcb t state = Some y)
od \<lbrace>\<lambda>rv s. is_subject aag t \<and> pas_refined aag s \<and> True\<rbrace>
 5. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> (?P20 s \<and> ?S20 s) \<and> ?P''3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> (True \<and> True) \<and> ((\<exists>y. get_tcb t s = Some y) \<longrightarrow> is_subject aag t \<and> pas_refined aag s \<and> True) proof (prove)
goal:
No subgoals!