theory Retype_C

lemma pspace_no_overlap_induce_cte:
  "\<lbrakk>cpspace_relation (ksPSpace (s::kernel_state))
      (underlying_memory (ksMachineState s)) hp;
    pspace_aligned' s; clift hp xa = Some (v::cte_C);
    is_aligned ptr bits; bits < word_bits;
    pspace_no_overlap' ptr bits s\<rbrakk>
   \<Longrightarrow> {ptr_val xa..+size_of TYPE(cte_C)} \<inter> {ptr..+2 ^ bits} = {}" supply cteSizeBits_le_cte_level_bits[simp del] apply (clarsimp simp: cpspace_relation_def) apply (clarsimp simp: cmap_relation_def size_of_def) apply (subgoal_tac "xa\<in>cte_Ptr ` dom (ctes_of 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_cte map_comp_def
                 split: option.splits kernel_object.split_asm) apply (frule ctes_of_is_aligned) apply (simp add: objBits_simps) apply (drule ctes_of_ko_at_strong) apply simp apply (clarsimp simp: objBits_defs) apply (erule disjoint_subset) apply (frule(1) pspace_no_overlapD') apply (subst intvl_range_conv) apply simp apply (simp add: word_bits_def) apply (simp add: obj_range'_def) 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>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_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; 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..+16} \<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> cte_Ptr ` dom (ctes_of s)\<rbrakk> \<Longrightarrow> {ptr_val xa..+16} \<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> cte_Ptr ` dom (ctes_of 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> cte_Ptr ` dom (ctes_of 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> cte_Ptr ` dom (ctes_of s)\<rbrakk> \<Longrightarrow> {ptr_val xa..+16} \<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> cte_Ptr ` dom (ctes_of s)\<rbrakk> \<Longrightarrow> {ptr_val xa..+16} \<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> cte_Ptr ` dom (ctes_of s)\<rbrakk> \<Longrightarrow> {ptr_val xa..+16} \<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> cte_Ptr ` dom (ctes_of s)\<rbrakk> \<Longrightarrow> {ptr_val xa..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (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 v \<Rightarrow> projectKO_opt v) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = cte_Ptr x; ctes_of s x = Some y\<rbrakk> \<Longrightarrow> {x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (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 v \<Rightarrow> projectKO_opt v) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = cte_Ptr x; ctes_of s x = Some y; is_aligned x (objBits y)\<rbrakk> \<Longrightarrow> {x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (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 v \<Rightarrow> projectKO_opt v) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = cte_Ptr x; ctes_of s x = Some y; is_aligned x cteSizeBits\<rbrakk> \<Longrightarrow> {x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (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 v \<Rightarrow> projectKO_opt v) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = cte_Ptr x; is_aligned x cteSizeBits\<rbrakk> \<Longrightarrow> is_aligned x cteSizeBits
 2. \<And>x y. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (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 v \<Rightarrow> projectKO_opt v) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = cte_Ptr x; is_aligned x cteSizeBits; \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {x..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko\<rbrakk> \<Longrightarrow> {x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; carray_map_relation pdBits (\<lambda>k. case ksPSpace s k of None \<Rightarrow> None | Some v \<Rightarrow> projectKO_opt v) (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 v \<Rightarrow> projectKO_opt v) (h_t_valid (hrs_htd hp) c_guard) pt_Ptr; xa = cte_Ptr x; is_aligned x cteSizeBits; \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {x..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko\<rbrakk> \<Longrightarrow> {x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {x..+16} \<subseteq> obj_range' ptra ko\<rbrakk> \<Longrightarrow> {x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko\<rbrakk> \<Longrightarrow> obj_range' ptra ko \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptra ko \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> is_aligned ptr bits
 2. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptra ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptra ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ptra ko. \<lbrakk>pspace_aligned' s; clift hp (cte_Ptr x) = Some v; is_aligned ptr bits; bits < word_bits; pspace_no_overlap' ptr bits s; 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 = cte_Ptr x; is_aligned x 4; ksPSpace s ptra = Some ko; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptra ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {} proof (prove)
goal:
No subgoals!