adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/spec
History
Gerwin Klein 55bf10c1ab
aarch64 aspec+ainvs: provide+use symbolic ppn_len definition 
We initially wanted to move ucast_ucast_ppn to Kernel_Config_Lemmas.
This doesn't work, because ppn is only defined in Arch_Structs_A, but
it turns out that ppn_len is exactly the term `ipa_size - pageBits`
that the lemma needs, so instead of moving the lemma up, we make its
proof generic by providing the symbolic form of `ppn_len` instead.

This still unfolds Kernel_Config.config_ARM_PA_SIZE_BITS_40, but it
does so only trivially and directly where ppn_len is defined.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2023-02-06 09:56:37 +11:00
..
abstract aarch64 aspec+ainvs: provide+use symbolic ppn_len definition 2023-02-06 09:56:37 +11:00
capDL spec+proofs+autocorres: theory import fixes 2023-01-24 11:30:06 +11:00
cspec all: adjust theory imports for TypHeapLib change 2023-01-25 10:13:45 +11:00
design aarch64 aspec+design: import flush_type from Haskell 2023-02-06 09:56:35 +11:00
haskell aarch64 haskell: port associateVCPUTCB fix from ARM_HYP 2023-02-06 09:56:35 +11:00
machine arm_hyp+aarch64 machine: use standard machine op naming scheme 2023-02-06 09:56:36 +11:00
sep-abstract license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
take-grant isabelle2021-1: global hide_lams -> opaque_lifting 2022-03-29 08:38:25 +11:00
Makefile Makefiles: remove unused report-regression target 2022-06-03 09:36:43 +10:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
ROOT isabelle2021-1: DSpec 2022-03-29 08:38:25 +11:00
tests.xml run_tests: increase timeout for Haskell kernel 2022-05-02 12:54:10 +10:00

README.md

Formal Specifications of seL4

See the sub directories for more details.

The Makefile and ROOT file define runnable Isabelle sessions for these specifications.