theory ArchFinalise_IF

lemma set_thread_state_reads_respects[Finalise_IF_assms]:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state ref ts)" unfolding set_thread_state_def fun_app_def apply (simp add: bind_assoc[symmetric]) apply (rule pre_ev) apply (rule_tac P'=\<top> in bind_ev) apply (rule set_thread_state_ext_reads_respects) apply (case_tac "aag_can_read aag ref \<or> aag_can_affect aag l ref") apply (wp set_object_reads_respects gets_the_ev) apply (fastforce simp: get_tcb_def split: option.splits
                     elim: reads_equivE affects_equivE equiv_forE) apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_bind) apply (rule equiv_valid_rv_trivial) apply (wp | simp)+ apply (rule_tac P=\<top> and P'=\<top> and L="{pasObjectAbs aag ref}" and L'="{pasObjectAbs aag ref}"
                  in ev2_invisible[OF domains_distinct]) apply (blast | simp add: labels_are_invisible_def)+ apply (rule set_object_modifies_at_most) apply (rule set_object_modifies_at_most) apply (simp | wp)+ apply (blast dest: get_tcb_not_asid_pool_at) apply (subst thread_set_def[symmetric, simplified fun_app_def]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state ref ts) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
do_extended_op (set_thread_state_ext ref)
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (do y <- do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od;
set_thread_state_ext ref
od) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (do y <- do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od;
set_thread_state_ext ref
od)
 2. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. reads_respects aag l (?Q3 rv) (set_thread_state_ext ref)
 2. reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 3. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>?Q3\<rbrace>
 4. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 2. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 3. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. aag_can_read aag ref \<or> aag_can_affect aag l ref \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 2. \<not> (aag_can_read aag ref \<or> aag_can_affect aag l ref) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 3. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 4. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag ref \<or> aag_can_affect aag l ref; True\<rbrakk> \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb ref s = get_tcb ref t) s \<and> (get_tcb ref s \<noteq> None \<longrightarrow> True)
 2. \<not> (aag_can_read aag ref \<or> aag_can_affect aag l ref) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 3. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 4. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. \<not> (aag_can_read aag ref \<or> aag_can_affect aag l ref) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 2. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 3. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od)
 2. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 3. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W173 (\<lambda>_. True) (gets_the (get_tcb ref))
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l); ?W173 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q173 rv) (?Q173 rv') (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>))) (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)))
 3. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>?Q173\<rbrace>
 4. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 5. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. \<And>P. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>P\<rbrace> gets_the (get_tcb ref) \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q173 rv) (?Q173 rv') (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>))) (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)))
 3. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>?Q173\<rbrace>
 4. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 5. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q173 rv) (?Q173 rv') (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>))) (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)))
 2. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>?Q173\<rbrace>
 3. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 4. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag ref}
 2. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag ref}
 3. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag ref} (?Q'185 rv) (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>)))
 4. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag ref} (?Q'185 rv') (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)))
 5. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)) t). rva = rvb)
 6. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q'185 rv\<rbrace>
 7. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 8. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag ref} (?Q'185 rv) (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>)))
 2. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag ref} (?Q'185 rv') (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)))
 3. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)) t). rva = rvb)
 4. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q'185 rv\<rbrace>
 5. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 6. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag ref} (\<lambda>s. \<not> typ_at (AArch AASIDPool) ref s \<and> (\<forall>asid_pool. TCB (rv'\<lparr>tcb_state := ts\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool))) (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)))
 2. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)) t). rva = rvb)
 3. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> typ_at (AArch AASIDPool) ref s \<and> (\<forall>asid_pool. TCB (rv\<lparr>tcb_state := ts\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool)))\<rbrace>
 4. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 5. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_object ref (TCB (rv\<lparr>tcb_state := ts\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_state := ts\<rparr>)) t). rva = rvb)
 2. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets_the (get_tcb ref) \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> typ_at (AArch AASIDPool) ref s \<and> (\<forall>asid_pool. TCB (rv\<lparr>tcb_state := ts\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool)))\<rbrace>
 3. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 4. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. \<And>s. pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag ref \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> \<not> typ_at (AArch AASIDPool) ref s
 2. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 3. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''3\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>))
od \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 2. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''3\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) ref \<lbrace>\<lambda>rv s. is_subject aag (cur_thread s)\<rbrace>
 2. \<And>s. is_subject aag (cur_thread s) \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal:
No subgoals!