llzk::ConstraintDependencyGraph Class Reference

A dependency graph of constraints enforced by an LLZK struct. More...

#include <ConstraintDependencyGraph.h>

Public Member Functions
void	dump () const
	Dumps the CDG to stderr.
void	print (mlir::raw_ostream &os) const
	Print the CDG to the specified output stream.
ConstraintDependencyGraph	translate (ConstrainRefRemappings translation) const
	Translate the ConstrainRefs in this CDG to that of a different context.
ConstrainRefSet	getConstrainingValues (const ConstrainRef &ref) const
	Get the values that are connected to the given ref via emitted constraints.
	ConstraintDependencyGraph (const ConstraintDependencyGraph &other)
ConstraintDependencyGraph &	operator= (const ConstraintDependencyGraph &other)
	~ConstraintDependencyGraph ()=default

Static Public Member Functions
static mlir::FailureOr< ConstraintDependencyGraph >	compute (mlir::ModuleOp mod, component::StructDefOp s, mlir::DataFlowSolver &solver, mlir::AnalysisManager &am)
	Compute a ConstraintDependencyGraph (CDG)

Detailed Description

A dependency graph of constraints enforced by an LLZK struct.

Mathematically speaking, a constraint dependency graph (CDG) is a transitive closure of edges where there is an edge between signals a and b iff a and b appear in the same constraint.

Less formally, a CDG is a set of signals that constrain one another through one or more emit operations (constrain.in or constrain.eq). The CDG only indicate that signals are connected by constraints, but do not include information about the type of computation that binds them together.

For example, a CDG of the form: { {arg1, arg2, arg3[@foo]} } Means that arg1, arg2, and field @foo of arg3, are connected via some constraints. These constraints could take the form of (in Circom notation): arg1 + arg3[@foo] === arg2 Or arg2 === arg2 / arg3[@foo] Or any other form of constraint including those values.

The CDG also records information about constant values (e.g., felt.const) that are included in constraints, but does not compute a transitive closure over constant values, as constant value usage in constraints does not imply any dependency between signal values (e.g., constraints a + b === 0 and c + d === 0 both use constant 0, but does not enforce a dependency between a, b, c, and d).

Definition at line 100 of file ConstraintDependencyGraph.h.

Constructor & Destructor Documentation

ConstraintDependencyGraph()

llzk::ConstraintDependencyGraph::ConstraintDependencyGraph ( const ConstraintDependencyGraph & other )

inline

Definition at line 147 of file ConstraintDependencyGraph.h.

~ConstraintDependencyGraph()

llzk::ConstraintDependencyGraph::~ConstraintDependencyGraph ( )

default

Member Function Documentation

compute()

mlir::FailureOr< ConstraintDependencyGraph > llzk::ConstraintDependencyGraph::compute ( mlir::ModuleOp mod, component::StructDefOp s, mlir::DataFlowSolver & solver, mlir::AnalysisManager & am )

static

Compute a ConstraintDependencyGraph (CDG)

Parameters

mod	The LLZK-complaint module that is the parent of struct s.
s	The struct to compute the CDG for.
solver	A pre-configured DataFlowSolver. The liveness of the struct must already be computed in this solver in order for the constraint analysis to run.
am	A module-level analysis manager. This analysis manager needs to originate from a module-level analysis (i.e., for the mod module) so that analyses for other constraints can be queried via the getChildAnalysis method.

Returns

Definition at line 244 of file ConstraintDependencyGraph.cpp.

dump()

void llzk::ConstraintDependencyGraph::dump

(

)

const

Dumps the CDG to stderr.

Definition at line 254 of file ConstraintDependencyGraph.cpp.

getConstrainingValues()

ConstrainRefSet llzk::ConstraintDependencyGraph::getConstrainingValues

(

const ConstrainRef &

ref

)

const

Get the values that are connected to the given ref via emitted constraints.

This method looks for constraints to the value in the ref and constraints to any prefix of this value. For example, if ref is an array element (foo[2]), this looks for constraints on foo[2] as well as foo, as arrays may be constrained in their entirety via constrain.in operations.

Parameters

ref

Returns

The set of references that are connected to ref via constraints.

Definition at line 510 of file ConstraintDependencyGraph.cpp.

operator=()

ConstraintDependencyGraph & llzk::ConstraintDependencyGraph::operator= ( const ConstraintDependencyGraph & other )

inline

Definition at line 150 of file ConstraintDependencyGraph.h.

print()

void llzk::ConstraintDependencyGraph::print

(

mlir::raw_ostream &

os

)

const

Print the CDG to the specified output stream.

Print all constraints. Any element that is unconstrained is omitted.

Parameters

os	The LLVM/MLIR output stream.

Definition at line 257 of file ConstraintDependencyGraph.cpp.

translate()

ConstraintDependencyGraph llzk::ConstraintDependencyGraph::translate

(

ConstrainRefRemappings

translation

)

const

Translate the ConstrainRefs in this CDG to that of a different context.

Used to translate a CDG of a struct to a CDG for a called subcomponent.

Parameters

translation

A vector of mappings of current reference prefix -> translated reference prefix.

Returns

A CDG that contains only translated references. Non-constant references with no translation are omitted. This omissions allows calling components to ignore internal references within subcomponents that are inaccessible to the caller.

Definition at line 428 of file ConstraintDependencyGraph.cpp.

---

The documentation for this class was generated from the following files:

• include/llzk/Analysis/ConstraintDependencyGraph.h
• lib/Analysis/ConstraintDependencyGraph.cpp