Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
82 commits
Select commit Hold shift + click to select a range
cc27083
Verify felt template argument fields
1sgtpepper Jul 23, 2026
46b04f8
fix: validate symbolic felt restrictions directionally
1sgtpepper Aug 6, 2026
692893f
style: format felt restriction helper
1sgtpepper Aug 6, 2026
1790828
fix: validate omitted template arguments in inference check
1sgtpepper Aug 6, 2026
683eab1
fix: preserve omitted calls without inferred bindings
1sgtpepper Aug 6, 2026
6677e38
fix: keep local felt bindings authoritative
1sgtpepper Aug 6, 2026
f0f9275
test: split independent struct restriction cases
1sgtpepper Aug 6, 2026
67b589f
docs: describe directional felt restrictions
1sgtpepper Aug 6, 2026
a836bf8
fix: validate symbolic felt restrictions in verifier paths
1sgtpepper Aug 6, 2026
bb5a793
debug: trace felt template argument verification
1sgtpepper Aug 6, 2026
07ce600
test: cover symbolic felt restriction verification
1sgtpepper Aug 6, 2026
8053b25
fix: preserve untyped struct restriction diagnostics
1sgtpepper Aug 6, 2026
d8e3023
test: keep deferred symbolic diagnostics behavior based
1sgtpepper Aug 6, 2026
69da888
test: align felt restriction negative cases
1sgtpepper Aug 6, 2026
baf9be8
fix: preserve deferred symbolic type bindings
1sgtpepper Aug 6, 2026
dd1492e
style: format deferred binding diagnostic
1sgtpepper Aug 6, 2026
569cea0
test: construct invalid felt calls in place
1sgtpepper Aug 6, 2026
5cba4be
test: keep symbolic verifier negatives at operation level
1sgtpepper Aug 6, 2026
2442c28
fix: normalize felt template values before inference
1sgtpepper Aug 6, 2026
71f0d0d
Validate concrete template parameter restrictions
1sgtpepper Aug 6, 2026
7a5b872
test: preserve affine restriction coverage
1sgtpepper Aug 7, 2026
74348bf
fix: validate all qualified global restrictions
1sgtpepper Aug 7, 2026
6cbe892
fix: enforce type-only template restrictions
1sgtpepper Aug 7, 2026
21c1e4c
test: split type restriction cases
1sgtpepper Aug 7, 2026
8277e75
test: align type restriction diagnostics
1sgtpepper Aug 7, 2026
2723b32
fix: reconcile felt template values safely
1sgtpepper Aug 9, 2026
5f02c7f
fix: reconcile resolved felt symbols with inferred values
1sgtpepper Aug 9, 2026
669755d
style: format felt reconciliation
1sgtpepper Aug 9, 2026
01b6975
fix: preserve inferred felt field evidence
1sgtpepper Aug 9, 2026
5030642
test: isolate felt reconciliation failures
1sgtpepper Aug 9, 2026
c365f0a
refactor: remove redundant felt field checks
1sgtpepper Aug 9, 2026
fbe6216
refactor: remove unused felt includes
1sgtpepper Aug 9, 2026
c9f454a
fix: reconcile resolved felt evidence symmetrically
1sgtpepper Aug 9, 2026
585ee47
style: format resolved felt reconciliation
1sgtpepper Aug 9, 2026
a6b6924
fix: qualify felt evidence types
1sgtpepper Aug 9, 2026
40975b8
refactor: remove unused felt namespaces
1sgtpepper Aug 9, 2026
82a0d3e
docs: explain resolved felt evidence helpers
1sgtpepper Aug 9, 2026
148758e
docs: narrow felt reconciliation contract
1sgtpepper Aug 10, 2026
44100b7
docs: clarify felt template restrictions
1sgtpepper Aug 10, 2026
108eab3
docs: clarify include verifier terminology
1sgtpepper Aug 10, 2026
081853f
Preserve deferred template expressions
1sgtpepper Jul 23, 2026
92bb335
Limit template expression evaluation to target uses
1sgtpepper Jul 23, 2026
960ff6c
Apply project formatting
1sgtpepper Jul 23, 2026
1aeaa87
Match main struct failure summary
1sgtpepper Jul 23, 2026
ebdc88e
Match nested function failure summary
1sgtpepper Jul 23, 2026
15c6ec5
Check split failure summary once
1sgtpepper Jul 23, 2026
4a2e86e
Keep unrelated expression regression referenced
1sgtpepper Jul 23, 2026
86b067c
Isolate target-local expression coverage
1sgtpepper Jul 23, 2026
696e404
Cover deferred expression type bindings
1sgtpepper Jul 23, 2026
2910c98
Keep deferred expression checks behavior-focused
1sgtpepper Jul 23, 2026
38ce56e
Refresh deferred expression checks
1sgtpepper Jul 24, 2026
264472b
Document flattening failure check
1sgtpepper Jul 25, 2026
4b4e423
Preserve generated FileCheck indentation
1sgtpepper Jul 27, 2026
4feec67
Refresh deferred expression specialization checks
1sgtpepper Aug 5, 2026
b68b83d
Fix deferred struct instantiation guard
1sgtpepper Aug 5, 2026
bd856c0
fix(flattening): normalize deferred expression types
1sgtpepper Aug 5, 2026
5301c0d
fix(flattening): materialize nested call bindings
1sgtpepper Aug 5, 2026
8081e07
style: format deferred expression changes
1sgtpepper Aug 5, 2026
d0b54a6
test(flattening): cover complete type-variable expressions
1sgtpepper Aug 5, 2026
32cbd98
fix(flattening): report partial expression diagnostics
1sgtpepper Aug 5, 2026
69348da
test(flattening): update normalized deferred expression checks
1sgtpepper Aug 5, 2026
9f7f258
fix(polymorphic): fold only identity casts
1sgtpepper Aug 5, 2026
a35af96
test(flattening): capture complete typevar output
1sgtpepper Aug 5, 2026
b4d54de
test(flattening): expose generated typevar output
1sgtpepper Aug 5, 2026
35a2a82
test(flattening): retain complete typevar output
1sgtpepper Aug 5, 2026
afc9a7c
Materialize felt constants after type conversion
1sgtpepper Aug 6, 2026
7daac8e
test: make felt expression coverage verifier-valid
1sgtpepper Aug 7, 2026
fb7a55f
fix: rollback failed struct specializations
1sgtpepper Aug 7, 2026
d959ff7
test: exercise struct specialization rollback
1sgtpepper Aug 7, 2026
cf2d570
fix: avoid caching failed partial struct tables
1sgtpepper Aug 7, 2026
2a9f7c9
fix(flattening): normalize felt specialization bindings
1sgtpepper Aug 9, 2026
9d2eb1b
test: cover partial felt normalization reuse
1sgtpepper Aug 9, 2026
1a0300e
fix: remove inherited felt helper dependency
1sgtpepper Aug 9, 2026
01f4557
test: verify partial felt normalization reuse
1sgtpepper Aug 9, 2026
209bd91
fix(flattening): diagnose invalid felt bindings
1sgtpepper Aug 9, 2026
fab377e
fix(flattening): type binding diagnostics consistently
1sgtpepper Aug 9, 2026
8a34574
fix(flattening): finalize specialization transaction
1sgtpepper Aug 10, 2026
1ad3703
fix(flattening): preserve nested template arguments
1sgtpepper Aug 10, 2026
d0e88b9
docs: define flattening specialization contracts
1sgtpepper Aug 10, 2026
ca13d5f
docs: define unifiable cast folding
1sgtpepper Aug 10, 2026
51d9f1e
fix: roll back function symbols atomically
1sgtpepper Aug 10, 2026
aef0391
fix(flattening): reuse function specializations by source identity
1sgtpepper Aug 10, 2026
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
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
fixed:
- Evaluate target-used template expressions when their value and type dependencies become concrete, preserving normalized expressions across partial specialization
- Preserve ordered explicit arguments on rebuilt nested calls and materialize enclosing bindings inside array, struct, POD, and scalar type arguments
- Canonicalize equivalent felt spellings before function and struct specialization identity is computed
- Roll back failed prospective specializations without retaining generated definitions or symbol-table entries, and suppress warnings from discarded clones
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
fixed:
- Materialize fieldless felt template constants in the required field and reject known field or value conflicts in concrete and symbolic arguments
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
fixed:
- Reuse fully instantiated free-function clones only when the source definition and ordered concrete parameter bindings match
3 changes: 2 additions & 1 deletion doc/doxygen/03_syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ module attributes {llzk.lang = "circom"} {
- `index`: (MLIR builtin) Machine integer.
- `felt.type`: Finite field element.
- `array.type<N x E>`: Aggregate type with indexed [pseudo-homogeneous](\ref pseudo-homogeneous) elements. Element type cannot be another array type, instead multi-dimensional arrays are specified with a comma-separated list of dimension sizes. Each dimension size can be specified as an integer literal, a symbol (referring to a template parameter within a templated `struct.def`), or an [affine_map](https://mlir.llvm.org/docs/Dialects/Affine/#polyhedral-structures) (used when creating arrays within a loop where the dimension size depends on the loop iteration variable).
- `struct.type<[..]>`: Aggregate type with named heterogeneous elements corresponding to a `struct.def`. Generally correlates to components/functions in the source language. Constituent elements may be local variables, subcomponents, and/or called functions. Optionally includes a list of parameters to instantiate a templated `struct.def` where each parameter can be an integer literal, a symbol (referring to a template parameter within a templated `struct.def`), a type used to instantiate a `poly.tvar<@N>` (see below), or an [affine_map](https://mlir.llvm.org/docs/Dialects/Affine/#polyhedral-structures) (used when the parameter of a templated `struct.type` depends on a loop iteration variable).
- `struct.type<@Name<[...]>>`: Aggregate type whose named heterogeneous elements are declared by a `struct.def`. For a definition nested in a `poly.template`, an optional instantiation list supplies one argument per `poly.param` in declaration order. An argument can be an integer literal, a felt constant such as `#felt<const 35>`, a symbol that resolves to an enclosing template parameter or global constant, a type used to instantiate a `poly.tvar<@N>` (see below), or an [affine_map](https://mlir.llvm.org/docs/Dialects/Affine/#polyhedral-structures) used when the argument depends on a loop iteration variable.
- `pod.type<..>`: Plain Old Data aggregate type with named heterogeneous elements. Unlike `struct.type`, there is no associated named declaration, the type itself specifies all constituent element types. It can be used more freely than `struct.type` since it has fewer restrictions on modifications.
- `poly.tvar<@N>`: Placeholder type variable within a templated `struct.def` that may be instantiated with different types.
- `string.type`: Sequence of characters.
Expand All @@ -46,6 +46,7 @@ LLZK supports arrays where the element type is not truly homogeneous, specifical
## Semantic Rules

- Each `array.new` operation creates a fresh mutable array allocation. Two identical `array.new` operations are not interchangeable when either result may be read or written. The same is true for `pod.new`.
- Felt arguments can instantiate parameters on `struct.type`, templated free-function calls, and `verif.include`. A fieldless felt restriction accepts any felt field. For a fielded restriction, a fieldless felt constant or integer is materialized in the required field, while an explicitly fielded constant or typed symbol must name that same field; an untyped symbol cannot establish a required field. If a call or inclusion signature independently infers the same parameter, all known fields and concrete values must also agree.
- A `function.def` argument may have `function.arg_name = "..."` to preserve the source-level argument name independently from the SSA name printed by MLIR. The value must be a non-empty, untyped string attribute; typed string attributes such as `"x" : i1` are rejected. Attached argument names must be unique within the function. Argument-splitting transforms derive names for generated arguments, such as `input[0]` for array elements or `self.member` for struct members.
- Ops marked with the `WitnessGen` trait can only be used in functions with the `allow_witness` attribute (`compute()` within `struct.def` has this by default). Similarly, ops marked with the `ConstraintGen` trait can only be used in functions with the `allow_constraint` attribute (`constrain()` within `struct.def` has this by default).
- Functions with the `allow_witness` attribute can only call other functions marked with `allow_witness`. Likewise for `allow_constraint`.
Expand Down
5 changes: 5 additions & 0 deletions include/llzk/Dialect/Felt/IR/Attrs.td
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,11 @@ def LLZK_FeltConstAttr
/// Returns the field name from the stored FeltType, or a null StringAttr
/// if no type is stored.
::mlir::StringAttr getFieldName() const;

/// Return a new constant with a compatible materialized type; this attribute is not mutated.
/// A fieldless expected type preserves an explicit field, while a fielded expected type is
/// applied to a fieldless constant. Materialization fails only when both fields differ.
::mlir::FailureOr<FeltConstAttr> materializeAs(FeltType expectedType) const;
}];
}

Expand Down
28 changes: 16 additions & 12 deletions include/llzk/Dialect/Function/IR/Ops.td
Original file line number Diff line number Diff line change
Expand Up @@ -332,7 +332,7 @@ def CallOp : FunctionDialectOp<

When the return StructType of a `compute()` function uses AffineMapAttr to
express struct parameter(s) that depend on a loop variable, the optional
instantiation parameter list of this operation must be used to instatiate
instantiation parameter list of this operation must be used to instantiate
all AffineMap used as parameters to the StructType.

Examples:
Expand All @@ -341,14 +341,16 @@ def CallOp : FunctionDialectOp<
%r = function.call @A::@compute(%x){(%i)} : (!felt.type) -> !struct.type<@A<[#M]>>
```

When the call targets a free function within a `poly.template` region, the optional
template parameter list can be used to instantiate all `poly.param` symbols within
the template. If all `poly.param` symbols are used within the function signature,
this can be elided. Otherwise, it is required to instantiate the function. The `?`
wildcard can be used for any `poly.param` with a `poly.tvar` type restriction, even
those that cannot be inferred from the function signature. The wildcard allows for
inference of the type within the function body itself during the flattening pass
but may fail if the type cannot be inferred from the function body.
When the call targets a free function within a `poly.template`, the optional template
parameter list supplies one argument per `poly.param`, in declaration order. The list may be
omitted only when every parameter appears in the function signature; omitted values are
inferred by unifying the call's operand and result types with that signature. The `?` wildcard
is valid only for a parameter with a `poly.tvar` restriction and leaves that type for a later
inference transformation.

Every explicit or inferred argument must satisfy its `poly.param` type restriction. If the
function signature independently infers a value for an explicitly supplied parameter, all
known fields and concrete values must agree.
}];

// See `VerifySizesForMultiAffineOps` for more explanation of these arguments.
Expand Down Expand Up @@ -460,7 +462,7 @@ def CallOp : FunctionDialectOp<
/// or else IR verification will fail.
::mlir::FunctionType getTypeSignature();

/// Attempt type unfication between the inferred FunctionType from this CallOp (as LHS) and
/// Attempt type unification between the inferred FunctionType from this CallOp (as LHS) and
/// the given FunctionType (as RHS). If successful, return a UnificationMap containing the
/// unifications that were made. Otherwise, return failure.
::mlir::FailureOr<UnificationMap> unifyTypeSignature(::mlir::FunctionType other);
Expand Down Expand Up @@ -539,8 +541,10 @@ def CallOp : FunctionDialectOp<
/// `UnificationMap` is expected to contain the unification results of this `CallOp` against
/// the target function type signature.
///
/// Pre-condition assertions:
/// - `!isNullOrEmpty(getTemplateParamsAttr())`
/// The template parameter list may be omitted when all parameters are inferable from the
/// function type signature.
///
/// Pre-condition assertions when the list is present:
/// - `getTemplateParamsAttr().size() == llvm::range_size(targetParamDefs)`
::mlir::LogicalResult verifyTemplateParamsMatchInferred(
::llvm::iterator_range<::mlir::Region::op_iterator<::llzk::polymorphic::TemplateParamOp>> targetParamDefs,
Expand Down
19 changes: 11 additions & 8 deletions include/llzk/Dialect/Polymorphic/IR/Ops.td
Original file line number Diff line number Diff line change
Expand Up @@ -264,18 +264,20 @@ def LLZK_UnifiableCastOp : PolymorphicDialectOp<"unifiable_cast", [Pure]> {
This operation reinterprets a value as a different type with the restriction
that the input and output types of the cast are unifiable.

Most ops that accept LLZK types accept unifiable types as input and thus there
is no need for casting between types. This op is meant to be used in situations where
is not possible to modify the given or the target type and they are different but unifiable.
For example, inside a conversion pattern the driver may introduce `unrealized_conversion_cast`
operations if the types are not equal. This will happen regardless of whether the two types unify.
This cast can be introduced instead of the default cast operation to satisfy MLIR's assumptions
on type equality.
Most operations that accept LLZK types also accept operands whose types unify, so an explicit
cast is normally unnecessary. Use this operation when neither the input nor result type can be
changed but MLIR still requires exact type equality. For example, a conversion pattern can use
this operation instead of an `unrealized_conversion_cast` while preserving the requirement that
the unequal types unify.

During constant folding, this operation returns its input constant only when the input and
result types are identical. Non-constant inputs do not fold. Merely unifiable but unequal
types do not fold because the input has a different type from the result.

Example:
```llzk
%0 = some_other_op : !array.type<@N x !felt.type>
%1 = unifiable_cast %0 : (!array.type<@N x @felt.type>) -> !array.type<affine_map<()[s0, s1] -> (s0 + s1)> x !felt.type>
%1 = poly.unifiable_cast %0 : (!array.type<@N x !felt.type>) -> !array.type<affine_map<()[s0, s1] -> (s0 + s1)> x !felt.type>
```
}];

Expand All @@ -286,6 +288,7 @@ def LLZK_UnifiableCastOp : PolymorphicDialectOp<"unifiable_cast", [Pure]> {
}];

let hasVerifier = 1;
let hasFolder = 1;
}

def LLZK_ApplyMapOp : PolymorphicDialectOp<"applymap", [Pure]> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -53,15 +53,31 @@ def EmptyTemplateRemovalPass : LLZKPass<"llzk-drop-empty-templates"> {
}

def FlatteningPass : LLZKPass<"llzk-flatten"> {
let summary = "Flatten structs and unroll loops";
let summary =
"Instantiate templates, unroll loops, and propagate instantiated types";
let description = [{
Performs the following transformations:
- Instantiate `affine_map` parameters of StructType and ArrayType
to constant values using the arguments at the instantiation site
- Replace parameterized structs with flattened (i.e., no parameter)
versions of those structs based on requested return type at calls
to `compute()` functions and unroll loops
- Unroll loops
Iterates the following transformations to a fixpoint, bounded by `max-iter`:

- Instantiate parameterized structs reached from `llzk.main` or struct uses. Specialize free
functions from concrete explicit arguments, signature unification, or body-inferred wildcard
types. If only some parameters are concrete, keep the specialization in a reduced
`poly.template`.
- Evaluate target-used `poly.expr` values whose dependencies are concrete. A partial
specialization retains normalized copies of target-used expressions that still depend on
remaining parameters. A concrete expression that cannot fold, or an expression that remains
deferred in a full specialization, is an error.
- Apply concrete bindings to scalar type variables, array dimensions and element types,
parameterized struct arguments, POD record types, and explicit arguments on nested calls.
- Unroll loops with known iteration bounds, instantiate `affine_map` parameters of struct and
array types, and propagate the resulting member, array, call, and function types.

Warnings accumulated while converting a prospective struct are retained only after body
conversion succeeds. For a prospective free function, body conversion and nested-call
verification must both succeed. A failed prospective specialization and its accumulated
warnings are discarded.

After the fixpoint, the pass applies the selected cleanup mode, removes empty templates, and
removes unused discardable array allocations.
}];
// Implementation note: These options should be kept in sync with
// `StructInliningFlatteningOptions` in `LLZKTransformationPassPipelines.h`.
Expand Down
8 changes: 6 additions & 2 deletions include/llzk/Dialect/Shared/TypeConversionPatterns.h
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,8 @@ class CreateArrayOpClassReplacePattern : public mlir::OpConversionPattern<array:
}
};

/// Pattern for `CallOp`. Converts result types only; the callee symbol is left unchanged.
/// Rebuild a `CallOp` with converted result types and remapped operands. Preserve its callee,
/// affine-map instantiation state, and ordered explicit template arguments unchanged.
class CallOpClassReplacePattern : public mlir::OpConversionPattern<function::CallOp> {
public:
CallOpClassReplacePattern(mlir::TypeConverter &converter, mlir::MLIRContext *ctx)
Expand All @@ -219,9 +220,12 @@ class CallOpClassReplacePattern : public mlir::OpConversionPattern<function::Cal
if (mlir::failed(getTypeConverter()->convertTypes(op.getResultTypes(), newResultTypes))) {
return op->emitError("Could not convert Op result types.");
}
mlir::ArrayAttr templateParamsAttr = op.getTemplateParamsAttr();
llvm::ArrayRef<mlir::Attribute> templateParams =
templateParamsAttr ? templateParamsAttr.getValue() : llvm::ArrayRef<mlir::Attribute>();
replaceOpWithNewOp<function::CallOp>(
rewriter, op, newResultTypes, op.getCalleeAttr(), adapter.getMapOperands(),
op.getNumDimsPerMapAttr(), adapter.getArgOperands()
op.getNumDimsPerMapAttr(), adapter.getArgOperands(), templateParams
);
return mlir::success();
}
Expand Down
23 changes: 13 additions & 10 deletions include/llzk/Dialect/Struct/IR/Types.td
Original file line number Diff line number Diff line change
Expand Up @@ -27,22 +27,25 @@ class StructDialectType<string name, string typeMnemonic,
def LLZK_StructType : StructDialectType<"Struct", "type"> {
let summary = "circuit component";
let description = [{
Type of a `struct` op instance. For structs that contain template parameters,
the type must contain a list of attributes that instantiate the template
parameters, one per parameter. Each attribute must be one of the following:
Type of a `struct.def` instance. An instantiation argument list supplies one attribute per
`poly.param` in the definition's enclosing `poly.template`, in declaration order. Every
argument must satisfy the corresponding parameter's type restriction; a symbol argument is
checked using its resolved enclosing template binding or global definition. Each attribute
must be one of the following:
- IntegerAttr (with IndexType), specifying a fixed parameter value
- SymbolRefAttr, specifying a parameter value defined by a struct parameter
- FeltConstAttr, specifying a fixed finite-field parameter value
- SymbolRefAttr, specifying a parameter value defined by an enclosing template parameter
or global constant
- AffineMapAttr, for an array of struct elements whose template parameters
vary based on some fixed pattern.
- TypeAttr, for specifying a type parameter.
- AffineMapAttr, specifying a single-result affine expression for an argument that varies
across an array of struct elements
- TypeAttr, specifying a type parameter

```llzk
// Type for struct `A` with no parameters.
!struct.type<@A>

// Type for struct `B` with IntegerAttr and SymbolRefAttr parameters.
!struct.type<@B<[5, @C]>>
// Type for struct `B` with IntegerAttr, FeltConstAttr, and SymbolRefAttr parameters.
!struct.type<@B<[5, #felt<const 35>, @C]>>

// Type for struct `C` with TypeAttr and IntegerAttr parameters.
!struct.type<@C<[!felt.type, 24]>>
Expand Down Expand Up @@ -99,7 +102,7 @@ def LLZK_StructType : StructDialectType<"Struct", "type"> {
// Verifies that this type references a valid struct, relative to the given `op`.
::mlir::LogicalResult verifySymbolRef(::mlir::SymbolTableCollection &symbolTable, ::mlir::Operation *op);

/// Returns wether the struct this type refers to has members marked as columns.
/// Returns whether the struct this type refers to has members marked as columns.
/// A lookup is necessary first and will forward the failure state if it fails.
mlir::LogicalResult hasColumns(mlir::SymbolTableCollection &symbolTable, mlir::Operation *op) const;
}];
Expand Down
Loading