theory Syscall_DR

lemma transform_intent_untyped_cap_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx\<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>" including no_pre supply gen_invocation_type_eq[symmetric, simp] apply (clarsimp simp:Decode_A.decode_invocation_def) apply wp apply (case_labels "invocation_type label") 
      (* 46 subgoals *)
       apply (clarsimp simp:Decode_A.decode_untyped_invocation_def unlessE_def, wp)+ apply (clarsimp simp:transform_intent_def Decode_A.decode_untyped_invocation_def unlessE_def split del:if_split) apply (clarsimp simp:transform_intent_untyped_retype_def split del:if_split) apply (case_tac "args") apply (clarsimp,wp)[1] apply (clarsimp split:list.split_asm split del:if_split) apply (wp+)[5] apply (clarsimp simp: transform_type_eq_None split del:if_split split:option.splits) apply (wp|clarsimp simp:whenE_def|rule conjI)+ apply (clarsimp simp: Decode_A.decode_untyped_invocation_def unlessE_def split del:if_split,wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx\<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.UntypedCap dev w n idx\<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.UntypedCap dev w n idx\<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.UntypedCap dev w n idx\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME invocation.InvokeUntyped (Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (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.UntypedCap dev w n idx\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (46 subgoals):
 1. \<And>x2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = ArchInvocationLabel x2; x2 = ARMPDClean_Data\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = InvalidInvocation\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 46 subgoals... proof (prove)
goal (46 subgoals):
 1. \<And>x2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = ArchInvocationLabel x2; x2 = ARMPDClean_Data\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = InvalidInvocation\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 46 subgoals... proof (prove)
goal (44 subgoals):
 1. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 44 subgoals... proof (prove)
goal (44 subgoals):
 1. \<lbrakk>transform_intent_untyped_retype args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- if unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat (args ! 3) = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat (args ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat (args ! 5) = 0 \<or> unat retypeFanOutLimit < unat (args ! 5)) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - unat (args ! 4) < unat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat (args ! 4)))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat (args ! Suc 0)))) new_type (unat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 44 subgoals... proof (prove)
goal (44 subgoals):
 1. \<lbrakk>(case args of [] \<Rightarrow> None | [type] \<Rightarrow> None | [type, size_bits] \<Rightarrow> None | [type, size_bits, index] \<Rightarrow> None | [type, size_bits, index, depth] \<Rightarrow> None | [type, size_bits, index, depth, offset] \<Rightarrow> None | type # size_bits # index # depth # offset # window # x \<Rightarrow> case transform_type type of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x size_bits index depth offset window)) = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- if unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat (args ! 3) = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat (args ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat (args ! 5) = 0 \<or> unat retypeFanOutLimit < unat (args ! 5)) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - unat (args ! 4) < unat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat (args ! 4)))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat (args ! Suc 0)))) new_type (unat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 44 subgoals... proof (prove)
goal (45 subgoals):
 1. \<lbrakk>(case args of [] \<Rightarrow> None | [type] \<Rightarrow> None | [type, size_bits] \<Rightarrow> None | [type, size_bits, index] \<Rightarrow> None | [type, size_bits, index, depth] \<Rightarrow> None | [type, size_bits, index, depth, offset] \<Rightarrow> None | type # size_bits # index # depth # offset # window # x \<Rightarrow> case transform_type type of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x size_bits index depth offset window)) = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- if unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat (args ! 3) = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat (args ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat (args ! 5) = 0 \<or> unat retypeFanOutLimit < unat (args ! 5)) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - unat (args ! 4) < unat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat (args ! 4)))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat (args ! Suc 0)))) new_type (unat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a list. \<lbrakk>(case args of [] \<Rightarrow> None | [type] \<Rightarrow> None | [type, size_bits] \<Rightarrow> None | [type, size_bits, index] \<Rightarrow> None | [type, size_bits, index, depth] \<Rightarrow> None | [type, size_bits, index, depth, offset] \<Rightarrow> None | type # size_bits # index # depth # offset # window # x \<Rightarrow> case transform_type type of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x size_bits index depth offset window)) = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- if unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat (args ! 3) = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat (args ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat (args ! 5) = 0 \<or> unat retypeFanOutLimit < unat (args ! 5)) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - unat (args ! 4) < unat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat (args ! 4)))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat (args ! Suc 0)))) new_type (unat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 45 subgoals... proof (prove)
goal (44 subgoals):
 1. \<And>a list. \<lbrakk>(case args of [] \<Rightarrow> None | [type] \<Rightarrow> None | [type, size_bits] \<Rightarrow> None | [type, size_bits, index] \<Rightarrow> None | [type, size_bits, index, depth] \<Rightarrow> None | [type, size_bits, index, depth, offset] \<Rightarrow> None | type # size_bits # index # depth # offset # window # x \<Rightarrow> case transform_type type of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x size_bits index depth offset window)) = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- if unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat (args ! 3) = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat (args ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat (args ! 5) = 0 \<or> unat retypeFanOutLimit < unat (args ! 5)) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - unat (args ! 4) < unat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat (args ! 4)))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat (args ! Suc 0)))) new_type (unat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 44 subgoals... proof (prove)
goal (49 subgoals):
 1. \<And>a. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = [a]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a x21. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = [a, x21]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>a x21 x21a. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = [a, x21, x21a]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>a x21 x21a x21b. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = [a, x21, x21a, x21b]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>a x21 x21a x21b x21c. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; args = [a, x21, x21a, x21b, x21c]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>a x21 x21a x21b x21c x21d x22d. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; (case transform_type a of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x x21 x21a x21b x21c x21d)) = None; args = a # x21 # x21a # x21b # x21c # x21d # x22d\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type a;
y <- if unat x21 < word_bits \<and> obj_bits_api new_type (unat x21) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat x21 = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat x21 < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat x21b = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl ((a # x21 # x21a # x21b # x21c # x21d # x22d) ! 2)) (unat ((a # x21 # x21a # x21b # x21c # x21d # x22d) ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat ((a # x21 # x21a # x21b # x21c # x21d # x22d) ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat x21c) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat x21d = 0 \<or> unat retypeFanOutLimit < unat x21d) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat x21d = 0 \<or> 2 ^ bits_of node_cap - unat x21c < unat x21d) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat x21c))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat x21c..<unat x21c + unat x21d]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat x21)) < unat x21d) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat x21))) new_type (unat x21) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat x21c..<unat x21c + unat x21d]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 49 subgoals... proof (prove)
goal (44 subgoals):
 1. \<And>a x21 x21a x21b x21c x21d x22d. \<lbrakk>cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; (case transform_type a of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x x21 x21a x21b x21c x21d)) = None; args = a # x21 # x21a # x21b # x21c # x21d # x22d\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type a;
y <- if unat x21 < word_bits \<and> obj_bits_api new_type (unat x21) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- whenE (new_type = CapTableObject \<and> unat x21 = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = apiobject_type.Untyped \<and> unat x21 < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if unat x21b = 0 then returnOk (map fst excaps ! 0) else doE node_slot <- lookup_target_slot (map fst excaps ! 0) (to_bl ((a # x21 # x21a # x21b # x21c # x21d # x22d) ! 2)) (unat ((a # x21 # x21a # x21b # x21c # x21d # x22d) ! 3));
liftE $ CSpaceAcc_A.get_cap node_slot
odE;
y <- if Structures_A.is_cnode_cap node_cap then returnOk () else throwError $ FailedLookup False $ MissingCapability (unat ((a # x21 # x21a # x21b # x21c # x21d # x22d) ! 3));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < unat x21c) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (unat x21d = 0 \<or> unat retypeFanOutLimit < unat x21d) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (unat x21d = 0 \<or> 2 ^ bits_of node_cap - unat x21c < unat x21d) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - unat x21c))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat x21c..<unat x21c + unat x21d]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children slot;
returnOk True
odE));
y <- whenE (unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)) >> obj_bits_api new_type (unat x21)) < unat x21d) (throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> apiobject_type.Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (untyped_invocation.Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (cap.UntypedCap dev w n idx))) (obj_bits_api new_type (unat x21))) new_type (unat x21) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [unat x21c..<unat x21c + unat x21d]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 44 subgoals... proof (prove)
goal (44 subgoals):
 1. \<And>a x21 x21a x21b x21c x21d x22d. \<lbrakk>args = a # x21 # x21a # x21b # x21c # x21d # x22d; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel UntypedRetype; transform_type a = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
throwError (InvalidArgument 0)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 44 subgoals... proof (prove)
goal (43 subgoals):
 1. \<lbrakk>transform_intent (GenInvocationLabel TCBReadRegisters) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx; invocation_type label = GenInvocationLabel x1; x1 = TCBSuspend\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args slot (cap.UntypedCap dev w n idx) (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> invocation.InvokeUntyped\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 43 subgoals... proof (prove)
goal:
No subgoals!