theory EmptyFail_AI

lemma decode_cnode_invocation_empty_fail[wp]:
  "\<And>a b c d. empty_fail (decode_cnode_invocation a b c d :: (cnode_invocation, 'state_ext) se_monad)" unfolding decode_cnode_invocation_def by (wp | wpc | intro impI conjI allI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>a b c d. empty_fail (decode_cnode_invocation a b c d) proof (prove)
goal (1 subgoal):
 1. \<And>a b c d. empty_fail (doE unlessE (gen_invocation_type a \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length b < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ b ! 0;
bits <- returnOk $ data_to_nat $ b ! 1;
args <- returnOk $ drop 2 b;
dest_slot <- lookup_target_slot c index bits;
if 2 \<le> length args \<and> 0 < length d \<and> gen_invocation_type a \<in> set [CNodeCopy .e. CNodeMutate] then doE src_index <- returnOk $ data_to_cptr $ args ! 0;
src_depth <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
src_root_cap <- returnOk $ d ! 0;
ensure_empty dest_slot;
src_slot <- lookup_source_slot src_root_cap src_index src_depth;
src_cap <- liftE $ get_cap src_slot;
whenE (src_cap = NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
(rights, cap_data, is_move) <- case (gen_invocation_type a, args) of (CNodeCopy, []) \<Rightarrow> throwError TruncatedMessage | (CNodeCopy, rightsWord # xa) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | (CNodeMint, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, [rightsWord]) \<Rightarrow> throwError TruncatedMessage | (CNodeMint, rightsWord # capData # x) \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, Some capData, False)
odE | (CNodeMove, x) \<Rightarrow> returnOk (all_rights, None, True) | (CNodeMutate, []) \<Rightarrow> throwError TruncatedMessage | (CNodeMutate, capData # xa) \<Rightarrow> returnOk (all_rights, Some capData, True) | (_, x) \<Rightarrow> throwError TruncatedMessage;
src_cap <- returnOk $ mask_cap rights src_cap;
new_cap <- (if is_move then returnOk else derive_cap src_slot) (case cap_data of None \<Rightarrow> src_cap | Some w \<Rightarrow> update_cap_data is_move w src_cap);
whenE (new_cap = NullCap) $ throwError IllegalOperation;
returnOk $ (if is_move then MoveCall else InsertCall) new_cap src_slot dest_slot
odE else if gen_invocation_type a = CNodeRevoke then returnOk $ RevokeCall dest_slot else if gen_invocation_type a = CNodeDelete then returnOk $ DeleteCall dest_slot else if gen_invocation_type a = CNodeSaveCaller then doE ensure_empty dest_slot;
returnOk $ SaveCall dest_slot
odE else if gen_invocation_type a = CNodeCancelBadgedSends then doE cap <- liftE $ get_cap dest_slot;
unlessE (has_cancel_send_rights cap) $ throwError IllegalOperation;
returnOk $ CancelBadgedSendsCall cap
odE else if gen_invocation_type a = CNodeRotate \<and> 5 < length args \<and> 1 < length d then doE pivot_new_data <- returnOk $ args ! 0;
pivot_index <- returnOk $ data_to_cptr $ args ! 1;
pivot_depth <- returnOk $ data_to_nat $ args ! 2;
src_new_data <- returnOk $ args ! 3;
src_index <- returnOk $ data_to_cptr $ args ! 4;
src_depth <- returnOk $ data_to_nat $ args ! 5;
pivot_root_cap <- returnOk $ d ! 0;
src_root_cap <- returnOk $ d ! 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) $ ensure_empty dest_slot;
src_cap <- liftE $ get_cap src_slot;
whenE (src_cap = NullCap) $ throwError $ FailedLookup True $ MissingCapability src_depth;
pivot_cap <- liftE $ get_cap pivot_slot;
whenE (pivot_cap = NullCap) $ throwError $ FailedLookup False $ MissingCapability pivot_depth;
new_src_cap <- returnOk $ update_cap_data True src_new_data src_cap;
new_pivot_cap <- returnOk $ update_cap_data True pivot_new_data pivot_cap;
whenE (new_src_cap = NullCap) $ throwError IllegalOperation;
whenE (new_pivot_cap = NullCap) $ throwError IllegalOperation;
returnOk $ RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
odE else throwError TruncatedMessage
odE)