theory Tcb_R

lemma decodeTCBConfigure_corres:
  notes if_cong [cong] option.case_cong [cong]
  shows
 "\<lbrakk> cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
     is_thread_cap cap \<rbrakk> \<Longrightarrow>
  corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x \<in> set extras. cte_at (snd x) s))
                                 (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x \<in> set extras'. cte_at' (snd x) s))
      (decode_tcb_configure args cap slot extras)
      (decodeTCBConfigure args cap' (cte_map slot) extras')" apply (clarsimp simp add: decode_tcb_configure_def decodeTCBConfigure_def) apply (cases "length args < 4") apply (clarsimp split: list.split) apply (cases "length extras < 3") apply (clarsimp split: list.split simp: list_all2_Cons2) apply (clarsimp simp: linorder_not_less val_le_length_Cons list_all2_Cons1
      priorityBits_def) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule decodeSetIPCBuffer_corres; simp) apply (rule corres_splitEE) apply (rule decodeSetSpace_corres; simp) apply (rule_tac F="tcb_invocation.is_ThreadControl set_params" in corres_gen_asm) apply (rule_tac F="tcb_invocation.is_ThreadControl set_space" in corres_gen_asm) apply (rule_tac F="tcThreadCapSlot setSpace = cte_map slot" in corres_gen_asm2) apply (rule corres_trivial) apply (clarsimp simp: tcb_invocation.is_ThreadControl_def returnOk_def is_cap_simps) apply (wp | simp add: invs_def valid_sched_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_configure args cap slot extras) (decodeTCBConfigure args cap' (cte_map slot) extras') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap; length args < 4\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE)
 2. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap; \<not> length args < 4\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap; \<not> length args < 4\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap; \<not> length args < 4; length extras < 3\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE)
 2. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap; \<not> length args < 4; \<not> length extras < 3\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; is_thread_cap cap; \<not> length args < 4; \<not> length extras < 3\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (length args < 4) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (length extras < 3) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
set_params <- decode_set_ipc_buffer [args ! 3] cap slot [extras ! 2];
set_space <- decode_set_space [args ! 0, args ! Suc 0, args ! 2] cap slot (take 2 extras);
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [faultEP, cRootData, vRootData] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | faultEP # cRootData # vRootData # buffer # xa \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [cRoot, vRoot] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | cRoot # vRoot # bufferFrame # xaa \<Rightarrow> doE setIPCParams <- decodeSetIPCBuffer [buffer] cap' (cte_map slot) [bufferFrame];
setSpace <- decodeSetSpace [faultEP, cRootData, vRootData] cap' (cte_map slot) [cRoot, vRoot];
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) Nothing Nothing (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) (doE set_params <- decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)];
set_space <- decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)];
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (doE setIPCParams <- decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))];
setSpace <- decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))];
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))
odE) proof (prove)
goal (3 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?Q351 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) (?Q'351 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) (doE set_params <- decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)];
set_space <- decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)];
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (doE setIPCParams <- decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))];
setSpace <- decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))];
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))
odE)
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q351 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q'351 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s proof (prove)
goal (6 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) (?P355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) (?P'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) (decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)]) (decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))])
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; ?r'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params) (?R'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams) (doE set_space <- decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)];
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (doE setSpace <- decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))];
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))
odE)
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>?R355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>?R'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> (?P355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> (?P'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (5 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params) (?R'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams) (doE set_space <- decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)];
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE) (doE setSpace <- decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))];
returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams))
odE)
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>?R355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>?R'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (8 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams) (?P373 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params) (?P'375 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams) (decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)]) (decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))])
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams; ?r'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space) (?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams setSpace) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)))
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>?R372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. ?P373 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. ?P'375 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 8. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams; tcbinv_relation set_space setSpace\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space) (?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams setSpace) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)))
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>?R372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set [(a, aa, b), (ab, ac, ba)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))]. cte_wp_at' (\<lambda>_. True) (snd x) s) and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 7. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams; tcbinv_relation set_space setSpace; tcb_invocation.is_ThreadControl set_params\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?P398 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space) (?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams setSpace) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)))
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>\<lambda>set_space. ?P398 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space and (\<lambda>s. tcb_invocation.is_ThreadControl set_params)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set [(a, aa, b), (ab, ac, ba)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))]. cte_wp_at' (\<lambda>_. True) (snd x) s) and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 7. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams; tcbinv_relation set_space setSpace; tcb_invocation.is_ThreadControl set_params; tcb_invocation.is_ThreadControl set_space\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?P400 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space) (?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams setSpace) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)))
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>\<lambda>set_space. ?P400 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space and (\<lambda>s. tcb_invocation.is_ThreadControl set_space) and (\<lambda>s. tcb_invocation.is_ThreadControl set_params)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>?R'372 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set [(a, aa, b), (ab, ac, ba)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))]. cte_wp_at' (\<lambda>_. True) (snd x) s) and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 7. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams; tcbinv_relation set_space setSpace; tcb_invocation.is_ThreadControl set_params; tcb_invocation.is_ThreadControl set_space; tcThreadCapSlot setSpace = cte_map slot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?P400 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space) (?P'402 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams setSpace) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)))
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>\<lambda>set_space. ?P400 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space and (\<lambda>s. tcb_invocation.is_ThreadControl set_space) and (\<lambda>s. tcb_invocation.is_ThreadControl set_params)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>\<lambda>setSpace. ?P'402 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams setSpace and (\<lambda>s. tcThreadCapSlot setSpace = cte_map slot)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set [(a, aa, b), (ab, ac, ba)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))]. cte_wp_at' (\<lambda>_. True) (snd x) s) and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 7. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (7 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams set_space setSpace. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams; tcbinv_relation set_space setSpace; tcb_invocation.is_ThreadControl set_params; tcb_invocation.is_ThreadControl set_space; tcThreadCapSlot setSpace = cte_map slot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))) (returnOk (tcbinvocation.ThreadControl (capTCBPtr cap') (tcThreadCapSlot setSpace) (tcNewFaultEP setSpace) None None (tcNewCRoot setSpace) (tcNewVRoot setSpace) (tcNewIPCBuffer setIPCParams)))
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>\<lambda>set_space. (\<lambda>_. True) and (\<lambda>s. tcb_invocation.is_ThreadControl set_space) and (\<lambda>s. tcb_invocation.is_ThreadControl set_params)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>\<lambda>setSpace. (\<lambda>_. True) and (\<lambda>s. tcThreadCapSlot setSpace = cte_map slot)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set [(a, aa, b), (ab, ac, ba)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))]. cte_wp_at' (\<lambda>_. True) (snd x) s) and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 7. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal (6 subgoals):
 1. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace> decode_set_space [y, ya, yb] cap slot [(a, aa, b), (ab, ac, ba)] \<lbrace>\<lambda>set_space. (\<lambda>_. True) and (\<lambda>s. tcb_invocation.is_ThreadControl set_space) and (\<lambda>s. tcb_invocation.is_ThreadControl set_params)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params setIPCParams. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; tcbinv_relation set_params setIPCParams\<rbrakk> \<Longrightarrow> \<lbrace>?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace> decodeSetSpace [y, ya, yb] cap' (cte_map slot) [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))] \<lbrace>\<lambda>setSpace. (\<lambda>_. True) and (\<lambda>s. tcThreadCapSlot setSpace = cte_map slot)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decode_set_ipc_buffer [yc] cap slot [(ad, ae, bb)] \<lbrace>\<lambda>set_params. invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set [(a, aa, b), (ab, ac, ba)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q374 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb set_params\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb\<rbrace> decodeSetIPCBuffer [yc] cap' (cte_map slot) [(ah, cte_map (ae, bb))] \<lbrace>\<lambda>setIPCParams. invs' and valid_cap' cap' and (\<lambda>s. \<forall>x\<in>set [(af, cte_map (aa, b)), (ag, cte_map (ac, ba))]. cte_wp_at' (\<lambda>_. True) (snd x) s) and ?Q'376 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb setIPCParams\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (einvs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>_. True) (aa, b) s \<and> cte_wp_at (\<lambda>_. True) (ac, ba) s \<and> cte_wp_at (\<lambda>_. True) (ae, bb) s \<and> (\<forall>x\<in>set yse. cte_wp_at (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>set [(ad, ae, bb)]. cte_wp_at (\<lambda>_. True) (snd x) s) and ?Q355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s
 6. \<And>y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb s. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; args = y # ya # yb # yc # ysf; extras = (a, aa, b) # (ab, ac, ba) # (ad, ae, bb) # yse; extras' = (af, cte_map (aa, b)) # (ag, cte_map (ac, ba)) # (ah, cte_map (ae, bb)) # zsb; cap_relation a af; cap_relation ab ag; cap_relation ad ah; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) yse zsb; (invs' and valid_cap' cap' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map (aa, b)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ac, ba)) s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ae, bb)) s \<and> (\<forall>x\<in>set zsb. cte_wp_at' (\<lambda>_. True) (snd x) s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<forall>x\<in>set [(ah, cte_map (ae, bb))]. cte_wp_at' (\<lambda>_. True) (snd x) s)) and ?Q'355 y a aa b ya ab ac ba yb ad ae bb yse yc ysf af ag ah zsb) s proof (prove)
goal:
No subgoals!