kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_R

lemma (in delete_one_conc_pre) suspend_nonq:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and tcb_at' t
                 and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
                 and (\<lambda>s. t \<noteq> ksIdleThread s) and K (t = t')\<rbrace>
     suspend t
   \<lbrace>\<lambda>rv s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: suspend_def unless_def) unfolding updateRestartPC_def apply (wp hoare_allI tcbSchedDequeue_t_notksQ sts_ksQ_oaQ) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. t \<noteq> ksIdleThread s) and K (t = t')\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. t = t' \<Longrightarrow> \<lbrace>Invariants_H.valid_queues and valid_objs' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. t = t' \<Longrightarrow> \<lbrace>Invariants_H.valid_queues and valid_objs' and tcb_at' t' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. t' \<noteq> ksIdleThread s)\<rbrace> do y <- cancelIPC t';
state <- getThreadState t';
y <- if state = Structures_H.thread_state.Running then updateRestartPC t' else return ();
y <- setThreadState Structures_H.thread_state.Inactive t';
tcbSchedDequeue t'
od \<lbrace>\<lambda>rv s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. t = t' \<Longrightarrow> \<lbrace>Invariants_H.valid_queues and valid_objs' and tcb_at' t' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. t' \<noteq> ksIdleThread s)\<rbrace> do y <- cancelIPC t';
state <- getThreadState t';
y <- if state = Structures_H.thread_state.Running then asUser t' (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) else return ();
y <- setThreadState Structures_H.thread_state.Inactive t';
tcbSchedDequeue t'
od \<lbrace>\<lambda>rv s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d p y. t = t' \<Longrightarrow> \<lbrace>?B5 d p y\<rbrace> getThreadState t' \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> Invariants_H.valid_queues s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> Invariants_H.valid_queues s)\<rbrace>
 2. \<And>d p. t = t' \<Longrightarrow> \<lbrace>?Q2\<rbrace> cancelIPC t' \<lbrace>?B5 d p\<rbrace>
 3. \<And>s. \<lbrakk>t = t'; (Invariants_H.valid_queues and valid_objs' and tcb_at' t' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. t' \<noteq> ksIdleThread s)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma suspend_makes_inactive:
  "\<lbrace>K (t = t')\<rbrace> suspend t \<lbrace>\<lambda>rv. st_tcb_at' ((=) Inactive) t'\<rbrace>" apply (cases "t = t'", simp_all) apply (simp add: suspend_def unless_def) apply (wp threadSet_pred_tcb_no_state setThreadState_st_tcb | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (t = t')\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. st_tcb_at' ((=) Structures_H.thread_state.Inactive) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> ThreadDecls_H.suspend t' \<lbrace>\<lambda>rv. st_tcb_at' ((=) Structures_H.thread_state.Inactive) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> do y <- cancelIPC t';
state <- getThreadState t';
y <- if state = Structures_H.thread_state.Running then updateRestartPC t' else return ();
y <- setThreadState Structures_H.thread_state.Inactive t';
tcbSchedDequeue t'
od \<lbrace>\<lambda>rv. st_tcb_at' ((=) Structures_H.thread_state.Inactive) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma tcbSchedEnqueue_sch_act_not_ct[wp]:
  "\<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>" by (rule hoare_weaken_pre, wps tcbSchedEnqueue_ct', wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>
theory IpcCancel_R

lemma sts_sch_act_not_ct[wp]:
  "\<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace>
   setThreadState st t \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>" by (rule hoare_weaken_pre, wps tcbSchedEnqueue_ct', wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>
theory IpcCancel_R

lemma set_ntfn_tcb_obj_at' [wp]:
  "\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace>
     setNotification ntfn v
   \<lbrace>\<lambda>_. obj_at' P t\<rbrace>" apply (clarsimp simp: setNotification_def, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setNotification ntfn v \<lbrace>\<lambda>_. obj_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma tcbSchedEnqueue_cur_tcb'[wp]:
  "\<lbrace>cur_tcb'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. cur_tcb'\<rbrace>" by (simp add: tcbSchedEnqueue_def unless_def)
     (wp threadSet_cur setQueue_cur | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. cur_tcb'\<rbrace>
theory IpcCancel_R

lemma rescheduleRequired_invs'[wp]:
  "\<lbrace>invs'\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp ssa_invs' | simp | wpc)+ apply (clarsimp simp: invs'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma invs_rct_ct_activatable':
  "\<lbrakk> invs' s; ksSchedulerAction s = ResumeCurrentThread \<rbrakk>
   \<Longrightarrow> st_tcb_at' activatable' (ksCurThread s) s" by (simp add: invs'_def valid_state'_def ct_in_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> st_tcb_at' activatable' (ksCurThread s) s
theory IpcCancel_R

lemma ct_not_in_ntfnQueue:
  assumes ko_at:  "ko_at' r ntfn_ptr s" and
          srefs:  "sym_refs (state_refs_of' s)" and
          nidle:  "ntfnObj r \<noteq> IdleNtfn \<and> (\<forall>b m. ntfnObj r \<noteq> ActiveNtfn b)" and
          st_act: "ct_in_state' simple' s"
  shows   "ksCurThread s \<notin> set (ntfnQueue (ntfnObj r))" using assms unfolding ct_in_state'_def by (rule not_in_ntfnQueue)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksCurThread s \<notin> set (ntfnQueue (ntfnObj r)) proof (prove)
using this:
ko_at' r ntfn_ptr s
sym_refs (state_refs_of' s)
ntfnObj r \<noteq> Structures_H.ntfn.IdleNtfn \<and> (\<forall>b m. ntfnObj r \<noteq> Structures_H.ntfn.ActiveNtfn b)
ct_in_state' simple' s

goal (1 subgoal):
 1. ksCurThread s \<notin> set (ntfnQueue (ntfnObj r)) proof (prove)
using this:
ko_at' r ntfn_ptr s
sym_refs (state_refs_of' s)
ntfnObj r \<noteq> Structures_H.ntfn.IdleNtfn \<and> (\<forall>b m. ntfnObj r \<noteq> Structures_H.ntfn.ActiveNtfn b)
st_tcb_at' simple' (ksCurThread s) s

goal (1 subgoal):
 1. ksCurThread s \<notin> set (ntfnQueue (ntfnObj r))
theory IpcCancel_R

lemma sch_act_wf_weak[elim!]:
  "sch_act_wf sa s \<Longrightarrow> weak_sch_act_wf sa s" by (case_tac sa, (simp add: weak_sch_act_wf_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_wf sa s \<Longrightarrow> weak_sch_act_wf sa s
theory IpcCancel_R

lemma cancelAllIPC_st_tcb_at:
  assumes x[simp]: "P Restart" shows
  "\<lbrace>st_tcb_at' P t\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" unfolding cancelAllIPC_def by (wp ep'_cases_weak_wp mapM_x_wp' sts_st_tcb_at'_cases | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P 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>rv. st_tcb_at' P t\<rbrace>
theory IpcCancel_R

lemma cancelAllSignals_st_tcb_at:
  assumes x[simp]: "P Restart" shows
  "\<lbrace>st_tcb_at' P t\<rbrace> cancelAllSignals epptr \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" unfolding cancelAllSignals_def by (wp ntfn'_cases_weak_wp mapM_x_wp' sts_st_tcb_at'_cases | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> cancelAllSignals epptr \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> do ntfn <- getNotification epptr;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification epptr (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>rv. st_tcb_at' P t\<rbrace>
theory IpcCancel_R

lemma threadSet_not_tcb[wp]:
  "\<lbrace>ko_wp_at' (\<lambda>x. P x \<and> (projectKO_opt x = (None :: tcb option))) p\<rbrace>
     threadSet f t
   \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>x. P x \<and> (projectKO_opt x = (None :: tcb option))) p\<rbrace>" by (clarsimp simp: threadSet_def valid_def getObject_def
                     setObject_def in_monad loadObject_default_def
                     ko_wp_at'_def projectKOs split_def in_magnitude_check
                     objBits_simps' updateObject_default_def
                     ps_clear_upd projectKO_opt_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>x. P x \<and> projectKO_opt x = None) p\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>x. P x \<and> projectKO_opt x = None) p\<rbrace>
theory IpcCancel_R

lemma setThreadState_not_tcb[wp]:
  "\<lbrace>ko_wp_at' (\<lambda>x. P x \<and> (projectKO_opt x = (None :: tcb option))) p\<rbrace>
     setThreadState st t
   \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>x. P x \<and> (projectKO_opt x = (None :: tcb option))) p\<rbrace>" apply (simp add: setThreadState_def setQueue_def
                   rescheduleRequired_def tcbSchedEnqueue_def
                   unless_def bitmap_fun_defs
             cong: scheduler_action.case_cong  cong del: if_cong
            | wp | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>x. P x \<and> projectKO_opt x = None) p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>x. P x \<and> projectKO_opt x = None) p\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma tcbSchedEnqueue_unlive:
  "\<lbrace>ko_wp_at' (\<lambda>x. \<not> live' x \<and> (projectKO_opt x = (None :: tcb option))) p
    and tcb_at' t\<rbrace>
    tcbSchedEnqueue t
   \<lbrace>\<lambda>_. ko_wp_at' (\<lambda>x. \<not> live' x \<and> (projectKO_opt x = (None :: tcb option))) p\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp | simp add: setQueue_def bitmap_fun_defs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p and tcb_at' t\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p and tcb_at' t\<rbrace> do queued <- threadGet tcbQueued t;
when (\<not> queued) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setObject_ko_wp_at':
  fixes v :: "'a :: pspace_storable"
  assumes x: "\<And>v :: 'a. updateObject v = updateObject_default v"
  assumes n: "\<And>v :: 'a. objBits v = n"
  assumes v: "(1 :: word32) < 2 ^ n"
  shows
  "\<lbrace>\<lambda>s. P (injectKO v)\<rbrace> setObject p v \<lbrace>\<lambda>rv. ko_wp_at' P p\<rbrace>" by (clarsimp simp: setObject_def valid_def in_monad
                     ko_wp_at'_def x split_def n
                     updateObject_default_def
                     objBits_def[symmetric] ps_clear_upd
                     in_magnitude_check v projectKOs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (injectKO v)\<rbrace> setObject p v \<lbrace>\<lambda>rv. ko_wp_at' P p\<rbrace>
theory InterruptAcc_R

lemma getIRQSlot_corres:
  "corres (\<lambda>sl sl'. sl' = cte_map sl) \<top> \<top> (get_irq_slot irq) (getIRQSlot irq)" apply (simp add: getIRQSlot_def get_irq_slot_def locateSlot_conv
                   liftM_def[symmetric]) apply (simp add: getInterruptState_def) apply (clarsimp simp: state_relation_def interrupt_state_relation_def) apply (simp add: cte_map_def cte_level_bits_def
                   ucast_nat_def shiftl_t2n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>sl sl'. sl' = cte_map sl) (\<lambda>_. True) (\<lambda>_. True) (get_irq_slot irq) (getIRQSlot irq) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x. (\<lambda>sl'. sl' = cte_map x) \<circ> (\<lambda>node. node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) \<circ> intStateIRQNode) (\<lambda>_. True) (\<lambda>_. True) (gets (\<lambda>st. (interrupt_irq_node st irq, []))) getInterruptState proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> irq_node' s' + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq = cte_map (interrupt_irq_node s irq, []) proof (prove)
goal (1 subgoal):
 1. \<And>s s' node irqs'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; cur_thread s = ksCurThread s'; ksInterruptState s' = InterruptState node irqs'; idle_thread s = ksIdleThread s'; \<forall>irq. interrupt_irq_node s irq = node + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits); \<forall>irq. irq_state_relation (interrupt_states s irq) (irqs' irq); machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq = cte_map (node + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), []) proof (prove)
goal:
No subgoals!
theory InterruptAcc_R

lemma getIRQSlot_real_cte[wp]:
  "\<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>real_cte_at'\<rbrace>" apply (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) apply wp apply (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def
                        cte_level_bits_def ucast_nat_def cteSizeBits_def shiftl_t2n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>real_cte_at'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
return (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>real_cte_at'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>node. real_cte_at' (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)) \<circ> intStateIRQNode) (ksInterruptState s) s proof (prove)
goal:
No subgoals!
theory InterruptAcc_R

lemma getIRQSlot_cte_at[wp]:
  "\<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>cte_at'\<rbrace>" apply (rule hoare_strengthen_post [OF getIRQSlot_real_cte]) apply (clarsimp simp: real_cte_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. real_cte_at' rv s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) rv s proof (prove)
goal:
No subgoals!
theory InterruptAcc_R

lemma work_units_updated_state_relationI[intro!]:
  "(s,s') \<in> state_relation \<Longrightarrow>
   (work_units_completed_update (\<lambda>_. work_units_completed s + 1) s, s'\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s' + 1\<rparr>) \<in> state_relation" apply (simp add: state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> (work_units_completed_update (\<lambda>_. work_units_completed s + 1) s, s'\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s' + 1\<rparr>) \<in> state_relation proof (prove)
goal:
No subgoals!
theory InterruptAcc_R

lemma work_units_and_irq_state_state_relationI [intro!]:
  "(s, s') \<in> state_relation \<Longrightarrow>
   (s \<lparr> work_units_completed := n,  machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>,
    s' \<lparr> ksWorkUnitsCompleted := n, ksMachineState := ksMachineState s' \<lparr> irq_state := f (irq_state (ksMachineState s')) \<rparr>\<rparr>)
   \<in> state_relation" by (simp add: state_relation_def swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> (s\<lparr>work_units_completed := n, machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>, s'\<lparr>ksWorkUnitsCompleted := n, ksMachineState := ksMachineState s'\<lparr>irq_state := f (irq_state (ksMachineState s'))\<rparr>\<rparr>) \<in> state_relation
theory InterruptAcc_R

lemma preemptionPoint_corres:
  "corres (dc \<oplus> dc) \<top> \<top> preemption_point preemptionPoint" apply (simp add: preemption_point_def preemptionPoint_def) by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
                 corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
                 alternative_def throwError_def returnOk_def return_def lift_def doMachineOp_def split_def
                 put_def getWorkUnits_def setWorkUnits_def modifyWorkUnits_def do_machine_op_def

                 update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def workUnitsLimit_def
                 work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
           elim: state_relationE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) preemption_point preemptionPoint proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (doE y <- liftE update_work_units;
OR_choiceE work_units_limit_reached (doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>x2. throwError ())
odE) (returnOk ())
odE) (doE y <- liftE (modifyWorkUnits (\<lambda>u. u + 1));
workUnits <- liftE getWorkUnits;
whenE (FaultMonad_H.workUnitsLimit \<le> workUnits) (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE)
odE)
theory InterruptAcc_R

lemma preemptionPoint_inv:
  assumes "(\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s)"
          "irq_state_independent_H P"
  shows "\<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace>" using assms apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) apply (wpc
          | wp whenE_wp hoare_seq_ext [OF _ select_inv] hoare_drop_imps
          | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
using this:
P (ksWorkUnitsCompleted_update ?f ?s) = P ?s
irq_state_independent_H P

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s; irq_state_independent_H P\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE y <- liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>));
workUnits <- liftE (gets ksWorkUnitsCompleted);
whenE (FaultMonad_H.workUnitsLimit \<le> workUnits) (doE y <- liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0)));
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE)
odE \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory InterruptAcc_R

lemma ct_running_irq_state_independent[intro!, simp]:
  "ct_running (s \<lparr>machine_state := machine_state s \<lparr>irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
   = ct_running s" by (simp add: ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = ct_running s
theory InterruptAcc_R

lemma ct_idle_irq_state_independent[intro!, simp]:
  "ct_idle (s \<lparr>machine_state := machine_state s \<lparr>irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
   = ct_idle s" by (simp add: ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_idle (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = ct_idle s
theory InterruptAcc_R

lemma typ_at'_irq_state_independent[simp, intro!]:
  "P (typ_at' T p (s \<lparr>ksMachineState := ksMachineState s \<lparr> irq_state := f (irq_state (ksMachineState s)) \<rparr>\<rparr>))
   = P (typ_at' T p s)" by (simp add: typ_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (typ_at' T p (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)) = P (typ_at' T p s)