theory ArchArch_IF

lemma as_user_set_register_ev2:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "labels_are_invisible aag l (pasObjectAbs aag ` {thread,thread'})
         \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) \<top> \<top>
                           (as_user thread (setRegister x y)) (as_user thread' (setRegister a b))" apply (simp add: as_user_def) apply (rule equiv_valid_2_guard_imp) apply (rule_tac L="{pasObjectAbs aag thread}" and L'="{pasObjectAbs aag thread'}"
               and Q="\<top>" and Q'="\<top>" in ev2_invisible[OF domains_distinct]) apply (simp add: labels_are_invisible_def)+ apply ((rule modifies_at_mostI | wp set_object_equiv_but_for_labels | simp add: split_def | fastforce dest: get_tcb_not_asid_pool_at)+)[2] apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. labels_are_invisible aag l (pasObjectAbs aag ` {thread, thread'}) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (as_user thread (setRegister x y)) (as_user thread' (setRegister a b)) proof (prove)
goal (1 subgoal):
 1. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) (do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) proof (prove)
goal (3 subgoals):
 1. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ?Q12 ?Q'12 (do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) (do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od)
 2. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> ?Q12 s
 3. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> ?Q'12 s proof (prove)
goal (7 subgoals):
 1. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag thread}
 2. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag thread'}
 3. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od)
 4. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread'} (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od)
 5. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> \<forall>s t. ?P16 s \<and> ?P'16 t \<longrightarrow> (\<forall>(rva, s')\<in>fst ((do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) s). \<forall>(rvb, t')\<in>fst ((do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) t). rva = rvb)
 6. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> (?P16 and (\<lambda>_. True)) s
 7. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> (?P'16 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> 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 \<and> pasObjectAbs aag thread' \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od)
 2. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread'} (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od)
 3. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> \<forall>s t. ?P16 s \<and> ?P'16 t \<longrightarrow> (\<forall>(rva, s')\<in>fst ((do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) s). \<forall>(rvb, t')\<in>fst ((do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) t). rva = rvb)
 4. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> (?P16 and (\<lambda>_. True)) s
 5. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> (?P'16 and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'} \<Longrightarrow> \<forall>s t. ?P16 s \<and> ?P'16 t \<longrightarrow> (\<forall>(rva, s')\<in>fst ((do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (setRegister x y (arch_tcb_context_get (tcb_arch tcb)));
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) s). \<forall>(rvb, t')\<in>fst ((do tcb <- gets_the (get_tcb thread');
(a, uc') <- select_f (setRegister a b (arch_tcb_context_get (tcb_arch tcb)));
set_object thread' (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) t). rva = rvb)
 2. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> (?P16 and (\<lambda>_. True)) s
 3. \<And>s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag thread, pasObjectAbs aag thread'}; True\<rbrakk> \<Longrightarrow> (?P'16 and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!