riscv machine+haskell: kernelELFPAddrBase change

Proof update for seL4/seL4#759 -- the main visible effect is that the definition of kernelELFPAddrBase changes. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Mar 3, 2025 · fc640c9 · fc640c9
1 parent f10a3c6
commit fc640c9
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/spec/haskell/src/SEL4/Machine/Hardware/RISCV64.hs b/spec/haskell/src/SEL4/Machine/Hardware/RISCV64.hs
@@ -93,7 +93,7 @@ pptrTop :: VPtr
 pptrTop = VPtr 0xFFFFFFFF80000000
 
 kernelELFPAddrBase :: PAddr
-kernelELFPAddrBase = toPAddr $ (fromPAddr Platform.physBase) + 0x4000000
+kernelELFPAddrBase = Platform.physBase
 
 kernelELFBase :: VPtr
 kernelELFBase = VPtr $ fromVPtr pptrTop + (fromPAddr kernelELFPAddrBase .&. (mask 30))

diff --git a/spec/machine/RISCV64/Platform.thy b/spec/machine/RISCV64/Platform.thy
@@ -116,7 +116,7 @@ lemma "kdevBase = 0xFFFFFFFFC0000000" (* Sanity check with C *)
 
 definition kernelELFPAddrBase :: machine_word
   where
-  "kernelELFPAddrBase = physBase + 0x4000000"
+  "kernelELFPAddrBase = physBase"
 
 definition pptrTop :: machine_word
   where