package octez-libs

  1. Overview
  2. Docs
package octez-libs
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct