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

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

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct