theory Recycle_C

lemma updateFreeIndex_ccorres:
  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte'
               \<and> cteCap cte = cap' \<and> ccte_relation cte cte'})
          c
        {t. \<exists>cap. cap_untyped_cap_lift cap = (cap_untyped_cap_lift
                    (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot)))))
                        \<lparr> cap_untyped_cap_CL.capFreeIndex_CL := ((of_nat idx') >> 4) \<rparr>
                \<and> cap_get_tag cap = scast cap_untyped_cap
                \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot)
                    (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot)))))
                    (t_hrs_' (globals s))
                \<and> t may_only_modify_globals s in [t_hrs]
        }
    \<Longrightarrow> ccorres dc xfdc
           (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte)
               \<and> cap' = (cteCap cte)) srcSlot
           and untyped_ranges_zero'
           and (\<lambda>_. is_aligned (of_nat idx' :: word32) 4 \<and> idx' \<le> 2 ^ (capBlockSize cap')))
           {s. \<not> capIsDevice cap'
               \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs
           (updateFreeIndex srcSlot idx') c"
  (is "_ \<Longrightarrow> ccorres dc xfdc (valid_objs' and ?cte_wp_at' and _ and _) ?P' hs ?a c") apply (rule ccorres_gen_asm) apply (simp add: updateFreeIndex_def getSlotCap_def updateCap_def) apply (rule ccorres_guard_imp2) apply (rule ccorres_split_noop_lhs, rule_tac cap'=cap' in updateTrackedFreeIndex_noop_ccorres) apply (rule ccorres_pre_getCTE)+ apply (rename_tac cte cte2) apply (rule_tac P = "\<lambda>s. ?cte_wp_at' s \<and> cte2 = cte \<and> cte_wp_at' ((=) cte) srcSlot s"
              and P'="{s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte'
               \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> ?P'" in ccorres_from_vcg) apply (rule allI, rule HoarePartial.conseq_exploit_pre, clarify) apply (drule_tac x=s in spec, rule conseqPre, erule conseqPost) defer apply clarsimp apply clarsimp apply (simp add: cte_wp_at_ctes_of) apply wp apply (clarsimp simp: isCap_simps cte_wp_at_ctes_of) apply (frule(1) rf_sr_ctes_of_clift) apply clarsimp apply (frule(1) cte_lift_ccte_relation) apply (rule exI, intro conjI[rotated], assumption, simp_all)[1] apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule(1) rf_sr_ctes_of_cliftE) apply (frule(1) rf_sr_ctes_of_clift) apply clarsimp apply (subgoal_tac "ccap_relation (capFreeIndex_update (\<lambda>_. idx')
        (cteCap (the (ctes_of \<sigma> srcSlot)))) cap") apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI [rotated]) apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def
      cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
      isCap_simps) apply (simp add:cpspace_relation_def) apply (clarsimp simp:typ_heap_simps' modify_map_def mex_def meq_def) apply (rule conjI) apply (rule cpspace_cte_relation_upd_capI, assumption+) apply (rule conjI) apply (rule setCTE_tcb_case, assumption+) apply (case_tac s', clarsimp) subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
                   typ_heap_simps') apply (clarsimp simp: isCap_simps) apply (drule(1) cte_lift_ccte_relation,
    drule ccte_relation_ccap_relation) apply (simp add: cte_to_H_def) apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: ccap_relation_def cap_lift_untyped_cap
                        cap_to_H_simps cap_untyped_cap_lift_def
                        is_aligned_shiftr_shiftl
                 dest!: ccte_relation_ccap_relation) apply (rule unat_of_nat_eq unat_of_nat_eq[symmetric],
    erule order_le_less_trans,
    rule power_strict_increasing, simp_all) apply (rule unat_less_helper, rule order_le_less_trans[OF word_and_le1], simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<Longrightarrow> ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero' and (\<lambda>_. is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap')) {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} hs (updateFreeIndex srcSlot idx') c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} hs (updateFreeIndex srcSlot idx') c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} hs (do y <- updateTrackedFreeIndex srcSlot idx';
cte <- getCTE srcSlot;
ctea <- getCTE srcSlot;
setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) ctea)
od) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q6 ?Q'6 hs (do y <- updateTrackedFreeIndex srcSlot idx';
cte <- getCTE srcSlot;
ctea <- getCTE srcSlot;
setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) ctea)
od) c
 2. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q9 rv) (?Q'9 rv rv') hs (do cte <- getCTE srcSlot;
ctea <- getCTE srcSlot;
setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) ctea)
od) c
 2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>?Q9\<rbrace>
 3. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'9 rv (xfdc s)} proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cte ctea. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P20 rv cte ctea) (?P'18 rv rv' cte ctea) hs (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) ctea)) c
 2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> ?P20 rv cte ctea s)\<rbrace>
 3. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> {sa. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr srcSlot) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> sa \<in> ?P'18 rv (xfdc s) (cte_to_H cte') (cte_to_H cte'a)}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cte cte2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P20 rv cte cte2) (?P'18 rv rv' cte cte2) hs (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte2)) c
 2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> ?P20 rv cte ctea s)\<rbrace>
 3. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> {sa. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr srcSlot) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> sa \<in> ?P'18 rv (xfdc s) (cte_to_H cte') (cte_to_H cte'a)}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cte cte2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; dc rv rv'\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot \<sigma> \<and> cte2 = cte \<and> cte_wp_at' ((=) cte) srcSlot \<sigma>) \<and> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte2) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot s \<and> ctea = cte \<and> cte_wp_at' ((=) cte) srcSlot s)\<rbrace>
 3. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s} \<inter> {s. (cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma> \<and> cte = cte \<and> cte_wp_at' ((=) cte) srcSlot \<sigma>) \<and> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0} \<and> (\<sigma>, s) \<in> rf_sr}) c {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot s \<and> ctea = cte \<and> cte_wp_at' ((=) cte) srcSlot s)\<rbrace>
 3. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 3. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea; \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}\<rbrakk> \<Longrightarrow> {s} \<inter> {s. (cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma> \<and> cte = cte \<and> cte_wp_at' ((=) cte) srcSlot \<sigma>) \<and> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}
 4. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot s \<and> ctea = cte \<and> cte_wp_at' ((=) cte) srcSlot s)\<rbrace>
 5. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea; \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}\<rbrakk> \<Longrightarrow> {s} \<inter> {s. (cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma> \<and> cte = cte \<and> cte_wp_at' ((=) cte) srcSlot \<sigma>) \<and> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}
 3. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot s \<and> ctea = cte \<and> cte_wp_at' ((=) cte) srcSlot s)\<rbrace>
 4. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}}
 5. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea; \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}\<rbrakk> \<Longrightarrow> {s} \<inter> {s. (cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma> \<and> cte = cte \<and> cte_wp_at' ((=) cte) srcSlot \<sigma>) \<and> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cteCap ctea \<and> ccte_relation cte cte'}
 2. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot s \<and> ctea = cte \<and> cte_wp_at' ((=) cte) srcSlot s)\<rbrace>
 3. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}}
 4. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s srcSlot = Some ctea \<longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot s \<and> ctea = cte \<and> cte_wp_at' ((=) cte) srcSlot s)\<rbrace>
 2. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}}
 3. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'\<rbrakk> \<Longrightarrow> \<lbrace>?R9\<rbrace> updateTrackedFreeIndex srcSlot idx' \<lbrace>\<lambda>rv s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> isUntypedCap (cteCap cte) \<and> cap' = cteCap cte\<rbrace>
 2. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and ?R9) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}}
 3. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; is_aligned (word_of_nat idx') 4 \<and> idx' \<le> 2 ^ capBlockSize cap'; (s, s') \<in> rf_sr; (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cap' = cteCap cte) srcSlot and untyped_ranges_zero') s; s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx' \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx' \<or> cap' = cap)) \<circ> cteCap) srcSlot and valid_objs' and untyped_ranges_zero' and (\<lambda>s. \<forall>cte. ctes_of s srcSlot = Some cte \<longrightarrow> isUntypedCap (cteCap cte) \<and> cap' = cteCap cte)) s \<and> s' \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0} \<inter> {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr srcSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx') (capFreeIndex cap' - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx') (capPtr cap' + word_of_nat idx') = replicate (capFreeIndex cap' - idx') 0}}}}
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte d v0 v1 f cte'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; (s, s') \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; valid_objs' s; untyped_ranges_zero' s; ctes_of s srcSlot = Some cte; cap' = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 f; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr srcSlot) = Some cte'; cl_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>cte cte'. cslift s' (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte d v0 v1 f cte'. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; (s, s') \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; valid_objs' s; untyped_ranges_zero' s; ctes_of s srcSlot = Some cte; cap' = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 f; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr srcSlot) = Some cte'; cl_valid_cte cte'; \<exists>cte'. cslift s' (cte_Ptr srcSlot) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>cte cte'. cslift s' (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s' d v0 v1 f cte' cte'a. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; (s, s') \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; valid_objs' s; untyped_ranges_zero' s; ctes_of s srcSlot = Some (cte_to_H cte'); cap' = capability.UntypedCap d v0 v1 f; cap_to_H (cap_CL cte') = capability.UntypedCap d v0 v1 f; cl_valid_cte cte'; cslift s' (cte_Ptr srcSlot) = Some cte'a; cte_lift cte'a = Some cte'; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> \<exists>cte. cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'a
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s' d v0 v1 f cte' cte'a. \<lbrakk>\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'}) c {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]}; (s, s') \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; valid_objs' s; untyped_ranges_zero' s; ctes_of s srcSlot = Some (cte_to_H cte'); cap' = capability.UntypedCap d v0 v1 f; cap_to_H (cap_CL cte') = capability.UntypedCap d v0 v1 f; cl_valid_cte cte'; cslift s' (cte_Ptr srcSlot) = Some cte'a; cte_lift cte'a = Some cte'; c_valid_cte cte'a; ccte_relation (cte_to_H cte') cte'a\<rbrakk> \<Longrightarrow> \<exists>cte. cteCap cte = capability.UntypedCap d v0 v1 f \<and> ccte_relation cte cte'a
 2. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' cte cte2 \<sigma> s ctea cte'. \<lbrakk>dc rv rv'; is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap ctea); cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> cteCap ctea = cteCap cte) srcSlot \<sigma>; (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap ctea) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap ctea) + word_of_nat idx') (capFreeIndex (cteCap ctea) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap ctea) - idx') (capPtr (cteCap ctea) + word_of_nat idx') = replicate (capFreeIndex (cteCap ctea) - idx') 0; cte_wp_at' ((=) cte) srcSlot \<sigma>; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap ctea\<rbrakk> \<Longrightarrow> {t. \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) (t_hrs_' (globals s)) \<and> t may_only_modify_globals s in [t_hrs]} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>cte \<sigma> s ctea cte' x cap. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap cte); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap cte) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap cte) + word_of_nat idx') (capFreeIndex (cteCap cte) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap cte) - idx') (capPtr (cteCap cte) + word_of_nat idx') = replicate (capFreeIndex (cteCap cte) - idx') 0; ctes_of \<sigma> srcSlot = Some cte; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap cte; isUntypedCap (cteCap cte); cteCap ctea = cteCap cte; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>cte \<sigma> s ctea cte' x cap cte'a ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap cte); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap cte) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap cte) + word_of_nat idx') (capFreeIndex (cteCap cte) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap cte) - idx') (capPtr (cteCap cte) + word_of_nat idx') = replicate (capFreeIndex (cteCap cte) - idx') 0; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap cte; isUntypedCap (cteCap cte); cteCap ctea = cteCap cte; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'a; cte_lift cte'a = Some ctel'; cte = cte_to_H ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>cte \<sigma> s ctea cte' x cap cte'a ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cteCap cte); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cteCap cte) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap cte) + word_of_nat idx') (capFreeIndex (cteCap cte) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cteCap cte) - idx') (capPtr (cteCap cte) + word_of_nat idx') = replicate (capFreeIndex (cteCap cte) - idx') 0; cslift s (cte_Ptr srcSlot) = Some cte'; ccte_relation ctea cte'; cap' = cteCap cte; isUntypedCap (cteCap cte); cteCap ctea = cteCap cte; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'a; cte_lift cte'a = Some ctel'; cte = cte_to_H ctel'; cl_valid_cte ctel'; \<exists>cte'. cslift s (cte_Ptr srcSlot) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte_to_H ctel' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cap_to_H (cap_CL ctel'))) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cap_to_H (cap_CL ctel'))) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap; ((), s') \<in> fst (setCTE srcSlot (?cte122 \<sigma> s ctea cte' x cap ctel') \<sigma>); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> ?cte122 \<sigma> s ctea cte' x cap ctel'); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE srcSlot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cap_to_H (cap_CL ctel'))) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx') (cap_to_H (cap_CL ctel'))) (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'\<rbrakk> \<Longrightarrow> case ((), s') of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s)); cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cpspace_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s') \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s') \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals x)) \<and> carch_state_relation (ksArchState s') (globals x) \<and> cmachine_state_relation (ksMachineState s') (globals x) \<and> cte_array_relation s' (globals s) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages s', gsCNodes s') \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s') \<and> ksDomainTime_' (globals x) = ksDomainTime s'
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)) \<and> cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)) \<and> cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel'))) (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace s') (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))) \<and> cmap_relation (map_to_eps (ksPSpace s')) (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_ntfns (ksPSpace s')) (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))))) \<and> cmap_relation (map_to_pdes (ksPSpace s')) (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace s')) (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace s')) (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))) \<and> cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)))) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s') \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s') \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals x)) \<and> carch_state_relation (ksArchState s') (globals x) \<and> cmachine_state_relation (ksMachineState s') (globals x) \<and> cte_array_relation s' (globals s) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages s', gsCNodes s') \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s') \<and> ksDomainTime_' (globals x) = ksDomainTime s'
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel'))) ((cslift s)(cte_Ptr srcSlot \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = ksIdleThread s' \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s' (globals s) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain \<sigma> = ksCurDomain s' \<and> ksDomainTime \<sigma> = ksDomainTime s'
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel'))) ((cslift s)(cte_Ptr srcSlot \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) cte_Ptr ccte_relation
 2. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = ksIdleThread s' \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s' (globals s) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain \<sigma> = ksCurDomain s' \<and> ksDomainTime \<sigma> = ksDomainTime s'
 3. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = ksIdleThread s' \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s' (globals s) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain \<sigma> = ksCurDomain s' \<and> ksDomainTime \<sigma> = ksDomainTime s'
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation
 2. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = ksIdleThread s' \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s' (globals s) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain \<sigma> = ksCurDomain s' \<and> ksDomainTime \<sigma> = ksDomainTime s'
 3. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' s' d v0 v1 f a b. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = ksIdleThread s' \<and> cinterrupt_relation (ksInterruptState s') intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s') (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s' (globals s) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s') \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s' \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s') kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s') \<and> ksCurDomain \<sigma> = ksCurDomain s' \<and> ksDomainTime \<sigma> = ksDomainTime s'
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s ctea cte' x cap ctel' d v0 v1 f a b ksPSpacea gsUserPagesa gsCNodesa gsUntypedZeroRangesa gsMaxObjectSizea ksDomScheduleIdxa ksDomSchedulea ksCurDomaina ksDomainTimea ksReadyQueuesa ksReadyQueuesL1Bitmapa ksReadyQueuesL2Bitmapa ksCurThreada ksIdleThreada ksSchedulerActiona ksInterruptStatea ksWorkUnitsCompleteda ksArchStatea ksMachineStatea. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a, b) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; ccap_relation (capability.UntypedCap d v0 v1 idx') cap; \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRangesa, gsMaxObjectSize = gsMaxObjectSizea, ksDomScheduleIdx = ksDomScheduleIdxa, ksDomSchedule = ksDomSchedulea, ksCurDomain = ksCurDomaina, ksDomainTime = ksDomainTimea, ksReadyQueues = ksReadyQueuesa, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmapa, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmapa, ksCurThread = ksCurThreada, ksIdleThread = ksIdleThreada, ksSchedulerAction = ksSchedulerActiona, ksInterruptState = ksInterruptStatea, ksWorkUnitsCompleted = ksWorkUnitsCompleteda, ksArchState = ksArchStatea, ksMachineState = ksMachineStatea\<rparr> = \<sigma>\<lparr>ksPSpace := ksPSpacea\<rparr>; map_to_ctes ksPSpacea = (ctes_of \<sigma>)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx') (cte_to_H ctel')); map_to_eps (ksPSpace \<sigma>) = map_to_eps ksPSpacea; map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns ksPSpacea; map_to_pdes (ksPSpace \<sigma>) = map_to_pdes ksPSpacea; map_to_ptes (ksPSpace \<sigma>) = map_to_ptes ksPSpacea; map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools ksPSpacea; map_to_user_data (ksPSpace \<sigma>) = map_to_user_data ksPSpacea; map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device ksPSpacea; map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs ksPSpacea; \<forall>T p. typ_at' T p \<sigma> = typ_at' T p (\<sigma>\<lparr>ksPSpace := ksPSpacea\<rparr>); cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs ksPSpacea) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s))); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>; globals x = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps ksPSpacea) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); cmap_relation (map_to_ntfns ksPSpacea) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes ksPSpacea) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes ksPSpacea) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools ksPSpacea) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data ksPSpacea (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data ksPSpacea (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes ksPSpacea) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes ksPSpacea) (c_h_t_valid s) pt_Ptr\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s))\<rparr>)
 2. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1_; \<not> d_ \<longrightarrow> region_actually_is_bytes (v0_ + word_of_nat idx') (f_ - idx') s_ \<and> heap_list (hrs_mem (t_hrs_' (globals s_))) (f_ - idx') (v0_ + word_of_nat idx') = replicate (f_ - idx') 0; ccte_relation ctea_ cte'_; cap' = capability.UntypedCap d_ v0_ v1_ f_; cteCap ctea_ = capability.UntypedCap d_ v0_ v1_ f_; cap_untyped_cap_lift cap_ = cap_untyped_cap_lift (cte_C.cap_C cte'_)\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap_ = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (a_, b_) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap_) cte'_)) (t_hrs_' (globals s_)); ctes_of \<sigma>_ srcSlot = Some (cte_to_H ctel'_); cslift s_ (cte_Ptr srcSlot) = Some cte'_; cte_lift cte'_ = Some ctel'_; cl_valid_cte ctel'_; c_valid_cte cte'_; ccap_relation (capability.UntypedCap d_ v0_ v1_ idx') cap_; \<lparr>ksPSpace = ksPSpacea_, gsUserPages = gsUserPagesa_, gsCNodes = gsCNodesa_, gsUntypedZeroRanges = gsUntypedZeroRangesa_, gsMaxObjectSize = gsMaxObjectSizea_, ksDomScheduleIdx = ksDomScheduleIdxa_, ksDomSchedule = ksDomSchedulea_, ksCurDomain = ksCurDomaina_, ksDomainTime = ksDomainTimea_, ksReadyQueues = ksReadyQueuesa_, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmapa_, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmapa_, ksCurThread = ksCurThreada_, ksIdleThread = ksIdleThreada_, ksSchedulerAction = ksSchedulerActiona_, ksInterruptState = ksInterruptStatea_, ksWorkUnitsCompleted = ksWorkUnitsCompleteda_, ksArchState = ksArchStatea_, ksMachineState = ksMachineStatea_\<rparr> = \<sigma>_\<lparr>ksPSpace := ksPSpacea_\<rparr>; map_to_ctes ksPSpacea_ = (ctes_of \<sigma>_)(srcSlot \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d_ v0_ v1_ idx') (cte_to_H ctel'_)); map_to_eps (ksPSpace \<sigma>_) = map_to_eps ksPSpacea_; map_to_ntfns (ksPSpace \<sigma>_) = map_to_ntfns ksPSpacea_; map_to_pdes (ksPSpace \<sigma>_) = map_to_pdes ksPSpacea_; map_to_ptes (ksPSpace \<sigma>_) = map_to_ptes ksPSpacea_; map_to_asidpools (ksPSpace \<sigma>_) = map_to_asidpools ksPSpacea_; map_to_user_data (ksPSpace \<sigma>_) = map_to_user_data ksPSpacea_; map_to_user_data_device (ksPSpace \<sigma>_) = map_to_user_data_device ksPSpacea_; map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>_) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs ksPSpacea_; \<forall>T p. typ_at' T p \<sigma>_ = typ_at' T p (\<sigma>_\<lparr>ksPSpace := ksPSpacea_\<rparr>); cap_to_H (cap_CL ctel'_) = capability.UntypedCap d_ v0_ v1_ f_; cready_queues_relation (cslift s_) (ksReadyQueues_' (globals s_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals s_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals s_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals s_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals s_)); carch_state_relation (ksArchState \<sigma>_) (globals s_); cmachine_state_relation (ksMachineState \<sigma>_) (globals s_); cte_array_relation \<sigma>_ (globals s_); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs ksPSpacea_) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s_))); apsnd fst (ghost'state_' (globals s_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals s_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals s_) = ksWorkUnitsCompleted \<sigma>_; s_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals s_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals s_) = ksDomainTime \<sigma>_; globals x_ = globals s_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap_) cte'_)) (t_hrs_' (globals s_))\<rparr>; cmap_relation (ctes_of \<sigma>_) (cslift s_) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift s_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps ksPSpacea_) (cslift s_) ep_Ptr (cendpoint_relation (cslift s_)); cmap_relation (map_to_ntfns ksPSpacea_) (cslift s_) ntfn_Ptr (cnotification_relation (cslift s_)); cmap_relation (map_to_pdes ksPSpacea_) (cslift s_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes ksPSpacea_) (cslift s_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools ksPSpacea_) (cslift s_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data ksPSpacea_ (underlying_memory (ksMachineState \<sigma>_))) (cslift s_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data ksPSpacea_ (underlying_memory (ksMachineState \<sigma>_))) (cslift s_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes ksPSpacea_) (c_h_t_valid s_) pd_Ptr; carray_map_relation ptBits (map_to_ptes ksPSpacea_) (c_h_t_valid s_) pt_Ptr\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>_) (globals s_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap_) cte'_)) (t_hrs_' (globals s_))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>_) (globals s_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap_) cte'_)) (t_hrs_' (globals s_))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ capBlockSize (cap_to_H (cap_CL ctel')); (\<sigma>, s) \<in> rf_sr; \<not> capIsDevice (cap_to_H (cap_CL ctel')) \<longrightarrow> region_actually_is_bytes (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') (capPtr (cap_to_H (cap_CL ctel')) + word_of_nat idx') = replicate (capFreeIndex (cap_to_H (cap_CL ctel')) - idx') 0; ccte_relation ctea cte'; cap' = cap_to_H (cap_CL ctel'); isUntypedCap (cap_to_H (cap_CL ctel')); cteCap ctea = cap_to_H (cap_CL ctel'); cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccap_relation (capFreeIndex_update (\<lambda>_. idx') (cteCap (the (ctes_of \<sigma> srcSlot)))) cap proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel' d v0 v1 f. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; (\<sigma>, s) \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; ccte_relation ctea cte'; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> ccap_relation (capability.UntypedCap d v0 v1 idx') cap proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel' d v0 v1 f. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; (\<sigma>, s) \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (cte_to_H ctel'); cslift s (cte_Ptr srcSlot) = Some cte'; cl_valid_cte ctel'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; ccte_relation (cte_to_H ctel') cte'; ccap_relation (cteCap ctea) (cte_C.cap_C cte')\<rbrakk> \<Longrightarrow> ccap_relation (capability.UntypedCap d v0 v1 idx') cap proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel' d v0 v1 f. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; (\<sigma>, s) \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (CTE (capability.UntypedCap d v0 v1 f) (mdb_node_to_H (cteMDBNode_CL ctel'))); cslift s (cte_Ptr srcSlot) = Some cte'; cl_valid_cte ctel'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; ccte_relation (CTE (capability.UntypedCap d v0 v1 f) (mdb_node_to_H (cteMDBNode_CL ctel'))) cte'; ccap_relation (capability.UntypedCap d v0 v1 f) (cte_C.cap_C cte')\<rbrakk> \<Longrightarrow> ccap_relation (capability.UntypedCap d v0 v1 idx') cap proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel' d v0 v1 f. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ v1; (\<sigma>, s) \<in> rf_sr; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx') (f - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (f - idx') (v0 + word_of_nat idx') = replicate (f - idx') 0; cap' = capability.UntypedCap d v0 v1 f; cteCap ctea = capability.UntypedCap d v0 v1 f; cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C cte')\<lparr>capFreeIndex_CL := word_of_nat idx' >> 4\<rparr>; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (CTE (capability.UntypedCap d v0 v1 f) (mdb_node_to_H (cteMDBNode_CL ctel'))); cslift s (cte_Ptr srcSlot) = Some cte'; cl_valid_cte ctel'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.UntypedCap d v0 v1 f; ccte_relation (CTE (capability.UntypedCap d v0 v1 f) (mdb_node_to_H (cteMDBNode_CL ctel'))) cte'; ccap_relation (capability.UntypedCap d v0 v1 f) (cte_C.cap_C cte'); cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> ccap_relation (capability.UntypedCap d v0 v1 idx') cap proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; idx' \<le> 2 ^ unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5); (\<sigma>, s) \<in> rf_sr; \<not> to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1) \<longrightarrow> region_actually_is_bytes ((cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) + word_of_nat idx') (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4) - idx') ((cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) + word_of_nat idx') = replicate (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4) - idx') 0; cap' = capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4)); cteCap ctea = capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4)); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (CTE (capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4))) (mdb_node_to_H (cteMDBNode_CL ctel'))); cslift s (cte_Ptr srcSlot) = Some cte'; cl_valid_cte ctel'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4)); cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (cap_C.words_C cap.[Suc 0] >> 6) && mask 26 = word_of_nat idx' >> 4; (cap_C.words_C cap.[Suc 0] >> 5) && 1 = (cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1; cap_C.words_C cap.[Suc 0] && mask 5 = cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5; cap_C.words_C cap.[0] && ~~ mask 4 = cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4\<rbrakk> \<Longrightarrow> idx' = unat (word_of_nat idx') proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s ctea cte' x cap ctel'. \<lbrakk>is_aligned (word_of_nat idx') 4; (\<sigma>, s) \<in> rf_sr; \<not> to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1) \<longrightarrow> region_actually_is_bytes ((cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) + word_of_nat idx') (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4) - idx') s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4) - idx') ((cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) + word_of_nat idx') = replicate (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4) - idx') 0; cap' = capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4)); cteCap ctea = capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4)); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; t_hrs_' (globals x) = hrs_mem_update (heap_update (cte_Ptr srcSlot) (cte_C.cap_C_update (\<lambda>_. cap) cte')) (t_hrs_' (globals s)); x may_only_modify_globals s in [t_hrs]; ctes_of \<sigma> srcSlot = Some (CTE (capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4))) (mdb_node_to_H (cteMDBNode_CL ctel'))); cslift s (cte_Ptr srcSlot) = Some cte'; cl_valid_cte ctel'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.UntypedCap (to_bool ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1)) (cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4) (unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5)) (unat ((cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 6) && mask 26 << 4)); cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; (cap_C.words_C cap.[Suc 0] >> 6) && mask 26 = word_of_nat idx' >> 4; (cap_C.words_C cap.[Suc 0] >> 5) && 1 = (cap_C.words_C (cte_C.cap_C cte').[Suc 0] >> 5) && 1; cap_C.words_C cap.[Suc 0] && mask 5 = cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5; cap_C.words_C cap.[0] && ~~ mask 4 = cap_C.words_C (cte_C.cap_C cte').[0] && ~~ mask 4\<rbrakk> \<Longrightarrow> unat (cap_C.words_C (cte_C.cap_C cte').[Suc 0] && mask 5) < 32 proof (prove)
goal:
No subgoals!