Parameter Sha256.L

type scalar

Element of the native scalar field.

type input_kind = [
  1. | `InputCom
  2. | `Public
  3. | `Private
]

Inputs to a plompiler program have three kinds:

  • Public: known by both the prover and verifier.
  • Private: known only by the prover.
  • InputCom: part of an Input Commitment. See Lib_plonk.Input_commitment.
type trace_kind = [
  1. | input_kind
  2. | `NoInput
]

The trace is the sequence of scalar values used in a Plompiler program. It includes the inputs and the intermediary variables. Inputs have to be a prefix of the trace, and public inputs come before private ones.

type 'a repr

Representation of values.

type 'a t

Plompiler program.

val ret : 'a -> 'a t

Monadic return.

val let* : 'a t -> ('a -> 'b t) -> 'b t

Monadic bind.

val (>*) : unit repr t -> 'a t -> 'a t

Monadic sequence operator.

val (<$>) : 'a t -> ('a -> 'b) -> 'b t

Infix map operator.

val with_bool_check : bool repr t -> unit repr t

with_bool_check c adds an implicit boolean check computed by c to the circuit. The computation of this check is delayed until the end of the circuit construction, which is useful for defining complex conditions while still processing inputs.

val get_checks_wire : bool repr t

get_checks_wire retrieves the boolean representing the conjunction of all previous implicit checks.

WARNING: This will "reset" the implicit check accumulator.

module Input : sig ... end

Module for describing inputs to Plompiler circuits.

type 'b open_input_com

Type that describes an open input commitment.

val serialize : 'a Input.t -> Csir.Scalar.t array

serialize i returns the array of scalars corresponding to its values.

val input : ?kind:input_kind -> 'a Input.t -> 'a repr t

input ~kind i declares an input of a given kind to the Plompiler program. It returns a Plompiler representation of the inputted value.

val begin_input_com : 'b -> 'b open_input_com

begin_input_com builder starts a new input commitment. builder is a function that takes the inputs to be committed one by one and returns the composite commitment.

An example of usage is

let* x1, x2 =
  begin_input_com (fun a b -> (a, b))
  |: Input.scalar x1 |: Input.scalar x2 |> end_input_com
in
val (|:) : ('c repr -> 'd) open_input_com -> 'c Input.t -> 'd open_input_com

ic |: i adds i to the input commitment ic

val end_input_com : 'a open_input_com -> 'a t

end_input_com ic ends the declaration of an input commitment.

val eq : 'a repr -> 'a repr -> bool

eq a b returns the physical equality of a and b. Handle with care.

val foldM : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t

Monadic fold over a list.

val pair : 'a repr -> 'b repr -> ('a * 'b) repr

pair x y makes a pair value out of two values.

val of_pair : ('a * 'b) repr -> 'a repr * 'b repr

of_pair p retrieves the values out of a pair value.

val to_list : 'a repr list -> 'a list repr

to_list l makes a list value out of a list of values.

val of_list : 'a list repr -> 'a repr list

of_list v retrieves a list of Plompiler values out of a list value.

val hd : 'a list repr -> 'a repr t

hd l returns the head of list l

val unit : unit repr

unit is the unit value.

val scalar_of_bool : bool repr -> scalar repr

scalar_of_bool b converts a boolean value into a scalar.

val unsafe_bool_of_scalar : scalar repr -> bool repr

unsafe_bool_of_scalar s converts a scalar value into a bool.

WARNING: s is expected to hold the values 0 or 1, but this is not checked.

val assert_equal : 'a repr -> 'a repr -> unit repr t

Assertion that two values are (structurally) equal.

val equal : 'a repr -> 'a repr -> bool repr t

equal a b computes the structural equality between a and b.

val scalar_of_limbs : nb_bits:int -> scalar list repr -> scalar repr t
val bits_of_scalar : ?shift:Z.t -> nb_bits:int -> scalar repr -> bool list repr t

Returns a list of Boolean variables representing the little endian bit decomposition of the given scalar (with the least significant bit on the head).

val limbs_of_scalar : ?shift:Z.t -> total_nb_bits:int -> nb_bits:int -> scalar repr -> scalar list repr t
val with_label : label:string -> 'a t -> 'a t

with_label ~label c adds a label to the Plompiler computation c. Useful for debugging and flamegraphs.

val debug : string -> 'a repr -> unit repr t

Prints on stdout the prefix string and the repr. It works only when running the Result interpreter, it has no effect in the Circuit interpreter.

module Limb (N : sig ... end) : sig ... end

Module for describing operations over fixed size integers

module Ecc : sig ... end

Addition on ECC curves.

module Mod_arith : sig ... end
module Poseidon : sig ... end

Helper functions for the Poseidon Hash defined over the scalar field of the BLS12-381 curve, using S-box function x -> x^5.

module Anemoi : sig ... end

Helper functions for the Anemoi Hash defined over the scalar field of the BLS12-381 curve.

val foldiM : ('a -> int -> 'a t) -> 'a -> int -> 'a t

foldiM is the monadic version of a fold over a natural number.

val fold2M : ('a -> 'b -> 'c -> 'a t) -> 'a -> 'b list -> 'c list -> 'a t

fold2M is the monadic version of List.fold_left2.

val mapM : ('a -> 'b t) -> 'a list -> 'b list t

mapM is the monadic version of List.map.

val map2M : ('a -> 'b -> 'c t) -> 'a list -> 'b list -> 'c list t

map2M is the monadic version of List.map2.

val iterM : ('a -> unit repr t) -> 'a list -> unit repr t

iterM is the monadic version of List.iter.

val iter2M : ('a -> 'b -> unit repr t) -> 'a list -> 'b list -> unit repr t

iter2M is the monadic version of List.iter2.

module Bool : sig ... end
module Num : sig ... end
module Enum (N : sig ... end) : sig ... end

Enumerations, represented as a list of cases.

module Bytes : sig ... end

Representation of bytes.

module Limbs (N : sig ... end) : sig ... end

This module is a more generic version of Bytes, where each scalar stores an nb_bits-bit number.

val add2 : (scalar * scalar) repr -> (scalar * scalar) repr -> (scalar * scalar) repr t

add2 p1 p2 returns the pair (fst p1 + fst p2, snd p1 + snd p2).

module Encodings : sig ... end