- Generated by
1.17.0
|
LLZK 3.0.0
An open-source IR for Zero Knowledge (ZK) circuits
|
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.
Print the LLZK module's call graph.
Print the SCCs from the LLZK module's call graph.
Print constraint dependency graph for all LLZK structs.
Print interval analysis results for all LLZK structs.
Print the predecessors of all operations.
Print symbol definition tree.
Print symbol use graph.
_Replace separate @compute and @constrain functions in a struct with a single @product function_
Replace separate @compute and @constrain functions in a struct with a single @product function
Remove redundant operations
Remove equivalent memory-effect-free operations and duplicate LLZK constraints.
Pass should be run after llzk-duplicate-read-write-elim for maximum effect.
Remove redundant reads and writes
Remove redundant or unnecessary reads and writes to struct members, arrays, globals, and RAM. Global writes are removed when they are overwritten or write an already-known value. RAM stores require the same translated address SSA value.
Struct-member accesses match only when the base, member, table offset, affine map metadata, and translated affine operands match. Omitted member-read offsets and member writes denote the current row.
Stateful reads are reused when the current analysis state proves the read observes the same value. Writes and stores update that known state, while unknown or non-read state effects invalidate it.
Checks that every struct member is written exactly once
This pass currently reports an error if any struct member may not be written exactly once (i.e. overwritten or left uninitialized), and does not attempt to perform any repairs (e.g. SSA-ifying overwritten struct members, or default-initializing unwritten members). This pass overapproximates conditionals, and can result in false positives.
_Fuse matching compute/constrain control flow in a @product function_
Fuse matching witness/constraint loops in a @product function
Inline calls to free functions
Inlines function.call operations inside function.def bodies when the target is a free function.def directly inside the pass's root builtin.module. Calls to functions in nested or included modules, and calls outside function.def bodies, are left unchanged. After inlining, root free functions that have no remaining symbol uses anywhere in the module are erased. This cleanup applies to every non-external root free function, regardless of its symbol visibility or whether any call to it was inlined.
Inlining is best effort: free functions that participate in a call cycle are skipped (inlining one would re-materialize its calls forever). If inlining a callee fails, its remaining calls are left in place with a warning while processing continues with other callees.
Lower 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.
High-degree subexpressions are factored into auxiliary struct members. The pass also recurses through degree-neutral roots such as felt.add, felt.sub, and felt.neg, so composite equality operands and struct constrain call arguments satisfy their degree bounds.
The pass expects already-flattened, straight-line compute and constrain bodies. Run llzk-flatten or another control-flow lowering pass before this pass; nested-region, successor-bearing, or multi-block functions are rejected instead of being rewritten with component-lifetime auxiliary members.
This pass is best used on already-flattened input as part of the -llzk-full-poly-lowering pipeline, which includes additional cleanup passes to ensure correctness and optimal performance.
Remove unread discardable allocations and their dead stores
Remove ops with the selected allocator operation name when they are marked with MemAlloc<DiscardableAllocationResource>, the allocation has no reads, and every direct user is a discardable allocation accessor that can be erased as a dead store.
Remove unused member and struct declarations
Remove member 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 member 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.
Converts scf.while loops to equivalent scf.for loops when possible
This pass identifies scf.while loops that have an induction variable and a uniform step, and converts them to equivalent scf.for loops, which are preferred by some analyses. This pass may introduce some spurious felt/index casts which should be cleaned up by –canonicalize.
Replace arrays with scalar values
Replace known-shape arrays with the proper number of scalar values
Lower bool quantifiers to SCF loops
Replace bool.forall and bool.exists over LLZK arrays with scf.for loops that iterate over the first array dimension and accumulate the predicate result with bool.and or bool.or, respectively.
Replace all IncludeOp with contents of the referenced file.
Trims the size of expressions by introducing intermediates
Trims the size of expressions by introducing intermediate bindings. This transformation is recommended before translating to PCL s-expressions if the circuit is large or it was converted from a circuit with many free functions.
When translating the MLIR representation of the PCL circuit to the s-expressions representation, each expression is expanded at each use point. This could lead to an explosion of the IR size. For example, consider the following IR:
Its s-expressions representation will expand to something roughtly 3 times the size:
This pass will introduce an intermediate binding in the middle of large expressions, resulting in smaller s-expressions in the final representation. The example above would be trimmed as follows.
Which results in the following s-expressions:
Replace PODs with scalar values
Scalarize pod.type values by splitting POD-typed struct members into multiple scalar members, splitting POD-typed array elements into parallel arrays, then rewriting affected member accesses plus function signatures, calls, and returns, and finally running POD-specific SROA + mem2reg cleanup so the remaining POD storage is promoted to SSA values.
If it is necessary to scalarize both PODs and arrays, run this pass before running the -llzk-array-to-scalar pass because that pass will not scalarize array types that are within a POD type.
Remove empty templates
Performs the following transformations:
Flatten structs and unroll loops
Performs the following transformations:
Infer concrete function types for polymorphic type variables
Infers concrete replacements for !poly.tvar template parameters from operations in function.def or poly.expr bodies, such as poly.unifiable_cast between a type variable and a more concrete type (which means for maximum effect you should run it before other optimization passes that can remove poly.unifiable_cast). Rewrites affected function signatures and body types, removes redundant casts, drops resolved poly.param declarations, and updates call-site template parameter lists.
The pass also creates template-local instantiated versions of functions for each type-variable replacement. The llzk-flatten pass performs similar instantiation of type variables but only as part of its more extensive lowering and flattening, all of which may not be desired in some cases (hence the utility of this pass).
This pass may result in poly.template containing no poly.param or poly.expr. Run llzk-drop-empty-templates after this pass to simplify these templates.
Refine wildcard array casts and specialize concrete call targets
Refines poly.unifiable_cast results when wildcard array.type dimensions can be replaced with concrete integer sizes from the input type. Then specializes free functions, extern declarations, and whole structs for calls whose wildcard array dimensions have become concrete.
This pass is intended to run after llzk-flatten. It iterates to a fixpoint so newly-refined cast result types can enable further callable specialization in later iterations.
Inlines nested structs (i.e., subcomponents).
This pass inlines nested structs (i.e., subcomponents) at struct-type members 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 member.
This pass also assumes that all subcomponents that are created by calling a struct "@compute" function are ultimately written to exactly one member within the current struct.
Rewrite constraints to be compatible with PCL constraints used by Picus
Transforms LLZK constraints into an equivalent set of constraints expressed in the pcl-mlir dialect. This pass currently expects the flattening and inlining passes to be run prior to its use.
Rewrite 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. The pass expects already-flattened, straight-line constrain bodies. Run llzk-flatten or another control-flow lowering pass before this pass; nested-region, successor-bearing, or multi-block constraints are rejected before R1CS normalization. This pass is best used on already-flattened input as part of the -llzk-full-r1cs-lowering pipeline which includes a degree lowering pass and clean up passes to ensure correctness and performance.
Detect multiple and missing writes to the same member of a component.
Detect multiple and missing writes to the same member of a component.
Note that this is overapproximate (i.e., some writes may erroneously be flagged as overwrites, and some members may erroneously be marked unwritten).
Remove unnecessary operations, such as redundant reads or repeated constraints.
Runs the following cleanup passes in order:
Remove unnecessary operations and member definitions.
Runs -llzk-remove-unnecessary-ops, followed by:
The unused-declaration pass uses its default options, so it removes unused members but does not remove struct definitions.
_Convert @compute/@constrain functions to an @product function and perform alignment._
Runs the following passes in order:
Flatten and inline all struct definitions into the main struct.
Runs the following passes in order:
POD scalarization precedes array scalarization because it can split pod.type array elements into parallel arrays. The pipeline defaults flattening cleanup to main-as-root; using another cleanup mode is not recommended because parameterized templates may survive flattening and cause -llzk-inline-structs to fail.
Inline free functions, then flatten and inline struct definitions.
This is the recommended pipeline before a downstream pass that does not support function.call. It first runs -llzk-inline-free-functions, then runs the same sequence and accepts the same options as -llzk-full-struct-inlining.
Flatten and inline structs, lower polynomial constraints, then remove unused IR.
Runs the following passes in order:
The nested struct-inlining stage uses main-as-root cleanup by default for the same reason as -llzk-full-struct-inlining.
Lower polynomial constraints to R1CS.
Runs the following passes in order:
The polynomial-lowering stage prepares flattened, degree-two constraints for R1CS conversion. CSE then removes redundant r1cs.to_linear operations.
llzk-translate is a version of the mlir-translate tool. Includes translations for backends specific to LLZK along with translations available in upstream MLIR (i.e. LLVM or C++). llzk-translate -h will show a list of all available flags and options.
The tool expects that the IR has already been converted to the backend's dialect IR. For example:
llzk-witgen executes LLZK witness-generation logic for the concrete main component declared by llzk.main. It evaluates compute() and prints JSON for either the public outputs of the main component or the full generated witness signal set.
The --inputs file must contain a top-level JSON object or JSON array.
At the main boundary, llzk-witgen only supports felt and array<... x felt> inputs, due to the restrictions posed on llzk.main components. Field element values are accepted in the same JSON form used by the witgen tests, namely JSON integers or decimal strings.
llzk-witgen writes one JSON object to stdout. The exact shape depends on --output-scope.
llzk-witgen currently supports two execution backends:
The default backend is interpreter, as the execution-engine does not currently support all LLZK features due to existing lowering limitations (e.g., in the -llzk-flattening pass).
Before execution, llzk-witgen performs the preprocessing needed to make witness generation concrete and executable:
Template parameters and affine instantiations are therefore supported only when they can be fully resolved by the preprocessing pipeline before execution.
llzk-smt-check runs an external SMT solver on an SMT-LIB 2 script and reports the result of each check-sat stage. It is intended to consume the staged SMT-LIB emitted by llzk-opt --smt-to-smtlib, including explicit metadata produced from smt.set_info ops such as (set-info :llzk-stage "pre") and (set-info :status unsat).
--smt-to-smtlib exports the unique top-level smt.solver directly contained in the root builtin.module. Module-scope func.func definitions are treated as helpers that may be called from within that solver body. Exported scripts preserve any smt.set_logic operation in that solver and otherwise begin with the conservative fallback (set-logic ALL). Any staged metadata consumed by llzk-smt-check must be introduced explicitly in the SMT dialect IR using smt.set_info, for example:
smt.check lowers only to a bare (check-sat). Because SMT-LIB scripts cannot branch on check-sat results internally, --smt-to-smtlib accepts only smt.check operations whose sat, unknown, and unsat regions are empty. Result-dependent script behavior would need a higher-level driver format outside SMT-LIB.
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.
1.17.0