theory ArchIpc_IF

lemma dmo_loadWord_reads_respects[Ipc_IF_assms]:
  "reads_respects aag l (K (for_each_byte_of_word (\<lambda> x. aag_can_read_or_affect aag l x) p))
                  (do_machine_op (loadWord p))" apply (rule gen_asm_ev) apply (rule use_spec_ev) apply (rule spec_equiv_valid_hoist_guard) apply (rule do_machine_op_spec_reads_respects) apply (simp add: loadWord_def equiv_valid_def2 spec_equiv_valid_def) apply (rule_tac R'="\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p"
               and Q="\<top>\<top>" and Q'="\<top>\<top>" and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre) apply (rule_tac R'="(=)" and Q="\<lambda> r s. p && mask 2 = 0" and Q'="\<lambda> r s. p && mask 2 = 0"
                    and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre) apply (rule return_ev2) apply (rule_tac f="word_rcat" in arg_cong) apply (fastforce intro: is_aligned_no_wrap' word_plus_mono_right
                               simp: is_aligned_mask for_each_byte_of_word_def word_size_def)  (* slow *)
             apply (rule assert_ev2[OF refl]) apply (rule assert_wp)+ apply simp+ apply (clarsimp simp: equiv_valid_2_def in_monad for_each_byte_of_word_def) apply (fastforce elim: equiv_forD orthD1 simp: ptr_range_def add.commute) apply (wp wp_post_taut loadWord_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (for_each_byte_of_word (aag_can_read_or_affect aag l) p)) (do_machine_op (loadWord p)) proof (prove)
goal (1 subgoal):
 1. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (loadWord p)) proof (prove)
goal (1 subgoal):
 1. \<And>st. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (loadWord p)) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (loadWord p)) proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) (loadWord p)
 2. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (do m <- gets underlying_memory;
y <- assert (p && mask 2 = 0);
return (word_rcat [m (p + 3), m (p + 2), m (p + 1), m p])
od)
 2. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> equiv_valid_2 (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (\<lambda>_. True) (do y <- assert (p && mask 2 = 0);
return (word_rcat [rv (p + 3), rv (p + 2), rv (p + 1), rv p])
od) (do y <- assert (p && mask 2 = 0);
return (word_rcat [rv' (p + 3), rv' (p + 2), rv' (p + 1), rv' p])
od)
 2. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 3. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 6. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
 7. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; rva = rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>s. p && mask 2 = 0) (\<lambda>s. p && mask 2 = 0) (return (word_rcat [rv (p + 3), rv (p + 2), rv (p + 1), rv p])) (return (word_rcat [rv' (p + 3), rv' (p + 2), rv' (p + 1), rv' p]))
 2. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 3. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 rv rv' s
 7. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 8. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a s t. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; rva = rv'a; p && mask 2 = 0; p && mask 2 = 0; equiv_machine_state (aag_can_read aag) s t; equiv_machine_state (aag_can_affect aag l) s t\<rbrakk> \<Longrightarrow> word_rcat [rv (p + 3), rv (p + 2), rv (p + 1), rv p] = word_rcat [rv' (p + 3), rv' (p + 2), rv' (p + 1), rv' p]
 2. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 3. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 rv rv' s
 7. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 8. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a s t. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; rva = rv'a; p && mask 2 = 0; p && mask 2 = 0; equiv_machine_state (aag_can_read aag) s t; equiv_machine_state (aag_can_affect aag l) s t\<rbrakk> \<Longrightarrow> [rv (p + 3), rv (p + 2), rv (p + 1), rv p] = [rv' (p + 3), rv' (p + 2), rv' (p + 1), rv' p]
 2. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 3. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 rv rv' s
 7. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 8. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 2. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 3. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 rv rv' s
 6. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 7. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 8. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 10. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 2. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 3. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 rv rv' s
 6. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 7. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 8. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 10. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 2. \<And>rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 3. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 rv rv' s
 4. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 rv rv' s
 5. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 6. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 7. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 9. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
 10. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> (p && mask 2 = 0 \<longrightarrow> p && mask 2 = 0)
 2. \<And>rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> (p && mask 2 = 0 \<longrightarrow> p && mask 2 = 0)
 3. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 4. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 5. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 7. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
 8. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (6 subgoals):
 1. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 2. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 5. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
 6. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s t y. \<lbrakk>\<forall>y\<in>{p..p + (word_size - 1)}. aag_can_read_or_affect aag l y; 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; p \<le> y; y \<le> p + (word_size - 1)\<rbrakk> \<Longrightarrow> underlying_memory s y = underlying_memory t y
 2. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 5. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
 6. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (5 subgoals):
 1. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 2. for_each_byte_of_word (aag_can_read_or_affect aag l) p \<Longrightarrow> \<lbrace>?S'9\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S9 s
 4. \<And>s. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 s
 5. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read_or_affect aag l) p; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> loadWord p \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal:
No subgoals!