LLZK 3.0.0
An open-source IR for Zero Knowledge (ZK) circuits
Loading...
Searching...
No Matches
LLZKFuseProductControlFlowPass.cpp
Go to the documentation of this file.
1//===-- LLZKFuseProductControlFlowPass.cpp ----------------------*- C++ -*-===//
2//
3// Part of the LLZK Project, under the Apache License v2.0.
4// See LICENSE.txt for license information.
5// Copyright 2026 Project LLZK
6// SPDX-License-Identifier: Apache-2.0
7//
8//===----------------------------------------------------------------------===//
13//===----------------------------------------------------------------------===//
14
21#include "llzk/Util/Constants.h"
22
23#include <mlir/Dialect/SCF/Utils/Utils.h>
24
25#include <llvm/Support/Debug.h>
26#include <llvm/Support/SMTAPI.h>
27
28#include <memory>
29#include <optional>
30
31// Include the generated base pass class definitions.
32namespace llzk {
33#define GEN_PASS_DEF_FUSEPRODUCTCONTROLFLOWPASS
35} // namespace llzk
36
37namespace {
38
39using namespace mlir;
40using namespace llzk;
41
42// Bitwidth of `index` for instantiating SMT variables
43constexpr int INDEX_WIDTH = 64;
44
45static inline bool isConstOrStructParam(Value val) {
46 // TODO: doing arithmetic over constants should also be fine?
47 return llvm::isa<arith::ConstantIndexOp, polymorphic::ConstReadOp, felt::FeltConstantOp>(
48 val.getDefiningOp()
49 );
50}
51
52static llvm::SMTExprRef mkExpr(Value value, llvm::SMTSolver *solver) {
53 if (auto constOp = value.getDefiningOp<arith::ConstantIndexOp>()) {
54 return solver->mkBitvector(llvm::APSInt::get(constOp.value()), INDEX_WIDTH);
55 } else if (auto polyReadOp = value.getDefiningOp<polymorphic::ConstReadOp>()) {
56
57 return solver->mkSymbol(
58 std::string {polyReadOp.getConstName()}.c_str(), solver->getBitvectorSort(INDEX_WIDTH)
59 );
60 }
61 assert(false && "unsupported: checking non-constant trip counts");
62 return nullptr; // Unreachable
63}
64
65static llvm::SMTExprRef tripCount(scf::ForOp op, llvm::SMTSolver *solver) {
66 const auto *one = solver->mkBitvector(llvm::APSInt::get(1), INDEX_WIDTH);
67 return solver->mkBVSDiv(
68 solver->mkBVAdd(
69 one,
70 solver->mkBVSub(mkExpr(op.getUpperBound(), solver), mkExpr(op.getLowerBound(), solver))
71 ),
72 mkExpr(op.getStep(), solver)
73 );
74}
75
76static inline bool canLoopsBeFused(scf::ForOp a, scf::ForOp b) {
77 // A priori, two loops can be fused if:
78 // 1. They live in the same parent region,
79 // 2. One comes from witgen and the other comes from constraint gen, and
80 // 3. They have the same trip count
81
82 // Check 1.
83 if (a->getParentRegion() != b->getParentRegion()) {
84 return false;
85 }
86
87 // Check 2.
88 if (!a->hasAttrOfType<StringAttr>(PRODUCT_SOURCE) ||
89 !b->hasAttrOfType<StringAttr>(PRODUCT_SOURCE)) {
90 // Ideally this should never happen, since the pass only runs on fused @product functions, but
91 // check anyway just to be safe
92 return false;
93 }
94 if (a->getAttrOfType<StringAttr>(PRODUCT_SOURCE) ==
95 b->getAttrOfType<StringAttr>(PRODUCT_SOURCE)) {
96 return false;
97 }
98
99 // Check 3.
100 // Easy case: both have a constant trip-count. If the trip counts are not "constant up to a struct
101 // param", we definitely can't tell if they're equal. If the trip counts are only "constant up to
102 // a struct param" but not actually constant, we can ask a solver if the equations are guaranteed
103 // to be the same
104 auto tripCountA = constantTripCount(
105 a.getLowerBound(), a.getUpperBound(), a.getStep(), /*isSigned=*/!a.getUnsignedCmp(),
106 scf::computeUbMinusLb
107 );
108 auto tripCountB = constantTripCount(
109 b.getLowerBound(), b.getUpperBound(), b.getStep(), /*isSigned=*/!b.getUnsignedCmp(),
110 scf::computeUbMinusLb
111 );
112 if (tripCountA.has_value() && tripCountB.has_value() && *tripCountA == *tripCountB) {
113 return true;
114 }
115
116 if (!isConstOrStructParam(a.getLowerBound()) || !isConstOrStructParam(a.getUpperBound()) ||
117 !isConstOrStructParam(a.getStep()) || !isConstOrStructParam(b.getLowerBound()) ||
118 !isConstOrStructParam(b.getUpperBound()) || !isConstOrStructParam(b.getStep())) {
119 return false;
120 }
121
122 llvm::SMTSolverRef solver = llvm::CreateZ3Solver();
123 solver->addConstraint(/* (actually ask if they "can't be different") */ solver->mkNot(
124 solver->mkEqual(tripCount(a, solver.get()), tripCount(b, solver.get()))
125 ));
126
127 return !*solver->check();
128}
129
133static FailureOr<SmallVector<Operation *>>
134canPrepareForFusion(scf::ForOp witnessLoop, scf::ForOp constraintLoop) {
135 if (witnessLoop->getBlock() != constraintLoop->getBlock()) {
136 return failure();
137 }
138
139 SmallVector<Operation *> opsToSink;
140 for (auto *op = witnessLoop->getNextNode(); op != constraintLoop; op = op->getNextNode()) {
141 if (op->getAttrOfType<StringAttr>(PRODUCT_SOURCE) == "fused") {
142 // "fused" means "compute" + "constrain". Conservatively, a "compute" op we want to sink can't
143 // be sunk if it also has "constrain" since we need to preserve the relative orders within
144 // compute/constrain
145 return failure();
146 }
147 if (op->getAttrOfType<StringAttr>(PRODUCT_SOURCE) == FUNC_NAME_COMPUTE) {
148 opsToSink.push_back(op);
149 }
150 }
151 return opsToSink;
152}
153
154static LogicalResult
155prepareForFusion(scf::ForOp witnessLoop, scf::ForOp constraintLoop, IRRewriter &rewriter) {
156 auto computeOpsToSink = canPrepareForFusion(witnessLoop, constraintLoop);
157 if (failed(computeOpsToSink)) {
158 return failure();
159 }
160
161 Operation *insertionPoint = constraintLoop.getOperation();
162 for (Operation *op : *computeOpsToSink) {
163 rewriter.moveOpAfter(op, insertionPoint);
164 insertionPoint = op;
165 }
166
167 return success();
168}
169
170static LogicalResult fuseMatchingLoopPairs(Region &body, MLIRContext *context) {
171 // Start by collecting all possible loops
172 llvm::SmallVector<scf::ForOp> witnessLoops, constraintLoops;
173 body.walk<WalkOrder::PreOrder>([&witnessLoops, &constraintLoops](scf::ForOp forOp) {
174 if (!forOp->hasAttrOfType<StringAttr>(PRODUCT_SOURCE)) {
175 return WalkResult::skip();
176 }
177 auto productSource = forOp->getAttrOfType<StringAttr>(PRODUCT_SOURCE);
178 if (productSource == FUNC_NAME_COMPUTE) {
179 witnessLoops.push_back(forOp);
180 } else if (productSource == FUNC_NAME_CONSTRAIN) {
181 constraintLoops.push_back(forOp);
182 }
183 // Skipping here, because any nested loops can't possibly be fused at this stage
184 return WalkResult::skip();
185 });
186
187 // A pair of loops will be fused iff (1) they can be fused according to the rules above, and (2)
188 // neither can be fused with anything else (so there's no ambiguity)
190 witnessLoops, constraintLoops, canLoopsBeFused
191 );
192
193 // This shouldn't happen, since we allow partial matches
194 if (failed(fusionCandidates)) {
195 return failure();
196 }
197
198 // Finally, fuse all the marked loops...
199 IRRewriter rewriter {context};
200 for (auto [w, c] : *fusionCandidates) {
201 if (failed(prepareForFusion(w, c, rewriter))) {
202 continue;
203 }
204 auto fusedLoop = fuseIndependentSiblingForLoops(w, c, rewriter);
205 fusedLoop->setAttr(PRODUCT_SOURCE, rewriter.getAttr<StringAttr>("fused"));
206 // ...and recurse to fuse nested loops
207 if (failed(fuseMatchingLoopPairs(fusedLoop.getBodyRegion(), context))) {
208 return failure();
209 }
210 }
211 return success();
212}
213
214class PassImpl : public llzk::impl::FuseProductControlFlowPassBase<PassImpl> {
215 using Base = FuseProductControlFlowPassBase<PassImpl>;
216 using Base::Base;
217
218 void runOnOperation() override {
219 ModuleOp mod = getOperation();
220 mod.walk([this](function::FuncDefOp funcDef) {
221 if (funcDef.isStructProduct()) {
222 if (failed(fuseMatchingLoopPairs(funcDef.getFunctionBody(), &getContext()))) {
223 signalPassFailure();
224 }
225 }
226 });
227 }
229
230} // namespace
bool isStructProduct()
Return true iff the function is within a StructDefOp and named FUNC_NAME_PRODUCT.
Definition Ops.h.inc:1102
llvm::FailureOr< llvm::SetVector< std::pair< ValueT, ValueT > > > getMatchingPairs(llvm::ArrayRef< ValueT > as, llvm::ArrayRef< ValueT > bs, FnT doesMatch, bool allowPartial=true)
constexpr char FUNC_NAME_COMPUTE[]
Symbol name for the witness generation (and resp.
Definition Constants.h:16
ExpressionValue mod(const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
constexpr char PRODUCT_SOURCE[]
Name of the attribute on aligned product program ops that specifies where they came from.
Definition Constants.h:40
constexpr char FUNC_NAME_CONSTRAIN[]
Definition Constants.h:17