theory ArchFinalise_IF

lemma thread_set_reads_respects[Finalise_IF_assms]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l \<top> (thread_set x y)" unfolding thread_set_def fun_app_def apply (case_tac "aag_can_read aag y \<or> aag_can_affect aag l y") apply (wp set_object_reads_respects) apply (clarsimp, rule reads_affects_equiv_get_tcb_eq, simp+)[1] apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_guard_imp) apply (rule_tac L="{pasObjectAbs aag y}" and L'="{pasObjectAbs aag y}"
                in ev2_invisible[OF domains_distinct]) apply (assumption | simp add: labels_are_invisible_def)+ apply (rule modifies_at_mostI[where P="\<top>"]
            | wp set_object_equiv_but_for_labels
            | simp
            | (clarify, drule get_tcb_not_asid_pool_at))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (thread_set x y) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read aag y \<or> aag_can_affect aag l y \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od)
 2. \<not> (aag_can_read aag y \<or> aag_can_affect aag l y) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag y \<or> aag_can_affect aag l y; True\<rbrakk> \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb y s = get_tcb y t) s \<and> (get_tcb y s \<noteq> None \<longrightarrow> True)
 2. \<not> (aag_can_read aag y \<or> aag_can_affect aag l y) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) proof (prove)
goal (1 subgoal):
 1. \<not> (aag_can_read aag y \<or> aag_can_affect aag l y) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ?P17 (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od)
 2. \<And>s. \<lbrakk>pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> ?P17 s proof (prove)
goal (6 subgoals):
 1. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag y}
 2. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag y}
 3. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag y} ?Q20 (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od)
 4. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag y} ?Q20 (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od)
 5. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<forall>s t. ?P20 s \<and> ?P20 t \<longrightarrow> (\<forall>(rva, s')\<in>fst ((do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) s). \<forall>(rvb, t')\<in>fst ((do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) t). rva = rvb)
 6. \<And>s. \<lbrakk>pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> (?P20 and ?Q20) s proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag y} ?Q20 (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od)
 2. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag y} ?Q20 (do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od)
 3. pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<forall>s t. ?P20 s \<and> ?P20 t \<longrightarrow> (\<forall>(rva, s')\<in>fst ((do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) s). \<forall>(rvb, t')\<in>fst ((do tcb <- gets_the (get_tcb y);
set_object y (TCB (x tcb))
od) t). rva = rvb)
 4. \<And>s. \<lbrakk>pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag y \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> (?P20 and ?Q20) s proof (prove)
goal:
No subgoals!