package octez-libs

You can search for identifiers within the package.

in-package search v0.2.0

A package that contains multiple base libraries used by the Octez suite

Install

Dune Dependency

www.tezos.com Readme Edit opam file Versions (5)

Authors

T

Tezos devteam

Maintainers

C

contact@tezos.com

Sources

tezos-octez-v20.1.tag.bz2

sha256=ddfb5076eeb0b32ac21c1eed44e8fc86a6743ef18ab23fff02d36e365bb73d61

sha512=d22a827df5146e0aa274df48bc2150b098177ff7e5eab52c6109e867eb0a1f0ec63e6bfbb0e3645a6c2112de3877c91a17df32ccbff301891ce4ba630c997a65

doc/octez-libs.plompiler/Plompiler/LibCircuit/index.html

Module `Plompiler.LibCircuit`Source

Circuit producing backend.

include LIB

Sourcetype scalar

Element of the native scalar field.

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

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

Sourcetype 'a repr

Representation of values.

Sourcetype 'a t

Plompiler program.

Sourceval ret : 'a -> 'a t

Monadic return.

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

Monadic bind.

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

Monadic sequence operator.

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

Infix map operator.

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

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

Sourcemodule Input : sig ... end

Module for describing inputs to Plompiler circuits.

Sourcetype 'b open_input_com

Type that describes an open input commitment.

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

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

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

Sourceval 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

Sourceval (|:) : ('c repr -> 'd) open_input_com -> 'c Input.t -> 'd open_input_com

ic |: i adds i to the input commitment ic

Sourceval end_input_com : 'a open_input_com -> 'a t

end_input_com ic ends the declaration of an input commitment.

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

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

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

Monadic fold over a list.

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

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

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

of_pair p retrieves the values out of a pair value.

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

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

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

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

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

hd l returns the head of list l

Sourceval unit : unit repr

unit is the unit value.

Sourceval scalar_of_bool : bool repr -> scalar repr

scalar_of_bool b converts a boolean value into a scalar.

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

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

Assertion that two values are (structurally) equal.

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

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

Sourceval scalar_of_limbs : nb_bits:int -> scalar list repr -> scalar repr t

Source

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

Source

val limbs_of_scalar : 
  ?shift:Z.t ->
  total_nb_bits:int ->
  nb_bits:int ->
  scalar repr ->
  scalar list repr t

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

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

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

Module for describing operations over fixed size integers

Sourcemodule Ecc : sig ... end

Addition on ECC curves.

Sourcemodule Mod_arith : sig ... end

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

Sourcemodule Anemoi : sig ... end

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

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

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

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

fold2M is the monadic version of List.fold_left2.

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

mapM is the monadic version of List.map.

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

map2M is the monadic version of List.map2.

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

iterM is the monadic version of List.iter.

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

iter2M is the monadic version of List.iter2.

Sourcemodule Bool : sig ... end

Sourcemodule Num : sig ... end

Sourcemodule Enum (N : sig ... end) : sig ... end

Enumerations, represented as a list of cases.

Sourcemodule Bytes : sig ... end

Representation of bytes.

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

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

Source

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

Sourcemodule Encodings : sig ... end

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

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

Sourceval 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).

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

Sourceval cs_result_t : cs_result Repr.t

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

package octez-libs

Install

Dune Dependency

Authors

Maintainers

Sources

doc/octez-libs.plompiler/Plompiler/LibCircuit/index.html

Module Plompiler.LibCircuitSource

Module `Plompiler.LibCircuit`Source