theory ArchRetype_AC

lemma freeMemory_vms:
  "valid_machine_state s \<Longrightarrow>
   \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). valid_machine_state (s\<lparr>machine_state := snd x\<rparr>)" apply (clarsimp simp: valid_machine_state_def disj_commute[of "in_user_frame p s" for p s]) apply (drule_tac x=p in spec, simp) apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
                in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all) apply (simp add: freeMemory_def machine_op_lift_def machine_rest_lift_def split_def) apply (wp hoare_drop_imps | simp | wp mapM_x_wp_inv)+ apply (simp add: storeWord_def | wp)+ apply (simp add: word_rsplit_0 word_bits_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state s \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). valid_machine_state (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>b p. \<lbrakk>\<forall>p. underlying_memory (machine_state s) p = 0 \<or> in_user_frame p s; ((), b) \<in> fst (freeMemory ptr bits (machine_state s)); \<not> in_user_frame p s\<rbrakk> \<Longrightarrow> underlying_memory b p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>b p. \<lbrakk>((), b) \<in> fst (freeMemory ptr bits (machine_state s)); \<not> in_user_frame p s; underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> underlying_memory b p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<not> in_user_frame p s; underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = 0\<rbrace> freeMemory ptr bits \<lbrace>\<lambda>_ m'. underlying_memory m' p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<not> in_user_frame p s; underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = 0\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<lbrace>\<lambda>_ m'. underlying_memory m' p = 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>p x. \<lbrakk>\<not> in_user_frame p s; underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = 0\<rbrace> storeWord x 0 \<lbrace>\<lambda>_ m'. underlying_memory m' p = 0\<rbrace>
 2. \<And>p sa. \<lbrakk>\<not> in_user_frame p s; underlying_memory (machine_state s) p = 0; underlying_memory sa p = 0\<rbrakk> \<Longrightarrow> underlying_memory sa p = 0 proof (prove)
goal (2 subgoals):
 1. \<And>p x sa. \<lbrakk>\<not> in_user_frame p s; underlying_memory (machine_state s) p = 0; underlying_memory sa p = 0\<rbrakk> \<Longrightarrow> (p = x \<longrightarrow> x && mask 2 = 0 \<longrightarrow> word_rsplit 0 ! 3 = 0) \<and> (p \<noteq> x \<longrightarrow> (p = x + 1 \<longrightarrow> x && mask 2 = 0 \<longrightarrow> word_rsplit 0 ! 2 = 0) \<and> (p \<noteq> x + 1 \<longrightarrow> (p = x + 2 \<longrightarrow> x && mask 2 = 0 \<longrightarrow> word_rsplit 0 ! Suc 0 = 0) \<and> (p \<noteq> x + 2 \<longrightarrow> p = x + 3 \<longrightarrow> x && mask 2 = 0 \<longrightarrow> word_rsplit 0 ! 0 = 0)))
 2. \<And>p sa. \<lbrakk>\<not> in_user_frame p s; underlying_memory (machine_state s) p = 0; underlying_memory sa p = 0\<rbrakk> \<Longrightarrow> underlying_memory sa p = 0 proof (prove)
goal:
No subgoals!