theory ArchADT_IF_Refine

lemma do_user_op_if_corres[ADT_IF_Refine_assms]:
  "corres (=) (einvs and ct_running and (\<lambda>_. \<forall>t pl pr pxn tcu. f t pl pr pxn tcu \<noteq> {}))
              (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running')
              (do_user_op_if f tc) (doUserOp_if f tc)" apply (rule corres_gen_asm) 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) apply fastforce 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 clarsimp 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) apply (clarsimp simp: user_memory_update_def) apply (rule no_fail_modify) apply (rule corres_split[OF corres_machine_op,where r'="(=)"]) apply (rule corres_underlying_trivial, wp) apply (rule corres_split[OF corres_machine_op, where r'="(=)"]) apply (rule corres_underlying_trivial, wp) apply (rule corres_return_same_trivial) by (wp hoare_TrueI[where P = \<top>] | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and ct_running and (\<lambda>_. \<forall>t pl pr pxn tcu. f t pl pr pxn tcu \<noteq> {})) (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. \<forall>t pl pr pxn tcu. f t pl pr pxn tcu \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running) s\<rbrakk> \<Longrightarrow> ?R2 (ptable_rights_s s) s
 3. \<And>pr. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and ?R2 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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running) s\<rbrakk> \<Longrightarrow> ?R2 (ptable_rights_s s) s
 3. \<And>pr. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and ?R2 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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running) s\<rbrakk> \<Longrightarrow> ?R2 (ptable_rights_s s) s
 3. \<And>pr. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and ?R2 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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running) s\<rbrakk> \<Longrightarrow> ?R2 (ptable_rights_s s) s
 2. \<And>pr. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and ?R2 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s\<rbrakk> \<Longrightarrow> ?R24 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 3. \<And>pr pxn. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R24 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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s\<rbrakk> \<Longrightarrow> ?R24 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 3. \<And>pr pxn. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R24 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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s\<rbrakk> \<Longrightarrow> ?R24 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 3. \<And>pr pxn. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R24 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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s)) s\<rbrakk> \<Longrightarrow> ?R24 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) s
 2. \<And>pr pxn. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (einvs and ct_running and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s s) and ?R24 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?R46 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 3. \<And>pr pxn pl. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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 ?R46 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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?R46 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 3. \<And>pr pxn pl. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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 ?R46 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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?R46 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 3. \<And>pr pxn pl. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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 ?R46 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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?R46 pr pxn (ptable_lift_s s |` {x. pr x \<noteq> {}}) s
 2. \<And>pr pxn pl. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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 ?R46 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?R64 pr pxn pl (cur_thread s) s
 3. \<And>pr pxn pl r. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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 ?R64 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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?R64 pr pxn pl (cur_thread s) s
 2. \<And>pr pxn pl r. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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 ?R64 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom (user_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))
 3. \<And>pr pxn pl r um. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom (user_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))
 2. \<And>pr pxn pl r um. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom (device_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))
 3. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom (device_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> dom (device_state (machine_state s))
 2. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>s x y. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; device_mem s x = Some y; 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; dom (user_mem s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) x = Some y
 2. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom ((device_state \<circ> machine_state) s) = dom (device_state (machine_state s))
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom ((device_state \<circ> machine_state) s) = dom (device_state (machine_state s))
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (?Q370 pr pxn pl r um dm ds) (?Q'370 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. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ?Q370 pr pxn pl r um dm ds s
 3. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ?Q'370 pr pxn pl r um dm ds s proof (prove)
goal (6 subgoals):
 1. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres_underlying Id False True (=) (?P375 pr pxn pl r um dm ds) (?Q375 pr pxn pl r um dm ds) getExMonitor getExMonitor
 2. \<And>pr pxn pl r um dm ds es esa. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; es = esa\<rbrakk> \<Longrightarrow> corres (=) (?R374 pr pxn pl r um dm ds es) (?R'374 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?R374 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>?R'374 pr pxn pl r um dm ds\<rbrace>
 5. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> (?P375 pr pxn pl r um dm ds \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 6. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> (?Q375 pr pxn pl r um dm ds \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (5 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; es = esa\<rbrakk> \<Longrightarrow> corres (=) (?R374 pr pxn pl r um dm ds es) (?R'374 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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?R374 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>?R'374 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 5. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (5 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (?R374 pr pxn pl r um dm ds (aa, ba)) (?R'374 pr pxn pl r um dm ds (aa, ba)) (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}, aa, ba));
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}, aa, ba));
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. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?R374 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>?R'374 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 5. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (8 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (?P436 pr pxn pl r um dm ds (aa, ba)) (?P'434 pr pxn pl r um dm ds (aa, ba)) (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}, aa, ba))) (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}, aa, ba)))
 2. \<And>pr pxn pl r um dm ds aa ba rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R390 pr pxn pl r um dm ds aa ba rv) (?R'390 pr pxn pl r um dm ds aa ba rv') (case rv of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (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, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (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 aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R390 pr pxn pl r um dm ds aa ba\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R'390 pr pxn pl r um dm ds aa ba\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. ?P436 pr pxn pl r um dm ds a and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. ?P'434 pr pxn pl r um dm ds a and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 8. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (8 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (\<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}, aa, ba))) (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}, aa, ba)))
 2. \<And>pr pxn pl r um dm ds aa ba rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R390 pr pxn pl r um dm ds aa ba rv) (?R'390 pr pxn pl r um dm ds aa ba rv') (case rv of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (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, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (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 aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R390 pr pxn pl r um dm ds aa ba\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R'390 pr pxn pl r um dm ds aa ba\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 8. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (7 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R390 pr pxn pl r um dm ds aa ba rv) (?R'390 pr pxn pl r um dm ds aa ba rv') (case rv of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (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, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (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 aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R390 pr pxn pl r um dm ds aa ba\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R'390 pr pxn pl r um dm ds aa ba\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 7. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (7 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres (=) (?R390 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)) (?R'390 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)) (do y <- do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 2. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R390 pr pxn pl r um dm ds aa ba\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>?R'390 pr pxn pl r um dm ds aa ba\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 7. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (10 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> corres_underlying Id False True (=) (?P490 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)) (?Q488 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)) (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds)))
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> corres (=) (?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y) (?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya) (do y <- do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. ?P490 pr pxn pl r um dm ds aa ba a \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. ?Q488 pr pxn pl r um dm ds aa ba a \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 10. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (10 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> no_fail (?Q488 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)) (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds)))
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> corres (=) (?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y) (?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya) (do y <- do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. ?Q488 pr pxn pl r um dm ds aa ba a \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 10. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (10 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> no_fail (?Q488 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)) (modify (\<lambda>ms. ms\<lparr>underlying_memory := \<lambda>a. case ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds)) a of None \<Rightarrow> underlying_memory ms a | Some x \<Rightarrow> x\<rparr>))
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> corres (=) (?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y) (?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya) (do y <- do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. ?Q488 pr pxn pl r um dm ds aa ba a \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 10. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (9 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> corres (=) (?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y) (?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya) (do y <- do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds));
y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>?R'461 pr pxn pl r um dm ds aa ba af ag ah ai aj bb\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 pr pxn pl r um dm ds) s
 9. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'374 pr pxn pl r um dm ds) s proof (prove)
goal (12 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> corres_underlying Id False True (=) (?P506 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y) (?Q508 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya) (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds))
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv) (?R'504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv') (do y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>?R504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>?R'504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>y. ?P506 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y \<circ> machine_state and ?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>ya. ?Q508 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya \<circ> ksMachineState and ?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 8. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv) (?R'504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv') (do y <- do_machine_op (setExMonitor (aj, bb));
return (af, ag)
od) (do y <- doMachineOp (setExMonitor (aj, bb));
return (af, ag)
od)
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>?R504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>?R'504 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>ya. (\<lambda>_. True) \<circ> ksMachineState and ?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
 10. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; (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\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q374 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 af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying Id False True (=) (?P521 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv) (?Q523 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv') (setExMonitor (aj, bb)) (setExMonitor (aj, bb))
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv' rva rv'a. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres (=) (?R519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv' rva) (?R'519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv' rv'a) (return (af, ag)) (return (af, ag))
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q522 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv\<rbrace> do_machine_op (setExMonitor (aj, bb)) \<lbrace>?R519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'524 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv'\<rbrace> doMachineOp (setExMonitor (aj, bb)) \<lbrace>?R'519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>\<lambda>rv. ?P521 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv \<circ> machine_state and ?Q522 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>\<lambda>rv'. ?Q523 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv' \<circ> ksMachineState and ?Q'524 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv'\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace>
 8. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>ya. (\<lambda>_. True) \<circ> ksMachineState and ?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace>
 9. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 10. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv' rva rv'a. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres (=) (?R519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv' rva) (?R'519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv' rv'a) (return (af, ag)) (return (af, ag))
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q522 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv\<rbrace> do_machine_op (setExMonitor (aj, bb)) \<lbrace>?R519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'524 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv'\<rbrace> doMachineOp (setExMonitor (aj, bb)) \<lbrace>?R'519 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>\<lambda>rv. (\<lambda>_. True) \<circ> machine_state and ?Q522 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) \<circ> ksMachineState and ?Q'524 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv'\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>ya. (\<lambda>_. True) \<circ> ksMachineState and ?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace>
 8. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 9. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q522 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv\<rbrace> do_machine_op (setExMonitor (aj, bb)) \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv rv'. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'524 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv'\<rbrace> doMachineOp (setExMonitor (aj, bb)) \<lbrace>\<lambda>rv'a _. True\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>\<lambda>rv. (\<lambda>_. True) \<circ> machine_state and ?Q522 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya. \<lbrakk>\<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {}; y = ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (ai |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` dom ds)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) \<circ> ksMachineState and ?Q'524 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y ya rv'\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q489 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> do_machine_op (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>y. (\<lambda>_. True) \<circ> machine_state and ?Q507 pr pxn pl r um dm ds aa ba af ag ah ai aj bb y\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba af ag ah ai aj bb. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'487 pr pxn pl r um dm ds aa ba (af, ag, ah, ai, aj, bb)\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (ah |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}) (addrFromPPtr a)) |` (- dom ds))) \<lbrace>\<lambda>ya. (\<lambda>_. True) \<circ> ksMachineState and ?Q'509 pr pxn pl r um dm ds aa ba af ag ah ai aj bb ya\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q435 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q489 pr pxn pl r um dm ds aa ba a\<rbrace>
 8. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'433 pr pxn pl r um dm ds (aa, ba)\<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}, aa, ba)) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> ksMachineState and ?Q'487 pr pxn pl r um dm ds aa ba a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q374 pr pxn pl r um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q435 pr pxn pl r um dm ds a\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn a aa ab ac b. f t pl pr pxn (a, aa, ab, ac, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'374 pr pxn pl r um dm ds\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'433 pr pxn pl r um dm ds a\<rbrace>
A total of 12 subgoals...