Skip to content
Merged
Show file tree
Hide file tree
Changes from 12 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
Empty file.
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
deprecated:
- Removed built-in `Signal` component in favor of using `signal` attribute on fields
- Update documentation to reflect removal of `Signal` component
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
changed:
- Rename `struct.field` -> `struct.member` to avoid confusion with finite field terminology
- Rename `struct.readf` and `struct.writef` to `struct.readm` and `struct.writem` respectively
- Update related code, tests, and documentation to reflect these changes
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
changed:
- Restrict `struct.readm` to disallow access to private members of subcomponents.
6 changes: 6 additions & 0 deletions changelogs/unreleased/th__LLZK-367.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
changed:
- felt.nondet is now llzk.nondet and includes a type argument
- replace uses of undef op with llzk.nondet

removed:
- undef op and dialect
1 change: 0 additions & 1 deletion doc/doxygen/7_dialects.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,4 +19,3 @@
\include{doc} build/doc/mlir/dialect/PolymorphicDialect.md
\include{doc} build/doc/mlir/dialect/StringDialect.md
\include{doc} build/doc/mlir/dialect/StructDialect.md
\include{doc} build/doc/mlir/dialect/UndefDialect.md
1 change: 0 additions & 1 deletion include/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ add_subdirectory(llzk/Dialect/Polymorphic/IR)
add_subdirectory(llzk/Dialect/Polymorphic/Transforms)
add_subdirectory(llzk/Dialect/String/IR)
add_subdirectory(llzk/Dialect/Struct/IR)
add_subdirectory(llzk/Dialect/Undef/IR)
add_subdirectory(llzk/Transforms)
add_subdirectory(llzk/Util)
add_subdirectory(llzk/Validators)
4 changes: 0 additions & 4 deletions include/llzk-c/Constants.h
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,6 @@
extern "C" {
#endif

/// Symbol name for the struct/component representing a signal. A "signal" has direct correspondence
/// to a circom signal or AIR/PLONK column, opposed to intermediate values or other expressions.
extern const char *LLZK_COMPONENT_NAME_SIGNAL;

/// Symbol name for the witness generation (and resp. constraint generation) functions within a
/// component.
extern const char *LLZK_FUNC_NAME_COMPUTE;
Expand Down
3 changes: 3 additions & 0 deletions include/llzk-c/Dialect/LLZK.h
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ llzkLoopBoundsAttrGet(MlirContext context, int64_t lower, int64_t upper, int64_t
/// Returns true if the attribute is a LoopBoundsAttr.
LLZK_DECLARE_ATTR_ISA(LoopBoundsAttr);

/// Returns true if the op is a NonDetOp
LLZK_DECLARE_OP_ISA(NonDetOp);

#ifdef __cplusplus
}
#endif
Expand Down
52 changes: 26 additions & 26 deletions include/llzk-c/Dialect/Struct.h
Original file line number Diff line number Diff line change
Expand Up @@ -105,18 +105,18 @@ MLIR_CAPI_EXPORTED MlirType llzkStructDefOpGetType(MlirOperation op);
MLIR_CAPI_EXPORTED MlirType
llzkStructDefOpGetTypeWithParams(MlirOperation op, MlirAttribute params);

/// Returns the operation that defines the field with the given name, if present.
MLIR_CAPI_EXPORTED MlirOperation llzkStructDefOpGetFieldDef(MlirOperation op, MlirStringRef name);
/// Returns the operation that defines the member with the given name, if present.
MLIR_CAPI_EXPORTED MlirOperation llzkStructDefOpGetMemberDef(MlirOperation op, MlirStringRef name);

/// Fills the given array with the FieldDefOp operations inside this struct. The pointer to the
/// operations must have been preallocated. See `llzkStructDefOpGetNumFieldDefs` for obtaining the
/// Fills the given array with the MemberDefOp operations inside this struct. The pointer to the
/// operations must have been preallocated. See `llzkStructDefOpGetNumMemberDefs` for obtaining the
/// required size of the array.
MLIR_CAPI_EXPORTED void llzkStructDefOpGetFieldDefs(MlirOperation op, MlirOperation *dst);
MLIR_CAPI_EXPORTED void llzkStructDefOpGetMemberDefs(MlirOperation op, MlirOperation *dst);

/// Returns the number of FieldDefOp operations defined in this struct.
MLIR_CAPI_EXPORTED intptr_t llzkStructDefOpGetNumFieldDefs(MlirOperation op);
/// Returns the number of MemberDefOp operations defined in this struct.
MLIR_CAPI_EXPORTED intptr_t llzkStructDefOpGetNumMemberDefs(MlirOperation op);

/// Returns true if the struct has fields marked as columns.
/// Returns true if the struct has members marked as columns.
MlirLogicalResult llzkStructDefOpGetHasColumns(MlirOperation op);

/// Returns the FuncDefOp operation that defines the witness computation of the struct.
Expand All @@ -140,45 +140,45 @@ MLIR_CAPI_EXPORTED MlirAttribute llzkStructDefOpGetFullyQualifiedName(MlirOperat
LLZK_DECLARE_OP_PREDICATE(StructDefOp, IsMainComponent);

//===----------------------------------------------------------------------===//
// FieldDefOp
// MemberDefOp
//===----------------------------------------------------------------------===//

/// Returns true if the op is a FieldDefOp
LLZK_DECLARE_OP_ISA(FieldDefOp);
/// Returns true if the op is a MemberDefOp
LLZK_DECLARE_OP_ISA(MemberDefOp);

/// Returns true if the field has been marked public with a PublicAttr
LLZK_DECLARE_OP_PREDICATE(FieldDefOp, HasPublicAttr);
/// Returns true if the member has been marked public with a PublicAttr
LLZK_DECLARE_OP_PREDICATE(MemberDefOp, HasPublicAttr);

/// Sets the public attribute in the given field.
MLIR_CAPI_EXPORTED void llzkFieldDefOpSetPublicAttr(MlirOperation op, bool value);
/// Sets the public attribute in the given member.
MLIR_CAPI_EXPORTED void llzkMemberDefOpSetPublicAttr(MlirOperation op, bool value);

//===----------------------------------------------------------------------===//
// FieldReadOp
// MemberReadOp
//===----------------------------------------------------------------------===//

/// Creates a FieldReadOp.
/// Creates a MemberReadOp.
LLZK_DECLARE_OP_BUILD_METHOD(
FieldReadOp, MlirType type, MlirValue component, MlirStringRef fieldName
MemberReadOp, MlirType type, MlirValue component, MlirStringRef memberName
);

/// Creates a FieldReadOp to a column offset by the given distance affine map. The values in the
/// Creates a MemberReadOp to a column offset by the given distance affine map. The values in the
/// ValueRange are operands representing the arguments to the affine map. The integer value is the
/// number of arguments in the map that are dimensions.
LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD(
FieldReadOp, WithAffineMapDistance, MlirType type, MlirValue component, MlirStringRef fieldName,
MlirAffineMap affineMap, MlirValueRange mapOperands
MemberReadOp, WithAffineMapDistance, MlirType type, MlirValue component,
MlirStringRef memberName, MlirAffineMap affineMap, MlirValueRange mapOperands
);

/// Creates a FieldReadOp to a column offset by the given distance defined by a name to a constant
/// Creates a MemberReadOp to a column offset by the given distance defined by a name to a constant
/// parameter in the struct.
LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD(
FieldReadOp, WithConstParamDistance, MlirType type, MlirValue component,
MlirStringRef fieldName, MlirStringRef paramName
MemberReadOp, WithConstParamDistance, MlirType type, MlirValue component,
MlirStringRef memberName, MlirStringRef paramName
);

/// Creates a FieldReadOp to a column offset by the given distance defined by an integer value.
/// Creates a MemberReadOp to a column offset by the given distance defined by an integer value.
LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD(
FieldReadOp, WithLiteralDistance, MlirType type, MlirValue component, MlirStringRef fieldName,
MemberReadOp, WithLiteralDistance, MlirType type, MlirValue component, MlirStringRef memberName,
int64_t distance
);

Expand Down
38 changes: 0 additions & 38 deletions include/llzk-c/Dialect/Undef.h

This file was deleted.

4 changes: 0 additions & 4 deletions include/llzk-c/Typing.h
Original file line number Diff line number Diff line change
Expand Up @@ -59,10 +59,6 @@ MLIR_CAPI_EXPORTED bool llzkIsValidArrayType(MlirType type);
/// - `StructType` with parameters if `allowStructParams==false`
MLIR_CAPI_EXPORTED bool llzkIsConcreteType(MlirType type, bool allowStructParams);

/// Return `true` iff the given type is a StructType referencing the `COMPONENT_NAME_SIGNAL`
/// struct.
MLIR_CAPI_EXPORTED bool llzkIsSignalType(MlirType type);

/// @brief Return `true` iff the given type contains an AffineMapAttr.
MLIR_CAPI_EXPORTED bool llzkHasAffineMapAttr(MlirType type);

Expand Down
2 changes: 1 addition & 1 deletion include/llzk/Analysis/ConstraintDependencyGraph.h
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ namespace llzk {
/// For example, a CDG of the form: {
/// {%arg1, %arg2, %arg3[@foo]}
/// }
/// Means that %arg1, %arg2, and field @foo of %arg3, are connected
/// Means that %arg1, %arg2, and member @foo of %arg3, are connected
/// via some constraints. These constraints could take the form of (in Circom notation):
/// %arg1 + %arg3[@foo] === %arg2
/// Or
Expand Down
34 changes: 17 additions & 17 deletions include/llzk/Analysis/IntervalAnalysis.h
Original file line number Diff line number Diff line change
Expand Up @@ -207,9 +207,9 @@ class IntervalAnalysisLattice : public dataflow::AbstractSparseLattice {
using LatticeValue = IntervalAnalysisLatticeValue;
// Map mlir::Values to LatticeValues
using ValueMap = mlir::DenseMap<mlir::Value, LatticeValue>;
// Map field references to LatticeValues. Used for field reads and writes.
// Structure is component value -> field attribute -> latticeValue
using FieldMap = mlir::DenseMap<mlir::Value, mlir::DenseMap<mlir::StringAttr, LatticeValue>>;
// Map member references to LatticeValues. Used for member reads and writes.
// Structure is component value -> member attribute -> latticeValue
using MemberMap = mlir::DenseMap<mlir::Value, mlir::DenseMap<mlir::StringAttr, LatticeValue>>;
// Expression to interval map for convenience.
using ExpressionIntervals = mlir::DenseMap<llvm::SMTExprRef, Interval>;
// Tracks all constraints and assignments in insertion order
Expand Down Expand Up @@ -253,7 +253,7 @@ class IntervalDataFlowAnalysis
using Lattice = IntervalAnalysisLattice;
using LatticeValue = IntervalAnalysisLattice::LatticeValue;

// Map fields to their symbols
// Map members to their symbols
using SymbolMap = mlir::DenseMap<SourceRef, llvm::SMTExprRef>;

public:
Expand All @@ -275,12 +275,12 @@ class IntervalDataFlowAnalysis
/// @return
llvm::SMTExprRef getOrCreateSymbol(const SourceRef &r);

const llvm::DenseMap<SourceRef, llvm::DenseSet<Lattice *>> &getFieldReadResults() const {
return fieldReadResults;
const llvm::DenseMap<SourceRef, llvm::DenseSet<Lattice *>> &getMemberReadResults() const {
return memberReadResults;
}

const llvm::DenseMap<SourceRef, ExpressionValue> &getFieldWriteResults() const {
return fieldWriteResults;
const llvm::DenseMap<SourceRef, ExpressionValue> &getMemberWriteResults() const {
return memberWriteResults;
}

private:
Expand All @@ -291,10 +291,10 @@ class IntervalDataFlowAnalysis
bool propagateInputConstraints;
mlir::SymbolTableCollection tables;

// Track field reads so that propagations to fields can be all updated efficiently.
llvm::DenseMap<SourceRef, llvm::DenseSet<Lattice *>> fieldReadResults;
// Track field writes values. For now, we'll overapproximate this.
llvm::DenseMap<SourceRef, ExpressionValue> fieldWriteResults;
// Track member reads so that propagations to members can be all updated efficiently.
llvm::DenseMap<SourceRef, llvm::DenseSet<Lattice *>> memberReadResults;
// Track member writes values. For now, we'll overapproximate this.
llvm::DenseMap<SourceRef, ExpressionValue> memberWriteResults;

void setToEntryState(Lattice *lattice) override {
// Initialize the value with an interval in our specified field.
Expand Down Expand Up @@ -360,12 +360,12 @@ class IntervalDataFlowAnalysis
getGeneralizedDecompInterval(mlir::Operation *baseOp, mlir::Value lhs, mlir::Value rhs);

bool isReadOp(mlir::Operation *op) const {
return llvm::isa<component::FieldReadOp, polymorphic::ConstReadOp, array::ReadArrayOp>(op);
return llvm::isa<component::MemberReadOp, polymorphic::ConstReadOp, array::ReadArrayOp>(op);
}

bool isDefinitionOp(mlir::Operation *op) const {
return llvm::isa<
component::StructDefOp, function::FuncDefOp, component::FieldDefOp, global::GlobalDefOp,
component::StructDefOp, function::FuncDefOp, component::MemberDefOp, global::GlobalDefOp,
mlir::ModuleOp>(op);
}

Expand Down Expand Up @@ -440,15 +440,15 @@ class StructIntervals {
void print(mlir::raw_ostream &os, bool withConstraints = false, bool printCompute = false) const;

const llvm::MapVector<SourceRef, Interval> &getConstrainIntervals() const {
return constrainFieldRanges;
return constrainMemberRanges;
}

const llvm::SetVector<ExpressionValue> getConstrainSolverConstraints() const {
return constrainSolverConstraints;
}

const llvm::MapVector<SourceRef, Interval> &getComputeIntervals() const {
return computeFieldRanges;
return computeMemberRanges;
}

const llvm::SetVector<ExpressionValue> getComputeSolverConstraints() const {
Expand All @@ -465,7 +465,7 @@ class StructIntervals {
component::StructDefOp structDef;
llvm::SMTSolverRef smtSolver;
// llvm::MapVector keeps insertion order for consistent iteration
llvm::MapVector<SourceRef, Interval> constrainFieldRanges, computeFieldRanges;
llvm::MapVector<SourceRef, Interval> constrainMemberRanges, computeMemberRanges;
// llvm::SetVector for the same reasons as above
llvm::SetVector<ExpressionValue> constrainSolverConstraints, computeSolverConstraints;

Expand Down
5 changes: 3 additions & 2 deletions include/llzk/Analysis/Matchers.h
Original file line number Diff line number Diff line change
Expand Up @@ -49,13 +49,14 @@ auto m_CommutativeOp(LhsMatcher lhs, RhsMatcher rhs) {
}

/// @brief Matches and optionally captures a SourceRef base value, which is either
/// a field read or a block argument (i.e., an input to a @constrain or @compute function).
/// a member read or a block argument (i.e., an input to a @constrain or @compute function).
struct RefValueCapture {
mlir::Value *what;
RefValueCapture(mlir::Value *capture) : what(capture) {}

bool match(mlir::Value v) {
if (isa<mlir::BlockArgument>(v) || isa_and_present<component::FieldReadOp>(v.getDefiningOp())) {
if (isa<mlir::BlockArgument>(v) ||
isa_and_present<component::MemberReadOp>(v.getDefiningOp())) {
if (what) {
*what = v;
}
Expand Down
Loading