theory Untyped_DR

lemma clearMemory_corres_noop:
  "full_sz = 2 ^ sz \<Longrightarrow> is_aligned p sz \<Longrightarrow> 2 \<le> sz
    \<Longrightarrow> sz < word_bits
    \<Longrightarrow> dcorres dc \<top>
     (pspace_no_overlap {p .. p + 2 ^ sz - 1} and valid_objs and valid_etcbs)
     (return ())
     (do_machine_op (clearMemory p full_sz))" apply (simp add: clearMemory_def freeMemory_def[symmetric]
                   do_machine_op_bind empty_fail_freeMemory) apply (rule corres_guard_imp) apply (rule corres_add_noop_lhs) apply (rule corres_split_nor) apply (rule freeMemory_dcorres; simp) apply (rule dcorres_machine_op_noop) apply (wp | simp)+ apply (clarsimp simp: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) (return ()) (do_machine_op (clearMemory p full_sz)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) (return ()) (do rv <- do_machine_op (freeMemory p sz);
do_machine_op (cleanCacheRange_RAM p (p + 2 ^ sz - 1) (addrFromPPtr p))
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc ?Q1 ?Q'1 (return ()) (do rv <- do_machine_op (freeMemory p sz);
do_machine_op (cleanCacheRange_RAM p (p + 2 ^ sz - 1) (addrFromPPtr p))
od)
 2. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; True\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc ?Q1 ?Q'1 (do _ <- return ();
return ()
od) (do rv <- do_machine_op (freeMemory p sz);
do_machine_op (cleanCacheRange_RAM p (p + 2 ^ sz - 1) (addrFromPPtr p))
od)
 2. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; True\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc ?P7 ?P'7 (return ()) (do_machine_op (freeMemory p sz))
 2. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc ?R7 ?R'7 (return ()) (do_machine_op (cleanCacheRange_RAM p (p + 2 ^ sz - 1) (addrFromPPtr p)))
 3. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> return () \<lbrace>\<lambda>x. ?R7\<rbrace>
 4. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> do_machine_op (freeMemory p sz) \<lbrace>\<lambda>x. ?R'7\<rbrace>
 5. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; True\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> dcorres dc ?R7 ?R'7 (return ()) (do_machine_op (cleanCacheRange_RAM p (p + 2 ^ sz - 1) (addrFromPPtr p)))
 2. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> return () \<lbrace>\<lambda>x. ?R7\<rbrace>
 3. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> do_machine_op (freeMemory p sz) \<lbrace>\<lambda>x. ?R'7\<rbrace>
 4. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 5. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pspace_no_overlap (up_aligned_area p sz) and valid_objs and valid_etcbs and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<And>m. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCacheRange_RAM p (p + 2 ^ sz - 1) (addrFromPPtr p) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> return () \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> do_machine_op (freeMemory p sz) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 5. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; (pspace_no_overlap {p..p + 2 ^ sz - 1} and valid_objs and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pspace_no_overlap (up_aligned_area p sz) and valid_objs and valid_etcbs and ?Q'7) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>full_sz = 2 ^ sz; is_aligned p sz; 2 \<le> sz; sz < word_bits; pspace_no_overlap {p..p + 2 ^ sz - 1} s \<and> valid_objs s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> pspace_no_overlap {p..p + (2 ^ sz - 1)} s proof (prove)
goal:
No subgoals!