theory Invoke_C

lemma object_type_from_H_bound:
  "object_type_from_H newType \<le> of_nat (length (enum::object_type list) - Suc 0)" apply (simp add:enum_object_type enum_apiobject_type object_type_from_H_def) apply (case_tac newType) apply (clarsimp simp:ARMSmallPageBits_def ARMLargePageBits_def objBits_simps
     Kernel_C_defs split:apiobject_type.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type_from_H newType \<le> word_of_nat (length enum - Suc 0) proof (prove)
goal (1 subgoal):
 1. (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA proof (prove)
goal (7 subgoals):
 1. \<And>x1. newType = APIObjectType x1 \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA
 2. newType = object_type.SmallPageObject \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA
 3. newType = object_type.LargePageObject \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA
 4. newType = object_type.SectionObject \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA
 5. newType = object_type.SuperSectionObject \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA
 6. newType = object_type.PageTableObject \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA
 7. newType = object_type.PageDirectoryObject \<Longrightarrow> (case newType of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) \<le> 0xA proof (prove)
goal:
No subgoals!