theory ArchRetype_AC

lemma dmo_clearMemory_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. aag_has_auth_to aag Write p))\<rbrace>
   do_machine_op (clearMemory ptr (2 ^ bits))
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding do_machine_op_def clearMemory_def apply (simp add: split_def cleanCacheRange_PoU_def) apply wp apply clarsimp apply (erule use_valid) apply wp apply (simp add: cleanCacheRange_RAM_def cleanCacheRange_PoC_def cacheRangeOp_def cleanL2Range_def
                     cleanByVA_def split_def dsb_def) apply (wp mol_respects mapM_x_wp' storeWord_respects)+ apply (simp add: word_size_bits_def) apply (clarsimp simp: word_size_def word_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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))\<rbrace> do_machine_op (clearMemory ptr (2 ^ 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f ((do mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat (2 ^ bits) - 1];
cleanCacheRange_RAM ptr (ptr + word_of_nat (2 ^ bits) - 1) (addrFromPPtr ptr)
od) 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))\<rbrace> do ms <- gets machine_state;
p <- select_f ((do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od) 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<Longrightarrow> \<forall>x\<in>fst ((do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od) (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 ((do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od) (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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s b\<rbrace> do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od \<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> ?P11 s b (machine_state s) proof (prove)
goal (3 subgoals):
 1. \<And>s b x. \<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s b x\<rbrace> cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr) \<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s b\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<lbrace>?B15 s b\<rbrace>
 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> ?P11 s b (machine_state s) proof (prove)
goal (3 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s b ()\<rbrace> do y <- mapM_x (\<lambda>p. machine_op_lift (cleanByVA_impl (fst p) (snd p))) (zip [lineStart ptr , lineStart ptr + word_of_nat cacheLine .e. lineStart (ptr + 2 ^ bits - 1)] [lineStart (addrFromPPtr ptr) , lineStart (addrFromPPtr ptr) + word_of_nat cacheLine .e. lineStart (addrFromPPtr ptr + (2 ^ bits - 1))]);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr ptr) (addrFromPPtr ptr + (2 ^ bits - 1)))
od \<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s b\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<lbrace>?B15 s b\<rbrace>
 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag; 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> (\<forall>p'\<in>ptr_range x word_size_bits. (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag)
 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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; 2 \<le> bits; \<forall>p\<in>ptr_range ptr bits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]; integrity aag X st (s\<lparr>machine_state := sa\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>p'\<in>ptr_range x 2. (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag
 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag; integrity aag X st (s\<lparr>machine_state := sa\<rparr>); xa < 2 ^ (bits - 2); p' \<in> ptr_range (ptr + word_of_nat xa * 4) 2\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag
 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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); 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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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)\<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)\<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)\<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)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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)\<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)\<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)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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)\<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)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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>)\<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>)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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>)\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<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. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal:
No subgoals!