theory CNodeInv_AI

lemma decode_cnode_inv_inv[wp]:
  "\<lbrace>P\<rbrace> decode_cnode_invocation mi args cap cs \<lbrace>\<lambda>rv. P\<rbrace>" unfolding decode_cnode_invocation_def apply (simp add: split_def unlessE_def whenE_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp hoare_drop_imps | simp | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_cnode_invocation mi args cap cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE unlessE (gen_invocation_type mi \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $ throwError IllegalOperation;
whenE (length args < 2) (throwError TruncatedMessage);
index <- returnOk $ data_to_cptr $ args ! 0;
bits <- returnOk $ data_to_nat $ args ! 1;
args <- returnOk $ drop 2 args;
dest_slot <- lookup_target_slot cap index bits;
if 2 \<le> length args \<and> 0 < length cs \<and> gen_invocation_type mi \<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 $ cs ! 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 mi, 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 mi = CNodeRevoke then returnOk $ RevokeCall dest_slot else if gen_invocation_type mi = CNodeDelete then returnOk $ DeleteCall dest_slot else if gen_invocation_type mi = CNodeSaveCaller then doE ensure_empty dest_slot;
returnOk $ SaveCall dest_slot
odE else if gen_invocation_type mi = 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 mi = CNodeRotate \<and> 5 < length args \<and> 1 < length cs 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 $ cs ! 0;
src_root_cap <- returnOk $ cs ! 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 \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE y <- if gen_invocation_type mi \<in> set [CNodeRevoke .e. CNodeSaveCaller] then returnOk () else throwError IllegalOperation;
y <- if length args < 2 then throwError TruncatedMessage else returnOk ();
dest_slot <- lookup_slot_for_cnode_op False cap (data_to_cptr (args ! 0)) (data_to_nat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> cs \<noteq> [] \<and> gen_invocation_type mi \<in> set [CNodeCopy .e. CNodeMutate] then doE y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op True (cs ! 0) (data_to_cptr (drop 2 args ! 0)) (data_to_nat (drop 2 args ! Suc 0));
src_cap <- liftE (get_cap src_slot);
y <- if src_cap = NullCap then throwError (FailedLookup True (MissingCapability (data_to_nat (drop 2 args ! Suc 0)))) else returnOk ();
p <- case gen_invocation_type mi of CNodeCopy \<Rightarrow> case snd (gen_invocation_type mi, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case snd (gen_invocation_type mi, drop 2 (drop 2 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 snd (gen_invocation_type mi, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if snd (snd p) then returnOk else derive_cap src_slot) (case fst (snd p) of None \<Rightarrow> mask_cap (fst p) src_cap | Some w \<Rightarrow> update_cap_data (snd (snd p)) w (mask_cap (fst p) src_cap));
y <- if new_cap = NullCap then throwError IllegalOperation else returnOk ();
returnOk ((if snd (snd p) then MoveCall else InsertCall) new_cap src_slot dest_slot)
odE else if gen_invocation_type mi = CNodeRevoke then returnOk (RevokeCall dest_slot) else if gen_invocation_type mi = CNodeDelete then returnOk (DeleteCall dest_slot) else if gen_invocation_type mi = CNodeSaveCaller then doE y <- ensure_empty dest_slot;
returnOk (SaveCall dest_slot)
odE else if gen_invocation_type mi = CNodeCancelBadgedSends then doE cap <- liftE (get_cap dest_slot);
y <- if has_cancel_send_rights cap then returnOk () else throwError IllegalOperation;
returnOk (CancelBadgedSendsCall cap)
odE else if gen_invocation_type mi = CNodeRotate \<and> 5 < length args - 2 \<and> Suc 0 < length cs then doE src_slot <- lookup_slot_for_cnode_op True (cs ! Suc 0) (data_to_cptr (drop 2 args ! 4)) (data_to_nat (drop 2 args ! 5));
pivot_slot <- lookup_slot_for_cnode_op True (cs ! 0) (data_to_cptr (drop 2 args ! Suc 0)) (data_to_nat (drop 2 args ! 2));
y <- if pivot_slot = src_slot \<or> pivot_slot = dest_slot then throwError IllegalOperation else returnOk ();
y <- if src_slot = dest_slot then returnOk () else ensure_empty dest_slot;
src_cap <- liftE (get_cap src_slot);
y <- if src_cap = NullCap then throwError (FailedLookup True (MissingCapability (data_to_nat (drop 2 args ! 5)))) else returnOk ();
pivot_cap <- liftE (get_cap pivot_slot);
y <- if pivot_cap = NullCap then throwError (FailedLookup False (MissingCapability (data_to_nat (drop 2 args ! 2)))) else returnOk ();
y <- if update_cap_data True (drop 2 args ! 3) src_cap = NullCap then throwError IllegalOperation else returnOk ();
y <- if update_cap_data True (drop 2 args ! 0) pivot_cap = NullCap then throwError IllegalOperation else returnOk ();
returnOk (RotateCall (update_cap_data True (drop 2 args ! 3) src_cap) (update_cap_data True (drop 2 args ! 0) pivot_cap) src_slot pivot_slot dest_slot)
odE else throwError TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q17\<rbrace> doE y <- if gen_invocation_type mi \<in> set [CNodeRevoke .e. CNodeSaveCaller] then returnOk () else throwError IllegalOperation;
y <- if length args < 2 then throwError TruncatedMessage else returnOk ();
dest_slot <- lookup_slot_for_cnode_op False cap (data_to_cptr (args ! 0)) (data_to_nat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> cs \<noteq> [] \<and> gen_invocation_type mi \<in> set [CNodeCopy .e. CNodeMutate] then doE y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op True (cs ! 0) (data_to_cptr (drop 2 args ! 0)) (data_to_nat (drop 2 args ! Suc 0));
src_cap <- liftE (get_cap src_slot);
y <- if src_cap = NullCap then throwError (FailedLookup True (MissingCapability (data_to_nat (drop 2 args ! Suc 0)))) else returnOk ();
p <- case gen_invocation_type mi of CNodeCopy \<Rightarrow> case snd (gen_invocation_type mi, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE | CNodeMint \<Rightarrow> case snd (gen_invocation_type mi, drop 2 (drop 2 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 snd (gen_invocation_type mi, drop 2 (drop 2 args)) of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True) | _ \<Rightarrow> throwError TruncatedMessage;
new_cap <- (if snd (snd p) then returnOk else derive_cap src_slot) (case fst (snd p) of None \<Rightarrow> mask_cap (fst p) src_cap | Some w \<Rightarrow> update_cap_data (snd (snd p)) w (mask_cap (fst p) src_cap));
y <- if new_cap = NullCap then throwError IllegalOperation else returnOk ();
returnOk ((if snd (snd p) then MoveCall else InsertCall) new_cap src_slot dest_slot)
odE else if gen_invocation_type mi = CNodeRevoke then returnOk (RevokeCall dest_slot) else if gen_invocation_type mi = CNodeDelete then returnOk (DeleteCall dest_slot) else if gen_invocation_type mi = CNodeSaveCaller then doE y <- ensure_empty dest_slot;
returnOk (SaveCall dest_slot)
odE else if gen_invocation_type mi = CNodeCancelBadgedSends then doE cap <- liftE (get_cap dest_slot);
y <- if has_cancel_send_rights cap then returnOk () else throwError IllegalOperation;
returnOk (CancelBadgedSendsCall cap)
odE else if gen_invocation_type mi = CNodeRotate \<and> 5 < length args - 2 \<and> Suc 0 < length cs then doE src_slot <- lookup_slot_for_cnode_op True (cs ! Suc 0) (data_to_cptr (drop 2 args ! 4)) (data_to_nat (drop 2 args ! 5));
pivot_slot <- lookup_slot_for_cnode_op True (cs ! 0) (data_to_cptr (drop 2 args ! Suc 0)) (data_to_nat (drop 2 args ! 2));
y <- if pivot_slot = src_slot \<or> pivot_slot = dest_slot then throwError IllegalOperation else returnOk ();
y <- if src_slot = dest_slot then returnOk () else ensure_empty dest_slot;
src_cap <- liftE (get_cap src_slot);
y <- if src_cap = NullCap then throwError (FailedLookup True (MissingCapability (data_to_nat (drop 2 args ! 5)))) else returnOk ();
pivot_cap <- liftE (get_cap pivot_slot);
y <- if pivot_cap = NullCap then throwError (FailedLookup False (MissingCapability (data_to_nat (drop 2 args ! 2)))) else returnOk ();
y <- if update_cap_data True (drop 2 args ! 3) src_cap = NullCap then throwError IllegalOperation else returnOk ();
y <- if update_cap_data True (drop 2 args ! 0) pivot_cap = NullCap then throwError IllegalOperation else returnOk ();
returnOk (RotateCall (update_cap_data True (drop 2 args ! 3) src_cap) (update_cap_data True (drop 2 args ! 0) pivot_cap) src_slot pivot_slot dest_slot)
odE else throwError TruncatedMessage
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q17 s proof (prove)
goal:
No subgoals!