theory Intent_DR

lemma ipc_frame_ptr_at_sz_at:
  "\<lbrakk>ko_at (ArchObj (DataPage dev sz)) obuf s; valid_objs s;ipc_frame_ptr_at obuf thread s \<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz thread s" apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def) apply (clarsimp split:cap.splits arch_cap.splits) apply (frule valid_tcb_objs) apply (erule get_tcb_rev) apply (subgoal_tac "valid_cap (tcb_ipcframe tcb) s") apply (clarsimp simp: valid_cap_def obj_at_def split: if_splits) apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (DataPage dev sz) obuf s; valid_objs s; ipc_frame_ptr_at obuf thread s\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz thread s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> obuf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35)\<rbrakk> \<Longrightarrow> sz = x34 proof (prove)
goal (2 subgoals):
 1. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35)\<rbrakk> \<Longrightarrow> get_tcb (?thread111 tcb x31 x33 x34 x35) s = Some (?y111 tcb x31 x33 x34 x35)
 2. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35); valid_tcb (?thread111 tcb x31 x33 x34 x35) (?y111 tcb x31 x33 x34 x35) s\<rbrakk> \<Longrightarrow> sz = x34 proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35); valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> sz = x34 proof (prove)
goal (2 subgoals):
 1. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35); valid_tcb thread tcb s; s \<turnstile> tcb_ipcframe tcb\<rbrakk> \<Longrightarrow> sz = x34
 2. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35); valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ipcframe tcb proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x34 x35. \<lbrakk>kheap s obuf = Some (ArchObj (DataPage dev sz)); valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 obuf x33 x34 x35); valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ipcframe tcb proof (prove)
goal:
No subgoals!