theory Tcb_R

lemma decodeSetIPC_wf[wp]:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot
        and (\<lambda>s. \<forall>v \<in> set extras. s \<turnstile>' fst v \<and> cte_at' (snd v) s)\<rbrace>
     decodeSetIPCBuffer args (ThreadCap t) slot extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp   add: decodeSetIPCBuffer_def Let_def whenE_def
          split del: if_split cong: list.case_cong prod.case_cong) apply (rule hoare_pre) apply (wp | wpc | simp)+ apply (rule checkValidIPCBuffer_ArchObject_wp) apply simp apply (wp hoare_drop_imps) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)\<rbrace> decodeSetIPCBuffer args (capability.ThreadCap t) slot extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE bufferFrame <- if bufferPtr = 0 then returnOk None else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
y <- checkValidIPCBuffer bufferPtr bufferCap';
returnOk (Some (bufferCap', bufferSlot))
odE;
returnOk (tcbinvocation.ThreadControl t slot None None None None None (Some (bufferPtr, bufferFrame)))
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'12\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE bufferFrame <- if bufferPtr = 0 then returnOk None else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
y <- checkValidIPCBuffer bufferPtr bufferCap';
returnOk (Some (bufferCap', bufferSlot))
odE;
returnOk (tcbinvocation.ThreadControl t slot None None None None None (Some (bufferPtr, bufferFrame)))
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s \<Longrightarrow> ?P'12 s proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x21a x22a x1 x2 bufferCap'. \<lbrakk>args = x21 # x22; extras = (x1, x2) # x22a; x21a = (x1, x2); x21 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'65 x21 x22 (x1, x2) x22a x1 x2 bufferCap'\<rbrace> checkValidIPCBuffer x21 bufferCap' \<lbrace>\<lambda>y a. tcb_at' t a \<and> ex_nonz_cap_to' t a \<and> valid_cap' bufferCap' a \<and> cte_wp_at' (\<lambda>_. True) x2 a \<and> is_aligned x21 msg_align_bits \<and> isArchObjectCap bufferCap' \<and> cte_wp_at' (\<lambda>_. True) slot a\<rbrace>, -
 2. \<And>x21 x22 x21a x22a x1 x2. \<lbrakk>args = x21 # x22; extras = x21a # x22a; x21a = (x1, x2); x21 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R60 x21 x22 x21a x22a x1 x2\<rbrace> global.deriveCap x2 x1 \<lbrace>\<lambda>bufferCap' s. True \<and> ?P'65 x21 x22 x21a x22a x1 x2 bufferCap' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xb xc. extras = xb # xc \<longrightarrow> (\<forall>xd xe. xb = (xd, xe) \<longrightarrow> True \<and> (x = 0 \<longrightarrow> tcb_inv_wf' (tcbinvocation.ThreadControl t slot None None None None None (Some (x, None))) s) \<and> (x \<noteq> 0 \<longrightarrow> ?R60 x xa xb xc xd xe s)))) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x21a x22a x1 x2. \<lbrakk>args = x21 # x22; extras = x21a # x22a; x21a = (x1, x2); x21 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R60 x21 x22 x21a x22a x1 x2\<rbrace> global.deriveCap x2 x1 \<lbrace>\<lambda>bufferCap' s. True \<and> (isArchObjectCap bufferCap' \<and> is_aligned x21 msg_align_bits \<longrightarrow> tcb_at' t s \<and> ex_nonz_cap_to' t s \<and> valid_cap' bufferCap' s \<and> cte_wp_at' (\<lambda>_. True) x2 s \<and> is_aligned x21 msg_align_bits \<and> isArchObjectCap bufferCap' \<and> cte_wp_at' (\<lambda>_. True) slot s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xb xc. extras = xb # xc \<longrightarrow> (\<forall>xd xe. xb = (xd, xe) \<longrightarrow> True \<and> (x = 0 \<longrightarrow> tcb_inv_wf' (tcbinvocation.ThreadControl t slot None None None None None (Some (x, None))) s) \<and> (x \<noteq> 0 \<longrightarrow> ?R60 x xa xb xc xd xe s)))) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x21a x22a x1 x2. \<lbrakk>args = x21 # x22; extras = (x1, x2) # x22a; x21a = (x1, x2); x21 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R60 x21 x22 (x1, x2) x22a x1 x2\<rbrace> global.deriveCap x2 x1 \<lbrace>\<lambda>bufferCap' s. isArchObjectCap bufferCap' \<and> is_aligned x21 msg_align_bits \<longrightarrow> tcb_at' t s \<and> ex_nonz_cap_to' t s \<and> valid_cap' bufferCap' s \<and> cte_wp_at' (\<lambda>_. True) x2 s \<and> cte_wp_at' (\<lambda>_. True) slot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xb xc. extras = xb # xc \<longrightarrow> (\<forall>xd xe. xb = (xd, xe) \<longrightarrow> True \<and> (x = 0 \<longrightarrow> tcb_inv_wf' (tcbinvocation.ThreadControl t slot None None None None None (Some (x, None))) s) \<and> (x \<noteq> 0 \<longrightarrow> ?R60 x xa xb xc xd xe s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xa xb. extras = xa # xb \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> True \<and> (x = 0 \<longrightarrow> tcb_inv_wf' (tcbinvocation.ThreadControl t slot None None None None None (Some (x, None))) s) \<and> (x \<noteq> 0 \<longrightarrow> True \<and> tcb_at' t s \<and> ex_nonz_cap_to' t s \<and> valid_cap' xb s \<and> cte_wp_at' (\<lambda>_. True) xc s \<and> cte_wp_at' (\<lambda>_. True) slot s)))) proof (prove)
goal:
No subgoals!