package octez-libs

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 LIB = sig ... end

The LIB module type extends the core language defined in Lang_core.COMMON by adding functions that build upon those primitives.

module Lib (C : sig ... end) : sig ... end

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.
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
OCaml

Innovation. Community. Security.