kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_R

lemma set_ep_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans \<rbrace>" apply (unfold setEndpoint_def) apply (rule setObject_ep_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp add: bitmapQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and ep_at' epptr\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d i. (\<exists>j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i) and ep_at' epptr\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 epptr ps));
obj' <- updateObject_default ep (snd p) epptr (fst p) (snd (lookupAround2 epptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. \<forall>d i. (\<exists>j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma ct_in_state_thread_state_lift':
  assumes ct: "\<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>"
  assumes st: "\<And>t. \<lbrace>st_tcb_at' P t\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>"
  shows "\<lbrace>ct_in_state' P\<rbrace> f \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" apply (clarsimp simp: ct_in_state'_def) apply (clarsimp simp: valid_def) apply (frule (1) use_valid [OF _ ct]) apply (drule (1) use_valid [OF _ st], assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> f \<lbrace>\<lambda>_. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' P (ksCurThread s) s\<rbrace> f \<lbrace>\<lambda>_ s. st_tcb_at' P (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>st_tcb_at' P (ksCurThread s) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> st_tcb_at' P (ksCurThread b) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>st_tcb_at' P (ksCurThread s) s; (a, b) \<in> fst (f s); st_tcb_at' P (ksCurThread b) s\<rbrakk> \<Longrightarrow> st_tcb_at' P (ksCurThread b) b proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma tcb_in_cur_domain'_lift:
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>"
  assumes b: "\<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace> f \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace>"
  shows "\<lbrace> tcb_in_cur_domain' t \<rbrace> f \<lbrace> \<lambda>_. tcb_in_cur_domain' t \<rbrace>" apply (simp add: tcb_in_cur_domain'_def) apply (rule_tac f="ksCurDomain" in  hoare_lift_Pf) apply (rule b) apply (rule a) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> f \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> f \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace> f \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_ep_obj_at'_tcb[wp]:
  "\<lbrace>obj_at' (P :: tcb \<Rightarrow> bool) t \<rbrace> setObject ptr (e::endpoint) \<lbrace>\<lambda>_. obj_at' (P :: tcb \<Rightarrow> bool) t\<rbrace>" apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setObject ptr e \<lbrace>\<lambda>_. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setEndpoint_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>" apply (clarsimp simp: setEndpoint_def) apply (rule tcb_in_cur_domain'_lift; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> setObject epptr ep \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setEndpoint_obj_at'_tcb[wp]:
  "\<lbrace>obj_at' (P :: tcb \<Rightarrow> bool) t \<rbrace> setEndpoint ptr (e::endpoint) \<lbrace>\<lambda>_. obj_at' (P :: tcb \<Rightarrow> bool) t\<rbrace>" by (clarsimp simp: setEndpoint_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setEndpoint ptr e \<lbrace>\<lambda>_. obj_at' P t\<rbrace>
theory KHeap_R

lemma set_ep_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
     setEndpoint epptr ep
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (wp sch_act_wf_lift) apply (simp add: setEndpoint_def split_def setObject_def
              | wp updateObject_default_inv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>s. sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_state_refs_of':
  assumes x: "updateObject val = updateObject_default val"
  assumes y: "(1 :: word32) < 2 ^ objBits val"
  shows
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (ptr := refs_of' (injectKO val)))\<rbrace>
     setObject ptr val
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (clarsimp simp: setObject_def valid_def in_monad split_def
                        updateObject_default_def x in_magnitude_check
                        projectKOs y
                 elim!: rsubst[where P=P] intro!: ext
             split del: if_split cong: option.case_cong if_cong) apply (clarsimp simp: state_refs_of'_def objBits_def[symmetric]
                        ps_clear_upd
                  cong: if_cong option.case_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(ptr := refs_of' (injectKO val)))\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x ba uu_. \<lbrakk>ksPSpace s ptr = Some ba; projectKO_opt ba = Some uu_; is_aligned ptr (objBits val); ps_clear ptr (objBits val) s\<rbrakk> \<Longrightarrow> (if x = ptr then refs_of' (injectKO val) else state_refs_of' s x) = state_refs_of' (s\<lparr>ksPSpace := (ksPSpace s)(ptr \<mapsto> injectKO val)\<rparr>) x proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_state_refs_of_eq:
  assumes x: "\<And>s s' obj obj' ptr' ptr''.
                  (obj', s') \<in> fst (updateObject val obj ptr ptr' ptr'' s)
                    \<Longrightarrow> refs_of' obj' = refs_of' obj"
  shows
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
     setObject ptr val
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (clarsimp simp: setObject_def valid_def in_monad split_def
                        updateObject_default_def in_magnitude_check
                        projectKOs lookupAround2_char1
                 elim!: rsubst[where P=P] intro!: ext
             split del: if_split cong: option.case_cong if_cong) apply (frule x, drule updateObject_objBitsKO) apply (simp add: state_refs_of'_def ps_clear_upd
             cong: option.case_cong if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x a ba s''a obj'. \<lbrakk>a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject val ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> state_refs_of' s x = state_refs_of' (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) x proof (prove)
goal (1 subgoal):
 1. \<And>s x a ba s''a obj'. \<lbrakk>a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; refs_of' obj' = refs_of' ba; objBitsKO obj' = objBitsKO ba\<rbrakk> \<Longrightarrow> state_refs_of' s x = state_refs_of' (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) x proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (epptr := ep_q_refs_of' ep))\<rbrace>
     setEndpoint epptr ep
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" unfolding setEndpoint_def by (wp setObject_state_refs_of',
      simp_all add: objBits_simps' fun_upd_def[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(epptr := ep_q_refs_of' ep))\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(epptr := ep_q_refs_of' ep))\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>
theory KHeap_R

lemma set_ntfn_valid_mdb' [wp]:
  "\<lbrace>valid_mdb'\<rbrace>
    setObject epptr (ntfn::Structures_H.notification)
   \<lbrace>\<lambda>_. valid_mdb'\<rbrace>" apply (simp add: valid_mdb'_def) apply (rule set_ntfn_ctes_of[simplified setNotification_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb'\<rbrace> setObject epptr ntfn \<lbrace>\<lambda>_. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb_ctes (ctes_of s)\<rbrace> setObject epptr ntfn \<lbrace>\<lambda>_ s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_valid_objs':
  "\<lbrace>valid_objs' and valid_ntfn' ntfn\<rbrace>
    setNotification p ntfn
   \<lbrace>\<lambda>r s. valid_objs' s\<rbrace>" apply (simp add: setNotification_def) apply (rule setObject_valid_objs') apply (clarsimp simp: updateObject_default_def in_monad
                        valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_ntfn' ntfn\<rbrace> setNotification p ntfn \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_ntfn' ntfn\<rbrace> setObject p ntfn \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject ntfn ko p x n s); valid_ntfn' ntfn s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_valid_bitmapQ[wp]:
  "\<lbrace>Invariants_H.valid_bitmapQ\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. Invariants_H.valid_bitmapQ\<rbrace>" apply (unfold setNotification_def) apply (rule setObject_ntfn_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and ntfn_at' p\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])) and ntfn_at' p\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default ntfn (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans \<rbrace>" apply (unfold setNotification_def) apply (rule setObject_ntfn_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and ntfn_at' p\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) and ntfn_at' p\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default ntfn (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans \<rbrace>" apply (unfold setNotification_def) apply (rule setObject_ntfn_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and ntfn_at' p\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d i. (\<exists>j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i) and ntfn_at' p\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default ntfn (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. \<forall>d i. (\<exists>j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (epptr := ntfn_q_refs_of' (ntfnObj ntfn)
                                      \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn)))\<rbrace>
     setNotification epptr ntfn
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" unfolding setNotification_def by (wp setObject_state_refs_of',
      simp_all add: objBits_simps' fun_upd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(epptr := ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn)))\<rbrace> setNotification epptr ntfn \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(epptr := ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn)))\<rbrace> setObject epptr ntfn \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>
theory KHeap_R

lemma setNotification_pred_tcb_at'[wp]:
  "\<lbrace>pred_tcb_at' proj P t\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" apply (simp add: pred_tcb_at'_def setNotification_def) apply (rule obj_at_setObject2) apply simp apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject_default v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> TCBT proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_ntfn_cur_domain[wp]:
  "\<lbrace> \<lambda>s. P (ksCurDomain s) \<rbrace> setObject ptr (ntfn::Structures_H.notification) \<lbrace> \<lambda>_s . P (ksCurDomain s) \<rbrace>" apply (clarsimp simp: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- updateObject_default ntfn (snd p) ptr (fst p) (snd (lookupAround2 ptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_ksCurDomain[wp]:
  "\<lbrace> \<lambda>s. P (ksCurDomain s) \<rbrace> setNotification ptr (ntfn::Structures_H.notification) \<lbrace> \<lambda>_s . P (ksCurDomain s) \<rbrace>" apply (simp add: setNotification_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> setNotification epptr ep \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>" apply (clarsimp simp: setNotification_def) apply (rule tcb_in_cur_domain'_lift; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> setNotification epptr ep \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> setObject epptr ep \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
     setNotification ntfnptr ntfn
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (wp sch_act_wf_lift | clarsimp simp: setNotification_def)+ apply (simp add: setNotification_def split_def setObject_def
         | wp updateObject_default_inv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> setNotification ntfnptr ntfn \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject ntfnptr ntfn \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setNotification ntfnptr ntfn \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>s. sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_cur_tcb'[wp]:
  "\<lbrace>cur_tcb'\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" apply (wp cur_tcb_lift) apply (simp add: setNotification_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>s. cur_tcb' s \<Longrightarrow> cur_tcb' s proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- updateObject_default ntfn (snd p) ptr (fst p) (snd (lookupAround2 ptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>s. cur_tcb' s \<Longrightarrow> cur_tcb' s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setEndpoint_typ_at'[wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" unfolding setEndpoint_def by (rule setObject_typ_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>