theory Ipc_R

lemma storeWordUser_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> storeWordUser a w \<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 pageBits = p && ~~ mask pageBits" 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> pageBits" by (simp add: pageBits_def) 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 storeWordUser_def
                     doMachineOp_def split_def) apply wp apply clarsimp apply (drule use_valid) apply (rule_tac x=p in storeWord_um_inv, simp+) apply (drule_tac x=p in spec) apply (erule disjE, simp_all) apply (erule conjE) apply (erule disjE, simp) apply (simp add: pointerInUserData_def word_size) apply (subgoal_tac "a && ~~ mask pageBits = p && ~~ mask pageBits", 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> storeWordUser a w \<lbrace>\<lambda>_. valid_machine_state'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> storeWordUser a w \<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 pageBits = p && ~~ mask pageBits proof (state)
goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask pageBits = p && ~~ mask pageBits proof (state)
goal (1 subgoal):
 1. \<And>l p sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask pageBits = p && ~~ mask pageBits 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 pageBits = p && ~~ mask pageBits 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 pageBits = p && ~~ mask pageBits 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 pageBits = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. 2 \<le> pageBits proof (state)
this:
2 \<le> pageBits

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

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

goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> storeWordUser a w \<lbrace>\<lambda>_. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> storeWordUser a w \<lbrace>\<lambda>_. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> do y <- stateAssert (pointerInUserData a) [];
ms <- gets ksMachineState;
p <- select_f (storeWord a w ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ s. \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0 \<Longrightarrow> pointerInUserData a s \<longrightarrow> (\<forall>x\<in>fst (storeWord a w (ksMachineState s)). \<forall>p. pointerInUserData p (s\<lparr>ksMachineState := snd x\<rparr>) \<or> pointerInDeviceData p (s\<lparr>ksMachineState := snd x\<rparr>) \<or> underlying_memory (ksMachineState (s\<lparr>ksMachineState := snd x\<rparr>)) p = 0) proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; pointerInUserData a s; ((), b) \<in> fst (storeWord a w (ksMachineState s)); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s b p. \<lbrakk>\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P14 s b p\<rbrace> storeWord a w \<lbrace>?Q14 s b p\<rbrace>
 2. \<And>s b p. \<lbrakk>\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> ?P14 s b p (ksMachineState s)
 3. \<And>s b p. \<lbrakk>\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; ?Q14 s b p () b\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; is_aligned a 2 \<and> (p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3) \<or> underlying_memory b p = underlying_memory (ksMachineState s) p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; is_aligned a 2 \<and> (p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3) \<or> underlying_memory b p = underlying_memory (ksMachineState s) p; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; is_aligned a 2 \<and> (p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3)\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; is_aligned a 2; p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>pointerInUserData a s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; is_aligned a 2; p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3; underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>typ_at' UserDataT (a && ~~ mask pageBits) s; \<not> typ_at' UserDataT (p && ~~ mask pageBits) s; underlying_memory b p \<noteq> 0; is_aligned a 2; p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3; underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>typ_at' UserDataT (a && ~~ mask pageBits) s; \<not> typ_at' UserDataT (p && ~~ mask pageBits) s; underlying_memory b p \<noteq> 0; is_aligned a 2; p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3; underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> a && ~~ mask pageBits = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>s b p. \<lbrakk>typ_at' UserDataT (a && ~~ mask pageBits) s; \<not> typ_at' UserDataT (p && ~~ mask pageBits) s; underlying_memory b p \<noteq> 0; a && mask 2 = 0; p = a \<or> p = a + 1 \<or> p = a + 2 \<or> p = a + 3; underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> a && ~~ mask pageBits = p && ~~ mask pageBits proof (prove)
goal (3 subgoals):
 1. \<And>s b p. \<lbrakk>typ_at' UserDataT (a && ~~ mask pageBits) s; \<not> typ_at' UserDataT (a + 1 && ~~ mask pageBits) s; underlying_memory b (a + 1) \<noteq> 0; a && mask 2 = 0; underlying_memory (ksMachineState s) (a + 1) = 0; p = a + 1\<rbrakk> \<Longrightarrow> a && ~~ mask pageBits = a + 1 && ~~ mask pageBits
 2. \<And>s b p. \<lbrakk>typ_at' UserDataT (a && ~~ mask pageBits) s; \<not> typ_at' UserDataT (a + 2 && ~~ mask pageBits) s; underlying_memory b (a + 2) \<noteq> 0; a && mask 2 = 0; underlying_memory (ksMachineState s) (a + 2) = 0; p = a + 2\<rbrakk> \<Longrightarrow> a && ~~ mask pageBits = a + 2 && ~~ mask pageBits
 3. \<And>s b p. \<lbrakk>typ_at' UserDataT (a && ~~ mask pageBits) s; \<not> typ_at' UserDataT (a + 3 && ~~ mask pageBits) s; underlying_memory b (a + 3) \<noteq> 0; a && mask 2 = 0; underlying_memory (ksMachineState s) (a + 3) = 0; p = a + 3\<rbrakk> \<Longrightarrow> a && ~~ mask pageBits = a + 3 && ~~ mask pageBits proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_machine_state'\<rbrace> storeWordUser a w \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>

goal:
No subgoals!