LLZK 0.1.0
Veridise's ZK Language IR
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | List of all members
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 (SourceRefRemappings translation) const
 Translate the SourceRefs in this CDG to that of a different context.
SourceRefSet getConstrainingValues (const SourceRef &ref) const
 Get the values that are connected to the given ref via emitted constraints.
const SourceRefLattice::Ref2Val & getRef2Val () const
 ConstraintDependencyGraph (const ConstraintDependencyGraph &other)
ConstraintDependencyGraph & operator= (const ConstraintDependencyGraph &other)
virtual ~ConstraintDependencyGraph ()=default

Static Public Member Functions

static mlir::FailureOr< ConstraintDependencyGraph > compute (mlir::ModuleOp mod, component::StructDefOp s, mlir::DataFlowSolver &solver, mlir::AnalysisManager &am, const CDGAnalysisContext &ctx)
 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 120 of file ConstraintDependencyGraph.h.

Constructor & Destructor Documentation

◆ ConstraintDependencyGraph()

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

Definition at line 170 of file ConstraintDependencyGraph.h.

◆ ~ConstraintDependencyGraph()

virtual llzk::ConstraintDependencyGraph::~ConstraintDependencyGraph ( )
virtualdefault

Member Function Documentation

◆ compute()

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

Compute a ConstraintDependencyGraph (CDG)

Parameters
modThe LLZK-complaint module that is the parent of struct s.
sThe struct to compute the CDG for.
solverA pre-configured DataFlowSolver. The liveness of the struct must already be computed in this solver in order for the constraint analysis to run.
amA 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.
ctxThe analysis context.
Returns

Definition at line 281 of file ConstraintDependencyGraph.cpp.

◆ dump()

void llzk::ConstraintDependencyGraph::dump ( ) const

Dumps the CDG to stderr.

Definition at line 292 of file ConstraintDependencyGraph.cpp.

◆ getConstrainingValues()

SourceRefSet llzk::ConstraintDependencyGraph::getConstrainingValues ( const SourceRef & 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 585 of file ConstraintDependencyGraph.cpp.

◆ getRef2Val()

const SourceRefLattice::Ref2Val & llzk::ConstraintDependencyGraph::getRef2Val ( ) const
inline

Definition at line 162 of file ConstraintDependencyGraph.h.

◆ operator=()

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

Definition at line 174 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
osThe LLVM/MLIR output stream.

Definition at line 295 of file ConstraintDependencyGraph.cpp.

◆ translate()

ConstraintDependencyGraph llzk::ConstraintDependencyGraph::translate ( SourceRefRemappings translation) const

Translate the SourceRefs 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
translationA 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 493 of file ConstraintDependencyGraph.cpp.

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