theory Retype_C

lemma pspace_no_overlap_induce_user_data:
  "\<lbrakk>cpspace_relation (ksPSpace (s::kernel_state)) (underlying_memory (ksMachineState s)) hp;
    pspace_aligned' s; clift hp xa = Some (v::user_data_C);
    is_aligned ptr bits; bits < word_bits;
    pspace_no_overlap' ptr bits s\<rbrakk>
     \<Longrightarrow> {ptr_val xa..+size_of TYPE(user_data_C)} \<inter> {ptr..+2 ^ bits} = {}" apply (clarsimp simp:cpspace_relation_def) apply (clarsimp simp:cmap_relation_def size_of_def) apply (subgoal_tac "xa\<in>Ptr ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState 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 heap_to_user_data_def projectKO_opt_user_data map_comp_def
                 split: option.splits kernel_object.splits) apply (frule(1) pspace_no_overlapD') apply (clarsimp simp: word_bits_def) apply (subst intvl_range_conv[where bits = 12,simplified]) apply (drule(1) pspace_alignedD') apply (simp add:objBits_simps archObjSize_def pageBits_def split:arch_kernel_object.split_asm) apply (clarsimp elim!:is_aligned_weaken) apply (subst intvl_range_conv, simp, simp) apply (clarsimp simp: field_simps) apply (simp add: p_assoc_help) apply (clarsimp simp: objBits_simps archObjSize_def pageBits_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..+4096} \<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..+4096} \<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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4096} \<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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState 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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState 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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4096} \<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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4096} \<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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4096} \<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> PTR(user_data_C) ` dom (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))\<rbrakk> \<Longrightarrow> {ptr_val xa..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData\<rbrakk> \<Longrightarrow> {x..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; {x..x + 2 ^ objBitsKO KOUserData - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> {x..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> {x..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> is_aligned x 12
 2. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 3. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> {x..0xFFF + x} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> is_aligned x 12
 2. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 3. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> {x..0xFFF + x} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 2. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> {x..0xFFF + x} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> {x..0xFFF + x} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> {x..0xFFF + x} \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + 2 ^ objBitsKO KOUserData - 1 \<longrightarrow> \<not> x \<le> x + 2 ^ objBitsKO KOUserData - 1; ptr \<le> x + 0xFFF; x \<le> x + 0xFFF; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<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 = PTR(user_data_C) x; pspace_aligned' s; clift hp (PTR(user_data_C) x) = Some v; is_aligned ptr bits; bits < 32; pspace_no_overlap' ptr bits s; ksPSpace s x = Some KOUserData; ptr \<le> x + (2 ^ objBitsKO KOUserData - 1) \<longrightarrow> \<not> x \<le> x + (2 ^ objBitsKO KOUserData - 1); ptr \<le> x + 0xFFF; x \<le> x + 0xFFF; x \<le> ptr + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!