theory ArchADT_IF_Refine

lemma doUserOp_if_empty_fail[ADT_IF_Refine_assms]:
  "empty_fail (doUserOp_if uop tc)" apply (simp add: doUserOp_if_def) apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (wp (once)) apply wp apply (subst bind_assoc[symmetric]) apply (rule empty_fail_bind) apply (rule empty_fail_select_bind) apply (wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (doUserOp_if uop tc) proof (prove)
goal (1 subgoal):
 1. empty_fail (do pr <- gets ptable_rights_s';
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. empty_fail (gets ptable_rights_s')
 2. \<And>x. empty_fail (do pxn <- gets (\<lambda>s xa. x xa \<noteq> {} \<and> ptable_xn_s' s xa);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {xa. x xa \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t pl x pxn (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl x pxn (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail (do pxn <- gets (\<lambda>s xa. x xa \<noteq> {} \<and> ptable_xn_s' s xa);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {xa. x xa \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t pl x pxn (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl x pxn (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x. empty_fail (gets (\<lambda>s xa. x xa \<noteq> {} \<and> ptable_xn_s' s xa))
 2. \<And>x xa. empty_fail (do pl <- gets (\<lambda>s. ptable_lift_s' s |` {xa. x xa \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t pl x xa (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl x xa (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. empty_fail (do pl <- gets (\<lambda>s. ptable_lift_s' s |` {xa. x xa \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t pl x xa (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl x xa (tc, um |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. pl xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. pl xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. empty_fail (gets (\<lambda>s. ptable_lift_s' s |` {xa. x xa \<noteq> {}}))
 2. \<And>x xa xb. empty_fail (do t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. empty_fail (do t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop t xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. empty_fail getCurThread
 2. \<And>x xa xb xc. empty_fail (do um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. empty_fail (do um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, um |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc. empty_fail (gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr))
 2. \<And>x xa xb xc xd. empty_fail (do dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd. empty_fail (do dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd. empty_fail (gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr))
 2. \<And>x xa xb xc xd xe. empty_fail (do ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe. empty_fail (do ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd xe. empty_fail (gets (device_state \<circ> ksMachineState))
 2. \<And>x xa xb xc xd xe xf. empty_fail (do y <- assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom xf);
y <- assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom xf);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe xf. empty_fail (do y <- assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom xf);
y <- assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom xf);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd xe xf. empty_fail (assert (dom (xd \<circ> addrFromPPtr) \<subseteq> - dom xf))
 2. \<And>x xa xb xc xd xe xf xg. empty_fail (do y <- assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom xf);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe xf xg. empty_fail (do y <- assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom xf);
es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd xe xf xg. empty_fail (assert (dom (xe \<circ> addrFromPPtr) \<subseteq> dom xf))
 2. \<And>x xa xb xc xd xe xf xg xh. empty_fail (do es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe xf xg xh. empty_fail (do es <- doMachineOp getExMonitor;
y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, es));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd xe xf xg xh. empty_fail (doMachineOp getExMonitor)
 2. \<And>x xa xb xc xd xe xf xg xh xi. empty_fail (do y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe xf xg xh xi. empty_fail (do y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi) \<noteq> {});
(e, tc', um', ds', es') <- select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi));
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe xf xg xh xi. empty_fail (do (e, tc', um', ds', es') <- do y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi) \<noteq> {});
select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi))
od;
y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd xe xf xg xh xi. empty_fail (do y <- assert (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi) \<noteq> {});
select (uop xc xb x xa (tc, xd |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, (xf \<circ> ptrFromPAddr) |` {y. \<exists>xa. xb xa = Some y \<and> AllowRead \<in> x xa}, xi))
od)
 2. \<And>x xa xb xc xd xe xf xg xh xi xj. empty_fail (case xj of (e, tc', um', ds', es') \<Rightarrow> do y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd xe xf xg xh xi xj. empty_fail (case xj of (e, tc', um', ds', es') \<Rightarrow> do y <- doMachineOp (user_memory_update ((um' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` (- dom xf)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>xa. xb xa = Some y \<and> AllowWrite \<in> x xa} \<circ> addrFromPPtr) |` dom xf));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od) proof (prove)
goal:
No subgoals!