theory CNode_DR

lemma decode_cnode_label_not_match:
  "\<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk>
   \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) (e) \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>" apply (case_tac "invocation_type label = GenInvocationLabel CNodeRevoke") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_cnode_index_and_depth_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeDelete") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_cnode_index_and_depth_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeCancelBadgedSends") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_cnode_index_and_depth_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeCopy") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_intent_cnode_copy_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeMint") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_intent_cnode_mint_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeMove") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_intent_cnode_move_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeMutate") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_intent_cnode_mutate_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeRotate") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_intent_cnode_rotate_def split:option.splits list.splits) apply (case_tac "invocation_type label = GenInvocationLabel CNodeSaveCaller") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def) apply (clarsimp simp:transform_cnode_index_and_depth_def split:option.splits list.splits) apply (clarsimp simp:Decode_A.decode_cnode_invocation_def unlessE_def) apply (subgoal_tac "\<not> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]") apply (clarsimp simp: gen_invocation_type_eq) apply wp apply (clarsimp simp: upto_enum_def fromEnum_def toEnum_def enum_invocation_label
                        enum_gen_invocation_labels gen_invocation_type_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label = GenInvocationLabel CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label = GenInvocationLabel CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label = GenInvocationLabel CNodeCopy\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_intent_cnode_copy args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeCopy\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label = GenInvocationLabel CNodeMint\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_intent_cnode_mint args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeMint\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label = GenInvocationLabel CNodeMove\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_intent_cnode_move args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeMove\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label = GenInvocationLabel CNodeMutate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_intent_cnode_mutate args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeMutate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label = GenInvocationLabel CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_intent_cnode_rotate args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label = GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args); \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label = GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label args (cap.CNodeCap a b c) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap a b c) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> e \<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 $ e ! 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 args) \<and> 1 < length e 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 $ e ! 0;
src_root_cap <- returnOk $ e ! 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 \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>) \<and> (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 2) (throwError TruncatedMessage);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap a b c) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> e \<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 $ e ! 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 args) \<and> 1 < length e 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 $ e ! 0;
src_root_cap <- returnOk $ e ! 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 \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>) \<and> (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>)
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; gen_invocation_type label \<noteq> CNodeRevoke; gen_invocation_type label \<noteq> CNodeDelete; gen_invocation_type label \<noteq> CNodeCancelBadgedSends; gen_invocation_type label \<noteq> CNodeCopy; gen_invocation_type label \<noteq> CNodeMint; gen_invocation_type label \<noteq> CNodeMove; gen_invocation_type label \<noteq> CNodeMutate; gen_invocation_type label \<noteq> CNodeRotate; gen_invocation_type label \<noteq> CNodeSaveCaller; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> CNodeIntent ui; invocation_type label \<noteq> GenInvocationLabel CNodeRevoke; invocation_type label \<noteq> GenInvocationLabel CNodeDelete; invocation_type label \<noteq> GenInvocationLabel CNodeCancelBadgedSends; invocation_type label \<noteq> GenInvocationLabel CNodeCopy; invocation_type label \<noteq> GenInvocationLabel CNodeMint; invocation_type label \<noteq> GenInvocationLabel CNodeMove; invocation_type label \<noteq> GenInvocationLabel CNodeMutate; invocation_type label \<noteq> GenInvocationLabel CNodeRotate; invocation_type label \<noteq> GenInvocationLabel CNodeSaveCaller\<rbrakk> \<Longrightarrow> gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] proof (prove)
goal:
No subgoals!