theory ArchUserOp_IF

lemma do_user_op_reads_respects_g:
  notes split_paired_All[simp del]
  shows
    "(\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s
                                \<longrightarrow> (\<exists>x. uop (cur_thread s) pl pr pxn (tc, ms) = {x}))
     \<Longrightarrow> reads_respects_g aag l (pas_refined aag and invs and valid_vspace_objs_if
                                                 and is_subject aag \<circ> cur_thread
                                                 and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc)
                          (do_user_op_if uop tc)" apply (simp add: do_user_op_if_def) apply (rule use_spec_ev) apply (rule spec_equiv_valid_add_asm) apply (rule spec_equiv_valid_add_rel[OF _ reads_equiv_g_refl]) apply (rule spec_equiv_valid_add_rel'[OF _ affects_equiv_refl]) apply (rule spec_equiv_valid_inv_gets[where proj=id,simplified]) apply (clarsimp simp: reads_equiv_g_def) apply (rule requiv_ptable_rights_eq,simp+)[1] apply (rule spec_equiv_valid_inv_gets[where proj=id,simplified]) apply (rule ext) apply (clarsimp simp: reads_equiv_g_def) apply (case_tac "ptable_rights_s st x = {}", simp) apply simp apply (rule requiv_ptable_xn_eq,simp+)[1] apply (rule spec_equiv_valid_inv_gets[where proj=id,simplified]) apply (subst expand_restrict_map_eq,clarsimp) apply (clarsimp simp: reads_equiv_g_def) apply (rule requiv_ptable_lift_eq,simp+)[1] apply (rule spec_equiv_valid_inv_gets[where proj=id,simplified]) apply (clarsimp simp: reads_equiv_g_def) apply (rule requiv_cur_thread_eq,fastforce) apply (rule spec_equiv_valid_inv_gets_more[where proj="\<lambda>m. dom m \<inter> cw"
                                               and projsnd="\<lambda>m. m |` cr" for cr and cw]) apply (rule context_conjI') apply (subst expand_restrict_map_eq) apply (clarsimp simp: reads_equiv_g_def restrict_map_def) apply (rule requiv_user_mem_eq) apply simp+ apply fastforce apply (rule spec_equiv_valid_inv_gets[where proj = "\<lambda>x. ()", simplified]) apply (rule spec_equiv_valid_inv_gets_more[where proj = "\<lambda>m. (m \<circ> ptrFromPAddr) |` cr" for cr]) apply (rule conjI) apply (subst expand_restrict_map_eq) apply (clarsimp simp: restrict_map_def reads_equiv_g_def) apply (rule requiv_user_device_eq) apply simp+ apply (clarsimp simp: globals_equiv_def reads_equiv_g_def) apply (rule spec_equiv_valid_guard_imp) apply (wpsimp wp: dmo_user_memory_update_reads_respects_g dmo_device_state_update_reads_respects_g
                     dmo_setExMonitor_reads_respects_g dmo_device_state_update_reads_respects_g
                     select_ev dmo_getExMonitor_reads_respects_g dmo_wp) apply clarsimp apply (rule conjI) apply clarsimp apply (drule spec)+ apply (erule impE) prefer 2 apply assumption apply (clarsimp simp: context_matches_state_def comp_def  reads_equiv_g_def globals_equiv_def) apply (clarsimp simp: reads_equiv_g_def globals_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>x. uop (cur_thread s) pl pr pxn (tc, ms) = {x}) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and invs and valid_vspace_objs_if and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) (do_user_op_if uop tc) proof (prove)
goal (1 subgoal):
 1. \<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) (do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}) \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) (do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) (do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st) (do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (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 <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> ptable_rights_s st = ptable_rights_s t
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pxn <- gets (\<lambda>s x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t\<rbrakk> \<Longrightarrow> ptable_rights_s st = ptable_rights_s t
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pxn <- gets (\<lambda>s x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pxn <- gets (\<lambda>s x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) = (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s t x)
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t x. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> (ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) = (ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s t x)
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t x. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t\<rbrakk> \<Longrightarrow> (ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) = (ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s t x)
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t x. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st x \<noteq> {}\<rbrakk> \<Longrightarrow> (ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) = (ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s t x)
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t x. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st x \<noteq> {}\<rbrakk> \<Longrightarrow> ptable_xn_s st x = ptable_xn_s t x
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do pl <- gets (\<lambda>s. ptable_lift_s s |` {x. ptable_rights_s st x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t pl (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}} = ptable_lift_s t |` {x. ptable_rights_s st x \<noteq> {}}
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t x. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); reads_equiv_g aag st t; affects_equiv aag l st t; pas_refined aag st; reads_equiv_g aag st st; affects_equiv aag l st st; pas_refined aag t; invs st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; ptable_rights_s st x \<noteq> {}\<rbrakk> \<Longrightarrow> ptable_lift_s st x = ptable_lift_s t x
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t x. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; affects_equiv aag l st st; pas_refined aag t; invs st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; ptable_rights_s st x \<noteq> {}; reads_equiv aag st t; globals_equiv st t; reads_equiv aag st st; globals_equiv st st\<rbrakk> \<Longrightarrow> ptable_lift_s st x = ptable_lift_s t x
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop t (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> cur_thread st = cur_thread t
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t\<rbrakk> \<Longrightarrow> cur_thread st = cur_thread t
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, um |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> dom (user_mem st \<circ> ptrFromPAddr) \<inter> ?cw144 st = dom (user_mem t \<circ> ptrFromPAddr) \<inter> ?cw144 st \<and> (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = (user_mem t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = (user_mem t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}
 2. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t; (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = (user_mem t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}\<rbrakk> \<Longrightarrow> dom (user_mem st \<circ> ptrFromPAddr) \<inter> ?cw144 st = dom (user_mem t \<circ> ptrFromPAddr) \<inter> ?cw144 st
 3. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} \<longrightarrow> (user_mem st \<circ> ptrFromPAddr) x = (user_mem t \<circ> ptrFromPAddr) x
 2. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t; (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = (user_mem t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}\<rbrakk> \<Longrightarrow> dom (user_mem st \<circ> ptrFromPAddr) \<inter> ?cw144 st = dom (user_mem t \<circ> ptrFromPAddr) \<inter> ?cw144 st
 3. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> user_mem st (ptrFromPAddr x) = user_mem t (ptrFromPAddr x)
 2. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t; (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = (user_mem t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}\<rbrakk> \<Longrightarrow> dom (user_mem st \<circ> ptrFromPAddr) \<inter> ?cw144 st = dom (user_mem t \<circ> ptrFromPAddr) \<inter> ?cw144 st
 3. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (13 subgoals):
 1. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> reads_equiv (?aag195 st t x xa) st t
 2. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> globals_equiv st t
 3. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> invs st
 4. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> invs t
 5. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap st). obj_valid_pdpt x
 6. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap t). obj_valid_pdpt x
 7. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> is_subject (?aag195 st t x xa) (cur_thread st)
 8. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> AllowRead \<in> ptable_rights_s st (?x195 st t x xa)
 9. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> ptable_lift_s st (?x195 st t x xa) = Some x
 10. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> pas_refined (?aag195 st t x xa) st
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st \<and> invs st \<and> (\<forall>x\<in>ran (kheap st). obj_valid_pdpt x) \<and> is_subject aag (cur_thread st) \<and> cur_thread st \<noteq> idle_thread st \<and> P tc st; reads_equiv_g aag st st \<and> affects_equiv aag l st st; pas_refined aag t \<and> invs t \<and> (\<forall>x\<in>ran (kheap t). obj_valid_pdpt x) \<and> is_subject aag (cur_thread t) \<and> cur_thread t \<noteq> idle_thread t \<and> P tc t; reads_equiv_g aag st t; affects_equiv aag l st t; (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = (\<lambda>a. user_mem t (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}\<rbrakk> \<Longrightarrow> dom (\<lambda>a. user_mem st (ptrFromPAddr a)) \<inter> ?cw144 st = dom (\<lambda>a. user_mem t (ptrFromPAddr a)) \<inter> ?cw144 st
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = ((device_state \<circ> machine_state) t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} \<and> dom ((device_state \<circ> machine_state) st) = dom ((device_state \<circ> machine_state) t)
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} = ((device_state \<circ> machine_state) t \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}
 2. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> dom ((device_state \<circ> machine_state) st) = dom ((device_state \<circ> machine_state) t)
 3. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x} \<longrightarrow> ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) x = ((device_state \<circ> machine_state) t \<circ> ptrFromPAddr) x
 2. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> dom ((device_state \<circ> machine_state) st) = dom ((device_state \<circ> machine_state) t)
 3. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> device_state (machine_state st) (ptrFromPAddr x) = device_state (machine_state t) (ptrFromPAddr x)
 2. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> dom ((device_state \<circ> machine_state) st) = dom ((device_state \<circ> machine_state) t)
 3. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (13 subgoals):
 1. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> reads_equiv (?aag300 st t x xa) st t
 2. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> globals_equiv st t
 3. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> invs st
 4. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> invs t
 5. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap st). obj_valid_pdpt x
 6. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap t). obj_valid_pdpt x
 7. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> is_subject (?aag300 st t x xa) (cur_thread st)
 8. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> AllowRead \<in> ptable_rights_s st (?x300 st t x xa)
 9. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> ptable_lift_s st (?x300 st t x xa) = Some x
 10. \<And>st t x xa. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); affects_equiv aag l st t; pas_refined aag st; reads_equiv aag st st; pas_refined aag t; invs st; globals_equiv st st; affects_equiv aag l st st; invs t; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap t). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread t); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread t \<noteq> idle_thread t; P tc t; reads_equiv aag st t; globals_equiv st t; ptable_rights_s st xa \<noteq> {}; ptable_lift_s st xa = Some x; AllowRead \<in> ptable_rights_s st xa\<rbrakk> \<Longrightarrow> pas_refined (?aag300 st t x xa) st
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>st t. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st \<and> invs st \<and> (\<forall>x\<in>ran (kheap st). obj_valid_pdpt x) \<and> is_subject aag (cur_thread st) \<and> cur_thread st \<noteq> idle_thread st \<and> P tc st; reads_equiv_g aag st st \<and> affects_equiv aag l st st; pas_refined aag t \<and> invs t \<and> (\<forall>x\<in>ran (kheap t). obj_valid_pdpt x) \<and> is_subject aag (cur_thread t) \<and> cur_thread t \<noteq> idle_thread t \<and> P tc t; reads_equiv_g aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> dom (device_state (machine_state st)) = dom (device_state (machine_state t))
 2. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od) proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (?P'312 st) (do es <- do_machine_op getExMonitor;
y <- assert (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es) \<noteq> {});
a <- select (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, es));
case a of (e, a) \<Rightarrow> case a of (tc', a) \<Rightarrow> case a of (um', a) \<Rightarrow> case a of (ds', es') \<Rightarrow> do y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> machine_state) st))));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x} \<circ> addrFromPPtr) |` dom ((device_state \<circ> machine_state) st)));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od
od)
 2. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) s\<rbrakk> \<Longrightarrow> ?P'312 st s proof (prove)
goal (1 subgoal):
 1. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc) st; (pas_refined aag and invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc and reads_equiv_g aag st and affects_equiv aag l st) s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s \<and> True \<and> K (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<exists>x. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {x})) (s\<lparr>machine_state := machine_state s\<rparr>) \<and> (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (user_mem st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, ((device_state \<circ> machine_state) st \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> True \<and> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state (s\<lparr>machine_state := machine_state s\<rparr>)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {(a, aa, ab, ac, ad, b)})) \<and> (uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s))))))) proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {(a, aa, ab, ac, ad, b)})
 2. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {(a, aa, ab, ac, ad, b)}
 2. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}; P (?tc506 st s) (?s510 st s) \<and> context_matches_state (?pl500 st s) (?pr502 st s) (?pxn504 st s) (?ms508 st s) (?s510 st s) \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread (?s510 st s)) (?pl500 st s) (?pr502 st s) (?pxn504 st s) (?tc506 st s, ?ms508 st s) = {(a, aa, ab, ac, ad, b)})\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {(a, aa, ab, ac, ad, b)}
 2. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal (3 subgoals):
 1. \<And>st s. \<lbrakk>pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}\<rbrakk> \<Longrightarrow> P (?tc506 st s) (?s510 st s) \<and> context_matches_state (?pl500 st s) (?pr502 st s) (?pxn504 st s) (?ms508 st s) (?s510 st s)
 2. \<And>st s. \<lbrakk>pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}; \<exists>a aa ab ac ad b. uop (cur_thread (?s510 st s)) (?pl500 st s) (?pr502 st s) (?pxn504 st s) (?tc506 st s, ?ms508 st s) = {(a, aa, ab, ac, ad, b)}\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {(a, aa, ab, ac, ad, b)}
 3. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal (3 subgoals):
 1. \<And>st s. \<lbrakk>pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}; \<exists>a aa ab ac ad b. uop (cur_thread (?s510 st s)) (?pl500 st s) (?pr502 st s) (?pxn504 st s) (?tc506 st s, ?ms508 st s) = {(a, aa, ab, ac, ad, b)}\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) = {(a, aa, ab, ac, ad, b)}
 2. \<And>st s. \<lbrakk>pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}\<rbrakk> \<Longrightarrow> P (?tc506 st s) (?s510 st s) \<and> context_matches_state (?pl500 st s) (?pr502 st s) (?pxn504 st s) (?ms508 st s) (?s510 st s)
 3. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s; uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {}\<rbrakk> \<Longrightarrow> P tc st \<and> context_matches_state (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) ((\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (device_state (machine_state st) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) st
 2. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal (1 subgoal):
 1. \<And>st s. \<lbrakk>\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>a aa ab ac ad b. uop (cur_thread s) pl pr pxn (tc, ms) = {(a, aa, ab, ac, ad, b)}); pas_refined aag st; pas_refined aag s; invs st; invs s; \<forall>x\<in>ran (kheap st). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; is_subject aag (cur_thread st); is_subject aag (cur_thread s); cur_thread st \<noteq> idle_thread st; P tc st; cur_thread s \<noteq> idle_thread s; P tc s; reads_equiv_g aag st s; affects_equiv aag l st s\<rbrakk> \<Longrightarrow> uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>uop (cur_thread st) (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) (ptable_rights_s st) (\<lambda>x. ptable_rights_s st x \<noteq> {} \<and> ptable_xn_s st x) (tc, (\<lambda>a. user_mem st (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, (\<lambda>a. device_state (machine_state st) (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s st x}, exclusive_state (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>x. (\<exists>a b. xb = (x, a, b)) \<longrightarrow> dom (\<lambda>a. (x |` {y. \<exists>x. (ptable_lift_s st |` {x. ptable_rights_s st x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s st x}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state st)) \<subseteq> dom (device_state (machine_state s)))))) proof (prove)
goal:
No subgoals!