The optimizer simplifies a constraint system, producing an equivalent one with fewer constraints in essentially three ways:
qlg, qrg and/or qog, which lead to a more compact representation of sums (linear combinations).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 = [] };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.
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] };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.
type constr = Csir.CS.raw_constrainttype scalar = Csir.Scalar.tval scalar_t : Csir.Scalar.t Repr.ttype block = constr arraytype term = scalar * intval term_t : (Csir.Scalar.t * int) Repr.tType 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.ttype pseudo_constr = {pc_head : term list;pc_body : term list;pc_tail : term list;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 listA pseudo block is a list of pseudo constraints that have been groupped in order to apply the Reusing shared-wires heuristic.Alcotest 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
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
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) ->
'a list ->
'a list ->
'a listSimilar 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
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 -> unitinline 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 ... endThe keys are wire indices and the values lists of constraints indices, such that the wire appears in each of the constraints.
module ISet : sig ... endAuxiliary 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 listCreates 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 ->
Csir.CS.raw_constraint array list ->
pseudo_constr list list * Csir.CS.raw_constraint array list * IMap.key listReturns 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:
val place_over_pseudo_block :
perfectly:bool ->
pseudo_constr list ->
pseudo_constr list ->
pseudo_constr list optionplace_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 listval linear_combination :
this:(Bls12_381.Fr.t * int) list ->
next:(Bls12_381.Fr.t * 'a) list ->
Bls12_381.Fr.t ->
Csir.CS.raw_constraintval dummy_linear_combination : ('a * int) list -> Csir.CS.raw_constraintval block_of_pseudo_block :
trace_info ->
pseudo_constr list ->
trace_info * Csir.CS.raw_constraint array * pseudo_constr list listGiven 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 listThis 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
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
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 trace_updater : trace_info -> scalar array -> scalar arrayTakes 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 listval add_boolean_checks :
boolean_vars:ISet.elt list ->
Csir.CS.raw_constraint array list ->
Csir.CS.raw_constraint array listval inline_renamings :
nb_inputs:IMap.key ->
Csir.CS.raw_constraint array list ->
Csir.CS.raw_constraint array list * IMap.key listval remove_trivial :
Csir.CS.raw_constraint array list ->
Csir.CS.raw_constraint array listval optimize :
nb_inputs:int ->
Csir.CS.gate list ->
Csir.CS.gate list * trace_infoTakes 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