- Generated by
1.14.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 witness/constraint loops 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
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.
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).
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.14.0