theory Refine

lemma do_user_op_corres:
  "corres (=) (einvs and ct_running)
                 (invs' and (%s. ksSchedulerAction s = ResumeCurrentThread) and
                  ct_running')
          (do_user_op f tc) (doUserOp f tc)" apply (simp add: do_user_op_def doUserOp_def split_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply (rule_tac r'="(=)" and P=einvs and P'=invs' in corres_split) apply (fastforce dest: absKState_correct [rotated]) apply (rule_tac r'="(=)" and P=einvs and P'=invs' in corres_split) apply (fastforce dest: absKState_correct [rotated]) apply (rule_tac r'="(=)" and P=invs and P'=invs' in corres_split) apply (rule user_mem_corres) apply (rule_tac r'="(=)" and P=invs and P'=invs' in corres_split) apply (rule device_mem_corres) apply (rule_tac r'="(=)" in corres_split) apply (rule corres_gets_machine_state) apply (rule_tac F = "dom (rvb \<circ> addrFromPPtr)  \<subseteq> - dom rvd" in corres_gen_asm) apply (rule_tac F = "dom (rvc \<circ> addrFromPPtr)  \<subseteq> dom rvd" in corres_gen_asm) apply simp apply (rule_tac r'="(=)" in corres_split[OF corres_select]) apply simp apply (rule corres_underlying_split[OF corres_machine_op]) apply simp apply (rule corres_underlying_trivial) apply (simp add: user_memory_update_def) apply (wp | simp)+ apply (rule corres_underlying_split[OF corres_machine_op,where Q = dc and Q'=dc]) apply (rule corres_underlying_trivial) apply (wp | simp add: dc_def device_memory_update_def)+ apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and ct_running) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do_user_op f tc) (doUserOp f tc) proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and ct_running) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') (do t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do t <- getCurThread;
trans <- gets (ptable_lift t \<circ> absKState);
perms <- gets (ptable_rights t \<circ> absKState);
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);
p <- select (fst (f t (trans |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do t <- getCurThread;
trans <- gets (ptable_lift t \<circ> absKState);
perms <- gets (ptable_rights t \<circ> absKState);
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);
p <- select (fst (f t (trans |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 2. \<And>s. (einvs and ct_running) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> corres (=) (?R4 t) (?R'4 ta) (do conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do trans <- gets (ptable_lift ta \<circ> absKState);
perms <- gets (ptable_rights ta \<circ> absKState);
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);
p <- select (fst (f ta (trans |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and ct_running) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> corres (=) einvs invs' (gets (ptable_lift t)) (gets (ptable_lift ta \<circ> absKState))
 2. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta rv) (?R'8 t ta rv') (do rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do perms <- gets (ptable_rights ta \<circ> absKState);
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);
p <- select (fst (f ta (rv' |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. invs' and ?Q'11 ta\<rbrace>
 7. \<And>s. (einvs and ct_running) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta rv) (?R'8 t ta rv') (do rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do perms <- gets (ptable_rights ta \<circ> absKState);
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);
p <- select (fst (f ta (rv' |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 2. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>?R8 t ta\<rbrace>
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>?R'8 t ta\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. invs' and ?Q'11 ta\<rbrace>
 6. \<And>s. (einvs and ct_running) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> corres (=) einvs invs' (gets (ptable_rights t)) (gets (ptable_rights ta \<circ> absKState))
 2. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres (=) (?R26 t ta rv rv' rva) (?R'26 t ta rv rv' rv'a) (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, um |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, um |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 3. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>?R26 t ta rv rv'\<rbrace>
 4. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>?R'26 t ta rv rv'\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>\<lambda>rv'. invs' and ?Q'29 t ta rv'\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. invs' and ?Q'11 ta\<rbrace>
 9. \<And>s. (einvs and ct_running) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres (=) (?R26 t ta rv rv' rva) (?R'26 t ta rv rv' rv'a) (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, um |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, um |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>?R26 t ta rv rv'\<rbrace>
 3. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>?R'26 t ta rv rv'\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>\<lambda>rv'. invs' and ?Q'29 t ta rv'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. invs' and ?Q'11 ta\<rbrace>
 8. \<And>s. (einvs and ct_running) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (12 subgoals):
 1. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres (=) invs invs' (gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr)) (gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> corres (=) (?R51 t ta rv rv' rva rv'a rvb) (?R'51 t ta rv rv' rva rv'a rv'b) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 3. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?R51 t ta rv rv' rva rv'a\<rbrace>
 4. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>?R'51 t ta rv rv' rva rv'a\<rbrace>
 5. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 6. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 7. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
 8. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>\<lambda>rv'. invs' and ?Q'29 t ta rv'\<rbrace>
 9. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. invs' and ?Q'11 ta\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> corres (=) (?R51 t ta rv rv' rva rv'a rvb) (?R'51 t ta rv rv' rva rv'a rv'b) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?R51 t ta rv rv' rva rv'a\<rbrace>
 3. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>?R'51 t ta rv rv' rva rv'a\<rbrace>
 4. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 5. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
 7. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>\<lambda>rv'. invs' and ?Q'29 t ta rv'\<rbrace>
 8. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. invs' and ?Q'11 ta\<rbrace>
 10. \<And>s. (einvs and ct_running) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> corres (=) invs invs' (gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr)) (gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> corres (=) (?R57 t ta rv rv' rva rv'a rvb rv'b rvc) (?R'57 t ta rv rv' rva rv'a rvb rv'b rv'c) (do ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?R57 t ta rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>?R'57 t ta rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 6. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 8. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 9. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
 10. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>\<lambda>rv'. invs' and ?Q'29 t ta rv'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> corres (=) (?R57 t ta rv rv' rva rv'a rvb rv'b rvc) (?R'57 t ta rv rv' rva rv'a rvb rv'b rv'c) (do ds <- gets (device_state \<circ> machine_state);
p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od) (do ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?R57 t ta rv rv' rva rv'a rvb rv'b\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>?R'57 t ta rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 5. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 6. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 7. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 8. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
 9. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'11 ta\<rbrace> gets (ptable_lift ta \<circ> absKState) \<lbrace>\<lambda>rv'. invs' and ?Q'29 t ta rv'\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. einvs and ?Q10 t\<rbrace>
A total of 13 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> corres (=) (?P65 t ta rv rv' rva rv'a rvb rv'b rvc) (?P'67 t ta rv rv' rva rv'a rvb rv'b rv'c) (gets (device_state \<circ> machine_state)) (gets (device_state \<circ> ksMachineState))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd\<rbrakk> \<Longrightarrow> corres (=) (?R63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd) (?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rv'd) (do p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (rvd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom rvd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom rvd));
return (fst p, fst (snd p))
od) (do y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd);
y <- assert (dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst p, fst (snd p))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?R63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. ?P65 t ta rv rv' rva rv'a rvb rv'b rvc and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. ?P'67 t ta rv rv' rva rv'a rvb rv'b rv'c and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 7. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 8. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 9. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 10. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd\<rbrakk> \<Longrightarrow> corres (=) (?R63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd) (?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rv'd) (do p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (rvd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom rvd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom rvd));
return (fst p, fst (snd p))
od) (do y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd);
y <- assert (dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?R63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 6. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 7. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 8. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 9. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 10. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd\<rbrakk> \<Longrightarrow> corres (=) (?P71 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd) (?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rv'd) (do p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (rvd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom rvd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom rvd));
return (fst p, fst (snd p))
od) (do y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd);
y <- assert (dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. ?P71 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 6. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 7. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 8. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 9. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 10. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd; dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd\<rbrakk> \<Longrightarrow> corres (=) (?P73 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd) (?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rv'd) (do p <- select (fst (f t (rv |` {pa. rva pa \<noteq> {}}) rva (tc, rvb |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va}, (rvd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv va = Some pa \<and> AllowRead \<in> rva va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` (- dom rvd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv va = Some pa \<and> AllowWrite \<in> rva va} \<circ> addrFromPPtr) |` dom rvd));
return (fst p, fst (snd p))
od) (do y <- assert (dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd);
y <- assert (dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd);
p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. ?P73 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 6. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 7. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 8. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 9. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 10. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> corres (=) (?P73 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd) (?R'63 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd) (do p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst p, fst (snd p))
od) (do p <- select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst p, fst (snd p))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. ?P73 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?R'63 t ta rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 6. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 7. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 8. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
 9. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 t ta rv'\<rbrace> gets (ptable_rights ta \<circ> absKState) \<lbrace>\<lambda>rv'a. invs' and ?Q'54 t ta rv rv' rv'a\<rbrace>
 10. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> gets (ptable_lift t) \<lbrace>\<lambda>rv. einvs and ?Q28 t ta rv\<rbrace>
A total of 15 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<forall>s'\<in>fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})). \<exists>s\<in>fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va})). s = s'
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> corres (=) (?R74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve) (?R'74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e) (do y <- do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rve, fst (snd rve))
od) (do y <- doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>?R74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>?R'74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 9. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 10. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> corres (=) (?R74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve) (?R'74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e) (do y <- do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- do_machine_op (device_memory_update ((snd (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rve, fst (snd rve))
od) (do y <- doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)));
y <- doMachineOp (device_memory_update ((snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>?R74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>?R'74 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 8. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
 9. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'54 t ta rv rv' rv'a\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'b. invs' and ?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace>
 10. \<And>t ta rv rv'. \<lbrakk>t = ta; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 t ta rv\<rbrace> gets (ptable_rights t) \<lbrace>\<lambda>rva. invs and ?Q53 t ta rv rv' rva\<rbrace>
A total of 17 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> corres_underlying Id False True (?r'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e) (?P115 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve) (?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e) (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd)))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf rv'f. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; ?r'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf rv'f\<rbrakk> \<Longrightarrow> corres (=) (?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf) (?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rv'f) (do y <- do_machine_op (device_memory_update ((snd (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rve, fst (snd rve))
od) (do y <- doMachineOp (device_memory_update ((snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?P115 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. ?P115 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve \<circ> machine_state\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. ?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 10. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> corres_underlying Id False True (?r'113 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e) (?P115 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e) (?Q116 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e) (user_memory_update ((\<lambda>a. (fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` (- dom rv'd))) (user_memory_update ((\<lambda>a. (fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` (- dom rv'd)))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf rv'f. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; ?r'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf rv'f\<rbrakk> \<Longrightarrow> corres (=) (?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf) (?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rv'f) (do y <- do_machine_op (device_memory_update ((snd (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rve, fst (snd rve))
od) (do y <- doMachineOp (device_memory_update ((snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?P115 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. ?P115 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve \<circ> machine_state\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. ?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 10. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; True\<rbrakk> \<Longrightarrow> no_fail (?Q116 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e) (user_memory_update ((\<lambda>a. (fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` (- dom rv'd)))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf rv'f. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; rvf = rv'f\<rbrakk> \<Longrightarrow> corres (=) (?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf) (?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rv'f) (do y <- do_machine_op (device_memory_update ((snd (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rve, fst (snd rve))
od) (do y <- doMachineOp (device_memory_update ((snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. (\<lambda>a. True) \<circ> machine_state\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. ?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 10. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> no_fail (?Q116 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e) (modify (\<lambda>ms. ms\<lparr>underlying_memory := \<lambda>a. case ((\<lambda>a. (fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` (- dom rv'd)) a of None \<Rightarrow> underlying_memory ms a | Some x \<Rightarrow> x\<rparr>))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf rv'f. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; rvf = rv'f\<rbrakk> \<Longrightarrow> corres (=) (?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rvf) (?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e rv'f) (do y <- do_machine_op (device_memory_update ((snd (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rve, fst (snd rve))
od) (do y <- doMachineOp (device_memory_update ((snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. (\<lambda>a. True) \<circ> machine_state\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. ?Q116 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rv'e \<circ> ksMachineState\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 10. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> corres (=) (?Q113 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e ()) (?Q'113 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e ()) (do y <- do_machine_op (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od) (do y <- doMachineOp (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd));
return (fst rv'e, fst (snd rv'e))
od)
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>?Q'113 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. (\<lambda>a. True) \<circ> machine_state\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. (\<lambda>a. True) \<circ> ksMachineState\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 t ta rv rv' rva rv'a rvb\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 t ta rv rv' rva rv'a rv'b\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 10. \<And>t ta rv rv' rva rv'a. \<lbrakk>t = ta; rv = rv'; rva = rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 t ta rv rv' rva\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>\<lambda>rvb. invs and ?Q59 t ta rv rv' rva rv'a rvb\<rbrace>
A total of 19 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> corres_underlying Id False True (?r'130 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e) (?P142 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e ()) (?Q140 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e ()) (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd)) (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e y ya. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; ?r'130 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e y ya\<rbrakk> \<Longrightarrow> corres (=) (dc y) (dc ya) (return (fst rv'e, fst (snd rv'e))) (return (fst rv'e, fst (snd rv'e)))
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?P142 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e () \<circ> machine_state\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd)) \<lbrace>dc\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?Q140 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e () \<circ> ksMachineState\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd)) \<lbrace>dc\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>\<lambda>a. ?P142 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e a \<circ> machine_state\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>\<lambda>a. ?Q140 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e a \<circ> ksMachineState\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. (\<lambda>a. True) \<circ> machine_state\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. (\<lambda>a. True) \<circ> ksMachineState\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 10. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
A total of 22 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; True\<rbrakk> \<Longrightarrow> no_fail (?Q140 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e ()) (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd))
 2. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e y ya. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e; y = ya\<rbrakk> \<Longrightarrow> corres (=) (dc y) (dc ya) (return (fst rv'e, fst (snd rv'e))) (return (fst rv'e, fst (snd rv'e)))
 3. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> machine_state\<rbrace> do_machine_op (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd)) \<lbrace>dc\<rbrace>
 4. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>?Q140 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd rv'd rv'e rv'e () \<circ> ksMachineState\<rbrace> doMachineOp (device_memory_update ((\<lambda>a. (snd (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va}) (addrFromPPtr a)) |` dom rv'd)) \<lbrace>dc\<rbrace>
 5. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> machine_state\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd rve)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state\<rbrace>
 6. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd; rve = rv'e\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>a. True) \<circ> ksMachineState\<rbrace> doMachineOp (user_memory_update ((fst (snd (snd rv'e)) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowWrite \<in> rv'a va} \<circ> addrFromPPtr) |` (- dom rv'd))) \<lbrace>\<lambda>a. ?Q140 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd rve rv'e a \<circ> ksMachineState\<rbrace>
 7. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rve. (\<lambda>a. True) \<circ> machine_state\<rbrace>
 8. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c; rvd = rv'd; dom (rv'b \<circ> addrFromPPtr) \<subseteq> - dom rv'd; dom (rv'c \<circ> addrFromPPtr) \<subseteq> dom rv'd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'109 ta ta rv' rv' rv'a rv'a rv'b rv'b rv'c rv'c rv'd\<rbrace> select (fst (f ta (rv' |` {pa. rv'a pa \<noteq> {}}) rv'a (tc, rv'b |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}, (rv'd \<circ> ptrFromPAddr) |` {pa. \<exists>va. rv' va = Some pa \<and> AllowRead \<in> rv'a va}))) \<lbrace>\<lambda>rv'e. (\<lambda>a. True) \<circ> ksMachineState\<rbrace>
 9. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 t ta rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>rvd. (\<lambda>_. True) and ?Q111 t ta rv rv' rva rv'a rvb rv'b rvc rv'c rvd and (\<lambda>s. dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd) and (\<lambda>s. dom (rvb \<circ> addrFromPPtr) \<subseteq> - dom rvd)\<rbrace>
 10. \<And>t ta rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>t = ta; rv = rv'; rva = rv'a; rvb = rv'b; rvc = rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 t ta rv rv' rva rv'a rvb rv'b rv'c\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'109 t ta rv rv' rva rv'a rvb rv'b rvc rv'c a\<rbrace>
A total of 22 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> ct_running s \<Longrightarrow> dom (device_mem s) \<subseteq> dom (device_state (machine_state s)) \<and> dom (user_mem s) \<subseteq> - dom (device_state (machine_state s))
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (invs' and (\<lambda>a. (invs' and (\<lambda>b. (invs' and (\<lambda>c. (invs' and ((\<lambda>_. True) and (\<lambda>d. ((\<lambda>_. True) and (\<lambda>e. \<forall>x\<in>fst (f (ksCurThread s) ((ptable_lift (ksCurThread s) \<circ> absKState) a |` {pa. (ptable_rights (ksCurThread s) \<circ> absKState) b pa \<noteq> {}}) ((ptable_rights (ksCurThread s) \<circ> absKState) b) (tc, (user_mem' c \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) a va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) b va}, ((device_state \<circ> ksMachineState) d \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) a va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) b va})). ((\<lambda>a. True) \<circ> ksMachineState) e)) d))) c)) b)) a)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (invs' and (\<lambda>a. (invs' and (\<lambda>b. (invs' and (\<lambda>c. (invs' and ((\<lambda>_. True) and (\<lambda>d. ((\<lambda>_. True) and (\<lambda>e. \<forall>x\<in>fst (f (ksCurThread s) ((ptable_lift (ksCurThread s) \<circ> absKState) a |` {pa. (ptable_rights (ksCurThread s) \<circ> absKState) b pa \<noteq> {}}) ((ptable_rights (ksCurThread s) \<circ> absKState) b) (tc, (user_mem' c \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) a va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) b va}, ((device_state \<circ> ksMachineState) d \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) a va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) b va})). ((\<lambda>a. True) \<circ> ksMachineState) e)) d))) c)) b)) a)) s)) s proof (prove)
goal:
No subgoals!