theory Retype_C

lemma pspace_no_overlap_underlying_zero:
  "pspace_no_overlap' ptr sz \<sigma>
    \<Longrightarrow> valid_machine_state' \<sigma>
    \<Longrightarrow> x \<in> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}
    \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0" using mask_in_range[where ptr'=x and bits=pageBits and ptr="x && ~~ mask pageBits"] apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=x in spec, clarsimp simp: pointerInUserData_def) apply (clarsimp simp: typ_at'_def ko_wp_at'_def koTypeOf_eq_UserDataT) apply (case_tac "pointerInDeviceData x \<sigma>") apply (clarsimp simp: pointerInDeviceData_def
                         ko_wp_at'_def obj_at'_def projectKOs
                  dest!: device_data_at_ko) apply (drule(1) pspace_no_overlapD') apply (drule_tac x=x in eqset_imp_iff) apply (simp add: objBits_simps) apply clarsimp apply (drule(1) pspace_no_overlapD') apply (drule_tac x=x in eqset_imp_iff, simp) apply (simp add: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; valid_machine_state' \<sigma>; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
using this:
is_aligned (x && ~~ mask pageBits) pageBits \<Longrightarrow> (x && ~~ mask pageBits = x && ~~ mask pageBits) = (x \<in> {x && ~~ mask pageBits..(x && ~~ mask pageBits) + 2 ^ pageBits - 1})

goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; valid_machine_state' \<sigma>; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; \<forall>p. pointerInUserData p \<sigma> \<or> pointerInDeviceData p \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) p = 0; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; typ_at' UserDataT (x && ~~ mask pageBits) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0; pointerInDeviceData x \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0
 2. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0; \<not> pointerInDeviceData x \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserDataDevice; is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserDataDevice); ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserDataDevice) \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0
 2. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0; \<not> pointerInDeviceData x \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserDataDevice); ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserDataDevice) \<sigma>; {x && ~~ mask pageBits..(x && ~~ mask pageBits) + 2 ^ objBitsKO KOUserDataDevice - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0
 2. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0; \<not> pointerInDeviceData x \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserDataDevice); ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserDataDevice) \<sigma>; (x \<in> {x && ~~ mask pageBits..(x && ~~ mask pageBits) + 2 ^ objBitsKO KOUserDataDevice - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}) = (x \<in> {})\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0
 2. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0; \<not> pointerInDeviceData x \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData \<and> is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData) \<and> ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma> \<or> pointerInDeviceData x \<sigma> \<or> underlying_memory (ksMachineState \<sigma>) x = 0; \<not> pointerInDeviceData x \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; \<not> pointerInDeviceData x \<sigma>; ksPSpace \<sigma> (x && ~~ mask pageBits) = Some KOUserData; is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData); ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma>\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; \<not> pointerInDeviceData x \<sigma>; is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData); ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma>; {x && ~~ mask pageBits..(x && ~~ mask pageBits) + 2 ^ objBitsKO KOUserData - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz \<sigma>; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; x && ~~ mask pageBits \<le> x; x \<le> (x && ~~ mask pageBits) + 2 ^ pageBits - 1; \<not> pointerInDeviceData x \<sigma>; is_aligned (x && ~~ mask pageBits) (objBitsKO KOUserData); ps_clear (x && ~~ mask pageBits) (objBitsKO KOUserData) \<sigma>; \<not> x \<le> (x && ~~ mask pageBits) + 2 ^ objBitsKO KOUserData - 1\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState \<sigma>) x = 0 proof (prove)
goal:
No subgoals!