theory StateRelation

lemma obj_relation_cutsE:
  "\<lbrakk> (y, P) \<in> obj_relation_cuts ko x; P ko ko';
     \<And>sz cs z cap cte. \<lbrakk> ko = CNode sz cs; well_formed_cnode_n sz cs; y = cte_map (x, z);
                      ko' = KOCTE cte; cs z = Some cap; cap_relation cap (cteCap cte) \<rbrakk>
              \<Longrightarrow> R;
     \<And>pt (z :: word8) pte'. \<lbrakk> ko = ArchObj (PageTable pt); y = x + (ucast z << 2);
                              ko' = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte' \<rbrakk>
              \<Longrightarrow> R;
     \<And>pd (z :: 12 word) pde'. \<lbrakk> ko = ArchObj (PageDirectory pd); y = x + (ucast z << 2);
                              ko' = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde' \<rbrakk>
              \<Longrightarrow> R;
     \<And>sz dev n. \<lbrakk> ko = ArchObj (DataPage dev sz); ko' = (if dev then KOUserDataDevice else KOUserData);
              y = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits) \<rbrakk> \<Longrightarrow> R;
            \<lbrakk> y = x; other_obj_relation ko ko'; is_other_obj_relation_type (a_type ko) \<rbrakk> \<Longrightarrow> R
    \<rbrakk> \<Longrightarrow> R" apply (simp add: obj_relation_cuts_def2 is_other_obj_relation_type_def
                   a_type_def
            split: Structures_A.kernel_object.split_asm if_split_asm
                   ARM_A.arch_kernel_obj.split_asm) apply ((clarsimp split: if_splits,
                force simp: cte_relation_def pte_relation_def pde_relation_def)+)[5] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; P ko ko'; \<And>sz cs z cap cte. \<lbrakk>ko = CNode sz cs; well_formed_cnode_n sz cs; y = cte_map (x, z); ko' = KOCTE cte; cs z = Some cap; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> R; \<And>pt z pte'. \<lbrakk>ko = ArchObj (PageTable pt); y = x + (UCAST(8 \<rightarrow> 32) z << 2); ko' = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte'\<rbrakk> \<Longrightarrow> R; \<And>pd z pde'. \<lbrakk>ko = ArchObj (PageDirectory pd); y = x + (UCAST(12 \<rightarrow> 32) z << 2); ko' = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde'\<rbrakk> \<Longrightarrow> R; \<And>sz dev n. \<lbrakk>ko = ArchObj (DataPage dev sz); ko' = (if dev then KOUserDataDevice else KOUserData); y = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> R; \<lbrakk>y = x; other_obj_relation ko ko'; is_other_obj_relation_type (a_type ko)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>ko = CNode x11 x12; P (CNode x11 x12) ko'; \<And>sz z cap cte. \<lbrakk>x11 = sz; well_formed_cnode_n sz x12; y = cte_map (x, z); ko' = KOCTE cte; x12 z = Some cap; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> R; well_formed_cnode_n x11 x12; \<exists>ya. y = cte_map (x, ya) \<and> P = cte_relation ya \<and> ya \<in> dom x12\<rbrakk> \<Longrightarrow> R
 2. \<And>x5 x2. \<lbrakk>ko = ArchObj (PageTable x2); P (ArchObj (PageTable x2)) ko'; \<And>pt z pte'. \<lbrakk>x2 = pt; y = x + (UCAST(8 \<rightarrow> 32) z << 2); ko' = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte'\<rbrakk> \<Longrightarrow> R; x5 = PageTable x2; (y, P) \<in> range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y))\<rbrakk> \<Longrightarrow> R
 3. \<And>x5 x3. \<lbrakk>ko = ArchObj (PageDirectory x3); P (ArchObj (PageDirectory x3)) ko'; \<And>pd z pde'. \<lbrakk>x3 = pd; y = x + (UCAST(12 \<rightarrow> 32) z << 2); ko' = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde'\<rbrakk> \<Longrightarrow> R; x5 = PageDirectory x3; (y, P) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y))\<rbrakk> \<Longrightarrow> R
 4. \<And>x5 x41 x42. \<lbrakk>ko = ArchObj (DataPage True x42); P (ArchObj (DataPage True x42)) ko'; \<And>sz n. \<lbrakk>x42 = sz; ko' = KOUserDataDevice; y = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> R; x5 = DataPage True x42; x41; \<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = KOUserDataDevice) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits)\<rbrakk> \<Longrightarrow> R
 5. \<And>x5 x41 x42. \<lbrakk>ko = ArchObj (DataPage False x42); P (ArchObj (DataPage False x42)) ko'; \<And>sz n. \<lbrakk>x42 = sz; ko' = KOUserData; y = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> R; x5 = DataPage False x42; \<not> x41; \<exists>n. y = x + n * 2 ^ pageBits \<and> P = (\<lambda>_ obj. obj = KOUserData) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits)\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!