theory Ipc_AI

lemma setup_caller_cap_objs[wp]:
  "\<lbrace>valid_objs and pspace_aligned and
    st_tcb_at (Not \<circ> halted) sender and
    st_tcb_at active rcvr and
    K (sender \<noteq> rcvr)\<rbrace>
   setup_caller_cap sender rcvr grant
   \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: setup_caller_cap_def) apply (intro conjI impI) apply (rule hoare_pre) apply (wp set_thread_state_valid_cap sts_tcb_cap_valid_cases) apply (subgoal_tac "s \<turnstile> cap.ReplyCap sender False {AllowGrant, AllowWrite}") prefer 2 apply (fastforce simp: valid_cap_def cap_aligned_def word_bits_def
                           st_tcb_def2 tcb_at_def is_tcb
                     dest: pspace_alignedD get_tcb_SomeD) apply (subgoal_tac "tcb_cap_valid (cap.ReplyCap sender False {AllowGrant, AllowWrite})
                                     (rcvr, tcb_cnode_index 3) s") prefer 2 apply (clarsimp simp: tcb_cap_valid_def is_cap_simps
                   split: Structures_A.thread_state.splits
                   elim!: pred_tcb_weakenE) apply (clarsimp simp: valid_tcb_state_def st_tcb_def2) 
(* \<not> grant *)
   apply (rule hoare_pre) apply (wp set_thread_state_valid_cap sts_tcb_cap_valid_cases) apply (subgoal_tac "s \<turnstile> cap.ReplyCap sender False {AllowWrite}") prefer 2 apply (fastforce simp: valid_cap_def cap_aligned_def word_bits_def
                          st_tcb_def2 tcb_at_def is_tcb
                          dest: pspace_alignedD get_tcb_SomeD) apply (subgoal_tac "tcb_cap_valid (cap.ReplyCap sender False {AllowWrite})
                                    (rcvr, tcb_cnode_index 3) s") prefer 2 apply (clarsimp simp: tcb_cap_valid_def is_cap_simps
                  split: Structures_A.thread_state.splits
                  elim!: pred_tcb_weakenE) apply (clarsimp simp: valid_tcb_state_def st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr and K (sender \<noteq> rcvr)\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. sender \<noteq> rcvr \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. sender \<noteq> rcvr \<Longrightarrow> (grant \<longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowGrant, AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>) \<and> (\<not> grant \<longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sender \<noteq> rcvr; grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowGrant, AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sender \<noteq> rcvr; grant\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowGrant, AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> ?Q9 s
 3. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}
 3. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 3. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}; tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s
 3. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}; tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 3. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite}; tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowGrant, AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowGrant, AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowGrant, AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sender \<noteq> rcvr; \<not> grant\<rbrakk> \<Longrightarrow> \<lbrace>?Q62\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> ?Q62 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> s \<turnstile> ReplyCap sender False {AllowWrite} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s\<rbrakk> \<Longrightarrow> s \<turnstile> ReplyCap sender False {AllowWrite}
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}; tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s)
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}\<rbrakk> \<Longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}\<rbrakk> \<Longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s
 2. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}; tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sender \<noteq> rcvr; \<not> grant; (valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and st_tcb_at active rcvr) s; s \<turnstile> ReplyCap sender False {AllowWrite}; tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) s \<and> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> (sender = rcvr \<longrightarrow> (case tcb_cap_cases (tcb_cnode_index 3) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr sender BlockedOnReply (ReplyCap sender False {AllowWrite})) \<and> (tcb_cnode_index 3 = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) rcvr s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap sender False {AllowWrite}) (tcb_ipc_buffer tcb)))) \<and> (sender \<noteq> rcvr \<longrightarrow> tcb_cap_valid (ReplyCap sender False {AllowWrite}) (rcvr, tcb_cnode_index 3) s) proof (prove)
goal:
No subgoals!