theory ArchDetype_AI

lemma caps_of_state_ko[Detype_AI_asms]:
  "valid_cap cap s
   \<Longrightarrow> is_untyped_cap cap \<or>
       cap_range cap = {} \<or>
       (\<forall>ptr \<in> cap_range cap. \<exists>ko. kheap s ptr = Some ko)" apply (case_tac cap) apply (clarsimp simp: cap_range_def valid_cap_def obj_at_def is_cap_simps
                   split: option.splits)+ apply (rename_tac arch_cap ptr) apply (case_tac arch_cap) apply (fastforce simp: cap_range_def obj_at_def is_cap_simps
                    split: option.splits if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 7. \<And>x7. \<lbrakk>s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 8. \<lbrakk>s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 9. \<lbrakk>s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
 10. \<And>x10. \<lbrakk>s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<or> cap_range cap = {} \<or> (\<forall>ptr\<in>cap_range cap. \<exists>ko. kheap s ptr = Some ko)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12 ptr. \<lbrakk>case x12 of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap x12; cap_aligned (ArchObjectCap x12); aobj_ref x12 = Some ptr\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap ptr. \<lbrakk>case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap arch_cap; cap_aligned (ArchObjectCap arch_cap); aobj_ref arch_cap = Some ptr\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko proof (prove)
goal (5 subgoals):
 1. \<And>arch_cap ptr x11 x12. \<lbrakk>case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap arch_cap; cap_aligned (ArchObjectCap arch_cap); aobj_ref arch_cap = Some ptr; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko
 2. \<And>arch_cap ptr. \<lbrakk>case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap arch_cap; cap_aligned (ArchObjectCap arch_cap); aobj_ref arch_cap = Some ptr; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko
 3. \<And>arch_cap ptr x31 x32 x33 x34 x35. \<lbrakk>case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap arch_cap; cap_aligned (ArchObjectCap arch_cap); aobj_ref arch_cap = Some ptr; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko
 4. \<And>arch_cap ptr x41 x42. \<lbrakk>case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap arch_cap; cap_aligned (ArchObjectCap arch_cap); aobj_ref arch_cap = Some ptr; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko
 5. \<And>arch_cap ptr x51 x52. \<lbrakk>case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> ((if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case x2 of (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base)))) | PageTableCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageTable) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageTable) r s \<and> (case x2 of (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))))) | PageDirectoryCap r mapdata \<Rightarrow> \<not> (mapdata = None \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> True) \<or> (\<exists>x2. mapdata = Some x2 \<and> \<not> (typ_at (AArch APageDirectory) r s \<and> 0 < x2 \<and> x2 \<le> 2 ^ local.asid_bits - 1))); cap = ArchObjectCap arch_cap; cap_aligned (ArchObjectCap arch_cap); aobj_ref arch_cap = Some ptr; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ptr = Some ko proof (prove)
goal:
No subgoals!