Sail Armv9.4-A ISA properties in Isabelle

This directory contains Isabelle proofs of key properties of the Armv9.4-A ISA related to virtual memory, in particular:

• A soundness proof of a simplified characterisation of address translation with respect to the full Sail specification
• A whole-ISA property that all memory accesses performed by instructions use physical addresses that are the result of address translation (excluding accesses to the page tables themselves)

This and related properties form a key part of the VM abstraction theorem described in the paper "ArchSem: Reusable rigorous semantics of relaxed architectures". The ISA properties used for that proof can be found in the file Translation_Properties.thy in the proofs directory. The proof document in the supplementary material of the ArchSem paper explains those properties in the Section "Isabelle ISA properties".

The other key files in the proofs directory are:

• characterisation_types.lem and characterisation.lem containing the specification of the characterisation in the Lem language
• Characterisation_assumptions.thy contains assumptions on system register values that we make for the soundness proof
• Characterisation_proofs.thy contains the soundness proof of the address translation characterisation
• Accessed_Addresses_Translated_Property.thy contains machinery for proving the whole-ISA properties (with the bulk of the proof being in Accessed_Addresses_Translated_Lemmas.thy, mostly auto-generated by the tool in the tools directory, generating lemmas about all instructions and auxiliary functions in the Sail specification)

The proof requires Isabelle 2025 and the Isabelle definitions generated from the Sail Armv9.4-A specification (which in turn is automatically generated from Arm's Armv9.4-A instruction semantics specification in ASL). A snapshot of the Isabelle specification together with other dependencies (the Sail and Lem libraries, as well as the Word_Lib library from the Archive of Formal Proofs) are in the deps directory.

The proof can either be opened interactively in Isabelle (see below for instructions), or built using the Isabelle build tool with a command like this (executed from this directory):

isabelle build -v -d deps -d proofs Sail-Armv9-Translation

Note, however, that due to the very large size of the Armv9.4-A specification (about 1.2 million lines of Isabelle definitions), running the proof requires a large amount of time and memory. On one of our machines with an Intel Xeon W-2145 CPU, processing the Armv9.4-A specification took around 2 hours, and processing the proofs took roughly another 3 hours, with a peak memory consumption of about 60GB.

We ran Isabelle in 64-bit mode for this proof, with the following setting in $ISABELLE_HOME_USER/etc/preferences

ML_system_64 = "true"

and with a large amount of memory allocated to PolyML and the JVM using the following settings in $ISABELLE_HOME_USER/etc/settings

ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx16g -Xss16m"
ML_OPTIONS="--minheap 4G --maxheap 48G"

For opening the proof interactively, it is useful to process the Arm specification once into an Isabelle heap image to avoid re-processing it every time the proof is opened in Isabelle. The ROOT file in deps/sail-arm contains suitable session definitions. To use them, pass a flag "-l Sail-Armv9" to Isabelle, as in the following command:

isabelle jedit -d deps -d proofs -l Sail-Armv9 proofs/Translation_Properties.thy

Dependencies

The proof has the following dependencies. Snapshots of the required Isabelle theories are provided in the deps directory, taken from the versions or commits listed below.

• Isabelle 2025
• Lem, version 2025-03-13
• Sail, with patches to add Lem/Isabelle support for the ArchSem interface in the lem_interface_v2 branch, at the time of writing in a fork, commit 8c034c420
• Sail-Arm specification of Armv9.4-A, with patches in the archsem-experiment2 branch to use the ArchSem interface, commit 2146aea
• Archive of Formal Proofs, specifically the Word_Lib library, here taken from the version of 2025-09-01.

Licence

The files in this repository are distributed under the BSD 2-clause licence given in LICENCE, except for the bundled third-party dependencies in the deps directory, whose licences are given in THIRD_PARTY_FILES.md.

The proofs in this repository were developed by Thomas Bauereiss, with the theories Trace_Subset and No_Exception originally developed by Thomas Sewell for the T-CHERI proofs about capability architectures.