theory Tcb_R

lemma decodeTCBConf_wf[wp]:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot
      and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile>' fst x \<and> cte_at' (snd x) s \<and> t \<noteq> snd x \<and> t + 2^cteSizeBits \<noteq> snd x)\<rbrace>
     decodeTCBConfigure args (ThreadCap t) slot extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (clarsimp simp add: decodeTCBConfigure_def Let_def
                 split del: if_split cong: list.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply (rule_tac Q'="\<lambda>setSpace s. tcb_inv_wf' setSpace s \<and> tcb_inv_wf' setIPCParams s
                             \<and> isThreadControl setSpace \<and> isThreadControl setIPCParams
                             \<and> tcThread setSpace = t \<and> tcNewCRoot setSpace \<noteq> None"
                        in hoare_post_imp_R) apply wp apply (clarsimp simp: isThreadControl_def2 cong: option.case_cong) apply wpsimp apply (fastforce simp: isThreadControl_def2 objBits_defs) 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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)\<rbrace> decodeTCBConfigure 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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # x \<Rightarrow> case extras of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] (capability.ThreadCap t) slot [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] (capability.ThreadCap t) slot [cRoot, vRoot];
returnOk (tcbinvocation.ThreadControl t (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'22\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # x \<Rightarrow> case extras of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] (capability.ThreadCap t) slot [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] (capability.ThreadCap t) slot [cRoot, vRoot];
returnOk (tcbinvocation.ThreadControl t (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))
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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s \<Longrightarrow> ?P'22 s proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f\<rbrakk> \<Longrightarrow> \<lbrace>?P'141 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams\<rbrace> decodeSetSpace [x21, x21a, x21b] (capability.ThreadCap t) slot [x21d, x21e] \<lbrace>\<lambda>setSpace. tcb_inv_wf' (tcbinvocation.ThreadControl t (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))\<rbrace>, -
 2. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f\<rbrace> decodeSetIPCBuffer [x21c] (capability.ThreadCap t) slot [x21f] \<lbrace>\<lambda>setIPCParams s. True \<and> ?P'141 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams 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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (xc = [] \<longrightarrow> True) \<and> (\<forall>xd xe. xc = xd # xe \<longrightarrow> (xe = [] \<longrightarrow> True) \<and> (\<forall>xf xg. xe = xf # xg \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xh xi. extras = xh # xi \<longrightarrow> (xi = [] \<longrightarrow> True) \<and> (\<forall>xj xk. xi = xj # xk \<longrightarrow> (xk = [] \<longrightarrow> True) \<and> (\<forall>xl xm. xk = xl # xm \<longrightarrow> ?R131 x xa xb xc xd xe xf xg xh xi xj xk xl xm s))))))) proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f\<rbrakk> \<Longrightarrow> \<lbrace>?P'141 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams\<rbrace> decodeSetSpace [x21, x21a, x21b] (capability.ThreadCap t) slot [x21d, x21e] \<lbrace>\<lambda>setSpace s. tcb_inv_wf' setSpace s \<and> tcb_inv_wf' setIPCParams s \<and> isThreadControl setSpace \<and> isThreadControl setIPCParams \<and> tcThread setSpace = t \<and> tcNewCRoot setSpace \<noteq> None\<rbrace>, -
 2. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams rv s. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f; tcb_inv_wf' rv s \<and> tcb_inv_wf' setIPCParams s \<and> isThreadControl rv \<and> isThreadControl setIPCParams \<and> tcThread rv = t \<and> tcNewCRoot rv \<noteq> None\<rbrakk> \<Longrightarrow> tcb_inv_wf' (tcbinvocation.ThreadControl t (tcThreadCapSlot rv) (tcNewFaultEP rv) None None (tcNewCRoot rv) (tcNewVRoot rv) (tcNewIPCBuffer setIPCParams)) s
 3. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f\<rbrace> decodeSetIPCBuffer [x21c] (capability.ThreadCap t) slot [x21f] \<lbrace>\<lambda>setIPCParams s. True \<and> ?P'141 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (xc = [] \<longrightarrow> True) \<and> (\<forall>xd xe. xc = xd # xe \<longrightarrow> (xe = [] \<longrightarrow> True) \<and> (\<forall>xf xg. xe = xf # xg \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xh xi. extras = xh # xi \<longrightarrow> (xi = [] \<longrightarrow> True) \<and> (\<forall>xj xk. xi = xj # xk \<longrightarrow> (xk = [] \<longrightarrow> True) \<and> (\<forall>xl xm. xk = xl # xm \<longrightarrow> ?R131 x xa xb xc xd xe xf xg xh xi xj xk xl xm s))))))) proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f setIPCParams rv s. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f; tcb_inv_wf' rv s \<and> tcb_inv_wf' setIPCParams s \<and> isThreadControl rv \<and> isThreadControl setIPCParams \<and> tcThread rv = t \<and> tcNewCRoot rv \<noteq> None\<rbrakk> \<Longrightarrow> tcb_inv_wf' (tcbinvocation.ThreadControl t (tcThreadCapSlot rv) (tcNewFaultEP rv) None None (tcNewCRoot rv) (tcNewVRoot rv) (tcNewIPCBuffer setIPCParams)) s
 2. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f\<rbrace> decodeSetIPCBuffer [x21c] (capability.ThreadCap t) slot [x21f] \<lbrace>\<lambda>setIPCParams s. True \<and> (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set [x21d, x21e]. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)) s \<and> tcb_inv_wf' setIPCParams s \<and> True \<and> isThreadControl setIPCParams \<and> capTCBPtr (capability.ThreadCap t) = t \<and> True\<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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (xc = [] \<longrightarrow> True) \<and> (\<forall>xd xe. xc = xd # xe \<longrightarrow> (xe = [] \<longrightarrow> True) \<and> (\<forall>xf xg. xe = xf # xg \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xh xi. extras = xh # xi \<longrightarrow> (xi = [] \<longrightarrow> True) \<and> (\<forall>xj xk. xi = xj # xk \<longrightarrow> (xk = [] \<longrightarrow> True) \<and> (\<forall>xl xm. xk = xl # xm \<longrightarrow> ?R131 x xa xb xc xd xe xf xg xh xi xj xk xl xm s))))))) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f. \<lbrakk>args = x21 # x22; x22 = x21a # x22a; x22a = x21b # x22b; x22b = x21c # x22c; extras = x21d # x22d; x22d = x21e # x22e; x22e = x21f # x22f\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x21 x22 x21a x22a x21b x22b x21c x22c x21d x22d x21e x22e x21f x22f\<rbrace> decodeSetIPCBuffer [x21c] (capability.ThreadCap t) slot [x21f] \<lbrace>\<lambda>setIPCParams s. True \<and> (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set [x21d, x21e]. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)) s \<and> tcb_inv_wf' setIPCParams s \<and> True \<and> isThreadControl setIPCParams \<and> capTCBPtr (capability.ThreadCap t) = t \<and> True\<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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (xc = [] \<longrightarrow> True) \<and> (\<forall>xd xe. xc = xd # xe \<longrightarrow> (xe = [] \<longrightarrow> True) \<and> (\<forall>xf xg. xe = xf # xg \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>xh xi. extras = xh # xi \<longrightarrow> (xi = [] \<longrightarrow> True) \<and> (\<forall>xj xk. xi = xj # xk \<longrightarrow> (xk = [] \<longrightarrow> True) \<and> (\<forall>xl xm. xk = xl # xm \<longrightarrow> ?R131 x xa xb xc xd xe xf xg xh xi xj xk xl xm 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>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>x xb. xa = x # xb \<longrightarrow> (xb = [] \<longrightarrow> True) \<and> (\<forall>x xa. xb = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>x xb. xa = x # xb \<longrightarrow> (extras = [] \<longrightarrow> True) \<and> (\<forall>x xa. extras = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (xc = [] \<longrightarrow> True) \<and> (\<forall>xa xd. xc = xa # xd \<longrightarrow> True \<and> True \<and> (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set [x, xb]. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)) s \<and> (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 [xa]. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s \<and> True \<and> True \<and> capTCBPtr (capability.ThreadCap t) = t \<and> True))))))) proof (prove)
goal:
No subgoals!