theory ArchRetype_AC

lemma dmo_freeMemory_respects[Retype_AC_assms]:
  "\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and>
                              (\<forall>p \<in> ptr_range ptr bits. is_subject aag p))\<rbrace>
   do_machine_op (freeMemory ptr bits)
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding do_machine_op_def freeMemory_def apply (simp add: split_def) apply wp apply clarsimp apply (erule use_valid) apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch) apply simp apply (clarsimp simp: word_size_def word_bits_def word_size_bits_def
                         upto_enum_step_shift_red[where us=2, simplified]) apply (erule bspec) apply (erule set_mp [rotated]) apply (rule ptr_range_subset) apply simp apply (simp add: is_aligned_mult_triv2 [where n = 2, simplified]) apply assumption apply (erule word_less_power_trans_ofnat [where k = 2, simplified]) apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p))\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p))\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p))\<rbrace> do ms <- gets machine_state;
p <- select_f (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p))) s \<Longrightarrow> \<forall>x\<in>fst (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] (machine_state s)). integrity aag X st (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] (machine_state s)); integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s b\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> ?P11 s b (machine_state s) proof (prove)
goal (2 subgoals):
 1. \<And>s b x sa. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]; integrity aag X st (s\<lparr>machine_state := sa\<rparr>)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := sa\<rparr>) \<and> (is_aligned x 2 \<longrightarrow> (\<forall>p'\<in>ptr_range x 2. is_subject aag p'))
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x sa. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]; integrity aag X st (s\<lparr>machine_state := sa\<rparr>)\<rbrakk> \<Longrightarrow> is_aligned x 2 \<longrightarrow> (\<forall>p'\<in>ptr_range x 2. is_subject aag p')
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2; p' \<in> ptr_range (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> is_subject aag p'
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2; p' \<in> ptr_range (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> p' \<in> ptr_range ptr bits
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> ptr_range (ptr + word_of_nat xa * 4) 2 \<subseteq> ptr_range ptr bits
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> is_aligned ptr bits
 2. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat xa * 4) 2
 3. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> 2 \<le> bits
 4. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> word_of_nat xa * 4 < 2 ^ bits
 5. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat xa * 4) 2
 2. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> 2 \<le> bits
 3. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> word_of_nat xa * 4 < 2 ^ bits
 4. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> 2 \<le> bits
 2. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> word_of_nat xa * 4 < 2 ^ bits
 3. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> word_of_nat xa * 4 < 2 ^ bits
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> 2 \<le> bits
 2. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sa xa p'. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < 32; 2 \<le> bits; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); is_aligned (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>integrity aag X st s; is_aligned ptr bits; bits < word_bits; word_size_bits \<le> bits; \<forall>p\<in>ptr_range ptr bits. is_subject aag p\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal:
No subgoals!