theory Ipc_AC

lemma setup_caller_cap_integrity_recv:
  "\<lbrace>integrity aag X st and valid_mdb and st_tcb_at (send_blocked_on ep) sender and
    pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender and
    K (aag_has_auth_to aag Receive ep \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace>
   setup_caller_cap sender receiver grant
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (unfold setup_caller_cap_def) apply (wp cap_insert_integrity_autarch_not_untyped set_thread_state_blocked_on_reply_respects) by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_mdb and st_tcb_at (send_blocked_on ep) sender and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender and K ((pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender) \<Longrightarrow> \<lbrace>integrity aag X st and valid_mdb and st_tcb_at (send_blocked_on ep) sender and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender) \<Longrightarrow> \<lbrace>?Q2\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender); (integrity aag X st and valid_mdb and st_tcb_at (send_blocked_on ep) sender and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender) \<Longrightarrow> \<lbrace>?Q2\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender); (integrity aag X st and valid_mdb and st_tcb_at (send_blocked_on ep) sender and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender); (integrity aag X st and valid_mdb and st_tcb_at (send_blocked_on ep) sender and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender) s\<rbrakk> \<Longrightarrow> (integrity aag X st and st_tcb_at (send_blocked_on ?ep11) sender and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ?ep11 (itcb_state itcb)) sender and K ((pasSubject aag, Receive, pasObjectAbs aag ?ep11) \<in> pasPolicy aag)) s \<and> K (\<not> is_untyped_cap (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) \<and> is_subject aag (fst (receiver, tcb_cnode_index 3))) s