- 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.
An explicit field overrides the detected field for interval arithmetic, but preserves the declared-field semantics of felt.const. A literal N with declared modulus p is first interpreted as N mod p, then reduced into the analysis field of modulus q: (N mod p) mod q. Fieldless constants are reduced directly as N mod q.
For example, felt.const 8 in a field of modulus 7 contributes 1 when analyzed with modulus 5, both before and after constant canonicalization. The option changes the analysis field; it does not retarget declared felt types or reinterpret their literals as raw integers in another field.
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 or within a nested module or template if every symbol reference in the function can be resolved from the root module. Calls to other nested functions, included functions, and calls outside function.def bodies are left unchanged.
After inlining, free functions that have no remaining symbol uses anywhere in the module are erased. This cleanup applies to every non-external free function within the pass's root module, 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 an already-flattened, straight-line constrain body. Run llzk-flatten or another control-flow lowering pass before this pass; nested-region, successor-bearing, or multi-block constrain functions are rejected instead of being rewritten with component-lifetime auxiliary members. Compute functions may contain control flow; auxiliary computations and writes are materialized on every return path.
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
Promote straight-line static array accesses to SSA values
Promote statically indexed array elements whose accesses have a single linear order within one block or nested single-execution regions. Arrays involving control-flow joins, dynamic indices, or escaping values are left unchanged.
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:
Expand main constrain into straight-line constraints
After template monomorphization and child-member visibility preparation, expand main's constrain function and reachable single-block callees. Resolve static branches, signed for loops with positive steps, and while loops directly, including field-valued iterators and comparisons.
Local arrays and PODs exist only as concrete paths bound to scalar SSA values. Reads resolve bindings; writes and aggregate assignments update local bindings without emitting allocations, copies, or writes. Aggregate arguments preserve identity and remain read-only during each call. Returned aggregates alias their original roots: caller-local roots remain shared and writable after the call, while function inputs and original storage remain read-only. Component handles preserve identity. Every array access index must resolve at compile time and be in bounds. Reads of uninitialized local leaves and writes to function inputs or original storage are diagnosed.
Replace only main's constrain body, retaining its signature, original component storage, compute functions, and other definitions. Signal leaves are read through paths rooted in the original arguments. Live non-signal scalar storage is rejected; no witness variables or definitions are inferred from equations or compute functions. Ordinary field arithmetic remains SSA.
Diagnose symbolic control flow, recursion, unsupported effects, and non-native constraint arithmetic that cannot be constant evaluated (including division and inversion). Non-native field operations are evaluated using the current call and iteration bindings and replaced with constants when foldable. Static integer arithmetic, affine maps, casts, and comparisons are evaluated only as structural facts using their fold hooks and declared overflow semantics; pure symbolic computations must be dead after expansion. Both felt-to-index and integer-to-felt casts in assert mode must fold to statically valid conversions even when unused. Unresolved or failing range checks for either cast are diagnosed, never discarded. Every surviving operation is checked independently: only felt constants, felt add/subtract/multiply/negate expressions, felt equalities, original storage reads, index/i1 constants, and conversions of constant integers to felt are permitted. Validated integer-to-felt assertions are retained even when their results are unused. Any failed expansion or validation fails the entire pass.
Equality constraints currently require scalar felt operands; array equality and constrain.in are unsupported. Symbolic if/select conditions are rejected. Callees must be concrete, defined, and single-block. Recursion is unsupported and call nesting is limited to 256. Signed integer and index induction variables are supported. Original family handles retain their rolled types. Member reads use the concrete specialization's field types, which must unify with the exposed rolled declarations. Specialization selection and concrete path validation stay inside the pass; no new handle operations are emitted.
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.
Specialize structs and free functions reachable from llzk.main
Starting with a concrete llzk.main, discover and instantiate struct and free-function dependencies until every requested specialization has been processed. Reuse definitions by source symbol and concrete argument list, including reachable definitions with no template parameters. Free-function arguments may be explicit on a call or inferred from its type signature. Preserve source templates and control flow, and update direct type uses and calls to their concrete definitions. A free-function call retained in an unselected branch receives a concrete callee only when struct type rewriting changes its signature.
Loops remain in the IR rather than being unrolled; discovery evaluates their iterations to identify specializations without expanding the loop bodies. "Rolled" calls and struct types below retain affine parameters that depend on those iterations or on array element indices.
Affine calls and array values retain their parameterized types. Their poly.family_specializations and poly.family attributes identify the concrete definitions needed by later elaboration; definitions carry poly.specialization_id, poly.origin and poly.arguments attributes. Free-function clones carry poly.origin and poly.arguments; their identities are separate from the struct IDs used by families. poly.family appears on members and operations producing an array value, including struct.readm and array.new. Each entry names the rolled struct type, the enclosing array's index tuple, and the matching specialization. The type entry retains the original affine-parameterized family type; it identifies which struct field is being specialized within a POD element. specialization identifies the concrete clone through its poly.specialization_id. For example, an element at index 2 of a Child family retains Child in type and names the clone whose poly.arguments are [2]. Concrete sibling fields have no family entry. On a rolled call, poly.family_specializations lists candidates collected from all matching arrays and affine calls in the source instance. The list may be empty only when a known array has an empty dimension. A consumer selects a target by evaluating the argument type's affine map using the value's affine inputs, often an array element's indices, and matching the resulting arguments to poly.arguments. poly.origin and every struct name nested in poly.arguments are relative to the outermost llzk.lang root, which is also the lookup anchor when reloading this metadata. Cache keys use the same argument spelling, so requests from different roots reuse the same specialization. Substitution re-spells type arguments relative to the clone's root; an argument whose definition is outside that root is diagnosed at the instantiation site. Arguments to typed poly.param declarations are converted to the declared type using the conversions below, before forming a cache key. An incompatible argument is diagnosed. Felt-to-index conversion requires a known field and a reduced representative in the nonnegative signed 64-bit index range. Fieldless felt literals cannot determine an index. Arguments to felt parameters with a known field are reduced modulo its prime before forming the cache key and substituting uses. A felt literal with no specified field acquires the parameter's declared field; a different explicit field is rejected. Equivalent field values therefore share a specialization. With no known field, index-to-felt conversion requires a nonnegative value and preserves it. Untyped parameters retain their input attributes, so differently spelled numeric values can create distinct specializations. An i1 parameter accepts only boolean arguments or index zero and one, which become false and true. Other index values fail type conversion at the instantiation site. The normalized boolean binding determines specialization identity and is used for every read and forwarded argument. Forwarding that value to an index parameter produces zero or one. A felt binding must be read with its exact felt type, including its field, even for untyped parameters. Mismatched felt types are diagnosed at poly.read_const. Reading it as index or i1 is diagnosed at poly.read_const; use an explicit cast after a felt read for numeric conversion. Integer bindings read as i1 must be zero or one. Integer-to-felt reads use the same modular conversion as typed arguments, and negative values require a known field modulus. Reads whose type is a type variable use its concrete binding.
Discovered methods and free functions must be defined and single-block. Supported regions are scf.if, signed scf.for with known bounds and positive steps, and scf.while with a known condition at every check. Unstructured branches are diagnosed. Constant evaluation uses template bindings and fold hooks; global and aggregate reads and call results remain unknown. Function arguments also begin unknown, even when a caller passes a constant. Required specialization arguments must resolve. External free functions retain their declared signatures. Calls with struct types rewritten to distinct clone types are diagnosed, including plain structs, because the declaration would otherwise have a mismatched type. Includes must be inlined before running this pass.
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.
Expose members of concrete child storage reachable from a selected root.
This pass makes subcomponent fields public, allowing the constraint body to access felt leaves when flattening constraints without scalarizing struct members.
For family storage, matching member declarations on the rolled template are also exposed. This legalizes ordinary reads through unchanged family handles; template bodies are not traversed or expanded. Signal annotations are preserved.
The root's own member visibility is preserved because changing it would change the circuit's public interface and hence its semantics.
Use root-struct to select a root explicitly; otherwise the pass uses llzk.main.
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 expects concrete structs and scalar members. Use llzk-full-pcl-lowering to normalize loops, flatten templates, and scalarize PODs and arrays first while preserving component boundaries.
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.
Monomorphize templates and expand main constrain while retaining component storage.
Runs these passes in order:
Inline includes and lower symbolic non-native constraint arithmetic before this pipeline. Constant non-native arithmetic is evaluated during expansion using the current call and loop bindings. Specialization discovery and constraint expansion share scalar folding and integer/field conversion logic, so known template and loop values use the same arithmetic semantics in both stages. Canonicalization removes frontend scf.execute_region wrappers before monomorphization and folds specialized constants before expansion. Control flow and all array indices must resolve statically; aggregate function inputs are read-only. The pass expands concrete constrain bodies and eliminates local aggregate storage while retaining the original component layout and ordinary scalar arithmetic. Family handles retain their rolled types, with concrete member read types validated against the selected specialization and exposed template declarations. Consumers must support these reads through rolled handles; -llzk-array-to-scalar currently does not.
Only scalar felt equality constraints are supported. Array equality, constrain.in, live non-signal storage reads, recursion, and undefined or multi-block callees are rejected. See -llzk-flatten-constraints for the binding model, diagnostics, and supported control flow.
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:
The --llzk-generate-layout pipeline monomorphizes LLZK IR and exports its logical felt-signal layout:
For already monomorphized IR, --llzk-layout exports the layout directly. Both commands require main to define a @constrain function; product-only main components are unsupported.
The text format starts with a layout map header and a # signals section. Each line gives a signal ID and a storage path, such as signal 0<TAB>main["children"][0]["out"]. IDs start at zero and cover every declared signal, including unused signals. A member's {signal} annotation marks signal storage; unmarked felt intermediates receive no IDs. Main's inputs and public output members are implicit signals. Child components are traversed to find their annotated members. Struct members and POD fields follow declaration order, expanding each field fully before moving to the next. Arrays follow numeric index order, with the last dimension varying fastest. Constrain arguments come first in signature order, followed by the main instance's members. The main root identifies the main instance; arg["name"] or argN identifies an argument to its constrain function. Argument names are display labels; the in-memory paths start with "main" or "arg" and the argument's signature position, so root names are separate from signal IDs. Non-felt scalars and empty arrays contribute no signals.
Array dimensions must be concrete. Rolled arrays of parameterized structs use the monomorphizer's poly.family metadata to select a concrete specialization at each element, including struct fields inside POD elements. Missing mappings are diagnosed, as are ambiguous specialization IDs and mismatched origins. The exporter trusts the monomorphizer's mapping of indices to specialization arguments; passes that change specializations must keep this metadata consistent. Unrelated specialization metadata does not block export. The exporter inspects storage declarations without evaluating function bodies. It assigns logical signal IDs independently of backend wires and auxiliary variables; later lowering can attach a wire-to-signal mapping. The C++ buildLLZKLayout API returns the paths indexed by ID, and getSignalId looks up an ID by path. Renaming clone symbols or repeating monomorphization does not change IDs for the same declarations. Reordering fields changes IDs.
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_info.set 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_info.set, 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