theory Retype_C

lemma heap_to_device_data_disj_mdf:
  assumes rc: "range_cover ptr sz (gbits + pageBits) n"
  and ko_at: "ksPSpace \<sigma> a = Some obj"
  and obj_size: "objBitsKO obj = pageBits"
  and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>"
  and pno: "pspace_no_overlap' ptr sz \<sigma>"
  and sz: "gbits + pageBits \<le> sz"
  and szb: "sz < word_bits"
  shows "(heap_to_device_data (ksPSpace \<sigma>)
          (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a)
          = (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a)" proof - from sz have "2 \<le> sz" by (simp add: objBits_simps pageBits_def) hence sz2: "2 ^ (sz - 2) * 4 = (2 :: nat) ^ sz" apply (subgoal_tac "(4 :: nat) = 2 ^ 2") apply (erule ssubst) apply (subst power_add [symmetric]) apply (rule arg_cong [where f = "\<lambda>n. 2 ^ n"]) apply simp apply simp done have p2dist: "n * (2::nat) ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ pageBits" (is "?lhs = ?rhs") by (simp add: monoid_mult_class.power_add) show ?thesis apply (simp add: heap_to_device_data_def) apply (case_tac "n = 0") apply simp apply (subst map_option_byte_to_word_heap) apply (erule range_cover_nca_neg[OF _ _ rc]) using range_cover_intvl[OF rc] apply (clarsimp simp add: heap_to_user_data_def Let_def
       byte_to_word_heap_def[abs_def] map_comp_Some_iff projectKOs) apply (cut_tac pspace_no_overlapD' [OF ko_at pno]) apply (subst (asm) upto_intvl_eq [symmetric]) apply (rule pspace_alignedD' [OF ko_at pal]) apply (simp add: obj_size p2dist) apply (drule_tac B' = "{ptr..ptr + (of_nat n * 2 ^ (gbits + pageBits) - 1)}" in disjoint_subset2[rotated]) apply (clarsimp simp: p2dist ) apply (rule range_cover_bound_weak) apply simp apply (rule rc) apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a proof (state)
goal (1 subgoal):
 1. heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a proof (chain)
picking this:
gbits + pageBits \<le> sz proof (prove)
using this:
gbits + pageBits \<le> sz

goal (1 subgoal):
 1. 2 \<le> sz proof (state)
this:
2 \<le> sz

goal (1 subgoal):
 1. heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a proof (prove)
using this:
2 \<le> sz

goal (1 subgoal):
 1. 2 ^ (sz - 2) * 4 = 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 \<le> sz; 4 = 2\<^sup>2\<rbrakk> \<Longrightarrow> 2 ^ (sz - 2) * 4 = 2 ^ sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> sz \<Longrightarrow> 2 ^ (sz - 2) * 2\<^sup>2 = 2 ^ sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> sz \<Longrightarrow> 2 ^ (sz - 2 + 2) = 2 ^ sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 \<le> sz \<Longrightarrow> sz - 2 + 2 = sz
 2. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal (1 subgoal):
 1. 2 \<le> sz \<Longrightarrow> 4 = 2\<^sup>2 proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ (sz - 2) * 4 = 2 ^ sz

goal (1 subgoal):
 1. heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a proof (prove)
goal (1 subgoal):
 1. n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ pageBits proof (state)
this:
n * 2 ^ (gbits + pageBits) = n * 2 ^ gbits * 2 ^ pageBits

goal (1 subgoal):
 1. heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a proof (prove)
goal (1 subgoal):
 1. heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a proof (prove)
goal (1 subgoal):
 1. map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a)
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<And>_ off x. \<lbrakk>n \<noteq> 0; x < 4\<rbrakk> \<Longrightarrow> a + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<And>_ off x. n \<noteq> 0 \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}

goal (2 subgoals):
 1. \<And>_ off x. n \<noteq> 0 \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..a + 2 ^ objBitsKO obj - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}\<rbrakk> \<Longrightarrow> is_aligned a (objBitsKO obj)
 2. \<lbrakk>0 < n; {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ objBitsKO obj} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 3. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ (gbits + pageBits)} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ objBitsKO obj} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ pageBits} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}\<rbrakk> \<Longrightarrow> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 3. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; ptr \<le> ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 3. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; ptr \<le> ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; ptr \<le> ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)\<rbrakk> \<Longrightarrow> range_cover ptr sz (gbits + pageBits) n
 3. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 4. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; ptr \<le> ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)\<rbrakk> \<Longrightarrow> range_cover ptr sz (gbits + pageBits) n
 2. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 3. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; {ptr..+n * 2 ^ gbits * 2 ^ pageBits} = {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}; {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}\<rbrakk> \<Longrightarrow> {a..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}
 2. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) = map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) a) (map_to_user_data_device (ksPSpace \<sigma>) a) proof (prove)
goal:
No subgoals! proof (state)
this:
heap_to_device_data (ksPSpace \<sigma>) (\<lambda>x. if x \<in> {ptr..+n * 2 ^ (gbits + pageBits)} then 0 else underlying_memory (ksMachineState \<sigma>) x) a = heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a

goal:
No subgoals!