LibCircuit (mavkit-libs.Plompiler.LibCircuit)

include LIB

type scalar

Element of the native scalar field.

type input_kind = [

| `InputCom
| `Public
| `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 = [

| input_kind
| `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

val deserialize : S.t array -> 'a Input.t -> 'a Input.t

deserialize scalars inpt populates the structure of inpt with the values from scalars.

val get_inputs : 'a repr t -> S.t array * int

get_inputs c returns the initial inputs for the computation c, together with the number of those inputs that are public. This fuction is useful when the inputs used for the circuit definition have meaningful values (in contrast to the often used dummy inputs, as explained in Lang_core.COMMON.Input).

type cs_result = {

nvars : int;
(*
Number of variables in the cs witness
*)
free_wires : int list;
(*
Wire indices that are not used in the cs, they have been freed by the optimizer.
*)
cs : Csir.CS.t;
(*
Constraint system
*)
public_input_size : int;
input_com_sizes : int list;
(*
Sizes for input commitments
*)
tables : Csir.Table.t list;
(*
Tables for lookups
*)
range_checks : (int * (int * int) list) list;
(*
Range checks following the format: index of wire * (index in wire * bound)
*)
range_checks_labels : (string list * int) list;
(*
label trace that creates a range-check and the size of the range-check
*)
solver : Solver.t;
(*
Solver for the cs
*)

}

Constraint system and auxiliary data resulting from a Plompiler program.

val cs_result_t : cs_result Repr.t

val get_cs : ?optimize:bool -> 'a repr t -> cs_result

get_cs ?optimize c runs the computation c generating a constraint system. If optimize is true, it will run the optimizer on the produced CS. The optimized CS will be cached in Utils.circuit_dir, using the TMPDIR environment variable.