theory Untyped_R

lemma updateFreeIndex_corres:
  "\<lbrakk>is_untyped_cap cap; free_index_of cap = idx \<rbrakk>
   \<Longrightarrow> corres dc
         (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and>
          cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs
           and pspace_aligned and pspace_distinct)
         (cte_at' (cte_map src)
           and pspace_distinct' and pspace_aligned')
         (set_cap cap src) (updateFreeIndex (cte_map src) idx)" apply (rule corres_name_pre) apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r_conj[where P'="cte_at' (cte_map src)"])+ apply (rule_tac F="isUntypedCap capa
                 \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)"
               in corres_gen_asm2) apply (rule updateCap_isUntypedCap_corres, simp+) apply (clarsimp simp: isCap_simps) apply simp apply (wp getSlotCap_wp)+ apply (clarsimp simp: state_relation_def cte_wp_at_ctes_of) apply (rule no_fail_pre, wp no_fail_getSlotCap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (wp getSlotCap_wp)+ apply (clarsimp simp: state_relation_def cte_wp_at_ctes_of) apply (rule no_fail_pre, wp no_fail_getSlotCap) apply simp apply clarsimp apply (clarsimp simp: cte_wp_at_ctes_of cte_wp_at_caps_of_state) apply (frule state_relation_pspace_relation) apply (frule(1) pspace_relation_ctes_ofI[OF _ caps_of_state_cteD], simp+) apply (clarsimp simp: isCap_simps is_cap_simps
                        cte_wp_at_caps_of_state free_index_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned') (set_cap cap src) (updateFreeIndex (cte_map src) idx) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) s; (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (updateFreeIndex (cte_map src) idx) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do y <- do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap (cte_map src);
updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. idx) cap)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc (?Q2 s s') (?Q'2 s s') (set_cap cap src) (do y <- do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap (cte_map src);
updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. idx) cap)
od)
 2. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s s' sa
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> ?Q'2 s s' sa proof (prove)
goal (9 subgoals):
 1. \<And>s s' y capa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc (?Q2 s s') (?R'11 s s' y capa) (set_cap cap src) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. idx) capa))
 2. \<And>s s' y. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 s s' y\<rbrace> getSlotCap (cte_map src) \<lbrace>?R'11 s s' y\<rbrace>
 3. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>cap s'. (sa, s') \<in> state_relation\<rbrace>
 4. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 5. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'11 s s' y\<rbrace>
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 7. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 8. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s s' sa
 9. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s s' y capa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)\<rbrakk> \<Longrightarrow> corres dc (?Q2 s s') (?P'16 s s' y capa) (set_cap cap src) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. idx) capa))
 2. \<And>s s' y. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 s s' y\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>capa. ?P'16 s s' y capa and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))\<rbrace>
 3. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>cap s'. (sa, s') \<in> state_relation\<rbrace>
 4. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 5. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'11 s s' y\<rbrace>
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 7. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 8. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s s' sa
 9. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (10 subgoals):
 1. \<And>s s' capa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)\<rbrakk> \<Longrightarrow> isUntypedCap (capFreeIndex_update (\<lambda>_. idx) capa)
 2. \<And>s s' y capa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)\<rbrakk> \<Longrightarrow> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)
 3. \<And>s s' y. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 s s' y\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>capa. cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))\<rbrace>
 4. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>cap s'. (sa, s') \<in> state_relation\<rbrace>
 5. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 6. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'11 s s' y\<rbrace>
 7. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 8. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 9. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 10. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s s' y capa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)\<rbrakk> \<Longrightarrow> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa)
 2. \<And>s s' y. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 s s' y\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>capa. cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))\<rbrace>
 3. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>cap s'. (sa, s') \<in> state_relation\<rbrace>
 4. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 5. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'11 s s' y\<rbrace>
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 7. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 8. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 9. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' y. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 s s' y\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>capa. cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))\<rbrace>
 2. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> getSlotCap (cte_map src) \<lbrace>\<lambda>cap s'. (sa, s') \<in> state_relation\<rbrace>
 3. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 4. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'11 s s' y\<rbrace>
 5. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 7. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 8. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' y sa sb. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; (sa, sb) \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) sb\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (cte_map src) sb \<and> (sa, sb) \<in> state_relation
 2. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 3. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)\<rbrace>
 4. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 5. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 7. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' y sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (getSlotCap (cte_map src))
 2. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)\<rbrace>
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 4. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 5. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' y sa sb. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True; (sa, sb) \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) sb\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map src) sb
 2. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)\<rbrace>
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 4. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 5. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 6. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 s s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y. cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)\<rbrace>
 2. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s'\<rbrace> do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>y s'. (sa, s') \<in> state_relation\<rbrace>
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 4. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 5. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ?Q'6 s s') sa proof (prove)
goal (4 subgoals):
 1. \<And>s s' sa sb. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; (sa, sb) \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) sb\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (cte_map src) sb \<and> (sa, sb\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges sb | Some r \<Rightarrow> gsUntypedZeroRanges sb - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges (sb\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges sb | Some r \<Rightarrow> gsUntypedZeroRanges sb - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (sb\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges sb | Some r \<Rightarrow> gsUntypedZeroRanges sb - {r}\<rparr>))\<rparr>) \<in> state_relation
 2. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 4. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) capa) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (sa, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) s') (do cap <- getSlotCap (cte_map src);
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 2. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) capa) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa sb. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; True; (sa, sb) \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map src) sb\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and ((\<lambda>_. True) and (\<lambda>s. True))) sb
 2. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 3. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) capa) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) sa
 2. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) capa) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>is_untyped_cap cap; free_index_of cap = idx; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and (\<lambda>s. \<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) (cte_map src) s \<and> (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. isUntypedCap capa \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. idx) capa))) s)) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) capa) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange capa of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa capa cte. \<lbrakk>is_untyped_cap cap; (s, sa) \<in> state_relation; idx = free_index_of cap; ctes_of sa (cte_map src) = Some cte; valid_objs s; caps_of_state s src = Some capa; pspace_distinct' sa; pspace_aligned' sa; pspace_aligned s; pspace_distinct s; is_untyped_cap capa; obj_ref_of capa = obj_ref_of cap; cap_bits capa = cap_bits cap; cap_is_device capa = cap_is_device cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. free_index_of cap) (cteCap cte)) proof (prove)
goal (1 subgoal):
 1. \<And>s sa capa cte. \<lbrakk>is_untyped_cap cap; (s, sa) \<in> state_relation; idx = free_index_of cap; ctes_of sa (cte_map src) = Some cte; valid_objs s; caps_of_state s src = Some capa; pspace_distinct' sa; pspace_aligned' sa; pspace_aligned s; pspace_distinct s; is_untyped_cap capa; obj_ref_of capa = obj_ref_of cap; cap_bits capa = cap_bits cap; cap_is_device capa = cap_is_device cap; pspace_relation (kheap s) (ksPSpace sa)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. free_index_of cap) (cteCap cte)) proof (prove)
goal (1 subgoal):
 1. \<And>s sa capa cte. \<lbrakk>is_untyped_cap cap; (s, sa) \<in> state_relation; idx = free_index_of cap; ctes_of sa (cte_map src) = Some cte; valid_objs s; caps_of_state s src = Some capa; pspace_distinct' sa; pspace_aligned' sa; pspace_aligned s; pspace_distinct s; is_untyped_cap capa; obj_ref_of capa = obj_ref_of cap; cap_bits capa = cap_bits cap; cap_is_device capa = cap_is_device cap; pspace_relation (kheap s) (ksPSpace sa); cap_relation capa (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) \<and> cap_relation cap (capFreeIndex_update (\<lambda>_. free_index_of cap) (cteCap cte)) proof (prove)
goal:
No subgoals!