theory CSpace_C

lemma ccorres_updateCap [corres]:
  fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> cap_C"
  shows "ccorres dc xfdc \<top>
        ({s. ccap_relation cap (val s)} \<inter> {s. ptr s = Ptr dest}) hs
        (updateCap dest cap)
        (Basic
  (\<lambda>s. globals_update
   (t_hrs_'_update
     (hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cap_C''])) (val s)))) s))" unfolding updateCap_def apply (cinitlift ptr) apply (erule ssubst) apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some rva" in
    ccorres_from_vcg [where P' = "{s. ccap_relation cap (val s)}"]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI [rotated]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp add: rf_sr_def cstate_relation_def
     Let_def cpspace_relation_def
     cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) apply (simp add:typ_heap_simps) apply (rule conjI) apply (erule (3) cpspace_cte_relation_upd_capI) apply (frule_tac f="ksPSpace" in arg_cong) apply (erule_tac t = s' in ssubst) apply simp apply (simp add: heap_to_user_data_def heap_to_device_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) by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) ({s. ccap_relation cap (val s)} \<inter> {s. ptr s = cte_Ptr dest}) hs (updateCap dest cap) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(\<acute>ptr\<rightarrow>[''cap_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) ({s. ccap_relation cap (val s)} \<inter> {s. ptr s = cte_Ptr dest}) hs (do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(\<acute>ptr\<rightarrow>[''cap_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. rv = cte_Ptr dest \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. ccap_relation cap (val s)} hs (do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(rv\<rightarrow>[''cap_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. ccorres dc xfdc (\<lambda>_. True) {s. ccap_relation cap (val s)} hs (do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) \<acute>val))) proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres dc xfdc (?Q21 rv) (?Q'21 rv) hs (do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) \<acute>val)))
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> ?Q21 rv s \<and> s' \<in> ?Q'21 rv proof (prove)
goal (2 subgoals):
 1. \<And>rv rva. ccorres dc xfdc (?P24 rv rva) (?P'24 rv rva) hs (setCTE dest (cteCap_update (\<lambda>_. cap) rva)) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) \<acute>val)))
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ?P24 rv cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?P'24 rv (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>rv rva. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ctes_of \<sigma> dest = Some rva \<and> s \<in> {s. ccap_relation cap (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) \<acute>val)) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteCap_update (\<lambda>_. cap) rva) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rv rva \<sigma>. \<Gamma>\<turnstile> {s. ctes_of \<sigma> dest = Some rva \<and> s \<in> {s. ccap_relation cap (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) \<acute>val)) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteCap_update (\<lambda>_. cap) rva) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (3 subgoals):
 1. \<And>rv rva \<sigma>. \<Gamma>\<turnstile> (?P'30 rv rva \<sigma>) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) \<acute>val)) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteCap_update (\<lambda>_. cap) rva) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>rv rva \<sigma>. {s. ctes_of \<sigma> dest = Some rva \<and> s \<in> {s. ccap_relation cap (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'30 rv rva \<sigma>
 3. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rv rva \<sigma>. {s. ctes_of \<sigma> dest = Some rva \<and> s \<in> {s. ccap_relation cap (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteCap_update (\<lambda>_. cap) rva) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val s)))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val s)))) s))}
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rva \<sigma> x. \<lbrakk>ctes_of \<sigma> dest = Some rva; ccap_relation cap (val x); (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE dest (cteCap_update (\<lambda>_. cap) rva) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rva \<sigma> x s'. \<lbrakk>ctes_of \<sigma> dest = Some rva; ccap_relation cap (val x); (\<sigma>, x) \<in> rf_sr; ((), s') \<in> fst (setCTE dest (?cte44 rva \<sigma> x) \<sigma>); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> ?cte44 rva \<sigma> x); 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 dest (cteCap_update (\<lambda>_. cap) rva) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rva \<sigma> x s'. \<lbrakk>ctes_of \<sigma> dest = Some rva; ccap_relation cap (val x); (\<sigma>, x) \<in> rf_sr; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) rva); 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>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rva \<sigma> x s'. \<lbrakk>ctes_of \<sigma> dest = Some rva; ccap_relation cap (val x); (\<sigma>, x) \<in> rf_sr; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) rva); 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', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>rva \<sigma> x s'. \<lbrakk>ctes_of \<sigma> dest = Some rva; ccap_relation cap (val x); (\<sigma>, x) \<in> rf_sr; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) rva); 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 dest) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> rva = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> (s', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y))) (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace s') (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x))) \<and> cmap_relation (map_to_eps (ksPSpace s')) (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_ntfns (ksPSpace s')) (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x))))) \<and> cmap_relation (map_to_pdes (ksPSpace s')) (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace s')) (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace s')) (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x))) \<and> cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues s') \<and> zero_ranges_are_zero (gsUntypedZeroRanges s') (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x)) (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') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> 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>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y))) ((cslift x)(cte_Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. val x) cte')) 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') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> 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>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y))) ((cslift x)(cte_Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. val x) cte')) cte_Ptr ccte_relation
 2. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> 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>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> 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>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>; ksPSpace s' = ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)\<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') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> 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>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>; ksPSpace s' = ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)\<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>)) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> 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>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x))
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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 (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data_device (ksPSpace s') p)) (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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x))
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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 (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data_device (ksPSpace s') p)) (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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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 s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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 (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data_device (ksPSpace s') p)) (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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x))
 3. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>ctes_of \<sigma> dest = Some (cte_to_H y); ccap_relation cap (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y)); 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'; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cslift x (cte_Ptr dest) = Some cte'; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte' = Some y; cmap_relation (map_to_eps (ksPSpace s')) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); c_valid_cte cte'; 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 (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data_device (ksPSpace s') p)) (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); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x))) (globals x))
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of \<sigma>_ dest = Some (cte_to_H y_); ccap_relation cap (val x_); ctes_of s'_ = (ctes_of \<sigma>_)(dest \<mapsto> cteCap_update (\<lambda>_. cap) (cte_to_H y_)); 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'_; cmap_relation (ctes_of \<sigma>_) (cslift x_) cte_Ptr ccte_relation; cslift x_ (cte_Ptr dest) = Some cte'_; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'_ = Some y_; cmap_relation (map_to_eps (ksPSpace s'_)) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); c_valid_cte cte'_; 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 (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>_)) p) (map_to_user_data_device (ksPSpace s'_) p)) (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_); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'_)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals 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>_) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x_))) (globals x_)) \<and> cmachine_state_relation (ksMachineState \<sigma>_) (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr dest\<rightarrow>[''cap_C''])) (val x_))) (globals x_)) proof (prove)
goal (1 subgoal):
 1. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. ccap_relation cap (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ctes_of s dest = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. ccap_relation cap (val s)}}