theory ArchADT_IF_Refine

lemma do_user_op_if_corres'[ADT_IF_Refine_assms]:
  "corres_underlying state_relation nf False (=) (einvs and ct_running)
     (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running')
     (do_user_op_if f tc) (doUserOp_if f tc)" apply (simp add: do_user_op_if_def doUserOp_if_def) apply (rule corres_gets_same) apply (clarsimp simp: ptable_rights_s_def ptable_rights_s'_def) apply (subst absKState_correct, fastforce, assumption+) apply (clarsimp elim!: state_relationE) apply simp apply (rule corres_gets_same) apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def) apply (subst absKState_correct, fastforce, assumption+) apply (clarsimp elim!: state_relationE) apply simp apply (rule corres_gets_same) apply (clarsimp simp: absArchState_correct curthread_relation ptable_lift_s'_def
                         ptable_lift_s_def) apply (subst absKState_correct, fastforce, assumption+) apply (clarsimp elim!: state_relationE) apply simp apply (simp add: getCurThread_def) apply (rule corres_gets_same) apply (simp add: curthread_relation) apply simp apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> - device_region s"]) apply (clarsimp simp add: user_mem_relation dest!: invs_valid_stateI invs_valid_stateI') apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def) apply fastforce apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> device_region s"]) apply (clarsimp simp add: device_mem_relation dest!: invs_valid_stateI invs_valid_stateI') apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def dom_def) apply (rule corres_gets_same[where R ="\<lambda>r s. dom r = device_region s"]) apply (clarsimp simp: state_relation_def) apply simp apply (rule corres_assert_imp_r) apply fastforce apply (rule corres_assert_imp_r) apply fastforce apply (rule corres_guard_imp) apply (rule corres_split[OF corres_machine_op',where r'="(=)"]) apply (rule corres_underlying_trivial, wp) apply (rule corres_split[where r'="dc"]) apply simp apply (rule corres_assert') apply (rule corres_split[where r'="(=)"]) apply (rule corres_trivial) apply (clarsimp simp: select_def corres_underlying_def) apply clarsimp apply (rule corres_split[OF corres_machine_op',where r'="(=)"]) apply (rule corres_underlying_trivial, simp) apply (rule corres_split[OF corres_machine_op', where r'="(=)"]) apply (rule corres_underlying_trivial, simp) apply (rule corres_split[OF corres_machine_op', where r'="(=)"]) apply (rule corres_underlying_trivial, simp) apply (rule corres_return_same_trivial) by wpsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying state_relation nf False (=) (einvs and ct_running) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do_user_op_if f tc) (doUserOp_if f tc) proof (prove)
goal (1 subgoal):
 1. corres_underlying state_relation nf False (=) (einvs and ct_running) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(einvs and ct_running) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ptable_rights_s s = ptable_rights_s' s'
 2. \<And>s. (einvs and ct_running) s \<Longrightarrow> ?R (ptable_rights_s s) s
 3. \<And>pr. corres_underlying state_relation nf False (=) (einvs and ct_running and ?R pr and (\<lambda>s. pr = ptable_rights_s s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do 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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; invs s; invs' s'; valid_list s; ksSchedulerAction s' = ResumeCurrentThread; ct_running' s'; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s = ptable_rights (ksCurThread s') (absKState s')
 2. \<And>s. (einvs and ct_running) s \<Longrightarrow> ?R (ptable_rights_s s) s
 3. \<And>pr. corres_underlying state_relation nf False (=) (einvs and ct_running and ?R pr and (\<lambda>s. pr = ptable_rights_s s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do 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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; invs s; invs' s'; valid_list s; ksSchedulerAction s' = ResumeCurrentThread; ct_running' s'; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s = ptable_rights (ksCurThread s') (abs_state s)
 2. \<And>s. (einvs and ct_running) s \<Longrightarrow> ?R (ptable_rights_s s) s
 3. \<And>pr. corres_underlying state_relation nf False (=) (einvs and ct_running and ?R pr and (\<lambda>s. pr = ptable_rights_s s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do 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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and ct_running) s \<Longrightarrow> ?R (ptable_rights_s s) s
 2. \<And>pr. corres_underlying state_relation nf False (=) (einvs and ct_running and ?R pr and (\<lambda>s. pr = ptable_rights_s s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do 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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do 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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>pr s s'. \<lbrakk>(einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s' s' x)
 2. \<And>pr s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s \<Longrightarrow> ?R22 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 3. \<And>pr pxn. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R22 pr pxn and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; invs s; invs' s'; valid_list s; ksSchedulerAction s' = ResumeCurrentThread; ct_running' s'; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> (\<lambda>x. ptable_rights_s s x \<noteq> {} \<and> XNever \<in> ptable_attrs (cur_thread s) s x) = (\<lambda>x. ptable_rights_s s x \<noteq> {} \<and> XNever \<in> ptable_attrs (ksCurThread s') (absKState s') x)
 2. \<And>pr s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s \<Longrightarrow> ?R22 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 3. \<And>pr pxn. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R22 pr pxn and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; invs s; invs' s'; valid_list s; ksSchedulerAction s' = ResumeCurrentThread; ct_running' s'; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> (\<lambda>x. ptable_rights_s s x \<noteq> {} \<and> XNever \<in> ptable_attrs (cur_thread s) s x) = (\<lambda>x. ptable_rights_s s x \<noteq> {} \<and> XNever \<in> ptable_attrs (ksCurThread s') (abs_state s) x)
 2. \<And>pr s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s \<Longrightarrow> ?R22 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 3. \<And>pr pxn. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R22 pr pxn and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s \<Longrightarrow> ?R22 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 2. \<And>pr pxn. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R22 pr pxn and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn s s'. \<lbrakk>(einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ptable_lift_s s |` {x. pr x \<noteq> {}} = ptable_lift_s' s' |` {x. pr x \<noteq> {}}
 2. \<And>pr pxn s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) s \<Longrightarrow> ?R44 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 3. \<And>pr pxn pl. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and ?R44 pr pxn pl and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; invs s; invs' s'; valid_list s; ksSchedulerAction s' = ResumeCurrentThread; ct_running' s'; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s |` {x. ptable_rights_s s x \<noteq> {}} = ptable_lift (cur_thread s) (absKState s') |` {x. ptable_rights_s s x \<noteq> {}}
 2. \<And>pr pxn s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) s \<Longrightarrow> ?R44 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 3. \<And>pr pxn pl. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and ?R44 pr pxn pl and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; invs s; invs' s'; valid_list s; ksSchedulerAction s' = ResumeCurrentThread; ct_running' s'; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s |` {x. ptable_rights_s s x \<noteq> {}} = ptable_lift (cur_thread s) (abs_state s) |` {x. ptable_rights_s s x \<noteq> {}}
 2. \<And>pr pxn s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) s \<Longrightarrow> ?R44 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 3. \<And>pr pxn pl. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and ?R44 pr pxn pl and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn s. (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x))) s \<Longrightarrow> ?R44 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 2. \<And>pr pxn pl. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and ?R44 pr pxn pl and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>a. True) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>a. True) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do t <- gets ksCurThread;
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) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn pl s s'. \<lbrakk>(einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> cur_thread s = ksCurThread s'
 2. \<And>pr pxn pl s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) s \<Longrightarrow> ?R62 pr pxn pl (cur_thread s) s
 3. \<And>pr pxn pl r. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and ?R62 pr pxn pl r and (\<lambda>s. r = cur_thread s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}})) s \<Longrightarrow> ?R62 pr pxn pl (cur_thread s) s
 2. \<And>pr pxn pl r. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and ?R62 pr pxn pl r and (\<lambda>s. r = cur_thread s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn pl r s s'. \<lbrakk>(einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s)) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> user_mem s \<circ> ptrFromPAddr = user_mem' s' \<circ> ptrFromPAddr
 2. \<And>pr pxn pl r s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s)) s \<Longrightarrow> dom (user_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))
 3. \<And>pr pxn pl r um. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl r s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s)) s \<Longrightarrow> dom (user_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))
 2. \<And>pr pxn pl r um. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>s x y ya. \<lbrakk>user_mem s x = Some y; device_state (machine_state s) x = Some ya; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; ct_running s\<rbrakk> \<Longrightarrow> False
 2. \<And>pr pxn pl r um. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn pl r um s s'. \<lbrakk>(einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> device_mem s \<circ> ptrFromPAddr = device_mem' s' \<circ> ptrFromPAddr
 2. \<And>pr pxn pl r um s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) s \<Longrightarrow> dom (device_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))
 3. \<And>pr pxn pl r um dm. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl r um s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr)) s \<Longrightarrow> dom (device_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))
 2. \<And>pr pxn pl r um dm. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um dm. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do 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 r 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 r 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) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn pl r um dm s s'. \<lbrakk>(einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr)) s; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (device_state \<circ> machine_state) s = (device_state \<circ> ksMachineState) s'
 2. \<And>pr pxn pl r um dm s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr)) s \<Longrightarrow> dom ((device_state \<circ> machine_state) s) = dom (device_state (machine_state s))
 3. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl r um dm s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr)) s \<Longrightarrow> dom ((device_state \<circ> machine_state) s) = dom (device_state (machine_state s))
 2. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds
 2. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds
 2. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn pl r um dm ds. corres_underlying state_relation nf False (=) (?Q250 pr pxn pl r um dm ds) (?Q'250 pr pxn pl r um dm ds) (do es <- do_machine_op getExMonitor;
y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do es <- doMachineOp getExMonitor;
y <- assert (f r 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 r 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)
 2. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ?Q250 pr pxn pl r um dm ds s
 3. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ?Q'250 pr pxn pl r um dm ds s proof (prove)
goal (6 subgoals):
 1. \<And>pr pxn pl r um dm ds. corres_underlying Id nf False (=) (?P255 pr pxn pl r um dm ds) (?Q255 pr pxn pl r um dm ds) getExMonitor getExMonitor
 2. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> corres_underlying state_relation nf False (=) (?R254 pr pxn pl r um dm ds es) (?R'254 pr pxn pl r um dm ds esa) (do y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (f r 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}, esa) \<noteq> {});
(e, tc', um', ds', es') <- select (f r 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}, esa));
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)
 3. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?R254 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>?R'254 pr pxn pl r um dm ds\<rbrace>
 5. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> (?P255 pr pxn pl r um dm ds \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 6. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> (?Q255 pr pxn pl r um dm ds \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (5 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> corres_underlying state_relation nf False (=) (?R254 pr pxn pl r um dm ds es) (?R'254 pr pxn pl r um dm ds esa) (do y <- assert (f r 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 r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do y <- assert (f r 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}, esa) \<noteq> {});
(e, tc', um', ds', es') <- select (f r 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}, esa));
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)
 2. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?R254 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>?R'254 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 5. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (8 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> corres_underlying state_relation nf False dc (?P265 pr pxn pl r um dm ds es) (?P'267 pr pxn pl r um dm ds esa) (assert (f r 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> {})) (assert (f r 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}, esa) \<noteq> {}))
 2. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R264 pr pxn pl r um dm ds es esa y) (?R'264 pr pxn pl r um dm ds es esa ya) (do (e, tc', um', ds', es') <- select (f r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do (e, tc', um', ds', es') <- select (f r 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}, esa));
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)
 3. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>?R264 pr pxn pl r um dm ds es esa\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>?R'264 pr pxn pl r um dm ds es esa\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. ?P265 pr pxn pl r um dm ds es and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. ?P'267 pr pxn pl r um dm ds esa and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 7. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 8. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (8 subgoals):
 1. \<And>pr pxn pl r um dm ds es. corres_underlying state_relation nf False dc (?P265 pr pxn pl r um dm ds es) (?P'267 pr pxn pl r um dm ds es) (assert (f r 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> {})) (assert (f r 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> {}))
 2. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R264 pr pxn pl r um dm ds es esa y) (?R'264 pr pxn pl r um dm ds es esa ya) (do (e, tc', um', ds', es') <- select (f r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do (e, tc', um', ds', es') <- select (f r 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}, esa));
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)
 3. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>?R264 pr pxn pl r um dm ds es esa\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>?R'264 pr pxn pl r um dm ds es esa\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. ?P265 pr pxn pl r um dm ds es and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. ?P'267 pr pxn pl r um dm ds esa and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 7. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 8. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (7 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R264 pr pxn pl r um dm ds es esa y) (?R'264 pr pxn pl r um dm ds es esa ya) (do (e, tc', um', ds', es') <- select (f r 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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (do (e, tc', um', ds', es') <- select (f r 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}, esa));
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)
 2. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>?R264 pr pxn pl r um dm ds es esa\<rbrace>
 3. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>?R'264 pr pxn pl r um dm ds es esa\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 6. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 7. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (10 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?P275 pr pxn pl r um dm ds es esa y) (?P'277 pr pxn pl r um dm ds es esa ya) (select (f r 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))) (select (f r 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}, esa)))
 2. \<And>pr pxn pl r um dm ds es esa y ya rv rv'. \<lbrakk>es = esa; dc y ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R274 pr pxn pl r um dm ds es esa y ya rv) (?R'274 pr pxn pl r um dm ds es esa y ya rv') (case rv of (e, tc', um', ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (case rv' of (e, tc', um', ds', es') \<Rightarrow> do 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)
 3. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>?R274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>?R'274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 5. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. ?P275 pr pxn pl r um dm ds es esa y and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 6. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. ?P'277 pr pxn pl r um dm ds es esa ya and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 9. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 10. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (10 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (\<lambda>_. True) (\<lambda>_. True) (select (f r 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))) (select (f r 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}, esa)))
 2. \<And>pr pxn pl r um dm ds es esa y ya rv rv'. \<lbrakk>es = esa; dc y ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R274 pr pxn pl r um dm ds es esa y ya rv) (?R'274 pr pxn pl r um dm ds es esa y ya rv') (case rv of (e, tc', um', ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (case rv' of (e, tc', um', ds', es') \<Rightarrow> do 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)
 3. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>?R274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>?R'274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 5. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 6. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 9. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 10. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (9 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa y ya rv rv'. \<lbrakk>es = esa; dc y ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R274 pr pxn pl r um dm ds es esa y ya rv) (?R'274 pr pxn pl r um dm ds es esa y ya rv') (case rv of (e, tc', um', ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) (case rv' of (e, tc', um', ds', es') \<Rightarrow> do 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)
 2. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>?R274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 3. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>?R'274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 5. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 8. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 9. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (9 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. corres_underlying state_relation nf False (=) (?R274 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)) (?R'274 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)) (do y <- do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor (ak, bc));
return (ag, ah)
od) (do y <- doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor (ak, bc));
return (ag, ah)
od)
 2. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>?R274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 3. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>?R'274 pr pxn pl r um dm ds es esa y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 5. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 8. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
 9. \<And>pr pxn pl r um dm ds s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'254 pr pxn pl r um dm ds) s proof (prove)
goal (12 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. corres_underlying Id nf False (=) (?P336 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)) (?Q334 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)) (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)))
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> corres_underlying state_relation nf False (=) (?R307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y) (?R'307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya) (do y <- do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor (ak, bc));
return (ag, ah)
od) (do y <- doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor (ak, bc));
return (ag, ah)
od)
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>?R307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>?R'307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc\<rbrace>
 5. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. ?P336 pr pxn pl r um dm ds es esa y ya a \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 6. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 7. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 8. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> corres_underlying state_relation nf False (=) (?R307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y) (?R'307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya) (do y <- do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor (ak, bc));
return (ag, ah)
od) (do y <- doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor (ak, bc));
return (ag, ah)
od)
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>?R307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>?R'307 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc\<rbrace>
 4. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 5. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 6. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 7. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<lbrace>?Q'254 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>esa. (\<lambda>_. True) and ?Q'268 pr pxn pl r um dm ds esa\<rbrace>
 10. \<And>pr pxn pl r um dm ds s. (einvs and ct_running and (\<lambda>s. pr = ptable_rights_s s) and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x)) and (\<lambda>s. pl = ptable_lift_s s |` {x. pr x \<noteq> {}}) and (\<lambda>a. True) and (\<lambda>s. r = cur_thread s) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))) and (\<lambda>s. um = user_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom (dm \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))) and (\<lambda>s. dm = device_mem s \<circ> ptrFromPAddr) and (\<lambda>s. dom ds = dom (device_state (machine_state s))) and (\<lambda>s. ds = (device_state \<circ> machine_state) s)) s \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q254 pr pxn pl r um dm ds) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> corres_underlying Id nf False (=) (?P345 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y) (?Q347 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya) (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds))
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv) (?R'343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv') (do y <- do_machine_op (setExMonitor (ak, bc));
return (ag, ah)
od) (do y <- doMachineOp (setExMonitor (ak, bc));
return (ag, ah)
od)
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace> do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>?R343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace> doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>?R'343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>y. ?P345 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y \<circ> machine_state and ?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>ya. ?Q347 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya \<circ> ksMachineState and ?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace>
 7. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 8. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 9. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 10. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv) (?R'343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv') (do y <- do_machine_op (setExMonitor (ak, bc));
return (ag, ah)
od) (do y <- doMachineOp (setExMonitor (ak, bc));
return (ag, ah)
od)
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace> do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>?R343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace> doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>?R'343 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>ya. ?Q347 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya \<circ> ksMachineState and ?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace>
 6. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 7. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 8. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 9. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<lbrace>?Q254 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>es. (\<lambda>_. True) and ?Q266 pr pxn pl r um dm ds es\<rbrace>
A total of 13 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying Id nf False (=) (?P357 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv) (?Q359 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv') (setExMonitor (ak, bc)) (setExMonitor (ak, bc))
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv' rva rv'a. \<lbrakk>y = ya; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv' rva) (?R'355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv' rv'a) (return (ag, ah)) (return (ag, ah))
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q358 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv\<rbrace> do_machine_op (setExMonitor (ak, bc)) \<lbrace>?R355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'360 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv'\<rbrace> doMachineOp (setExMonitor (ak, bc)) \<lbrace>?R'355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace> do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>rv. ?P357 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv \<circ> machine_state and ?Q358 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace> doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>rv'. ?Q359 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv' \<circ> ksMachineState and ?Q'360 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv'\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace>
 8. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>ya. ?Q347 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya \<circ> ksMachineState and ?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace>
 9. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 10. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv' rva rv'a. \<lbrakk>y = ya; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres_underlying state_relation nf False (=) (?R355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv' rva) (?R'355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv' rv'a) (return (ag, ah)) (return (ag, ah))
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q358 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv\<rbrace> do_machine_op (setExMonitor (ak, bc)) \<lbrace>?R355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'360 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv'\<rbrace> doMachineOp (setExMonitor (ak, bc)) \<lbrace>?R'355 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace> do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>rv. (\<lambda>_. True) \<circ> machine_state and ?Q358 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace> doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>rv'. ?Q359 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv' \<circ> ksMachineState and ?Q'360 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv'\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>ya. ?Q347 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya \<circ> ksMachineState and ?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace>
 8. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 9. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 10. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q358 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv\<rbrace> do_machine_op (setExMonitor (ak, bc)) \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv rv'. \<lbrakk>y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'360 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv'\<rbrace> doMachineOp (setExMonitor (ak, bc)) \<lbrace>\<lambda>rv'a _. True\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace> do_machine_op (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>rv. (\<lambda>_. True) \<circ> machine_state and ?Q358 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya. y = ya \<Longrightarrow> \<lbrace>?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace> doMachineOp (device_memory_update ((aj |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>rv'. ?Q359 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv' \<circ> ksMachineState and ?Q'360 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y ya rv'\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q335 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> do_machine_op (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q346 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc y\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba ag ah ai aj ak bc. \<lbrace>?Q'333 pr pxn pl r um dm ds (aa, ba) (aa, ba) () () (ag, ah, ai, aj, ak, bc)\<rbrace> doMachineOp (user_memory_update ((ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>ya. ?Q347 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya \<circ> ksMachineState and ?Q'348 pr pxn pl r um dm ds aa ba ag ah ai aj ak bc ya\<rbrace>
 7. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 pr pxn pl r um dm ds es esa y\<rbrace> select (f r 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)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q335 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 8. \<And>pr pxn pl r um dm ds es esa y ya. \<lbrakk>es = esa; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace> select (f r 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}, esa)) \<lbrace>\<lambda>a. ?Q334 pr pxn pl r um dm ds es esa y ya a \<circ> ksMachineState and ?Q'333 pr pxn pl r um dm ds es esa y ya a\<rbrace>
 9. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q266 pr pxn pl r um dm ds es\<rbrace> assert (f r 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> {}) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q276 pr pxn pl r um dm ds es esa y\<rbrace>
 10. \<And>pr pxn pl r um dm ds es esa. es = esa \<Longrightarrow> \<lbrace>?Q'268 pr pxn pl r um dm ds esa\<rbrace> assert (f r 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}, esa) \<noteq> {}) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'278 pr pxn pl r um dm ds es esa ya\<rbrace>
A total of 14 subgoals...