theory Retype_C

lemma pspace_no_overlap_induce_pte:
  "\<lbrakk>cpspace_relation (ksPSpace (s::kernel_state)) (underlying_memory (ksMachineState s)) hp;
    pspace_aligned' s; clift hp xa = Some (v::pte_C);
    is_aligned ptr bits; bits < word_bits;
    pspace_no_overlap' ptr bits s\<rbrakk>
     \<Longrightarrow> {ptr_val xa..+size_of TYPE(pte_C)} \<inter> {ptr..+2 ^ bits} = {}" apply (clarsimp simp:cpspace_relation_def) apply (clarsimp simp:cmap_relation_def) apply (subgoal_tac "xa\<in>pte_Ptr ` dom (map_to_ptes (ksPSpace s))") prefer 2 apply (simp add:domI) apply (thin_tac "S = dom K" for S K)+ apply (thin_tac "\<forall>x\<in> S. K x" for S K)+ apply (clarsimp simp: image_def projectKO_opt_pte map_comp_def
                 split: option.splits kernel_object.split_asm) apply (frule(1) pspace_no_overlapD') apply (subst intvl_range_conv) apply simp apply (simp add: word_bits_def) apply (subst intvl_range_conv[where bits = 2,simplified]) apply (drule(1) pspace_alignedD') apply (simp add: objBits_simps archObjSize_def pteBits_def
                split:arch_kernel_object.split_asm) apply (simp add: word_bits_conv) apply (simp add: objBits_simps archObjSize_def  pteBits_def
              split:arch_kernel_object.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> ptr_span xa \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cmap_relation (ctes_of s) (clift hp) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) hp; cmap_relation (map_to_eps (ksPSpace s)) (clift hp) ep_Ptr (cendpoint_relation (clift hp)); cmap_relation (map_to_ntfns (ksPSpace s)) (clift hp) ntfn_Ptr (cnotification_relation (clift hp)); cmap_relation (map_to_pdes (ksPSpace s)) (clift hp) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift hp) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift hp) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; cpspace_device_data_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; cte_Ptr ` dom (ctes_of s) = dom (clift hp); \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); pde_Ptr ` dom (map_to_pdes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); pte_Ptr ` dom (map_to_ptes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); ap_Ptr ` dom (map_to_asidpools (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; cte_Ptr ` dom (ctes_of s) = dom (clift hp); \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); pde_Ptr ` dom (map_to_pdes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); pte_Ptr ` dom (map_to_ptes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); ap_Ptr ` dom (map_to_asidpools (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x))); xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {}
 2. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; cte_Ptr ` dom (ctes_of s) = dom (clift hp); \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); pde_Ptr ` dom (map_to_pdes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); pte_Ptr ` dom (map_to_ptes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); ap_Ptr ` dom (map_to_asidpools (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; cte_Ptr ` dom (ctes_of s) = dom (clift hp); \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); pde_Ptr ` dom (map_to_pdes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); pte_Ptr ` dom (map_to_ptes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); ap_Ptr ` dom (map_to_asidpools (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s))
 2. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; cte_Ptr ` dom (ctes_of s) = dom (clift hp); \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); pde_Ptr ` dom (map_to_pdes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); pte_Ptr ` dom (map_to_ptes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); ap_Ptr ` dom (map_to_asidpools (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x))); xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; cte_Ptr ` dom (ctes_of s) = dom (clift hp); \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); pde_Ptr ` dom (map_to_pdes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); pte_Ptr ` dom (map_to_ptes (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); ap_Ptr ` dom (map_to_asidpools (ksPSpace s)) = dom (clift hp); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) = dom (clift hp); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x))); xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; \<forall>x\<in>dom (ctes_of s). ccte_relation (the (ctes_of s x)) (the (clift hp (cte_Ptr x))); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (clift hp (tcb_ptr_to_ctcb_ptr x))); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation (clift hp) (the (map_to_eps (ksPSpace s) x)) (the (clift hp (ep_Ptr x))); \<forall>x\<in>dom (map_to_ntfns (ksPSpace s)). cnotification_relation (clift hp) (the (map_to_ntfns (ksPSpace s) x)) (the (clift hp (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_pdes (ksPSpace s)). cpde_relation (the (map_to_pdes (ksPSpace s) x)) (the (clift hp (pde_Ptr x))); \<forall>x\<in>dom (map_to_ptes (ksPSpace s)). cpte_relation (the (map_to_ptes (ksPSpace s) x)) (the (clift hp (pte_Ptr x))); \<forall>x\<in>dom (map_to_asidpools (ksPSpace s)). casid_pool_relation (the (map_to_asidpools (ksPSpace s) x)) (the (clift hp (ap_Ptr x))); \<forall>x\<in>dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_relation (the (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)) x)) (the (clift hp (PTR(user_data_device_C) x))); xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; clift hp xa = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; cpspace_pde_array_relation (ksPSpace s) hp; cpspace_pte_array_relation (ksPSpace s) hp; xa \<in> pte_Ptr ` dom (map_to_ptes (ksPSpace s))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y\<rbrakk> \<Longrightarrow> {x..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> is_aligned ptr bits
 2. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..+4} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..+4} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..+4} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..3 + x} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}; is_aligned x (objBitsKO (KOArch x8))\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..3 + x} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..3 + x} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y x8. \<lbrakk>carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pd_Ptr; carray_map_relation ptBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some x \<Rightarrow> projectKO_opt x) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = pte_Ptr x; pspace_aligned' s; clift hp (pte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some (KOArch x8); (case x8 of KOPTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some y; {x..x + 2 ^ objBitsKO (KOArch x8) - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..3 + x} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal:
No subgoals!