theory CNodeInv_R

lemma Final_notUntyped_capRange_disjoint:
  "\<lbrakk> isFinal cap sl (cteCaps_of s); cteCaps_of s sl' = Some cap';
      sl \<noteq> sl'; capUntypedPtr cap = capUntypedPtr cap'; capBits cap = capBits cap';
      isThreadCap cap \<or> isCNodeCap cap; s \<turnstile>' cap;
      \<not> isUntypedCap cap'; \<not> isArchPageCap cap'; \<not> isZombie cap';
      capClass cap' = PhysicalClass; valid_objs' s \<rbrakk>
          \<Longrightarrow> P" apply (clarsimp simp add: isFinal_def) apply (drule_tac x=sl' in spec) apply (clarsimp simp: cteCaps_of_def) apply (drule(1) ctes_of_valid') apply (elim disjE isCapDs[elim_format]) apply (clarsimp simp: valid_cap'_def
                         obj_at'_def projectKOs objBits_simps'
                         typ_at'_def ko_wp_at'_def
                  split: capability.split_asm zombie_type.split_asm
                         arch_capability.split_asm
                  dest!: spec[where x=0]) apply (clarsimp simp: sameObjectAs_def3 isCap_simps) apply (simp add: isCap_simps) apply (simp add: isCap_simps) apply (clarsimp simp: valid_cap'_def
                        obj_at'_def projectKOs objBits_simps
                        typ_at'_def ko_wp_at'_def
                        page_table_at'_def page_directory_at'_def
                 split: capability.split_asm zombie_type.split_asm
                        arch_capability.split_asm
                 dest!: spec[where x=0]) apply fastforce+ apply (clarsimp simp: isCap_simps sameObjectAs_def3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isFinal cap sl (cteCaps_of s); cteCaps_of s sl' = Some cap'; sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr cap'; capBits cap = capBits cap'; isThreadCap cap \<or> isCNodeCap cap; valid_cap' cap s; \<not> isUntypedCap cap'; \<not> isArchPageCap cap'; \<not> isZombie cap'; capClass cap' = PhysicalClass; valid_objs' s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCaps_of s sl' = Some cap'; sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr cap'; capBits cap = capBits cap'; isThreadCap cap \<or> isCNodeCap cap; valid_cap' cap s; \<not> isUntypedCap cap'; \<not> isArchPageCap cap'; \<not> isZombie cap'; capClass cap' = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<forall>p' c. cteCaps_of s p' = Some c \<longrightarrow> sl \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCaps_of s sl' = Some cap'; sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr cap'; capBits cap = capBits cap'; isThreadCap cap \<or> isCNodeCap cap; valid_cap' cap s; \<not> isUntypedCap cap'; \<not> isArchPageCap cap'; \<not> isZombie cap'; capClass cap' = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<forall>c. cteCaps_of s sl' = Some c \<longrightarrow> sl \<noteq> sl' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); isThreadCap cap \<or> isCNodeCap cap; valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); ctes_of s sl' = Some z; cap' = cteCap z\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); isThreadCap cap \<or> isCNodeCap cap; valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s; \<exists>ptr. cap = capability.ThreadCap ptr\<rbrakk> \<Longrightarrow> P
 2. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s; \<exists>ptr bits grd gsize. cap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>z x1a obj. \<lbrakk>cap = capability.ThreadCap x1a; \<not> isArchPageCap (capability.ThreadCap x1a); \<not> isZombie (capability.ThreadCap x1a); valid_objs' s; \<not> global.sameObjectAs (capability.ThreadCap x1a) (capability.ThreadCap x1a); cap' = capability.ThreadCap x1a; sl \<noteq> sl'; capAligned (capability.ThreadCap x1a); cteCap z = capability.ThreadCap x1a; ksPSpace s x1a = Some (KOTCB obj); is_aligned x1a 9; ps_clear x1a 9 s\<rbrakk> \<Longrightarrow> P
 2. \<And>z obj x31 x32 x33 x34 x35. \<lbrakk>cap = capability.ThreadCap x32; \<not> isArchPageCap (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); \<not> isZombie (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); valid_objs' s; \<not> global.sameObjectAs (capability.ThreadCap x32) (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); sl \<noteq> sl'; pageBitsForSize x34 = 9; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ThreadCap x32); cteCap z = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); ksPSpace s x32 = Some (KOTCB obj); is_aligned x32 9; ps_clear x32 9 s; x32 \<noteq> 0; case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase; 0 < 2 ^ (9 - pageBits) \<longrightarrow> TCBT = (if x31 then UserDataDeviceT else UserDataT)\<rbrakk> \<Longrightarrow> P
 3. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s; \<exists>ptr bits grd gsize. cap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>z obj x31 x32 x33 x34 x35. \<lbrakk>cap = capability.ThreadCap x32; \<not> isArchPageCap (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); \<not> isZombie (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); valid_objs' s; \<not> global.sameObjectAs (capability.ThreadCap x32) (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); sl \<noteq> sl'; pageBitsForSize x34 = 9; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); capAligned (capability.ThreadCap x32); cteCap z = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); ksPSpace s x32 = Some (KOTCB obj); is_aligned x32 9; ps_clear x32 9 s; x32 \<noteq> 0; case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase; 0 < 2 ^ (9 - pageBits) \<longrightarrow> TCBT = (if x31 then UserDataDeviceT else UserDataT)\<rbrakk> \<Longrightarrow> P
 2. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s; \<exists>ptr bits grd gsize. cap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); valid_cap' cap s; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); \<not> isZombie (cteCap z); capClass (cteCap z) = PhysicalClass; valid_objs' s; \<not> isUntypedCap cap; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s; \<exists>ptr bits grd gsize. cap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>sl \<noteq> sl'; global.capUntypedPtr cap = global.capUntypedPtr (cteCap z); capBits cap = capBits (cteCap z); valid_cap' cap s; \<forall>d v0 v1 f. cteCap z \<noteq> capability.UntypedCap d v0 v1 f; \<forall>d ref rghts sz data. cteCap z \<noteq> capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data); \<forall>v0 v1 v2. cteCap z \<noteq> capability.Zombie v0 v1 v2; capClass (cteCap z) = PhysicalClass; valid_objs' s; \<forall>d v0 v1 f. cap \<noteq> capability.UntypedCap d v0 v1 f; \<not> global.sameObjectAs cap (cteCap z); cap' = cteCap z; valid_cap' (cteCap z) s; \<exists>ptr bits grd gsize. cap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>z x112 x113 x114 x31 x32 x33 x34 x35 obj. \<lbrakk>cap = capability.CNodeCap x32 x112 x113 x114; All Not; valid_objs' s; x31; cap' = capability.ArchObjectCap (arch_capability.PageCap True x32 x33 x34 x35); cteSizeBits + x112 = pageBitsForSize x34; capAligned (capability.ArchObjectCap (arch_capability.PageCap True x32 x33 x34 x35)); capAligned (capability.CNodeCap x32 x112 x113 x114); 0 < x112; x112 + x114 \<le> word_bits; x113 && mask x114 = x113; cteCap z = capability.ArchObjectCap (arch_capability.PageCap True x32 x33 x34 x35); case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase; \<not> 0 < 2 ^ (pageBitsForSize x34 - pageBits); ksPSpace s x32 = Some (KOCTE obj); is_aligned x32 cteSizeBits; ps_clear x32 cteSizeBits s\<rbrakk> \<Longrightarrow> P
 2. \<And>z x112 x113 x114 x101 x102 x104 obj. \<lbrakk>cap = capability.CNodeCap x102 x112 x113 x114; All Not; x101; valid_objs' s; cap' = capability.UntypedCap True x102 (cteSizeBits + x112) x104; capAligned (capability.UntypedCap True x102 (cteSizeBits + x112) x104); capAligned (capability.CNodeCap x102 x112 x113 x114); 0 < x112; x112 + x114 \<le> word_bits; x113 && mask x114 = x113; cteCap z = capability.UntypedCap True x102 (cteSizeBits + x112) x104; valid_untyped' True x102 (cteSizeBits + x112) x104 s; ksPSpace s x102 = Some (KOCTE obj); minUntypedSizeBits \<le> cteSizeBits + x112; is_aligned x102 cteSizeBits; cteSizeBits + x112 \<le> maxUntypedSizeBits; ps_clear x102 cteSizeBits s; x104 \<le> 2 ^ (cteSizeBits + x112); is_aligned (word_of_nat x104) minUntypedSizeBits\<rbrakk> \<Longrightarrow> P
 3. \<And>z x113 x114 x111a x112a x113a x114a obj. \<lbrakk>cap = capability.CNodeCap x111a x112a x113 x114; valid_objs' s; \<not> global.sameObjectAs (capability.CNodeCap x111a x112a x113 x114) (capability.CNodeCap x111a x112a x113a x114a); cap' = capability.CNodeCap x111a x112a x113a x114a; sl \<noteq> sl'; capAligned (capability.CNodeCap x111a x112a x113a x114a); capAligned (capability.CNodeCap x111a x112a x113 x114); x112a + x114 \<le> word_bits; x113 && mask x114 = x113; cteCap z = capability.CNodeCap x111a x112a x113a x114a; 0 < x112a; ksPSpace s x111a = Some (KOCTE obj); x112a + x114a \<le> word_bits; x113a && mask x114a = x113a; is_aligned x111a cteSizeBits; ps_clear x111a cteSizeBits s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z x113 x114 x111a x112a x113a x114a obj. \<lbrakk>cap = capability.CNodeCap x111a x112a x113 x114; valid_objs' s; \<not> global.sameObjectAs (capability.CNodeCap x111a x112a x113 x114) (capability.CNodeCap x111a x112a x113a x114a); cap' = capability.CNodeCap x111a x112a x113a x114a; sl \<noteq> sl'; capAligned (capability.CNodeCap x111a x112a x113a x114a); capAligned (capability.CNodeCap x111a x112a x113 x114); x112a + x114 \<le> word_bits; x113 && mask x114 = x113; cteCap z = capability.CNodeCap x111a x112a x113a x114a; 0 < x112a; ksPSpace s x111a = Some (KOCTE obj); x112a + x114a \<le> word_bits; x113a && mask x114a = x113a; is_aligned x111a cteSizeBits; ps_clear x111a cteSizeBits s\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!