vestigia-0.2.0: Where an execution depended on a secret.
Copyright(c) 2026 Jared Tobin
LicenseMIT
MaintainerJared Tobin <jared@ppad.tech>
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Synopsis

Documentation

encodings :: [Encoding] Source #

Every encoding, in the specification's file order.