Tool Guides

Table of Contents

• llzk-opt
  • • • LLZK-Specific Options
  • LLZK Pass Documentation
    • Analysis Passes
      • -llzk-print-call-graph
      • -llzk-print-call-graph-sccs
      • -llzk-print-constraint-dependency-graphs
        • Options
      • -llzk-print-interval-analysis
        • Options
      • -llzk-print-symbol-def-tree
        • Options
      • -llzk-print-symbol-use-graph
        • Options
    • General Transformation Passes
      • -llzk-duplicate-op-elim
      • -llzk-duplicate-read-write-elim
      • -llzk-inline-structs
        • Options
      • -llzk-poly-lowering-pass
        • Options
      • -llzk-r1cs-lowering
      • -llzk-unused-declaration-elim
        • Options
    • 'array' Dialect Transformation Passes
      • -llzk-array-to-scalar
    • 'polymorphic' Dialect Transformation Passes
      • -llzk-drop-empty-params
      • -llzk-flatten
        • Options
    • Validation Passes
      • -llzk-validate-field-writes
• llzk-lsp-server

llzk-opt

llzk-opt is a version of the mlir-opt tool that supports passes on LLZK IR files. You can refer to the mlir-opt documentation for a general overview of the operation of *-opt tooling, but note that many options and passes available in mlir-opt are not available in llzk-opt. llzk-opt -h will show a list of all available flags and options.

LLZK-Specific Options

-I <directory> : Directory of include files

LLZK Pass Documentation

Analysis Passes

-llzk-print-call-graph

Print the LLZK module's call graph.

-llzk-print-call-graph-sccs

Print the SCCs from the LLZK module's call graph.

-llzk-print-constraint-dependency-graphs

Print constraint dependency graph for all LLZK structs.

Options

-intraprocedural : Whether to run the analysis intra-procedurally only (default is false).

-llzk-print-interval-analysis

Print interval analysis results for all LLZK structs.

Options

-field                       : The field to use for interval analysis. Supported fields: bn128/bn254, babybear, goldilocks, mersenne31
-propagate-input-constraints : Whether to propagate constraints on inputs from @constrain to @compute functions. This allows for tighter intervals to possibly be found for computed values, assuming that the witness generator would include constraints as assertions during the computation.
-print-solver-constraints    : Whether to output SMT solver constraints along with intervals.
-print-compute-intervals     : Whether to print compute function intervals (default only prints constrain function intervals).

-llzk-print-symbol-def-tree

Print symbol definition tree.

Options

-stream  : Specifies the stream to which the pass prints.
-saveDot : Whether to dump the graph to DOT format.

-llzk-print-symbol-use-graph

Print symbol use graph.

Options

-stream  : Specifies the stream to which the pass prints.
-saveDot : Whether to dump the graph to DOT format.

General Transformation Passes

-llzk-duplicate-op-elim

Remove redundant operations

Remove llzk and arith dialect operations that produce the same results as previously executed operations.

Pass should be run after llzk-duplicate-read-write-elim for maximum effect.

-llzk-duplicate-read-write-elim

Remove redundant reads and writes

Remove read and write operations to struct fields and arrays that are redundant or unnecessary.

-llzk-inline-structs

Inlines nested structs (i.e., subcomponents).

This pass inlines nested structs (i.e., subcomponents) at struct-type fields and at calls to the subcomponent compute/constrain functions. Inlining decisions are guided by the call graph of "constrain" functions.

The max-merge-complexity parameter can be used to limit the complexity of the resulting structs such that a potential inlining will not take place if doing so would push the sum of constraint and multiplications in the combined struct over the limit. The default value 0 indicates no limits which means all structs will be inlined into the Main struct.

This pass should be run after llzk-flatten to ensure structs do not have template parameters because structs with template parameters cannot (currently) be inlined. Inlining is also not (currently) supported for subcomponent structs stored in an array-type field.

This pass also assumes that all subcomponents that are created by calling a struct "@compute" function are ultimately written to exactly one field within the current struct.

Options

-max-merge-complexity : Maximum allowed constraint+multiplications in merged @constrain functions

-llzk-poly-lowering-pass

Lowers the degree of all polynomial equations to a specified maximum

Rewrites constraint expressions into an (observationally) equivalent system where the degree of every polynomial is less than or equal to the specified maximum.

This pass is best used as part of the -llzk-full-poly-lowering pipeline, which includes additional cleanup passes to ensure correctness and optimal performance.

Options

-max-degree : Maximum degree of constraint polynomials (default 2, minimum 2)

-llzk-r1cs-lowering

Rewrites constraints to be compatible with R1CS constraints i.e a*b - c = 0

Transforms LLZK constraints into an equivalent set of R1CS constraints expressed in the r1cs dialect. This pass is best used as part of the -llzk-full-r1cs-lowering pipeline which includes a degree lowering pass and clean up passes to ensure correctness and performance.

-llzk-unused-declaration-elim

Remove unused field and struct declarations

Remove field and struct declarations that are unused within the current compilation unit. Note that this pass may cause linking issues with external modules that depend on any unused field and struct declarations from this compilation unit.

Pass should be run after llzk-duplicate-read-write-elim and llzk-duplicate-op-elim for maximum effect.

Options

-remove-structs : Whether to remove unused struct definitions as well. Requires module to declare a Main component, otherwise all components will appear unused.

'array' Dialect Transformation Passes

-llzk-array-to-scalar

Replace arrays with scalar values

Replace known-shape arrays with the proper number of scalar values

'polymorphic' Dialect Transformation Passes

-llzk-drop-empty-params

Remove empty struct parameter lists

-llzk-flatten

Flatten structs and unroll loops

Performs the following transformations:

• Instantiate affine_map parameters of StructType and ArrayType to constant values using the arguments at the instantiation site
• Replace parameterized structs with flattened (i.e., no parameter) versions of those structs based on requested return type at calls to compute() functions and unroll loops
• Unroll loops

Options

-max-iter : Maximum number of times the pass will run if a fixpoint is not reached earlier. Unrolling loops can provide more opportunities for instantiating structs but the converse is true as well. Thus, the pass will run multiple times until no further changes can be made or the upper limit provided in this option is reached.
-cleanup  : Specifies the extent to which unused parameterized structs are removed during the flattening pass.

Validation Passes

-llzk-validate-field-writes

Detect multiple and missing writes to the same field of a component.

llzk-lsp-server

cmake --build <build dir> --target llzk-lsp-server will produce an LLZK-specific LSP server that can be used in an IDE to provide language information for LLZK. Refer to the MLIR LSP documentation for a more detailed explanation of the MLIR LSP tools and how to set them up in your IDE.

Previous	Next
Setup	Contribution Guide