theory ArchNoninterference

lemma dmo_storeWord_reads_respects_g[Noninterference_assms, wp]:
  "reads_respects_g aag l \<top> (do_machine_op (storeWord ptr w))" apply (clarsimp simp: do_machine_op_def bind_def gets_def get_def return_def fail_def
                        select_f_def storeWord_def assert_def simpler_modify_def) apply (fold simpler_modify_def) apply (intro impI conjI) apply (rule ev_modify) apply (rule conjI) apply (fastforce simp: reads_equiv_g_def globals_equiv_def reads_equiv_def2 states_equiv_for_def
                           equiv_for_def equiv_asids_def equiv_asid_def silc_dom_equiv_def) apply (rule affects_equiv_machine_state_update, assumption) apply (fastforce simp: equiv_for_def affects_equiv_def states_equiv_for_def) apply (simp add: equiv_valid_def2 equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (do_machine_op (storeWord ptr w)) proof (prove)
goal (1 subgoal):
 1. (ptr && mask 2 = 0 \<longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({((), s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>)}, False))) \<and> (ptr && mask 2 \<noteq> 0 \<longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True))) proof (prove)
goal (1 subgoal):
 1. (ptr && mask 2 = 0 \<longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>))) \<and> (ptr && mask 2 \<noteq> 0 \<longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True))) proof (prove)
goal (2 subgoals):
 1. ptr && mask 2 = 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>))
 2. ptr && mask 2 \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True)) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>ptr && mask 2 = 0; True; True; affects_equiv aag l s t; reads_equiv_g aag s t\<rbrakk> \<Longrightarrow> reads_equiv_g aag (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>) (t\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state t)\<rparr>) \<and> affects_equiv aag l (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>) (t\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state t)\<rparr>)
 2. ptr && mask 2 \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True)) proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>ptr && mask 2 = 0; True; True; affects_equiv aag l s t; reads_equiv_g aag s t\<rbrakk> \<Longrightarrow> reads_equiv_g aag (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>) (t\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state t)\<rparr>)
 2. \<And>s t. \<lbrakk>ptr && mask 2 = 0; True; True; affects_equiv aag l s t; reads_equiv_g aag s t\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>) (t\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state t)\<rparr>)
 3. ptr && mask 2 \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True)) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>ptr && mask 2 = 0; True; True; affects_equiv aag l s t; reads_equiv_g aag s t\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)\<rparr>) (t\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state t)\<rparr>)
 2. ptr && mask 2 \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True)) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>ptr && mask 2 = 0; True; True; affects_equiv aag l s t; reads_equiv_g aag s t\<rbrakk> \<Longrightarrow> equiv_machine_state (aag_can_affect aag l) (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state s)) (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (machine_state t))
 2. ptr && mask 2 \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True)) proof (prove)
goal (1 subgoal):
 1. ptr && mask 2 \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (\<lambda>s. ({}, True)) proof (prove)
goal:
No subgoals!