theory Intent_DR

lemma valid_tcb_obj_ipc_align_etc:
  "\<lbrakk>valid_objs s;pspace_aligned s;ipc_frame_ptr_at buf thread s;ipc_frame_sz_at pgsz thread s;
    get_tcb thread s = Some tcb\<rbrakk>
    \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb) 2
    \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2" apply (frule ipc_frame_ptr_at_frame_at) apply simp+ apply (drule(1) valid_tcb_objs) apply (clarsimp dest!: get_tcb_SomeD simp:valid_tcb_def valid_ipc_buffer_cap_def
                         ipc_frame_wp_at_def obj_at_def) apply (clarsimp split: cap.splits arch_cap.splits bool.split_asm) apply (rule conjI) apply (rule is_aligned_weaken,simp+) apply (simp add:msg_align_bits_def) apply (simp add:pspace_aligned_def obj_at_def ipc_frame_wp_at_def) apply (drule_tac x = buf in bspec) apply (clarsimp simp:) apply (clarsimp simp:obj_at_def) apply (rule is_aligned_weaken) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at pgsz thread s; get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at pgsz thread s; get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ?buf ?thread s
 2. \<lbrakk>valid_objs s; pspace_aligned s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at pgsz thread s; get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> ipc_frame_sz_at ?sz ?thread s
 3. \<lbrakk>valid_objs s; pspace_aligned s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at pgsz thread s; get_tcb thread s = Some tcb; ako_at (DataPage False ?sz) ?buf s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at pgsz thread s; get_tcb thread s = Some tcb; ako_at (DataPage False pgsz) buf s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at pgsz thread s; get_tcb thread s = Some tcb; ako_at (DataPage False pgsz) buf s; valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); case tcb_ipcframe tcb of cap.NullCap \<Rightarrow> True | ArchObjectCap acap \<Rightarrow> valid_ipc_buffer_cap_arch acap (tcb_ipc_buffer tcb) | _ \<Rightarrow> False; 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 sz mapdata) \<Rightarrow> pgsz = sz | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; 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 \<and> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; pspace_aligned s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) 2 \<and> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; pspace_aligned s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) 2
 2. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; pspace_aligned s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; pspace_aligned s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) msg_align_bits\<rbrakk> \<Longrightarrow> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; pspace_aligned s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n))\<rbrakk> \<Longrightarrow> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n))\<rbrakk> \<Longrightarrow> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n))\<rbrakk> \<Longrightarrow> buf \<in> dom (kheap s)
 2. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n)); is_aligned buf (obj_bits (the (kheap s buf)))\<rbrakk> \<Longrightarrow> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n)); is_aligned buf (obj_bits (the (kheap s buf)))\<rbrakk> \<Longrightarrow> is_aligned buf (pageBitsForSize pgsz) \<and> is_aligned buf 2 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n)); is_aligned buf (pageBitsForSize pgsz)\<rbrakk> \<Longrightarrow> is_aligned buf 2 proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n)); is_aligned buf (pageBitsForSize pgsz)\<rbrakk> \<Longrightarrow> is_aligned buf (?x146 x31 x33 x35)
 2. \<And>x31 x33 x35. \<lbrakk>valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; kheap s buf = Some (ArchObj (DataPage False pgsz)); \<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 thread (tcb_state tcb) (getF tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 pgsz x35); \<not> x31; is_aligned (tcb_ipc_buffer tcb) (word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n)); is_aligned buf (pageBitsForSize pgsz)\<rbrakk> \<Longrightarrow> 2 \<le> ?x146 x31 x33 x35 proof (prove)
goal:
No subgoals!