theory ArchIpc_AC

lemma lookup_ipc_buffer_aligned[Ipc_AC_assms]:
  "\<lbrace>valid_objs\<rbrace>
   lookup_ipc_buffer True thread
   \<lbrace>\<lambda>rv _. (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)\<rbrace>" unfolding lookup_ipc_buffer_def apply (rule hoare_pre) apply (wp get_cap_wp thread_get_wp' | wpc)+ apply (clarsimp simp: cte_wp_at_caps_of_state get_tcb_ko_at [symmetric]) apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) apply (simp add: dom_tcb_cap_cases) apply (frule (1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_simps cap_aligned_def) apply (erule aligned_add_aligned) apply (rule is_aligned_andI1) apply (drule (1) valid_tcb_objs) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def
                   split: if_splits) apply (rule order_trans [OF _ pbfs_atleast_pageBits]) apply (simp add: msg_align_bits pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread \<lbrace>\<lambda>rv _. case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do buffer_ptr <- thread_get tcb_ipc_buffer thread;
buffer_frame_slot <- return (thread, tcb_cnode_index 4);
buffer_cap <- get_cap buffer_frame_slot;
case buffer_cap of ArchObjectCap (PageCap x p R vms xa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> True then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None
od \<lbrace>\<lambda>rv _. case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do buffer_ptr <- thread_get tcb_ipc_buffer thread;
buffer_frame_slot <- return (thread, tcb_cnode_index 4);
buffer_cap <- get_cap buffer_frame_slot;
case buffer_cap of ArchObjectCap (PageCap x p R vms xa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> True then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None
od \<lbrace>\<lambda>rv _. case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> \<forall>tcb. ko_at (TCB tcb) thread s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (thread, tcb_cnode_index 4) s \<longrightarrow> (cap = NullCap \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (cap = DomainCap \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (cap = IRQControlCap \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (x = ASIDControlCap \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> (vm_read_write \<subseteq> xc \<or> vm_read_only \<subseteq> xc \<and> \<not> True \<longrightarrow> (case Some $ xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)) of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<not> (vm_read_write \<subseteq> xc \<or> vm_read_only \<subseteq> xc \<and> \<not> True) \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc\<rbrakk> \<Longrightarrow> tcb_cnode_index 4 \<in> dom tcb_cap_cases
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base; valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned ref xd \<and> ref < kernel_base\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal:
No subgoals!