theory ArchIpc_AI

lemma lookup_ipc_buffer_in_user_frame[wp, Ipc_AI_assms]:
  "\<lbrace>valid_objs and tcb_at t\<rbrace> lookup_ipc_buffer b t
   \<lbrace>case_option (\<lambda>_. True) in_user_frame\<rbrace>" apply (simp add: lookup_ipc_buffer_def) apply (wp get_cap_wp thread_get_wp | wpc | simp)+ apply (clarsimp simp add: obj_at_def is_tcb) apply (rename_tac dev p R sz m) apply (subgoal_tac "in_user_frame (p + (tcb_ipc_buffer tcb &&
                                           mask (pageBitsForSize sz))) s", simp) apply (frule (1) cte_wp_valid_cap) apply (clarsimp simp add: valid_cap_def cap_aligned_def in_user_frame_def) apply (thin_tac "case_option a b c" for a b c) apply (rule_tac x=sz in exI) apply (subst is_aligned_add_helper[THEN conjunct2]) apply simp apply (simp add: and_mask_less' word_bits_def) apply (clarsimp simp: caps_of_state_cteD'[where P = "\<lambda>x. True",simplified,symmetric]) apply (drule(1) CSpace_AI.tcb_cap_slot_regular) apply simp apply (simp add: is_nondevice_page_cap_def is_nondevice_page_cap_arch_def case_bool_If
            split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and tcb_at t\<rbrace> lookup_ipc_buffer b t \<lbrace>case_option (\<lambda>_. True) in_user_frame\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and tcb_at t\<rbrace> do buffer_ptr <- thread_get tcb_ipc_buffer t;
get_cap (t, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> b then return (Some (p + (buffer_ptr && mask (pageBitsForSize vms)))) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od \<lbrace>case_option (\<lambda>_. True) in_user_frame\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<and> tcb_at t s \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 4) s \<longrightarrow> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb xc xd. (\<exists>xe. x = PageCap xa xb xc xd xe) \<longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> in_user_frame (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) s) \<and> (vm_read_only \<subseteq> xc \<and> \<not> b \<longrightarrow> in_user_frame (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) s))))) t s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap xa xb xc xd xe))) (t, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> in_user_frame (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) s) \<and> (vm_read_only \<subseteq> xc \<and> \<not> b \<longrightarrow> in_user_frame (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> R \<longrightarrow> in_user_frame (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))) s) \<and> (vm_read_only \<subseteq> R \<and> \<not> b \<longrightarrow> in_user_frame (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> in_user_frame (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; s \<turnstile> ArchObjectCap (PageCap dev p R sz m)\<rbrakk> \<Longrightarrow> in_user_frame (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights; case m 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\<rbrakk> \<Longrightarrow> \<exists>sza. typ_at (AArch (AUserData sza)) (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sza)) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> \<exists>sza. typ_at (AArch (AUserData sza)) (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sza)) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (p + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (3 subgoals):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> is_aligned p (pageBitsForSize sz)
 2. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz
 3. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize sz) < 2 ^ pageBitsForSize sz
 2. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap dev p R sz m))) (t, tcb_cnode_index 4) s; is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); caps_of_state s (t, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap dev p R sz m)); is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> kheap s (fst (t, tcb_cnode_index 4)) = Some (TCB (?tcb196 s tcb dev p R sz m))
 2. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights; \<exists>f upd check. tcb_cap_cases (snd (t, tcb_cnode_index 4)) = Some (f, upd, check) \<and> check (fst (t, tcb_cnode_index 4)) (tcb_state (?tcb196 s tcb dev p R sz m)) (ArchObjectCap (PageCap dev p R sz m))\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb dev p R sz m. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb); is_aligned p (pageBitsForSize sz); pageBitsForSize sz < word_bits; if dev then typ_at (AArch (ADeviceData sz)) p s else typ_at (AArch (AUserData sz)) p s; R \<in> valid_vm_rights; \<exists>f upd check. tcb_cap_cases (snd (t, tcb_cnode_index 4)) = Some (f, upd, check) \<and> check (fst (t, tcb_cnode_index 4)) (tcb_state tcb) (ArchObjectCap (PageCap dev p R sz m))\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s proof (prove)
goal:
No subgoals!