l4v/spec/machine/

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

• 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.

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

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