theory CSpace_C

lemma ccorres_updateMDB_const [corres]:
  fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> mdb_node_C"
  shows "ccorres dc xfdc (\<lambda>_. dest \<noteq> 0)
        ({s. cmdbnode_relation m (val s)} \<inter> {s. ptr s = Ptr dest}) hs
        (updateMDB dest (const m))
        (Basic
  (\<lambda>s. globals_update
   (t_hrs_'_update
     (hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cteMDBNode_C''])) (val s)))) s))" unfolding updateMDB_def apply (cinitlift ptr) apply (erule ssubst) apply (rule ccorres_gen_asm [where G = \<top>, simplified]) apply (simp only: Let_def) apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some cte" in ccorres_from_vcg [where P' = "{s. cmdbnode_relation m (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 (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps
     Let_def cpspace_relation_def
     cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) apply (rule conjI) apply (erule (3) cspace_cte_relation_upd_mdbI) apply (erule_tac t = s' in ssubst) apply (simp add: heap_to_user_data_def) apply (rule conjI) apply (erule (1) setCTE_tcb_case) apply (simp add: carch_state_relation_def cmachine_state_relation_def
                    typ_heap_simps) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. dest \<noteq> 0) ({s. cmdbnode_relation m (val s)} \<inter> {s. ptr s = cte_Ptr dest}) hs (updateMDB dest (const m)) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(\<acute>ptr\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. dest \<noteq> 0) ({s. cmdbnode_relation m (val s)} \<inter> {s. ptr s = cte_Ptr dest}) hs (let slot = dest in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (const m mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(\<acute>ptr\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. rv = cte_Ptr dest \<Longrightarrow> ccorres dc xfdc (\<lambda>_. dest \<noteq> 0) {s. cmdbnode_relation m (val s)} hs (let slot = dest in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (const m mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(rv\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. ccorres dc xfdc (\<lambda>_. dest \<noteq> 0) {s. cmdbnode_relation m (val s)} hs (let slot = dest in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (const m mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. dest \<noteq> 0 \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. cmdbnode_relation m (val s)} hs (let slot = dest in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (const m mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. dest \<noteq> 0 \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. cmdbnode_relation m (val s)} hs (if False then return () else do cte <- getCTE dest;
mdb <- return (cteMDBNode cte);
mdb' <- return (const m mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE dest
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (1 subgoal):
 1. 0 < dest \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. cmdbnode_relation m (val s)} hs (do cte <- getCTE dest;
setCTE dest (cteMDBNode_update (\<lambda>_. m) cte)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val))) proof (prove)
goal (2 subgoals):
 1. 0 < dest \<Longrightarrow> ccorres dc xfdc ?Q29 ?Q'29 hs (do cte <- getCTE dest;
setCTE dest (cteMDBNode_update (\<lambda>_. m) cte)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val)))
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (val s)}\<rbrakk> \<Longrightarrow> ?Q29 s \<and> s' \<in> ?Q'29 proof (prove)
goal (2 subgoals):
 1. \<And>cte. 0 < dest \<Longrightarrow> ccorres dc xfdc (?P32 cte) (?P'32 cte) hs (setCTE dest (cteMDBNode_update (\<lambda>_. m) cte)) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val)))
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (val s)}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> ?P32 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'32 (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>cte. 0 < dest \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ctes_of \<sigma> dest = Some cte \<and> s \<in> {s. cmdbnode_relation m (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val)) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteMDBNode_update (\<lambda>_. m) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma>. 0 < dest \<Longrightarrow> \<Gamma>\<turnstile> {s. ctes_of \<sigma> dest = Some cte \<and> s \<in> {s. cmdbnode_relation m (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val)) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteMDBNode_update (\<lambda>_. m) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma>. 0 < dest \<Longrightarrow> \<Gamma>\<turnstile> (?P'38 cte \<sigma>) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) \<acute>val)) {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteMDBNode_update (\<lambda>_. m) cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>cte \<sigma>. 0 < dest \<Longrightarrow> {s. ctes_of \<sigma> dest = Some cte \<and> s \<in> {s. cmdbnode_relation m (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'38 cte \<sigma>
 3. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma>. 0 < dest \<Longrightarrow> {s. ctes_of \<sigma> dest = Some cte \<and> s \<in> {s. cmdbnode_relation m (val s)} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCTE dest (cteMDBNode_update (\<lambda>_. m) cte) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val s)))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val s)))) s))}
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some cte; cmdbnode_relation m (val x); (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setCTE dest (cteMDBNode_update (\<lambda>_. m) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x s'. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some cte; cmdbnode_relation m (val x); (\<sigma>, x) \<in> rf_sr; ((), s') \<in> fst (setCTE dest (?cte52 cte \<sigma> x) \<sigma>); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> ?cte52 cte \<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 (cteMDBNode_update (\<lambda>_. m) cte) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x s'. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some cte; cmdbnode_relation m (val x); (\<sigma>, x) \<in> rf_sr; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) 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'\<rbrakk> \<Longrightarrow> case ((), s') of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>cte \<sigma> x s'. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some cte; cmdbnode_relation m (val x); (\<sigma>, x) \<in> rf_sr; s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) 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'; \<exists>cte'. cslift x (cte_Ptr dest) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> case ((), s') of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x)))) x) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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> cteMDBNode_update (\<lambda>_. m) (cte_to_H y))) ((cslift x)(cte_Ptr dest \<mapsto> cteMDBNode_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 (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_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>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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> cteMDBNode_update (\<lambda>_. m) (cte_to_H y))) ((cslift x)(cte_Ptr dest \<mapsto> cteMDBNode_C_update (\<lambda>_. val x) cte')) cte_Ptr ccte_relation
 2. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_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>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); s' = \<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>; ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState s') (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_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>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (\<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 (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'\<rparr>)) (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_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>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (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 (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x))
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (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
 2. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (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> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x))
 3. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x s' cte' y. \<lbrakk>0 < dest; ctes_of \<sigma> dest = Some (cte_to_H y); cmdbnode_relation m (val x); ctes_of s' = (ctes_of \<sigma>)(dest \<mapsto> cteMDBNode_update (\<lambda>_. m) (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 (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> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr dest\<rightarrow>[''cteMDBNode_C''])) (val x))) (globals x))
 2. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>0 < dest; (s, s') \<in> rf_sr; True; s' \<in> {s. cmdbnode_relation m (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. cmdbnode_relation m (val s)}} proof (prove)
goal:
No subgoals!