Skip to content

Arithmetize constraint-side scf.if operations - #643

Open
krushimir wants to merge 2 commits into
project-llzk:mainfrom
reilabs:krushimir/arithmetize-scf-if
Open

Arithmetize constraint-side scf.if operations#643
krushimir wants to merge 2 commits into
project-llzk:mainfrom
reilabs:krushimir/arithmetize-scf-if

Conversation

@krushimir

Copy link
Copy Markdown

Implements stage 3 of #585.

Adds -llzk-arithmetize-scf-if, which replaces constraint-side scf.if operations with select polynomials. Felt results use else + condition * (then - else), while branch constraints are gated so inactive branches do not apply. Nested conditionals are supported.

Because both branches execute after rewriting, branch operations must be safe to speculate. Unsupported operations and non-felt results or constraints are rejected. Run -llzk-algebraize-felt-ops first for felt division and non-native operations.

Also fixes PCL legalization for operations outside constraint functions, such as scf operations in @compute.

Tested with the ArithmetizeSCFIf and PCLLowering lit suites. Together with #586 and #640, the full pipeline lowers all eight noir_llzk examples, including multi_scalar_mul.

@krushimir
krushimir requested a review from a team as a code owner July 24, 2026 06:25
@krushimir
krushimir force-pushed the krushimir/arithmetize-scf-if branch from ef3b102 to e174691 Compare July 24, 2026 06:30
@iangneal

Copy link
Copy Markdown
Contributor

@codex review

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Breezy!

Reviewed commit: 3db75d8bf9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@0xddom

0xddom commented Jul 28, 2026

Copy link
Copy Markdown
Contributor

Also fixes PCL legalization for operations outside constraint functions, such as scf operations in @compute.

The PCL conversion pass shouldn't care about what goes on inside @compute, so I don't fully understand this point.

@0xddom 0xddom left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Still going through the code. I have a first batch of comments.

Comment on lines +143 to +149
if (failed(validateBranch(ifOp, ifOp.getThenRegion().front()))) {
return failure();
}
if (!ifOp.getElseRegion().empty() && failed(validateBranch(ifOp, ifOp.getElseRegion().front()))) {
return failure();
}
return success();

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

success and failure accept a bool as optional argument so this could be written as something similar to this:

Suggested change
if (failed(validateBranch(ifOp, ifOp.getThenRegion().front()))) {
return failure();
}
if (!ifOp.getElseRegion().empty() && failed(validateBranch(ifOp, ifOp.getElseRegion().front()))) {
return failure();
}
return success();
return failure(
failed(validateBranch(ifOp, ifOp.getThenRegion().front())) ||
(!ifOp.getElseRegion().empty() && failed(validateBranch(ifOp, ifOp.getElseRegion().front())))
);

continue;
}
if (auto eq = llvm::dyn_cast<EmitEqualityOp>(op)) {
if (!llvm::isa<FeltType>(eq.getLhs().getType())) {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is not necessarily the case that eq.getLhs().getType() == eq.getRhs().getType() so this check should probably handle both.

Comment on lines +125 to +127
op.emitError() << "cannot arithmetize scf.if branch operation '" << op.getName()
<< "' because executing both branches may change its effects";
return failure();

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The result of this expression can be converted into a LogicalResult.

Suggested change
op.emitError() << "cannot arithmetize scf.if branch operation '" << op.getName()
<< "' because executing both branches may change its effects";
return failure();
return op.emitError() << "cannot arithmetize scf.if branch operation '" << op.getName()
<< "' because executing both branches may change its effects";

There are other places where this could be applied as well.

Comment on lines +252 to +256
for (mlir::scf::IfOp ifOp : ifOps) {
if (failed(validate(ifOp))) {
return failure();
}
}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can use llvm::any_of for this. Something like

if (llvm::any_of(ifOps, [this](mlir::scf::IfOp ifOp) { return failed(validate(ifOp)); })) {
  return failure();
}

}];
}

def ArithmetizeSCFIfPass : LLZKPass<"llzk-arithmetize-scf-if"> {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can also make this pass an op pass for function.def. The same rationale in #640 applies here.

@V-k-h

V-k-h commented Jul 29, 2026

Copy link
Copy Markdown

Built this branch and ran it on a real Noir multi_scalar_mul circuit: --llzk-arithmetize-scf-if cleanly dissolves all ~2800 constraint-side scf.if (2801 → 0), with end-to-end lowering then gated only on the felt-op support in #640. Nice to see this land — the else + condition * (then − else) approach is exactly right.

Minor, and pre-existing (not introduced here): with the pass built but not invoked, --llzk-full-r1cs-lowering still segfaults in lowerPolyToR1CS on a data-dependent scf.if, whereas --llzk-to-pcl rejects the same input cleanly (failed to legalize operation 'arith.select'). Happy to file that separately if it's useful rather than something you're already handling as part of the pipeline wiring.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants