theory VSpace_C

lemma updateCap_frame_mapped_addr_ccorres:
  notes option.case_cong_weak [cong]
  shows "ccorres dc xfdc
           (cte_wp_at' (\<lambda>c. ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap))
           UNIV []
           (updateCap ctSlot (ArchObjectCap (capVPMappedAddress_update Map.empty cap)))
           (CALL generic_frame_cap_ptr_set_capFMappedAddress(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),(scast asidInvalid),0))" unfolding updateCap_def apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac P = "\<lambda>s. ctes_of s ctSlot = Some cte \<and> cteCap cte = ArchObjectCap cap \<and> isPageCap cap" and
                   P' = "UNIV"
                in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (erule (1) rf_sr_ctes_of_cliftE) apply (frule cap_CL_lift) apply (clarsimp simp: typ_heap_simps) apply (rule conjI) apply (clarsimp simp: isCap_simps) apply (drule cap_CL_lift) apply (drule (1) cap_to_H_PageCap_tag) apply simp apply (clarsimp simp: isCap_simps) apply (rule exI) apply (rule conjI, rule refl) apply clarsimp apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI [rotated]) apply clarsimp apply (frule (1) rf_sr_ctes_of_clift) apply clarsimp apply (subgoal_tac "ccte_relation (cteCap_update (\<lambda>_. ArchObjectCap (PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a") prefer 2 apply (clarsimp simp: ccte_relation_def) apply (clarsimp simp: cte_lift_def) apply (simp split: option.splits) apply clarsimp apply (simp add: cte_to_H_def c_valid_cte_def) apply (erule (4) generic_frame_mapped_address) apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps
     Let_def cpspace_relation_def) apply (rule conjI) apply (erule (3) cmap_relation_updI) subgoal by simp apply (erule_tac t = s' in ssubst) apply (simp add: heap_to_user_data_def) apply (rule conjI) apply (erule (1) setCTE_tcb_case) subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
                         typ_heap_simps h_t_valid_clift_Some_iff
                         cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) UNIV [] (updateCap ctSlot (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap))) (CALL generic_frame_cap_ptr_set_capFMappedAddress_'proc(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),SCAST(32 signed \<rightarrow> 32) asidInvalid,0)) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) UNIV [] (do cte <- getCTE ctSlot;
setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte)
od) (CALL generic_frame_cap_ptr_set_capFMappedAddress_'proc(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),SCAST(32 signed \<rightarrow> 32) asidInvalid,0)) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?Q' [] (do cte <- getCTE ctSlot;
setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte)
od) (CALL generic_frame_cap_ptr_set_capFMappedAddress_'proc(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),SCAST(32 signed \<rightarrow> 32) asidInvalid,0))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>cte. ccorres dc xfdc (?P3 cte) (?P'3 cte) [] (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte)) (CALL generic_frame_cap_ptr_set_capFMappedAddress_'proc(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),SCAST(32 signed \<rightarrow> 32) asidInvalid,0))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ?P3 cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?P'3 (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (ctes_of \<sigma> ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} CALL generic_frame_cap_ptr_set_capFMappedAddress_'proc(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),SCAST(32 signed \<rightarrow> 32) asidInvalid,0) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma>. {s. (ctes_of \<sigma> ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (\<exists>cap. cslift s (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C''])) = Some cap \<and> cap_lift cap \<noteq> None \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap)) \<and> (\<exists>cte_slot. cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = cap_Ptr &(cte_slot\<rightarrow>[''cap_C'']) \<and> cslift s cte_slot \<noteq> None \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift s (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']))))) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (K cap')) (cte_lift (the (cslift s cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals s))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte) \<sigma>). (\<sigma>', s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)))))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>ctes_of \<sigma> ctSlot = Some cte; cteCap cte = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<exists>cap. cslift x (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C''])) = Some cap \<and> (\<exists>y. cap_lift cap = Some y) \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap)) \<and> (\<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift x (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']))))) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x cte' ctel'. \<lbrakk>cteCap cte = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cte = cte_to_H ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> (\<exists>cap. cslift x (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C''])) = Some cap \<and> (\<exists>y. cap_lift cap = Some y) \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap)) \<and> (\<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift x (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']))))) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x cte' ctel'. \<lbrakk>cteCap cte = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cte = cte_to_H ctel'; cl_valid_cte ctel'; cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel')\<rbrakk> \<Longrightarrow> (\<exists>cap. cslift x (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C''])) = Some cap \<and> (\<exists>y. cap_lift cap = Some y) \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap)) \<and> (\<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift x (cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']))))) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> (cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) \<and> (\<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 2. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> \<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap
 2. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> \<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel')\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap
 2. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> \<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel'); cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap
 2. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> \<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap cap; isPageCap cap; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> \<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>x. None) cap)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3\<rbrakk> \<Longrightarrow> \<exists>cte_slot. &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(cte_slot\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x cte_slot = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x cte_slot))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3\<rbrakk> \<Longrightarrow> &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']) = &(?cte_slot81 \<sigma> x cte' ctel' d v0 v1 v2 v3\<rightarrow>[''cap_C'']) \<and> (\<exists>y. cslift x (?cte_slot81 \<sigma> x cte' ctel' d v0 v1 v2 v3) = Some y) \<and> (\<forall>t. (\<exists>cte'a cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte'a = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x (?cte_slot81 \<sigma> x cte' ctel' d v0 v1 v2 v3)))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (?cte_slot81 \<sigma> x cte' ctel' d v0 v1 v2 v3) cte'a) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3\<rbrakk> \<Longrightarrow> (\<exists>y. cslift x (cte_Ptr ctSlot) = Some y) \<and> (\<forall>t. (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift (the (cslift x (cte_Ptr ctSlot)))) \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte') (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); ((), s') \<in> fst (setCTE ctSlot (?cte95 \<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap') \<sigma>); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> ?cte95 \<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap'); 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 ctSlot (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; \<exists>cte'. cslift x (cte_Ptr ctSlot) = 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> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel') = cte_to_H (ctel'\<lparr>cap_CL := cap'\<rparr>) \<and> c_valid_cte cte'a
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>) = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; (case cap_lift (cte_C.cap_C cte'a) of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte'a)\<rparr>) = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel') = cte_to_H (ctel'\<lparr>cap_CL := cap'\<rparr>) \<and> c_valid_cte cte'a
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s' x2 x2a. \<lbrakk>t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cap_lift (cte_C.cap_C cte') = Some x2; \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr> = ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift (cte_C.cap_C cte'a) = Some x2a; \<lparr>cap_CL = x2a, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte'a)\<rparr> = ctel'\<lparr>cap_CL := cap'\<rparr>\<rbrakk> \<Longrightarrow> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel') = cte_to_H (ctel'\<lparr>cap_CL := cap'\<rparr>) \<and> c_valid_cte cte'a
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' d v0 v1 v2 v3 t cte'a cap' s' x2. \<lbrakk>t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>)); 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'; c_valid_cte cte'; cap_to_H x2 = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>); cslift x (cte_Ptr ctSlot) = Some cte'; cap_lift (cte_C.cap_C cte') = Some x2; cl_valid_cte \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some x2) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift (cte_C.cap_C cte'a) = Some cap'; mdb_node_lift (cteMDBNode_C cte'a) = mdb_node_lift (cteMDBNode_C cte')\<rbrakk> \<Longrightarrow> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>) = cte_to_H \<lparr>cap_CL = cap', cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr> \<and> c_valid_cte cte'a
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' d v0 v1 v2 v3 t cte'a cap' s' x2. \<lbrakk>t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> CTE (capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (mdb_node_to_H (mdb_node_lift (cteMDBNode_C cte')))); 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'; c_valid_cap (cte_C.cap_C cte'); cap_to_H x2 = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (CTE (capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3)) (mdb_node_to_H (mdb_node_lift (cteMDBNode_C cte')))); cslift x (cte_Ptr ctSlot) = Some cte'; cap_lift (cte_C.cap_C cte') = Some x2; cl_valid_cte \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some x2) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift (cte_C.cap_C cte'a) = Some cap'; mdb_node_lift (cteMDBNode_C cte'a) = mdb_node_lift (cteMDBNode_C cte')\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap (cte_C.cap_C cte'a)
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a\<rbrakk> \<Longrightarrow> (s', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel'))) ((cslift x)(cte_Ptr ctSlot \<mapsto> cte'a)) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = 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\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cte_array_relation s' (globals x) \<and> tcb_cte_array_relation s' (globals x) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals x)) (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>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel'))) ((cslift x)(cte_Ptr ctSlot \<mapsto> cte'a)) cte_Ptr ccte_relation
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = 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\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cte_array_relation s' (globals x) \<and> tcb_cte_array_relation s' (globals x) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals x)) (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>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> inj cte_Ptr
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = 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\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cte_array_relation s' (globals x) \<and> tcb_cte_array_relation s' (globals x) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals x)) (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>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_to_H (cap_CL ctel'_) = capability.ArchObjectCap (arch_capability.PageCap d_ v0_ v1_ v2_ v3_); ctes_of \<sigma>_ ctSlot = Some (cte_to_H ctel'_); cslift x_ (cte_Ptr ctSlot) = Some cte'_; cte_lift cte'_ = Some ctel'_; cl_valid_cte ctel'_; cap = arch_capability.PageCap d_ v0_ v1_ v2_ v3_; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel'_)) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'_; cte_lift cte'a_ = Some (ctel'_\<lparr>cap_CL := cap'_\<rparr>); t_hrs_' (globals t_) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a_) (t_hrs_' (globals x_)); s'_ = \<sigma>_\<lparr>ksPSpace := ksPSpace s'_\<rparr>; ctes_of s'_ = (ctes_of \<sigma>_)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d_ v0_ v1_ v2_ None)) (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'_; c_valid_cte cte'_; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d_ v0_ v1_ v2_ None)) (cte_to_H ctel'_)) cte'a_; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'_)) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); cmap_relation (map_to_ntfns (ksPSpace s'_)) (cslift x_) ntfn_Ptr (cnotification_relation (cslift x_)); cmap_relation (map_to_pdes (ksPSpace s'_)) (cslift x_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'_)) (cslift x_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'_)) (cslift x_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s'_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'_)) (c_h_t_valid x_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'_)) (c_h_t_valid x_) pt_Ptr; cready_queues_relation (cslift x_) (ksReadyQueues_' (globals x_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals x_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals x_)); carch_state_relation (ksArchState \<sigma>_) (globals x_); cmachine_state_relation (ksMachineState \<sigma>_) (globals x_); cte_array_relation \<sigma>_ (globals x_); tcb_cte_array_relation \<sigma>_ (globals x_); apsnd fst (ghost'state_' (globals x_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals x_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals x_) = ksWorkUnitsCompleted \<sigma>_; x_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x_))); - 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 x_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals x_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals x_) = ksDomainTime \<sigma>_\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s') \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s') \<and> ksCurThread \<sigma> = ksCurThread s' \<and> ksIdleThread \<sigma> = 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\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState s') (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cte_array_relation s' (globals x) \<and> tcb_cte_array_relation s' (globals x) \<and> gsUserPages \<sigma> = gsUserPages s' \<and> gsCNodes \<sigma> = gsCNodes s' \<and> ghost_size_rel (ghost'state_' (globals x)) (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>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>))) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (underlying_memory (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (underlying_memory (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) \<and> zero_ranges_are_zero (gsUntypedZeroRanges (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) \<and> ksCurThread \<sigma> = ksCurThread (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) \<and> ksIdleThread \<sigma> = ksIdleThread (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) \<and> cinterrupt_relation (ksInterruptState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (ksSchedulerAction_' (globals x)) \<and> carch_state_relation (ksArchState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cte_array_relation (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) (globals x) \<and> tcb_cte_array_relation (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) (globals x) \<and> gsUserPages \<sigma> = gsUserPages (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) \<and> gsCNodes \<sigma> = gsCNodes (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) \<and> cdom_schedule_relation (kernel_state.ksDomSchedule (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) \<and> ksCurDomain \<sigma> = ksCurDomain (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>) \<and> ksDomainTime \<sigma> = ksDomainTime (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s') p)) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> tcb_cte_array_relation s' (globals x)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s') p)) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s')) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation
 2. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s') p)) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> tcb_cte_array_relation s' (globals x)
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte' ctel' d v0 v1 v2 v3 t cte'a cap' s'. \<lbrakk>cap_to_H (cap_CL ctel') = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); ctes_of \<sigma> ctSlot = Some (cte_to_H ctel'); cslift x (cte_Ptr ctSlot) = Some cte'; cte_lift cte' = Some ctel'; cl_valid_cte ctel'; cap = arch_capability.PageCap d v0 v1 v2 v3; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel')) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cte_lift cte'a = Some (ctel'\<lparr>cap_CL := cap'\<rparr>); t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x)); ctes_of s' = (ctes_of \<sigma>)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (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'; c_valid_cte cte'; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace s')) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace s')) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s') p)) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s')) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s')) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a) (t_hrs_' (globals x))\<rparr>) \<and> tcb_cte_array_relation s' (globals x)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_to_H (cap_CL ctel'_) = capability.ArchObjectCap (arch_capability.PageCap d_ v0_ v1_ v2_ v3_); ctes_of \<sigma>_ ctSlot = Some (cte_to_H ctel'_); cslift x_ (cte_Ptr ctSlot) = Some cte'_; cte_lift cte'_ = Some ctel'_; cl_valid_cte ctel'_; cap = arch_capability.PageCap d_ v0_ v1_ v2_ v3_; generic_frame_cap_set_capFMappedAddress_CL (Some (cap_CL ctel'_)) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'_; cte_lift cte'a_ = Some (ctel'_\<lparr>cap_CL := cap'_\<rparr>); t_hrs_' (globals t_) = hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a_) (t_hrs_' (globals x_)); ctes_of s'_ = (ctes_of \<sigma>_)(ctSlot \<mapsto> cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d_ v0_ v1_ v2_ None)) (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'_; c_valid_cte cte'_; ccte_relation (cteCap_update (\<lambda>_. capability.ArchObjectCap (arch_capability.PageCap d_ v0_ v1_ v2_ None)) (cte_to_H ctel'_)) cte'a_; cmap_relation (ctes_of \<sigma>_) (cslift x_) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'_)) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); cmap_relation (map_to_ntfns (ksPSpace s'_)) (cslift x_) ntfn_Ptr (cnotification_relation (cslift x_)); cmap_relation (map_to_pdes (ksPSpace s'_)) (cslift x_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'_)) (cslift x_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'_)) (cslift x_) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>_)) p) (map_to_user_data (ksPSpace s'_) p)) (cslift x_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'_)) (c_h_t_valid x_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'_)) (c_h_t_valid x_) pt_Ptr; cready_queues_relation (cslift x_) (ksReadyQueues_' (globals x_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals x_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals x_)); carch_state_relation (ksArchState \<sigma>_) (globals x_); cmachine_state_relation (ksMachineState \<sigma>_) (globals x_); cte_array_relation \<sigma>_ (globals x_); tcb_cte_array_relation \<sigma>_ (globals x_); apsnd fst (ghost'state_' (globals x_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals x_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals x_) = ksWorkUnitsCompleted \<sigma>_; x_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x_))); - 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 x_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals x_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals x_) = ksDomainTime \<sigma>_\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>_) (globals x_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a_) (t_hrs_' (globals x_))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>_) (globals x_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ctSlot) cte'a_) (t_hrs_' (globals x_))\<rparr>) \<and> tcb_cte_array_relation s'_ (globals x_) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. capability.ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s ctSlot = Some cte \<longrightarrow> ctes_of s ctSlot = Some cte \<and> cteCap cte = capability.ArchObjectCap cap \<and> isPageCap cap) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr ctSlot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal:
No subgoals!