Plompiler.Optimizer
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).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.
type constr = Csir.CS.raw_constraint
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 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 = {
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 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
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) ->
'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
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
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:
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:(Mavryk_bls12_381.Fr.t * int) list ->
next:(Mavryk_bls12_381.Fr.t * 'a) list ->
Mavryk_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
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 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