theory Syscall_DR

lemma transform_intent_cnode_cap_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk>
   \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" supply if_cong[cong] apply (clarsimp simp:Decode_A.decode_invocation_def) apply (simp add: Decode_A.decode_cnode_invocation_def unlessE_def upto_enum_def
                   fromEnum_def toEnum_def enum_invocation_label enum_gen_invocation_labels
                   whenE_def) apply (intro conjI impI;
           clarsimp simp: transform_intent_def transform_cnode_index_and_depth_def
                          transform_intent_cnode_copy_def
                          transform_intent_cnode_mint_def transform_intent_cnode_move_def
                          transform_intent_cnode_mutate_def transform_intent_cnode_rotate_def
                    simp flip: gen_invocation_type_eq
                    split: list.split_asm;
           (solves \<open>wpsimp\<close>)?) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (Decode_A.decode_cnode_invocation label args (cap.CNodeCap w n list) (map fst excaps)) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk> \<Longrightarrow> (length args < 2 \<longrightarrow> (gen_invocation_type label = CNodeRevoke \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError TruncatedMessage) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (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> CNodeCopy \<and> gen_invocation_type label \<noteq> CNodeMint \<and> gen_invocation_type label \<noteq> CNodeMove \<and> gen_invocation_type label \<noteq> CNodeMutate \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError IllegalOperation) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>)) \<and> (\<not> length args < 2 \<longrightarrow> (gen_invocation_type label = CNodeRevoke \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
returnOk (cnode_invocation.RevokeCall dest_slot)
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
returnOk (cnode_invocation.DeleteCall dest_slot)
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
cap <- liftE (CSpaceAcc_A.get_cap dest_slot);
y <- if CSpace_A.has_cancel_send_rights cap then returnOk () else throwError IllegalOperation;
returnOk (cnode_invocation.CancelBadgedSendsCall cap)
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] then doE y <- CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True (fst (excaps ! 0)) (to_bl (args ! 2)) (unat (args ! 3));
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- if src_cap = cap.NullCap then throwError (FailedLookup True (MissingCapability (unat (args ! 3)))) else returnOk ();
(rights, cap_data, is_move) <- case drop 4 args of [] \<Rightarrow> throwError TruncatedMessage | rightsWord # x \<Rightarrow> doE rights <- returnOk $ data_to_rights $ rightsWord;
returnOk $ (rights, None, False)
odE;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- if new_cap = cap.NullCap then throwError IllegalOperation else returnOk ();
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot)
odE else throwError TruncatedMessage
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] then doE y <- CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True (fst (excaps ! 0)) (to_bl (args ! 2)) (unat (args ! 3));
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- if src_cap = cap.NullCap then throwError (FailedLookup True (MissingCapability (unat (args ! 3)))) else returnOk ();
(rights, cap_data, is_move) <- case drop 4 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;
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- if new_cap = cap.NullCap then throwError IllegalOperation else returnOk ();
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot)
odE else throwError TruncatedMessage
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] then doE y <- CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True (fst (excaps ! 0)) (to_bl (args ! 2)) (unat (args ! 3));
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- if src_cap = cap.NullCap then throwError (FailedLookup True (MissingCapability (unat (args ! 3)))) else returnOk ();
y <- if src_cap = cap.NullCap then throwError IllegalOperation else returnOk ();
returnOk (cnode_invocation.MoveCall (mask_cap all_rights src_cap) src_slot dest_slot)
odE else throwError TruncatedMessage
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 2 \<le> length args - 2 \<and> excaps \<noteq> [] then doE y <- CSpaceAcc_A.ensure_empty dest_slot;
src_slot <- CSpace_A.lookup_slot_for_cnode_op True (fst (excaps ! 0)) (to_bl (args ! 2)) (unat (args ! 3));
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- if src_cap = cap.NullCap then throwError (FailedLookup True (MissingCapability (unat (args ! 3)))) else returnOk ();
(rights, cap_data, is_move) <- case drop 4 args of [] \<Rightarrow> throwError TruncatedMessage | capData # x \<Rightarrow> returnOk (all_rights, Some capData, True);
new_cap <- (if is_move then returnOk else CSpace_A.derive_cap src_slot) (case cap_data of None \<Rightarrow> mask_cap rights src_cap | Some w \<Rightarrow> CSpace_A.update_cap_data is_move w (mask_cap rights src_cap));
y <- if new_cap = cap.NullCap then throwError IllegalOperation else returnOk ();
returnOk ((if is_move then cnode_invocation.MoveCall else cnode_invocation.InsertCall) new_cap src_slot dest_slot)
odE else throwError TruncatedMessage
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
if 5 < length args - 2 \<and> Suc 0 < length excaps then doE src_slot <- CSpace_A.lookup_slot_for_cnode_op True (fst (excaps ! Suc 0)) (to_bl (args ! 6)) (unat (args ! 7));
pivot_slot <- CSpace_A.lookup_slot_for_cnode_op True (map fst excaps ! 0) (to_bl (args ! 3)) (unat (args ! 4));
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 CSpaceAcc_A.ensure_empty dest_slot;
src_cap <- liftE (CSpaceAcc_A.get_cap src_slot);
y <- if src_cap = cap.NullCap then throwError (FailedLookup True (MissingCapability (unat (args ! 7)))) else returnOk ();
pivot_cap <- liftE (CSpaceAcc_A.get_cap pivot_slot);
y <- if pivot_cap = cap.NullCap then throwError (FailedLookup False (MissingCapability (unat (args ! 4)))) else returnOk ();
y <- if CSpace_A.update_cap_data True (args ! 5) src_cap = cap.NullCap then throwError IllegalOperation else returnOk ();
y <- if CSpace_A.update_cap_data True (args ! 2) pivot_cap = cap.NullCap then throwError IllegalOperation else returnOk ();
returnOk (cnode_invocation.RotateCall (CSpace_A.update_cap_data True (args ! 5) src_cap) (CSpace_A.update_cap_data True (args ! 2) pivot_cap) src_slot pivot_slot dest_slot)
odE else throwError TruncatedMessage
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (doE dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (cap.CNodeCap w n list) (to_bl (args ! 0)) (unat (args ! Suc 0));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (cnode_invocation.SaveCall dest_slot)
odE) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>) \<and> (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> CNodeCopy \<and> gen_invocation_type label \<noteq> CNodeMint \<and> gen_invocation_type label \<noteq> CNodeMove \<and> gen_invocation_type label \<noteq> CNodeMutate \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeCNode (throwError IllegalOperation) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>)) proof (prove)
goal:
No subgoals!