theory CSpace_C

lemma ccorres_updateMDB_set_mdbNext [corres]:
  "src=src' \<Longrightarrow>
   ccorres dc xfdc ((\<lambda>_. src \<noteq> 0 \<and> (dest\<noteq>0 \<longrightarrow> is_aligned dest 3)))
  ({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter>
   {s. v32_' s = dest}) []
  (updateMDB src (mdbNext_update (\<lambda>_. dest)))
  (Call mdb_node_ptr_set_mdbNext_'proc)" unfolding updateMDB_def apply (hypsubst) 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 [where P = "\<lambda>cte s. ctes_of s src' = Some cte" and
     P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>)"]) apply (rule ccorres_from_spec_modifies_heap) apply (rule mdb_node_ptr_set_mdbNext_spec) apply (rule mdb_node_ptr_set_mdbNext_modifies) apply simp apply clarsimp apply (rule rf_sr_cte_at_valid) apply simp apply (erule ctes_of_cte_at) apply assumption apply clarsimp apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI [rotated]) apply (clarsimp simp add: rf_sr_def cstate_relation_def
      Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def
     cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
     typ_heap_simps') apply (rule conjI) apply (erule (2) cspace_cte_relation_upd_mdbI) apply (simp add: cmdbnode_relation_def) subgoal for _ s' by (cases "v32_' s' = 0"; simp) apply (erule_tac t = s'a in ssubst) apply simp apply (rule conjI) apply (erule (1) setCTE_tcb_case) subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
                     typ_heap_simps h_t_valid_clift_Some_iff) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src = src' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. src \<noteq> 0 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (updateMDB src (mdbNext_update (\<lambda>_. dest))) (Call mdb_node_ptr_set_mdbNext_'proc) proof (prove)
goal (1 subgoal):
 1. src = src' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. src \<noteq> 0 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (let slot = src in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (mdbNext_update (\<lambda>_. dest) mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (Call mdb_node_ptr_set_mdbNext_'proc) proof (prove)
goal (1 subgoal):
 1. src = src' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. src' \<noteq> 0 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (let slot = src' in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (mdbNext_update (\<lambda>_. dest) mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (Call mdb_node_ptr_set_mdbNext_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src = src'; src' \<noteq> 0 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (let slot = src' in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (mdbNext_update (\<lambda>_. dest) mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) (Call mdb_node_ptr_set_mdbNext_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src = src'; src' \<noteq> 0 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (if False then return () else do cte <- getCTE src';
mdb <- return (cteMDBNode cte);
mdb' <- return (mdbNext_update (\<lambda>_. dest) mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE src'
od) (Call mdb_node_ptr_set_mdbNext_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (do cte <- getCTE src';
setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte)
od) (Call mdb_node_ptr_set_mdbNext_'proc) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q11 ?Q'11 [] (do cte <- getCTE src';
setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte)
od) (Call mdb_node_ptr_set_mdbNext_'proc)
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> ?Q11 s \<and> s' \<in> ?Q'11 proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>s. ctes_of s src' = Some cte) (\<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>) [] (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte)) (Call mdb_node_ptr_set_mdbNext_'proc)
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>cte. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. ?P16 cte s\<rbrace> Call mdb_node_ptr_set_mdbNext_'proc {t. ?Q16 cte s t}
 2. \<And>cte. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'proc {t. t may_only_modify_globals s in [t_hrs]}
 3. \<And>cte f s. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> xfdc (globals_update f s) = xfdc s
 4. \<And>cte s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ?P16 cte s'
 5. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; ?Q16 cte s' t'\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 6. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>cte. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'proc {t. t may_only_modify_globals s in [t_hrs]}
 2. \<And>cte f s. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> xfdc (globals_update f s) = xfdc s
 3. \<And>cte s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']
 4. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 5. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>cte f s. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3)\<rbrakk> \<Longrightarrow> xfdc (globals_update f s) = xfdc s
 2. \<And>cte s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']
 3. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 4. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>cte s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']
 2. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>cte s s'. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr src'
 2. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>cte s s'. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'\<rbrakk> \<Longrightarrow> cte_wp_at' (?P29 cte s s') (ptr_val (cte_Ptr src')) (?s29 cte s s')
 2. \<And>cte s s'. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'\<rbrakk> \<Longrightarrow> (?s29 cte s s', s') \<in> rf_sr
 3. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 4. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>cte s s'. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'\<rbrakk> \<Longrightarrow> cte_wp_at' (?P29 cte s s') src' (?s29 cte s s')
 2. \<And>cte s s'. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'\<rbrakk> \<Longrightarrow> (?s29 cte s s', s') \<in> rf_sr
 3. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 4. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>cte s s'. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'\<rbrakk> \<Longrightarrow> (s, s') \<in> rf_sr
 2. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>cte s s' t'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); ctes_of s src' = Some cte; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>; (s, s') \<in> rf_sr; \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr> \<and> t_hrs_' (globals t') = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cparent (mdb_node_ptr_' s') [''cteMDBNode_C'']))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>(rv, t)\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte) s). (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc t')
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>cte s s' t' mdb_node. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cte_Ptr src'))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cte_Ptr src'))))) (t_hrs_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (cteMDBNode cte)) cte) s). case x of (rv, t) \<Rightarrow> (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cte_Ptr src'))))) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>cte s s' t' mdb_node. \<lbrakk>src = src'; ctes_of s src' = Some cte; (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s' (cte_Ptr src'))))\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cte_Ptr src'))))) (t_hrs_' (globals s')); \<exists>cte'. cslift s' (cte_Ptr src') = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (cteMDBNode cte)) cte) s). case x of (rv, t) \<Rightarrow> (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s' (cte_Ptr src'))))) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)) s). case x of (rv, t) \<Rightarrow> (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ((), s'a) \<in> fst (setCTE src' (?cte53 s s' t' mdb_node cte' y) s); s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> ?cte53 s s' t' mdb_node cte' y); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setCTE src' (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)) s). case x of (rv, t) \<Rightarrow> (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); (s, s') \<in> rf_sr; 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a\<rbrakk> \<Longrightarrow> case ((), s'a) of (rv, t) \<Rightarrow> (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y))) ((cslift s')(cte_Ptr src' \<mapsto> cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s'a)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread s = ksCurThread s'a \<and> ksIdleThread s = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cte_array_relation s'a (globals s') \<and> gsUserPages s = gsUserPages s'a \<and> gsCNodes s = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain s = ksCurDomain s'a \<and> ksDomainTime s = ksDomainTime s'a
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y))) ((cslift s')(cte_Ptr src' \<mapsto> cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) cte_Ptr ccte_relation
 2. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s'a)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread s = ksCurThread s'a \<and> ksIdleThread s = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cte_array_relation s'a (globals s') \<and> gsUserPages s = gsUserPages s'a \<and> gsCNodes s = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain s = ksCurDomain s'a \<and> ksDomainTime s = ksDomainTime s'a
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmdbnode_relation (mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) mdb_node
 2. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s'a)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread s = ksCurThread s'a \<and> ksIdleThread s = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cte_array_relation s'a (globals s') \<and> gsUserPages s = gsUserPages s'a \<and> gsCNodes s = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain s = ksCurDomain s'a \<and> ksDomainTime s = ksDomainTime s'a
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y)) = mdbNext_update (\<lambda>_. v32_' s' && ~~ mask 3) (mdb_node_to_H (cteMDBNode_CL y))
 2. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s'a)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread s = ksCurThread s'a \<and> ksIdleThread s = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cte_array_relation s'a (globals s') \<and> gsUserPages s = gsUserPages s'a \<and> gsCNodes s = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain s = ksCurDomain s'a \<and> ksDomainTime s = ksDomainTime s'a
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src = src'; ctes_of s_ src' = Some (cte_to_H y_); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node_ = cteMDBNode_CL y_\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t'_) = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node_) cte'_)) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'_; cte_lift cte'_ = Some y_; c_valid_cte cte'_; s'a_ = s_\<lparr>ksPSpace := ksPSpace s'a_\<rparr>; ctes_of s'a_ = (ctes_of s_)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y_))) (cte_to_H y_)); map_to_eps (ksPSpace s_) = map_to_eps (ksPSpace s'a_); map_to_ntfns (ksPSpace s_) = map_to_ntfns (ksPSpace s'a_); map_to_pdes (ksPSpace s_) = map_to_pdes (ksPSpace s'a_); map_to_ptes (ksPSpace s_) = map_to_ptes (ksPSpace s'a_); map_to_asidpools (ksPSpace s_) = map_to_asidpools (ksPSpace s'a_); map_to_user_data (ksPSpace s_) = map_to_user_data (ksPSpace s'a_); map_to_user_data_device (ksPSpace s_) = map_to_user_data_device (ksPSpace s'a_); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s_) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a_); \<forall>T p. typ_at' T p s_ = typ_at' T p s'a_; cmap_relation (map_to_tcbs (ksPSpace s_)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a_)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a_)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a_)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a_)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a_)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s_)) p) (map_to_user_data (ksPSpace s'a_) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a_) (underlying_memory (ksMachineState s_))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a_)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a_)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s_); zero_ranges_are_zero (gsUntypedZeroRanges s_) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s_); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s_); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s_); cinterrupt_relation (ksInterruptState s_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s_) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s_) (globals s'); cmachine_state_relation (ksMachineState s_) (globals s'); cte_array_relation s_ (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a_)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s_, gsCNodes s_); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s_); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s_; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s_); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s_); ksDomainTime_' (globals s') = ksDomainTime s_\<rbrakk> \<Longrightarrow> mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y_)) = mdbNext_update (\<lambda>_. v32_' s' && ~~ mask 3) (mdb_node_to_H (cteMDBNode_CL y_)) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; s'a = s\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s'a)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread s = ksCurThread s'a \<and> ksIdleThread s = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cte_array_relation s'a (globals s') \<and> gsUserPages s = gsUserPages s'a \<and> gsCNodes s = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain s = ksCurDomain s'a \<and> ksDomainTime s = ksDomainTime s'a
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>))) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>))) p) (map_to_user_data (ksPSpace (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (underlying_memory (ksMachineState (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> zero_ranges_are_zero (gsUntypedZeroRanges (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> ksCurThread s = ksCurThread (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> ksIdleThread s = ksIdleThread (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> cinterrupt_relation (ksInterruptState (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cte_array_relation (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) (globals s') \<and> gsUserPages s = gsUserPages (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> gsCNodes s = gsCNodes (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> cdom_schedule_relation (kernel_state.ksDomSchedule (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> ksCurDomain s = ksCurDomain (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> ksDomainTime s = ksDomainTime (s\<lparr>ksPSpace := ksPSpace s'a\<rparr>)
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> carch_state_relation (ksArchState s) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>)
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
 2. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>)
 3. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' mdb_node cte' y s'a. \<lbrakk>src = src'; ctes_of s src' = Some (cte_to_H y); 0 < src'; 0 < v32_' s' \<longrightarrow> is_aligned (v32_' s') 3; mdb_node_ptr_' s' = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'; mdb_node_lift mdb_node = cteMDBNode_CL y\<lparr>mdbNext_CL := v32_' s' && ~~ mask 3\<rparr>; t_hrs_' (globals t') = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s')); cslift s' (cte_Ptr src') = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of s'a = (ctes_of s)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s') (mdb_node_to_H (cteMDBNode_CL y))) (cte_to_H y)); map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p s = typ_at' T p s'a; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>) \<and> cmachine_state_relation (ksMachineState s) (globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node) cte')) (t_hrs_' (globals s'))\<rparr>)
 2. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src = src'; ctes_of s_ src' = Some (cte_to_H y_); 0 < src'; 0 < v32_' s'_ \<longrightarrow> is_aligned (v32_' s'_) 3; mdb_node_ptr_' s'_ = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C'']); dest = v32_' s'_; mdb_node_lift mdb_node_ = cteMDBNode_CL y_\<lparr>mdbNext_CL := v32_' s'_ && ~~ mask 3\<rparr>; t_hrs_' (globals t'_) = hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node_) cte'_)) (t_hrs_' (globals s'_)); cslift s'_ (cte_Ptr src') = Some cte'_; cte_lift cte'_ = Some y_; c_valid_cte cte'_; ctes_of s'a_ = (ctes_of s_)(src' \<mapsto> cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. v32_' s'_) (mdb_node_to_H (cteMDBNode_CL y_))) (cte_to_H y_)); map_to_eps (ksPSpace s_) = map_to_eps (ksPSpace s'a_); map_to_ntfns (ksPSpace s_) = map_to_ntfns (ksPSpace s'a_); map_to_pdes (ksPSpace s_) = map_to_pdes (ksPSpace s'a_); map_to_ptes (ksPSpace s_) = map_to_ptes (ksPSpace s'a_); map_to_asidpools (ksPSpace s_) = map_to_asidpools (ksPSpace s'a_); map_to_user_data (ksPSpace s_) = map_to_user_data (ksPSpace s'a_); map_to_user_data_device (ksPSpace s_) = map_to_user_data_device (ksPSpace s'a_); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s_) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a_); \<forall>T p. typ_at' T p s_ = typ_at' T p s'a_; cmap_relation (ctes_of s_) (cslift s'_) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s_)) (cslift s'_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s'a_)) (cslift s'_) ep_Ptr (cendpoint_relation (cslift s'_)); cmap_relation (map_to_ntfns (ksPSpace s'a_)) (cslift s'_) ntfn_Ptr (cnotification_relation (cslift s'_)); cmap_relation (map_to_pdes (ksPSpace s'a_)) (cslift s'_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a_)) (cslift s'_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a_)) (cslift s'_) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s_)) p) (map_to_user_data (ksPSpace s'a_) p)) (cslift s'_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a_) (underlying_memory (ksMachineState s_))) (cslift s'_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a_)) (c_h_t_valid s'_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a_)) (c_h_t_valid s'_) pt_Ptr; cready_queues_relation (cslift s'_) (ksReadyQueues_' (globals s'_)) (ksReadyQueues s_); zero_ranges_are_zero (gsUntypedZeroRanges s_) (t_hrs_' (globals s'_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s'_)) (ksReadyQueuesL1Bitmap s_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s'_)) (ksReadyQueuesL2Bitmap s_); ksCurThread_' (globals s'_) = tcb_ptr_to_ctcb_ptr (ksCurThread s_); ksIdleThread_' (globals s'_) = tcb_ptr_to_ctcb_ptr (ksIdleThread s_); cinterrupt_relation (ksInterruptState s_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s'_)); cscheduler_action_relation (ksSchedulerAction s_) (ksSchedulerAction_' (globals s'_)); carch_state_relation (ksArchState s_) (globals s'_); cmachine_state_relation (ksMachineState s_) (globals s'_); cte_array_relation s_ (globals s'_); cvariable_array_map_relation (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a_)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'_))); apsnd fst (ghost'state_' (globals s'_)) = (gsUserPages s_, gsCNodes s_); ghost_size_rel (ghost'state_' (globals s'_)) (gsMaxObjectSize s_); ksWorkUnitsCompleted_' (globals s'_) = ksWorkUnitsCompleted s_; s'_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s'_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s'_) = word_of_nat (ksDomScheduleIdx s_); ksCurDomain_' (globals s'_) = UCAST(8 \<rightarrow> 32) (ksCurDomain s_); ksDomainTime_' (globals s'_) = ksDomainTime s_\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s_) (globals s'_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node_) cte'_)) (t_hrs_' (globals s'_))\<rparr>) \<and> cmachine_state_relation (ksMachineState s_) (globals s'_\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr src') (cteMDBNode_C_update (\<lambda>_. mdb_node_) cte'_)) (t_hrs_' (globals s'_))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>src = src'; 0 < src' \<and> (0 < dest \<longrightarrow> is_aligned dest 3); (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s src' = Some cte \<longrightarrow> ctes_of s src' = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src') = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr src'\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>} proof (prove)
goal:
No subgoals!