This repo contains tools for machine reasoning about the ISA semantics of processors. These tools are part of our larger Smalltalk-25 project (described e.g. in our Towards a Dynabook for verified VM construction paper), which uses them for verification of the Tinyrossa compiler and for synthesis of the PIG superoptimizer.
There exists a long tradition of mechanized reasoning about processor semantics. In the recent decade, the field has enjoyed significant progress. We have advanced from ad-hoc fragmentary axiomatizations and vendors' semi-formal specification documents, to systems such as Armstrong et al.'s Sail / Isla which compute with full-scale authoritative definitions taking into accout both sequential and nondeterministic aspects of the semantics.
Our tooling builds on top of Armstrong et al.'s Isla and Alglave et al.'s Cat. We take Jib IR and from there we have a few usage scenatios:
- proving invariants about running code by transforming into MachineArithmetic core; or
- the simpler scenario of simulating a sequential machine by symbolic interpretation.
One would wish to hope that formal semantics specifications were available for all ISAs of interest (RISC-V, OpenPOWER, AArch64, MIPS) via some uniform way; unfortunately, this is not the case, therefore we have to consider alternative forms of ISA definitions.
For example, even if the now-deprecated partial Sail definition of POWER were alive, the authoritative definition is still the detailed pseudocode in the "Green Cloth". Libre-SOC OpenPOWER core machine-processes this pseudocode to arrive at "ISACaller"; we adopt this to serve as our POWER definition.