From e2955fca5000f56faa65604d8577b7c0f7ab1537 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 cacb24c27d9..798b5cf3f55 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -2785,6 +2785,9 @@ lemma hoarep_Cond_UNIV: apply simp done +(* always unfold StrictC'_mode_object_defs together with api_object_defs *) +lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs + lemma object_type_from_H_toAPIType_simps: "(object_type_from_H tp = scast seL4_UntypedObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.Untyped)" "(object_type_from_H tp = scast seL4_TCBObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.TCBObject)"