Module Plompiler

Plompiler core language.

The COMMON module type defines the set of primitives needed to interpret a Plompiler program. This module type provides the monadic interface needed to deal with Plompier computations, and a number of sub-modules to handle inputs and basic types.

Plompiler is an OCaml eDSL for writing PlonK arithmetic circuits (see Lib_plonk.Main_protocol for an introduction to PlonK circuits).

The eDSL is implemented following a tagless-final approach and is split into a core language and a standard library, each described as a module type. The core is defined by Lang_core.COMMON while the standard library is defined by Lang_stdlib.LIB.

The Plompiler library is defined around three main parameterized types. First, 'a t is a monadic type that represents a Plompiler computation returning a value of type 'a. Second, 'a repr is the Plompiler representation of a value of type 'a. Finally, 'a input represents an input to a circuit of type 'a. These two final types are related: an 'a input will become an 'a repr once inputted into a circuit.

A Plompiler program, then, will be a functor over LIB. The general structure of of a Plompiler program is:

module Program (L : LIB) = struct
  open L

  let logic : 'a repr -> 'b repr -> unit repr t = ...

  let prog : 'a input -> 'b input -> unit repr t =
    fun a b ->
      let* a = input ~kind:'Public a in
      let* b = input b in
      logic a b
end

Here, the first function defines the logic of the program, while prog declares the inputs, the first of which is public.

A module implementing the `LIB` signature can be seen as an interpreter of the language. Concretely, two such interpreters are defined: LibResult and LibCircuit. The first runs a Plompiler program with pure values, i.e. without generating a circuit. This means that, for this interpreter, 'a repr is essentially 'a. The second, LibCircuit, is the actual circuit backend. Here, 'a repr will represent a PlonK wire carrying a value of type 'a.

The rest of the library is implemented through the following modules:

• Csir: defines the Constraint System intermediate representation, which is an abstract representation for PlonK constraint systems. This is the target of the LibCircuit interpreter, and can be converted into a PlonK circuit.
• Encoding: encoders/decoders for usage of structured data types in circuits. Simplifies data manipulation and the definition of inputs.
• Optimizer: low-level generic optimizer of Csir constraint systems.
• Solver: description and interpretation of the programs needed to populate the PlonK witness for a Plompiler circuit given the initial inputs.
• Gadget_X: building blocks for circuits, mainly implementing cryptographic primitives.