kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF_Refine

lemma ADT_A_if_enabled:
  "uop_sane uop \<Longrightarrow> enabled_system (ADT_A_if uop) s0" apply (rule Init_Fin_serial.enabled) apply (rule ADT_A_if_Init_Fin_serial) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_sane uop \<Longrightarrow> enabled_system (ADT_A_if uop) s0 proof (prove)
goal (1 subgoal):
 1. uop_sane uop \<Longrightarrow> Init_Fin_serial (ADT_A_if uop) s0 ?I proof (prove)
goal (1 subgoal):
 1. uop_sane uop \<Longrightarrow> uop_sane uop proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma (in valid_initial_state_noenabled) uop_nonempty:
  "uop_nonempty utf" by (simp add: uop_nonempty_def utf_non_empty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty utf
theory ADT_IF_Refine

lemma (in valid_initial_state_noenabled) uop_sane:
  "uop_sane utf" apply (simp add: uop_sane_def utf_non_empty) apply (cut_tac utf_non_interrupt) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_sane utf proof (prove)
goal (1 subgoal):
 1. \<forall>t pl pr pxn a aa ab ac b tc um ad ae ba. (Some Interrupt, tc, um, ad, ae, ba) \<notin> utf t pl pr pxn (a, aa, ab, ac, b) proof (prove)
goal (1 subgoal):
 1. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt \<Longrightarrow> \<forall>t pl pr pxn a aa ab ac b tc um ad ae ba. (Some Interrupt, tc, um, ad, ae, ba) \<notin> utf t pl pr pxn (a, aa, ab, ac, b) proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma kernelEntry_invs'[ADT_IF_Refine_assms, wp]:
  "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)
          and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
          and arch_extras\<rbrace>
   kernelEntry_if e tc
   \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: kernelEntry_if_def) apply (wp threadSet_invs_trivial threadSet_ct_running' hoare_weak_lift_imp
         | wp (once) hoare_drop_imps
         | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> do t <- getCurThread;
y <- threadSet (tcbArch_update (atcbContextSet tc)) t;
r <- handleEvent e;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (e = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma kernelEntry_arch_extras[ADT_IF_Refine_assms, wp]:
  "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)
          and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
          and arch_extras\<rbrace>
   kernelEntry_if e tc
   \<lbrace>\<lambda>_. arch_extras\<rbrace>" apply (simp add: kernelEntry_if_def) apply (wp handleEvent_valid_duplicates' threadSet_invs_trivial threadSet_ct_running' hoare_weak_lift_imp
         | wp (once) hoare_drop_imps
         | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>_. arch_extras\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> do t <- getCurThread;
y <- threadSet (tcbArch_update (atcbContextSet tc)) t;
r <- handleEvent e;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (e = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma arch_tcb_context_set_tcb_relation[ADT_IF_Refine_assms]:
  "tcb_relation tcb tcb'
   \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>)
                    (tcbArch_update (atcbContextSet tc) tcb')" by (simp add: tcb_relation_def arch_tcb_relation_def arch_tcb_context_set_def atcbContextSet_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) (tcbArch_update (atcbContextSet tc) tcb')
theory ArchADT_IF_Refine

lemma arch_tcb_context_get_atcbContextGet[ADT_IF_Refine_assms]:
  "tcb_relation tcb tcb'
   \<Longrightarrow> (arch_tcb_context_get \<circ> tcb_arch) tcb = (atcbContextGet \<circ> tcbArch) tcb'" by (simp add: tcb_relation_def arch_tcb_relation_def arch_tcb_context_get_def atcbContextGet_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_relation tcb tcb' \<Longrightarrow> (arch_tcb_context_get \<circ> tcb_arch) tcb = (atcbContextGet \<circ> tcbArch) tcb'
theory ArchADT_IF_Refine

lemma getExMonitor_empty_fail[wp]:
  "empty_fail getExMonitor" by (simp add: getExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail getExMonitor
theory ArchADT_IF_Refine

lemma setExMonitor_empty_fail[wp]:
  "empty_fail (setExMonitor es)" by (simp add: setExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (setExMonitor es)
theory ArchADT_IF_Refine

lemma getExMonitor_no_fail[wp]:
  "no_fail \<top> getExMonitor" by (simp add: getExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) getExMonitor
theory ArchADT_IF_Refine

lemma setExMonitor_no_fail'[wp]:
  "no_fail \<top> (setExMonitor (x, y))" by (simp add: setExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setExMonitor (x, y))
theory ArchADT_IF_Refine

lemma setExMonitor_no_fail[wp]:
  "no_fail \<top> (setExMonitor es)" by (simp add: setExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setExMonitor es)
theory ArchADT_IF_Refine

lemma ptable_attrs_abs_state[simp]:
  "ptable_attrs thread (abs_state s) = ptable_attrs thread s" by (simp add: ptable_attrs_def abs_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptable_attrs thread (abs_state s) = ptable_attrs thread s
theory ArchADT_IF_Refine

lemma dmo_getExMonitor_wp'[wp]:
  "\<lbrace>\<lambda>s. P (exclusive_state (ksMachineState s)) s\<rbrace>
   doMachineOp getExMonitor
   \<lbrace>P\<rbrace>" apply(simp add: doMachineOp_def) apply(wp modify_wp | wpc)+ apply clarsimp apply(erule use_valid) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (exclusive_state (ksMachineState s)) s\<rbrace> doMachineOp getExMonitor \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (exclusive_state (ksMachineState s)) s\<rbrace> do ms <- gets ksMachineState;
(r, ms') <- select_f (getExMonitor ms);
y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (exclusive_state (ksMachineState s)) s \<Longrightarrow> \<forall>x\<in>fst (getExMonitor (ksMachineState s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P xa (s\<lparr>ksMachineState := xb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa bb x. \<lbrakk>P (exclusive_state (ksMachineState s)) s; ((aa, bb), x) \<in> fst (getExMonitor (ksMachineState s))\<rbrakk> \<Longrightarrow> P (aa, bb) (s\<lparr>ksMachineState := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s aa bb x. P (exclusive_state (ksMachineState s)) s \<Longrightarrow> \<lbrace>?P34 s aa bb x\<rbrace> getExMonitor \<lbrace>\<lambda>a b. P a (s\<lparr>ksMachineState := b\<rparr>)\<rbrace>
 2. \<And>s aa bb x. P (exclusive_state (ksMachineState s)) s \<Longrightarrow> ?P34 s aa bb x (ksMachineState s) proof (prove)
goal (1 subgoal):
 1. \<And>s aa bb x. P (exclusive_state (ksMachineState s)) s \<Longrightarrow> P (exclusive_state (ksMachineState s)) (s\<lparr>ksMachineState := ksMachineState s\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma dmo_setExMonitor_wp'[wp]:
  "\<lbrace>\<lambda>s. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace>
   doMachineOp (setExMonitor es)
   \<lbrace>\<lambda>_. P\<rbrace>" apply(simp add: doMachineOp_def) apply(wp modify_wp | wpc)+ apply clarsimp apply(erule use_valid) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace> doMachineOp (setExMonitor es) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace> do ms <- gets ksMachineState;
(r, ms') <- select_f (setExMonitor es ms);
modify (ksMachineState_update (\<lambda>_. ms'))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> \<forall>x\<in>fst (setExMonitor es (ksMachineState s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P (s\<lparr>ksMachineState := xb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>); ((), x) \<in> fst (setExMonitor es (ksMachineState s))\<rbrakk> \<Longrightarrow> P (s\<lparr>ksMachineState := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> \<lbrace>?P27 s x\<rbrace> setExMonitor es \<lbrace>\<lambda>a b. P (s\<lparr>ksMachineState := b\<rparr>)\<rbrace>
 2. \<And>s x. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> ?P27 s x (ksMachineState s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma valid_state'_exclusive_state_update[iff]:
  "valid_state' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = valid_state' s" by (simp add: valid_state'_def valid_machine_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_state' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = valid_state' s
theory ArchADT_IF_Refine

lemma invs'_exclusive_state_update[iff]:
  "invs' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = invs' s" by (simp add: invs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = invs' s
theory ArchADT_IF_Refine

lemma doUserOp_valid_duplicates[ADT_IF_Refine_assms, wp]:
  "doUserOp_if f tc \<lbrace>arch_extras\<rbrace>" apply (simp add: doUserOp_if_def split_def) apply (wp dmo_setExMonitor_wp' dmo_invs' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>arch_extras\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_. arch_extras\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do pr <- gets ptable_rights_s';
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
p <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((fst (snd (snd (snd p))) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor (snd (snd (snd (snd p)))));
return (fst p, fst (snd p))
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma doUserOp_if_schedact[ADT_IF_Refine_assms, wp]:
  "doUserOp_if f tc \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: doUserOp_if_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do pr <- gets ptable_rights_s';
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma doUserOp_if_st_tcb_at[ADT_IF_Refine_assms, wp]:
   "doUserOp_if f tc \<lbrace>st_tcb_at' st t\<rbrace>" apply (simp add: doUserOp_if_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' st t\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_. st_tcb_at' st t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' st t\<rbrace> do pr <- gets ptable_rights_s';
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>_. st_tcb_at' st t\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma doUserOp_if_cur_thread[ADT_IF_Refine_assms, wp]:
  "doUserOp_if f tc \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace>" apply (simp add: doUserOp_if_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do pr <- gets ptable_rights_s';
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma dmo_getActiveIRQ_corres[ADT_IF_Refine_assms]:
  "corres (=) \<top> \<top> (do_machine_op (getActiveIRQ in_kernel)) (doMachineOp (getActiveIRQ in_kernel'))" apply (rule SubMonad_R.corres_machine_op) apply (rule corres_Id) apply (simp add: getActiveIRQ_def non_kernel_IRQs_def) apply simp apply (rule no_fail_getActiveIRQ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (do_machine_op (getActiveIRQ in_kernel)) (doMachineOp (getActiveIRQ in_kernel')) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (getActiveIRQ in_kernel) (getActiveIRQ in_kernel') proof (prove)
goal (3 subgoals):
 1. getActiveIRQ in_kernel = getActiveIRQ in_kernel'
 2. \<And>rv. rv = rv
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) (getActiveIRQ in_kernel') proof (prove)
goal (2 subgoals):
 1. \<And>rv. rv = rv
 2. True \<Longrightarrow> no_fail (\<lambda>_. True) (getActiveIRQ in_kernel') proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> no_fail (\<lambda>_. True) (getActiveIRQ in_kernel') proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma scheduler_if'_arch_extras[ADT_IF_Refine_assms, wp]:
  "\<lbrace>invs' and arch_extras\<rbrace>
   schedule'_if tc
   \<lbrace>\<lambda>_. arch_extras\<rbrace>" apply (simp add: schedule'_if_def) apply (wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and arch_extras\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. arch_extras\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> do y <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma handlePreemption_if_arch_extras[ADT_IF_Refine_assms, wp]:
  "handlePreemption_if tc \<lbrace>arch_extras\<rbrace>" apply (simp add: handlePreemption_if_def) apply (wp dmo'_getActiveIRQ_wp hoare_drop_imps) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>arch_extras\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. arch_extras\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do irq <- doMachineOp (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (if \<exists>y. irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s)) = Some y then \<lambda>s. vs_valid_duplicates' (ksPSpace s) else (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine

lemma handleEvent_corres_arch_extras[ADT_IF_Refine_assms]:
    "corres (dc \<oplus> dc)
       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)
              and (\<lambda>s. scheduler_action s = resume_cur_thread))
       (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s)
              and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
              and arch_extras)
       (handle_event event) (handleEvent event)" by (fastforce intro: corres_guard2_imp[OF handleEvent_corres])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) (handle_event event) (handleEvent event)
theory ADT_IF_Refine_C

lemma corres_select_f':
  "\<lbrakk> \<And>s s'. P s \<Longrightarrow> P' s' \<Longrightarrow> \<forall>s' \<in> fst S'. \<exists>s \<in> fst S. rvr s s'; nf' \<Longrightarrow> \<not> snd S' \<rbrakk>
      \<Longrightarrow> corres_underlying sr nf nf' rvr P P' (select_f S) (select_f S')" by (clarsimp simp: select_f_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; P' s'\<rbrakk> \<Longrightarrow> \<forall>s'\<in>fst S'. \<exists>s\<in>fst S. rvr s s'; nf' \<Longrightarrow> \<not> snd S'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr P P' (select_f S) (select_f S')