theory ArchNoninterference

lemma do_user_op_if_globals_equiv_scheduler[Noninterference_assms]:
  "\<lbrace>globals_equiv_scheduler st and invs\<rbrace>
   do_user_op_if tc uop
   \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" apply (simp add: do_user_op_if_def) apply (wpsimp wp: dmo_user_memory_update_globals_equiv_scheduler
                    dmo_device_memory_update_globals_equiv_scheduler)+ apply (auto simp: ptable_lift_s_def ptable_rights_s_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and invs\<rbrace> do_user_op_if tc uop \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and invs\<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 (tc t pl pr pxn (uop, 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 (tc t pl pr pxn (uop, 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>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x ae af ag ah ba. \<lbrakk>globals_equiv_scheduler st s; invs s; tc (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) (uop, (\<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> {}; (x, ae, af, ag, ah, ba) \<in> tc (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) (uop, (\<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> ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}} = ptable_lift (?t186 ah ba (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (cur_thread s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (exclusive_state (machine_state s)) () (x, ae, af, ag, ah, ba) x (ae, af, ag, ah, ba) ae (af, ag, ah, ba) af (ag, ah, ba) ag (ah, ba)) s |` {x. ptable_rights_s s x \<noteq> {}} \<and> ptable_rights_s s = ptable_rights (?t186 ah ba (ptable_rights_s s) (\<lambda>a. ptable_rights_s s a \<noteq> {} \<and> ptable_xn_s s a) (ptable_lift_s s |` {x. ptable_rights_s s x \<noteq> {}}) (cur_thread s) (\<lambda>a. user_mem s (ptrFromPAddr a)) (\<lambda>a. device_mem s (ptrFromPAddr a)) (device_state (machine_state s)) (exclusive_state (machine_state s)) () (x, ae, af, ag, ah, ba) x (ae, af, ag, ah, ba) ae (af, ag, ah, ba) af (ag, ah, ba) ag (ah, ba)) s proof (prove)
goal:
No subgoals!