theory CSpace_C

lemma ccap_relation_get_capPtr_physical:
  notes unfolds = ccap_relation_def get_capPtr_CL_def cap_lift_def
                  cap_tag_defs cap_to_H_def get_capZombiePtr_CL_def
                  get_capZombieBits_CL_def Let_def objBits_simps
                  capAligned_def
  shows
  "\<lbrakk> ccap_relation hcap ccap; capClass hcap = PhysicalClass; capAligned hcap \<rbrakk> \<Longrightarrow>
     get_capPtr_CL (cap_lift ccap)
        = Ptr (capUntypedPtr hcap)" apply (cases hcap; simp add: isCap_simps) defer 4 defer 4 apply ((frule cap_get_tag_isCap_unfolded_H_cap,
                    clarsimp simp: unfolds
                    split: if_split_asm dest!: ctcb_ptr_to_tcb_ptr_mask)+)[5] apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: unfolds split: if_split_asm dest!: ctcb_ptr_to_tcb_ptr_mask) apply (rule arg_cong [OF less_mask_eq]) apply (simp add: capAligned_def word_bits_conv objBits_simps
                    word_less_nat_alt) subgoal for arch_capability apply (cases arch_capability; simp) defer 2  (* page caps last *)
      apply (fold_subgoals (prefix))[3] subgoal by ((frule cap_get_tag_isCap_unfolded_H_cap,
                  clarsimp simp: unfolds split: if_split_asm)+) defer subgoal for \<dots> vmpage_size option apply (cases "vmpage_size = ARMSmallPage"; simp?) apply (frule cap_get_tag_isCap_unfolded_H_cap(16), simp) subgoal by (clarsimp simp: unfolds split: if_split_asm) by (frule cap_get_tag_isCap_unfolded_H_cap(17), simp,
          clarsimp simp: unfolds
                         cap_tag_defs cap_to_H_def
                  split: if_split_asm)+ done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation hcap ccap; capClass hcap = PhysicalClass; capAligned hcap\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (global.capUntypedPtr hcap) proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>ccap_relation (capability.ThreadCap x1) ccap; capAligned (capability.ThreadCap x1); hcap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x1
 2. \<And>x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) ccap; capAligned (capability.NotificationCap x31 x32 x33 x34); hcap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x31
 3. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) ccap; capAligned (capability.EndpointCap x51 x52 x53 x54 x55 x56); hcap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x51
 4. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x71
 5. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8)
 6. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x102
 7. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x111 proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>ccap_relation (capability.ThreadCap x1) ccap; capAligned (capability.ThreadCap x1); hcap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x1
 2. \<And>x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) ccap; capAligned (capability.NotificationCap x31 x32 x33 x34); hcap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x31
 3. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) ccap; capAligned (capability.EndpointCap x51 x52 x53 x54 x55 x56); hcap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x51
 4. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8)
 5. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x102
 6. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x111
 7. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x71 proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>ccap_relation (capability.ThreadCap x1) ccap; capAligned (capability.ThreadCap x1); hcap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x1
 2. \<And>x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) ccap; capAligned (capability.NotificationCap x31 x32 x33 x34); hcap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x31
 3. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) ccap; capAligned (capability.EndpointCap x51 x52 x53 x54 x55 x56); hcap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x51
 4. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x102
 5. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x111
 6. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x71
 7. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8) proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x71
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8) proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x71
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>hcap = capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6))) (unat (cap_C.words_C ccap.[Suc 0] && mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6))))); cap_get_tag ccap = 0x2E; \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && mask 6); is_aligned (cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))) (cteSizeBits + unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)); cteSizeBits + unat ((cap_C.words_C ccap.[0] >> 8) && mask 6) < word_bits\<rbrakk> \<Longrightarrow> cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat (((cap_C.words_C ccap.[0] >> 8) && mask 6) && mask 5))) = cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>hcap = capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6))) (unat (cap_C.words_C ccap.[Suc 0] && mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6))))); cap_get_tag ccap = 0x2E; \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && mask 6); is_aligned (cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))) (cteSizeBits + unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)); cteSizeBits + unat ((cap_C.words_C ccap.[0] >> 8) && mask 6) < word_bits\<rbrakk> \<Longrightarrow> (cap_C.words_C ccap.[0] >> 8) && mask 6 < 2 ^ 5
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8) proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr x8) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_capability) ccap; acapClass arch_capability = PhysicalClass; capAligned (capability.ArchObjectCap arch_capability); hcap = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) (Arch.capUntypedPtr arch_capability) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)) ccap; capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)); hcap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12); arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11
 2. \<And>x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32
 3. \<And>x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); hcap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x41
 4. \<And>x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); hcap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x51 proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)) ccap; capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)); hcap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12); arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11
 2. \<And>x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); hcap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x41
 3. \<And>x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); hcap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x51
 4. \<And>x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32 proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)) ccap; capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)); hcap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12); arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11
 2. \<And>x41 x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); hcap = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x41
 3. \<And>x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); hcap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x51
 4. \<And>x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32 proof (prove)
goal (2 subgoals):
 1. \<And>x11. (\<And>x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)) ccap; capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)); hcap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12); arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11) &&& (\<And>x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x11 x42)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x11 x42)); hcap = capability.ArchObjectCap (arch_capability.PageTableCap x11 x42); arch_capability = arch_capability.PageTableCap x11 x42\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11) &&& (\<And>x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x11 x52)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x11 x52)); hcap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x11 x52); arch_capability = arch_capability.PageDirectoryCap x11 x52\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11)
 2. \<And>x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32 proof (prove)
goal (1 subgoal):
 1. (\<And>x12. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11_ x12)) ccap; capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11_ x12)); hcap = capability.ArchObjectCap (arch_capability.ASIDPoolCap x11_ x12); arch_capability = arch_capability.ASIDPoolCap x11_ x12\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11_) &&& (\<And>x42. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap x11_ x42)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x11_ x42)); hcap = capability.ArchObjectCap (arch_capability.PageTableCap x11_ x42); arch_capability = arch_capability.PageTableCap x11_ x42\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11_) &&& (\<And>x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x11_ x52)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x11_ x52)); hcap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x11_ x52); arch_capability = arch_capability.PageDirectoryCap x11_ x52\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x11_) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32 proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ vmpage_size option\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_ proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option; vmpage_size = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ vmpage_size option; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_ proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option; vmpage_size = Wellformed_C.ARMSmallPage; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ vmpage_size option; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option; vmpage_size = Wellformed_C.ARMSmallPage; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31_ x32_ x33_ vmpage_size option); arch_capability = arch_capability.PageCap x31_ x32_ x33_ vmpage_size option; vmpage_size \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> get_capPtr_CL (cap_lift ccap) = PTR(unit) x32_ proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!