theory Retype_AC

lemma decode_untyped_invocation_authorised:
  "\<lbrace>invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot
         and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap
                  \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s))
         and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)
         and K (cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and>
                (\<forall>c \<in> set excaps. pas_cap_cur_auth aag c) \<and>
                (\<forall> ref \<in> untyped_range cap. is_subject aag ref))\<rbrace>
   decode_untyped_invocation label args slot cap excaps
   \<lbrace>\<lambda>rv _. authorised_untyped_inv aag rv\<rbrace>,-" apply (rule hoare_gen_asmE) apply (rule hoare_pre) apply (strengthen authorised_untyped_invI[mk_strg I]) apply (wp dui_inv_wf | simp)+ apply (clarsimp simp: decode_untyped_invocation_def split_def
                         authorised_untyped_inv'_def
                   split del: if_split split: untyped_invocation.splits) 
   (* need to hoist the is_cnode_cap assumption into postcondition later on *)
    apply (simp add: unlessE_def[symmetric] whenE_def[symmetric] unlessE_whenE split del: if_split) apply (wp whenE_throwError_wp  hoare_vcg_all_lift mapME_x_inv_wp
          | simp split: untyped_invocation.splits
          | (auto)[1])+ apply (rule_tac Q="\<lambda>node_cap s.
                              (is_cnode_cap node_cap \<longrightarrow> is_subject aag (obj_ref_of node_cap)) \<and>
                              is_subject aag (fst slot) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and>
                              (\<forall>cap. cte_wp_at ((=) cap) slot s
                                     \<longrightarrow> (\<forall>ref \<in> ptr_range base (bits_of cap). is_subject aag ref))"
                        in hoare_strengthen_post) apply (wp get_cap_inv get_cap_ret_is_subject) apply (fastforce simp: nonzero_data_to_nat_simp) apply clarsimp apply (wp lookup_slot_for_cnode_op_authorised
                    lookup_slot_for_cnode_op_inv whenE_throwError_wp)+ apply (rule hoare_drop_imps)+ apply clarsimp apply (rule_tac Q'=
               "\<lambda>rv s. rv \<noteq> ArchObject ASIDPoolObj \<and>
                       (\<forall>cap. cte_wp_at ((=) cap) slot s
                              \<longrightarrow> (\<forall>ref \<in> ptr_range base (bits_of cap). is_subject aag ref)) \<and>
                       is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and>
                       sz < word_bits \<and> is_aligned base sz \<and>
                       (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))"
                   in hoare_post_imp_R) apply (wp data_to_obj_type_ret_not_asid_pool data_to_obj_type_inv2) apply (case_tac "excaps ! 0", simp_all, fastforce simp: nonzero_data_to_nat_simp)[1] apply (wp whenE_throwError_wp)+ apply (auto dest!: bang_0_in_set dest: cte_wp_at_eqD2
               simp: valid_cap_def cap_aligned_def obj_ref_of_def is_cap_simps
                     cap_auth_conferred_def pas_refined_all_auth_is_owns bits_of_UntypedCap
                     aag_cap_auth_def ptr_range_def le_trans[OF word_size_bits_untyped_min_bits]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x) and K (cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref))\<rbrace> decode_untyped_invocation label args slot cap excaps \<lbrace>\<lambda>rv _. authorised_untyped_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref) \<Longrightarrow> \<lbrace>invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)\<rbrace> decode_untyped_invocation label args slot cap excaps \<lbrace>\<lambda>rv _. authorised_untyped_inv aag rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref) \<Longrightarrow> \<lbrace>?P'2\<rbrace> decode_untyped_invocation label args slot cap excaps \<lbrace>\<lambda>rv _. authorised_untyped_inv aag rv\<rbrace>, -
 2. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref) \<Longrightarrow> \<lbrace>?P'2\<rbrace> decode_untyped_invocation label args slot cap excaps \<lbrace>\<lambda>r s. valid_untyped_inv r (?s8 r s) \<and> pas_refined aag (?s8 r s) \<and> authorised_untyped_inv' aag r\<rbrace>, -
 2. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref) \<Longrightarrow> \<lbrace>?P'12\<rbrace> decode_untyped_invocation label args slot (UntypedCap dev base sz idx) excaps \<lbrace>\<lambda>rv s. authorised_untyped_inv' aag rv\<rbrace>, -
 2. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> doE y <- unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- unlessE (data_to_nat (args ! Suc 0) < word_bits \<and> 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_slot_for_cnode_op False (excaps ! 0) (to_bl (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 <- 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 (UntypedCap dev base sz idx)) >> 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 (UntypedCap dev base sz idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (Retype slot reset base (alignUp (get_free_ref base (if reset then 0 else free_index_of (UntypedCap dev base sz 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 s. case rv of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))\<rbrace>, -
 2. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> doE y <- unlessE (gen_invocation_type label = UntypedRetype) (throwError IllegalOperation);
y <- whenE (length args < 6) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
new_type <- data_to_obj_type (args ! 0);
y <- unlessE (data_to_nat (args ! Suc 0) < word_bits \<and> 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_slot_for_cnode_op False (excaps ! 0) (to_bl (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 <- 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 (UntypedCap dev base sz idx)) >> 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 (UntypedCap dev base sz idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (Retype slot reset base (alignUp (get_free_ref base (if reset then 0 else free_index_of (UntypedCap dev base sz 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 s. case rv of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))\<rbrace>, -
 2. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> 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_slot_for_cnode_op False (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 (UntypedCap dev base sz idx)) >> 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 (UntypedCap dev base sz idx)))));
y <- whenE (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) (throwError (InvalidArgument (Suc 0)));
returnOk (Retype slot reset base (alignUp (get_free_ref base (if reset then 0 else free_index_of (UntypedCap dev base sz 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 s. case rv of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))\<rbrace>, -
 2. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (10 subgoals):
 1. \<And>new_type a b. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; 0 < data_to_nat (args ! 3)\<rbrakk> \<Longrightarrow> \<lbrace>?B94 () () () new_type () () () (a, b)\<rbrace> get_cap (a, b) \<lbrace>\<lambda>node_cap s. is_cnode_cap node_cap \<longrightarrow> \<not> 2 ^ bits_of node_cap - 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 node_cap - data_to_nat (args ! 4) < data_to_nat (args ! 5) \<longrightarrow> (\<not> unat (2 ^ sz - word_of_nat (free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type new_type \<or> new_type = Untyped) \<longrightarrow> 0 < args ! 5 \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> ((\<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 node_cap))) \<and> (\<not> unat (2 ^ sz >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type new_type \<or> new_type = Untyped) \<longrightarrow> 0 < args ! 5 \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> ((\<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 node_cap)))\<rbrace>
 2. \<And>y ya yb new_type yc yd ye. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; data_to_nat (args ! 3) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R92 y ya yb new_type yc yd ye\<rbrace> lookup_slot_for_cnode_op False (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>?B94 y ya yb new_type yc yd ye\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y ya yb new_type yc yd. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B30 y ya yb new_type yc yd\<rbrace> whenE (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>ye s. True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R92 y ya yb new_type yc yd ye s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya yb new_type yc. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B29 y ya yb new_type yc\<rbrace> whenE (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>?B30 y ya yb new_type yc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y ya yb new_type. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B28 y ya yb new_type\<rbrace> 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))) \<lbrace>?B29 y ya yb new_type\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B27 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>?B28 y ya yb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>?B27 y ya\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (11 subgoals):
 1. \<And>new_type a b. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; 0 < data_to_nat (args ! 3)\<rbrakk> \<Longrightarrow> \<lbrace>?B94 () () () new_type () () () (a, b)\<rbrace> get_cap (a, b) \<lbrace>\<lambda>node_cap s. (is_cnode_cap node_cap \<longrightarrow> is_subject aag (obj_ref_of node_cap)) \<and> is_subject aag (fst slot) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))\<rbrace>
 2. \<And>new_type a b rv s. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; 0 < data_to_nat (args ! 3); (is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and> is_subject aag (fst slot) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))\<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> (\<not> unat (2 ^ sz - word_of_nat (free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type new_type \<or> new_type = Untyped) \<longrightarrow> 0 < args ! 5 \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> (\<not> unat (2 ^ sz >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type new_type \<or> new_type = Untyped) \<longrightarrow> 0 < args ! 5 \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> ((\<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)))
 3. \<And>y ya yb new_type yc yd ye. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; data_to_nat (args ! 3) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R92 y ya yb new_type yc yd ye\<rbrace> lookup_slot_for_cnode_op False (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>?B94 y ya yb new_type yc yd ye\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya yb new_type yc yd. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B30 y ya yb new_type yc yd\<rbrace> whenE (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>ye s. True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R92 y ya yb new_type yc yd ye s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y ya yb new_type yc. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B29 y ya yb new_type yc\<rbrace> whenE (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>?B30 y ya yb new_type yc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya yb new_type. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B28 y ya yb new_type\<rbrace> 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))) \<lbrace>?B29 y ya yb new_type\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B27 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>?B28 y ya yb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>?B27 y ya\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>new_type a b rv s. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; 0 < data_to_nat (args ! 3); (is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and> is_subject aag (fst slot) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))\<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> (\<not> unat (2 ^ sz - word_of_nat (free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type new_type \<or> new_type = Untyped) \<longrightarrow> 0 < args ! 5 \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> (\<not> unat (2 ^ sz >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type new_type \<or> new_type = Untyped) \<longrightarrow> 0 < args ! 5 \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> ((\<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)))
 2. \<And>y ya yb new_type yc yd ye. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; data_to_nat (args ! 3) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R92 y ya yb new_type yc yd ye\<rbrace> lookup_slot_for_cnode_op False (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>\<lambda>x8 x9. (pas_refined aag and K (is_subject aag (fst x8))) x9 \<and> is_subject aag (fst slot) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot x9 \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y ya yb new_type yc yd. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B30 y ya yb new_type yc yd\<rbrace> whenE (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>ye s. True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R92 y ya yb new_type yc yd ye s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya yb new_type yc. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B29 y ya yb new_type yc\<rbrace> whenE (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>?B30 y ya yb new_type yc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y ya yb new_type. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B28 y ya yb new_type\<rbrace> 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))) \<lbrace>?B29 y ya yb new_type\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B27 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>?B28 y ya yb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>?B27 y ya\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (9 subgoals):
 1. \<And>y ya yb new_type yc yd ye. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; data_to_nat (args ! 3) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R92 y ya yb new_type yc yd ye\<rbrace> lookup_slot_for_cnode_op False (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>\<lambda>x8 x9. (pas_refined aag and K (is_subject aag (fst x8))) x9 \<and> is_subject aag (fst slot) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot x9 \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>y ya yb new_type yc yd. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B30 y ya yb new_type yc yd\<rbrace> whenE (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>ye s. True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R92 y ya yb new_type yc yd ye s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y ya yb new_type yc. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B29 y ya yb new_type yc\<rbrace> whenE (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>?B30 y ya yb new_type yc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya yb new_type. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B28 y ya yb new_type\<rbrace> 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))) \<lbrace>?B29 y ya yb new_type\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B27 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>?B28 y ya yb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>?B27 y ya\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (9 subgoals):
 1. \<And>new_type. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; 0 < data_to_nat (args ! 3)\<rbrakk> \<Longrightarrow> \<lbrace>?R92 () () () new_type () () ()\<rbrace> lookup_slot_for_cnode_op False (excaps ! 0) (to_bl (args ! 2)) (data_to_nat (args ! 3)) \<lbrace>\<lambda>x8 x9. pas_refined aag x9 \<and> is_subject aag (fst x8) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot x9 \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>y ya yb new_type yc yd. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B30 y ya yb new_type yc yd\<rbrace> whenE (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) (throwError (InvalidArgument (Suc 0))) \<lbrace>\<lambda>ye s. True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> ?R92 y ya yb new_type yc yd ye s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y ya yb new_type yc. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B29 y ya yb new_type yc\<rbrace> whenE (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) (throwError (InvalidArgument (Suc 0))) \<lbrace>?B30 y ya yb new_type yc\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya yb new_type. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B28 y ya yb new_type\<rbrace> 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))) \<lbrace>?B29 y ya yb new_type\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B27 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>?B28 y ya yb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>?B27 y ya\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'207 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>\<lambda>new_type s. \<not> (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) \<longrightarrow> \<not> (new_type = CapTableObject \<and> data_to_nat (args ! Suc 0) = 0) \<longrightarrow> \<not> (new_type = Untyped \<and> data_to_nat (args ! Suc 0) < untyped_min_bits) \<longrightarrow> True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api new_type (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type new_type \<and> new_type \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz 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 (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> True \<and> pas_refined aag s \<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> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)))\<rbrace>, -
 2. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>\<lambda>yb s. True \<and> ?P'207 y ya yb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'207 y ya yb\<rbrace> data_to_obj_type (args ! 0) \<lbrace>\<lambda>rv s. True \<and> (data_to_nat (args ! 3) = 0 \<longrightarrow> \<not> \<not> is_cnode_cap (excaps ! 0) \<longrightarrow> \<not> 2 ^ bits_of (excaps ! 0) - Suc 0 < data_to_nat (args ! 4) \<longrightarrow> \<not> (data_to_nat (args ! 5) = 0 \<or> unat retypeFanOutLimit < data_to_nat (args ! 5)) \<longrightarrow> \<not> (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> unat (2 ^ sz - word_of_nat (if False then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type rv \<and> rv \<noteq> Untyped) \<longrightarrow> (case Retype slot False base (alignUp (get_free_ref base (if False then 0 else free_index_of (UntypedCap dev base sz idx))) (obj_bits_api rv (data_to_nat (args ! Suc 0)))) rv (data_to_nat (args ! Suc 0)) (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x)))) \<and> True \<and> (\<not> unat (2 ^ sz - word_of_nat (if True then 0 else free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> \<not> (dev \<and> \<not> is_frame_type rv \<and> rv \<noteq> Untyped) \<longrightarrow> (case Retype slot True base (alignUp (get_free_ref base (if True then 0 else free_index_of (UntypedCap dev base sz idx))) (obj_bits_api rv (data_to_nat (args ! Suc 0)))) rv (data_to_nat (args ! Suc 0)) (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)]) dev of Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> is_subject aag (fst src_slot) \<and> 0 < word_of_nat (length slots) \<and> new_type \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set slots. is_subject aag (fst x))))) \<and> (data_to_nat (args ! 3) \<noteq> 0 \<longrightarrow> True \<and> pas_refined aag s \<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> rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)))\<rbrace>, -
 2. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>\<lambda>yb s. True \<and> ?P'207 y ya yb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'207 () () ()\<rbrace> data_to_obj_type (args ! 0) \<lbrace>\<lambda>rv s. (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> (\<not> unat (2 ^ sz - word_of_nat (free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type rv \<or> rv = Untyped) \<longrightarrow> 0 < args ! 5 \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> (\<not> unat (2 ^ sz >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type rv \<or> rv = Untyped) \<longrightarrow> 0 < args ! 5 \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> pas_refined aag s \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)))\<rbrace>, -
 2. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>\<lambda>yb s. True \<and> ?P'207 y ya yb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'207 () () ()\<rbrace> data_to_obj_type (args ! 0) \<lbrace>\<lambda>rv s. rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and> sz < word_bits \<and> is_aligned base sz \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))\<rbrace>, -
 2. \<And>rv s. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and> sz < word_bits \<and> is_aligned base sz \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))\<rbrakk> \<Longrightarrow> (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> (\<not> unat (2 ^ sz - word_of_nat (free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type rv \<or> rv = Untyped) \<longrightarrow> 0 < args ! 5 \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> (\<not> unat (2 ^ sz >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type rv \<or> rv = Untyped) \<longrightarrow> 0 < args ! 5 \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> pas_refined aag s \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)))
 3. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>\<lambda>yb s. True \<and> ?P'207 y ya yb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref; rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and> sz < word_bits \<and> is_aligned base sz \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))\<rbrakk> \<Longrightarrow> (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> (\<not> unat (2 ^ sz - word_of_nat (free_index_of (UntypedCap dev base sz idx)) >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type rv \<or> rv = Untyped) \<longrightarrow> 0 < args ! 5 \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> (\<not> unat (2 ^ sz >> obj_bits_api rv (data_to_nat (args ! Suc 0))) < data_to_nat (args ! 5) \<longrightarrow> (dev \<longrightarrow> is_frame_type rv \<or> rv = Untyped) \<longrightarrow> 0 < args ! 5 \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> ((\<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> pas_refined aag s \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x)) \<and> rv \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)))
 2. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>\<lambda>yb s. True \<and> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and> sz < word_bits \<and> is_aligned base sz \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B26 y ya\<rbrace> whenE (excaps = []) (throwError TruncatedMessage) \<lbrace>\<lambda>yb s. True \<and> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and> sz < word_bits \<and> is_aligned base sz \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>y. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?B25 y\<rbrace> whenE (length args < 6) (throwError TruncatedMessage) \<lbrace>?B26 y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>cap = UntypedCap dev base sz idx; is_subject aag (fst slot); Ball (set excaps) (pas_cap_cur_auth aag); \<forall>ref\<in>{base..base + 2 ^ sz - 1}. is_subject aag ref\<rbrakk> \<Longrightarrow> \<lbrace>?P'12\<rbrace> whenE (gen_invocation_type label \<noteq> UntypedRetype) (throwError IllegalOperation) \<lbrace>?B25\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> ?P'12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = UntypedCap dev base sz idx \<and> is_subject aag (fst slot) \<and> Ball (set excaps) (pas_cap_cur_auth aag) \<and> (\<forall>ref\<in>untyped_range cap. is_subject aag ref); (invs and pas_refined aag and valid_cap cap and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at ((=) (UntypedCap dev base sz idx)) slot and (\<lambda>s. \<forall>cap\<in>set excaps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x)) s \<and> pas_refined aag s \<and> (\<not> gen_invocation_type label \<noteq> UntypedRetype \<longrightarrow> \<not> length args < 6 \<longrightarrow> excaps \<noteq> [] \<longrightarrow> True \<and> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and> sz < word_bits \<and> is_aligned base sz \<and> (is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (excaps ! 0). is_subject aag x))) proof (prove)
goal:
No subgoals!