theory ArchIpc_AI

lemma store_word_offs_vms[wp, Ipc_AI_assms]:
  "\<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" proof - have aligned_offset_ignore:
    "\<And>(l::word32) (p::word32) sz. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow>
       p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)" proof - fix l p sz assume al: "(p::word32) && mask 2 = 0" assume "(l::word32) < 4" hence less: "l<2^2" by simp have le: "2 \<le> pageBitsForSize sz" by (case_tac sz, simp_all) show "?thesis l p sz" by (rule is_aligned_add_helper[simplified is_aligned_mask,
          THEN conjunct2, THEN mask_out_first_mask_some,
          where n=2, OF al less le]) qed show ?thesis apply (simp add: valid_machine_state_def store_word_offs_def
                     do_machine_op_def split_def) apply wp apply clarsimp apply (drule_tac use_valid) apply (rule_tac x=p in storeWord_um_inv, simp+) apply (drule_tac x=p in spec) apply (erule disjE, simp) apply (erule disjE, simp_all) apply (erule conjE) apply (erule disjE, simp) apply (simp add: in_user_frame_def word_size_def) apply (erule exEI) apply (subgoal_tac "(ptr + of_nat offs * 4) && ~~ mask (pageBitsForSize x) =
                        p && ~~ mask (pageBitsForSize x)", simp) apply (simp only: is_aligned_mask[of _ 2]) apply (elim disjE, simp_all) apply (rule aligned_offset_ignore[symmetric], simp+)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
this:
p && mask 2 = 0

goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
this:
l < 4

goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (prove)
using this:
l < 4

goal (1 subgoal):
 1. l < 2\<^sup>2 proof (state)
this:
l < 2\<^sup>2

goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. 2 \<le> pageBitsForSize sz proof (state)
this:
2 \<le> pageBitsForSize sz

goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
this:
p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)

goal:
No subgoals! proof (state)
this:
\<lbrakk>?l < 4; ?p && mask 2 = 0\<rbrakk> \<Longrightarrow> ?p + ?l && ~~ mask (pageBitsForSize ?sz) = ?p && ~~ mask (pageBitsForSize ?sz)

goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrace> do s <- get;
y <- assert (in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s);
ms <- gets machine_state;
p <- select_f (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0 \<Longrightarrow> in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s \<longrightarrow> (\<forall>x\<in>fst (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v (machine_state s)). \<forall>p. in_user_frame p (s\<lparr>machine_state := snd x\<rparr>) \<or> underlying_memory (machine_state (s\<lparr>machine_state := snd x\<rparr>)) p = 0) proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; ((), b) \<in> fst (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v (machine_state s)); underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (3 subgoals):
 1. \<And>s b p. \<lbrakk>\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P14 s b p\<rbrace> storeWord (ptr + word_of_nat offs * word_of_nat word_size) v \<lbrace>?Q14 s b p\<rbrace>
 2. \<And>s b p. \<lbrakk>\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> ?P14 s b p (machine_state s)
 3. \<And>s b p. \<lbrakk>\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; ?Q14 s b p () b\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; is_aligned (ptr + word_of_nat offs * word_of_nat word_size) 2 \<and> (p = ptr + word_of_nat offs * word_of_nat word_size \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 1 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 2 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 3) \<or> underlying_memory b p = underlying_memory (machine_state s) p\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; is_aligned (ptr + word_of_nat offs * word_of_nat word_size) 2 \<and> (p = ptr + word_of_nat offs * word_of_nat word_size \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 1 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 2 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 3) \<or> underlying_memory b p = underlying_memory (machine_state s) p; in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; is_aligned (ptr + word_of_nat offs * word_of_nat word_size) 2 \<and> (p = ptr + word_of_nat offs * word_of_nat word_size \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 1 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 2 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 3) \<or> underlying_memory b p = underlying_memory (machine_state s) p; underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; is_aligned (ptr + word_of_nat offs * word_of_nat word_size) 2 \<and> (p = ptr + word_of_nat offs * word_of_nat word_size \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 1 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 2 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 3)\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; is_aligned (ptr + word_of_nat offs * word_of_nat word_size) 2; p = ptr + word_of_nat offs * word_of_nat word_size \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 1 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 2 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 3\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; is_aligned (ptr + word_of_nat offs * word_of_nat word_size) 2; p = ptr + word_of_nat offs * word_of_nat word_size + 1 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 2 \<or> p = ptr + word_of_nat offs * word_of_nat word_size + 3\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>\<exists>sz. typ_at (AArch (AUserData sz)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize sz)) s; underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; is_aligned (ptr + word_of_nat offs * 4) 2; p = ptr + word_of_nat offs * 4 + 1 \<or> p = ptr + word_of_nat offs * 4 + 2 \<or> p = ptr + word_of_nat offs * 4 + 3\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>s b p x. \<lbrakk>underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; is_aligned (ptr + word_of_nat offs * 4) 2; p = ptr + word_of_nat offs * 4 + 1 \<or> p = ptr + word_of_nat offs * 4 + 2 \<or> p = ptr + word_of_nat offs * 4 + 3; typ_at (AArch (AUserData x)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData x)) (p && ~~ mask (pageBitsForSize x)) s proof (prove)
goal (1 subgoal):
 1. \<And>s b p x. \<lbrakk>underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; is_aligned (ptr + word_of_nat offs * 4) 2; p = ptr + word_of_nat offs * 4 + 1 \<or> p = ptr + word_of_nat offs * 4 + 2 \<or> p = ptr + word_of_nat offs * 4 + 3; typ_at (AArch (AUserData x)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x)) s\<rbrakk> \<Longrightarrow> ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x) = p && ~~ mask (pageBitsForSize x) proof (prove)
goal (1 subgoal):
 1. \<And>s b p x. \<lbrakk>underlying_memory b p \<noteq> 0; underlying_memory (machine_state s) p = 0; ptr + word_of_nat offs * 4 && mask 2 = 0; p = ptr + word_of_nat offs * 4 + 1 \<or> p = ptr + word_of_nat offs * 4 + 2 \<or> p = ptr + word_of_nat offs * 4 + 3; typ_at (AArch (AUserData x)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x)) s\<rbrakk> \<Longrightarrow> ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x) = p && ~~ mask (pageBitsForSize x) proof (prove)
goal (3 subgoals):
 1. \<And>s b p x. \<lbrakk>underlying_memory b (ptr + word_of_nat offs * 4 + 1) \<noteq> 0; underlying_memory (machine_state s) (ptr + word_of_nat offs * 4 + 1) = 0; ptr + word_of_nat offs * 4 && mask 2 = 0; typ_at (AArch (AUserData x)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x)) s; p = ptr + word_of_nat offs * 4 + 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x) = ptr + word_of_nat offs * 4 + 1 && ~~ mask (pageBitsForSize x)
 2. \<And>s b p x. \<lbrakk>underlying_memory b (ptr + word_of_nat offs * 4 + 2) \<noteq> 0; underlying_memory (machine_state s) (ptr + word_of_nat offs * 4 + 2) = 0; ptr + word_of_nat offs * 4 && mask 2 = 0; typ_at (AArch (AUserData x)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x)) s; p = ptr + word_of_nat offs * 4 + 2\<rbrakk> \<Longrightarrow> ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x) = ptr + word_of_nat offs * 4 + 2 && ~~ mask (pageBitsForSize x)
 3. \<And>s b p x. \<lbrakk>underlying_memory b (ptr + word_of_nat offs * 4 + 3) \<noteq> 0; underlying_memory (machine_state s) (ptr + word_of_nat offs * 4 + 3) = 0; ptr + word_of_nat offs * 4 && mask 2 = 0; typ_at (AArch (AUserData x)) (ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x)) s; p = ptr + word_of_nat offs * 4 + 3\<rbrakk> \<Longrightarrow> ptr + word_of_nat offs * 4 && ~~ mask (pageBitsForSize x) = ptr + word_of_nat offs * 4 + 3 && ~~ mask (pageBitsForSize x) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace>

goal:
No subgoals!