From 4d97b26dbf44a21b40b9111ba6bea2f2f55ccc3f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 11 Aug 2023 17:05:05 +0200 Subject: [PATCH] arm-hyp crefine: proof update for object_type enum reorder Signed-off-by: Gerwin Klein --- proof/crefine/ARM_HYP/Retype_C.thy | 3 +++ 1 file changed, 3 insertions(+) diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index cacb24c27d..088a5ba965 100644 --- 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 \ scast seL4_ARM_PageDirectoryObject | ARM_HYP_H.VCPUObject \ 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: