theory ArchArch_IF

lemma as_user_set_register_reads_respects'[Arch_IF_assms]:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag l \<top> (as_user thread (setRegister x y))" apply (case_tac "aag_can_read aag thread \<or> aag_can_affect aag l thread") apply (simp add: as_user_def split_def) apply (rule gen_asm_ev) apply (wp set_object_reads_respects select_f_ev gets_the_ev) apply (auto intro: reads_affects_equiv_get_tcb_eq det_setRegister)[1] apply (simp add: equiv_valid_def2) apply (rule as_user_set_register_ev2[OF domains_distinct]) apply (simp add: labels_are_invisible_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (2 subgoals):
 1. aag_can_read aag thread \<or> aag_can_affect aag l thread \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y))
 2. \<not> (aag_can_read aag thread \<or> aag_can_affect aag l thread) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (2 subgoals):
 1. aag_can_read aag thread \<or> aag_can_affect aag l thread \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
p <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))
od)
 2. \<not> (aag_can_read aag thread \<or> aag_can_affect aag l thread) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aag_can_read aag thread \<or> aag_can_affect aag l thread; True\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
p <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))
od)
 2. \<not> (aag_can_read aag thread \<or> aag_can_affect aag l thread) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag thread \<or> aag_can_affect aag l thread; True; True\<rbrakk> \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb thread s = get_tcb thread t) s \<and> K (det (setRegister x y)) s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (setRegister x y (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). True))
 2. \<not> (aag_can_read aag thread \<or> aag_can_affect aag l thread) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (1 subgoal):
 1. \<not> (aag_can_read aag thread \<or> aag_can_affect aag l thread) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (as_user thread (setRegister x y)) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> labels_are_invisible aag l (pasObjectAbs aag ` {thread, thread}) proof (prove)
goal:
No subgoals!