theory ArchFinalise_IF

lemma set_bound_notification_none_reads_respects[Finalise_IF_assms]:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag l \<top> (set_bound_notification ref None)" unfolding set_bound_notification_def fun_app_def apply (rule pre_ev(5)[where Q=\<top>]) apply (case_tac "aag_can_read aag ref \<or> aag_can_affect aag l ref") apply (wp set_object_reads_respects gets_the_ev)[1] 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 simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_bound_notification ref None) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := None\<rparr>))
od) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := None\<rparr>))
od)
 2. \<And>s. True \<Longrightarrow> True proof (prove)
goal (3 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_bound_notification := None\<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_bound_notification := None\<rparr>))
od)
 3. \<And>s. True \<Longrightarrow> True proof (prove)
goal (3 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_bound_notification := None\<rparr>))
od)
 3. \<And>s. True \<Longrightarrow> True proof (prove)
goal (2 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_bound_notification := None\<rparr>))
od)
 2. \<And>s. True \<Longrightarrow> True proof (prove)
goal (2 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_bound_notification := None\<rparr>))
od)
 2. \<And>s. True \<Longrightarrow> True proof (prove)
goal (4 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 ?W170 (\<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); ?W170 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q170 rv) (?Q170 rv') (set_object ref (TCB (rv\<lparr>tcb_bound_notification := None\<rparr>))) (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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>?Q170\<rbrace>
 4. \<And>s. True \<Longrightarrow> True proof (prove)
goal (4 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) (=) (?Q170 rv) (?Q170 rv') (set_object ref (TCB (rv\<lparr>tcb_bound_notification := None\<rparr>))) (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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>?Q170\<rbrace>
 4. \<And>s. True \<Longrightarrow> True proof (prove)
goal (3 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) (=) (?Q170 rv) (?Q170 rv') (set_object ref (TCB (rv\<lparr>tcb_bound_notification := None\<rparr>))) (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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>?Q170\<rbrace>
 3. \<And>s. True \<Longrightarrow> True proof (prove)
goal (7 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'182 rv) (set_object ref (TCB (rv\<lparr>tcb_bound_notification := None\<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'182 rv') (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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_bound_notification := None\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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'182 rv\<rbrace>
 7. \<And>s. True \<Longrightarrow> True proof (prove)
goal (5 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'182 rv) (set_object ref (TCB (rv\<lparr>tcb_bound_notification := None\<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'182 rv') (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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_bound_notification := None\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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'182 rv\<rbrace>
 5. \<And>s. True \<Longrightarrow> True 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> modifies_at_most aag {pasObjectAbs aag ref} (\<lambda>s. \<not> typ_at (AArch AASIDPool) ref s \<and> (\<forall>asid_pool. TCB (rv'\<lparr>tcb_bound_notification := None\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool))) (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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_bound_notification := None\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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_bound_notification := None\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool)))\<rbrace>
 4. \<And>s. True \<Longrightarrow> True proof (prove)
goal (3 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_bound_notification := None\<rparr>)) s). \<forall>(rvb, t')\<in>fst (set_object ref (TCB (rv'\<lparr>tcb_bound_notification := None\<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_bound_notification := None\<rparr>) \<noteq> ArchObj (ASIDPool asid_pool)))\<rbrace>
 3. \<And>s. True \<Longrightarrow> True proof (prove)
goal (2 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. \<And>s. True \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> True proof (prove)
goal:
No subgoals!