We present Tinyrossa, an experimental compilation framework which is part of our larger “Smalltalk-25” program of research towards constructing dynamic-language VMs using formal methods. It performs JIT- and AoT-compilation based around OMR’s Testarossa Intermediate Language. As far as compilation per se, Tinyrossa does not make novel contributions; it is a traditional compiler that performs IL-to-IL and IL-to-Native code transformations. The main point of our work is to treat existing compilation algorithms within a mathematically-rigorous framework of executable logical specifications.

Each IL-to-IL and IL-to-Native transformation is a derivation rule. Every transformation rule’s soundness is automatically justified as a theorem in “MachineArithmetic” which is our implementation of refinement calculus. The core of MachineArithmetic is a Horn solver implementing Rondon–Kawaguchi–Jhala’s “Logically-Qualified Data Types” over the Z3 SMT checker using standard algorithms. On top of this core, we mount a calculus of program refinements. This calculus endows Smalltalk objects with a defined game-theoretic semantics.

We start from formalizing the Testarossa IL in a Plotkin-style small-step structural semantics. Next, Charguéraud’s logical reflection in the refinement calculus infers the Testarossa IL program’s axiomatic (Floyd–Hoare-style) verification conditions. The latter are then checked by reducing them to an SMT tautology, thus justifying the IL-to-IL transformation rule.

Justifying IL-to-Native code instruction selection rules is more complex: IL semantics aside, we also need the semantics of the target processor comprising (1) the ISA semantics and (2) the relaxed memory semantics. We obtain ISA semantics by reading the ISA’s “Sail” specification. We ignore memory semantics for now. Bisimilarity between the Testarossa IL and the native code is then established using standard methods.

Tinyrossa is an ongoing research effort. The complete Smalltalk source code for Tinyrossa, MachineArithmetic and all other parts of our system are available on GitHub under the MIT license. In this workshop talk, we present our current status using an example walking through the compilation of a simple method down to optimized native RISC-V code.