theory Syscall_AC

lemma handle_reply_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread\<rbrace>
   handle_reply
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding handle_reply_def apply (rule hoare_pre) apply (wp do_reply_transfer_respects get_cap_auth_wp [where aag = aag]| wpc)+ apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
                         cur_tcb_def cte_wp_at_caps_of_state is_reply_cap_to_def
                  intro: aag_Control_into_owns
                   dest: invs_cur) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread\<rbrace> handle_reply \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. (integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> pas_refined aag s \<and> is_subject aag (fst (cur_thread s, tcb_cnode_index 3)) \<and> (\<forall>cap. caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> integrity aag X st s) \<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> (pas_refined aag and integrity aag X st and einvs and tcb_at (cur_thread s) and cte_wp_at (is_reply_cap_to x) (cur_thread s, tcb_cnode_index 3) and K (is_subject aag (cur_thread s)) and K ((pasSubject aag, Reply, pasObjectAbs aag x) \<in> pasPolicy aag) and K (is_subject aag (fst (cur_thread s, tcb_cnode_index 3)) \<and> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x))) 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:
No subgoals!