From 4913aa8af9db0ff05f060cad7421ce9b0af79248 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Tue, 18 Jul 2023 17:55:56 +0700
Subject: [PATCH] aarch64 haskell: tweak createNewCaps definition

Tweak formulation of createNewCaps for page tables to be in the expected
"addr ~elem~ map .." form. The previous definition was not wrong, but
the lemmas in Retype_R expect the set membership form.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 spec/design/skel/AARCH64/ArchIntermediate_H.thy | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/spec/design/skel/AARCH64/ArchIntermediate_H.thy b/spec/design/skel/AARCH64/ArchIntermediate_H.thy
index 424e2d0b5..016a51f40 100644
--- a/spec/design/skel/AARCH64/ArchIntermediate_H.thy
+++ b/spec/design/skel/AARCH64/ArchIntermediate_H.thy
@@ -31,8 +31,9 @@ private abbreviation (input)
       addrs \<leftarrow> createObjects regionBase numObjects (injectKO objectProto) tableSize;
       pts \<leftarrow> return (map (PPtr \<circ> fromPPtr) addrs);
       modify (\<lambda>ks. ks \<lparr>ksArchState :=
-                         ksArchState ks \<lparr>gsPTTypes :=
-                                           gsPTTypes (ksArchState ks) (regionBase \<mapsto> ptType)\<rparr>\<rparr>);
+                         ksArchState ks \<lparr>gsPTTypes := (\<lambda>addr.
+                                           if addr `~elem~` map fromPPtr addrs then Just ptType
+                                           else gsPTTypes (ksArchState ks) addr)\<rparr>\<rparr>);
       initialiseMappings pts;
       return $ map (\<lambda>pt. cap pt Nothing) pts
     od)"