package octez-libs

  1. Overview
  2. Docs
package octez-libs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Plompiler.LibResultSource

Pure-value backend. Used to check the semantics of LibCircuit in the tests.

include LIB
Sourcetype scalar

Element of the native scalar field.

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

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

Sourceval 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
Sourceval 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 get_result : 'a repr t -> 'a Input.t

get_result prog runs the Plompiler computation prog and returns its result. The result is wrapped in the Input.t structure as this describes the possible values that Plompiler can deal with.