theory CNode_AC

lemma decode_cnode_invocation_auth_derived:
  "\<lbrace>\<top> :: det_ext state \<Rightarrow> bool\<rbrace>
   decode_cnode_invocation label args cap excaps
   \<lbrace>cnode_inv_auth_derivations\<rbrace>,-" apply (simp add: decode_cnode_invocation_def split_def whenE_def unlessE_def split del: if_split) apply (wpsimp wp: derive_cap_auth_derived get_cap_auth_derived hoare_vcg_all_lift
              simp: cnode_inv_auth_derivations_If_Insert_Move[unfolded cnode_inv_auth_derivations_def]
                    cnode_inv_auth_derivations_def split_def whenE_def split_del: if_split
         | strengthen cte_wp_at_auth_derived_mask_cap_strg cte_wp_at_auth_derived_update_cap_data_strg
         | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> decode_cnode_invocation label args cap excaps \<lbrace>cnode_inv_auth_derivations\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE y <- if gen_invocation_type label \<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 (to_bl (args ! 0)) (data_to_nat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then doE y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op True (excaps ! 0) (to_bl (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 label of CNodeCopy \<Rightarrow> case snd (gen_invocation_type label, 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 label, 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 label, 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 label = CNodeRevoke then returnOk (RevokeCall dest_slot) else if gen_invocation_type label = CNodeDelete then returnOk (DeleteCall dest_slot) else if gen_invocation_type label = CNodeSaveCaller then doE y <- ensure_empty dest_slot;
returnOk (SaveCall dest_slot)
odE else if gen_invocation_type label = 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 label = CNodeRotate \<and> 5 < length args - 2 \<and> Suc 0 < length excaps then doE src_slot <- lookup_slot_for_cnode_op True (excaps ! Suc 0) (to_bl (drop 2 args ! 4)) (data_to_nat (drop 2 args ! 5));
pivot_slot <- lookup_slot_for_cnode_op True (excaps ! 0) (to_bl (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>cnode_inv_auth_derivations\<rbrace>, - proof (prove)
goal:
No subgoals!