project-llzk · raghav198 · Jul 10, 2026 · May 26, 2026 · May 26, 2026 · May 27, 2026
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "circom-benchmarks"]
+	path = circom-benchmarks
+	url = git@github.com:project-llzk/circom-benchmarks
diff --git a/README.md b/README.md
@@ -1,2 +1,123 @@
-# LLZK-Verifier
-Porting [ZEQUAL](https://www.cs.utexas.edu/~isil/zequal.pdf) to LLZK 
+# LLEQ
+
+LLEQ is an equivalence verifier for zero-knowledge circuits in LLZK IR, based on [Zequal](https://veridise.com/wp-content/uploads/2025/08/zequal.pdf). LLEQ consumes **LLZK IR**, not high-level circuit languages directly. If your circuit is written in another language, first lower it to LLZK using an appropriate frontend (see [Frontends](https://github.com/project-llzk/.github/blob/main/profile/README.md)), then run LLEQ on the resulting `.llzk` file
+
+## Quick Links
+
+- [Build](#build)
+- [Usage](#usage)
+- [Examples](#examples)
+- [Capabilities and Limitations](#capabilities-and-limitations)
+
+## Build
+
+LLEQ can be built with Nix, or manually with CMake.
+
+### Nix (Recommended)
+
+This repository is configured with a Nix flakes environment. The flake was built using Nix version 2.31; older/newer versions may or may not.
+Once you have a Nix installation (See [Installation](https://nix.dev/manual/nix/2.31/installation/index.html)), you can run `nix build .#lleq` from the repository root, or `nix develop` to enter a developer shell. Inside the dev shell, the built `lleq` binary is added to `PATH` for
+convenience.
+
+### Manual
+
+For a manual build, you will need the following:
+
+- LLVM
+- MLIR
+- LLZK
+- a C++23-capable compiler
+- `cvc5`
+- `z3`
+- Python 3
+
+Both LLZK and MLIR must be built and installed in a way that CMake can discover with `find_package(LLZK)` (See [project-llzk/llzk-lib](https://github.com/project-llzk/llzk-lib/blob/main/doc/doxygen/01_setup.md#manual-build-setup) for instructions on how to build LLVM/MLIR/LLZK).
+
+At runtime, LLEQ expects both `cvc5` and `z3` to be available on `PATH`. Solver
+discovery can also be overridden by setting the following environment variables:
+
+```
+LLEQ_CVC5=/path/to/cvc5
+LLEQ_Z3=/path/to/z3
+```
+
+#### Build with CMake
+
+Configure:
+
+```bash
+cmake -G Ninja -S . -B build -DCMAKE_BUILD_TYPE=Release
+```
+
+If LLVM, MLIR, or LLZK are installed in nonstandard locations, point CMake at
+their package configuration directories with `-DLLVM_DIR=...`,
+`-DMLIR_DIR=...`, and `-DLLZK_DIR=...`.
+
+Build:
+
+```bash
+cmake --build build
+```
+
+### Run the Test Suite
+
+To run the LIT regression tests after a manual build:
+
+```bash
+cmake --build build --target check
+```
+
+The Nix package build also runs the test suite.
+
+## Usage
+
+LLEQ operates on an input `.llzk` file and a selected struct:
+
+```bash
+lleq <subcommand> --struct <StructName> [options] input.llzk
+```
+
+Available subcommands:
+
+- `dump-store`: print the symbolic store constructed for the selected struct
+- `verify`: prove equivalence of signal members
+- `dump-smt`: print the SMT-LIB query generated for deductive verification
+- `wp`: infer loop invariants and emit weakest-precondition-style verification conditions as SMT-LIB
+
+Common options:
+
+- `--struct <name>`: required; selects the struct to analyze
+- `--field <field-name>`: selects the prime field when it cannot be inferred
+- `--flatten`: run LLZK flattening and array-to-scalar lowering before analysis
+- `--enable-store`: available for `verify` and `dump-smt`; adds extra symbolic-store facts
+
+### Verify Output
+
+`lleq verify` reports one line per signal member:
+
+- `+ @Struct::member`: proven equivalent
+- `- @Struct::member`: proven inequivalent
+- `* @Struct::member`: unknown
+
+For inequivalent members, LLEQ also prints a witness/constraint counterexample model.
+
+Note that `lleq verify` does not perform loop invariant inference. To verify a struct containing loops or arrays, pass the `--flatten` argument to first unroll and scalarize the struct.
+
+### Weakest-Precondition Queries
+
+`lleq wp` emits an SMT-LIB query that can be sent directly to an SMT solver to
+check the verification condition and, when it fails, obtain a counterexample.
+
+For example:
+
+```bash
+lleq wp --struct DecomposeProduct_1 --field babybear examples/circom-examples/DecomposeProduct.llzk | z3 -in
+```
+
+## Examples
+
+See [Examples](examples/README.md)
+
+## Capabilities and Limitations
+
+Analysis of structs with multidimensional arrays or subcomponent calls is not currently well-supported. Verification may also fail for structs where LLZK's product alignment produces poor alignments.
diff --git a/circom-benchmarks b/circom-benchmarks
diff --git a/examples/README.md b/examples/README.md
@@ -0,0 +1,54 @@
+# Examples
+
+This directory collects example circuits and benchmark artifacts used for LLEQ
+development, demos, and evaluation.
+
+## `circom-examples`
+
+To import and generate benchmarks from [`project-llzk/circom-benchmarks`](https://github.com/project-llzk/circom-benchmarks), run:
+
+```bash
+python3 scripts/import_circom_demo_examples.py --circom-frontend <circom> --llzk <llzk-opt>
+```
+
+Each imported benchmark is lowered to LLZK and then normalized with the
+following pass pipeline before being checked into this repository:
+
+```text
+--llzk-while-to-for
+--llzk-compute-constrain-to-product=root-struct=<RootStruct>
+--llzk-fuse-product-loops
+--canonicalize
+```
+
+Here, `<RootStruct>` is the benchmark's `llzk.main` root struct. The resulting
+normalized `.llzk` files are stored flat in [`circom-examples`](./circom-examples).
+
+The subdirectory also includes `verification_results.csv`, which records LLEQ
+verification outcomes for the imported set.
+
+## Collecting Verification Data
+
+Run:
+
+```bash
+python3 scripts/collect_circom_demo_results.py --lleq-bin <lleq> --z3-bin <z3>
+```
+
+For each imported benchmark, the script currently runs:
+
+```text
+lleq wp --struct <RootStruct> | z3 -in
+```
+
+Each run uses a 120-second timeout and reports one of:
+
+- `verified`
+- `counterexample`
+- `partial`
+- `timeout`
+- `error`
+
+`wp` is classified as `partial` when z3 returns `unknown`.
+
+Results are saved in `examples/verification_results.csv`.
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -35,6 +35,9 @@
 
         # Default lleq build uses the default compiler for the system (usually gcc for Linux and clang for Macos)
         lleq = (final.callPackage ./nix/lleq.nix { clang = final.clang_20; llzk = final.llzk; mlir = final.mlir; }).overrideAttrs(attr: {
+          cmakeBuildType = "RelWithDebInfo";
+        });
+        lleqDebug = (final.callPackage ./nix/lleq.nix { clang = final.clang_20; llzk = final.llzk-debug; mlir = final.mlir-debug; }).overrideAttrs(attr: {
           cmakeBuildType = "Debug";
         });
         # Build in release with symbols mode with a particular compiler and sanitizers enabled.

diff --git a/include/Analysis/ScalarSymbolAnalysis.h b/include/Analysis/ScalarSymbolAnalysis.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 
@@ -20,6 +20,7 @@
 #include <mlir/Analysis/DataFlowFramework.h>
 #include <mlir/Dialect/SCF/IR/SCF.h>
 #include <mlir/IR/Value.h>
+#include <mlir/Interfaces/CallInterfaces.h>
 
 namespace lleq {
 
@@ -135,6 +136,11 @@ class ScalarSymbolAnalysis
   mlir::LogicalResult
   visitOperation(mlir::Operation *op, llvm::ArrayRef<const Lattice *> operands,
                  llvm::ArrayRef<Lattice *> results) override;
+
+  void visitExternalCall(mlir::CallOpInterface call,
+                         llvm::ArrayRef<const Lattice *> arguments,
+                         llvm::ArrayRef<Lattice *> results) override;
+
   void setToEntryState(Lattice *lattice) override {
     lattice->getValue().initPool(&pool.get());
     mlir::Value anchor = lattice->getAnchor();
@@ -143,19 +149,21 @@ class ScalarSymbolAnalysis
       // since all the symbolic expressions are relative to these
       if (llvm::isa<llzk::function::FuncDefOp>(
               blockArg.getOwner()->getParentOp())) {
-        propagateIfChanged(
+        return propagateIfChanged(
             lattice, lattice->join(pool.get().index(lattice->getAnchor(), {})));
-        return;
       }
       // Apparently setToEntryState gets called on loop induction vars too, but
       // these should just be set to Unknown because `i` and `i + step` will
       // never antiunify to anything interesting
       if (llvm::isa<mlir::scf::ForOp>(blockArg.getOwner()->getParentOp())) {
-        propagateIfChanged(lattice, lattice->join(pool.get().fresh_unknown()));
+        return propagateIfChanged(lattice,
+                                  lattice->join(pool.get().fresh_unknown()));
       }
     }
+
     // If nothing else is known, a default of `uninitialized` is fine
-    propagateIfChanged(lattice, lattice->join(pool.get().uninitialized()));
+    return propagateIfChanged(lattice,
+                              lattice->join(pool.get().uninitialized()));
   }
 };
 
@@ -175,4 +183,9 @@ inline bool sourceMatchesOp(mlir::Operation *op, Signal::Source source) {
          (source == Signal::Source::Witness && isWitnessOp(op));
 }
 
+inline bool isSubcmpRead(llzk::component::MemberReadOp read) {
+  return read.getComponent().getType() !=
+         read->getParentOfType<llzk::component::StructDefOp>().getType();
+}
+
 } // namespace lleq
diff --git a/include/Analysis/Store.h b/include/Analysis/Store.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Analysis/SymbolExpr.h b/include/Analysis/SymbolExpr.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2025 Veridise Inc.
+ * Copyright 2025 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Analysis/SymbolImpls.h b/include/Analysis/SymbolImpls.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Analysis/SymbolicStore.h b/include/Analysis/SymbolicStore.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2025 Veridise Inc.
+ * Copyright 2025 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 
@@ -19,6 +19,7 @@
 #include <llzk/Dialect/Struct/IR/Ops.h>
 #include <mlir/Analysis/DataFlow/ConstantPropagationAnalysis.h>
 #include <mlir/Analysis/DataFlow/DeadCodeAnalysis.h>
+#include <mlir/Analysis/DataFlowFramework.h>
 #include <mlir/IR/Block.h>
 #include <mlir/IR/Operation.h>
 #include <mlir/IR/Value.h>
@@ -31,7 +32,7 @@ namespace lleq {
 /// prove equivalence between pairs of witness/constraint signals.
 class SymbolicStore {
   std::unique_ptr<SymbolPool> pool = std::make_unique<SymbolPool>();
-  mlir::DataFlowSolver solver;
+  mlir::DataFlowSolver solver{mlir::DataFlowConfig{}.setInterprocedural(false)};
 
   llzk::component::StructDefOp component;
   SignalStore *signalStore;

diff --git a/include/Analysis/SymbolicStoreAnalysis.h b/include/Analysis/SymbolicStoreAnalysis.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Analysis/Unification.h b/include/Analysis/Unification.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2025 Veridise Inc.
+ * Copyright 2025 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Transforms/LLEQIfToIfElse.h b/include/Transforms/LLEQIfToIfElse.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Transforms/LLEQWhileToFor.h b/include/Transforms/LLEQWhileToFor.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Verification/DeductiveVerifier.h b/include/Verification/DeductiveVerifier.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Verification/FixpointVerifier.h b/include/Verification/FixpointVerifier.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Verification/SMTLIBEquivalenceEmitter.h b/include/Verification/SMTLIBEquivalenceEmitter.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */
 

diff --git a/include/Verification/SymbolicVerifier.h b/include/Verification/SymbolicVerifier.h
@@ -1,5 +1,5 @@
 /**
- * Copyright 2026 Veridise Inc.
+ * Copyright 2026 Project LLZK
  * SPDX-License-Identifier: Apache-2.0
  */