theory ArchNoninterference

lemma do_user_op_if_integrity[Noninterference_assms]:
  "\<lbrace>invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag\<rbrace>
   do_user_op_if uop tc
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: do_user_op_if_def) apply (wpsimp wp: dmo_user_memory_update_respects_Write dmo_device_update_respects_Write
                    hoare_vcg_all_lift hoare_vcg_imp_lift
            wp_del: select_wp) apply (rule hoare_pre_cont) apply (wp | wpc | clarsimp)+ apply (rule conjI) apply clarsimp apply (simp add: restrict_map_def ptable_lift_s_def ptable_rights_s_def split: if_splits) apply (drule_tac auth=Write in user_op_access') apply (simp add: vspace_cap_rights_to_auth_def)+ apply clarsimp apply (simp add: restrict_map_def ptable_lift_s_def ptable_rights_s_def split: if_splits) apply (drule_tac auth=Write in user_op_access') apply (simp add: vspace_cap_rights_to_auth_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>pr pxn pl x um dm ds a b xa aa ab ac ad ba. \<lbrace>?P'137 aa ab ac ad ba (ad, ba) (ac, ad, ba) (ab, ac, ad, ba) a b pr pxn pl x um dm ds (a, b) () xa (aa, ab, ac, ad, ba)\<rbrace> select (uop x 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}, a, b)) \<lbrace>\<lambda>rv s. rv \<noteq> (xa, aa, ab, ac, ad, ba)\<rbrace>
 2. \<And>pr pxn pl x um dm ds es y xa xb. \<lbrace>?Q'124 pr pxn pl x um dm ds es y xa xb\<rbrace> select (uop x 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)) \<lbrace>\<lambda>rv s. \<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>xa xc. xb = (xa, xc) \<longrightarrow> (integrity aag X st and K (\<forall>p\<in>dom ((x |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<and> K (\<forall>p\<in>dom ((xa |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) s))\<rbrace>
 3. \<And>pr pxn pl x um dm ds es. \<lbrace>?B9 pr pxn pl x um dm ds es\<rbrace> assert (uop x 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> {}) \<lbrace>\<lambda>y s. \<forall>xa xb. ?P'137 (fst xb) (fst (snd xb)) (fst (snd (snd xb))) (fst (snd (snd (snd xb)))) (snd (snd (snd (snd xb)))) (snd (snd (snd xb))) (snd (snd xb)) (snd xb) (fst es) (snd es) pr pxn pl x um dm ds es y xa xb s \<or> ?Q'124 pr pxn pl x um dm ds es y xa xb s\<rbrace>
 4. \<And>pr pxn pl x um dm ds. \<lbrace>?B8 pr pxn pl x um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?B9 pr pxn pl x um dm ds\<rbrace>
 5. \<And>pr pxn pl x um dm. \<lbrace>?B7 pr pxn pl x um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?B8 pr pxn pl x um dm\<rbrace>
 6. \<And>pr pxn pl x um. \<lbrace>?B6 pr pxn pl x um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B7 pr pxn pl x um\<rbrace>
 7. \<And>pr pxn pl x. \<lbrace>?B5 pr pxn pl x\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B6 pr pxn pl x\<rbrace>
 8. \<And>pr pxn pl. \<lbrace>?B4 pr pxn pl\<rbrace> gets cur_thread \<lbrace>?B5 pr pxn pl\<rbrace>
 9. \<And>pr pxn. \<lbrace>?B3 pr pxn\<rbrace> gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}}) \<lbrace>?B4 pr pxn\<rbrace>
 10. \<And>pr. \<lbrace>?B2 pr\<rbrace> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x) \<lbrace>?B3 pr\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pr pxn pl x um dm ds es y xa xb. \<lbrace>?Q'124 pr pxn pl x um dm ds es y xa xb\<rbrace> select (uop x 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)) \<lbrace>\<lambda>rv s. \<forall>x xa. xb = (x, xa) \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> (\<forall>xa xc. xb = (xa, xc) \<longrightarrow> (integrity aag X st and K (\<forall>p\<in>dom ((x |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<and> K (\<forall>p\<in>dom ((xa |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) s))\<rbrace>
 2. \<And>pr pxn pl x um dm ds es. \<lbrace>?B9 pr pxn pl x um dm ds es\<rbrace> assert (uop x 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> {}) \<lbrace>\<lambda>y s. \<forall>xa xb. False \<or> ?Q'124 pr pxn pl x um dm ds es y xa xb s\<rbrace>
 3. \<And>pr pxn pl x um dm ds. \<lbrace>?B8 pr pxn pl x um dm ds\<rbrace> do_machine_op getExMonitor \<lbrace>?B9 pr pxn pl x um dm ds\<rbrace>
 4. \<And>pr pxn pl x um dm. \<lbrace>?B7 pr pxn pl x um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?B8 pr pxn pl x um dm\<rbrace>
 5. \<And>pr pxn pl x um. \<lbrace>?B6 pr pxn pl x um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B7 pr pxn pl x um\<rbrace>
 6. \<And>pr pxn pl x. \<lbrace>?B5 pr pxn pl x\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B6 pr pxn pl x\<rbrace>
 7. \<And>pr pxn pl. \<lbrace>?B4 pr pxn pl\<rbrace> gets cur_thread \<lbrace>?B5 pr pxn pl\<rbrace>
 8. \<And>pr pxn. \<lbrace>?B3 pr pxn\<rbrace> gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}}) \<lbrace>?B4 pr pxn\<rbrace>
 9. \<And>pr. \<lbrace>?B2 pr\<rbrace> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x) \<lbrace>?B3 pr\<rbrace>
 10. \<lbrace>?Q1\<rbrace> gets ptable_rights_s \<lbrace>?B2\<rbrace>
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> (\<forall>a. \<forall>p\<in>dom (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x} \<circ> addrFromPPtr) \<inter> - dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) \<and> (\<forall>a. \<forall>p\<in>dom (\<lambda>b. (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr b)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> \<forall>a. \<forall>p\<in>dom (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x} \<circ> addrFromPPtr) \<inter> - dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> \<forall>a. \<forall>p\<in>dom (\<lambda>b. (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr b)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ad b ae p y. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)); (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; (ae |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) p = Some y
 2. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> \<forall>a. \<forall>p\<in>dom (\<lambda>b. (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr b)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ad b ae p y x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) p = Some y
 2. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> \<forall>a. \<forall>p\<in>dom (\<lambda>b. (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr b)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (6 subgoals):
 1. \<And>s a aa ab ac ad b ae p y x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> pas_refined (?aag271 s a aa ab ac ad b ae p y x) s
 2. \<And>s a aa ab ac ad b ae p y x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> is_subject (?aag271 s a aa ab ac ad b ae p y x) (?tcb271 s a aa ab ac ad b ae p y x)
 3. \<And>s a aa ab ac ad b ae p y x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> ptable_lift (?tcb271 s a aa ab ac ad b ae p y x) s (?x271 s a aa ab ac ad b ae p y x) = Some (addrFromPPtr (?ptr271 s a aa ab ac ad b ae p y x))
 4. \<And>s a aa ab ac ad b ae p y x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> Write \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb271 s a aa ab ac ad b ae p y x) s (?x271 s a aa ab ac ad b ae p y x))
 5. \<And>s a aa ab ac ad b ae p y x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); (pasObjectAbs (?aag271 s a aa ab ac ad b ae p y x) (?tcb271 s a aa ab ac ad b ae p y x), Write, pasObjectAbs (?aag271 s a aa ab ac ad b ae p y x) (?ptr271 s a aa ab ac ad b ae p y x)) \<in> pasPolicy (?aag271 s a aa ab ac ad b ae p y x)\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) p = Some y
 6. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> \<forall>a. \<forall>p\<in>dom (\<lambda>b. (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr b)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab ac ad b. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s))\<rbrakk> \<Longrightarrow> \<forall>a. \<forall>p\<in>dom (\<lambda>b. (a |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr b)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab ac ad b ae p y ya. \<lbrakk>invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s s x}, exclusive_state (machine_state s)); (ae |` {y. \<exists>x. (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s s x}) (addrFromPPtr p) = Some y; device_state (machine_state s) p = Some ya\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab ac ad b ae p y ya x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; device_state (machine_state s) p = Some ya; invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>s a aa ab ac ad b ae p y ya x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; device_state (machine_state s) p = Some ya; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> pas_refined (?aag355 s a aa ab ac ad b ae p y ya x) s
 2. \<And>s a aa ab ac ad b ae p y ya x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; device_state (machine_state s) p = Some ya; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> is_subject (?aag355 s a aa ab ac ad b ae p y ya x) (?tcb355 s a aa ab ac ad b ae p y ya x)
 3. \<And>s a aa ab ac ad b ae p y ya x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; device_state (machine_state s) p = Some ya; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> ptable_lift (?tcb355 s a aa ab ac ad b ae p y ya x) s (?x355 s a aa ab ac ad b ae p y ya x) = Some (addrFromPPtr (?ptr355 s a aa ab ac ad b ae p y ya x))
 4. \<And>s a aa ab ac ad b ae p y ya x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; device_state (machine_state s) p = Some ya; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p)\<rbrakk> \<Longrightarrow> Write \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb355 s a aa ab ac ad b ae p y ya x) s (?x355 s a aa ab ac ad b ae p y ya x))
 5. \<And>s a aa ab ac ad b ae p y ya x. \<lbrakk>(a, aa, ab, ac, ad, b) \<in> uop (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); uop (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa = {} \<or> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; device_state (machine_state s) p = Some ya; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; AllowWrite \<in> ptable_rights (cur_thread s) s x; ae (addrFromPPtr p) = Some y; ptable_rights (cur_thread s) s x \<noteq> {}; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); (pasObjectAbs (?aag355 s a aa ab ac ad b ae p y ya x) (?tcb355 s a aa ab ac ad b ae p y ya x), Write, pasObjectAbs (?aag355 s a aa ab ac ad b ae p y ya x) (?ptr355 s a aa ab ac ad b ae p y ya x)) \<in> pasPolicy (?aag355 s a aa ab ac ad b ae p y ya x)\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!