theory Untyped_DR

lemma freeMemory_dcorres:
  "is_aligned ptr bits \<Longrightarrow> 2 \<le> bits \<Longrightarrow> bits < word_bits \<Longrightarrow>
   dcorres dc (\<lambda>_. True)
     (pspace_no_overlap_range_cover ptr bits and valid_objs and valid_etcbs)
     (return rv) (do_machine_op (freeMemory ptr bits))" apply (clarsimp simp add: corres_underlying_def split_def return_def) apply (rename_tac s t) apply (drule_tac P="(=) s" and
                   Q="%_ u. (\<exists>ms. u=s\<lparr>machine_state := ms\<rparr>) \<and>
                            (\<forall>p\<in>UNIV-{ptr..ptr + 2 ^ bits - 1}.
                                underlying_memory (machine_state s) p =
                                underlying_memory (machine_state u) p)"
                in use_valid) apply (simp add: do_machine_op_def split_def) apply wp apply (clarsimp simp: freeMemory_def mapM_x_storeWord_step[simplified word_size_bits_def]
                          intvl_range_conv') apply (rule conjI, fastforce) apply clarsimp apply (erule use_valid[where P=P and Q="%_. P" for P]) apply wp apply (clarsimp simp: is_aligned_no_wrap' of_nat_less_pow_32 word_bits_def
                           x_power_minus_1 word_plus_mono_right) apply (rule refl) apply (rule refl) apply (clarsimp simp: transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp simp: transform_objects_def map_add_def) apply (clarsimp simp: option_map_def split: option.splits) apply (clarsimp simp: transform_object_def transform_tcb_def
                 split: Structures_A.kernel_object.split option.splits) apply (rename_tac s ms tref etcb tcb) apply (clarsimp simp: restrict_map_def split: if_split_asm) apply (frule(1) valid_etcbs_tcb_etcb) apply (case_tac "\<not> is_arch_page_cap (tcb_ipcframe tcb)") apply (erule transform_full_intent_no_ipc_buffer) apply (clarsimp simp: is_arch_page_cap_def2) apply (simp add: valid_objs_def) apply (drule_tac x=tref in bspec, clarsimp+) apply (clarsimp simp: valid_obj_def valid_tcb_def) 
    (* FIXME: extract a sensible lemma for that *)
   apply (drule_tac x="(tcb_ipcframe, tcb_ipcframe_update,
                        \<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap)" in bspec) apply (simp add: ran_tcb_cap_cases) apply clarsimp apply (thin_tac "case_option x y z" for x y z) apply (clarsimp simp add: valid_ipc_buffer_cap_def is_nondevice_page_cap_def split: bool.split_asm) apply (drule valid_page_cap_imp_valid_buf) apply (frule_tac transform_full_intent_machine_state_eq, simp_all) apply clarsimp apply (erule_tac x=p in bspec) apply (frule is_aligned_no_overflow') apply (clarsimp simp: pspace_no_overlap_def typ_at_eq_kheap_obj obj_at_def
                        mask_2pm1[symmetric]) apply (erule_tac x="(p && ~~ mask (pageBitsForSize sz))" in allE) apply clarsimp apply (thin_tac "length xs = y" for xs y) apply (erule impE) apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help) apply (erule order_trans[OF word_and_le2]) apply (erule impE) apply (rule_tac y = p in order_trans) apply simp apply (cut_tac ptr = p and n = "pageBitsForSize sz" in word_neg_and_le) apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help) apply (thin_tac "x\<noteq>y" for x y) apply (erule notE)+ apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) apply (rule le_refl) apply (simp add:mask_def not_le pbfs_less_wb'[unfolded word_bits_def, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_no_overlap (up_aligned_area ptr bits) and valid_objs and valid_etcbs) (return rv) (do_machine_op (freeMemory ptr bits)) proof (prove)
goal (1 subgoal):
 1. \<And>b ba. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; ((), ba) \<in> fst (do_machine_op (freeMemory ptr bits) b); pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} b; valid_objs b; valid_etcbs b\<rbrakk> \<Longrightarrow> transform ba = transform b proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; ((), t) \<in> fst (do_machine_op (freeMemory ptr bits) s); pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_ u. (\<exists>ms. u = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state u) p)\<rbrace>
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do ms <- gets machine_state;
p <- select_f (freeMemory ptr bits ms);
modify (update_machine (snd p))
od \<lbrace>\<lambda>_ u. (\<exists>ms. u = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state u) p)\<rbrace>
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; s = sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr bits (machine_state sa)). (\<exists>ms. update_machine (snd x) sa = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state (update_machine (snd x) sa)) p)
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>sa b. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ((), b) \<in> fst (modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits then 0 else m x)) (machine_state sa))\<rbrakk> \<Longrightarrow> (\<exists>ms. update_machine b sa = update_machine ms sa) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state sa) p = underlying_memory b p)
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>sa b. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ((), b) \<in> fst (modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits then 0 else m x)) (machine_state sa))\<rbrakk> \<Longrightarrow> \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state sa) p = underlying_memory b p
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>sa b p. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ((), b) \<in> fst (modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits then 0 else m x)) (machine_state sa)); ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> underlying_memory (machine_state sa) p = underlying_memory b p
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (4 subgoals):
 1. \<And>sa b p. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. underlying_memory (machine_state sa) p = underlying_memory a p\<rbrace> modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits then 0 else m x)) \<lbrace>\<lambda>_ a. underlying_memory (machine_state sa) p = underlying_memory a p\<rbrace>
 2. \<And>sa b p. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> underlying_memory (machine_state sa) p = underlying_memory (machine_state sa) p
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 4. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (4 subgoals):
 1. \<And>sa b p s. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1; underlying_memory (machine_state sa) p = underlying_memory s p\<rbrakk> \<Longrightarrow> underlying_memory (machine_state sa) p = underlying_memory (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits then 0 else m x) s) p
 2. \<And>sa b p. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> underlying_memory (machine_state sa) p = underlying_memory (machine_state sa) p
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 4. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (3 subgoals):
 1. \<And>sa b p. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} sa; valid_objs sa; valid_etcbs sa; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> underlying_memory (machine_state sa) p = underlying_memory (machine_state sa) p
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 3. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> s = s
 2. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; (\<exists>ms. t = update_machine ms s) \<and> (\<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory (machine_state t) p)\<rbrakk> \<Longrightarrow> transform t = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s ms. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p\<rbrakk> \<Longrightarrow> transform_objects (update_machine ms s) = transform_objects s proof (prove)
goal (1 subgoal):
 1. \<And>s ms x. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p\<rbrakk> \<Longrightarrow> transform_objects (update_machine ms s) x = transform_objects s x proof (prove)
goal (1 subgoal):
 1. \<And>s ms x. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p\<rbrakk> \<Longrightarrow> (case (kheap s |` (- {idle_thread s})) x of None \<Rightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s})) x | Some xa \<Rightarrow> (Some \<circ> transform_object ms x ((ekheap s |` (- {idle_thread s})) x)) xa) = (case (kheap s |` (- {idle_thread s})) x of None \<Rightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s})) x | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state s) x ((ekheap s |` (- {idle_thread s})) x)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>s ms x x2. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; (kheap s |` (- {idle_thread s})) x = Some x2\<rbrakk> \<Longrightarrow> transform_object ms x ((ekheap s |` (- {idle_thread s})) x) x2 = transform_object (machine_state s) x ((ekheap s |` (- {idle_thread s})) x) x2 proof (prove)
goal (1 subgoal):
 1. \<And>s ms x x2a x2b. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; (kheap s |` (- {idle_thread s})) x = Some (TCB x2b); (ekheap s |` (- {idle_thread s})) x = Some x2a\<rbrakk> \<Longrightarrow> transform_full_intent ms x x2b = transform_full_intent (machine_state s) x x2b proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; (kheap s |` (- {idle_thread s})) tref = Some (TCB tcb); (ekheap s |` (- {idle_thread s})) tref = Some etcb\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); \<exists>etcb. ekheap s tref = Some etcb\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (2 subgoals):
 1. \<And>s ms tref etcb tcb. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); \<exists>etcb. ekheap s tref = Some etcb; \<not> is_arch_page_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb
 2. \<And>s ms tref etcb tcb. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); \<exists>etcb. ekheap s tref = Some etcb; \<not> \<not> is_arch_page_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); \<exists>etcb. ekheap s tref = Some etcb; \<not> \<not> is_arch_page_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_objs s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata)\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata)\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); valid_obj tref (TCB tcb) s\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr tref (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr tref (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (2 subgoals):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap) \<in> ran tcb_cap_cases
 2. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; case (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap) of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr tref (tcb_state tcb) (getF tcb))\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; case (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap) of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr tref (tcb_state tcb) (getF tcb))\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; s \<turnstile> ArchObjectCap (PageCap dev buf rights sz mapdata); is_nondevice_page_cap (ArchObjectCap (PageCap dev buf rights sz mapdata))\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev buf rights sz mapdata); valid_ipc_buffer_cap (ArchObjectCap (PageCap dev buf rights sz mapdata)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; s \<turnstile> ArchObjectCap (PageCap dev buf rights sz mapdata); is_nondevice_page_cap (ArchObjectCap (PageCap dev buf rights sz mapdata))\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; s \<turnstile> ArchObjectCap (PageCap False buf rights sz mapdata); is_nondevice_page_cap_arch (PageCap False buf rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False buf rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned buf (pageBitsForSize sz) \<and> typ_at (AArch (AUserData sz)) buf s\<rbrakk> \<Longrightarrow> transform_full_intent ms tref tcb = transform_full_intent (machine_state s) tref tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev buf rights sz mapdata. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False buf rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned buf (pageBitsForSize sz) \<and> typ_at (AArch (AUserData sz)) buf s\<rbrakk> \<Longrightarrow> \<forall>p. buf = p && ~~ mask (pageBitsForSize sz) \<longrightarrow> underlying_memory (machine_state s) p = underlying_memory ms p proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; \<forall>p\<in>UNIV - {ptr..ptr + 2 ^ bits - 1}. underlying_memory (machine_state s) p = underlying_memory ms p; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> underlying_memory (machine_state s) p = underlying_memory ms p proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> p \<in> UNIV - {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s ms tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; pspace_no_overlap {ptr..ptr + (2 ^ bits - 1)} s; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s; ptr \<le> ptr + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> p \<in> UNIV - {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; \<forall>x ko. kheap s x = Some ko \<longrightarrow> x \<le> ptr + mask bits \<longrightarrow> ptr \<le> x + mask (obj_bits ko) \<longrightarrow> \<not> x \<le> x + mask (obj_bits ko); valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<forall>ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<le> ptr + mask bits \<longrightarrow> ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (obj_bits ko) \<longrightarrow> \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (obj_bits ko)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; p && ~~ mask (pageBitsForSize sz) \<le> ptr + mask bits \<longrightarrow> ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz) \<longrightarrow> \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; p && ~~ mask (pageBitsForSize sz) \<le> ptr + mask bits \<longrightarrow> ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz) \<longrightarrow> \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<le> ptr + mask bits
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz) \<longrightarrow> \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<le> ptr + mask bits
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz) \<longrightarrow> \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz) \<longrightarrow> \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> ptr \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> ptr \<le> p
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)
 3. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; p \<le> (p && ~~ mask (pageBitsForSize sz)) + (2 ^ pageBitsForSize sz - 1)\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; tref \<noteq> idle_thread s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); \<not> dev; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1; \<not> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<le> (p && ~~ mask (pageBitsForSize sz)) + mask (pageBitsForSize sz) proof (prove)
goal (2 subgoals):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> ?sz209 s tref etcb tcb dev rights sz mapdata p \<le> pageBitsForSize sz
 2. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> mask (pageBitsForSize sz) < 2 ^ ?sz209 s tref etcb tcb dev rights sz mapdata p proof (prove)
goal (1 subgoal):
 1. \<And>s tref etcb tcb dev rights sz mapdata p. \<lbrakk>valid_tcb_state (tcb_state tcb) s; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; is_nondevice_page_cap_arch (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); ekheap s tref = Some etcb; is_aligned ptr bits; 2 \<le> bits; bits < word_bits; valid_etcbs s; kheap s tref = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False (p && ~~ mask (pageBitsForSize sz)) rights sz mapdata); is_aligned (tcb_ipc_buffer tcb) msg_align_bits; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)); ptr \<le> ptr + mask bits; ptr \<le> p; p \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz proof (prove)
goal:
No subgoals!