secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-L4.verified/spec/machine
History
Gerwin Klein be238597cc arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 
The value of gicNumTargets_bits was wrong for GICv3 platforms, breaking
CRefine for those platforms.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2025-07-07 19:19:20 +10:00
..
AARCH64 arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 2025-07-07 19:19:20 +10:00
ARM arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 2025-07-07 19:19:20 +10:00
ARM_HYP arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 2025-07-07 19:19:20 +10:00
RISCV64 riscv machine+haskell: kernelELFPAddrBase change 2025-03-03 14:35:15 +11:00
X64 x64 machine: remove unused cacheLineBits 2024-09-24 22:24:08 +02:00
Kernel_Config_Lemmas.thy machine+aspec: add Arch_Kernel_Config_Lemmas 2023-03-29 10:04:47 +11:00
MachineExports.thy machine: requalify more machine op consts and types 2024-08-19 10:34:09 +02:00
MachineMonad.thy machine+aspec: use arch_requalify commands 2024-08-08 18:05:03 +10:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
Setup_Locale.thy isabelle-2021: update Lib 2021-09-30 16:53:17 +10:00

README.md

The Machine Interface Specification of seL4

l4v/spec/machine/

This directory contains the Isabelle sources for the machine interface specification used in the abstract and design specifications of seL4.

Overview

  • ARMMachineTypes: ARM register set and related definitions.
  • MachineOps: definitions for the machine interface functions. Most interface functions are left non-deterministic. Some are assumed not to mutate C-observable state, others are defined in more detail.
  • MachineTypes: entry point to select a machine. Currently ARM only.
  • Platform: word size and other basic platform definitions.

Building

This module is not built in isolation, but included in the ASpec and ExecSpec sessions.

Remarks

  • the theory ARMMachineTypes is generated from Haskell using the tool in tools/haskell-translator and the skeleton file in spec/design/m-skel.