theory ArchInfoFlow_IF

lemma dmo_loadWord_rev[InfoFlow_IF_assms]:
  "reads_equiv_valid_inv A aag (K (for_each_byte_of_word (aag_can_read aag) 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_rev) 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 (erule equiv_forD) apply fastforce apply (wp wp_post_taut loadWord_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (for_each_byte_of_word (aag_can_read aag) p)) (do_machine_op (loadWord p)) proof (prove)
goal (1 subgoal):
 1. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (do_machine_op (loadWord p)) proof (prove)
goal (1 subgoal):
 1. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> reads_spec_equiv_valid_inv st A aag (\<lambda>_. True) (do_machine_op (loadWord p)) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> reads_spec_equiv_valid_inv st A aag (\<lambda>_. True) (do_machine_op (loadWord p)) proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv (machine_state st) (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>_. True) (loadWord p)
 2. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_2 (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>_ _. True) (=) ((=) (machine_state st)) (\<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) (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 aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (\<lambda>_ _. True) (=) (\<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. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 3. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 6. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 7. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>st rv rv' rva rv'a. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (\<lambda>_ _. True) (=) (\<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>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 3. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 5. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 st rv rv' s
 6. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 st rv rv' s
 7. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 8. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>st rv rv' rva rv'a s t. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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; True\<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>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 3. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 5. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 st rv rv' s
 6. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 st rv rv' s
 7. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 8. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>st rv rv' rva rv'a s t. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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; True\<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>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 3. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 5. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 st rv rv' s
 6. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 st rv rv' s
 7. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 8. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 2. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 3. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 st rv rv' s
 5. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 st rv rv' s
 6. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 7. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 10. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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)) (\<lambda>_ _. True) (=) (\<lambda>_. True) (assert (p && mask 2 = 0))
 2. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 3. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 4. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 st rv rv' s
 5. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 st rv rv' s
 6. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 7. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 10. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 2. \<And>st rv rv'. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p\<rbrakk> \<Longrightarrow> \<lbrace>?S'11 st rv rv'\<rbrace> assert (p && mask 2 = 0) \<lbrace>\<lambda>r s. p && mask 2 = 0\<rbrace>
 3. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S11 st rv rv' s
 4. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; for_each_byte_of_word (\<lambda>y. rv y = rv' y) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'11 st rv rv' s
 5. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 6. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 9. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 10. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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>st rv rv' s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) 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. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 4. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 7. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 8. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>rv rv'. for_each_byte_of_word (\<lambda>y. rv y = rv' y) p) (\<lambda>_. True) (gets underlying_memory)
 2. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 5. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 6. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s t y. \<lbrakk>\<forall>y\<in>{p..p + (word_size - 1)}. aag_can_read aag y; equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; p \<le> y; y \<le> p + (word_size - 1)\<rbrakk> \<Longrightarrow> underlying_memory s y = underlying_memory t y
 2. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 5. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 6. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s t y. \<lbrakk>\<forall>y\<in>{p..p + (word_size - 1)}. aag_can_read aag y; equiv_for (aag_can_read aag) device_state s t; p \<le> y; y \<le> p + (word_size - 1)\<rbrakk> \<Longrightarrow> aag_can_read aag y
 2. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 5. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 6. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>st. for_each_byte_of_word (aag_can_read aag) p \<Longrightarrow> \<lbrace>?S'9 st\<rbrace> gets underlying_memory \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; machine_state st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 st s
 4. \<And>st s. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 st s
 5. \<And>st P. \<lbrakk>for_each_byte_of_word (aag_can_read aag) p; True\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord p \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!