theory Invoke_C

lemma Arch_isFrameType_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
             Call Arch_isFrameType_'proc
  \<lbrace> \<acute>ret__unsigned_long =
     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>" apply vcg apply (simp add: toEnum_object_type_to_H) apply (frule object_type_from_to_H) apply (auto dest!: object_type_from_H_toAPIType_simps[THEN iffD1,OF eq_commute[THEN iffD1]]) apply (auto simp: object_type_to_H_def isFrameType_def isFrameType_def
             split: if_splits object_type.splits) apply (auto simp: object_type_from_H_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum maxBound\<rbrace> Call Arch_isFrameType_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isFrameType (toEnum (unat \<^bsup>s\<^esup>type)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>type. unat type \<le> fromEnum maxBound \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject = type \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (isFrameType (toEnum (unat type)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject = type \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (isFrameType (toEnum (unat type)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject = type \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (isFrameType (toEnum (unat type)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject = type \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (isFrameType (toEnum (unat type)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> type \<longrightarrow> (True \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (isFrameType (toEnum (unat type)))) \<and> (\<not> True \<longrightarrow> False))))) proof (prove)
goal (1 subgoal):
 1. \<And>type. unat type \<le> fromEnum maxBound \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> type \<longrightarrow> \<not> isFrameType (object_type_to_H type))))) proof (prove)
goal (1 subgoal):
 1. \<And>type. \<lbrakk>unat type \<le> fromEnum maxBound; type = object_type_from_H (object_type_to_H type)\<rbrakk> \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> type \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject = type \<longrightarrow> isFrameType (object_type_to_H type)) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> type \<longrightarrow> \<not> isFrameType (object_type_to_H type))))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>unat (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject) \<le> fromEnum maxBound; object_type_to_H (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject) = object_type.SmallPageObject\<rbrakk> \<Longrightarrow> isFrameType object_type.SmallPageObject
 2. \<lbrakk>unat (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject) \<le> fromEnum maxBound; seL4_ARM_SmallPageObject \<noteq> seL4_ARM_LargePageObject; object_type_to_H (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject) = object_type.LargePageObject\<rbrakk> \<Longrightarrow> isFrameType object_type.LargePageObject
 3. \<lbrakk>unat (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject) \<le> fromEnum maxBound; seL4_ARM_SmallPageObject \<noteq> seL4_ARM_SectionObject; seL4_ARM_LargePageObject \<noteq> seL4_ARM_SectionObject; object_type_to_H (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject) = object_type.SectionObject\<rbrakk> \<Longrightarrow> isFrameType object_type.SectionObject
 4. \<lbrakk>unat (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject) \<le> fromEnum maxBound; seL4_ARM_SmallPageObject \<noteq> seL4_ARM_SuperSectionObject; seL4_ARM_LargePageObject \<noteq> seL4_ARM_SuperSectionObject; seL4_ARM_SectionObject \<noteq> seL4_ARM_SuperSectionObject; object_type_to_H (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject) = object_type.SuperSectionObject\<rbrakk> \<Longrightarrow> isFrameType object_type.SuperSectionObject
 5. \<And>type. \<lbrakk>unat type \<le> fromEnum maxBound; type = object_type_from_H (object_type_to_H type); SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> type; SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> type; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> type; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> type; isFrameType (object_type_to_H type)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>unat (object_type_from_H object_type.SmallPageObject) \<le> fromEnum maxBound; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> object_type_from_H object_type.SmallPageObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> object_type_from_H object_type.SmallPageObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> object_type_from_H object_type.SmallPageObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> object_type_from_H object_type.SmallPageObject; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; object_type_from_H object_type.SmallPageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; undefined = object_type.SmallPageObject\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>unat (object_type_from_H object_type.LargePageObject) \<le> fromEnum maxBound; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> object_type_from_H object_type.LargePageObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> object_type_from_H object_type.LargePageObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> object_type_from_H object_type.LargePageObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> object_type_from_H object_type.LargePageObject; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; object_type_from_H object_type.LargePageObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; undefined = object_type.LargePageObject\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>unat (object_type_from_H object_type.SectionObject) \<le> fromEnum maxBound; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> object_type_from_H object_type.SectionObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> object_type_from_H object_type.SectionObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> object_type_from_H object_type.SectionObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> object_type_from_H object_type.SectionObject; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; object_type_from_H object_type.SectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; undefined = object_type.SectionObject\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>unat (object_type_from_H object_type.SuperSectionObject) \<le> fromEnum maxBound; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> object_type_from_H object_type.SuperSectionObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> object_type_from_H object_type.SuperSectionObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> object_type_from_H object_type.SuperSectionObject; SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> object_type_from_H object_type.SuperSectionObject; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; object_type_from_H object_type.SuperSectionObject \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; undefined = object_type.SuperSectionObject\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!