Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,31 @@
## v2.1.2 - 2026-06-18
### Added
- `--llzk-remove-unused-discardable-allocations` for removing unread discardable allocations and their dead stores.
- `Destructurable*Interface` and `Promotable*Interface` to pod ops/types
- `PodRefOpInterface` and `PodAccessOpInterface` for ops that reference or access pods
- `llzk-pod-to-scalar` pass to destructure pod type values into scalar SSA values
- `llzk-specialize-wildcard-arrays` pass to refine array types with wildcard dimensions
- `--check-output` option for `llzk-witgen`
- AI coding agent instructions file

### Changed
- Allow non-native field ops in `verif.contract`
- Apply `llzk-flatten` cleanup option to free functions, not just structs
- `verif.contract` now rejects preconditions (`verif.require_*`) derived from struct members or function return values
- `verif.contract` for the `llzk.main` struct now rejects direct `verif.require_*` ops as well

### Fixed
- Added `scf.if` handling for `llzk-witgen --backend=execution-engine`
- Emit all R1CS-lowering auxiliary members with the exact type of the materialized expression
- Emit polynomial-lowering auxiliary members with the exact type of the materialized expression
- Emit synthesized zero R1CS linear-combination constants with a printable integer width
- Handle wildcard `CallOp` template parameters in the flattening pass.
- Implement missing felt ops for `llzk-witgen`
- Lower high-degree `felt.add`, `felt.sub`, and `felt.neg` equality roots and nonlinear struct constrain call arguments in the poly-lowering pass
- Prevent `--cse` from merging distinct `array.new` allocations or `pod.new` allocations.
- Reject polynomial and R1CS lowering on non-straight-line constrain bodies instead of materializing component-scope auxiliaries inside control flow
- Update SourceRefAnalysis to handle `scf.while`, `verif.contract`, and `verif.include`
- Array and pod scalarization passes now use the RDV pass wrapper with bug fix
## v2.1.1 - 2026-06-04
### Fixed
- Fixed prime field definitions
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,4 +19,4 @@ namespace pcl::conversion {
#define GEN_PASS_REGISTRATION
#include "pcl-conv/Transforms/TransformationPasses.h.inc"

}; // namespace pcl::conversion
} // namespace pcl::conversion
2 changes: 1 addition & 1 deletion backends/r1cs/include/r1cs/Dialect/IR/Attrs.td
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//===-- Attrs.td -----------------------------------------*--- tablegen -*-===//
//===-- Attrs.td -------------------------------------------*- tablegen -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
Expand Down
2 changes: 1 addition & 1 deletion backends/r1cs/include/r1cs/Dialect/IR/Ops.td
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//===-- Ops.td -------------------------------------------*--- tablegen -*-===//
//===-- Ops.td ---------------------------------------------*- tablegen -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
Expand Down
2 changes: 1 addition & 1 deletion backends/r1cs/include/r1cs/Dialect/IR/Types.td
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//===-- Types.td -----------------------------------------*--- tablegen -*-===//
//===-- Types.td -------------------------------------------*- tablegen -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
//===-- TransformationPassPipelines.h ---------------------------*- C++ -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
// Copyright 2026 Project LLZK
// SPDX-License-Identifier: Apache-2.0
//
//===----------------------------------------------------------------------===//

#pragma once

#include <mlir/Pass/PassManager.h>
#include <mlir/Pass/PassOptions.h>

namespace r1cs {

void buildFullR1CSLoweringPipeline(mlir::OpPassManager &);

void registerTransformationPassPipelines();

} // namespace r1cs
4 changes: 1 addition & 3 deletions backends/r1cs/include/r1cs/Transforms/TransformationPasses.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,8 @@

namespace r1cs {

void registerTransformationPassPipelines();

#define GEN_PASS_DECL
#define GEN_PASS_REGISTRATION
#include "r1cs/Transforms/TransformationPasses.h.inc"

}; // namespace r1cs
} // namespace r1cs
2 changes: 1 addition & 1 deletion backends/r1cs/lib/r1cs/Dialect/Dialect.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//===-- Dialect.cpp - R1CS dialect implementation -----------*- C++ -*-----===//
//===-- Dialect.cpp - R1CS dialect implementation ---------------*- C++ -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
Expand Down
2 changes: 1 addition & 1 deletion backends/r1cs/lib/r1cs/Transforms/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ add_library(R1CS::Transforms ALIAS R1CSTransforms)

file(GLOB R1CSTransforms_SOURCES "*.cpp")


target_sources(R1CSTransforms PRIVATE ${R1CSTransforms_SOURCES})

target_link_libraries(
Expand All @@ -15,6 +14,7 @@ target_link_libraries(
MLIRIR MLIRPass MLIRParser MLIRTransformUtils MLIRSCFTransforms
LLVMHeaders MLIRHeaders
PRIVATE
LLZKTransforms
LLZKDialect
R1CSDialect
LLZKAnalysis
Expand Down
9 changes: 6 additions & 3 deletions backends/r1cs/lib/r1cs/Transforms/R1CSLoweringPass.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -340,7 +340,7 @@ class PassImpl : public r1cs::impl::R1CSLoweringPassBase<PassImpl> {
if (degLhs == 2 && degRhs == 2) {
builder.setInsertionPoint(op);
std::string auxName = R1CS_AUXILIARY_MEMBER_PREFIX + std::to_string(auxCounter++);
MemberDefOp auxMember = addAuxMember(structDef, auxName);
MemberDefOp auxMember = addAuxMember(structDef, auxName, val.getType());
Value aux = builder.create<MemberReadOp>(
val.getLoc(), val.getType(), constrainFunc.getSelfValueFromConstrain(),
auxMember.getNameAttr()
Expand Down Expand Up @@ -532,7 +532,7 @@ class PassImpl : public r1cs::impl::R1CSLoweringPassBase<PassImpl> {
// Entire linear combination was zero
result = builder.create<r1cs::ConstOp>(
loc, r1cs::LinearType::get(builder.getContext()),
r1cs::FeltAttr::get(builder.getContext(), 0)
r1cs::FeltAttr::get(builder.getContext(), toAPSInt(lc.constant))
);
}

Expand Down Expand Up @@ -673,7 +673,7 @@ class PassImpl : public r1cs::impl::R1CSLoweringPassBase<PassImpl> {
if (degLhs == 2 && degRhs == 2) {
builder.setInsertionPoint(eqOp);
std::string auxName = R1CS_AUXILIARY_MEMBER_PREFIX + std::to_string(auxCounter++);
MemberDefOp auxMember = addAuxMember(structDef, auxName);
MemberDefOp auxMember = addAuxMember(structDef, auxName, lhs.getType());
Value aux = builder.create<MemberReadOp>(
eqOp.getLoc(), lhs.getType(), constrainFunc.getSelfValueFromConstrain(),
auxMember.getNameAttr()
Expand Down Expand Up @@ -704,6 +704,9 @@ class PassImpl : public r1cs::impl::R1CSLoweringPassBase<PassImpl> {
buildAndEmitR1CS(moduleOp, structDef, constrainFunc, degreeMemo);
structDef.erase();
});

// Remove `llzk.main` attribute because all structs were replaced with `r1cs.circuit` ops.
moduleOp->removeAttr(MAIN_ATTR_NAME);
}
};

Expand Down
36 changes: 22 additions & 14 deletions backends/r1cs/lib/r1cs/Transforms/TransformationPassPipelines.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,11 @@
///
//===----------------------------------------------------------------------===//

#include "r1cs/Transforms/TransformationPassPipelines.h"

#include "r1cs/Transforms/TransformationPasses.h"

#include "llzk/Transforms/LLZKTransformationPasses.h"
#include "llzk/Transforms/LLZKTransformationPassPipelines.h"

#include <mlir/Pass/PassManager.h>
#include <mlir/Pass/PassRegistry.h>
Expand All @@ -24,22 +26,28 @@ using namespace mlir;

namespace r1cs {

void registerTransformationPassPipelines() {
PassPipelineRegistration<>(
"llzk-full-r1cs-lowering", "Lower already-flattened polynomial constraints to r1cs",
[](OpPassManager &pm) {
// 1. Degree lowering
pm.addPass(llzk::createPolyLoweringPass(llzk::PolyLoweringPassOptions {.maxDegree = 2}));
void buildFullR1CSLoweringPipeline(OpPassManager &pm) {
// 1. Polynomial degree lowering and cleanup
llzk::FullPolyLoweringConfig config;
config.polyLowering = llzk::PolyLoweringPassOptions {.maxDegree = 2};
llzk::buildFullPolyLoweringPipeline(pm, config);

// 2. Cleanup
llzk::addRemoveUnnecessaryOpsAndDefsPipeline(pm);
// 2. Convert to R1CS
pm.addPass(r1cs::createR1CSLoweringPass());

// 3. Convert to R1CS
pm.addPass(r1cs::createR1CSLoweringPass());
// 3. Run CSE to eliminate to_linear ops
pm.addPass(mlir::createCSEPass());

// 4. Run CSE to eliminate to_linear ops
pm.addPass(mlir::createCSEPass());
}
// Other passes that may be helpful to add in the future:
// - llzk::createRemoveDeadValuesWorkaroundPass()
// - mlir::createCanonicalizerPass()
// (was run via poly-lowering -> struct-inlining but again may be useful)
}

void registerTransformationPassPipelines() {
PassPipelineRegistration<>(
"llzk-full-r1cs-lowering", "Lower polynomial constraints to r1cs",
buildFullR1CSLoweringPipeline
);
}

Expand Down
4 changes: 0 additions & 4 deletions changelogs/unreleased/array-new-cse-allocation.yaml

This file was deleted.

This file was deleted.

2 changes: 2 additions & 0 deletions changelogs/unreleased/dani__verif-invariant-ops.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
added:
- Operations in the `verif` dialect for expression loop invariants
2 changes: 2 additions & 0 deletions changelogs/unreleased/fix__poly-aux-write-order.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
fixed:
- Topologically order polynomial-lowering auxiliary writes in compute functions
4 changes: 0 additions & 4 deletions changelogs/unreleased/iangneal__execution-engine-updates.yaml

This file was deleted.

2 changes: 0 additions & 2 deletions changelogs/unreleased/iangneal__implement-witgen-ops.yaml

This file was deleted.

This file was deleted.

2 changes: 0 additions & 2 deletions changelogs/unreleased/lower-composite-poly-roots.yaml

This file was deleted.

2 changes: 0 additions & 2 deletions changelogs/unreleased/poly-dynamic-aux-scope.yaml

This file was deleted.

2 changes: 0 additions & 2 deletions changelogs/unreleased/th__agent_instructions.yaml

This file was deleted.

2 changes: 0 additions & 2 deletions changelogs/unreleased/th__allow_non_native_in_contract.yaml

This file was deleted.

2 changes: 2 additions & 0 deletions changelogs/unreleased/th__change_record_name_to_str.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
changed:
- use `StringAttr` instead of `FlatSymbolRefAttr` for record name in pod read/write ops
Empty file.
2 changes: 0 additions & 2 deletions changelogs/unreleased/th__fix_313_and_465.yaml

This file was deleted.

8 changes: 8 additions & 0 deletions changelogs/unreleased/th__pass_pipelines.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
added:
- "`llzk-full-struct-inlining` pass pipeline definition"

changed:
- "[header incompatibility] move `llzk-inline-structs` pass definition to `llzk/Dialect/Struct/Transforms/TransformationPasses.h`"
- "[CLI incompatibility] `llzk-full-poly-lowering` option `max-degree` is now `lowering={max-degree=3}`"
- "run `llzk-full-struct-inlining` at start of `llzk-full-poly-lowering` pass pipeline"
- "run `llzk-full-poly-lowering` with `max-degree=2` at start of `llzk-full-r1cs-lowering` pass pipeline"
3 changes: 0 additions & 3 deletions changelogs/unreleased/th__pod_op_interfaces.yaml

This file was deleted.

2 changes: 0 additions & 2 deletions changelogs/unreleased/th__prevent_new_pod_cse.yaml

This file was deleted.

Empty file.
Empty file.
2 changes: 0 additions & 2 deletions changelogs/unreleased/th__use_rdv_wrapper.yaml

This file was deleted.

1 change: 1 addition & 0 deletions include/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ add_subdirectory(llzk/Dialect/Shared)
add_subdirectory(llzk/Dialect/SMT/IR)
add_subdirectory(llzk/Dialect/String/IR)
add_subdirectory(llzk/Dialect/Struct/IR)
add_subdirectory(llzk/Dialect/Struct/Transforms)
add_subdirectory(llzk/Dialect/Verif/IR)

add_subdirectory(llzk/Transforms)
Expand Down
1 change: 1 addition & 0 deletions include/llzk-c/Dialect/Struct.h
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@
// Include the generated CAPI
#include "llzk/Dialect/Struct/IR/Ops.capi.h.inc"
#include "llzk/Dialect/Struct/IR/Types.capi.h.inc"
#include "llzk/Dialect/Struct/Transforms/TransformationPasses.capi.h.inc"

#ifdef __cplusplus
extern "C" {
Expand Down
16 changes: 16 additions & 0 deletions include/llzk-c/Dialect/Verif.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,11 @@ extern "C" {
/// Get reference to the LLZK `verif` dialect.
MLIR_DECLARE_CAPI_DIALECT_REGISTRATION(Verif, llzk__verif);

/// Attaches the interfaces defined by the `verif` dialect to upstream IR elements
///
/// Attempting to use those interfaces without calling this function first will result in an error.
MLIR_CAPI_EXPORTED void llzkVerif_attachInterfaces(MlirContext context);

/// Build a `verif.contract` from explicit attributes and signature metadata.
LLZK_DECLARE_OP_BUILD_METHOD(
Verif, ContractOp, MlirIdentifier sym_name, MlirAttribute target, MlirAttribute function_type,
Expand All @@ -55,6 +60,17 @@ LLZK_DECLARE_OP_BUILD_METHOD(
Verif, IncludeOp, MlirAttribute callee, MlirValueRange argOperands, MlirAttribute templateParams
);

/// Build a `verif.invariant` with a list of argument types and locations.
///
/// The pointers to the types and locations must point to the same amount of elements.
LLZK_DECLARE_OP_BUILD_METHOD(
Verif, InvariantOp, MlirStringRef loopName, intptr_t numArgs, MlirType const *types,
MlirLocation const *locs
);

/// Returns the body of the invariant operation.
MLIR_CAPI_EXPORTED MlirBlock llzkVerif_InvariantOpGetBody(MlirOperation op);

#ifdef __cplusplus
}
#endif
Expand Down
2 changes: 1 addition & 1 deletion include/llzk/Analysis/MemberOverwriteAnalysis.h
Original file line number Diff line number Diff line change
Expand Up @@ -149,4 +149,4 @@ class MemberOverwriteAnalysis
void setToEntryState(MemberOverwriteLattice *lattice) override { lattice->entry(); }
};

}; // namespace llzk
} // namespace llzk
2 changes: 1 addition & 1 deletion include/llzk/Analysis/SparseAnalysis.h
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//===- SparseAnalysis.h - Sparse data-flow analysis -----------------------===//
//===- SparseAnalysis.h - Sparse data-flow analysis -------------*- C++ -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,4 @@ namespace llzk::array {
#define GEN_PASS_REGISTRATION
#include "llzk/Dialect/Array/Transforms/TransformationPasses.h.inc"

}; // namespace llzk::array
} // namespace llzk::array
1 change: 1 addition & 0 deletions include/llzk/Dialect/Function/IR/Ops.h
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
#include "llzk/Dialect/Polymorphic/IR/Ops.h"
#include "llzk/Dialect/Shared/OpHelpers.h"
#include "llzk/Dialect/Struct/IR/Ops.h"
#include "llzk/Dialect/Verif/IR/OpInterfaces.h"
#include "llzk/Util/Constants.h"
#include "llzk/Util/SymbolHelper.h"

Expand Down
12 changes: 7 additions & 5 deletions include/llzk/Dialect/Function/IR/Ops.td
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
#define LLZK_FUNC_OPS

include "llzk/Dialect/Function/IR/Dialect.td"
include "llzk/Dialect/Verif/IR/OpInterfaces.td"
include "llzk/Dialect/Shared/OpTraits.td"
include "llzk/Dialect/Shared/Types.td"

Expand All @@ -36,11 +37,12 @@ class FunctionDialectOp<string mnemonic, list<Trait> traits = []>

def FuncDefOp
: FunctionDialectOp<
"def",
[ParentOneOf<["::mlir::ModuleOp", "::llzk::component::StructDefOp",
"::llzk::polymorphic::TemplateOp"]>,
DeclareOpInterfaceMethods<SymbolUserOpInterface>, AffineScope,
AutomaticAllocationScope, FunctionOpInterface, IsolatedFromAbove]> {
"def", [ParentOneOf<["::mlir::ModuleOp",
"::llzk::component::StructDefOp",
"::llzk::polymorphic::TemplateOp"]>,
DeclareOpInterfaceMethods<SymbolUserOpInterface>, AffineScope,
AutomaticAllocationScope, FunctionOpInterface,
IsolatedFromAbove, ContractTarget]> {
// NOTE: Cannot have SymbolTable trait because that would cause global
// functions without a body to produce "Operations with a 'SymbolTable' must
// have exactly one block"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,4 @@ namespace llzk::include {
#define GEN_PASS_REGISTRATION
#include "llzk/Dialect/Include/Transforms/InlineIncludesPass.h.inc"

}; // namespace llzk::include
} // namespace llzk::include
7 changes: 1 addition & 6 deletions include/llzk/Dialect/POD/IR/OpInterfaces.td
Original file line number Diff line number Diff line change
Expand Up @@ -49,18 +49,13 @@ def PodAccessOpInterface
// Requires implementors to have a '$record_name' attribute.
InterfaceMethod<
[{Gets the record name attribute from the pod access op.}],
"::mlir::FlatSymbolRefAttr", "getRecordNameAttr", (ins)>,
"::mlir::StringAttr", "getRecordNameAttr", (ins)>,
InterfaceMethod<
[{Return `true` if the op is a read, `false` if it's a write.}],
"bool", "isRead", (ins)>,
];

let extraClassDeclaration = [{
/// Gets the record name as an attribute suitable for destructuring indices.
inline ::mlir::StringAttr getRecordNameAsStringAttr() {
return getRecordNameAttr().getLeafReference();
}

/// Required by companion interface DestructurableAccessorOpInterface / SROA pass
bool canRewire(const ::mlir::DestructurableMemorySlot &slot,
::llvm::SmallPtrSetImpl<::mlir::Attribute> &usedIndices,
Expand Down
Loading