theory Invoke_C

lemma getObjectSize_spec:
  "\<forall>s. \<Gamma>\<turnstile>\<lbrace>s. \<acute>t \<le> of_nat (length (enum::object_type list) - 1)\<rbrace> Call getObjectSize_'proc
           \<lbrace>\<acute>ret__unsigned_long = of_nat (getObjectSize (object_type_to_H (t_' s)) (unat (userObjSize_' s)))\<rbrace>" apply vcg apply (clarsimp simp:ARMSmallPageBits_def ARMLargePageBits_def objBits_simps'
    object_type_to_H_def Kernel_C_defs APIType_capBits_def ARMSectionBits_def ARMSuperSectionBits_def) apply (simp add:nAPIObjects_def) apply (simp add:enum_object_type enum_apiobject_type) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<acute>t \<le> word_of_nat (length enum - 1)\<rbrace> Call getObjectSize_'proc \<lbrace>\<acute>ret__unsigned_long = word_of_nat (getObjectSize (object_type_to_H \<^bsup>s\<^esup>t) (unat \<^bsup>s\<^esup>userObjSize))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>userObjSize t. t \<le> word_of_nat (length enum - 1) \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSmallPageBits = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMLargePageBits = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSectionBits = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSuperSectionBits = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject = t \<longrightarrow> - 2147483648 \<le> sint 2 + sint 8 \<and> sint 2 + sint 8 \<le> 2147483647 \<and> SCAST(32 signed \<rightarrow> 32) (2 + 8) = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject = t \<longrightarrow> - 2147483648 \<le> sint 2 + sint 0xC \<and> sint 2 + sint 0xC \<le> 2147483647 \<and> SCAST(32 signed \<rightarrow> 32) (2 + 0xC) = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject \<noteq> t \<longrightarrow> (True \<longrightarrow> False) \<and> (\<not> True \<longrightarrow> False)))))))) \<and> (\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_TCBObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 9 = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 4 = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 4 = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject = t \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 4 + userObjSize = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<noteq> t \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject = t \<longrightarrow> userObjSize = word_of_nat (getObjectSize (object_type_to_H t) (unat userObjSize))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject \<noteq> t \<longrightarrow> (True \<longrightarrow> False) \<and> (\<not> True \<longrightarrow> False))))))) proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<le> word_of_nat (length enum - Suc 0) \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t \<longrightarrow> t \<noteq> 6 \<longrightarrow> t \<noteq> 7 \<longrightarrow> t \<noteq> 8 \<longrightarrow> t \<noteq> 9 \<longrightarrow> t \<noteq> 0xA \<longrightarrow> t = 5) \<and> (\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t \<longrightarrow> t \<noteq> 1 \<longrightarrow> t \<noteq> 2 \<longrightarrow> t \<noteq> 3 \<longrightarrow> t \<noteq> 4 \<longrightarrow> t = 0) proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<le> word_of_nat (length enum - Suc 0) \<Longrightarrow> (5 \<le> t \<longrightarrow> t \<noteq> 6 \<longrightarrow> t \<noteq> 7 \<longrightarrow> t \<noteq> 8 \<longrightarrow> t \<noteq> 9 \<longrightarrow> t \<noteq> 0xA \<longrightarrow> t = 5) \<and> (\<not> 5 \<le> t \<longrightarrow> t \<noteq> 1 \<longrightarrow> t \<noteq> 2 \<longrightarrow> t \<noteq> 3 \<longrightarrow> t \<noteq> 4 \<longrightarrow> t = 0) proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<le> 0xA \<Longrightarrow> (5 \<le> t \<longrightarrow> t \<noteq> 6 \<longrightarrow> t \<noteq> 7 \<longrightarrow> t \<noteq> 8 \<longrightarrow> t \<noteq> 9 \<longrightarrow> t \<noteq> 0xA \<longrightarrow> t = 5) \<and> (\<not> 5 \<le> t \<longrightarrow> t \<noteq> 1 \<longrightarrow> t \<noteq> 2 \<longrightarrow> t \<noteq> 3 \<longrightarrow> t \<noteq> 4 \<longrightarrow> t = 0) proof (prove)
goal:
No subgoals!