theory Syscall_DR

lemma dcorres_reply_from_kernel:
  "dcorres dc \<top> (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (reply_from_kernel oid msg_rv)" apply (simp add:reply_from_kernel_def) apply (case_tac msg_rv) apply (clarsimp simp:corrupt_ipc_buffer_def) apply (rule dcorres_expand_pfx) apply (rule_tac Q' = "\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)"
                  in corres_symb_exec_r) apply (rule dcorres_expand_pfx) apply (clarsimp) apply (case_tac rv) apply (rule corres_symb_exec_l) apply (rule_tac F="rva = None" in corres_gen_asm) apply clarsimp apply (rule corres_guard_imp) apply (rule corres_corrupt_tcb_intent_dupl) apply (rule corres_split[OF set_register_corres]) unfolding K_bind_def apply (rule corres_corrupt_tcb_intent_dupl) apply (rule corres_split[OF set_mrs_corres_no_recv_buffer]) unfolding K_bind_def apply (rule set_message_info_corres) apply (wp | clarsimp simp:not_idle_thread_def)+ apply (wp get_ipc_buffer_noop, clarsimp) apply (fastforce simp: not_idle_thread_def) apply (simp add: pred_conj_def) apply (strengthen refl[where t=True]) apply (wp cdl_get_ipc_buffer_None  | simp)+ apply clarsimp apply (drule lookup_ipc_buffer_SomeB_evalMonad) apply clarsimp apply (rule corres_symb_exec_l) apply (rule_tac F = "rv = Some ba" in corres_gen_asm) apply clarsimp apply (rule corrupt_frame_include_self[where y = oid]) apply (rule corres_guard_imp) apply (rule corres_split[OF set_register_corres]) unfolding K_bind_def apply (rule_tac y = oid in corrupt_frame_include_self') apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_set_mrs]) unfolding K_bind_def apply (rule set_message_info_corres) apply (wp| simp add:not_idle_thread_def)+ apply (clarsimp simp:not_idle_thread_def) apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def valid_pspace_def
                              ipc_frame_wp_at_def ipc_buffer_wp_at_def obj_at_def) apply (clarsimp simp:cte_wp_at_cases obj_at_def) apply (drule_tac s="cap.ArchObjectCap c" for c in sym) apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def) apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def cte_wp_at_cases) apply (drule_tac s="cap.ArchObjectCap c" for c in sym) apply simp apply (wp get_ipc_buffer_noop, clarsimp) apply fastforce apply simp apply (rule cdl_get_ipc_buffer_Some) apply fastforce apply (simp add:tcb_at_def not_idle_thread_def get_tcb_rev)+ apply wp apply (rule evalMonad_wp) apply (simp add:empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+ apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (reply_from_kernel oid msg_rv) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (case msg_rv of (label, msg) \<Rightarrow> do buf <- lookup_ipc_buffer True oid;
y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid buf msg;
set_message_info oid (MI len 0 0 label)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b. msg_rv = (a, b) \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (case msg_rv of (label, msg) \<Rightarrow> do buf <- lookup_ipc_buffer True oid;
y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid buf msg;
set_message_info oid (MI len 0 0 label)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b. msg_rv = (a, b) \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (do buffer <- get_ipc_buffer oid True;
case buffer of None \<Rightarrow> corrupt_tcb_intent oid | Some a \<Rightarrow> corrupt_frame a
od) (do buf <- lookup_ipc_buffer True oid;
y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid buf b;
set_message_info oid (MI len 0 0 a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do buffer <- get_ipc_buffer oid True;
case buffer of None \<Rightarrow> corrupt_tcb_intent oid | Some a \<Rightarrow> corrupt_frame a
od) (do buf <- lookup_ipc_buffer True oid;
y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid buf b;
set_message_info oid (MI len 0 0 a)
od) proof (prove)
goal (4 subgoals):
 1. \<And>a b s s' rv. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some rv)) (do buffer <- get_ipc_buffer oid True;
case buffer of None \<Rightarrow> corrupt_tcb_intent oid | Some a \<Rightarrow> corrupt_frame a
od) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s s' rv sa s'a. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; sa = transform s'a; s = sa; ((=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some rv)) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) sa) ((=) s'a) (do buffer <- get_ipc_buffer oid True;
case buffer of None \<Rightarrow> corrupt_tcb_intent oid | Some a \<Rightarrow> corrupt_frame a
od) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (5 subgoals):
 1. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 3. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 4. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b s' rv rva. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?Q14 a b s' rv rva) ((=) s') (case rva of None \<Rightarrow> corrupt_tcb_intent oid | Some x \<Rightarrow> corrupt_frame x) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>?Q14 a b s' rv\<rbrace>
 4. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b s' rv rva. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; rva = None\<rbrakk> \<Longrightarrow> dcorres dc (?P19 a b s' rv rva) ((=) s') (case rva of None \<Rightarrow> corrupt_tcb_intent oid | Some x \<Rightarrow> corrupt_frame x) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 4. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?P19 a b s' None None) ((=) s') (corrupt_tcb_intent oid) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid None b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 4. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (10 subgoals):
 1. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q26 a b s') (?Q'26 a b s') (corrupt_tcb_intent oid) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid None b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ?Q26 a b s' s
 3. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'26 a b s' s
 4. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 6. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 7. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 9. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (10 subgoals):
 1. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q26 a b s') (?Q'26 a b s') (do corrupt_tcb_intent oid;
corrupt_tcb_intent oid
od) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid None b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ?Q26 a b s' s
 3. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'26 a b s' s
 4. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 6. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 7. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 9. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (12 subgoals):
 1. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R32 a b s' rv) (?R'32 a b s' rv') (K_bind (corrupt_tcb_intent oid) rv) (do len <- set_mrs oid None b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 a b s'\<rbrace> corrupt_tcb_intent oid \<lbrace>?R32 a b s'\<rbrace>
 3. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 a b s'\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'32 a b s'\<rbrace>
 4. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q32 a b s') s
 5. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'32 a b s') s
 6. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 8. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 9. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R32 a b s' rv) (?R'32 a b s' rv') (corrupt_tcb_intent oid) (do len <- set_mrs oid None b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 a b s'\<rbrace> corrupt_tcb_intent oid \<lbrace>?R32 a b s'\<rbrace>
 3. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 a b s'\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'32 a b s'\<rbrace>
 4. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q32 a b s') s
 5. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'32 a b s') s
 6. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 8. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 9. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R32 a b s' rv) (?R'32 a b s' rv') (do corrupt_tcb_intent oid;
corrupt_tcb_intent oid
od) (do len <- set_mrs oid None b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 a b s'\<rbrace> corrupt_tcb_intent oid \<lbrace>?R32 a b s'\<rbrace>
 3. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 a b s'\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'32 a b s'\<rbrace>
 4. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q32 a b s') s
 5. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'32 a b s') s
 6. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 8. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 9. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a b s' rv rv' rva len. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'; dc rva len\<rbrakk> \<Longrightarrow> dcorres dc (?R39 a b s' rv rv' rva) (?R'39 a b s' rv rv' len) (K_bind (corrupt_tcb_intent oid) rva) (set_message_info oid (MI len 0 0 a))
 2. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 a b s' rv\<rbrace> corrupt_tcb_intent oid \<lbrace>?R39 a b s' rv rv'\<rbrace>
 3. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 a b s' rv'\<rbrace> set_mrs oid None b \<lbrace>?R'39 a b s' rv rv'\<rbrace>
 4. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 a b s'\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q41 a b s' rv\<rbrace>
 5. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 a b s'\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread oid and valid_etcbs and ?Q'43 a b s' rv'\<rbrace>
 6. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q32 a b s') s
 7. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'32 a b s') s
 8. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 10. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a b s' rv rv' rva len. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'; dc rva len\<rbrakk> \<Longrightarrow> dcorres dc (?R39 a b s' rv rv' rva) (?R'39 a b s' rv rv' len) (corrupt_tcb_intent oid) (set_message_info oid (MI len 0 0 a))
 2. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 a b s' rv\<rbrace> corrupt_tcb_intent oid \<lbrace>?R39 a b s' rv rv'\<rbrace>
 3. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 a b s' rv'\<rbrace> set_mrs oid None b \<lbrace>?R'39 a b s' rv rv'\<rbrace>
 4. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 a b s'\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q41 a b s' rv\<rbrace>
 5. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 a b s'\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread oid and valid_etcbs and ?Q'43 a b s' rv'\<rbrace>
 6. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q32 a b s') s
 7. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'32 a b s') s
 8. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 10. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 a b s' rv\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>a b s' rv rv'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 a b s' rv'\<rbrace> set_mrs oid None b \<lbrace>\<lambda>len. valid_idle and not_idle_thread oid and valid_etcbs\<rbrace>
 3. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 a b s'\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q41 a b s' rv\<rbrace>
 4. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 a b s'\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread oid and valid_etcbs and ?Q'43 a b s' rv'\<rbrace>
 5. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; ?P19 a b s' None None s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q32 a b s') s
 6. \<And>a b s' s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'32 a b s') s
 7. \<And>a b s' rv s. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 9. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 10. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
A total of 13 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; oid \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) (transform s')\<rbrace>
 2. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 3. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 4. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b s'. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; oid \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<exists>s'a. transform s' = transform s'a \<and> tcb_at oid s'a \<and> valid_etcbs s'a \<and> not_idle_thread oid s'a
 2. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 3. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 4. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (6 subgoals):
 1. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva. ?P19 a b s' rv rva and (\<lambda>s. rva = None)\<rbrace>
 2. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 3. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 5. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (6 subgoals):
 1. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rva x. ?P19 a b s' None rva x \<and> rva = None\<rbrace>
 2. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 3. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 5. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (6 subgoals):
 1. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some None; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>r s. True \<and> r = None\<rbrace>
 2. \<And>a b s' rv. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 3. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some rv; invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid rv b;
set_message_info oid (MI len 0 0 a)
od)
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 5. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s' rv aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some (Some aa); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; rv = Some aa\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some aa) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s' aa. \<lbrakk>msg_rv = (a, b); evalMonad (lookup_ipc_buffer True oid) s' = Some (Some aa); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some aa) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s' aa. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> True \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at oid b rs sz s' \<and> ko_at (TCB obj) oid s' \<and> aa = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some aa) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer oid True >>= case_option (corrupt_tcb_intent oid) corrupt_frame) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q159 a b s' ba rs sz mapdata obj dev rv) ((=) s') (case rv of None \<Rightarrow> corrupt_tcb_intent oid | Some x \<Rightarrow> corrupt_frame x) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>?Q159 a b s' ba rs sz mapdata obj dev\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; rv = Some ba\<rbrakk> \<Longrightarrow> dcorres dc (?P164 a b s' ba rs sz mapdata obj dev rv) ((=) s') (case rv of None \<Rightarrow> corrupt_tcb_intent oid | Some x \<Rightarrow> corrupt_frame x) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. ?P164 a b s' ba rs sz mapdata obj dev rv and (\<lambda>s. rv = Some ba)\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> dcorres dc (?P164 a b s' ba rs sz mapdata obj dev (Some ba)) ((=) s') (corrupt_frame ba) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. ?P164 a b s' ba rs sz mapdata obj dev rv and (\<lambda>s. rv = Some ba)\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (do corrupt_tcb_intent oid;
corrupt_frame ba
od) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (10 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q173 a b s' ba rs sz mapdata obj dev) (?Q'173 a b s' ba rs sz mapdata obj dev) (do corrupt_tcb_intent oid;
corrupt_frame ba
od) (do y <- as_user oid (setRegister badge_register 0);
len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ?Q173 a b s' ba rs sz mapdata obj dev s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'173 a b s' ba rs sz mapdata obj dev s
 4. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 5. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 7. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 9. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (12 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R177 a b s' ba rs sz mapdata obj dev rv) (?R'177 a b s' ba rs sz mapdata obj dev rv') (K_bind (corrupt_frame ba) rv) (do len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>?R177 a b s' ba rs sz mapdata obj dev\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 5. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
 6. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 7. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 9. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R177 a b s' ba rs sz mapdata obj dev rv) (?R'177 a b s' ba rs sz mapdata obj dev rv') (corrupt_frame ba) (do len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>?R177 a b s' ba rs sz mapdata obj dev\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 5. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
 6. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 7. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 9. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 10. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?R'177 a b s' ba rs sz mapdata obj dev rv') (do corrupt_frame ba;
corrupt_tcb_intent oid
od) (do len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 6. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
 7. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 8. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 10. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q183 a b s' ba rs sz mapdata obj dev rv rv') (?Q'183 a b s' ba rs sz mapdata obj dev rv rv') (do corrupt_frame ba;
corrupt_tcb_intent oid
od) (do len <- set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b;
set_message_info oid (MI len 0 0 a)
od)
 2. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; True\<rbrakk> \<Longrightarrow> ?Q183 a b s' ba rs sz mapdata obj dev rv rv' s
 3. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> ?Q'183 a b s' ba rs sz mapdata obj dev rv rv' s
 4. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv _. True\<rbrace>
 6. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 7. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 8. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
 9. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 10. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv' rva len. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; dc rva len\<rbrakk> \<Longrightarrow> dcorres dc (?R187 a b s' ba rs sz mapdata obj dev rv rv' rva) (?R'187 a b s' ba rs sz mapdata obj dev rv rv' len) (K_bind (corrupt_tcb_intent oid) rva) (set_message_info oid (MI len 0 0 a))
 2. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace> corrupt_frame ba \<lbrace>?R187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace> set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b \<lbrace>?R'187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q187 a b s' ba rs sz mapdata obj dev rv rv') s
 5. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread oid and ipc_frame_ptr_at ba oid and ipc_frame_sz_at sz oid and ipc_buffer_wp_at (tcb_ipc_buffer obj) oid and valid_etcbs and ?Q'187 a b s' ba rs sz mapdata obj dev rv rv') s
 6. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 7. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 9. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 10. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
A total of 17 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv' rva len. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; dc rva len\<rbrakk> \<Longrightarrow> dcorres dc (?R187 a b s' ba rs sz mapdata obj dev rv rv' rva) (?R'187 a b s' ba rs sz mapdata obj dev rv rv' len) (corrupt_tcb_intent oid) (set_message_info oid (MI len 0 0 a))
 2. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace> corrupt_frame ba \<lbrace>?R187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace> set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b \<lbrace>?R'187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q187 a b s' ba rs sz mapdata obj dev rv rv') s
 5. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread oid and ipc_frame_ptr_at ba oid and ipc_frame_sz_at sz oid and ipc_buffer_wp_at (tcb_ipc_buffer obj) oid and valid_etcbs and ?Q'187 a b s' ba rs sz mapdata obj dev rv rv') s
 6. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 7. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 9. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 10. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace> corrupt_frame ba \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>a b s' ba rs sz mapdata obj dev rv rv'. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'187 a b s' ba rs sz mapdata obj dev rv rv'\<rbrace> set_mrs oid (Some (ba + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) b \<lbrace>\<lambda>len. valid_idle and not_idle_thread oid and valid_etcbs\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q187 a b s' ba rs sz mapdata obj dev rv rv') s
 4. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread oid and ipc_frame_ptr_at ba oid and ipc_frame_sz_at sz oid and ipc_buffer_wp_at (tcb_ipc_buffer obj) oid and valid_etcbs and ?Q'187 a b s' ba rs sz mapdata obj dev rv rv') s
 5. \<And>a b s' ba rs sz mapdata obj dev rv rv' s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; dc rv rv'; ?R'177 a b s' ba rs sz mapdata obj dev rv' s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 6. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q177 a b s' ba rs sz mapdata obj dev\<rbrace> corrupt_tcb_intent oid \<lbrace>\<lambda>rv _. True\<rbrace>
 7. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'177 a b s' ba rs sz mapdata obj dev\<rbrace> as_user oid (setRegister badge_register 0) \<lbrace>?R'177 a b s' ba rs sz mapdata obj dev\<rbrace>
 8. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q177 a b s' ba rs sz mapdata obj dev) s
 9. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread oid and valid_etcbs and ?Q'177 a b s' ba rs sz mapdata obj dev) s
 10. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
A total of 16 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s; tcb_at oid s; oid \<noteq> idle_thread s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s; ko_at (TCB obj) oid s; s' = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> ipc_frame_ptr_at ba oid s \<and> ipc_frame_sz_at sz oid s \<and> ipc_buffer_wp_at (tcb_ipc_buffer obj) oid s \<and> valid_idle s
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s; tcb_at oid s; oid \<noteq> idle_thread s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s; ko_at (TCB obj) oid s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> ipc_frame_ptr_at ba oid s \<and> ipc_frame_sz_at sz oid s \<and> ipc_buffer_wp_at (tcb_ipc_buffer obj) oid s \<and> valid_idle s
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); oid \<noteq> idle_thread s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s; kheap s oid = Some (TCB obj); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> ba = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); oid \<noteq> idle_thread s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; ArchObjectCap (PageCap dev ba rs sz mapdata) = tcb_ipcframe obj; kheap s oid = Some (TCB obj); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> ba = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); oid \<noteq> idle_thread s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; kheap s oid = Some (TCB obj); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; tcb_ipcframe obj = ArchObjectCap (PageCap dev ba rs sz mapdata)\<rbrakk> \<Longrightarrow> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> ba = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 3. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at ba oid s \<and> not_idle_thread oid s \<and> valid_etcbs s
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s; not_idle_thread oid s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; ArchObjectCap (PageCap dev ba rs sz mapdata) = tcb_ipcframe obj; kheap s oid = Some (TCB obj)\<rbrakk> \<Longrightarrow> case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> ba = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (7 subgoals):
 1. \<And>a b ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s; not_idle_thread oid s; valid_etcbs s; AllowRead \<in> rs; AllowWrite \<in> rs; kheap s oid = Some (TCB obj); tcb_ipcframe obj = ArchObjectCap (PageCap dev ba rs sz mapdata)\<rbrakk> \<Longrightarrow> case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> ba = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 6. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (6 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev s. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer oid True \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 5. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (6 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<exists>s'a. transform s' = transform s'a \<and> tcb_at oid s'a \<and> valid_etcbs s'a \<and> not_idle_thread oid s'a
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 5. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (5 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some ba)\<rbrace>
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 3. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 4. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (5 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer oid True \<lbrace>\<lambda>rv s. rv = Some ba\<rbrace>
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 3. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 4. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (9 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> ipc_frame_cte_at oid ba (?rs306 a b s' ba rs sz mapdata obj dev) (?sz306 a b s' ba rs sz mapdata obj dev) s'
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> valid_etcbs s'
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> tcb_at oid s'
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> not_idle_thread oid s'
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> AllowRead \<in> ?rs306 a b s' ba rs sz mapdata obj dev \<and> (\<not> True \<or> AllowWrite \<in> ?rs306 a b s' ba rs sz mapdata obj dev)
 6. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 7. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 8. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (8 subgoals):
 1. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> valid_etcbs s'
 2. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> tcb_at oid s'
 3. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> not_idle_thread oid s'
 4. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'\<rbrakk> \<Longrightarrow> AllowRead \<in> rs \<and> (\<not> True \<or> AllowWrite \<in> rs)
 5. \<And>a b s' ba rs sz mapdata obj dev. \<lbrakk>msg_rv = (a, b); invs s'; tcb_at oid s'; not_idle_thread oid s'; valid_etcbs s'; AllowRead \<in> rs; AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev ba rs sz mapdata))) (oid, tcb_cnode_index 4) s'; ko_at (TCB obj) oid s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer oid True)
 6. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 7. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (3 subgoals):
 1. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; invs s' \<and> (\<exists>tcb. get_tcb oid s' = Some tcb) \<and> oid \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) s' and (\<lambda>y. evalMonad (lookup_ipc_buffer True oid) s' = Some r)\<rbrace>
 2. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (4 subgoals):
 1. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; invs s' \<and> (\<exists>tcb. get_tcb oid s' = Some tcb) \<and> oid \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'319 a b s s'\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>rv s. evalMonad (lookup_ipc_buffer True oid) s' = Some rv\<rbrace>
 2. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; invs s' \<and> (\<exists>tcb. get_tcb oid s' = Some tcb) \<and> oid \<noteq> idle_thread s' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> ?P'319 a b s s' sa
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (5 subgoals):
 1. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; invs s' \<and> (\<exists>tcb. get_tcb oid s' = Some tcb) \<and> oid \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> empty_when_fail (lookup_ipc_buffer True oid)
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; invs s' \<and> (\<exists>tcb. get_tcb oid s' = Some tcb) \<and> oid \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s') (lookup_ipc_buffer True oid)
 3. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; invs s' \<and> (\<exists>tcb. get_tcb oid s' = Some tcb) \<and> oid \<noteq> idle_thread s' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> s' = sa
 4. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal (2 subgoals):
 1. \<And>a b s s' sa. \<lbrakk>msg_rv = (a, b); s = transform sa; invs sa \<and> tcb_at oid sa \<and> not_idle_thread oid sa \<and> valid_etcbs sa; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> lookup_ipc_buffer True oid \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>a b s s'. \<lbrakk>msg_rv = (a, b); s = transform s'; True; (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (lookup_ipc_buffer True oid) proof (prove)
goal:
No subgoals!