theory Refine

lemma pointerInDeviceData_relation:
  "\<lbrakk> (s,s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk>
   \<Longrightarrow> pointerInDeviceData p s' = in_device_frame p s" apply (simp add: pointerInDeviceData_def in_device_frame_def) apply (rule iffI) apply (erule typ_at_DeviceDataI, (clarsimp simp: valid_state_def)+)[1] apply clarsimp apply (drule_tac sz = sz and
                   n = "(p && mask (pageBitsForSize sz)) >> pageBits"
    in typ_at_ADeviceDataI [where s = s and s' = s']) apply (fastforce simp: valid_state'_def)+ apply (rule shiftr_less_t2n') apply (simp add: pbfs_atleast_pageBits mask_twice) apply (case_tac sz, simp_all)[1] apply (subgoal_tac "(p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits = (p && ~~ mask pageBits)") apply simp apply (subst mult.commute) apply (subst shiftl_t2n [symmetric]) apply (simp add: shiftr_shiftl1) apply (subst mask_out_add_aligned) apply (rule is_aligned_neg_mask) apply (simp add: pbfs_atleast_pageBits) apply (subst add.commute) apply (simp add: word_plus_and_or_coroll2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> pointerInDeviceData p s' = in_device_frame p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' = (\<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s
 2. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (5 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 3. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 4. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> p && mask (pageBitsForSize sz) >> pageBits < 2 ^ (pageBitsForSize sz - pageBits)
 5. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> p && mask (pageBitsForSize sz) >> pageBits < 2 ^ (pageBitsForSize sz - pageBits)
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (3 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> (p && mask (pageBitsForSize sz)) && mask (pageBits + (pageBitsForSize sz - pageBits)) = p && mask (pageBitsForSize sz)
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - pageBits < LENGTH(32)
 3. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - pageBits < LENGTH(32)
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'; (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits = p && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + 2 ^ pageBits * (p && mask (pageBitsForSize sz) >> pageBits) = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits << pageBits) = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + ((p && mask (pageBitsForSize sz)) && ~~ mask pageBits) = p && ~~ mask pageBits proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> is_aligned (p && ~~ mask (pageBitsForSize sz)) pageBits
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz)) && ~~ mask pageBits = p && ~~ mask pageBits proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> pageBits \<le> pageBitsForSize sz
 2. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz)) && ~~ mask pageBits = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz)) && ~~ mask pageBits = p && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s; typ_at' UserDataDeviceT ((p && ~~ mask (pageBitsForSize sz)) + (p && mask (pageBitsForSize sz) >> pageBits) * 2 ^ pageBits) s'\<rbrakk> \<Longrightarrow> (p && mask (pageBitsForSize sz)) + (p && ~~ mask (pageBitsForSize sz)) && ~~ mask pageBits = p && ~~ mask pageBits proof (prove)
goal:
No subgoals!