theory Tcb_AI

lemma (in Tcb_AI) decode_set_ipc_wf[wp]:
  "\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool) and tcb_at t and cte_at slot and ex_cte_cap_to slot
      and ex_nonz_cap_to t
      and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> fst x \<and> cte_at (snd x) s
                          \<and> ex_cte_cap_to (snd x) s
                          \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace>
     decode_set_ipc_buffer args (cap.ThreadCap t) slot excaps
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp   add: decode_set_ipc_buffer_def whenE_def split_def
          split del: if_split) apply (rule hoare_pre, wp check_valid_ipc_buffer_wp) apply simp apply (wp derive_cap_valid_cap hoare_drop_imps)[1] apply wp+ apply (clarsimp simp: neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace> decode_set_ipc_buffer args (ThreadCap t) slot excaps \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace> doE y <- if args = [] then throwError TruncatedMessage else returnOk ();
y <- if excaps = [] then throwError TruncatedMessage else returnOk ();
newbuf <- if data_to_vref (args ! 0) = 0 then returnOk None else doE buffer_cap <- derive_cap (snd (excaps ! 0)) (fst (excaps ! 0));
y <- check_valid_ipc_buffer (data_to_vref (args ! 0)) buffer_cap;
returnOk (Some (buffer_cap, snd (excaps ! 0)))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), newbuf)))
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>y ya. data_to_vref (args ! 0) \<noteq> 0 \<Longrightarrow> \<lbrace>?P'24 y ya\<rbrace> derive_cap (snd (excaps ! 0)) (fst (excaps ! 0)) \<lbrace>\<lambda>rv s. is_arch_cap rv \<and> is_cnode_or_valid_arch rv \<and> valid_ipc_buffer_cap rv (data_to_vref (args ! 0)) \<and> is_aligned (data_to_vref (args ! 0)) msg_align_bits \<longrightarrow> tcb_inv_wf (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), Some (rv, snd (excaps ! 0))))) s\<rbrace>, -
 2. \<And>y. \<lbrace>?B8 y\<rbrace> if excaps = [] then throwError TruncatedMessage else returnOk () \<lbrace>\<lambda>ya s. True \<and> (data_to_vref (args ! 0) = 0 \<longrightarrow> tcb_inv_wf (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), None))) s) \<and> (data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> True \<and> True \<and> ?P'24 y ya s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?P'4\<rbrace> if args = [] then throwError TruncatedMessage else returnOk () \<lbrace>?B8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> ?P'4 s proof (prove)
goal (4 subgoals):
 1. data_to_vref (args ! 0) \<noteq> 0 \<Longrightarrow> \<lbrace>?P'24 () ()\<rbrace> derive_cap (snd (excaps ! 0)) (fst (excaps ! 0)) \<lbrace>\<lambda>rv s. is_arch_cap rv \<and> is_cnode_or_valid_arch rv \<and> valid_ipc_buffer_cap rv (data_to_vref (args ! 0)) \<and> is_aligned (data_to_vref (args ! 0)) msg_align_bits \<longrightarrow> tcb_at t s \<and> s \<turnstile> rv \<and> no_cap_to_obj_dr_emp rv s \<and> cte_wp_at (\<lambda>_. True) (snd (excaps ! 0)) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd (excaps ! 0)) s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> ex_cte_cap_wp_to (\<lambda>_. True) slot s \<and> ex_nonz_cap_to t s\<rbrace>, -
 2. \<And>y. \<lbrace>?B8 y\<rbrace> if excaps = [] then throwError TruncatedMessage else returnOk () \<lbrace>\<lambda>ya s. True \<and> (data_to_vref (args ! 0) = 0 \<longrightarrow> tcb_inv_wf (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), None))) s) \<and> (data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> True \<and> True \<and> ?P'24 y ya s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?P'4\<rbrace> if args = [] then throwError TruncatedMessage else returnOk () \<lbrace>?B8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> ?P'4 s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B8 y\<rbrace> if excaps = [] then throwError TruncatedMessage else returnOk () \<lbrace>\<lambda>ya s. True \<and> (data_to_vref (args ! 0) = 0 \<longrightarrow> tcb_inv_wf (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), None))) s) \<and> (data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> True \<and> True \<and> tcb_at t s \<and> s \<turnstile> fst (excaps ! 0) \<and> no_cap_to_obj_dr_emp (fst (excaps ! 0)) s \<and> cte_wp_at (\<lambda>_. True) (snd (excaps ! 0)) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd (excaps ! 0)) s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> ex_cte_cap_wp_to (\<lambda>_. True) slot s \<and> ex_nonz_cap_to t s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?P'4\<rbrace> if args = [] then throwError TruncatedMessage else returnOk () \<lbrace>?B8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> ?P'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> True \<and> True \<and> True \<and> (excaps = [] \<longrightarrow> True) \<and> (args = [] \<longrightarrow> True) \<and> (args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (data_to_vref (args ! 0) = 0 \<longrightarrow> tcb_inv_wf (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), None))) s) \<and> (data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> True \<and> True \<and> tcb_at t s \<and> s \<turnstile> fst (excaps ! 0) \<and> no_cap_to_obj_dr_emp (fst (excaps ! 0)) s \<and> cte_wp_at (\<lambda>_. True) (snd (excaps ! 0)) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd (excaps ! 0)) s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> ex_cte_cap_wp_to (\<lambda>_. True) slot s \<and> ex_nonz_cap_to t s)) proof (prove)
goal:
No subgoals!