theory Syscall_DR

lemma reply_from_kernel_error:
  notes option.case_cong_weak [cong]
  shows
  "\<lbrace>tcb_at oid and K (fst e \<le> mask 19 \<and> 0 < fst e = er)\<rbrace>reply_from_kernel oid e
    \<lbrace>\<lambda>rv s. (\<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and>
    ko_at (TCB tcb) oid s)\<rbrace>" apply (rule hoare_gen_asm) apply (case_tac e) apply (clarsimp simp:reply_from_kernel_def guess_error_def split_def set_message_info_def) apply (rule hoare_pre) apply (wp) apply (simp add:as_user_def split_def set_object_def get_object_def) apply (wp set_object_at_obj) apply (rule hoare_strengthen_post[where Q = "\<lambda>x s. x \<le> mask 12"]) apply (simp add:set_mrs_def) apply (wp|wpc)+ apply (clarsimp simp:setRegister_def simpler_modify_def) apply (drule get_tcb_SomeD) apply (rule exI) apply (rule conjI[rotated]) apply (simp add:obj_at_def) apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv mask_def) apply (simp add:shiftr_over_or_dist le_mask_iff word_neq_0_conv) apply (subst shiftl_shiftr_id) apply (simp add:word_bits_def mask_def le_mask_iff[symmetric])+ apply unat_arith apply (word_bitwise, simp) apply (wp hoare_drop_imp hoare_vcg_all_lift)+ apply clarsimp apply (rule conjI) apply (rule word_of_nat_le) apply (rule le_trans[OF min.cobounded1]) apply (simp add:mask_def) apply (rule le_trans) apply (rule less_imp_le[OF msg_registers_lt_msg_max_length]) apply (simp add:msg_max_length_def) apply (rule plus_one_helper) apply (simp add:mask_def) apply (rule word_of_nat_less) apply (simp add:msg_max_length_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at oid and K (fst e \<le> mask 19 \<and> (0 < fst e) = er)\<rbrace> reply_from_kernel oid e \<lbrace>\<lambda>rv s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> ko_at (TCB tcb) oid s\<rbrace> proof (prove)
goal (1 subgoal):
 1. fst e \<le> mask 19 \<and> (0 < fst e) = er \<Longrightarrow> \<lbrace>tcb_at oid\<rbrace> reply_from_kernel oid e \<lbrace>\<lambda>rv s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> ko_at (TCB tcb) oid s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst e \<le> mask 19 \<and> (0 < fst e) = er; e = (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at oid\<rbrace> reply_from_kernel oid e \<lbrace>\<lambda>rv s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> ko_at (TCB tcb) oid s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at oid\<rbrace> do buf <- lookup_ipc_buffer True oid;
y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid buf b;
as_user oid (setRegister msg_info_register ((a << 12) || len))
od \<lbrace>\<lambda>rv s. \<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> do buf <- lookup_ipc_buffer True oid;
y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid buf b;
as_user oid (setRegister msg_info_register ((a << 12) || len))
od \<lbrace>\<lambda>rv s. \<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid s\<rbrace>
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b x y len. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 a b x y len\<rbrace> as_user oid (setRegister msg_info_register ((a << 12) || len)) \<lbrace>\<lambda>rv s. \<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid s\<rbrace>
 2. \<And>a b x y. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 a b x y\<rbrace> set_mrs oid x b \<lbrace>?B13 a b x y\<rbrace>
 3. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?B12 a b x\<rbrace>
 4. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 5. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b x len. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 a b x () len\<rbrace> do tcb <- gets_the (get_tcb oid);
p <- select_f (setRegister msg_info_register ((a << 12) || len) (arch_tcb_context_get (tcb_arch tcb)));
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh oid = Some y);
return (the (kh oid))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (update_kheap ((kheap s)(oid \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))) s)
od \<lbrace>\<lambda>rv s. \<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid s\<rbrace>
 2. \<And>a b x y. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 a b x y\<rbrace> set_mrs oid x b \<lbrace>?B13 a b x y\<rbrace>
 3. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?B12 a b x\<rbrace>
 4. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 5. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b x y. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 a b x y\<rbrace> set_mrs oid x b \<lbrace>\<lambda>b c. get_tcb oid c \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (setRegister msg_info_register ((a << 12) || b) (arch_tcb_context_get (tcb_arch (the (get_tcb oid c))))). (\<exists>y. kheap c oid = Some y) \<longrightarrow> a_type (the (kheap c oid)) = ATCB \<longrightarrow> (\<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid (update_kheap ((kheap c)(oid \<mapsto> TCB (the (get_tcb oid c)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb oid c)))\<rparr>))) c)))\<rbrace>
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?B12 a b x\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b x y. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 a b x y\<rbrace> set_mrs oid x b \<lbrace>\<lambda>x s. x \<le> mask 12\<rbrace>
 2. \<And>a b x y rv s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12\<rbrakk> \<Longrightarrow> get_tcb oid s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (setRegister msg_info_register ((a << 12) || rv) (arch_tcb_context_get (tcb_arch (the (get_tcb oid s))))). (\<exists>y. kheap s oid = Some y) \<longrightarrow> a_type (the (kheap s oid)) = ATCB \<longrightarrow> (\<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid (update_kheap ((kheap s)(oid \<mapsto> TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb oid s)))\<rparr>))) s)))
 3. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?B12 a b x\<rbrace>
 4. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 5. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 a b x ()\<rbrace> do tcb <- gets_the (get_tcb oid);
y <- KHeap_A.set_object oid (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>));
case x of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length b)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) b);
return $ nat_to_len $ min (length b) msg_max_length
od
od \<lbrace>\<lambda>x s. x \<le> mask 12\<rbrace>
 2. \<And>a b x y rv s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12\<rbrakk> \<Longrightarrow> get_tcb oid s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (setRegister msg_info_register ((a << 12) || rv) (arch_tcb_context_get (tcb_arch (the (get_tcb oid s))))). (\<exists>y. kheap s oid = Some y) \<longrightarrow> a_type (the (kheap s oid)) = ATCB \<longrightarrow> (\<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid (update_kheap ((kheap s)(oid \<mapsto> TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb oid s)))\<rparr>))) s)))
 3. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?B12 a b x\<rbrace>
 4. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 5. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b x y rv s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12\<rbrakk> \<Longrightarrow> get_tcb oid s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (setRegister msg_info_register ((a << 12) || rv) (arch_tcb_context_get (tcb_arch (the (get_tcb oid s))))). (\<exists>y. kheap s oid = Some y) \<longrightarrow> a_type (the (kheap s oid)) = ATCB \<longrightarrow> (\<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid (update_kheap ((kheap s)(oid \<mapsto> TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb oid s)))\<rparr>))) s)))
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12; get_tcb oid s = Some y; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid (update_kheap (\<lambda>b. if b = oid then Some (TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>b. if b = msg_info_register then (a << 12) || rv else arch_tcb_context_get (tcb_arch (the (get_tcb oid s))) b) (tcb_arch (the (get_tcb oid s)))\<rparr>)) else kheap s b) s)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12; kheap s oid = Some (TCB tcb); kheap s oid = Some (TCB y)\<rbrakk> \<Longrightarrow> \<exists>tcb. (mi_label (get_tcb_message_info tcb) \<noteq> 0) = (0 < a) \<and> ko_at (TCB tcb) oid (update_kheap (\<lambda>b. if b = oid then Some (TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>b. if b = msg_info_register then (a << 12) || rv else arch_tcb_context_get (tcb_arch (the (get_tcb oid s))) b) (tcb_arch (the (get_tcb oid s)))\<rparr>)) else kheap s b) s)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12; kheap s oid = Some (TCB tcb); kheap s oid = Some (TCB y)\<rbrakk> \<Longrightarrow> (mi_label (get_tcb_message_info (?tcb83 a b rv s y tcb)) \<noteq> 0) = (0 < a) \<and> ko_at (TCB (?tcb83 a b rv s y tcb)) oid (update_kheap (\<lambda>b. if b = oid then Some (TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>b. if b = msg_info_register then (a << 12) || rv else arch_tcb_context_get (tcb_arch (the (get_tcb oid s))) b) (tcb_arch (the (get_tcb oid s)))\<rparr>)) else kheap s b) s)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12; kheap s oid = Some (TCB tcb); kheap s oid = Some (TCB y)\<rbrakk> \<Longrightarrow> ko_at (TCB (?tcb83 a b rv s y tcb)) oid (update_kheap (\<lambda>b. if b = oid then Some (TCB (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>b. if b = msg_info_register then (a << 12) || rv else arch_tcb_context_get (tcb_arch (the (get_tcb oid s))) b) (tcb_arch (the (get_tcb oid s)))\<rparr>)) else kheap s b) s)
 2. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12; kheap s oid = Some (TCB tcb); kheap s oid = Some (TCB y)\<rbrakk> \<Longrightarrow> (mi_label (get_tcb_message_info (?tcb83 a b rv s y tcb)) \<noteq> 0) = (0 < a)
 3. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 4. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 5. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); rv \<le> mask 12; kheap s oid = Some (TCB tcb); kheap s oid = Some (TCB y)\<rbrakk> \<Longrightarrow> (mi_label (get_tcb_message_info (the (get_tcb oid s)\<lparr>tcb_arch := arch_tcb_context_set (\<lambda>b. if b = msg_info_register then (a << 12) || rv else arch_tcb_context_get (tcb_arch (the (get_tcb oid s))) b) (tcb_arch (the (get_tcb oid s)))\<rparr>)) \<noteq> 0) = (0 < a)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (0 < ((a << 12) || rv >> 12) && 0xFFFFF) = (0 < a)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (0 < ((a << 12 >> 12) || (rv >> 12)) && 0xFFFFF) = (0 < a)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (6 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 2. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> a < 2 ^ (LENGTH(32) - 12)
 3. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (0 < (a || (rv >> 12)) && 0xFFFFF) = (0 < a)
 4. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 5. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 6. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (5 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> a < 0x100000
 2. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (0 < (a || (rv >> 12)) && 0xFFFFF) = (0 < a)
 3. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 4. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 5. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (4 subgoals):
 1. \<And>a b rv s y tcb. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); rv \<le> 0xFFF; y = tcb; kheap s oid = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (0 < (a || (rv >> 12)) && 0xFFFFF) = (0 < a)
 2. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 3. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 4. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?B11 a b x\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>a c. get_tcb oid c \<noteq> None \<longrightarrow> (x = None \<longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (nat_to_len $ min (length b) msg_max_length) \<le> mask 12)\<rbrace>
 2. \<And>a b. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a b\<rbrace> lookup_ipc_buffer True oid \<lbrace>?B11 a b\<rbrace>
 3. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?Q7 a b s proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> nat_to_len (min (length msg_registers) (length b)) \<le> mask 12 \<and> (\<forall>x. (nat_to_len $ min (length b) msg_max_length) \<le> mask 12) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length msg_registers) (length b)) \<le> mask 12 \<and> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length msg_registers) (length b)) \<le> mask 12
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> min (length msg_registers) (length b) \<le> unat (mask 12)
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> length msg_registers \<le> unat (mask 12)
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> length msg_registers \<le> 4095
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (3 subgoals):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> length msg_registers \<le> ?j121 a b s
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> ?j121 a b s \<le> 4095
 3. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> msg_max_length \<le> 4095
 2. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) \<le> mask 12 proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> mask 19; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) < mask 12 + 1 proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> word_of_nat (min (length b) msg_max_length) < 0x1000 proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>e = (a, b); a \<le> 0x7FFFF; er = (0 < a); tcb_at oid s\<rbrakk> \<Longrightarrow> min (length b) msg_max_length < unat 0x1000 proof (prove)
goal:
No subgoals!