theory Refine

lemma typ_at_UserDataI:
  "\<lbrakk> typ_at' UserDataT (p && ~~ mask pageBits) s';
     pspace_relation (kheap s) (ksPSpace s'); pspace_aligned s \<rbrakk>
  \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s" apply (clarsimp simp: exists_disj obj_at'_def typ_at'_def ko_wp_at'_def
                        projectKOs) apply (frule (1) in_related_pspace_dom) apply (clarsimp simp: pspace_dom_def) apply (clarsimp simp: pspace_relation_def dom_def) apply (erule allE, erule impE, blast) apply clarsimp apply (drule (1) bspec) apply clarsimp apply (subst mask_lower_twice [where n = pageBits, OF pbfs_atleast_pageBits, symmetric]) apply (clarsimp simp: obj_relation_cuts_def2 pte_relation_def
                        cte_relation_def other_obj_relation_def
                        pde_relation_def
              split: Structures_A.kernel_object.split_asm
                     Structures_H.kernel_object.split_asm
                     if_split_asm arch_kernel_obj.split_asm) apply (rename_tac vmpage_size n) apply (rule_tac x = vmpage_size in exI) apply (subst conjunct2 [OF is_aligned_add_helper]) apply (drule (1) pspace_alignedD) apply simp apply (erule word_less_power_trans2 [OF _ pbfs_atleast_pageBits]) apply (case_tac vmpage_size, simp_all add: word_bits_conv)[1] apply (simp add: obj_at_def  a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' UserDataT (p && ~~ mask pageBits) s'; pspace_relation (kheap s) (ksPSpace s'); pspace_aligned s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; p && ~~ mask pageBits \<in> pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y; pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)))\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y; pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y; pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; \<forall>x\<in>obj_relation_cuts y x. case x of (ya, P) \<Rightarrow> P y (the (ksPSpace s' ya))\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y; pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; case (p && ~~ mask pageBits, b) of (ya, P) \<Rightarrow> P y (the (ksPSpace s' ya))\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y; pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; b y ko\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>ko x b y. \<lbrakk>pspace_aligned s; ksPSpace s' (p && ~~ mask pageBits) = Some ko; is_aligned (p && ~~ mask pageBits) (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear (p && ~~ mask pageBits) (objBitsKO ko) s'; (p && ~~ mask pageBits, b) \<in> obj_relation_cuts y x; kheap s x = Some y; pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; b y ko\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) ((p && ~~ mask pageBits) && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>x x41 x42 n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False x42)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize x42 - pageBits)\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (x + n * 2 ^ pageBits && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (x + n * 2 ^ pageBits && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData vmpage_size)) (x + n * 2 ^ pageBits && ~~ mask (pageBitsForSize vmpage_size)) s proof (prove)
goal (3 subgoals):
 1. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> is_aligned x (pageBitsForSize vmpage_size)
 2. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size
 3. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData vmpage_size)) x s proof (prove)
goal (3 subgoals):
 1. \<And>x x41 vmpage_size n. \<lbrakk>pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits); is_aligned x (obj_bits (ArchObj (DataPage False vmpage_size)))\<rbrakk> \<Longrightarrow> is_aligned x (pageBitsForSize vmpage_size)
 2. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size
 3. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData vmpage_size)) x s proof (prove)
goal (2 subgoals):
 1. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size
 2. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData vmpage_size)) x s proof (prove)
goal (2 subgoals):
 1. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size < LENGTH(32)
 2. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData vmpage_size)) x s proof (prove)
goal (1 subgoal):
 1. \<And>x x41 vmpage_size n. \<lbrakk>kheap s x = Some (ArchObj (DataPage False vmpage_size)); pspace_dom (kheap s) = {a. \<exists>y. ksPSpace s' a = Some y}; pspace_aligned s; ksPSpace s' (x + n * 2 ^ pageBits) = Some KOUserData; is_aligned (x + n * 2 ^ pageBits) (objBitsKO KOUserData); ps_clear (x + n * 2 ^ pageBits) (objBitsKO KOUserData) s'; \<not> x41; p && ~~ mask pageBits = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData vmpage_size)) x s proof (prove)
goal:
No subgoals!