package octez-libs
module S = Csir.Scalar
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.
module type NUM = sig ... end
Numeric operations over the native field.
module type BOOL = sig ... end
module type COMMON = sig ... end
module type Limb_list = sig ... end
module type LIB = sig ... end
The LIB
module type extends the core language defined in Lang_core.COMMON
by adding functions that build upon those primitives.
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 theLibCircuit
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 ofCsir
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.
module LibResult : sig ... end
Pure-value backend. Used to check the semantics of LibCircuit
in the tests.
module LibCircuit : sig ... end
Circuit producing backend.
module Gadget : sig ... end
include module type of struct include Gadget end
module type HASH = Gadget.HASH
module Anemoi128 = Gadget.Anemoi128
module AnemoiJive_128_1 = Gadget.AnemoiJive_128_1
module Poseidon128 = Gadget.Poseidon128
module Poseidon252 = Gadget.Poseidon252
module PoseidonFull = Gadget.PoseidonFull
module Merkle = Gadget.Merkle
module Merkle_narity = Gadget.Merkle_narity
module JubjubEdwards = Gadget.JubjubEdwards
module JubjubWeierstrass = Gadget.JubjubWeierstrass
module Schnorr = Gadget.Schnorr
module Edwards25519 = Gadget.Edwards25519
module Ed25519 = Gadget.Ed25519
module Blake2s = Gadget.Blake2s
module ArithMod25519 = Gadget.ArithMod25519
module ArithMod64 = Gadget.ArithMod64
module Sha256 = Gadget.Sha256
module Sha512 = Gadget.Sha512
module Utils : sig ... end
module Linear_algebra : sig ... end
module Optimizer : sig ... end
module Solver : sig ... end
This module defines a description format and interpretation of the programs needed to populate the PlonK witness for a Plompiler circuit given the initial inputs.
module Bounded : sig ... end
module Csir : sig ... end