adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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>
This commit is contained in:
Gerwin Klein 2023-07-18 17:55:56 +07:00
parent e74d5fe4b8
commit 4913aa8af9
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
spec/design/skel/AARCH64/ArchIntermediate_H.thy
View File

@ -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)"