theory Decode_IF

lemma decode_untyped_invocation_rev:
  "reads_equiv_valid_inv A aag (pas_refined aag and (K (cap = UntypedCap dev bs sz idx \<and>
                                                        is_subject aag (fst slot) \<and>
                                                        (\<forall>c\<in>set excaps. pas_cap_cur_auth aag c))))
                         (decode_untyped_invocation label args slot cap excaps)" unfolding decode_untyped_invocation_def fun_app_def apply (rule gen_asm_ev) apply (simp add: unlessE_def[symmetric] unlessE_whenE split del: if_split) apply (wp (once) whenE_throwError_wp
         | wp mapME_x_ev' ensure_empty_rev get_cap_rev
              lookup_slot_for_cnode_op_rev
              ensure_no_children_rev
              const_on_failure_ev mapME_x_inv_wp
         | assumption
         | simp
         | rule validE_R_validE | strengthen aag_can_read_self)+ apply (rule hoare_strengthen_post[
                                  where Q="\<lambda> rv s. (is_cnode_cap rv
                                                         \<longrightarrow> is_subject aag (obj_ref_of rv))
                                                 \<and> pas_refined aag s"]) apply (wp (once) whenE_throwError_wp
                          | wp get_cap_ret_is_subject data_to_obj_type_rev data_to_obj_type_inv
                          | simp
                          | wp (once) hoare_drop_imps)+ apply (clarify, drule_tac x="excaps ! 0" in bspec, fastforce intro: bang_0_in_set) apply (auto dest: is_cnode_into_is_subject elim: prop_of_obj_ref_of_cnode_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag))) (decode_untyped_invocation label args slot cap excaps) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag))) (doE unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
whenE (length args < 6) (throwError TruncatedMessage);
whenE (length excaps = 0) (throwError TruncatedMessage);
root_cap <- returnOk (excaps ! 0);
new_type <- data_to_obj_type (args ! 0);
user_obj_size <- returnOk (data_to_nat (args ! 1));
object_size <- returnOk (obj_bits_api new_type user_obj_size);
unlessE (user_obj_size < word_bits \<and> object_size \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits)));
whenE (new_type = CapTableObject \<and> user_obj_size = 0) (throwError (InvalidArgument 1));
whenE (new_type = Untyped \<and> user_obj_size < untyped_min_bits) (throwError (InvalidArgument 1));
node_index <- returnOk (data_to_cptr (args ! 2));
node_depth <- returnOk (data_to_nat (args ! 3));
node_cap <- if node_depth = 0 then returnOk root_cap else doE node_slot <- lookup_target_slot root_cap node_index node_depth;
liftE (get_cap node_slot)
odE;
if is_cnode_cap node_cap then returnOk () else throwError (FailedLookup False (MissingCapability node_depth));
node_offset <- returnOk (data_to_nat (args ! 4));
node_window <- returnOk (data_to_nat (args ! 5));
radix_bits <- returnOk (bits_of node_cap);
node_size <- returnOk (2 ^ radix_bits);
whenE (node_offset < 0 \<or> node_size - 1 < node_offset) (throwError (RangeError 0 (word_of_nat (node_size - 1))));
whenE (node_window < 1 \<or> unat retypeFanOutLimit < node_window) (throwError (RangeError 1 retypeFanOutLimit));
whenE (node_window < 1 \<or> node_size - node_offset < node_window) (throwError (RangeError 1 (word_of_nat (node_size - node_offset))));
oref <- returnOk (obj_ref_of node_cap);
offsets <- returnOk (map (nat_to_cref radix_bits) [node_offset..<node_offset + node_window]);
slots <- returnOk (map (Pair oref) offsets);
mapME_x ensure_empty slots;
reset <- liftE (const_on_failure False (doE ensure_no_children slot;
returnOk True
odE));
free_index <- returnOk (if reset then 0 else free_index_of cap);
free_ref <- returnOk (get_free_ref (obj_ref_of cap) free_index);
aligned_free_ref <- returnOk (alignUp free_ref object_size);
untyped_free_bytes <- returnOk (obj_size cap - word_of_nat free_index);
max_count <- returnOk (untyped_free_bytes >> object_size);
whenE (unat max_count < node_window) (throwError (NotEnoughMemory untyped_free_bytes));
not_frame <- returnOk (\<not> is_frame_type new_type);
(ptr, is_device) <- case cap of UntypedCap dev p n f \<Rightarrow> returnOk (p, dev) | _ \<Rightarrow> fail;
whenE (is_device \<and> not_frame \<and> new_type \<noteq> Untyped) (throwError (InvalidArgument 1));
returnOk (Retype slot reset ptr aligned_free_ref new_type user_obj_size slots is_device)
odE) proof (prove)
goal (1 subgoal):
 1. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (pas_refined aag) (doE unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
whenE (length args < 6) (throwError TruncatedMessage);
whenE (length excaps = 0) (throwError TruncatedMessage);
root_cap <- returnOk (excaps ! 0);
new_type <- data_to_obj_type (args ! 0);
user_obj_size <- returnOk (data_to_nat (args ! 1));
object_size <- returnOk (obj_bits_api new_type user_obj_size);
unlessE (user_obj_size < word_bits \<and> object_size \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits)));
whenE (new_type = CapTableObject \<and> user_obj_size = 0) (throwError (InvalidArgument 1));
whenE (new_type = Untyped \<and> user_obj_size < untyped_min_bits) (throwError (InvalidArgument 1));
node_index <- returnOk (data_to_cptr (args ! 2));
node_depth <- returnOk (data_to_nat (args ! 3));
node_cap <- if node_depth = 0 then returnOk root_cap else doE node_slot <- lookup_target_slot root_cap node_index node_depth;
liftE (get_cap node_slot)
odE;
if is_cnode_cap node_cap then returnOk () else throwError (FailedLookup False (MissingCapability node_depth));
node_offset <- returnOk (data_to_nat (args ! 4));
node_window <- returnOk (data_to_nat (args ! 5));
radix_bits <- returnOk (bits_of node_cap);
node_size <- returnOk (2 ^ radix_bits);
whenE (node_offset < 0 \<or> node_size - 1 < node_offset) (throwError (RangeError 0 (word_of_nat (node_size - 1))));
whenE (node_window < 1 \<or> unat retypeFanOutLimit < node_window) (throwError (RangeError 1 retypeFanOutLimit));
whenE (node_window < 1 \<or> node_size - node_offset < node_window) (throwError (RangeError 1 (word_of_nat (node_size - node_offset))));
oref <- returnOk (obj_ref_of node_cap);
offsets <- returnOk (map (nat_to_cref radix_bits) [node_offset..<node_offset + node_window]);
slots <- returnOk (map (Pair oref) offsets);
mapME_x ensure_empty slots;
reset <- liftE (const_on_failure False (doE ensure_no_children slot;
returnOk True
odE));
free_index <- returnOk (if reset then 0 else free_index_of cap);
free_ref <- returnOk (get_free_ref (obj_ref_of cap) free_index);
aligned_free_ref <- returnOk (alignUp free_ref object_size);
untyped_free_bytes <- returnOk (obj_size cap - word_of_nat free_index);
max_count <- returnOk (untyped_free_bytes >> object_size);
whenE (unat max_count < node_window) (throwError (NotEnoughMemory untyped_free_bytes));
not_frame <- returnOk (\<not> is_frame_type new_type);
(ptr, is_device) <- case cap of UntypedCap dev p n f \<Rightarrow> returnOk (p, dev) | _ \<Rightarrow> fail;
whenE (is_device \<and> not_frame \<and> new_type \<noteq> Untyped) (throwError (InvalidArgument 1));
returnOk (Retype slot reset ptr aligned_free_ref new_type user_obj_size slots is_device)
odE) proof (prove)
goal (1 subgoal):
 1. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (pas_refined aag) (doE y <- whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- whenE (data_to_nat (args ! Suc 0) < word_bits \<longrightarrow> \<not> obj_bits_api new_type (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits)));
y <- whenE (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0)));
y <- whenE (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0)));
node_cap <- if data_to_nat (args ! 3) = 0 then returnOk (excaps ! 0) else doE node_slot <- lookup_target_slot (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3));
liftE (get_cap node_slot)
odE;
y <- whenE (\<not> is_cnode_cap node_cap) (throwError (FailedLookup False (MissingCapability (data_to_nat (args ! 3)))));
y <- whenE (2 ^ bits_of node_cap - Suc 0 < data_to_nat (args ! 4)) (throwError (RangeError 0 (2 ^ bits_of node_cap - 1)));
y <- whenE (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) (throwError (RangeError 1 retypeFanOutLimit));
y <- whenE (data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of node_cap - data_to_nat (args ! 4) < data_to_nat (args ! 5)) (throwError (RangeError 1 (word_of_nat (2 ^ bits_of node_cap - data_to_nat (args ! 4)))));
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 <- whenE (unat (2 ^ sz - word_of_nat (if reset then 0 else free_index_of cap) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5)) (throwError (NotEnoughMemory (2 ^ sz - word_of_nat (if reset then 0 else free_index_of cap))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (Retype slot reset bs (alignUp (get_free_ref bs (if reset then 0 else free_index_of cap)) (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) proof (prove)
goal (17 subgoals):
 1. \<And>rvc node_slot. \<lbrakk>cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag); 0 < data_to_nat (args ! 3)\<rbrakk> \<Longrightarrow> \<lbrace>?B243 () () () rvc () () () node_slot\<rbrace> get_cap node_slot \<lbrace>\<lambda>rvg s. is_cnode_cap rvg \<longrightarrow> \<not> 2 ^ bits_of rvg - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> 0 < data_to_nat (args ! 5) \<and> \<not> unat retypeFanOutLimit < data_to_nat (args ! 5) \<longrightarrow> \<not> 2 ^ bits_of rvg - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> ((\<exists>x\<ge>data_to_nat (args ! 4). x < data_to_nat (args ! 4) + data_to_nat (args ! 5)) \<longrightarrow> is_subject aag (obj_ref_of rvg)) \<and> pas_refined aag s\<rbrace>
 2. \<And>rv rva rvb rvc rvd rve rvf. \<lbrakk>cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag); data_to_nat (args ! 3) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R237 rv rva rvb rvc rvd rve rvf\<rbrace> lookup_target_slot (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>?B243 rv rva rvb rvc rvd rve rvf\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'20 rv rva rvb rvc rvd rve) (whenE (rvc = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))))
 4. \<And>rv rva rvb rvc rvd rve. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''20 rv rva rvb rvc rvd rve\<rbrace> whenE (rvc = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>rvf s. ((data_to_nat (args ! 3) = 0 \<longrightarrow> True) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> (data_to_nat (args ! 3) \<noteq> 0 \<and> data_to_nat (args ! 3) \<le> word_bits \<longrightarrow> pas_refined aag s \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> is_subject aag (obj_ref_of (excaps ! 0)))) \<and> (pas_refined aag and K (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))) s)) \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> (\<not> is_cnode_cap (excaps ! 0) \<longrightarrow> True) \<and> (\<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> (2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> True) \<and> (\<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> (data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of (excaps ! 0) - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> (data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of (excaps ! 0) - data_to_nat (args ! 4) < data_to_nat (args ! 5)) \<longrightarrow> K (\<forall>x\<in>set (map (Pair (obj_ref_of (excaps ! 0)) \<circ> nat_to_cref (bits_of (excaps ! 0))) [data_to_nat (args ! 4)..<data_to_nat (args ! 4) + data_to_nat (args ! 5)]). is_subject aag (fst x)) s \<and> pas_refined aag s \<and> K (is_subject aag (fst slot)) s \<and> True \<and> (unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped \<longrightarrow> True) \<and> (\<not> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped) \<longrightarrow> True)) \<and> True \<and> (unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped \<longrightarrow> True) \<and> (\<not> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped) \<longrightarrow> True))))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R237 rv rva rvb rvc rvd rve rvf s)\<rbrace>, -
 5. \<And>rv rva rvb rvc rvd. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'17 rv rva rvb rvc rvd) (whenE (rvc = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))))
 6. \<And>rv rva rvb rvc rvd. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''17 rv rva rvb rvc rvd\<rbrace> whenE (rvc = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>rve s. ?P'20 rv rva rvb rvc rvd rve s \<and> ?P''20 rv rva rvb rvc rvd rve s\<rbrace>, -
 7. \<And>rv rva rvb rvc. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'14 rv rva rvb rvc) (whenE (data_to_nat (args ! Suc 0) < word_bits \<longrightarrow> \<not> obj_bits_api rvc (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits))))
 8. \<And>rv rva rvb rvc. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''14 rv rva rvb rvc\<rbrace> whenE (data_to_nat (args ! Suc 0) < word_bits \<longrightarrow> \<not> obj_bits_api rvc (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits))) \<lbrace>\<lambda>rvd s. ?P'17 rv rva rvb rvc rvd s \<and> ?P''17 rv rva rvb rvc rvd s\<rbrace>, -
 9. \<And>rv rva rvb. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'11 rv rva rvb) (data_to_obj_type (args ! 0))
 10. \<And>rv rva rvb. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''11 rv rva rvb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>\<lambda>rvc s. ?P'14 rv rva rvb rvc s \<and> ?P''14 rv rva rvb rvc s\<rbrace>, -
A total of 17 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rvc node_slot. \<lbrakk>cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag); 0 < data_to_nat (args ! 3)\<rbrakk> \<Longrightarrow> \<lbrace>?B243 () () () rvc () () () node_slot\<rbrace> get_cap node_slot \<lbrace>\<lambda>rv s. (is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and> pas_refined aag s\<rbrace>
 2. \<And>rvc node_slot rv s. \<lbrakk>cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag); 0 < data_to_nat (args ! 3); (is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> is_cnode_cap rv \<longrightarrow> \<not> 2 ^ bits_of rv - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> 0 < data_to_nat (args ! 5) \<and> \<not> unat retypeFanOutLimit < data_to_nat (args ! 5) \<longrightarrow> \<not> 2 ^ bits_of rv - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> ((\<exists>x\<ge>data_to_nat (args ! 4). x < data_to_nat (args ! 4) + data_to_nat (args ! 5)) \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and> pas_refined aag s
 3. \<And>rv rva rvb rvc rvd rve rvf. \<lbrakk>cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag); data_to_nat (args ! 3) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R237 rv rva rvb rvc rvd rve rvf\<rbrace> lookup_target_slot (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>?B243 rv rva rvb rvc rvd rve rvf\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'20 rv rva rvb rvc rvd rve) (whenE (rvc = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))))
 5. \<And>rv rva rvb rvc rvd rve. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''20 rv rva rvb rvc rvd rve\<rbrace> whenE (rvc = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>rvf s. ((data_to_nat (args ! 3) = 0 \<longrightarrow> True) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> (data_to_nat (args ! 3) \<noteq> 0 \<and> data_to_nat (args ! 3) \<le> word_bits \<longrightarrow> pas_refined aag s \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> is_subject aag (obj_ref_of (excaps ! 0)))) \<and> (pas_refined aag and K (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))) s)) \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> (\<not> is_cnode_cap (excaps ! 0) \<longrightarrow> True) \<and> (\<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> (2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> True) \<and> (\<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> (data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of (excaps ! 0) - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> (data_to_nat (args ! 5) = 0 \<or> 2 ^ bits_of (excaps ! 0) - data_to_nat (args ! 4) < data_to_nat (args ! 5)) \<longrightarrow> K (\<forall>x\<in>set (map (Pair (obj_ref_of (excaps ! 0)) \<circ> nat_to_cref (bits_of (excaps ! 0))) [data_to_nat (args ! 4)..<data_to_nat (args ! 4) + data_to_nat (args ! 5)]). is_subject aag (fst x)) s \<and> pas_refined aag s \<and> K (is_subject aag (fst slot)) s \<and> True \<and> (unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped \<longrightarrow> True) \<and> (\<not> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped) \<longrightarrow> True)) \<and> True \<and> (unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> True) \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of cap) >> obj_bits_api rvc (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped \<longrightarrow> True) \<and> (\<not> (dev \<and> \<not> is_frame_type rvc \<and> rvc \<noteq> Untyped) \<longrightarrow> True))))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R237 rv rva rvb rvc rvd rve rvf s)\<rbrace>, -
 6. \<And>rv rva rvb rvc rvd. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'17 rv rva rvb rvc rvd) (whenE (rvc = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))))
 7. \<And>rv rva rvb rvc rvd. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''17 rv rva rvb rvc rvd\<rbrace> whenE (rvc = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>rve s. ?P'20 rv rva rvb rvc rvd rve s \<and> ?P''20 rv rva rvb rvc rvd rve s\<rbrace>, -
 8. \<And>rv rva rvb rvc. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'14 rv rva rvb rvc) (whenE (data_to_nat (args ! Suc 0) < word_bits \<longrightarrow> \<not> obj_bits_api rvc (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits))))
 9. \<And>rv rva rvb rvc. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> \<lbrace>?P''14 rv rva rvb rvc\<rbrace> whenE (data_to_nat (args ! Suc 0) < word_bits \<longrightarrow> \<not> obj_bits_api rvc (data_to_nat (args ! Suc 0)) \<le> untyped_max_bits) (throwError (RangeError 0 (word_of_nat untyped_max_bits))) \<lbrace>\<lambda>rvd s. ?P'17 rv rva rvb rvc rvd s \<and> ?P''17 rv rva rvb rvc rvd s\<rbrace>, -
 10. \<And>rv rva rvb. cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<Longrightarrow> reads_equiv_valid_inv A aag (?P'11 rv rva rvb) (data_to_obj_type (args ! 0))
A total of 18 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = UntypedCap dev bs sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag); pas_refined aag s\<rbrakk> \<Longrightarrow> gen_invocation_type label = UntypedRetype \<longrightarrow> \<not> length args < 6 \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (0 < data_to_nat (args ! 3) \<longrightarrow> (data_to_nat (args ! 3) \<le> word_bits \<longrightarrow> is_cnode_cap (excaps ! 0) \<longrightarrow> is_subject aag (obj_ref_of (excaps ! 0))) \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))) \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> 0 < data_to_nat (args ! 5) \<and> \<not> unat retypeFanOutLimit < data_to_nat (args ! 5) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> (\<exists>x\<ge>data_to_nat (args ! 4). x < data_to_nat (args ! 4) + data_to_nat (args ! 5)) \<longrightarrow> is_subject aag (obj_ref_of (excaps ! 0))) \<and> (0 < data_to_nat (args ! 3) \<longrightarrow> is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; cap = UntypedCap dev bs sz idx; is_subject aag (fst slot); gen_invocation_type label = UntypedRetype; \<not> length args < 6; excaps \<noteq> []; pas_cap_cur_auth aag (excaps ! 0)\<rbrakk> \<Longrightarrow> (0 < data_to_nat (args ! 3) \<longrightarrow> (data_to_nat (args ! 3) \<le> word_bits \<longrightarrow> is_cnode_cap (excaps ! 0) \<longrightarrow> is_subject aag (obj_ref_of (excaps ! 0))) \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))) \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> 0 < data_to_nat (args ! 5) \<and> \<not> unat retypeFanOutLimit < data_to_nat (args ! 5) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> (\<exists>x\<ge>data_to_nat (args ! 4). x < data_to_nat (args ! 4) + data_to_nat (args ! 5)) \<longrightarrow> is_subject aag (obj_ref_of (excaps ! 0))) \<and> (0 < data_to_nat (args ! 3) \<longrightarrow> is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) proof (prove)
goal:
No subgoals!