theory Untyped_AI

lemma dui_inv[wp]:
  "\<lbrace>P\<rbrace> decode_untyped_invocation label args slot (UntypedCap dev w n idx) cs \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decode_untyped_invocation_def whenE_def
                   split_def data_to_obj_type_def unlessE_def
              split del: if_split cong: if_cong) apply (rule hoare_pre) apply (simp split del: if_split
              | wp (once) mapME_x_inv_wp hoare_drop_imps const_on_failure_wp
              | assumption
              | simp add: lookup_target_slot_def
              | wpcw
              | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_untyped_invocation label args slot (UntypedCap dev w n idx) cs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE y <- if gen_invocation_type label = UntypedRetype then returnOk () else throwError IllegalOperation;
y <- if length args < 6 then throwError TruncatedMessage else returnOk ();
y <- if cs = [] then throwError TruncatedMessage else returnOk ();
new_type <- if data_to_nat (args ! 0) = 0 then returnOk Untyped else if data_to_nat (args ! 0) = Suc 0 then returnOk TCBObject else if data_to_nat (args ! 0) = 2 then returnOk EndpointObject else if data_to_nat (args ! 0) = 3 then returnOk NotificationObject else if data_to_nat (args ! 0) = 4 then returnOk CapTableObject else case arch_data_to_obj_type (data_to_nat (args ! 0) - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp);
y <- if data_to_nat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- if new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0 then throwError (InvalidArgument (Suc 0)) else returnOk ();
y <- if new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits then throwError (InvalidArgument (Suc 0)) else returnOk ();
node_cap <- if data_to_nat (args ! 3) = 0 then returnOk (cs ! 0) else doE node_slot <- lookup_target_slot (cs ! 0) (data_to_cptr (args ! 2)) (data_to_nat (args ! 3));
liftE (get_cap node_slot)
odE;
y <- if is_cnode_cap node_cap then returnOk () else throwError (FailedLookup False (MissingCapability (data_to_nat (args ! 3))));
y <- if 2 ^ bits_of node_cap - Suc 0 < data_to_nat (args ! 4) then throwError (RangeError 0 (2 ^ bits_of node_cap - 1)) else returnOk ();
y <- if data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5) then throwError (RangeError 1 retypeFanOutLimit) else returnOk ();
y <- if data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - data_to_nat (args ! 4) < data_to_nat (args ! 5) then throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - data_to_nat (args ! 4)))) else returnOk ();
y <- mapME_x ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [data_to_nat (args ! 4)..<data_to_nat (args ! 4) + data_to_nat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- ensure_no_children slot;
returnOk True
odE));
y <- if unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (UntypedCap dev w n idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) then throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (UntypedCap dev w n idx)))) else returnOk ();
y <- if dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped then throwError (InvalidArgument (Suc 0)) else returnOk ();
returnOk (Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (UntypedCap dev w n idx))) (obj_bits_api new_type (data_to_nat (args ! Suc 0)))) new_type (data_to_nat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [data_to_nat (args ! 4)..<data_to_nat (args ! 4) + data_to_nat (args ! 5)]) dev)
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q12\<rbrace> doE y <- if gen_invocation_type label = UntypedRetype then returnOk () else throwError IllegalOperation;
y <- if length args < 6 then throwError TruncatedMessage else returnOk ();
y <- if cs = [] then throwError TruncatedMessage else returnOk ();
new_type <- if data_to_nat (args ! 0) = 0 then returnOk Untyped else if data_to_nat (args ! 0) = Suc 0 then returnOk TCBObject else if data_to_nat (args ! 0) = 2 then returnOk EndpointObject else if data_to_nat (args ! 0) = 3 then returnOk NotificationObject else if data_to_nat (args ! 0) = 4 then returnOk CapTableObject else case arch_data_to_obj_type (data_to_nat (args ! 0) - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp);
y <- if data_to_nat (args ! Suc 0) < word_bits \<and> obj_bits_api new_type (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits then returnOk () else throwError (RangeError 0 (word_of_nat untyped_max_bits));
y <- if new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0 then throwError (InvalidArgument (Suc 0)) else returnOk ();
y <- if new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits then throwError (InvalidArgument (Suc 0)) else returnOk ();
node_cap <- if data_to_nat (args ! 3) = 0 then returnOk (cs ! 0) else doE node_slot <- lookup_target_slot (cs ! 0) (data_to_cptr (args ! 2)) (data_to_nat (args ! 3));
liftE (get_cap node_slot)
odE;
y <- if is_cnode_cap node_cap then returnOk () else throwError (FailedLookup False (MissingCapability (data_to_nat (args ! 3))));
y <- if 2 ^ bits_of node_cap - Suc 0 < data_to_nat (args ! 4) then throwError (RangeError 0 (2 ^ bits_of node_cap - 1)) else returnOk ();
y <- if data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5) then throwError (RangeError 1 retypeFanOutLimit) else returnOk ();
y <- if data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - data_to_nat (args ! 4) < data_to_nat (args ! 5) then throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - data_to_nat (args ! 4)))) else returnOk ();
y <- mapME_x ensure_empty (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [data_to_nat (args ! 4)..<data_to_nat (args ! 4) + data_to_nat (args ! 5)]);
reset <- liftE (const_on_failure False (doE y <- ensure_no_children slot;
returnOk True
odE));
y <- if unat (2 ^ n - word_of_nat (if reset then 0 else free_index_of (UntypedCap dev w n idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) then throwError (NotEnoughMemory (2 ^ n - word_of_nat (if reset then 0 else free_index_of (UntypedCap dev w n idx)))) else returnOk ();
y <- if dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped then throwError (InvalidArgument (Suc 0)) else returnOk ();
returnOk (Retype slot reset w (alignUp (get_free_ref w (if reset then 0 else free_index_of (UntypedCap dev w n idx))) (obj_bits_api new_type (data_to_nat (args ! Suc 0)))) new_type (data_to_nat (args ! Suc 0)) (map (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) [data_to_nat (args ! 4)..<data_to_nat (args ! 4) + data_to_nat (args ! 5)]) dev)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q12 s proof (prove)
goal:
No subgoals!