package octez-libs

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

• 1. Introducing next-gate selectors qlg, qrg and/or qog, which lead to a more compact representation of sums (linear combinations).

• 2. Reusing shared-wires among different constraints.

• 3. Compacting blocks which operate on independent wires.

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

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.

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.

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)

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

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

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.

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

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.

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.

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.

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

• 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]

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

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