package octez-libs
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
.
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.
val ret : 'a -> 'a t
Monadic return.
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.
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.
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.
eq a b
returns the physical equality of a
and b
. Handle with care.
of_pair p
retrieves the values out of a pair value.
of_list v
retrieves a list of Plompiler values out of a list value.
val unit : unit repr
unit
is the unit value.
scalar_of_bool b
converts a boolean value into a scalar.
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.
Assertion that two values are (structurally) equal.
equal a b
computes the structural equality between a
and b
.
Returns a list of Boolean variables representing the little endian bit decomposition of the given scalar (with the least significant bit on the head).
with_label ~label c
adds a label
to the Plompiler computation c
. Useful for debugging and flamegraphs.
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 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.
foldiM
is the monadic version of a fold over a natural number.
fold2M
is the monadic version of List.fold_left2
.
map2M
is the monadic version of List.map2
.
iter2M
is the monadic version of List.iter2
.
module Bool : sig ... end
module Num : sig ... end
module Bytes : sig ... end
Representation of bytes.
This module is a more generic version of Bytes, where each scalar stores an nb_bits
-bit number.
add2 p1 p2
returns the pair (fst p1 + fst p2, snd p1 + snd p2)
.
module Encodings : sig ... end