LLZK 3.0.0
An open-source IR for Zero Knowledge (ZK) circuits
Loading...
Searching...
No Matches
LLZKFuseProductLoopsPass.cpp
Go to the documentation of this file.
1//===-- LLZKFuseProductLoopsPass.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_FUSEPRODUCTLOOPSPASS
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(a.getLowerBound(), a.getUpperBound(), a.getStep());
105 auto tripCountB = constantTripCount(b.getLowerBound(), b.getUpperBound(), b.getStep());
106 if (tripCountA.has_value() && tripCountB.has_value() && *tripCountA == *tripCountB) {
107 return true;
108 }
109
110 if (!isConstOrStructParam(a.getLowerBound()) || !isConstOrStructParam(a.getUpperBound()) ||
111 !isConstOrStructParam(a.getStep()) || !isConstOrStructParam(b.getLowerBound()) ||
112 !isConstOrStructParam(b.getUpperBound()) || !isConstOrStructParam(b.getStep())) {
113 return false;
114 }
115
116 llvm::SMTSolverRef solver = llvm::CreateZ3Solver();
117 solver->addConstraint(/* (actually ask if they "can't be different") */ solver->mkNot(
118 solver->mkEqual(tripCount(a, solver.get()), tripCount(b, solver.get()))
119 ));
120
121 return !*solver->check();
122}
123
127static FailureOr<SmallVector<Operation *>>
128canPrepareForFusion(scf::ForOp witnessLoop, scf::ForOp constraintLoop) {
129 if (witnessLoop->getBlock() != constraintLoop->getBlock()) {
130 return failure();
131 }
132
133 SmallVector<Operation *> opsToSink;
134 for (auto *op = witnessLoop->getNextNode(); op != constraintLoop; op = op->getNextNode()) {
135 if (op->getAttrOfType<StringAttr>(PRODUCT_SOURCE) == "fused") {
136 // "fused" means "compute" + "constrain". Conservatively, a "compute" op we want to sink can't
137 // be sunk if it also has "constrain" since we need to preserve the relative orders within
138 // compute/constrain
139 return failure();
140 }
141 if (op->getAttrOfType<StringAttr>(PRODUCT_SOURCE) == FUNC_NAME_COMPUTE) {
142 opsToSink.push_back(op);
143 }
144 }
145 return opsToSink;
146}
147
148static LogicalResult
149prepareForFusion(scf::ForOp witnessLoop, scf::ForOp constraintLoop, IRRewriter &rewriter) {
150 auto computeOpsToSink = canPrepareForFusion(witnessLoop, constraintLoop);
151 if (failed(computeOpsToSink)) {
152 return failure();
153 }
154
155 Operation *insertionPoint = constraintLoop.getOperation();
156 for (Operation *op : *computeOpsToSink) {
157 rewriter.moveOpAfter(op, insertionPoint);
158 insertionPoint = op;
159 }
160
161 return success();
162}
163
164static LogicalResult fuseMatchingLoopPairs(Region &body, MLIRContext *context) {
165 // Start by collecting all possible loops
166 llvm::SmallVector<scf::ForOp> witnessLoops, constraintLoops;
167 body.walk<WalkOrder::PreOrder>([&witnessLoops, &constraintLoops](scf::ForOp forOp) {
168 if (!forOp->hasAttrOfType<StringAttr>(PRODUCT_SOURCE)) {
169 return WalkResult::skip();
170 }
171 auto productSource = forOp->getAttrOfType<StringAttr>(PRODUCT_SOURCE);
172 if (productSource == FUNC_NAME_COMPUTE) {
173 witnessLoops.push_back(forOp);
174 } else if (productSource == FUNC_NAME_CONSTRAIN) {
175 constraintLoops.push_back(forOp);
176 }
177 // Skipping here, because any nested loops can't possibly be fused at this stage
178 return WalkResult::skip();
179 });
180
181 // A pair of loops will be fused iff (1) they can be fused according to the rules above, and (2)
182 // neither can be fused with anything else (so there's no ambiguity)
184 witnessLoops, constraintLoops, canLoopsBeFused
185 );
186
187 // This shouldn't happen, since we allow partial matches
188 if (failed(fusionCandidates)) {
189 return failure();
190 }
191
192 // Finally, fuse all the marked loops...
193 IRRewriter rewriter {context};
194 for (auto [w, c] : *fusionCandidates) {
195 if (failed(prepareForFusion(w, c, rewriter))) {
196 continue;
197 }
198 auto fusedLoop = fuseIndependentSiblingForLoops(w, c, rewriter);
199 fusedLoop->setAttr(PRODUCT_SOURCE, rewriter.getAttr<StringAttr>("fused"));
200 // ...and recurse to fuse nested loops
201 if (failed(fuseMatchingLoopPairs(fusedLoop.getBodyRegion(), context))) {
202 return failure();
203 }
204 }
205 return success();
206}
207
208class PassImpl : public llzk::impl::FuseProductLoopsPassBase<PassImpl> {
209 using Base = FuseProductLoopsPassBase<PassImpl>;
210 using Base::Base;
211
212 void runOnOperation() override {
213 ModuleOp mod = getOperation();
214 mod.walk([this](function::FuncDefOp funcDef) {
215 if (funcDef.isStructProduct()) {
216 if (failed(fuseMatchingLoopPairs(funcDef.getFunctionBody(), &getContext()))) {
217 signalPassFailure();
218 }
219 }
220 });
221 }
222};
223
224} // namespace
bool isStructProduct()
Return true iff the function is within a StructDefOp and named FUNC_NAME_PRODUCT.
Definition Ops.h.inc:905
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