theory CNodeInv_R

lemma decodeCNodeInvocation_inv[wp]:
  "\<lbrace>P\<rbrace>  decodeCNodeInvocation label args cap cs  \<lbrace>\<lambda>rv. P\<rbrace>" apply (cases "\<not>isCNodeCap cap") apply (simp only: decodeCNodeInvocation_def Let_def split_def
                     fst_conv snd_conv, simp) apply (rule decode_cnode_cases2[where label=label and args=args and exs=cs]) apply (simp_all add: decodeCNodeInvocation_def isCNodeCap_CNodeCap split_def
                             Let_def whenE_def unlessE_def cnode_invok_case_cleanup
                  split del: if_split cong del: if_cong)[6] apply (fold_subgoals (prefix))[6] subgoal premises prems by (safe intro!: hoare_pre[where P=P],
                (wp hoare_drop_imps | simp | wpcw)+) apply (elim disjE exE conjE,
         simp_all add: decodeCNodeInvocation_def isCNodeCap_CNodeCap
                       cnode_invok_case_cleanup unlessE_whenE
                split: list.split_asm split del: if_split) apply (simp_all split: list.split add: unlessE_whenE) apply safe apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<not> isCNodeCap cap \<Longrightarrow> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<not> \<not> isCNodeCap cap \<Longrightarrow> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> \<not> isCNodeCap cap \<Longrightarrow> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>\<not> \<not> isCNodeCap cap; args = index # bits # src_index # src_depth # args'; cs = 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>index bits args'. \<lbrakk>\<not> \<not> isCNodeCap cap; 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>index bits args'. \<lbrakk>\<not> \<not> isCNodeCap cap; 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>index bits args'. \<lbrakk>\<not> \<not> isCNodeCap cap; 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>index bits args'. \<lbrakk>\<not> \<not> isCNodeCap cap; 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 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>\<not> \<not> isCNodeCap cap; args = index # bits # pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; cs = 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<lbrakk>\<not> \<not> isCNodeCap cap; 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', cs) 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', cs) 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>index bits src_index src_depth args' src_root_cap exs'. \<lbrakk>isCNodeCap cap; args = index # bits # src_index # src_depth # args'; cs = 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> 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\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
y <- ensureEmptySlot destSlot;
srcSlot <- lookupSlotForCNodeOp True src_root_cap src_index (unat src_depth);
srcCTE <- liftE (getCTE srcSlot);
y <- if cteCap srcCTE = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup True (Fault_H.lookup_failure.MissingCapability (unat src_depth))) else returnOk ();
p <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | rights # x \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | CNodeMint \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [rights] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | rights # newData # xa \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | CNodeMove \<Rightarrow> returnOk $ (allRights, Nothing) | CNodeMutate \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newData # x \<Rightarrow> returnOk $ (allRights, Just newData) | _ \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
newCap <- (if gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate then returnOk else global.deriveCap srcSlot) (case snd p of None \<Rightarrow> global.maskCapRights (fst p) (cteCap srcCTE) | Some w \<Rightarrow> global.updateCapData (gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate) w (global.maskCapRights (fst p) (cteCap srcCTE)));
y <- if newCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk ((if gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate then Move else Insert) newCap srcSlot destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = index # bits # args'; CNodeRevoke \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeRevoke \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
returnOk (Revoke destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = index # bits # args'; CNodeDelete \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeDelete \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
returnOk (Delete destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = index # bits # args'; CNodeSaveCaller \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeSaveCaller \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
y <- ensureEmptySlot destSlot;
returnOk (SaveCaller destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = index # bits # args'; CNodeCancelBadgedSends \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeCancelBadgedSends \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
cte <- liftE (getCTE destSlot);
y <- if hasCancelSendRights (cteCap cte) then returnOk () else throwError Fault_H.syscall_error.IllegalOperation;
returnOk (CancelBadgedSends (cteCap cte))
odE \<lbrace>\<lambda>rv. P\<rbrace>
 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>isCNodeCap cap; args = index # bits # pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; cs = pivot_root_cap # src_root_cap # exs'; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
srcSlot <- lookupSlotForCNodeOp True src_root_cap src_index (unat src_depth);
pivotSlot <- lookupSlotForCNodeOp True pivot_root_cap pivot_index (unat pivot_depth);
y <- if pivotSlot = srcSlot \<or> pivotSlot = destSlot then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
y <- if srcSlot = destSlot then returnOk () else ensureEmptySlot destSlot;
srcCap <- liftE (liftM cteCap (getCTE srcSlot));
y <- if srcCap = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup True (Fault_H.lookup_failure.MissingCapability (unat src_depth))) else returnOk ();
pivotCap <- liftE (liftM cteCap (getCTE pivotSlot));
y <- if pivotCap = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup False (Fault_H.lookup_failure.MissingCapability (unat pivot_depth))) else returnOk ();
y <- if global.updateCapData True src_new_data srcCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
y <- if global.updateCapData True pivot_new_data pivotCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (Rotate (global.updateCapData True src_new_data srcCap) (global.updateCapData True pivot_new_data pivotCap) srcSlot pivotSlot destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<lbrakk>\<not> \<not> isCNodeCap cap; 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', cs) 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', cs) 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>index bits. isCNodeCap cap \<Longrightarrow> (\<And>src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index # bits # src_index # src_depth # args'; cs = 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> 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\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
y <- ensureEmptySlot destSlot;
srcSlot <- lookupSlotForCNodeOp True src_root_cap src_index (unat src_depth);
srcCTE <- liftE (getCTE srcSlot);
y <- if cteCap srcCTE = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup True (Fault_H.lookup_failure.MissingCapability (unat src_depth))) else returnOk ();
p <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | rights # x \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | CNodeMint \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [rights] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | rights # newData # xa \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | CNodeMove \<Rightarrow> returnOk $ (allRights, Nothing) | CNodeMutate \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newData # x \<Rightarrow> returnOk $ (allRights, Just newData) | _ \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
newCap <- (if gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate then returnOk else global.deriveCap srcSlot) (case snd p of None \<Rightarrow> global.maskCapRights (fst p) (cteCap srcCTE) | Some w \<Rightarrow> global.updateCapData (gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate) w (global.maskCapRights (fst p) (cteCap srcCTE)));
y <- if newCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk ((if gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate then Move else Insert) newCap srcSlot destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index # bits # args'; CNodeRevoke \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeRevoke \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
returnOk (Revoke destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index # bits # args'; CNodeDelete \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeDelete \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
returnOk (Delete destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index # bits # args'; CNodeSaveCaller \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeSaveCaller \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
y <- ensureEmptySlot destSlot;
returnOk (SaveCaller destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index # bits # args'; CNodeCancelBadgedSends \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeCancelBadgedSends \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
cte <- liftE (getCTE destSlot);
y <- if hasCancelSendRights (cteCap cte) then returnOk () else throwError Fault_H.syscall_error.IllegalOperation;
returnOk (CancelBadgedSends (cteCap cte))
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args' pivot_root_cap src_root_cap exs'. \<lbrakk>args = index # bits # pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; cs = pivot_root_cap # src_root_cap # exs'; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
srcSlot <- lookupSlotForCNodeOp True src_root_cap src_index (unat src_depth);
pivotSlot <- lookupSlotForCNodeOp True pivot_root_cap pivot_index (unat pivot_depth);
y <- if pivotSlot = srcSlot \<or> pivotSlot = destSlot then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
y <- if srcSlot = destSlot then returnOk () else ensureEmptySlot destSlot;
srcCap <- liftE (liftM cteCap (getCTE srcSlot));
y <- if srcCap = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup True (Fault_H.lookup_failure.MissingCapability (unat src_depth))) else returnOk ();
pivotCap <- liftE (liftM cteCap (getCTE pivotSlot));
y <- if pivotCap = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup False (Fault_H.lookup_failure.MissingCapability (unat pivot_depth))) else returnOk ();
y <- if global.updateCapData True src_new_data srcCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
y <- if global.updateCapData True pivot_new_data pivotCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (Rotate (global.updateCapData True src_new_data srcCap) (global.updateCapData True pivot_new_data pivotCap) srcSlot pivotSlot destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>)
 2. \<lbrakk>\<not> \<not> isCNodeCap cap; 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', cs) 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', cs) 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>src_index src_depth args' src_root_cap exs'. \<lbrakk>args = index_ # bits_ # src_index # src_depth # args'; cs = 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> 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\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index_ (unat bits_);
y <- ensureEmptySlot destSlot;
srcSlot <- lookupSlotForCNodeOp True src_root_cap src_index (unat src_depth);
srcCTE <- liftE (getCTE srcSlot);
y <- if cteCap srcCTE = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup True (Fault_H.lookup_failure.MissingCapability (unat src_depth))) else returnOk ();
p <- case gen_invocation_type label of CNodeCopy \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | rights # x \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | CNodeMint \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [rights] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | rights # newData # xa \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | CNodeMove \<Rightarrow> returnOk $ (allRights, Nothing) | CNodeMutate \<Rightarrow> case snd (gen_invocation_type label, args') of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newData # x \<Rightarrow> returnOk $ (allRights, Just newData) | _ \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
newCap <- (if gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate then returnOk else global.deriveCap srcSlot) (case snd p of None \<Rightarrow> global.maskCapRights (fst p) (cteCap srcCTE) | Some w \<Rightarrow> global.updateCapData (gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate) w (global.maskCapRights (fst p) (cteCap srcCTE)));
y <- if newCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk ((if gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate then Move else Insert) newCap srcSlot destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index_ # bits_ # args'; CNodeRevoke \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeRevoke \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index_ (unat bits_);
returnOk (Revoke destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index_ # bits_ # args'; CNodeDelete \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeDelete \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index_ (unat bits_);
returnOk (Delete destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index_ # bits_ # args'; CNodeSaveCaller \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeSaveCaller \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index_ (unat bits_);
y <- ensureEmptySlot destSlot;
returnOk (SaveCaller destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>args'. \<lbrakk>args = index_ # bits_ # args'; CNodeCancelBadgedSends \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeCancelBadgedSends \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index_ (unat bits_);
cte <- liftE (getCTE destSlot);
y <- if hasCancelSendRights (cteCap cte) then returnOk () else throwError Fault_H.syscall_error.IllegalOperation;
returnOk (CancelBadgedSends (cteCap cte))
odE \<lbrace>\<lambda>rv. P\<rbrace>) &&& (\<And>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args' pivot_root_cap src_root_cap exs'. \<lbrakk>args = index_ # bits_ # pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; cs = pivot_root_cap # src_root_cap # exs'; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index_ (unat bits_);
srcSlot <- lookupSlotForCNodeOp True src_root_cap src_index (unat src_depth);
pivotSlot <- lookupSlotForCNodeOp True pivot_root_cap pivot_index (unat pivot_depth);
y <- if pivotSlot = srcSlot \<or> pivotSlot = destSlot then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
y <- if srcSlot = destSlot then returnOk () else ensureEmptySlot destSlot;
srcCap <- liftE (liftM cteCap (getCTE srcSlot));
y <- if srcCap = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup True (Fault_H.lookup_failure.MissingCapability (unat src_depth))) else returnOk ();
pivotCap <- liftE (liftM cteCap (getCTE pivotSlot));
y <- if pivotCap = capability.NullCap then throwError (Fault_H.syscall_error.FailedLookup False (Fault_H.lookup_failure.MissingCapability (unat pivot_depth))) else returnOk ();
y <- if global.updateCapData True src_new_data srcCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
y <- if global.updateCapData True pivot_new_data pivotCap = capability.NullCap then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (Rotate (global.updateCapData True src_new_data srcCap) (global.updateCapData True pivot_new_data pivotCap) srcSlot pivotSlot destSlot)
odE \<lbrace>\<lambda>rv. P\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<not> isCNodeCap cap; 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', cs) 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', cs) 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> \<lbrace>P\<rbrace> decodeCNodeInvocation label args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (14 subgoals):
 1. \<lbrakk>isCNodeCap cap; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> case args of [] \<Rightarrow> throw $ if genInvocationType label `~elem~` [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation | [index] \<Rightarrow> throw $ if genInvocationType label `~elem~` [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation | index # bits # args \<Rightarrow> doE inv <- returnOk (genInvocationType label);
unlessE (inv `~elem~` [CNodeRevoke .e. CNodeSaveCaller]) $ throw Fault_H.syscall_error.IllegalOperation;
destSlot <- lookupTargetSlot cap (CPtr index) (fromIntegral bits);
case (inv `~elem~` [CNodeCopy .e. CNodeMutate], inv, args, cs) of (True, CNodeRevoke, [], xb) \<Rightarrow> returnOk $ Revoke destSlot | (True, CNodeRevoke, [srcIndex], xb) \<Rightarrow> returnOk $ Revoke destSlot | (True, CNodeRevoke, srcIndex # srcDepth # args, []) \<Rightarrow> returnOk $ Revoke destSlot | (True, CNodeRevoke, srcIndex # srcDepth # args, srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, args) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeDelete, [], xb) \<Rightarrow> returnOk $ Delete destSlot | (True, CNodeDelete, [srcIndex], xb) \<Rightarrow> returnOk $ Delete destSlot | (True, CNodeDelete, srcIndex # srcDepth # args, []) \<Rightarrow> returnOk $ Delete destSlot | (True, CNodeDelete, srcIndex # srcDepth # args, srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, args) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeCancelBadgedSends, [], xb) \<Rightarrow> doE cte <- withoutFailure $ getCTE destSlot;
unlessE (hasCancelSendRights $ cteCap cte) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ CancelBadgedSends $ cteCap cte
odE | (True, CNodeCancelBadgedSends, [srcIndex], xb) \<Rightarrow> doE cte <- withoutFailure $ getCTE destSlot;
unlessE (hasCancelSendRights $ cteCap cte) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ CancelBadgedSends $ cteCap cte
odE | (True, CNodeCancelBadgedSends, srcIndex # srcDepth # args, []) \<Rightarrow> doE cte <- withoutFailure $ getCTE destSlot;
unlessE (hasCancelSendRights $ cteCap cte) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ CancelBadgedSends $ cteCap cte
odE | (True, CNodeCancelBadgedSends, srcIndex # srcDepth # args, srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, args) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeRotate, [], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, [srcIndex], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, [srcIndex, srcDepth], []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, [srcIndex, srcDepth], srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, []) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeRotate, [srcIndex, srcDepth, aa], []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, [srcIndex, srcDepth, aa], srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, [aa]) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeRotate, [srcIndex, srcDepth, aa, ad], []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, [srcIndex, srcDepth, aa, ad], srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, [aa, ad]) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeRotate, [srcIndex, srcDepth, aa, ad, af], []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, [srcIndex, srcDepth, aa, ad, af], srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, [aa, ad, af]) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeRotate, srcIndex # srcDepth # aa # ad # af # ah # lista, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, CNodeRotate, srcIndex # srcDepth # aa # ad # af # ah # lista, srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, aa # ad # af # ah # lista) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, CNodeSaveCaller, [], xb) \<Rightarrow> doE ensureEmptySlot destSlot;
returnOk $ SaveCaller destSlot
odE | (True, CNodeSaveCaller, [srcIndex], xb) \<Rightarrow> doE ensureEmptySlot destSlot;
returnOk $ SaveCaller destSlot
odE | (True, CNodeSaveCaller, srcIndex # srcDepth # args, []) \<Rightarrow> doE ensureEmptySlot destSlot;
returnOk $ SaveCaller destSlot
odE | (True, CNodeSaveCaller, srcIndex # srcDepth # args, srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, args) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (True, _, [], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, _, [srcIndex], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, _, srcIndex # srcDepth # args, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (True, _, srcIndex # srcDepth # args, srcRootCap # xa) \<Rightarrow> doE ensureEmptySlot destSlot;
srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
srcCTE <- withoutFailure $ getCTE srcSlot;
whenE (isNullCap $ cteCap srcCTE) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
(rights, capData) <- case (inv, args) of (CNodeCopy, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeCopy, rights # xa) \<Rightarrow> returnOk $ (rightsFromWord rights, Nothing) | (CNodeMint, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, [rights]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMint, rights # newData # x) \<Rightarrow> returnOk $ (rightsFromWord rights, Just newData) | (CNodeMove, x) \<Rightarrow> returnOk $ (allRights, Nothing) | (CNodeMutate, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (CNodeMutate, newData # xa) \<Rightarrow> returnOk $ (allRights, Just newData) | (_, x) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage;
isMove <- returnOk (inv `~elem~` [CNodeMove, CNodeMutate]);
srcCap <- returnOk (global.maskCapRights rights $ cteCap srcCTE);
newCap <- (if isMove then returnOk else global.deriveCap srcSlot) $ case capData of None \<Rightarrow> srcCap | Some w \<Rightarrow> global.updateCapData isMove w srcCap;
whenE (isNullCap newCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ (if isMove then Move else Insert) newCap srcSlot destSlot
odE | (False, CNodeRevoke, xa, xb) \<Rightarrow> returnOk $ Revoke destSlot | (False, CNodeDelete, xa, xb) \<Rightarrow> returnOk $ Delete destSlot | (False, CNodeCancelBadgedSends, xa, xb) \<Rightarrow> doE cte <- withoutFailure $ getCTE destSlot;
unlessE (hasCancelSendRights $ cteCap cte) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ CancelBadgedSends $ cteCap cte
odE | (False, CNodeRotate, [], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, [pivotNewData], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, [pivotNewData, pivotIndex], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, [pivotNewData, pivotIndex, pivotDepth], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, [pivotNewData, pivotIndex, pivotDepth, srcNewData], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, [pivotNewData, pivotIndex, pivotDepth, srcNewData, srcIndex], b) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, pivotNewData # pivotIndex # pivotDepth # srcNewData # srcIndex # srcDepth # xa, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, pivotNewData # pivotIndex # pivotDepth # srcNewData # srcIndex # srcDepth # xa, [pivotRootCap]) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (False, CNodeRotate, pivotNewData # pivotIndex # pivotDepth # srcNewData # srcIndex # srcDepth # xa, pivotRootCap # srcRootCap # xb) \<Rightarrow> doE srcSlot <- lookupSourceSlot srcRootCap (CPtr srcIndex) (fromIntegral srcDepth);
pivotSlot <- lookupPivotSlot pivotRootCap (CPtr pivotIndex) (fromIntegral pivotDepth);
whenE (pivotSlot = srcSlot \<or> pivotSlot = destSlot) $ throw Fault_H.syscall_error.IllegalOperation;
unlessE (srcSlot = destSlot) $ ensureEmptySlot destSlot;
srcCap <- withoutFailure $ liftM cteCap $ getCTE srcSlot;
whenE (isNullCap srcCap) $ throw $ Fault_H.syscall_error.FailedLookup True $ Fault_H.lookup_failure.MissingCapability (fromIntegral srcDepth);
pivotCap <- withoutFailure $ liftM cteCap $ getCTE pivotSlot;
whenE (isNullCap pivotCap) $ throw $ Fault_H.syscall_error.FailedLookup False $ Fault_H.lookup_failure.MissingCapability (fromIntegral pivotDepth);
newSrcCap <- returnOk (global.updateCapData True srcNewData srcCap);
newPivotCap <- returnOk (global.updateCapData True pivotNewData pivotCap);
whenE (isNullCap newSrcCap) $ throw Fault_H.syscall_error.IllegalOperation;
whenE (isNullCap newPivotCap) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk $ Rotate newSrcCap newPivotCap srcSlot pivotSlot destSlot
odE | (False, CNodeSaveCaller, xa, xb) \<Rightarrow> doE ensureEmptySlot destSlot;
returnOk $ SaveCaller destSlot
odE | (False, _, ba) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<lbrakk>isCNodeCap cap; args = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x. \<lbrakk>isCNodeCap cap; args = [x]\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = [index, bits]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; args' = []; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>index bits args' x21 x22. \<lbrakk>isCNodeCap cap; args = [index, bits, x21]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>index bits args' x21 x22 x21a x22a. \<lbrakk>isCNodeCap cap; args = index # bits # x21 # x21a # x22a; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller; args' = x21 # x21a # x22a; x22 = x21a # x22a; cs = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = [index, bits]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 8. \<And>index bits args' x21 x22. \<lbrakk>isCNodeCap cap; args = [index, bits, x21]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 9. \<And>index bits args' x21 x22 x21a x22a. \<lbrakk>isCNodeCap cap; args = [index, bits, x21, x21a]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = [x21, x21a]; x22 = [x21a]; x22a = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 10. \<And>index bits args' x21 x22 x21a x22a x21b x22b. \<lbrakk>isCNodeCap cap; args = [index, bits, x21, x21a, x21b]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = [x21, x21a, x21b]; x22 = [x21a, x21b]; x22a = [x21b]; x22b = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<lbrakk>isCNodeCap cap; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> \<lbrace>P\<rbrace> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args = [x21] \<longrightarrow> \<lbrace>P\<rbrace> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (\<forall>x21a x22a. x22 = x21a # x22a \<longrightarrow> args = x21 # x21a # x22a \<longrightarrow> \<lbrace>P\<rbrace> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>))
 2. \<lbrakk>isCNodeCap cap; args = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x. \<lbrakk>isCNodeCap cap; args = [x]\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = [index, bits]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; args' = []; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>index bits args' x21 x22. \<lbrakk>isCNodeCap cap; args = [index, bits, x21]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>index bits args' x21 x22 x21a x22a. \<lbrakk>isCNodeCap cap; args = index # bits # x21 # x21a # x22a; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller; args' = x21 # x21a # x22a; x22 = x21a # x22a; cs = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = [index, bits]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 8. \<And>index bits args' x21 x22. \<lbrakk>isCNodeCap cap; args = [index, bits, x21]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 9. \<And>index bits args' x21 x22 x21a x22a. \<lbrakk>isCNodeCap cap; args = [index, bits, x21, x21a]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = [x21, x21a]; x22 = [x21a]; x22a = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 10. \<And>index bits args' x21 x22 x21a x22a x21b x22b. \<lbrakk>isCNodeCap cap; args = [index, bits, x21, x21a, x21b]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate; args' = [x21, x21a, x21b]; x22 = [x21a, x21b]; x22a = [x21b]; x22b = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<lbrakk>isCNodeCap cap; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]; args = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>x21 x22. \<lbrakk>isCNodeCap cap; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]; args = [x21]\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x21 x22 x21a x22a. \<lbrakk>isCNodeCap cap; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]; args = x21 # x21a # x22a\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<lbrakk>isCNodeCap cap; args = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x. \<lbrakk>isCNodeCap cap; args = [x]\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (if gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = [index, bits]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<And>index bits args' x21 x22. \<lbrakk>isCNodeCap cap; args = [index, bits, x21]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 8. \<And>index bits args' x21 x22 x21a x22a. \<lbrakk>isCNodeCap cap; args = index # bits # x21 # x21a # x22a; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller; cs = []\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 9. \<And>index bits args'. \<lbrakk>isCNodeCap cap; args = [index, bits]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 10. \<And>index bits args' x21 x22. \<lbrakk>isCNodeCap cap; args = [index, bits, x21]; CNodeRotate \<in> set [CNodeRevoke .e. CNodeSaveCaller]; CNodeRotate \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE destSlot <- lookupSlotForCNodeOp False cap index (unat bits);
throwError Fault_H.syscall_error.TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
A total of 16 subgoals... proof (prove)
goal:
No subgoals!