theory Ipc_DR

lemma corres_update_waiting_ntfn_do_notification_transfer:
  "dcorres dc \<top>
    (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and
     (st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification epptr)) y) and
     valid_ntfn (\<lparr>ntfn_obj = case ys of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> ))
          (Endpoint_D.do_notification_transfer y)
          (update_waiting_ntfn epptr (y # ys) bound_tcb badge)" apply (simp add: Endpoint_D.do_notification_transfer_def update_waiting_ntfn_def assert_def) apply (rule corres_dummy_return_pl) apply (rule corres_split_keep_pfx[where r'="dc" and Q="%x. \<top>" and Q'="%x. \<top>"]) apply (rule corres_guard_imp,rule corres_dummy_set_notification,clarsimp+) apply (rule dcorres_expand_pfx) apply clarsimp apply (frule_tac y = y in  generates_pending_not_idle) apply (clarsimp simp:st_tcb_at_def obj_at_def) apply (drule_tac t = "tcb_state tcb" in sym) apply (simp add:generates_pending_def) apply (rule corres_guard_imp) apply (rule dcorres_dc_rhs_noop_below_2_True[OF allI[OF possible_switch_to_dcorres]]) apply (rule corres_split[OF set_thread_state_corres]) apply (rule set_register_corres) apply (wp)+ apply simp apply (frule generates_pending_not_idle[where y = y]) apply (clarsimp simp: pred_tcb_at_def obj_at_def generates_pending_def) apply (drule_tac t = "tcb_state tcb" in sym) apply ((clarsimp simp:pred_tcb_at_def obj_at_def not_idle_thread_def split:Structures_A.thread_state.splits)+)[3] apply (wp set_simple_ko_aligned set_ep_mdb set_simple_ko_valid_objs sts_typ_ats) apply (simp add: not_idle_thread_def a_type_def ntfn_at_def2[symmetric, simplified]) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (drule valid_tcb_objs,erule get_tcb_rev) apply (drule_tac t = "tcb_state tcb" in sym) apply (clarsimp simp: valid_tcb_def valid_tcb_state_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) (do_notification_transfer y) (update_waiting_ntfn epptr (y # ys) bound_tcb badge) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>;
ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) (do return ?b1;
ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>;
ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od) proof (prove)
goal (4 subgoals):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) (return ?b1) (set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>)
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> dcorres dc ((\<lambda>_. True) and (\<lambda>_. True)) (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)) (K_bind (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) rv) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'\<rbrakk> \<Longrightarrow> st_tcb_at generates_pending y s'
 2. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; kheap s' y = Some (TCB tcb); BlockedOnNotification epptr = tcb_state tcb\<rbrakk> \<Longrightarrow> generates_pending (tcb_state tcb)
 2. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; kheap s' y = Some (TCB tcb); tcb_state tcb = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> generates_pending (tcb_state tcb)
 2. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q38 s') (?Q'38 s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do ya <- set_thread_state y Running;
ya <- as_user y (setRegister badge_register badge);
possible_switch_to y
od)
 2. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q38 s' s
 3. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'38 s' s
 4. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 5. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q38 s') (?Q'38 s') (do ya <- KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent y
od) (do x <- set_thread_state y Running;
as_user y (setRegister badge_register badge)
od)
 2. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q38 s' s
 3. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'38 s' s
 4. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 5. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s' ya x. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; dc ya x\<rbrakk> \<Longrightarrow> dcorres dc (?R47 s' ya) (?R'47 s' x) (corrupt_tcb_intent y) (as_user y (setRegister badge_register badge))
 2. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q47 s'\<rbrace> KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap \<lbrace>?R47 s'\<rbrace>
 3. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'47 s'\<rbrace> set_thread_state y Running \<lbrace>?R'47 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q47 s') s
 5. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and ?Q'47 s') s
 6. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 7. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q47 s'\<rbrace> KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>s'. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'47 s'\<rbrace> set_thread_state y Running \<lbrace>\<lambda>x. valid_idle and not_idle_thread y and valid_etcbs\<rbrace>
 3. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q47 s') s
 4. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and ?Q'47 s') s
 5. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 6. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s
 2. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. y = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread y s \<and> valid_etcbs s)) s
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. y = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread y s \<and> valid_etcbs s)) s
 2. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s\<rbrakk> \<Longrightarrow> st_tcb_at generates_pending y s'
 2. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s; not_idle_thread y s'\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. y = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread y s \<and> valid_etcbs s)) s
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s tcb. \<lbrakk>pspace_aligned s; valid_objs s; valid_mdb s; pspace_distinct s; valid_idle s; valid_etcbs s; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s; not_idle_thread y s; kheap s y = Some (TCB tcb); BlockedOnNotification epptr = tcb_state tcb\<rbrakk> \<Longrightarrow> case tcb_state tcb of Inactive \<Rightarrow> False | IdleThreadState \<Rightarrow> False | _ \<Rightarrow> True
 2. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s; not_idle_thread y s'\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. y = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread y s \<and> valid_etcbs s)) s
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s tcb. \<lbrakk>pspace_aligned s; valid_objs s; valid_mdb s; pspace_distinct s; valid_idle s; valid_etcbs s; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s; not_idle_thread y s; kheap s y = Some (TCB tcb); tcb_state tcb = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> case tcb_state tcb of Inactive \<Rightarrow> False | IdleThreadState \<Rightarrow> False | _ \<Rightarrow> True
 2. \<And>s' s. \<lbrakk>pspace_aligned s'; valid_objs s'; valid_mdb s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; st_tcb_at ((=) (BlockedOnNotification epptr)) y s'; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s'; not_idle_thread y s'; s' = s; not_idle_thread y s'\<rbrakk> \<Longrightarrow> (not_idle_thread y and K (RunningCap = infer_tcb_pending_op y Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. y = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread y s \<and> valid_etcbs s)) s
 3. \<lbrace>\<lambda>_. True\<rbrace> return ?b1 \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>\<rbrace> set_notification epptr \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>x. pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> and (\<lambda>_. True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_objs and valid_mdb and pspace_distinct and valid_idle and valid_etcbs and st_tcb_at ((=) (BlockedOnNotification epptr)) y and valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) s \<Longrightarrow> pspace_aligned s \<and> (valid_objs and valid_simple_obj (kernel_object.Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>) and K (is_simple_type (kernel_object.Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr>))) s \<and> valid_mdb s \<and> pspace_distinct s \<and> (obj_at (\<lambda>ko. partial_inv kernel_object.Notification ko \<noteq> None) epptr and valid_idle) s \<and> valid_etcbs s \<and> st_tcb_at ((=) (BlockedOnNotification epptr)) y s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<and> valid_objs s \<and> valid_mdb s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s \<and> st_tcb_at ((=) (BlockedOnNotification epptr)) y s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s \<Longrightarrow> ntfn_at epptr s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>pspace_aligned s; valid_objs s; valid_mdb s; pspace_distinct s; valid_idle s; valid_etcbs s; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s; kheap s y = Some (TCB tcb); BlockedOnNotification epptr = tcb_state tcb\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s epptr = Some ko \<and> is_ntfn ko proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>pspace_aligned s; valid_mdb s; pspace_distinct s; valid_idle s; valid_etcbs s; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s; kheap s y = Some (TCB tcb); BlockedOnNotification epptr = tcb_state tcb; valid_tcb y tcb s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s epptr = Some ko \<and> is_ntfn ko proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>pspace_aligned s; valid_mdb s; pspace_distinct s; valid_idle s; valid_etcbs s; valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn ys, ntfn_bound_tcb = bound_tcb\<rparr> s; kheap s y = Some (TCB tcb); valid_tcb y tcb s; tcb_state tcb = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s epptr = Some ko \<and> is_ntfn ko proof (prove)
goal:
No subgoals!