theory Noninterference

lemma dmo_user_memory_update_globals_equiv_scheduler:
  "\<lbrace>globals_equiv_scheduler st and
    (invs and (\<lambda>s. pl = ptable_lift t s |` {x. pr x \<noteq> {}} \<and> pr = ptable_rights t s))\<rbrace>
   do_machine_op
     (user_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` S))
   \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" apply (rule do_machine_op_globals_equiv_scheduler) apply clarsimp apply (erule use_valid) apply (simp add: user_memory_update_def) apply (wp modify_wp) apply (clarsimp simp: globals_equiv_scheduler_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and (invs and (\<lambda>s. pl = ptable_lift t s |` {x. pr x \<noteq> {}} \<and> pr = ptable_rights t s))\<rbrace> do_machine_op (user_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` S)) \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(invs and (\<lambda>s. pl = ptable_lift t s |` {x. pr x \<noteq> {}} \<and> pr = ptable_rights t s)) sa; globals_equiv_scheduler s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (user_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` S) (machine_state sa)). globals_equiv_scheduler s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; ((), b) \<in> fst (user_memory_update ((ba |` {y. \<exists>x. (ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights t sa x} \<circ> addrFromPPtr) |` S) (machine_state sa)); invs sa; pl = ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}; pr = ptable_rights t sa\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; invs sa; pl = ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}; pr = ptable_rights t sa\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s sa b\<rbrace> user_memory_update ((ba |` {y. \<exists>x. (ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights t sa x} \<circ> addrFromPPtr) |` S) \<lbrace>\<lambda>a b. globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; invs sa; pl = ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}; pr = ptable_rights t sa\<rbrakk> \<Longrightarrow> ?P11 s sa b (machine_state sa) proof (prove)
goal (2 subgoals):
 1. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; invs sa; pl = ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}; pr = ptable_rights t sa\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s sa b\<rbrace> modify (\<lambda>ms. ms\<lparr>underlying_memory := \<lambda>a. case ((\<lambda>a. (ba |` {y. \<exists>x. (ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights t sa x}) (addrFromPPtr a)) |` S) a of None \<Rightarrow> underlying_memory ms a | Some x \<Rightarrow> x\<rparr>) \<lbrace>\<lambda>a b. globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; invs sa; pl = ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}; pr = ptable_rights t sa\<rbrakk> \<Longrightarrow> ?P11 s sa b (machine_state sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; invs sa; pl = ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}; pr = ptable_rights t sa\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := machine_state sa\<lparr>underlying_memory := \<lambda>a. case ((\<lambda>a. (ba |` {y. \<exists>x. (ptable_lift t sa |` {x. ptable_rights t sa x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights t sa x}) (addrFromPPtr a)) |` S) a of None \<Rightarrow> underlying_memory (machine_state sa) a | Some x \<Rightarrow> x\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!