theory ADT_C

lemma device_mem_C_relation:
  "\<lbrakk>cpspace_device_data_relation (ksPSpace s')
      (underlying_memory (ksMachineState s')) (t_hrs_' s);
    pspace_distinct' s'\<rbrakk>
   \<Longrightarrow> device_mem_C s = device_mem' s'" apply (rule ext) apply (rename_tac p) apply (clarsimp simp: device_mem_C_def device_mem'_def
                  split: if_splits option.splits) apply (rule conjI) apply (clarsimp simp: pointerInDeviceData_def) apply (clarsimp simp: cmap_relation_def) apply (subgoal_tac "(Ptr (p && ~~mask pageBits) :: user_data_device_C ptr) \<in>
                        Ptr ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))") apply clarsimp apply (thin_tac "Ball A P" for A P) apply (thin_tac "t = dom (clift (t_hrs_' s))" for t) apply (drule device_data_at_ko) apply (rule imageI) apply (clarsimp simp: dom_def heap_to_device_data_def obj_at'_def projectKOs) apply (clarsimp simp: pointerInDeviceData_def) apply (clarsimp simp: cmap_relation_def) apply (drule equalityD2) apply (drule subsetD) apply (fastforce simp: dom_def) apply clarsimp apply (drule bspec) apply (fastforce simp: dom_def) apply (clarsimp simp: heap_to_device_data_def map_comp_def projectKOs
                  split: option.splits) apply (clarsimp simp: typ_at'_def ko_wp_at'_def objBitsKO_def) apply (drule pspace_distinctD') apply fastforce apply (clarsimp simp: objBitsKO_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> device_mem_C s = device_mem' s' proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> device_mem_C s x = device_mem' s' x proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> device_mem_C s p = device_mem' s' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None \<longrightarrow> \<not> pointerInDeviceData p s') \<and> ((\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s') proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None \<longrightarrow> \<not> pointerInDeviceData p s'
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'; PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) = dom (clift (t_hrs_' s)); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'; PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) = dom (clift (t_hrs_' s)); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x))); PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'; PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) = dom (clift (t_hrs_' s)); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 3. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'; PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) = dom (clift (t_hrs_' s)); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'; PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) = dom (clift (t_hrs_' s))\<rbrakk> \<Longrightarrow> PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; typ_at' UserDataDeviceT (p && ~~ mask pageBits) s'\<rbrakk> \<Longrightarrow> PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; ko_at' UserDataDevice (p && ~~ mask pageBits) s'\<rbrakk> \<Longrightarrow> PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = None; ko_at' UserDataDevice (p && ~~ mask pageBits) s'\<rbrakk> \<Longrightarrow> p && ~~ mask pageBits \<in> dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 2. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'\<rbrakk> \<Longrightarrow> (\<exists>x2. clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2) \<longrightarrow> pointerInDeviceData p s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>cpspace_device_data_relation (ksPSpace s') (underlying_memory (ksMachineState s')) (t_hrs_' s); pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))) = dom (clift (t_hrs_' s)); \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x))); dom (clift (t_hrs_' s)) \<subseteq> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (2 subgoals):
 1. \<And>p x2. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> ?c44 p x2 \<in> dom (clift (t_hrs_' s))
 2. \<And>p x2. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x))); ?c44 p x2 \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x))); PTR(user_data_device_C) (p && ~~ mask pageBits) \<in> PTR(user_data_device_C) ` dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2 y. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; \<forall>x\<in>dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s'))). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) x)) (the (clift (t_hrs_' s) (PTR(user_data_device_C) x))); heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits) = Some y\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (2 subgoals):
 1. \<And>p x2 y. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits) = Some y\<rbrakk> \<Longrightarrow> ?x63 p x2 y \<in> dom (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')))
 2. \<And>p x2 y. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits) = Some y; cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) (?x63 p x2 y))) (the (clift (t_hrs_' s) (PTR(user_data_device_C) (?x63 p x2 y))))\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2 y. \<lbrakk>pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits) = Some y; cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace s') (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits))) (the (clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits))))\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>cuser_user_data_device_relation (the (map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits)) (projectKO_opt KOUserDataDevice))) x2; pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; ksPSpace s' (p && ~~ mask pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>cuser_user_data_device_relation (the (map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits)) (projectKO_opt KOUserDataDevice))) x2; pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; ksPSpace s' (p && ~~ mask pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> ps_clear (p && ~~ mask pageBits) pageBits s' proof (prove)
goal (2 subgoals):
 1. \<And>p x2. \<lbrakk>cuser_user_data_device_relation (the (map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits)) (projectKO_opt KOUserDataDevice))) x2; pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>p x2. \<lbrakk>cuser_user_data_device_relation (the (map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits)) (projectKO_opt KOUserDataDevice))) x2; pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; ps_clear (p && ~~ mask pageBits) (objBitsKO KOUserDataDevice) s'\<rbrakk> \<Longrightarrow> ps_clear (p && ~~ mask pageBits) pageBits s' proof (prove)
goal (1 subgoal):
 1. \<And>p x2. \<lbrakk>cuser_user_data_device_relation (the (map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s')) (p && ~~ mask pageBits)) (projectKO_opt KOUserDataDevice))) x2; pspace_distinct' s'; clift (t_hrs_' s) (PTR(user_data_device_C) (p && ~~ mask pageBits)) = Some x2; ps_clear (p && ~~ mask pageBits) (objBitsKO KOUserDataDevice) s'\<rbrakk> \<Longrightarrow> ps_clear (p && ~~ mask pageBits) pageBits s' proof (prove)
goal:
No subgoals!