theory ArchArch_IF

lemma store_word_offs_reads_respects[Arch_IF_assms]:
  "reads_respects aag l \<top> (store_word_offs ptr offs v)" apply (simp add: store_word_offs_def) apply (rule equiv_valid_get_assert) apply (simp add: storeWord_def) apply (simp add: do_machine_op_bind) apply wp apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects) apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def in_monad) apply (fastforce intro: equiv_forI elim: equiv_forE) apply (rule use_spec_ev do_machine_op_spec_reads_respects assert_ev2
            | simp add: spec_equiv_valid_def | wp modify_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (store_word_offs ptr offs v) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do s <- get;
y <- assert (in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s);
do_machine_op (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v)
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v)) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (do y <- assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)))
od)) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do rv <- do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0));
do_machine_op (modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0))))
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. reads_respects aag l (?Q2 rv) (do_machine_op (modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)))))
 2. reads_respects aag l ?P'2 (do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)))
 3. \<lbrace>?P''2\<rbrace> do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)) \<lbrace>?Q2\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (4 subgoals):
 1. \<And>rv st. spec_reads_respects st aag l (?Q2 rv) (do_machine_op (modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)))))
 2. reads_respects aag l ?P'2 (do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)))
 3. \<lbrace>?P''2\<rbrace> do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)) \<lbrace>?Q2\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv st. equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) (modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0))))
 2. \<And>rv st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0))) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>
 3. reads_respects aag l ?P'2 (do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)))
 4. \<lbrace>?P''2\<rbrace> do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)) \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (5 subgoals):
 1. \<And>s t. \<lbrakk>equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag) underlying_memory (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)) s) (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)) t) \<and> equiv_for (aag_can_read aag) device_state (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)) s) (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)) t) \<and> equiv_machine_state (aag_can_affect aag l) (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)) s) (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0)) t)
 2. \<And>rv st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0))) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>
 3. reads_respects aag l ?P'2 (do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)))
 4. \<lbrace>?P''2\<rbrace> do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)) \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (4 subgoals):
 1. \<And>rv st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (underlying_memory_update (\<lambda>m. m(ptr + word_of_nat offs * word_of_nat word_size := word_rsplit v ! 3, ptr + word_of_nat offs * word_of_nat word_size + 1 := word_rsplit v ! 2, ptr + word_of_nat offs * word_of_nat word_size + 2 := word_rsplit v ! Suc 0, ptr + word_of_nat offs * word_of_nat word_size + 3 := word_rsplit v ! 0))) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>
 2. reads_respects aag l ?P'2 (do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)))
 3. \<lbrace>?P''2\<rbrace> do_machine_op (assert (ptr + word_of_nat offs * word_of_nat word_size && mask 2 = 0)) \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal:
No subgoals!