theory CNode_DR

lemma decode_cnode_error_corres:
  "\<not> (\<exists> ui. (Some (CNodeIntent ui)) = (transform_intent (invocation_type label) args)) \<Longrightarrow>
     dcorres (dc \<oplus> anyrel) \<top> \<top>
      (throwError e)
      (Decode_A.decode_cnode_invocation label args (cap.CNodeCap word n list) excaps)" apply(subst (asm) (1) transform_intent_isnot_CNodeIntent) apply(unfold Decode_A.decode_cnode_invocation_def) apply (rule_tac label=label and args=args and exs=excaps in decode_cnode_cases2) apply (simp_all add: unlessE_whenE gen_invocation_type_eq del: disj_not1) apply clarsimp apply (rule corres_symb_exec_r_dcE, wp) apply (rule corres_symb_exec_r_dcE, wp) apply (rule corres_symb_exec_r_dcE, wp) apply (rule corres_symb_exec_r_dcE, wp) apply (rule corres_symb_exec_r_dcE) apply (rule hoare_pre, wp whenE_wp) apply simp apply (rule corres_trivial) apply (simp split: gen_invocation_labels.split invocation_label.split list.split) apply (auto)[1] apply wp+ apply (elim disjE, simp_all) apply (simp add: whenE_def) apply (clarsimp simp: whenE_def) apply clarsimp apply (elim disjE) apply (clarsimp split: list.split_asm
            | rule corres_symb_exec_r_dcE[OF _ corres_trivial]
            | wp | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>ui. Some (CNodeIntent ui) = transform_intent (invocation_type label) args \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (Decode_A.decode_cnode_invocation label args (cap.CNodeCap word n list) excaps) proof (prove)
goal (1 subgoal):
 1. (invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (Decode_A.decode_cnode_invocation label args (cap.CNodeCap word n list) excaps) proof (prove)
goal (1 subgoal):
 1. (invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (7 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<notin> {CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller}\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 2. \<And>index bits args'. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRevoke\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 3. \<And>index bits args'. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeDelete\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 4. \<And>index bits args'. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 5. \<And>index bits args'. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 6. \<And>index bits pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args' pivot_root_cap src_root_cap exs'. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); args = index # bits # pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; excaps = pivot_root_cap # src_root_cap # exs'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 7. \<lbrakk>(invocation_type label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (invocation_type label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (invocation_type label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (invocation_type label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (invocation_type label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (invocation_type label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<notin> {CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller} \<and> (case (args', excaps) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs') \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case (args', excaps) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot (cap.CNodeCap word n list) index bits;
if 2 \<le> length args \<and> 0 < length excaps \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length args \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (2 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2) \<and> gen_invocation_type label \<noteq> CNodeMove \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []) \<and> gen_invocation_type label \<noteq> CNodeSaveCaller; args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits);
y <- CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth);
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth))));
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot)
odE)
 2. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (2 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits);
y <- CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth);
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth))));
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot)
odE)
 2. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (3 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R19 index bits src_index src_depth args' src_root_cap exs' x) (throwError e) (doE y <- CSpaceAcc_A.ensure_empty x;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth);
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth))));
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 3. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (4 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R27 index bits src_index src_depth args' src_root_cap exs' x y) (throwError e) (doE src_slot <- CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth);
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth))));
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 4. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (5 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot) (throwError e) (doE src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth))));
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 5. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (6 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap) (throwError e) (doE y <- whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth))));
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 6. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (8 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap P. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R53 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya) (throwError e) (doE (rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>?R53 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 6. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 7. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 8. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (8 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap P s. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller; P s\<rbrakk> \<Longrightarrow> (if src_cap = cap.NullCap then \<lambda>s. P s \<and> True else P) s
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R53 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya) (throwError e) (doE (rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>?R53 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 6. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 7. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 8. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (7 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (?R53 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya) (throwError e) (doE (rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>?R53 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 6. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 7. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (7 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap ya. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE (rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args' of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>\<lambda>ya _. True\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 6. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 7. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (7 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<forall>x21 x21a. (\<exists>x22. args' = x21 # x21a # x22) \<longrightarrow> gen_invocation_type label = CNodeMint \<longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE new_cap <- CSpace_A.derive_cap src_slot (CSpace_A.update_cap_data False x21a (mask_cap (data_to_rights x21) src_cap));
y <- whenE (new_cap = cap.NullCap) (throwError IllegalOperation);
returnOk (cnode_invocation.InsertCall new_cap src_slot x)
odE)
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>\<lambda>ya _. True\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 6. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 7. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (6 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot src_cap\<rbrace> whenE (src_cap = cap.NullCap) (throwError (FailedLookup True (MissingCapability (unat src_depth)))) \<lbrace>\<lambda>ya _. True\<rbrace>, -
 2. \<And>index bits src_index src_depth args' src_root_cap exs' x y src_slot. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace> liftE (CSpaceAcc_A.get_cap src_slot) \<lbrace>?R43 index bits src_index src_depth args' src_root_cap exs' x y src_slot\<rbrace>, -
 3. \<And>index bits src_index src_depth args' src_root_cap exs' x y. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace> CSpace_A.lookup_slot_for_cnode_op True src_root_cap (to_bl src_index) (unat src_depth) \<lbrace>?R35 index bits src_index src_depth args' src_root_cap exs' x y\<rbrace>, -
 4. \<And>index bits src_index src_depth args' src_root_cap exs' x. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs' x\<rbrace> CSpaceAcc_A.ensure_empty x \<lbrace>?R27 index bits src_index src_depth args' src_root_cap exs' x\<rbrace>, -
 5. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; excaps = src_root_cap # exs'; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> args' = []; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 2; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label = CNodeMutate \<longrightarrow> args' = []; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits) \<lbrace>?R19 index bits src_index src_depth args' src_root_cap exs'\<rbrace>, -
 6. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (3 subgoals):
 1. args = [] \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
throwError TruncatedMessage
odE)
 2. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); \<exists>x. args = [x]\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 3. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); \<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); \<exists>x. args = [x]\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 2. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); \<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(gen_invocation_type label = CNodeRevoke \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> length args < 6) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> length args < 4) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> length args < 5) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> length args < 8) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> length args < 2); \<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE y <- whenE (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]) (throwError IllegalOperation);
y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 args ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 1;
args <- returnOk $ drop 2 (drop 2 args);
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type label, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 args) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 args ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 args ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 args ! 2;
src_new_data <- returnOk $ drop 2 args ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 args ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 args ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (1 subgoal):
 1. \<And>index bits args'. \<lbrakk>gen_invocation_type label \<noteq> CNodeRevoke; args = index # bits # args'; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False); gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> length args' < 3; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 4; gen_invocation_type label = CNodeMove \<longrightarrow> length args' < 2; gen_invocation_type label = CNodeMutate \<longrightarrow> length args' < 3; gen_invocation_type label = CNodeRotate \<longrightarrow> length args' < 6; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits);
if 2 \<le> length args' \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 1;
args <- returnOk $ drop 2 (drop 2 (index # bits # args'));
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 (index # bits # args')) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 (index # bits # args') ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 2;
src_new_data <- returnOk $ drop 2 (index # bits # args') ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal (2 subgoals):
 1. \<And>index bits args'. \<lbrakk>gen_invocation_type label \<noteq> CNodeRevoke; args = index # bits # args'; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> length args' < 3; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 4; gen_invocation_type label = CNodeMove \<longrightarrow> length args' < 2; gen_invocation_type label = CNodeMutate \<longrightarrow> length args' < 3; gen_invocation_type label = CNodeRotate \<longrightarrow> length args' < 6; gen_invocation_type label \<noteq> CNodeSaveCaller; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | src_root_cap # exs' \<Rightarrow> False)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits);
if 2 \<le> length args' \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 1;
args <- returnOk $ drop 2 (drop 2 (index # bits # args'));
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 (index # bits # args')) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 (index # bits # args') ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 2;
src_new_data <- returnOk $ drop 2 (index # bits # args') ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)
 2. \<And>index bits args'. \<lbrakk>gen_invocation_type label \<noteq> CNodeRevoke; args = index # bits # args'; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label = CNodeCopy \<longrightarrow> length args' < 3; gen_invocation_type label = CNodeMint \<longrightarrow> length args' < 4; gen_invocation_type label = CNodeMove \<longrightarrow> length args' < 2; gen_invocation_type label = CNodeMutate \<longrightarrow> length args' < 3; gen_invocation_type label = CNodeRotate \<longrightarrow> length args' < 6; gen_invocation_type label \<noteq> CNodeSaveCaller; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case args' of [] \<Rightarrow> True | [pivot_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data] \<Rightarrow> True | [pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index] \<Rightarrow> True | pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'' \<Rightarrow> case excaps of [] \<Rightarrow> True | [pivot_root_cap] \<Rightarrow> True | pivot_root_cap # src_root_cap # exs' \<Rightarrow> False)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap word n list) (to_bl index) (unat bits);
if 2 \<le> length args' \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 0;
src_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 1;
args <- returnOk $ drop 2 (drop 2 (index # bits # args'));
src_root_cap <- returnOk $ excaps ! 0;
CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [rightsWord] \<Rightarrow> throwError TruncatedMessage | rightsWord # capData # xa \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | CNodeMove \<Rightarrow> returnOk (all_rights, None, True) | CNodeMutate \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w src_cap);
whenE (new_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type label = CNodeRevoke then returnOk $ cnode_invocation.RevokeCall dest_slot else if gen_invocation_type label = CNodeDelete then returnOk $ cnode_invocation.DeleteCall dest_slot else if gen_invocation_type label = CNodeSaveCaller then doE CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ cnode_invocation.SaveCall dest_slot
odE else if gen_invocation_type label = CNodeCancelBadgedSends then doE cap <- liftE $ CSpaceAcc_A.get_cap dest_slot;
unlessE (CSpace_A.has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.CancelBadgedSendsCall cap
odE else if gen_invocation_type label = CNodeRotate \<and> 5 < length (drop 2 (index # bits # args')) \<and> 1 < length excaps then doE pivot_new_data <- returnOk $ drop 2 (index # bits # args') ! 0;
pivot_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 1;
pivot_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 2;
src_new_data <- returnOk $ drop 2 (index # bits # args') ! 3;
src_index <- returnOk $ data_to_cptr $ drop 2 (index # bits # args') ! 4;
src_depth <- returnOk $ data_to_nat $ drop 2 (index # bits # args') ! 5;
pivot_root_cap <- returnOk $ excaps ! 0;
src_root_cap <- returnOk $ excaps ! 1;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $ throwError IllegalOperation;
unlessE (src_slot = dest_slot) $ CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE $ CSpaceAcc_A.get_cap src_slot;
whenE (src_cap = cap.NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ CSpaceAcc_A.get_cap pivot_slot;
whenE (pivot_cap = cap.NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ CSpace_A.update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ CSpace_A.update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = cap.NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = cap.NullCap) $ throwError IllegalOperation;
returnOk $ cnode_invocation.RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE) proof (prove)
goal:
No subgoals!