theory CSpace_C

lemma ccap_relation_get_capSizeBits_physical:
  notes unfolds = ccap_relation_def get_capSizeBits_CL_def cap_lift_def
                  cap_tag_defs cap_to_H_def objBits_simps'
                  Let_def field_simps mask_def asid_low_bits_def ARM_H.capUntypedSize_def
  shows
  "\<lbrakk> ccap_relation hcap ccap; capClass hcap = PhysicalClass;
            capAligned hcap \<rbrakk> \<Longrightarrow>
   2 ^ get_capSizeBits_CL (cap_lift ccap) = capUntypedSize hcap" apply (case_tac hcap, simp_all) defer 4  (* zombie caps second last *)
         defer 4  (* arch caps last *)
         apply ((frule cap_get_tag_isCap_unfolded_H_cap,
                     clarsimp simp: unfolds
                             split: if_split_asm)+)[5] apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: unfolds split: if_split_asm) apply (rule arg_cong [OF less_mask_eq[where n=5, unfolded mask_def, simplified]]) apply (simp add: capAligned_def objBits_simps word_bits_conv word_less_nat_alt) subgoal for arch_capability apply (cases arch_capability; simp) defer 2  (* page caps last *)
      apply (fold_subgoals (prefix))[3] subgoal premises prems by ((frule cap_get_tag_isCap_unfolded_H_cap,
               clarsimp simp: unfolds ptBits_def pteBits_def pdBits_def pdeBits_def
                       split: if_split_asm)+) apply (rename_tac vmpage_size option) apply (case_tac "vmpage_size = ARMSmallPage", simp_all) 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
                        pageBitsForSize_spec gen_framesize_to_H_def
                        c_valid_cap_def cl_valid_cap_def framesize_to_H_def
                        generic_frame_cap_get_capFSize_CL_def
                 split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation hcap ccap; capClass hcap = PhysicalClass; capAligned hcap\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = global.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72
 5. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ x103
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ (objBits undefined + x112) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 4. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ x103
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ (objBits undefined + x112)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 4. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ x103
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ (objBits undefined + x112)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ x103
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ (objBits undefined + x112)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72
 7. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize x8 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ objBits undefined
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ x103
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ (objBits undefined + x112)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72
 7. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = 2 ^ zBits x72
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize x8 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>capAligned (capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ ((2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1)) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F))) (unat (cap_C.words_C ccap.[Suc 0] && (2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1))); hcap = capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ ((2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1)) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F))) (unat (cap_C.words_C ccap.[Suc 0] && (2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1)); cap_get_tag ccap = 0x2E; \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && 0x3F)\<rbrakk> \<Longrightarrow> 2 ^ (4 + unat (((cap_C.words_C ccap.[0] >> 8) && 0x3F) && 0x1F)) = 2 ^ (4 + unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F))
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize x8 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>capAligned (capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ ((2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1)) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F))) (unat (cap_C.words_C ccap.[Suc 0] && (2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1))); hcap = capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ ((2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1)) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F))) (unat (cap_C.words_C ccap.[Suc 0] && (2 << unat ((cap_C.words_C ccap.[0] >> 8) && 0x3F)) - 1)); cap_get_tag ccap = 0x2E; \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && 0x3F)\<rbrakk> \<Longrightarrow> (cap_C.words_C ccap.[0] >> 8) && 0x3F < 0x20
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; acapClass x8 = PhysicalClass; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.ASIDPoolCap x11 x12)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 x34 x35)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageTableCap x41 x42)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageDirectoryCap x51 x52) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.ASIDPoolCap x11 x12)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageTableCap x41 x42)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageDirectoryCap x51 x52)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 x34 x35) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.ASIDPoolCap x11 x12)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageTableCap x41 x42)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageDirectoryCap x51 x52)
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 x34 x35) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.ASIDPoolCap x11 x12)) &&& (\<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageTableCap x11 x42)) &&& (\<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageDirectoryCap x11 x52))
 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 x34 x35) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.ASIDPoolCap x11_ x12)) &&& (\<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageTableCap x11_ x42)) &&& (\<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageDirectoryCap x11_ x52)) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 x34 x35) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 vmpage_size option. \<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 vmpage_size option) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 vmpage_size option. \<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage option)
 2. \<And>x31 x32 x33 vmpage_size option. \<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 vmpage_size option) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 vmpage_size option. \<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSmallPage option)
 2. \<And>x31 x32 x33 vmpage_size option. \<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 vmpage_size option) 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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31_ x32_ x33_ Wellformed_C.ARMSmallPage option_) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 vmpage_size option. \<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> 2 ^ get_capSizeBits_CL (cap_lift ccap) = Arch.capUntypedSize (arch_capability.PageCap x31 x32 x33 vmpage_size option) proof (prove)
goal:
No subgoals!