theory Tcb_R

lemma decodeSetIPCBuffer_is_tc[wp]:
  "\<lbrace>\<top>\<rbrace> decodeSetIPCBuffer args cap slot extras \<lbrace>\<lambda>rv s. isThreadControl rv\<rbrace>,-" apply (simp add: decodeSetIPCBuffer_def Let_def
             split del: if_split cong: list.case_cong prod.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply (simp only: isThreadControl_def tcbinvocation.simps) apply wp+ apply (clarsimp simp: isThreadControl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decodeSetIPCBuffer args cap slot extras \<lbrace>\<lambda>rv s. isThreadControl rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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 (capTCBPtr cap) slot None None None None None (Some (bufferPtr, bufferFrame)))
odE \<lbrace>\<lambda>rv s. isThreadControl rv\<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 (capTCBPtr cap) slot None None None None None (Some (bufferPtr, bufferFrame)))
odE \<lbrace>\<lambda>rv s. isThreadControl rv\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ?P'12 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>?P'72 x21 x22 x21a x22a x1 x2\<rbrace> global.deriveCap x2 x1 \<lbrace>\<lambda>rv s. isThreadControl (tcbinvocation.ThreadControl (capTCBPtr cap) slot None None None None None (Some (x21, Some (rv, x2))))\<rbrace>, -
 2. \<And>s. True \<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> isThreadControl (tcbinvocation.ThreadControl (capTCBPtr cap) slot None None None None None (Some (x, None)))) \<and> (x \<noteq> 0 \<longrightarrow> True \<and> True \<and> ?P'72 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>?P'72 x21 x22 (x1, x2) x22a x1 x2\<rbrace> global.deriveCap x2 x1 \<lbrace>\<lambda>rv s. True\<rbrace>, -
 2. \<And>s. True \<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> isThreadControl (tcbinvocation.ThreadControl (capTCBPtr cap) slot None None None None None (Some (x, None)))) \<and> (x \<noteq> 0 \<longrightarrow> True \<and> True \<and> ?P'72 x xa xb xc xd xe s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<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> isThreadControl (tcbinvocation.ThreadControl (capTCBPtr cap) slot None None None None None (Some (x, None)))) \<and> (x \<noteq> 0 \<longrightarrow> True \<and> True \<and> True)))) proof (prove)
goal:
No subgoals!