package octez-libs

  1. Overview
  2. Docs
package octez-libs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val list_map : ('a -> 'b) -> 'a list -> 'c list

The optimizer simplifies a constraint system, producing an equivalent one with fewer constraints in essentially three ways:

Optimization Rules

Introducing next-gate selectors

In a system with 3-wires architecture, adding (in a linear combination) n elements requires n-1 constraints. For example, computing out = 1 + 2 x1 + 4 x2 + 8 x3 + 16 x4 + 32 x5 can be implemented in 4 constraints as follows:

{ a = x1;   b = x2;   c = aux1; identity = [ql 2; qr 4; qo -1; qc 1] };
{ a = x3;   b = x4;   c = aux2; identity = [ql 8; qr 16; qo -1] };
{ a = x5;   b = aux1; c = aux3; identity = [ql 32; qr 1; qo -1] };
{ a = aux2; b = aux3; c = out;  identity = [ql 1; qr 1; qo -1] };

Instead, by using next-gate selectors, a linear combination of n terms can be implemented in (n-1)/2 constraints. In this case, just two:

{ a = x1; b = x2; c = out; identity = [ql 2; qr 4; qlg 8; qrg 16; qog 32; qo -1; qc 1] };
{ a = x3; b = x4; c = x5;  identity = [] };

Reusing shared-wires

Remarkably, two linear combinations that involve some common wires can be implemented more efficiently if they are handled together. For example, out1 = 5 x + 3 y + 9 z and out2 = 2 x - 3 y + 7 t can be implemented with 3 constraints (instead of 4) as follows:

{ a = z;        c = out1; identity = [ql 9; qlg 5; qrg 3; qog -1] };
{ a = x; b = y; c = out2; identity = [ql 2; qr -3; qrg 7; qog -1] };
{        b = t;         ; identity = [] };

Furthermore, observe how, conveniently, some wires in the above constraints are unbound, which can lead to our next optimization.

Compacting blocks

Consider a gate which only takes one wire as input, e.g. for computing out3 = 3 w + 1, implemented with constraint:

{ a = w;        c = out3; identity = [ql 3; qo -1; qc 1] }

This constraint can be merged with our previous block, which only uses wire b in its last constraint and has unbound selectors for it:

{ a = z;        c = out1; identity = [ql 9; qlg 5; qrg 3; qog -1] };
{ a = x; b = y; c = out2; identity = [ql 2; qr -3; qrg 7; qog -1] };
{ a = w; b = t; c = out3; identity = [ql 3; qo -1; qc 1] };

Algorithm

The optimization proceeds in several steps:

1. Collect information about all linear constraints/gates (see is_linear), including the number of occurrences of their output wire among the circuit.

2. Inline any linear_computation whose output is used only once among the circuit, in the computation where it is used (only if the latter is also linear).

3. Transform any non-inlined linear computation into a pseudo_block and join pseudo blocks that share at least a wire (preferably two wires).

4. Transform pseudo blocks to actual blocks (also considering the non-linear computations that were left aside) and join blocks that operate on independent wires together.

val nb_wires_arch : int
type scalar = Csir.Scalar.t
val scalar_t : Csir.Scalar.t Repr.t
type block = constr array
type term = scalar * int
val term_t : (Csir.Scalar.t * int) Repr.t
type trace_info = {
  1. free_wires : int list;
  2. assignments : (int * term list) list;
}

Type to store the trace_updater information. free_wires represents a list of indices of wires that have been removed from the system and have not been used again for auxiliary computations. If a free wire w is used to store an auxiliary linear computation on some terms, it is removed from free_wires and the pair (v, terms) is added to the list of assignments.

val trace_info_t : trace_info Repr.t
type pseudo_constr = {
  1. pc_head : term list;
  2. pc_body : term list;
  3. pc_tail : term list;
  4. pc_const : Csir.Scalar.t;
}

A pseudo constraint represents an equation between an arbitrary number of terms. In particular, adding all terms from its head, body, tail and its constant term should produce 0. The length of pc_head and pc_tail should never exceed nb_wires_arch.

type pseudo_block = pseudo_constr list

A pseudo block is a list of pseudo constraints that have been groupped in order to apply the Reusing shared-wires heuristic. The constraints in a pseudo block satisfy (by construction) the invariant the pc_head of a constraint starts with the pc_tail of the previous one (when considering the term variables, coefficients may be different). Note that the pc_head may contain extra terms that do not appear in the previous pc_tail. This invariant is important for block_of_pseudo_block to be correct

val join_list : join:('a -> 'a -> 'a option) -> int -> 'a -> 'a list -> 'a list option

join_list ~join scope x xs joins x with another element among the first scope elements of the list of candidates xs, or returns None if no union was possible. This function may not preserve the order in xs

val combine_quadratic : scope:int -> join:('a -> 'a -> 'a option) -> 'a list -> 'a list

combine_quadratic ~join xs takes a list of elements xs and returns a (potentially) shorter list xs' where some of the elements have been combined according to join. join x x' is None if x and x' cannot be combined and it is Some union otherwise. This algorithm tries to combine every element of xs with any other element by greedily trying all possible n choose 2 different pairings of elements, where n is the length of xs.

val combine_quadratic_efficient : scope:int -> join:('a -> 'a -> 'a option) -> 'b list -> 'a list -> 'c list

Similar to combine_quadratic, but more efficient. Takes a list of top_candidates that will each be tried to be combined with rest. This function may not preserve the order in rest

val add_terms : term list -> term list -> term list

Concatenates two lists of terms, merging terms with the same wire identifier (by adding their coefficients)

val inline : int -> from:int -> into:int -> term list array -> unit

inline w ~from ~into linear takes an array of linear constraints (a linear constraint is represented by list of terms), solves for wire w in constraint linear.(from) and substitutes wire w by the result in constraint linear.(into). linear.(from) is left empty. This routine should only be called if w does not appear in any other constraint. In that case, constraint linear.(from) can then be removed and wire w is said to be "free".

module IMap : sig ... end

The keys are wire indices and the values lists of constraints indices, such that the wire appears in each of the constraints.

module ISet : sig ... end
val increase_occurrences : 'a list IMap.t -> 'b -> ('c * IMap.key) list -> 'a list IMap.t

Auxiliary function used in inline_linear.

increase_occurrences map i terms updates map by adding i to the list of occurrences of wire w for every (_, w) in terms.

val pseudo_block_of_terms : term list -> pseudo_constr list

Creates a pseudo block with all terms in the body except for the wire -1 which is set as constant.

val inline_linear : nb_inputs:IMap.key -> range_checked:Plompiler__.Range_checks.t -> Csir.CS.raw_constraint array list -> pseudo_constr list list * Csir.CS.raw_constraint array list * IMap.key list

Returns a list of linear gates that have possibly been inlined, the list of wires that were inlined (and thus freed) and the list of unchanged non-linear gates. The wires selected for inlining must:

  • appear in exactly two linear gates of size one
  • not be inputs
  • not be range-checked The inlined linear gates are returned as pseudo blocks because they may need to be split again to fit 3 wires.
val place_over_pseudo_block : perfectly:bool -> pseudo_constr list -> pseudo_constr list -> pseudo_constr list option

place_over_pseudo_block ~perfectly b1 b2 tries to join pseudo block b1 on top of b2, i.e., link the last pseudo constraint of b1 with the first pseudo constraint of b2. It returns an optional argument containing the combined pseudo block if the combination was successful. perfectly is a Boolean argument that specifies whether only "perfect" matches should be accepted. In this context, "perfect" means that the two constraints to be combined share exactly nb_wires_arch wires.

val combine_pseudo_blocks : scope:int -> perfectly:bool -> pseudo_constr list list -> pseudo_constr list list
val linear_combination : this:(Bls12_381.Fr.t * int) list -> next:(Bls12_381.Fr.t * 'a) list -> Bls12_381.Fr.t -> Csir.CS.raw_constraint
val dummy_linear_combination : ('a * int) list -> Csir.CS.raw_constraint
val block_of_pseudo_block : trace_info -> pseudo_constr list -> trace_info * Csir.CS.raw_constraint array * pseudo_constr list list

Given a pseudo block, i.e., a list of pseudo constraints, transform it into a block. Thanks to the invariant that the pc_head of a pseudo constraint starts with the pc_tail of the previous one, it is enough to add a constraint for each pc_head (and encode each pc_tail with next-gate selectors). Note that pc_bodies may need to be freed through auxiliary variables.

val blocks_of_pseudo_blocks : scope:int -> int list -> pseudo_constr list list -> trace_info * Csir.CS.raw_constraint array list

This function takes a list of pseudo blocks, combines them if possible and converts them into blocks. This conversion may lead to residue pseudo blocks (if auxiliary variables were involved to free a pc_body). It then applies the same process on the residue pseudo blocks. Observe that it is relatively rare that a residue pseudo block is produced after the convertion. Consequently the second iteration of this function will be among many fewer pseudo blocks and it quickly reaches termination

val place_over_block : perfectly:bool -> block -> block -> block option

place_over_block ~perfectly pb pb' tries to join block b1 on top of b2. It works only if the last constraint of b1 has no selectors. perfectly returns only matches that have no empty selectors (no holes). It is relevant for a heuristic where we first want to find perfect matches and then any match.

The joining is done by

  • finding a permutation that makes the wires of b1.last and b2.first match (being relaxed about unset wires)
  • checking if the permutation if perfect and failing if required
  • renaming the selectors of b1.last
  • renaming the next selectors of b1.second_last

Example: (1 1 1) [ql:a qlg:b] (3 2 -1) [] (2 3 4) [ql:a] (1 1 1) [ql:a] becomes (1 1 1) [ql:a qrg:b] (2 3 4) [ql:a] (1 1 1) [ql:a]

val combine_blocks : perfectly:bool -> block list -> scope:int -> block list
val trace_updater : trace_info -> scalar array -> scalar array

Takes trace_info and returns a function that updates a given trace to make it compatible with the optimized constraints.

val remove_boolean_gates : Csir.CS.raw_constraint array list -> Csir.CS.raw_constraint array list * int list
val add_boolean_checks : boolean_vars:ISet.elt list -> Csir.CS.raw_constraint array list -> Csir.CS.raw_constraint array list
val inline_renamings : nb_inputs:IMap.key -> range_checked:Plompiler__.Range_checks.t -> Csir.CS.raw_constraint array list -> Csir.CS.raw_constraint array list * IMap.key list
val remove_trivial : Csir.CS.raw_constraint array list -> Csir.CS.raw_constraint array list
val optimize : nb_inputs:int -> range_checks:Plompiler__.Range_checks.t -> Csir.CS.gate list -> Csir.CS.gate list * trace_info

Takes a list of raw_constraints and returns an equivalent constraint system with potentially fewer constraints. As a second output, it returns the necessary information to build a function that updates the trace to make it compatible with the new constraints

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