theory Ipc_IF

lemma handle_reply_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag
                                             and is_subject aag \<circ> cur_thread) handle_reply" unfolding handle_reply_def apply (wp do_reply_transfer_reads_respects_f hoare_vcg_all_lift
            get_cap_wp reads_respects_f[OF get_cap_reads_respects, where Q="\<top>" and st=st]
         | wpc | blast)+ apply (rule conjI) apply (fastforce simp: reads_equiv_f_def) apply clarsimp apply (rule conjI) apply assumption apply (rule conjI) apply (drule cte_wp_valid_cap) apply (erule invs_valid_objs) apply (simp add: valid_cap_simps) apply (rule conjI, fastforce simp: tcb_at_invs) apply (rule conjI) apply (erule emptyable_cte_wp_atD) apply (erule invs_valid_objs) apply (simp add: is_master_reply_cap_def) apply (frule_tac p="(cur_thread s, tcb_cnode_index 3)" in cap_cur_auth_caps_of_state[rotated]) apply simp apply (simp add: cte_wp_at_caps_of_state) apply (fastforce intro: read_reply_thread_read_thread_rev
                    simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
                    dest: aag_Control_into_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) handle_reply proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> (silc_inv aag st and K (aag_can_read_or_affect aag l (fst (cur_thread s, tcb_cnode_index 3))) and (\<lambda>_. True)) s \<and> (\<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (silc_inv aag (?st98 (cur_thread s) cap x xa xb) and invs and pas_refined aag and pas_cur_domain aag and tcb_at x and tcb_at (cur_thread s) and emptyable (cur_thread s, tcb_cnode_index 3) and is_subject aag \<circ> cur_thread and K (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) and K (is_subject aag (cur_thread s) \<and> aag_can_read aag x \<and> is_subject aag (fst (cur_thread s, tcb_cnode_index 3)))) s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> \<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag st and K (aag_can_read_or_affect aag l (fst (cur_thread s, tcb_cnode_index 3))) and (\<lambda>_. True)) s \<and> (\<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (silc_inv aag (?st98 (cur_thread s) cap x xa xb) and invs and pas_refined aag and pas_cur_domain aag and tcb_at x and tcb_at (cur_thread s) and emptyable (cur_thread s, tcb_cnode_index 3) and is_subject aag \<circ> cur_thread and K (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) and K (is_subject aag (cur_thread s) \<and> aag_can_read aag x \<and> is_subject aag (fst (cur_thread s, tcb_cnode_index 3)))) s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag st and K (aag_can_read_or_affect aag l (fst (cur_thread s, tcb_cnode_index 3))) and (\<lambda>_. True)) s \<and> (\<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (silc_inv aag (?st98 (cur_thread s) cap x xa xb) and invs and pas_refined aag and pas_cur_domain aag and tcb_at x and tcb_at (cur_thread s) and emptyable (cur_thread s, tcb_cnode_index 3) and is_subject aag \<circ> cur_thread and K (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) and K (is_subject aag (cur_thread s) \<and> aag_can_read aag x \<and> is_subject aag (fst (cur_thread s, tcb_cnode_index 3)))) s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> silc_inv aag (?st98 (cur_thread s) (ReplyCap x False xb) x False xb) s \<and> tcb_at x s \<and> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> silc_inv aag (?st98 (cur_thread s) (ReplyCap x False xb) x False xb) s
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at x s \<and> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at x s \<and> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at x s
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); \<not> xa\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); \<not> xa; s \<turnstile> ReplyCap x False xb\<rbrakk> \<Longrightarrow> tcb_at x s
 3. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); \<not> xa; s \<turnstile> ReplyCap x False xb\<rbrakk> \<Longrightarrow> tcb_at x s
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s \<and> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> emptyable (cur_thread s, tcb_cnode_index 3) s \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> emptyable (cur_thread s, tcb_cnode_index 3) s
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); \<not> xa\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); \<not> xa\<rbrakk> \<Longrightarrow> \<forall>cap. ReplyCap x False xb = cap \<longrightarrow> \<not> is_master_reply_cap cap
 3. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); \<not> xa\<rbrakk> \<Longrightarrow> \<forall>cap. ReplyCap x False xb = cap \<longrightarrow> \<not> is_master_reply_cap cap
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> is_subject aag (fst (cur_thread s, tcb_cnode_index 3))
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some (?cap191 s x xa xb)
 3. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa; pas_cap_cur_auth aag (?cap191 s x xa xb)\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some (?cap191 s x xa xb)
 2. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa; pas_cap_cur_auth aag (?cap191 s x xa xb)\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa; pas_cap_cur_auth aag (ReplyCap x xa xb)\<rbrakk> \<Longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> aag_can_read aag x proof (prove)
goal:
No subgoals!