theory ADT_AC

lemma do_user_op_respects:
 "\<lbrace>invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag\<rbrace>
  do_user_op uop tc
  \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: do_user_op_def) apply wpsimp+ apply (rule dmo_device_update_respects_Write) apply (wpsimp wp: dmo_um_upd_machine_state
                            dmo_user_memory_update_respects_Write
                            hoare_vcg_all_lift hoare_vcg_imp_lift
                    wp_del: select_wp)+ apply (rule hoare_pre_cont) apply (wpsimp wp: select_wp)+ apply (simp add: restrict_map_def split: if_splits) apply (rule conjI) apply (clarsimp split: if_splits) apply (drule_tac auth=Write in user_op_access') apply (simp add: write_in_vspace_cap_rights)+ apply (rule conjI, simp) apply (clarsimp split: if_splits) apply (drule_tac auth=Write in user_op_access') apply (simp add: write_in_vspace_cap_rights)+ 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 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 t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
(e, tc', um', ds') <- select (fst (uop t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((um' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (e, tc')
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>t conv rights um dm ds x1 x1a x1b x2b. \<lbrace>?B34 t conv rights um dm ds (x1, x1a, x1b, x2b) x1 (x1a, x1b, x2b) x1a (x1b, x2b) x1b x2b ()\<rbrace> do_machine_op (device_memory_update ((x2b |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds)) \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 2. \<And>t conv rights um dm ds x x1 x2 x1a x2a x1b x2b. \<lbrakk>x = (x1, x2); x2 = (x1a, x2a); x2a = (x1b, x2b)\<rbrakk> \<Longrightarrow> \<lbrace>?R32 t conv rights um dm ds x x1 x2 x1a x2a x1b x2b\<rbrace> do_machine_op (user_memory_update ((x1b |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>?B34 t conv rights um dm ds x x1 x2 x1a x2a x1b x2b\<rbrace>
 3. \<And>t conv rights um dm ds. \<lbrace>?B7 t conv rights um dm ds\<rbrace> select (fst (uop t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}))) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> (\<forall>xe xf. xd = (xe, xf) \<longrightarrow> ?R32 t conv rights um dm ds x xa xb xc xd xe xf s))\<rbrace>
 4. \<And>t conv rights um dm. \<lbrace>?B6 t conv rights um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?B7 t conv rights um dm\<rbrace>
 5. \<And>t conv rights um. \<lbrace>?B5 t conv rights um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B6 t conv rights um\<rbrace>
 6. \<And>t conv rights. \<lbrace>?B4 t conv rights\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B5 t conv rights\<rbrace>
 7. \<And>t conv. \<lbrace>?B3 t conv\<rbrace> gets (ptable_rights t) \<lbrace>?B4 t conv\<rbrace>
 8. \<And>t. \<lbrace>?B2 t\<rbrace> gets (ptable_lift t) \<lbrace>?B3 t\<rbrace>
 9. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 10. \<And>s. (invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag) s \<Longrightarrow> ?Q1 s proof (prove)
goal (9 subgoals):
 1. \<And>t conv rights um dm ds x x1 x2 x1a x2a x1b x2b. \<lbrakk>x = (x1, x2); x2 = (x1a, x2a); x2a = (x1b, x2b)\<rbrakk> \<Longrightarrow> \<lbrace>?R32 t conv rights um dm ds x x1 x2 x1a x2a x1b x2b\<rbrace> do_machine_op (user_memory_update ((x1b |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>a. integrity aag X st and (\<lambda>s. device_state (machine_state s) = ?um73 t conv rights um dm ds x x1 x2 x1a x2a x1b x2b a) and K (\<forall>p\<in>dom ((x2b |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)\<rbrace>
 2. \<And>t conv rights um dm ds. \<lbrace>?B7 t conv rights um dm ds\<rbrace> select (fst (uop t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}))) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> (\<forall>xe xf. xd = (xe, xf) \<longrightarrow> ?R32 t conv rights um dm ds x xa xb xc xd xe xf s))\<rbrace>
 3. \<And>t conv rights um dm. \<lbrace>?B6 t conv rights um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?B7 t conv rights um dm\<rbrace>
 4. \<And>t conv rights um. \<lbrace>?B5 t conv rights um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B6 t conv rights um\<rbrace>
 5. \<And>t conv rights. \<lbrace>?B4 t conv rights\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B5 t conv rights\<rbrace>
 6. \<And>t conv. \<lbrace>?B3 t conv\<rbrace> gets (ptable_rights t) \<lbrace>?B4 t conv\<rbrace>
 7. \<And>t. \<lbrace>?B2 t\<rbrace> gets (ptable_lift t) \<lbrace>?B3 t\<rbrace>
 8. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 9. \<And>s. (invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag) s \<Longrightarrow> ?Q1 s proof (prove)
goal (9 subgoals):
 1. \<And>t conv rights um dm ds x a aa b. \<lbrace>?P'104 a aa b (aa, b) t conv rights um dm ds x (a, aa, b)\<rbrace> select (fst (uop t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}))) \<lbrace>\<lambda>rv s. rv \<noteq> (x, a, aa, b)\<rbrace>
 2. \<And>t conv rights um dm ds x xa. \<lbrace>?Q'98 t conv rights um dm ds x xa\<rbrace> select (fst (uop t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}))) \<lbrace>\<lambda>rv s. \<forall>xb xc. xa = (xb, xc) \<longrightarrow> (\<forall>xd xe. xc = (xd, xe) \<longrightarrow> (integrity aag X st and K (\<forall>p\<in>dom ((xd |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<and> device_state (machine_state s) = ?um97 t conv rights um dm ds rv x xa xb xc xd xe \<and> K (\<forall>p\<in>dom ((xe |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) s)\<rbrace>
 3. \<And>t conv rights um dm. \<lbrace>?B6 t conv rights um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>ds s. \<forall>x xa. ?P'104 (fst xa) (fst (snd xa)) (snd (snd xa)) (snd xa) t conv rights um dm ds x xa s \<or> ?Q'98 t conv rights um dm ds x xa s\<rbrace>
 4. \<And>t conv rights um. \<lbrace>?B5 t conv rights um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B6 t conv rights um\<rbrace>
 5. \<And>t conv rights. \<lbrace>?B4 t conv rights\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B5 t conv rights\<rbrace>
 6. \<And>t conv. \<lbrace>?B3 t conv\<rbrace> gets (ptable_rights t) \<lbrace>?B4 t conv\<rbrace>
 7. \<And>t. \<lbrace>?B2 t\<rbrace> gets (ptable_lift t) \<lbrace>?B3 t\<rbrace>
 8. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 9. \<And>s. (invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag) s \<Longrightarrow> ?Q1 s proof (prove)
goal (8 subgoals):
 1. \<And>t conv rights um dm ds x xa. \<lbrace>?Q'98 t conv rights um dm ds x xa\<rbrace> select (fst (uop t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}))) \<lbrace>\<lambda>rv s. \<forall>xb xc. xa = (xb, xc) \<longrightarrow> (\<forall>xd xe. xc = (xd, xe) \<longrightarrow> (integrity aag X st and K (\<forall>p\<in>dom ((xd |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<and> device_state (machine_state s) = ?um97 t conv rights um dm ds rv x xa xb xc xd xe \<and> K (\<forall>p\<in>dom ((xe |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) s)\<rbrace>
 2. \<And>t conv rights um dm. \<lbrace>?B6 t conv rights um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>\<lambda>ds s. \<forall>x xa. False \<or> ?Q'98 t conv rights um dm ds x xa s\<rbrace>
 3. \<And>t conv rights um. \<lbrace>?B5 t conv rights um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B6 t conv rights um\<rbrace>
 4. \<And>t conv rights. \<lbrace>?B4 t conv rights\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B5 t conv rights\<rbrace>
 5. \<And>t conv. \<lbrace>?B3 t conv\<rbrace> gets (ptable_rights t) \<lbrace>?B4 t conv\<rbrace>
 6. \<And>t. \<lbrace>?B2 t\<rbrace> gets (ptable_lift t) \<lbrace>?B3 t\<rbrace>
 7. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 8. \<And>s. (invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (uop (cur_thread s) (ptable_lift (cur_thread s) s |` {pa. ptable_rights (cur_thread s) s pa \<noteq> {}}) (ptable_rights (cur_thread s) s) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowRead \<in> ptable_rights (cur_thread s) s va}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowRead \<in> ptable_rights (cur_thread s) s va})); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>p\<in>dom (aa |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va} \<circ> addrFromPPtr) \<inter> - dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) \<and> device_state (machine_state s) = ?um142 ab ac ad ba (ad, ba) (ac, ad, ba) (cur_thread s) (ptable_lift (cur_thread s) s) (ptable_rights (cur_thread s) s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (ab, ac, ad, ba) x (a, aa, b) a (aa, b) aa b \<and> (\<forall>p\<in>dom (\<lambda>a. (b |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va}) (addrFromPPtr a)) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>p\<in>dom ((\<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then aa x else None) \<circ> addrFromPPtr) \<inter> - dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) \<and> device_state (machine_state s) = ?um142 ab ac ad ba (ad, ba) (ac, ad, ba) (cur_thread s) (ptable_lift (cur_thread s) s) (ptable_rights (cur_thread s) s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (ab, ac, ad, ba) x (a, aa, b) a (aa, b) aa b \<and> (\<forall>p\<in>dom (\<lambda>a. if \<exists>va. ptable_lift (cur_thread s) s va = Some (addrFromPPtr a) \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then b (addrFromPPtr a) else None) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>p\<in>dom ((\<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then aa x else None) \<circ> addrFromPPtr) \<inter> - dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> device_state (machine_state s) = ?um142 ab ac ad ba (ad, ba) (ac, ad, ba) (cur_thread s) (ptable_lift (cur_thread s) s) (ptable_rights (cur_thread s) s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (ab, ac, ad, ba) x (a, aa, b) a (aa, b) aa b \<and> (\<forall>p\<in>dom (\<lambda>a. if \<exists>va. ptable_lift (cur_thread s) s va = Some (addrFromPPtr a) \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then b (addrFromPPtr a) else None) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ab ac ad ba p y va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; aa (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) p = Some y
 2. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> device_state (machine_state s) = ?um142 ab ac ad ba (ad, ba) (ac, ad, ba) (cur_thread s) (ptable_lift (cur_thread s) s) (ptable_rights (cur_thread s) s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (ab, ac, ad, ba) x (a, aa, b) a (aa, b) aa b \<and> (\<forall>p\<in>dom (\<lambda>a. if \<exists>va. ptable_lift (cur_thread s) s va = Some (addrFromPPtr a) \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then b (addrFromPPtr a) else None) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (6 subgoals):
 1. \<And>s aa ab ac ad ba p y va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; aa (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s aa ab ac ad ba p y va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; aa (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> is_subject aag (?tcb178 s aa ab ac ad ba p y va)
 3. \<And>s aa ab ac ad ba p y va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; aa (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> ptable_lift (?tcb178 s aa ab ac ad ba p y va) s (?x178 s aa ab ac ad ba p y va) = Some (addrFromPPtr (?ptr178 s aa ab ac ad ba p y va))
 4. \<And>s aa ab ac ad ba p y va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; aa (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> Write \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb178 s aa ab ac ad ba p y va) s (?x178 s aa ab ac ad ba p y va))
 5. \<And>s aa ab ac ad ba p y va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; (pasSubject aag, Write, pasObjectAbs aag p) \<notin> pasPolicy aag; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; aa (addrFromPPtr p) = Some y; (pasObjectAbs aag (?tcb178 s aa ab ac ad ba p y va), Write, pasObjectAbs aag (?ptr178 s aa ab ac ad ba p y va)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) p = Some y
 6. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> device_state (machine_state s) = ?um142 ab ac ad ba (ad, ba) (ac, ad, ba) (cur_thread s) (ptable_lift (cur_thread s) s) (ptable_rights (cur_thread s) s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (ab, ac, ad, ba) x (a, aa, b) a (aa, b) aa b \<and> (\<forall>p\<in>dom (\<lambda>a. if \<exists>va. ptable_lift (cur_thread s) s va = Some (addrFromPPtr a) \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then b (addrFromPPtr a) else None) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> device_state (machine_state s) = ?um142 ab ac ad ba (ad, ba) (ac, ad, ba) (cur_thread s) (ptable_lift (cur_thread s) s) (ptable_rights (cur_thread s) s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (ab, ac, ad, ba) x (a, aa, b) a (aa, b) aa b \<and> (\<forall>p\<in>dom (\<lambda>a. if \<exists>va. ptable_lift (cur_thread s) s va = Some (addrFromPPtr a) \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then b (addrFromPPtr a) else None) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b ab ac ad ba. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>p\<in>dom (\<lambda>a. if \<exists>va. ptable_lift (cur_thread s) s va = Some (addrFromPPtr a) \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va then b (addrFromPPtr a) else None) \<inter> dom (device_state (machine_state s)). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s b ab ac ad ba p y ya va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); invs s; integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; device_state (machine_state s) p = Some ya; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; b (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>s b ab ac ad ba p y ya va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; device_state (machine_state s) p = Some ya; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; b (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s b ab ac ad ba p y ya va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; device_state (machine_state s) p = Some ya; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; b (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> is_subject aag (?tcb206 s b ab ac ad ba p y ya va)
 3. \<And>s b ab ac ad ba p y ya va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; device_state (machine_state s) p = Some ya; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; b (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> ptable_lift (?tcb206 s b ab ac ad ba p y ya va) s (?x206 s b ab ac ad ba p y ya va) = Some (addrFromPPtr (?ptr206 s b ab ac ad ba p y ya va))
 4. \<And>s b ab ac ad ba p y ya va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; device_state (machine_state s) p = Some ya; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; b (addrFromPPtr p) = Some y\<rbrakk> \<Longrightarrow> Write \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb206 s b ab ac ad ba p y ya va) s (?x206 s b ab ac ad ba p y ya va))
 5. \<And>s b ab ac ad ba p y ya va. \<lbrakk>(ab, ac, ad, ba) \<in> fst (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) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); integrity aag X st s; is_subject aag (cur_thread s); pas_refined aag s; device_state (machine_state s) p = Some ya; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; b (addrFromPPtr p) = Some y; (pasObjectAbs aag (?tcb206 s b ab ac ad ba p y ya va), Write, pasObjectAbs aag (?ptr206 s b ab ac ad ba p y ya va)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!