| Copyright | (c) 2026 Jared Tobin |
|---|---|
| License | MIT |
| Maintainer | Jared Tobin <jared@ppad.tech> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Vestigia.Contract.Arm
Description
Arm's data-independent-timing contract (PSTATE.DIT), encoding by
encoding, generated from Arm's machine-readable specification.
Source
A64 ISA XML for A-profile Architecture, version 2022-12
(package ISA_A64_xml_A_profile-2022-12, sha256
1839a9722eab26aa3bdcd91adeeaf2e6c5c6df085f0e096f949c55cbee7d1a5a),
retrieved 2026-10-27 from the Internet Archive mirror of Arm's
exploration-tools release,
archive.org/details/arm-xml-a-profile-2022-12, its md5
matching the mirror's record.
Rule
Every encoding of every A64 instruction section (type
instruction, one per file) of the general, Advanced SIMD,
floating-point, SIMD&FP load/store, and system classes; SVE and SME
are left out. An instruction is covered exactly when its section's
<operationalnotes> name PSTATE.DIT, whose data-processing
note reads:
If PSTATE.DIT is 1: The execution time of this instruction is independent of: The values of the data supplied in any of its registers. The values of the NZCV flags.
An encoding's fixed bits are its class's register diagram with the
encoding's own boxes over it. One not covered is control flow or
system (Control) where its pseudocode lies under
aarch64/instrs/branch/ or aarch64/instrs/system/, or
its section is of the system class; otherwise it is Outside, with
its source registers: the five-bit register fields its assembler
template names whose explanation is neither destination-only nor
an address (a base register, or one holding an address).