theory Untyped_DR

lemma decode_untyped_label_not_match:
  "\<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk>
    \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e
             \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>" apply (case_tac "invocation_type label = GenInvocationLabel UntypedRetype") apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def)+ apply (clarsimp simp:transform_intent_untyped_retype_def split:option.splits list.splits) apply (simp add:Decode_A.decode_untyped_invocation_def unlessE_def gen_invocation_type_eq) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui; invocation_type label = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui; invocation_type label \<noteq> GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = map_option UntypedIntent (transform_intent_untyped_retype args); \<forall>ui. intent \<noteq> UntypedIntent ui; invocation_type label = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> (Structures_A.is_cnode_cap (e ! 0) \<longrightarrow> (unat (args ! 3) = 0 \<longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (e = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- unlessE (unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits) (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)));
y <- whenE (2 ^ bits_of (e ! 0) - Suc 0 < unat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of (e ! 0) - 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 (e ! 0) - unat (args ! 4) < unat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of (e ! 0) - unat (args ! 4)))));
y <- mapME_x CSpaceAcc_A.ensure_empty (map (Pair (obj_ref_of (e ! 0)) \<circ> nat_to_cref (bits_of (e ! 0))) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- CSpace_A.ensure_no_children ref;
returnOk True
odE));
y <- whenE (unat (2 ^ b - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev a b idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ b - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev a b 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 ref reset a (alignUp (get_free_ref a (if reset then 0 else free_index_of (cap.UntypedCap dev a b idx))) (obj_bits_api new_type (unat (args ! Suc 0)))) new_type (unat (args ! Suc 0)) (map (Pair (obj_ref_of (e ! 0)) \<circ> nat_to_cref (bits_of (e ! 0))) [unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)]) dev)
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>) \<and> (0 < unat (args ! 3) \<longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (e = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- unlessE (unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits) (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 <- doE node_slot <- CSpace_A.lookup_slot_for_cnode_op False (e ! 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 ref;
returnOk True
odE));
y <- whenE (unat (2 ^ b - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev a b idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ b - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev a b 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 ref reset a (alignUp (get_free_ref a (if reset then 0 else free_index_of (cap.UntypedCap dev a b 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>e. (=) s\<rbrace>)) \<and> (\<not> Structures_A.is_cnode_cap (e ! 0) \<longrightarrow> (unat (args ! 3) = 0 \<longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (e = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- unlessE (unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits) (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)));
throwError (FailedLookup False (MissingCapability 0))
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>) \<and> (0 < unat (args ! 3) \<longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (e = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- unlessE (unat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (unat (args ! Suc 0)) \<le> untyped_max_bits) (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 <- doE node_slot <- CSpace_A.lookup_slot_for_cnode_op False (e ! 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 ref;
returnOk True
odE));
y <- whenE (unat (2 ^ b - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev a b idx)) >> obj_bits_api new_type (unat (args ! Suc 0))) < unat (args ! 5)) (throwError (NotEnoughMemory (2 ^ b - word_of_nat (if reset then 0 else free_index_of (cap.UntypedCap dev a b 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 ref reset a (alignUp (get_free_ref a (if reset then 0 else free_index_of (cap.UntypedCap dev a b 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>e. (=) s\<rbrace>))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui; invocation_type label \<noteq> GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui; invocation_type label \<noteq> GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui; gen_invocation_type label \<noteq> UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal:
No subgoals!