kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_R

lemma reply_descendants_mdbNext_nonnull:
  assumes descs: "descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {}"
  and        sr: "(s, s') \<in> state_relation"
  and       tcb: "st_tcb_at (Not \<circ> halted) t s"
  and       cte: "ctes_of s' (t + 2*2^cte_level_bits) = Some cte"
  shows          "mdbNext (cteMDBNode cte) \<noteq> nullPointer" proof - from tcb have "cte_at (t, tcb_cnode_index 2) s" by (simp add: st_tcb_at_tcb_at tcb_at_cte_at dom_tcb_cap_cases) hence "descendants_of' (t + 2*2^cte_level_bits) (ctes_of s') \<noteq> {}" using sr descs by (fastforce simp: state_relation_def cdt_relation_def cte_map_def tcb_cnode_index_def) thus ?thesis using cte unfolding nullPointer_def by (fastforce simp: descendants_of'_def dest: subtree_next_0) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer proof (state)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer proof (chain)
picking this:
st_tcb_at (Not \<circ> halted) t s proof (prove)
using this:
st_tcb_at (Not \<circ> halted) t s

goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s proof (state)
this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer proof (prove)
using this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') \<noteq> {} proof (prove)
using this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s
(s, s') \<in> state_relation
descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {}

goal (1 subgoal):
 1. descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') \<noteq> {} proof (state)
this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') \<noteq> {}

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer proof (prove)
using this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') \<noteq> {}

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer proof (prove)
using this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') \<noteq> {}
ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer proof (prove)
using this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') \<noteq> {}
ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> 0 proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> nullPointer

goal:
No subgoals!
theory IpcCancel_R

lemma reply_descendants_of_mdbNext:
  "\<lbrakk> (s, s') \<in> state_relation; valid_reply_caps s; valid_reply_masters s;
     valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s';
     pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s;
     ctes_of s' (t + 2*2^cte_level_bits) = Some cte \<rbrakk> \<Longrightarrow>
   (descendants_of (t, tcb_cnode_index 2) (cdt s) = {}) =
       (mdbNext (cteMDBNode cte) = nullPointer)" apply (case_tac "descendants_of (t, tcb_cnode_index 2) (cdt s) = {}") apply (simp add: reply_no_descendants_mdbNext_null) apply (simp add: reply_descendants_mdbNext_nonnull) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte\<rbrakk> \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {}) = (mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte; descendants_of (t, tcb_cnode_index 2) (cdt s) = {}\<rbrakk> \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {}) = (mdbNext (cteMDBNode cte) = nullPointer)
 2. \<lbrakk>(s, s') \<in> state_relation; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte; descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {}) = (mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte; descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {}) = (mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setNotification_utr[wp]:
  "\<lbrace>untyped_ranges_zero'\<rbrace> setNotification ntfn nobj \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) apply (simp add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero'\<rbrace> setNotification ntfn nobj \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s)\<rbrace> setNotification ntfn nobj \<lbrace>\<lambda>rv s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s) \<Longrightarrow> untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setEndpoint_utr[wp]:
  "\<lbrace>untyped_ranges_zero'\<rbrace> setEndpoint p ep \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) apply (simp add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero'\<rbrace> setEndpoint p ep \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s)\<rbrace> setEndpoint p ep \<lbrace>\<lambda>rv s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s) \<Longrightarrow> untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma sch_act_simple_not_t[simp]: "sch_act_simple s \<Longrightarrow> sch_act_not t s" by (clarsimp simp: sch_act_simple_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple s \<Longrightarrow> sch_act_not t s
theory IpcCancel_R

lemma ep_redux_simps3:
  "ep_q_refs_of' (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> RecvEP (y # ys))
        = (set xs \<times> {EPRecv})"
  "ep_q_refs_of' (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> SendEP (y # ys))
        = (set xs \<times> {EPSend})" by (fastforce split: list.splits simp: valid_ep_def valid_ntfn_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_q_refs_of' (case xs of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> Structures_H.endpoint.RecvEP (y # ys)) = set xs \<times> {EPRecv} &&& ep_q_refs_of' (case xs of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> Structures_H.endpoint.SendEP (y # ys)) = set xs \<times> {EPSend}
theory IpcCancel_R

lemma setEndpoint_pde_mappings'[wp]:
  "\<lbrace>valid_pde_mappings'\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (wp valid_pde_mappings_lift') apply (simp add: setEndpoint_def) apply (rule obj_at_setObject2) apply (clarsimp dest!: updateObject_default_result)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings'\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x ko s' v oko xa y n s. (ko, s') \<in> fst (updateObject v oko xa y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(ARM_H.pde)
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setEndpoint_vms[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setEndpoint epptr ep' \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" by (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def)
     (wp hoare_vcg_all_lift hoare_vcg_disj_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> setEndpoint epptr ep' \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>
theory IpcCancel_R

lemma setEndpoint_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>" apply (simp add: setEndpoint_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

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

lemma setEndpoint_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace> ct_idle_or_in_cur_domain' \<rbrace> setEndpoint ptr ep \<lbrace> \<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift hoare_vcg_imp_lift setObject_ep_ct
       | rule obj_at_setObject2
       | clarsimp simp: updateObject_default_def in_monad setEndpoint_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>d a t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setEndpoint_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> setEndpoint eeptr ep' \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF setEndpoint_nosch]) apply (simp add: setEndpoint_def) apply (rule hoare_weaken_pre) apply (wps setObject_ep_ct) apply (wp obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> setEndpoint eeptr ep' \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setEndpoint eeptr ep' \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setObject eeptr ep' \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q10\<rbrace> setObject eeptr ep' \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q10 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P13 prev_s\<rbrace> setObject eeptr ep' \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P13 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s 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)
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setEndpoint_ksDomScheduleIdx[wp]:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace>" apply (simp add: setEndpoint_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

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

lemma (in delete_one_conc_pre) cancelIPC_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace>
    cancelIPC t
   \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (simp add: cancelIPC_def cancelSignal_def Let_def
             cong: if_cong Structures_H.thread_state.case_cong) apply (wp hoare_drop_imps delete_one_sch_act_simple
       | simp add: getThreadReplySlot_def | wpcw
       | rule sch_act_simple_lift
       | (rule_tac Q="\<lambda>rv. sch_act_simple" in hoare_post_imp, simp))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> getThreadState t >>= Structures_H.thread_state.case_thread_state (\<lambda>x xa. do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) (\<lambda>x. do ntfn <- getNotification x;
y <- assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn);
y <- setNotification x (ntfnObj_update (\<lambda>_. ntfn') ntfn);
setThreadState Structures_H.thread_state.Inactive t
od) (return ()) (return ()) (return ()) (\<lambda>x xa xb xc xd. do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od) (return ()) \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma cancelSignal_st_tcb_at:
  assumes x[simp]: "P Inactive" shows
  "\<lbrace>st_tcb_at' P t\<rbrace>
     cancelSignal t' ntfn
   \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" apply (simp add: cancelSignal_def Let_def list_case_If) apply (wp sts_st_tcb_at'_cases hoare_vcg_const_imp_lift
            hoare_drop_imp[where R="%rv s. P' rv" for P']) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> cancelSignal t' ntfn \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- if remove1 t' (ntfnQueue (ntfnObj ntfna)) = [] then return $ Structures_H.ntfn.IdleNtfn else return $ ntfnQueue_update (\<lambda>_. remove1 t' (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t'
od \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' P t s \<Longrightarrow> (t' = t \<longrightarrow> P Structures_H.thread_state.Inactive \<and> tcb_at' t s \<and> tcb_at' t s) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' P t s \<and> st_tcb_at' P t s) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma sts_sch_act_not[wp]:
  "\<lbrace>sch_act_not t\<rbrace> setThreadState st t' \<lbrace>\<lambda>rv. sch_act_not t\<rbrace>" apply (simp add: setThreadState_def rescheduleRequired_def) apply (wp hoare_drop_imps | simp | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_not t\<rbrace> setThreadState st t' \<lbrace>\<lambda>rv. sch_act_not t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_not t\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) (do action <- getSchedulerAction;
y <- case action of SwitchToThread x \<Rightarrow> tcbSchedEnqueue x | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od)
od \<lbrace>\<lambda>rv. sch_act_not t\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma cancelSignal_tcb_at_runnable':
  "t \<noteq> t' \<Longrightarrow>
  \<lbrace>st_tcb_at' runnable' t'\<rbrace> cancelSignal t ntfnptr \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>" unfolding cancelSignal_def by (wpsimp wp: sts_pred_tcb_neq' hoare_drop_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at' runnable' t'\<rbrace> cancelSignal t ntfnptr \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at' runnable' t'\<rbrace> let isWaiting = \<lambda>ntfn. case ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False in do ntfn <- getNotification ntfnptr;
haskell_assert (isWaiting (ntfnObj ntfn)) [];
queue' <- return (delete t $ ntfnQueue $ ntfnObj ntfn);
ntfn' <- case queue' of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. queue') (ntfnObj ntfn);
setNotification ntfnptr (ntfnObj_update (\<lambda>_. ntfn') ntfn);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
theory IpcCancel_R

lemma cancelAllIPC_tcb_at_runnable':
  "\<lbrace>st_tcb_at' runnable' t\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>" unfolding cancelAllIPC_def by (wpsimp wp: mapM_x_wp' sts_st_tcb' hoare_drop_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' t\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' t\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>
theory IpcCancel_R

lemma cancelAllSignals_tcb_at_runnable':
  "\<lbrace>st_tcb_at' runnable' t\<rbrace> cancelAllSignals ntfnptr \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>" unfolding cancelAllSignals_def by (wpsimp wp: mapM_x_wp' sts_st_tcb' hoare_drop_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' t\<rbrace> cancelAllSignals ntfnptr \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' t\<rbrace> do ntfn <- getNotification ntfnptr;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>