theory Ipc_AI

lemma setup_caller_cap_mdb[wp]:
  "\<And>sender.
    \<lbrace>valid_mdb and valid_objs and pspace_aligned and
          st_tcb_at (Not \<circ> halted) sender and
          K (sender \<noteq> rcvr)\<rbrace>
      setup_caller_cap sender rcvr grant
    \<lbrace>\<lambda>_. valid_mdb :: 'state_ext state \<Rightarrow> bool\<rbrace>" unfolding setup_caller_cap_def apply (rule hoare_pre) apply (wp set_thread_state_valid_cap set_thread_state_cte_wp_at | simp)+ apply (clarsimp simp: valid_cap_def cap_aligned_def word_bits_def
                        st_tcb_def2 tcb_at_def is_tcb
                        st_tcb_at_reply_cap_valid) apply (frule(1) valid_tcb_objs) apply (clarsimp dest!:pspace_alignedD get_tcb_SomeD) apply (clarsimp simp:valid_tcb_def) apply (clarsimp simp:valid_tcb_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sender. \<lbrace>valid_mdb and valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and K (sender \<noteq> rcvr)\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sender. \<lbrace>valid_mdb and valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and K (sender \<noteq> rcvr)\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sender. \<lbrace>?Q sender\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. valid_mdb\<rbrace>
 2. \<And>sender s. (valid_mdb and valid_objs and pspace_aligned and st_tcb_at (Not \<circ> halted) sender and K (sender \<noteq> rcvr)) s \<Longrightarrow> ?Q sender s proof (prove)
goal (1 subgoal):
 1. \<And>sender s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> st_tcb_at (Not \<circ> halted) sender s \<and> sender \<noteq> rcvr \<Longrightarrow> (grant \<longrightarrow> s \<turnstile> ReplyCap sender False {AllowGrant, AllowWrite} \<and> valid_tcb_state BlockedOnReply s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s) \<and> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s) \<and> (\<not> grant \<longrightarrow> s \<turnstile> ReplyCap sender False {AllowWrite} \<and> valid_tcb_state BlockedOnReply s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s) \<and> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s) proof (prove)
goal (1 subgoal):
 1. \<And>sender s tcb. \<lbrakk>valid_mdb s; valid_objs s; pspace_aligned s; sender \<noteq> rcvr; get_tcb sender s = Some tcb; \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> is_aligned sender 9 \<and> valid_tcb_state BlockedOnReply s proof (prove)
goal (1 subgoal):
 1. \<And>sender s tcb. \<lbrakk>valid_mdb s; valid_objs s; pspace_aligned s; sender \<noteq> rcvr; get_tcb sender s = Some tcb; \<not> halted (tcb_state tcb); valid_tcb sender tcb s\<rbrakk> \<Longrightarrow> is_aligned sender 9 \<and> valid_tcb_state BlockedOnReply s proof (prove)
goal (1 subgoal):
 1. \<And>sender s tcb. \<lbrakk>valid_mdb s; valid_objs s; pspace_aligned s; sender \<noteq> rcvr; \<not> halted (tcb_state tcb); valid_tcb sender tcb s; is_aligned sender 9\<rbrakk> \<Longrightarrow> valid_tcb_state BlockedOnReply s proof (prove)
goal (1 subgoal):
 1. \<And>sender s tcb. \<lbrakk>valid_mdb s; valid_objs s; pspace_aligned s; sender \<noteq> rcvr; \<not> halted (tcb_state tcb); is_aligned sender 9; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr sender (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> valid_tcb_state BlockedOnReply s proof (prove)
goal:
No subgoals!