theory ArchADT_IF_Refine_C

lemma do_user_op_if_C_corres[ADT_IF_Refine_assms]:
   "corres_underlying rf_sr False False (=)
   (invs' and ex_abs einvs and (\<lambda>_. uop_nonempty f)) \<top>
   (doUserOp_if f tc) (doUserOp_C_if f tc)" apply (rule corres_gen_asm) apply (simp add: doUserOp_if_def doUserOp_C_if_def uop_nonempty_def del: split_paired_All) apply (rule corres_gets_same) apply (clarsimp simp: absKState_crelation ptable_rights_s'_def ptable_rights_s''_def
           rf_sr_def  cstate_relation_def Let_def cstate_to_H_correct) apply simp apply (rule corres_gets_same) apply (clarsimp simp: ptable_xn_s'_def ptable_xn_s''_def ptable_attrs_s_def
                          absKState_crelation ptable_attrs_s'_def ptable_attrs_s''_def  rf_sr_def) apply simp apply (rule corres_gets_same) apply (clarsimp simp: absKState_crelation curthread_relation ptable_lift_s'_def ptable_lift_s''_def
                         ptable_lift_s_def rf_sr_def) apply simp apply (simp add: getCurThread_def) apply (rule corres_gets_same) apply (simp add: absKState_crelation rf_sr_def) apply simp apply (rule corres_gets_same) apply (rule fun_cong[where x=ptrFromPAddr]) apply (rule_tac f=comp in arg_cong) apply (rule user_mem_C_relation[symmetric]) apply (simp add: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) apply fastforce apply simp apply (rule corres_gets_same) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                          cpspace_relation_def) apply (drule device_mem_C_relation[symmetric]) apply fastforce apply (simp add: comp_def) apply simp apply (rule corres_gets_same) apply (clarsimp simp: cstate_relation_def rf_sr_def
                          Let_def cmachine_state_relation_def) apply simp apply (rule corres_guard_imp) apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split) apply (clarsimp simp add: corres_underlying_def fail_def
                                 assert_def return_def
                          split: if_splits) apply simp apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split) apply (clarsimp simp add: corres_underlying_def fail_def
                                   assert_def return_def
                            split: if_splits) apply simp apply (rule corres_split[OF corres_dmo_getExMonitor_C]) apply clarsimp apply (rule_tac r'="(=)" in corres_split[OF corres_select]) apply clarsimp apply simp apply (rule corres_underlying_split5) apply (rule corres_split[OF user_memory_update_corres_C]) apply (rule corres_split[OF device_update_corres_C]) apply (rule corres_split[OF corres_dmo_setExMonitor_C,
                              where R="\<top>\<top>" and R'="\<top>\<top>"]) apply (wp | simp)+ apply (clarsimp simp:  ex_abs_def restrict_map_def invs_pspace_aligned'
                          invs_pspace_distinct' ptable_lift_s'_def ptable_rights_s'_def
                  split: if_splits) apply (drule ptable_rights_imp_UserData[rotated -1]) apply ((fastforce | intro conjI)+)[4] apply (clarsimp simp: user_mem'_def device_mem'_def dom_def split: if_splits) apply fastforce apply (clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def ex_abs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and (\<lambda>_. uop_nonempty f)) (\<lambda>_. True) (doUserOp_if f tc) (doUserOp_C_if f tc) proof (prove)
goal (1 subgoal):
 1. uop_nonempty f \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) (\<lambda>_. True) (doUserOp_if f tc) (doUserOp_C_if f tc) proof (prove)
goal (1 subgoal):
 1. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) (\<lambda>_. True) (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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ptable_rights_s' s = ptable_rights_s'' s'
 2. \<And>s. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs) s\<rbrakk> \<Longrightarrow> ?R2 (ptable_rights_s' s) s
 3. \<And>pr. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and ?R2 pr and (\<lambda>s. pr = ptable_rights_s' s)) (\<lambda>_. True) (do pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs) s\<rbrakk> \<Longrightarrow> ?R2 (ptable_rights_s' s) s
 2. \<And>pr. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and ?R2 pr and (\<lambda>s. pr = ptable_rights_s' s)) (\<lambda>_. True) (do pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s' s)) (\<lambda>_. True) (do pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (3 subgoals):
 1. \<And>pr s s'. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s' s)) s; True; (s, s') \<in> rf_sr\<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 tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s' s)) s\<rbrakk> \<Longrightarrow> ?R35 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s' s x) s
 3. \<And>pr pxn. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s' s) and ?R35 pr pxn and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s' s x))) (\<lambda>_. True) (do pl <- gets (\<lambda>s. ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do pl <- gets (\<lambda>s. ptable_lift_s'' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>pr s. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s' s)) s\<rbrakk> \<Longrightarrow> ?R35 pr (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s' s x) s
 2. \<And>pr pxn. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and (\<lambda>a. True) and (\<lambda>s. pr = ptable_rights_s' s) and ?R35 pr pxn and (\<lambda>s. pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s' s x))) (\<lambda>_. True) (do pl <- gets (\<lambda>s. ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do pl <- gets (\<lambda>s. ptable_lift_s'' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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))) (\<lambda>_. True) (do pl <- gets (\<lambda>s. ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do pl <- gets (\<lambda>s. ptable_lift_s'' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>);
t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn s s'. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs 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; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub> = ptable_lift_s'' s'|\<^bsub>{x. pr x \<noteq> {}}\<^esub>
 2. \<And>pr pxn s. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs 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> ?R39 pr pxn (ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) s
 3. \<And>pr pxn pl. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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 ?R39 pr pxn pl and (\<lambda>s. pl = ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn s. \<lbrakk>\<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {}; (invs' and ex_abs einvs 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> ?R39 pr pxn (ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) s
 2. \<And>pr pxn pl. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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 ?R39 pr pxn pl and (\<lambda>s. pl = ptable_lift_s' s|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl. \<forall>t pl pr pxn tc um es. f t pl pr pxn (tc, um, es) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do t <- gets (\<lambda>s. cur_thread (cstate_to_A s));
um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (3 subgoals):
 1. \<And>pr pxn pl s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ksCurThread s = cur_thread (cstate_to_A s')
 2. \<And>pr pxn pl s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) s\<rbrakk> \<Longrightarrow> ?R43 pr pxn pl (ksCurThread s) s
 3. \<And>pr pxn pl r. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and ?R43 pr pxn pl r and (\<lambda>s. r = ksCurThread s)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>)) s\<rbrakk> \<Longrightarrow> ?R43 pr pxn pl (ksCurThread s) s
 2. \<And>pr pxn pl r. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and ?R43 pr pxn pl r and (\<lambda>s. r = ksCurThread s)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do um <- gets (\<lambda>s. user_mem_C (globals s) \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> user_mem' s \<circ> ptrFromPAddr = user_mem_C (globals s') \<circ> ptrFromPAddr
 2. \<And>pr pxn pl r s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s\<rbrakk> \<Longrightarrow> ?R47 pr pxn pl r (user_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and ?R47 pr pxn pl r um and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<circ>) (user_mem' s) = (\<circ>) (user_mem_C (globals s'))
 2. \<And>pr pxn pl r s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s\<rbrakk> \<Longrightarrow> ?R47 pr pxn pl r (user_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and ?R47 pr pxn pl r um and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> user_mem' s = user_mem_C (globals s')
 2. \<And>pr pxn pl r s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s\<rbrakk> \<Longrightarrow> ?R47 pr pxn pl r (user_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and ?R47 pr pxn pl r um and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (4 subgoals):
 1. \<And>pr pxn pl r s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation
 2. \<And>pr pxn pl r s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> pspace_distinct' s
 3. \<And>pr pxn pl r s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s\<rbrakk> \<Longrightarrow> ?R47 pr pxn pl r (user_mem' s \<circ> ptrFromPAddr) s
 4. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and ?R47 pr pxn pl r um and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. \<And>pr pxn pl r s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s\<rbrakk> \<Longrightarrow> ?R47 pr pxn pl r (user_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and ?R47 pr pxn pl r um and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>pr pxn pl r s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s)) s\<rbrakk> \<Longrightarrow> ?R47 pr pxn pl r (user_mem' s \<circ> ptrFromPAddr) s
 2. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and ?R47 pr pxn pl r um and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do dm <- gets (\<lambda>s. device_mem_C (globals s) \<circ> ptrFromPAddr);
ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> device_mem' s \<circ> ptrFromPAddr = device_mem_C (globals s') \<circ> ptrFromPAddr
 2. \<And>pr pxn pl r um s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R75 pr pxn pl r um (device_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and ?R75 pr pxn pl r um dm and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; ex_abs einvs s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> device_mem' s \<circ> ptrFromPAddr = device_mem_C (globals s') \<circ> ptrFromPAddr
 2. \<And>pr pxn pl r um s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R75 pr pxn pl r um (device_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and ?R75 pr pxn pl r um dm and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; ex_abs einvs s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. \<And>s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; ex_abs einvs s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; device_mem' s = device_mem_C (globals s')\<rbrakk> \<Longrightarrow> device_mem' s \<circ> ptrFromPAddr = device_mem_C (globals s') \<circ> ptrFromPAddr
 3. \<And>pr pxn pl r um s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R75 pr pxn pl r um (device_mem' s \<circ> ptrFromPAddr) s
 4. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and ?R75 pr pxn pl r um dm and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; ex_abs einvs s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; device_mem' s = device_mem_C (globals s')\<rbrakk> \<Longrightarrow> device_mem' s \<circ> ptrFromPAddr = device_mem_C (globals s') \<circ> ptrFromPAddr
 2. \<And>pr pxn pl r um s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R75 pr pxn pl r um (device_mem' s \<circ> ptrFromPAddr) s
 3. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and ?R75 pr pxn pl r um dm and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R75 pr pxn pl r um (device_mem' s \<circ> ptrFromPAddr) s
 2. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and ?R75 pr pxn pl r um dm and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um dm. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) (\<lambda>_. True) (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;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do ds <- gets (\<lambda>s. device_state (phantom_machine_state_' (globals s)));
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) s; True; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (device_state \<circ> ksMachineState) s = device_state (phantom_machine_state_' (globals s'))
 2. \<And>pr pxn pl r um dm s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R124 pr pxn pl r um dm ((device_state \<circ> ksMachineState) s) s
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and ?R124 pr pxn pl r um dm ds and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) (\<lambda>_. True) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr)) s\<rbrakk> \<Longrightarrow> ?R124 pr pxn pl r um dm ((device_state \<circ> ksMachineState) s) s
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and ?R124 pr pxn pl r um dm ds and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) (\<lambda>_. True) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) (\<lambda>_. True) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (?Q128 pr pxn pl r um dm ds) (?Q'128 pr pxn pl r um dm ds) (do y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ?Q128 pr pxn pl r um dm ds s
 3. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ?Q'128 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds)) (assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds))
 2. \<And>pr pxn pl r um dm ds rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R132 pr pxn pl r um dm ds rv) (?R'132 pr pxn pl r um dm ds rv') (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?R132 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?R'132 pr pxn pl r um dm ds\<rbrace>
 5. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 6. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (5 subgoals):
 1. \<And>pr pxn pl r um dm ds rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R132 pr pxn pl r um dm ds rv) (?R'132 pr pxn pl r um dm ds rv') (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?R132 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?R'132 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 5. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (5 subgoals):
 1. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (?R132 pr pxn pl r um dm ds ()) (?R'132 pr pxn pl r um dm ds ()) (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?R132 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?R'132 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 5. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (8 subgoals):
 1. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds)) (assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds))
 2. \<And>pr pxn pl r um dm ds rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R140 pr pxn pl r um dm ds rv) (?R'140 pr pxn pl r um dm ds rv') (do es <- doMachineOp getExMonitor;
a <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
case a 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'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od
od) (do es <- doMachineOp_C getExMonitor;
a <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od
od)
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?R140 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?R'140 pr pxn pl r um dm ds\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 8. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (7 subgoals):
 1. \<And>pr pxn pl r um dm ds rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R140 pr pxn pl r um dm ds rv) (?R'140 pr pxn pl r um dm ds rv') (do es <- doMachineOp getExMonitor;
a <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
case a 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'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od
od) (do es <- doMachineOp_C getExMonitor;
a <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (ds \<circ> ptrFromPAddr)|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- setUserMem_C ((um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub> \<circ> addrFromPPtr)|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od
od)
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?R140 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?R'140 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 7. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (7 subgoals):
 1. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (?R140 pr pxn pl r um dm ds ()) (?R'140 pr pxn pl r um dm ds ()) (do es <- doMachineOp getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- doMachineOp (user_memory_update ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do es <- doMachineOp_C getExMonitor;
(e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
y <- setUserMem_C ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?R140 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?R'140 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 7. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (9 subgoals):
 1. \<And>pr pxn pl r um dm ds es esa. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; es = esa\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R192 pr pxn pl r um dm ds es) (?R'192 pr pxn pl r um dm ds esa) (do a <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, es));
case a 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 ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od
od) (do a <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, esa));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- setUserMem_C ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od
od)
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>?R192 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>?R'192 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 9. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (9 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> corres_underlying rf_sr False False (=) (?R192 pr pxn pl r um dm ds (aa, ba)) (?R'192 pr pxn pl r um dm ds (aa, ba)) (do (e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba));
y <- doMachineOp (user_memory_update ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) (do (e, tc', um', ds', es') <- select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba));
y <- setUserMem_C ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>?R192 pr pxn pl r um dm ds\<rbrace>
 3. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>?R'192 pr pxn pl r um dm ds\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
 9. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'132 pr pxn pl r um dm ds) s proof (prove)
goal (12 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<forall>s'\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba). \<exists>s\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba). s = s'
 2. \<And>pr pxn pl r um dm ds aa ba rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R243 pr pxn pl r um dm ds aa ba rv) (?R'243 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 <- doMachineOp (user_memory_update ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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 <- setUserMem_C ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 3. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>?R243 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>?R'243 pr pxn pl r um dm ds aa ba\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'287 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R243 pr pxn pl r um dm ds aa ba rv) (?R'243 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 <- doMachineOp (user_memory_update ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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 <- setUserMem_C ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>?R243 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>?R'243 pr pxn pl r um dm ds aa ba\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'287 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba rv rv'. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R243 pr pxn pl r um dm ds aa ba rv') (?R'243 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 <- doMachineOp (user_memory_update ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (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 <- setUserMem_C ((\<lambda>a. (um'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (ds'|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor es');
return (e, tc')
od)
 2. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>?R243 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>?R'243 pr pxn pl r um dm ds aa ba\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'287 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?Q290 pr pxn pl r um dm ds aa ba rv' a b c d e) (?Q'292 pr pxn pl r um dm ds aa ba rv' a b c d e) (do y <- doMachineOp (user_memory_update ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>));
y <- doMachineOp (device_memory_update ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor e);
return (a, b)
od) (do y <- setUserMem_C ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>);
y <- setDeviceState_C ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor e);
return (a, b)
od)
 2. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> ?Q290 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> ?Q'292 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 4. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
 5. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'287 pr pxn pl r um dm ds a\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'186 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 tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; (invs' and ex_abs einvs 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|\<^bsub>{x. pr x \<noteq> {}}\<^esub>) and (\<lambda>a. True) and (\<lambda>s. r = ksCurThread s) and (\<lambda>a. True) and (\<lambda>s. um = user_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. dm = device_mem' s \<circ> ptrFromPAddr) and (\<lambda>a. True) and (\<lambda>s. ds = (device_state \<circ> ksMachineState) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q132 pr pxn pl r um dm ds) s
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R295 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva) (?R'295 pr pxn pl r um dm ds aa ba rv rv' a b c d e rv'a) (do y <- doMachineOp (device_memory_update ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>));
y <- doMachineOp (setExMonitor e);
return (a, b)
od) (do y <- setDeviceState_C ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>);
y <- doMachineOp_C (setExMonitor e);
return (a, b)
od)
 2. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q298 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>)) \<lbrace>?R295 pr pxn pl r um dm ds aa ba rv rv' a b c d e\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'299 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace> setUserMem_C ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>) \<lbrace>?R'295 pr pxn pl r um dm ds aa ba rv rv' a b c d e\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>) \<subseteq> dom (user_mem' s)) and ?Q298 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> (\<lambda>_. True) and ?Q'299 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 6. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
 7. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'287 pr pxn pl r um dm ds a\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'186 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'232 pr pxn pl r um dm ds a\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q132 pr pxn pl r um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q187 pr pxn pl r um dm ds a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb rv'b. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True; rvb = rv'b\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (?R303 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb) (?R'303 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rv'b) (do y <- doMachineOp (setExMonitor e);
return (a, b)
od) (do y <- doMachineOp_C (setExMonitor e);
return (a, b)
od)
 2. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q305 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>)) \<lbrace>?R303 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'306 pr pxn pl r um dm ds aa ba rv rv' a b c d e rv'a\<rbrace> setDeviceState_C ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>) \<lbrace>?R'303 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q298 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>)) \<lbrace>\<lambda>rva. (\<lambda>_. True) and ?Q305 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'299 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace> setUserMem_C ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>) \<lbrace>\<lambda>rv'a. (\<lambda>_. True) and ?Q'306 pr pxn pl r um dm ds aa ba rv rv' a b c d e rv'a\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>) \<subseteq> dom (user_mem' s)) and ?Q298 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> (\<lambda>_. True) and ?Q'299 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 8. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
 9. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'232 pr pxn pl r um dm ds ()\<rbrace> doMachineOp_C getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'287 pr pxn pl r um dm ds a\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q187 pr pxn pl r um dm ds ()\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q233 pr pxn pl r um dm ds a\<rbrace>
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb rv'b rvc rv'c. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True; rvb = rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (return (a, b)) (return (a, b))
 2. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb rv'b. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q312 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb\<rbrace> doMachineOp (setExMonitor e) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb rv'b. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'313 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rv'b\<rbrace> doMachineOp_C (setExMonitor e) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q305 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>)) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and ?Q312 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rvb\<rbrace>
 5. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'306 pr pxn pl r um dm ds aa ba rv rv' a b c d e rv'a\<rbrace> setDeviceState_C ((\<lambda>a. (d|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>dom ds\<^esub>) \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and ?Q'313 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva rv'a rv'b\<rbrace>
 6. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q298 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace> doMachineOp (user_memory_update ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>)) \<lbrace>\<lambda>rva. (\<lambda>_. True) and ?Q305 pr pxn pl r um dm ds aa ba rv rv' a b c d e rva\<rbrace>
 7. \<And>pr pxn pl r um dm ds aa ba rv rv' a b c d e. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'299 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace> setUserMem_C ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>) \<lbrace>\<lambda>rv'a. (\<lambda>_. True) and ?Q'306 pr pxn pl r um dm ds aa ba rv rv' a b c d e rv'a\<rbrace>
 8. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q288 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom ((\<lambda>a. (c|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}\<^esub>) (addrFromPPtr a))|\<^bsub>(- dom ds)\<^esub>) \<subseteq> dom (user_mem' s)) and ?Q298 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 9. \<And>pr pxn pl r um dm ds aa ba. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q'287 pr pxn pl r um dm ds (aa, ba)\<rbrace> select (f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, aa, ba)) \<lbrace>\<lambda>rv'. case rv' of (a, b, c, d, e) \<Rightarrow> (\<lambda>_. True) and ?Q'299 pr pxn pl r um dm ds aa ba rv' a b c d e\<rbrace>
 10. \<And>pr pxn pl r um dm ds. \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {} \<Longrightarrow> \<lbrace>?Q233 pr pxn pl r um dm ds ()\<rbrace> doMachineOp getExMonitor \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q288 pr pxn pl r um dm ds a\<rbrace>
A total of 17 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s \<and> ex_abs einvs s\<rbrakk> \<Longrightarrow> dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)) \<longrightarrow> dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)) \<longrightarrow> (\<forall>x\<in>f (ksCurThread s) (ptable_lift_s' s|\<^bsub>{x. ptable_rights_s' s x \<noteq> {}}\<^esub>) (ptable_rights_s' s) (\<lambda>a. ptable_rights_s' s a \<noteq> {} \<and> ptable_xn_s' s a) (tc, (\<lambda>a. user_mem' s (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. (ptable_lift_s' s|\<^bsub>{x. ptable_rights_s' s x \<noteq> {}}\<^esub>) x = Some y \<and> AllowRead \<in> ptable_rights_s' s x}\<^esub>, (\<lambda>a. device_state (ksMachineState s) (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. (ptable_lift_s' s|\<^bsub>{x. ptable_rights_s' s x \<noteq> {}}\<^esub>) x = Some y \<and> AllowRead \<in> ptable_rights_s' s x}\<^esub>, exclusive_state (ksMachineState s)). (case x of (a, b, c, aa) \<Rightarrow> \<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> dom (\<lambda>a. (c|\<^bsub>{y. \<exists>x. (ptable_lift_s' s|\<^bsub>{x. ptable_rights_s' s x \<noteq> {}}\<^esub>) x = Some y \<and> AllowWrite \<in> ptable_rights_s' s x}\<^esub>) (addrFromPPtr a)) \<inter> - dom (device_state (ksMachineState s)) \<subseteq> dom (user_mem' a)) s)
 2. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>aa. \<forall>x\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, exclusive_state (phantom_machine_state_' (globals a))). (case x of (a, aa) \<Rightarrow> case aa of (b, aa) \<Rightarrow> case aa of (c, aa) \<Rightarrow> case aa of (d, e) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) aa)) a)) a)) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; ptable_lift (ksCurThread s) (absKState s) xa = Some (addrFromPPtr x); AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa\<rbrakk> \<Longrightarrow> \<exists>y. device_state (ksMachineState s) x = Some y
 2. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>aa. \<forall>x\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, exclusive_state (phantom_machine_state_' (globals a))). (case x of (a, aa) \<Rightarrow> case aa of (b, aa) \<Rightarrow> case aa of (c, aa) \<Rightarrow> case aa of (d, e) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) aa)) a)) a)) s)) s proof (prove)
goal (6 subgoals):
 1. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa\<rbrakk> \<Longrightarrow> einvs (?s564 s sa a aa ab ac ad b x y xa)
 2. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa\<rbrakk> \<Longrightarrow> (?s564 s sa a aa ab ac ad b x y xa, s) \<in> state_relation
 4. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa\<rbrakk> \<Longrightarrow> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}
 5. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa; pointerInUserData x s \<or> pointerInDeviceData x s\<rbrakk> \<Longrightarrow> \<exists>y. device_state (ksMachineState s) x = Some y
 6. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>aa. \<forall>x\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, exclusive_state (phantom_machine_state_' (globals a))). (case x of (a, aa) \<Rightarrow> case aa of (b, aa) \<Rightarrow> case aa of (c, aa) \<Rightarrow> case aa of (d, e) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) aa)) a)) a)) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); user_mem' s x = None; \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom (device_mem' s) \<subseteq> dom (device_state (ksMachineState s)); ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa; pointerInUserData x s \<or> pointerInDeviceData x s\<rbrakk> \<Longrightarrow> \<exists>y. device_state (ksMachineState s) x = Some y
 2. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>aa. \<forall>x\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, exclusive_state (phantom_machine_state_' (globals a))). (case x of (a, aa) \<Rightarrow> case aa of (b, aa) \<Rightarrow> case aa of (c, aa) \<Rightarrow> case aa of (d, e) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) aa)) a)) a)) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s sa a aa ab ac ad b x y xa. \<lbrakk>{a. pointerInDeviceData a s} \<subseteq> {a. \<exists>y. device_state (ksMachineState s) a = Some y}; (a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (\<lambda>a. ptable_rights (ksCurThread s) (absKState s) a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} \<longrightarrow> ptable_lift (ksCurThread s) (absKState s) xa = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) xa) \<and> ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {} then device_state (ksMachineState s) (ptrFromPAddr x) else None, exclusive_state (ksMachineState s)); \<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; invs' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; ptable_rights (ksCurThread s) (absKState s) xa \<noteq> {}; ab (addrFromPPtr x) = Some y; AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) xa; pointerInDeviceData x s; \<not> pointerInUserData x s; {a. pointerInUserData a s} \<subseteq> - {a. \<exists>y. device_state (ksMachineState s) a = Some y}\<rbrakk> \<Longrightarrow> \<exists>y. device_state (ksMachineState s) x = Some y
 2. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>aa. \<forall>x\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, exclusive_state (phantom_machine_state_' (globals a))). (case x of (a, aa) \<Rightarrow> case aa of (b, aa) \<Rightarrow> case aa of (c, aa) \<Rightarrow> case aa of (d, e) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) aa)) a)) a)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>pr pxn pl r um dm ds s. \<lbrakk>\<forall>t pl pr pxn tc um a aa b. f t pl pr pxn (tc, um, a, aa, b) \<noteq> {}; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>aa. \<forall>x\<in>f r pl pr pxn (tc, um|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, (\<lambda>a. ds (ptrFromPAddr a))|\<^bsub>{y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}\<^esub>, exclusive_state (phantom_machine_state_' (globals a))). (case x of (a, aa) \<Rightarrow> case aa of (b, aa) \<Rightarrow> case aa of (c, aa) \<Rightarrow> case aa of (d, e) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) aa)) a)) a)) s)) s proof (prove)
goal:
No subgoals!