Skip to content

vampir

Compiling to VampIR through Geb

Note

The compilation described is currently not supported by the newest version of Juvix and Geb. Changes are forthcoming.

Before, we discussed the standard normalization approach to compiling Juvix programs to VampIR. An alternative backend is provided by the Geb project currently implemented in Lisp providing a categorical view of the needed translations.

The post will be devoted to discussing the core ideas of Geb, the practical steps to take in order to use the corresponding pipeline, as well as the current limitations the backend faces.

We assume basic familiarity with categorical concepts and VampIR.

Geb Pipeline

Geb is a developing language providing a useful interface for specifying categorical constructs and helping define compilers in terms of functors. The approach is inspired by a classical observation that instead of dealing with 'good' compilation procedures one can instead specify functors between appropriate categories representing the languages one initially considers.

In the current state of development, Geb is a fairly simple category in which one can do "basic arithmetic." It is a category freely spanned by terminal/initial objects and finite (co)products with additional constructs for objects representing n-bit natural numbers. The pipeline itself is a string of functors between categories:

  • in vampir
  • 15 min read

Compiling Juvix programs to arithmetic circuits via Vamp-IR

Since version 0.3.5, the Juvix compiler supports the vampir target which generates Vamp-IR input files that can be compiled to various proof systems based on arithmetic circuits, like Plonk or Halo 2. Vamp-IR is a proof-system-agnostic language for writing arithmetic circuits.

In this post, we will not be discussing the details of Vamp-IR or the circuit computation model. Instead, we will describe how high-level functional Juvix programs can be compiled to circuits, what the common pitfalls and current limitations are. The reader is assumed to have at least basic familiarity with Vamp-IR.