theory Intent_DR

lemma within_page_ipc_buf:
  "\<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; ipc_frame_ptr_at buf y s; ipc_frame_sz_at sz y s;
                ipc_buffer_wp_at bptr y s; x < 2 ^ (msg_align_bits - 2) \<rbrakk>
      \<Longrightarrow> within_page buf (buf + (bptr && mask (pageBitsForSize sz)) + of_nat x * of_nat word_size) sz" apply (clarsimp simp:ipc_buffer_wp_at_def obj_at_def) apply (frule valid_tcb_obj_ipc_align_etc,simp+) apply (erule get_tcb_rev) apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def within_page_def) apply (clarsimp split: cap.split_asm arch_cap.split_asm) apply (frule valid_tcb_objs, erule get_tcb_rev) apply (clarsimp simp: valid_tcb_def valid_ipc_buffer_cap_def) apply (subst add.assoc) apply (erule is_aligned_add_helper[THEN conjunct2]) apply (rule iffD1[OF le_mask_iff_lt_2n[where n = "pageBitsForSize sz"],THEN iffD1]) apply (simp add:word_size) apply (case_tac sz,simp_all) apply (rule bound_preserve_mask[where n = msg_align_bits]) apply (rule is_aligned_after_mask) apply (simp add:word_and_le1)+ apply (simp add:msg_align_bits mask_2pm1) apply (rule div_le_mult) apply (simp add:word_size_def) apply (rule word_of_nat_le) apply (simp add:word_size_def msg_align_bits)+ apply (cases sz,auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; ipc_frame_ptr_at buf y s; ipc_frame_sz_at sz y s; ipc_buffer_wp_at bptr y s; x < 2 ^ (msg_align_bits - 2)\<rbrakk> \<Longrightarrow> within_page buf (buf + (bptr && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) sz proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; ipc_frame_ptr_at buf y s; ipc_frame_sz_at sz y s; x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb\<rbrakk> \<Longrightarrow> within_page buf (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) sz proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; ipc_frame_ptr_at buf y s; ipc_frame_sz_at sz y s; x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb\<rbrakk> \<Longrightarrow> get_tcb y s = Some (?tcb8 tcb)
 2. \<And>tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; ipc_frame_ptr_at buf y s; ipc_frame_sz_at sz y s; x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer (?tcb8 tcb)) msg_align_bits \<and> is_aligned (tcb_ipc_buffer (?tcb8 tcb)) 2 \<and> is_aligned buf (pageBitsForSize sz) \<and> is_aligned buf 2\<rbrakk> \<Longrightarrow> within_page buf (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) sz proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; ipc_frame_ptr_at buf y s; ipc_frame_sz_at sz y s; x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize sz) \<and> is_aligned buf 2\<rbrakk> \<Longrightarrow> within_page buf (buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) sz proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf (pageBitsForSize sz); is_aligned buf 2\<rbrakk> \<Longrightarrow> buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf (pageBitsForSize sz); is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35)\<rbrakk> \<Longrightarrow> buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf (pageBitsForSize sz); is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); valid_tcb y tcb s\<rbrakk> \<Longrightarrow> buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf (pageBitsForSize sz); is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf (pageBitsForSize sz); is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> buf + ((tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) && ~~ mask (pageBitsForSize sz) = buf proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size < 2 ^ pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < LENGTH(32)
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size \<le> mask (pageBitsForSize sz) proof (prove)
goal (2 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size \<le> mask (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size \<le> mask (pageBitsForSize sz) proof (prove)
goal (6 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> is_aligned (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) msg_align_bits
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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_ipc_buffer tcb && mask (pageBitsForSize sz) \<le> mask (pageBitsForSize sz)
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> word_of_nat x * word_of_nat word_size \<le> mask msg_align_bits
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 5. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 6. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (7 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> is_aligned (tcb_ipc_buffer tcb) msg_align_bits
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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_ipc_buffer tcb && mask (pageBitsForSize sz) \<le> mask (pageBitsForSize sz)
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> word_of_nat x * word_of_nat word_size \<le> mask msg_align_bits
 5. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 6. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 7. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (4 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> word_of_nat x * word_of_nat word_size \<le> mask msg_align_bits
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (4 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> word_of_nat x * word_of_nat word_size \<le> 0x1FF
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (5 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> word_of_nat x \<le> 0x1FF div word_of_nat word_size
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> 0 < word_of_nat word_size
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 5. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (5 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> word_of_nat x \<le> 0x7F
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> 0 < word_of_nat word_size
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 5. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (5 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> x \<le> unat 0x7F
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> 0 < word_of_nat word_size
 3. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits < 32
 4. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 5. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>x < 128; kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) 9; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> pageBitsForSize sz < 32
 2. \<And>tcb x31 x33 x35. \<lbrakk>x < 2 ^ (msg_align_bits - 2); kheap s y = Some (TCB tcb); bptr = tcb_ipc_buffer tcb; is_aligned (tcb_ipc_buffer tcb) msg_align_bits; is_aligned (tcb_ipc_buffer tcb) 2; is_aligned buf 2; valid_objs s; pspace_aligned s; pspace_distinct s; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); \<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 y (tcb_state tcb) (getF tcb)); case x31 of True \<Rightarrow> False | False \<Rightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits; 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> msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal:
No subgoals!