arm-hyp crefine: proof update for object_type enum reorder

Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Aug 14, 2023 · 4d97b26 · 4d97b26
1 parent 540bb64
commit 4d97b26
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy
@@ -2332,6 +2332,9 @@ definition
                             | ARM_HYP_H.PageDirectoryObject \<Rightarrow> scast seL4_ARM_PageDirectoryObject
                             | ARM_HYP_H.VCPUObject \<Rightarrow> scast seL4_ARM_VCPUObject"
 
+(* always unfold StrictC'_mode_object_defs together with api_object_defs *)
+lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs
+
 lemmas nAPIObjects_def = seL4_NonArchObjectTypeCount_def
 
 lemma nAPIOBjects_object_type_from_H: