theory Untyped_R

lemma decodeUntyped_inv[wp]:
  "\<lbrace>P\<rbrace> decodeUntypedInvocation label args slot
       (UntypedCap d w n idx) cs \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decodeUntypedInvocation_def whenE_def
                   split_def unlessE_def Let_def
              split del: if_split cong: if_cong list.case_cong) apply (rule hoare_pre) apply (wp mapME_x_inv_wp hoare_drop_imps constOnFailure_wp
             mapM_wp'
               | wpcw
               | simp add: lookupTargetSlot_def locateSlot_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decodeUntypedInvocation label args slot (capability.UntypedCap d w n idx) cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case args of [] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW, nodeIndexW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW, nodeIndexW, nodeDepthW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW, nodeIndexW, nodeDepthW, nodeOffset] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | newTypeW # userObjSizeW # nodeIndexW # nodeDepthW # nodeOffset # nodeWindow # x \<Rightarrow> case cs of [] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | rootCap # xa \<Rightarrow> doE y <- if gen_invocation_type label = UntypedRetype then returnOk () else throwError Fault_H.syscall_error.IllegalOperation;
y <- if fromEnum maxBound < unat newTypeW then throwError (Fault_H.syscall_error.InvalidArgument 0) else returnOk ();
y <- if unat userObjSizeW < wordBits then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (word_of_nat maxUntypedSizeBits));
y <- rangeCheck (APIType_capBits (toEnum (unat newTypeW)) (unat userObjSizeW)) 0 maxUntypedSizeBits;
y <- if toEnum (unat newTypeW) = fromAPIType ArchTypes_H.apiobject_type.CapTableObject \<and> unat userObjSizeW = 0 then throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)) else returnOk ();
y <- if toEnum (unat newTypeW) = fromAPIType ArchTypes_H.apiobject_type.Untyped \<and> unat userObjSizeW < minUntypedSizeBits then throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)) else returnOk ();
nodeCap <- if unat nodeDepthW = 0 then returnOk rootCap else doE nodeSlot <- lookupTargetSlot rootCap nodeIndexW (unat nodeDepthW);
liftE (getSlotCap nodeSlot)
odE;
y <- case nodeCap of capability.CNodeCap x xa xb xc \<Rightarrow> returnOk () | _ \<Rightarrow> throw $ Fault_H.syscall_error.FailedLookup False $ Fault_H.lookup_failure.MissingCapability (unat nodeDepthW);
y <- rangeCheck nodeOffset 0 (2 ^ capCNodeBits nodeCap - 1);
y <- rangeCheck nodeWindow 1 retypeFanOutLimit;
y <- rangeCheck nodeWindow 1 (2 ^ capCNodeBits nodeCap - nodeOffset);
slots <- liftE (mapM (locateSlotCap nodeCap) [nodeOffset .e. nodeOffset + nodeWindow - 1]);
y <- mapME_x ensureEmptySlot slots;
reset <- liftE (constOnFailure False (doE y <- ensureNoChildren slot;
returnOk True
odE));
y <- if word_of_nat (shiftR (shiftL (Suc 0) n - (if reset then 0 else idx)) (APIType_capBits (toEnum (unat newTypeW)) (unat userObjSizeW))) < nodeWindow then throwError (Fault_H.syscall_error.NotEnoughMemory (word_of_nat (shiftL (Suc 0) n - (if reset then 0 else idx)))) else returnOk ();
y <- if d \<and> \<not> isFrameType (toEnum (unat newTypeW)) \<and> toEnum (unat newTypeW) \<noteq> fromAPIType ArchTypes_H.apiobject_type.Untyped then throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)) else returnOk ();
returnOk (Invocations_H.untyped_invocation.Retype slot reset w (More_Word_Operations.alignUp (getFreeRef w (if reset then 0 else idx)) (APIType_capBits (toEnum (unat newTypeW)) (unat userObjSizeW))) (toEnum (unat newTypeW)) (unat userObjSizeW) slots d)
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q28\<rbrace> case args of [] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW, nodeIndexW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW, nodeIndexW, nodeDepthW] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | [newTypeW, userObjSizeW, nodeIndexW, nodeDepthW, nodeOffset] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | newTypeW # userObjSizeW # nodeIndexW # nodeDepthW # nodeOffset # nodeWindow # x \<Rightarrow> case cs of [] \<Rightarrow> throwError (if gen_invocation_type label = UntypedRetype then Fault_H.syscall_error.TruncatedMessage else Fault_H.syscall_error.IllegalOperation) | rootCap # xa \<Rightarrow> doE y <- if gen_invocation_type label = UntypedRetype then returnOk () else throwError Fault_H.syscall_error.IllegalOperation;
y <- if fromEnum maxBound < unat newTypeW then throwError (Fault_H.syscall_error.InvalidArgument 0) else returnOk ();
y <- if unat userObjSizeW < wordBits then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (word_of_nat maxUntypedSizeBits));
y <- rangeCheck (APIType_capBits (toEnum (unat newTypeW)) (unat userObjSizeW)) 0 maxUntypedSizeBits;
y <- if toEnum (unat newTypeW) = fromAPIType ArchTypes_H.apiobject_type.CapTableObject \<and> unat userObjSizeW = 0 then throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)) else returnOk ();
y <- if toEnum (unat newTypeW) = fromAPIType ArchTypes_H.apiobject_type.Untyped \<and> unat userObjSizeW < minUntypedSizeBits then throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)) else returnOk ();
nodeCap <- if unat nodeDepthW = 0 then returnOk rootCap else doE nodeSlot <- lookupTargetSlot rootCap nodeIndexW (unat nodeDepthW);
liftE (getSlotCap nodeSlot)
odE;
y <- case nodeCap of capability.CNodeCap x xa xb xc \<Rightarrow> returnOk () | _ \<Rightarrow> throw $ Fault_H.syscall_error.FailedLookup False $ Fault_H.lookup_failure.MissingCapability (unat nodeDepthW);
y <- rangeCheck nodeOffset 0 (2 ^ capCNodeBits nodeCap - 1);
y <- rangeCheck nodeWindow 1 retypeFanOutLimit;
y <- rangeCheck nodeWindow 1 (2 ^ capCNodeBits nodeCap - nodeOffset);
slots <- liftE (mapM (locateSlotCap nodeCap) [nodeOffset .e. nodeOffset + nodeWindow - 1]);
y <- mapME_x ensureEmptySlot slots;
reset <- liftE (constOnFailure False (doE y <- ensureNoChildren slot;
returnOk True
odE));
y <- if word_of_nat (shiftR (shiftL (Suc 0) n - (if reset then 0 else idx)) (APIType_capBits (toEnum (unat newTypeW)) (unat userObjSizeW))) < nodeWindow then throwError (Fault_H.syscall_error.NotEnoughMemory (word_of_nat (shiftL (Suc 0) n - (if reset then 0 else idx)))) else returnOk ();
y <- if d \<and> \<not> isFrameType (toEnum (unat newTypeW)) \<and> toEnum (unat newTypeW) \<noteq> fromAPIType ArchTypes_H.apiobject_type.Untyped then throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)) else returnOk ();
returnOk (Invocations_H.untyped_invocation.Retype slot reset w (More_Word_Operations.alignUp (getFreeRef w (if reset then 0 else idx)) (APIType_capBits (toEnum (unat newTypeW)) (unat userObjSizeW))) (toEnum (unat newTypeW)) (unat userObjSizeW) slots d)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q28 s proof (prove)
goal:
No subgoals!