Module common_subexpression

The CommonSubexpressionOptimizer: a meta-transformer which factors common subexpressions out of a Circuit into intermediate witnesses, reducing the total number of opcodes.

The name comes from its net effect. The sub-passes below collectively detect subexpressions that the circuit computes more than once and bind each of them to a single intermediate witness, so the value is constrained once and then reused. csat::CSatTransformer is the pass that forms the candidate subexpressions (by slicing wide expressions into backend-width-sized chunks, caching identical chunks so the same subexpression maps to the same witness), and merge_expressions::MergeExpressionsOptimizer is the pass that discards the candidates which turned out not to be common (those used in only two opcodes are merged back). What survives are the genuinely shared subexpressions.

On opcode “width”

Several passes here are parameterized by a width. This is not a hard upper bound on the size of an emitted opcode: ACIR places no limit on how many terms an AssertZero opcode may contain, and proving backends are expected to handle linear combinations of unbounded width. The width is a heuristic target that controls the granularity at which the csat::CSatTransformer slices expressions, which in turn determines which subexpressions become reuse candidates. Because it is only a target, an emitted opcode may legitimately exceed it — see csat::CSatTransformer for the cases where this happens (e.g. an opcode whose sole unknown sits inside a multiplication term, which cannot be sliced without making the circuit unsolvable). Solvability, checked by crate::compiler::CircuitSimulator, is the property these passes actually preserve; width is not.

Sub-passes

CSAT: slices AssertZero opcodes towards the backend’s preferred width.

For instance, with a width of 4, the AssertZero opcode x1 + x2 + x3 + x4 + x5 - y = 0 is sliced using 2 intermediate variables (z1, z2):

x1 + x2 + x3 = z1
x4 + x5 = z2
z1 + z2 - y = 0

If x1,..x5 are inputs to the program, they are tagged as ‘solvable’, and would be used to compute the value of y. If we generated the intermediate variable x4 + x5 - y = z3 instead, we would get an unsolvable circuit because that AssertZero opcode has two unknown values: y and z3. So the CSAT transformation keeps track of which witnesses would be solved for each opcode in order to only generate solvable intermediate variables. Identical slices are cached, so a subexpression appearing in several opcodes is assigned a single shared intermediate witness — this is where the common subexpressions are formed.

Eliminate intermediate variables

The ‘eliminate intermediate variables’ pass will remove any intermediate variables (for instance created by the previous transformation) that are used in exactly two AssertZero opcodes. This results in arithmetic opcodes having linear combinations of potentially large width. For instance if the intermediate variable is z1 and is only used in y:

z1 = x1 + x2 + x3
y = z1 + x4

We remove it, undoing the work done during the CSAT transformation: y = x1 + x2 + x3 + x4.

We do this because the backend is expected to handle linear combinations of ‘unbounded width’ in a more efficient way than the ‘CSAT transformation’. However, it is worthwhile to keep an intermediate variable if it is used in more than two opcodes: that is precisely a common subexpression, and materializing it once is cheaper than recomputing it in each opcode.

redundant_range

The ‘range optimization’ pass, from the optimizers module, will remove any redundant range opcodes.

Modules

csat 🔒

merge_expressions 🔒

Structs

WitnessFolder 🔒

Fold all witnesses in a circuit.

Constants

DEFAULT_EXPRESSION_WIDTH 🔒

DEFAULT_MAX_TRANSFORMER_PASSES 🔒

We use multiple passes to stabilize the output in many cases

Functions

max_witness 🔒

Find the witness with the highest ID in the circuit.

transform_internal 🔒

Applies backend specific optimizations to a Circuit.

transform_internal_once 🔒

Accepts an injected acir_opcode_positions to allow transformations to be applied directly after optimizations.