theory Intent_DR

lemma ipc_frame_ptr_at_frame_at:
  "\<lbrakk>valid_objs s;ipc_frame_ptr_at buf thread s;ipc_frame_sz_at sz thread s\<rbrakk> \<Longrightarrow>ko_at (ArchObj (DataPage False sz)) buf s" apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def) apply (clarsimp split:cap.splits arch_cap.splits) apply (drule valid_tcb_objs) apply (erule get_tcb_rev) apply (simp add:valid_tcb_def) apply (clarsimp simp: valid_ipc_buffer_cap_def tcb_cap_cases_def is_nondevice_page_cap_def
                 split: bool.split_asm) apply (clarsimp simp: valid_cap_def obj_at_def a_type_def is_nondevice_page_cap_def) by (clarsimp split: Structures_A.kernel_object.splits if_splits arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; ipc_frame_ptr_at buf thread s; ipc_frame_sz_at sz thread s\<rbrakk> \<Longrightarrow> ako_at (DataPage False sz) buf s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_objs s; kheap s thread = Some (TCB tcb); 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\<rbrakk> \<Longrightarrow> kheap s buf = Some (ArchObj (DataPage False sz)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>valid_objs s; kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35)\<rbrakk> \<Longrightarrow> kheap s buf = Some (ArchObj (DataPage False sz)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb x31 x33 x35. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35)\<rbrakk> \<Longrightarrow> get_tcb (?thread110 tcb x31 x33 x35) s = Some (?y110 tcb x31 x33 x35)
 2. \<And>tcb x31 x33 x35. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); valid_tcb (?thread110 tcb x31 x33 x35) (?y110 tcb x31 x33 x35) s\<rbrakk> \<Longrightarrow> kheap s buf = Some (ArchObj (DataPage False sz)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 sz x35); valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> kheap s buf = Some (ArchObj (DataPage False sz)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>kheap s thread = Some (TCB tcb); 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 thread (tcb_state tcb) (getF tcb))) \<and> valid_ipc_buffer_cap (ArchObjectCap (PageCap x31 buf x33 sz x35)) (tcb_ipc_buffer tcb) \<and> valid_tcb_state (tcb_state tcb) s \<and> (case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f) \<and> length (tcb_fault_handler tcb) = word_bits \<and> valid_bound_ntfn (tcb_bound_notification tcb) s \<and> valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> kheap s buf = Some (ArchObj (DataPage False sz)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 sz x35); \<not> x31; s \<turnstile> ArchObjectCap (PageCap False buf x33 sz x35); is_nondevice_page_cap_arch (PageCap False buf x33 sz x35); s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = thread \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb; 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 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> kheap s buf = Some (ArchObj (DataPage False sz)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x33 x35 ko. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False buf x33 sz x35); \<not> x31; is_nondevice_page_cap_arch (PageCap False buf x33 sz x35); (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = thread \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; 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 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; cap_aligned (ArchObjectCap (PageCap False buf x33 sz x35)); cap_aligned (tcb_caller tcb); case tcb_caller tcb of cap.UntypedCap dev p b f \<Rightarrow> valid_untyped (tcb_caller tcb) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | cap.EndpointCap r badge rights \<Rightarrow> ep_at r s | cap.NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | ArchObjectCap (arch_cap.PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (arch_cap.PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True; cap_aligned (tcb_reply tcb); case tcb_reply tcb of cap.UntypedCap dev p b f \<Rightarrow> valid_untyped (tcb_reply tcb) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | cap.EndpointCap r badge rights \<Rightarrow> ep_at r s | cap.NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | ArchObjectCap (arch_cap.PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (arch_cap.PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True; cap_aligned (tcb_vtable tcb); case tcb_vtable tcb of cap.UntypedCap dev p b f \<Rightarrow> valid_untyped (tcb_vtable tcb) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | cap.EndpointCap r badge rights \<Rightarrow> ep_at r s | cap.NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | ArchObjectCap (arch_cap.PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (arch_cap.PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True; cap_aligned (tcb_ctable tcb); case tcb_ctable tcb of cap.UntypedCap dev p b f \<Rightarrow> valid_untyped (tcb_ctable tcb) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | cap.EndpointCap r badge rights \<Rightarrow> ep_at r s | cap.NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | cap.CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | ArchObjectCap (arch_cap.PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (arch_cap.PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True; x33 \<in> valid_vm_rights; case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base; kheap s buf = Some ko; (case ko of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch (AUserData sz)\<rbrakk> \<Longrightarrow> ko = ArchObj (DataPage False sz)