theory Tcb_R

lemma decodeSetIPCBuffer_corres:
  notes if_cong [cong]
  shows
  "\<lbrakk> cap_relation cap cap'; is_thread_cap cap;
     list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras' \<rbrakk> \<Longrightarrow>
   corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x \<in> set extras. cte_at (snd x) s)
                            (\<lambda>s. invs' s \<and> (\<forall>x \<in> set extras'. cte_at' (snd x) s))
       (decode_set_ipc_buffer args cap slot extras)
       (decodeSetIPCBuffer args cap' (cte_map slot) extras')" apply (simp    add: decode_set_ipc_buffer_def decodeSetIPCBuffer_def
           split del: if_split) apply (cases args) apply simp apply (cases extras) apply simp apply (clarsimp simp: list_all2_Cons1 liftME_def[symmetric]
                        is_cap_simps
             split del: if_split) apply (clarsimp simp add: returnOk_def newroot_rel_def) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule deriveCap_corres; simp) apply (simp add: o_def newroot_rel_def split_def dc_def[symmetric]) apply (erule checkValidIPCBuffer_corres) apply (wp hoareE_TrueI | simp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_ipc_buffer args cap slot extras) (decodeSetIPCBuffer args cap' (cte_map slot) extras') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; args = []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE)
 2. \<And>a list. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; args = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; args = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; args = a # list; extras = []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE)
 2. \<And>a list aa lista. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; args = a # list; extras = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>cap_relation cap cap'; is_thread_cap cap; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; args = a # list; extras = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>s. \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s) (\<lambda>s. invs' s \<and> (\<forall>x\<in>set extras'. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE y <- whenE (args = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
case extras ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (tcb_invocation.ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | bufferPtr # x \<Rightarrow> case extras' of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (bufferCap, bufferSlot) # xa \<Rightarrow> doE ipcBuffer <- returnOk (VPtr bufferPtr);
bufferFrame <- if ipcBuffer = 0 then returnOk Nothing else doE bufferCap' <- global.deriveCap bufferSlot bufferCap;
checkValidIPCBuffer ipcBuffer bufferCap';
returnOk $ Just (bufferCap', bufferSlot)
odE;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap') (cte_map slot) Nothing Nothing Nothing Nothing Nothing (Just (ipcBuffer, bufferFrame))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. tcbinv_relation x \<circ> (\<lambda>bufferFrame. tcbinvocation.ThreadControl r (cte_map slot) None None None None None (Some (a, bufferFrame)))) \<circ> (\<lambda>newbuf. tcb_invocation.ThreadControl r slot None None None None None (Some (a, newbuf))))) (\<lambda>s. cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)) (\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)) (if a = 0 then returnOk None else doE buffer_cap <- derive_cap (ab, b) aa;
liftME (\<lambda>y. Some (buffer_cap, ab, b)) (check_valid_ipc_buffer a buffer_cap)
odE) (if a = 0 then returnOk None else doE bufferCap' <- global.deriveCap (cte_map (ab, b)) ac;
liftME (\<lambda>y. Some (bufferCap', cte_map (ab, b))) (checkValidIPCBuffer a bufferCap')
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. tcbinv_relation x \<circ> (\<lambda>bufferFrame. tcbinvocation.ThreadControl r (cte_map slot) None None None None None (Some (a, bufferFrame)))) \<circ> (\<lambda>newbuf. tcb_invocation.ThreadControl r slot None None None None None (Some (a, newbuf))))) (\<lambda>s. cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)) (\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)) (doE buffer_cap <- derive_cap (ab, b) aa;
liftME (\<lambda>y. Some (buffer_cap, ab, b)) (check_valid_ipc_buffer a buffer_cap)
odE) (doE bufferCap' <- global.deriveCap (cte_map (ab, b)) ac;
liftME (\<lambda>y. Some (bufferCap', cte_map (ab, b))) (checkValidIPCBuffer a bufferCap')
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. tcbinv_relation x \<circ> (\<lambda>bufferFrame. tcbinvocation.ThreadControl r (cte_map slot) None None None None None (Some (a, bufferFrame)))) \<circ> (\<lambda>newbuf. tcb_invocation.ThreadControl r slot None None None None None (Some (a, newbuf))))) (?Q26 a list aa ab b lista r ac zs) (?Q'26 a list aa ab b lista r ac zs) (doE buffer_cap <- derive_cap (ab, b) aa;
liftME (\<lambda>y. Some (buffer_cap, ab, b)) (check_valid_ipc_buffer a buffer_cap)
odE) (doE bufferCap' <- global.deriveCap (cte_map (ab, b)) ac;
liftME (\<lambda>y. Some (bufferCap', cte_map (ab, b))) (checkValidIPCBuffer a bufferCap')
odE)
 2. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> ?Q26 a list aa ab b lista r ac zs s
 3. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> ?Q'26 a list aa ab b lista r ac zs s proof (prove)
goal (6 subgoals):
 1. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'30 a list aa ab b lista r ac zs) (?P30 a list aa ab b lista r ac zs) (?P'30 a list aa ab b lista r ac zs) (derive_cap (ab, b) aa) (global.deriveCap (cte_map (ab, b)) ac)
 2. \<And>a list aa ab b lista r ac zs buffer_cap bufferCap'. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; ?r'30 a list aa ab b lista r ac zs buffer_cap bufferCap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. tcbinv_relation x \<circ> (\<lambda>bufferFrame. tcbinvocation.ThreadControl r (cte_map slot) None None None None None (Some (a, bufferFrame)))) \<circ> (\<lambda>newbuf. tcb_invocation.ThreadControl r slot None None None None None (Some (a, newbuf))))) (?R30 a list aa ab b lista r ac zs buffer_cap) (?R'30 a list aa ab b lista r ac zs bufferCap') (liftME (\<lambda>y. Some (buffer_cap, ab, b)) (check_valid_ipc_buffer a buffer_cap)) (liftME (\<lambda>y. Some (bufferCap', cte_map (ab, b))) (checkValidIPCBuffer a bufferCap'))
 3. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 a list aa ab b lista r ac zs\<rbrace> derive_cap (ab, b) aa \<lbrace>?R30 a list aa ab b lista r ac zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30 a list aa ab b lista r ac zs\<rbrace> global.deriveCap (cte_map (ab, b)) ac \<lbrace>?R'30 a list aa ab b lista r ac zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (?P30 a list aa ab b lista r ac zs and ?Q30 a list aa ab b lista r ac zs) s
 6. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (?P'30 a list aa ab b lista r ac zs and ?Q'30 a list aa ab b lista r ac zs) s proof (prove)
goal (5 subgoals):
 1. \<And>a list aa ab b lista r ac zs buffer_cap bufferCap'. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; cap_relation buffer_cap bufferCap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ((\<lambda>x. tcbinv_relation x \<circ> (\<lambda>bufferFrame. tcbinvocation.ThreadControl r (cte_map slot) None None None None None (Some (a, bufferFrame)))) \<circ> (\<lambda>newbuf. tcb_invocation.ThreadControl r slot None None None None None (Some (a, newbuf))))) (?R30 a list aa ab b lista r ac zs buffer_cap) (?R'30 a list aa ab b lista r ac zs bufferCap') (liftME (\<lambda>y. Some (buffer_cap, ab, b)) (check_valid_ipc_buffer a buffer_cap)) (liftME (\<lambda>y. Some (bufferCap', cte_map (ab, b))) (checkValidIPCBuffer a bufferCap'))
 2. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 a list aa ab b lista r ac zs\<rbrace> derive_cap (ab, b) aa \<lbrace>?R30 a list aa ab b lista r ac zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30 a list aa ab b lista r ac zs\<rbrace> global.deriveCap (cte_map (ab, b)) ac \<lbrace>?R'30 a list aa ab b lista r ac zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (ab, b) and ?Q30 a list aa ab b lista r ac zs) s
 5. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) and valid_mdb' and ?Q'30 a list aa ab b lista r ac zs) s proof (prove)
goal (5 subgoals):
 1. \<And>a list aa ab b lista r ac zs buffer_cap bufferCap'. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>p pa. cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)) lista zs; cap_relation aa ac; a \<noteq> 0; cap_relation buffer_cap bufferCap'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?R30 a list aa ab b lista r ac zs buffer_cap) (?R'30 a list aa ab b lista r ac zs bufferCap') (check_valid_ipc_buffer a buffer_cap) (checkValidIPCBuffer a bufferCap')
 2. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 a list aa ab b lista r ac zs\<rbrace> derive_cap (ab, b) aa \<lbrace>?R30 a list aa ab b lista r ac zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30 a list aa ab b lista r ac zs\<rbrace> global.deriveCap (cte_map (ab, b)) ac \<lbrace>?R'30 a list aa ab b lista r ac zs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (ab, b) and ?Q30 a list aa ab b lista r ac zs) s
 5. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) and valid_mdb' and ?Q'30 a list aa ab b lista r ac zs) s proof (prove)
goal (4 subgoals):
 1. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 a list aa ab b lista r ac zs\<rbrace> derive_cap (ab, b) aa \<lbrace>\<lambda>buffer_cap _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a list aa ab b lista r ac zs. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30 a list aa ab b lista r ac zs\<rbrace> global.deriveCap (cte_map (ab, b)) ac \<lbrace>\<lambda>bufferCap' _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; cte_wp_at (\<lambda>_. True) (ab, b) s \<and> (\<forall>x\<in>set lista. cte_wp_at (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (ab, b) and ?Q30 a list aa ab b lista r ac zs) s
 4. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) and valid_mdb' and ?Q'30 a list aa ab b lista r ac zs) s proof (prove)
goal (1 subgoal):
 1. \<And>a list aa ab b lista r ac zs s. \<lbrakk>cap' = capability.ThreadCap r; args = a # list; extras = (aa, ab, b) # lista; cap = cap.ThreadCap r; extras' = (ac, cte_map (ab, b)) # zs; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) lista zs; cap_relation aa ac; a \<noteq> 0; invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map (ab, b)) s \<and> (\<forall>x\<in>set zs. cte_wp_at' (\<lambda>_. True) (snd x) s)\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> ?Q'30 a list aa ab b lista r ac zs s proof (prove)
goal:
No subgoals!