theory Ipc_AI

lemma setup_caller_cap_reply[wp]:
  "\<lbrace>valid_reply_caps and pspace_aligned and
    st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt\<rbrace>
   setup_caller_cap st rt grant
   \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace>" unfolding setup_caller_cap_def apply wp apply (rule_tac Q="\<lambda>rv s. pspace_aligned s \<and> tcb_at st s \<and>
         st_tcb_at (\<lambda>ts. ts = Structures_A.thread_state.BlockedOnReply) st s \<and>
         \<not> has_reply_cap st s"
                 in hoare_post_imp) apply (fastforce simp: valid_cap_def cap_aligned_def
                           tcb_at_def pspace_aligned_def word_bits_def
                    dest!: get_tcb_SomeD
                    elim!: my_BallE [where y=st] pred_tcb_weakenE) apply (wp sts_st_tcb_at has_reply_cap_cte_lift) apply (strengthen reply_cap_doesnt_exist_strg) apply (clarsimp simp: st_tcb_at_tcb_at)+ apply (clarsimp intro!: tcb_at_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt\<rbrace> do set_thread_state st BlockedOnReply;
cap_insert (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> set_thread_state st BlockedOnReply \<lbrace>\<lambda>rv s. \<forall>t R. ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}) = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s\<rbrace>
 2. \<And>s. (valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt) s \<Longrightarrow> (valid_reply_caps s \<and> (BlockedOnReply \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap st s)) \<and> cte_wp_at (\<lambda>_. True) (rt, tcb_cnode_index 3) s \<and> ?P'8 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. pspace_aligned s \<and> tcb_at st s \<and> st_tcb_at awaiting_reply st s \<and> \<not> has_reply_cap st s \<Longrightarrow> \<forall>t R. ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}) = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<lbrace>?P'8\<rbrace> set_thread_state st BlockedOnReply \<lbrace>\<lambda>rv s. pspace_aligned s \<and> tcb_at st s \<and> st_tcb_at awaiting_reply st s \<and> \<not> has_reply_cap st s\<rbrace>
 3. \<And>s. (valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt) s \<Longrightarrow> (valid_reply_caps s \<and> (BlockedOnReply \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap st s)) \<and> cte_wp_at (\<lambda>_. True) (rt, tcb_cnode_index 3) s \<and> ?P'8 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> set_thread_state st BlockedOnReply \<lbrace>\<lambda>rv s. pspace_aligned s \<and> tcb_at st s \<and> st_tcb_at awaiting_reply st s \<and> \<not> has_reply_cap st s\<rbrace>
 2. \<And>s. (valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt) s \<Longrightarrow> (valid_reply_caps s \<and> (BlockedOnReply \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap st s)) \<and> cte_wp_at (\<lambda>_. True) (rt, tcb_cnode_index 3) s \<and> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt) s \<Longrightarrow> (valid_reply_caps s \<and> (BlockedOnReply \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap st s)) \<and> cte_wp_at (\<lambda>_. True) (rt, tcb_cnode_index 3) s \<and> pspace_aligned s \<and> tcb_at st s \<and> True \<and> \<not> has_reply_cap st s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_reply_caps and pspace_aligned and st_tcb_at (Not \<circ> awaiting_reply) st and tcb_at rt) s \<Longrightarrow> (valid_reply_caps s \<and> (BlockedOnReply \<noteq> BlockedOnReply \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) st s)) \<and> cte_wp_at (\<lambda>_. True) (rt, tcb_cnode_index 3) s \<and> pspace_aligned s \<and> tcb_at st s \<and> True \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) st s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_reply_caps s; pspace_aligned s; st_tcb_at (Not \<circ> awaiting_reply) st s; tcb_at rt s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (rt, tcb_cnode_index 3) s proof (prove)
goal:
No subgoals!