Add pass to algebraize felt operations by krushimir · Pull Request #640 · project-llzk/llzk-lib

krushimir · 2026-07-23T16:14:45Z

Implements stage 2 of #585.

Adds -llzk-algebraize-felt-ops, an LLZK pre-lowering pass for functions marked function.allow_constraint. It lowers unsupported felt bitwise, shift, inverse, division, unsigned division, and modulo operations into basic felt arithmetic, nondeterministic witnesses, bit decompositions, and equality constraints.

The pass reuses decompositions, uses known width bounds where available, and rejects unsupported division/modulo cases rather than producing unsound constraints.

Tested with the AlgebraizeFeltOps and PCLLowering lit suites (15 tests).

iangneal · 2026-07-24T15:14:21Z

@codex review

chatgpt-codex-connector · 2026-07-24T15:17:03Z

Review

No blocking issues found in the proposed algebraization pass.

The implementation consistently limits rewriting to constraint-bearing functions, handles unsupported unsigned division/modulo inputs with explicit diagnostics, and avoids caching full-width bit decompositions that could represent non-canonical field values. lib/Transforms/LLZKAlgebraizeFeltOpsPass.cppL353-L364 lib/Transforms/LLZKAlgebraizeFeltOpsPass.cppL571-L590 lib/Transforms/LLZKAlgebraizeFeltOpsPass.cppL665-L680

I did not modify the branch, so no commit or follow-up pull request was created.

Checks

✅ git diff --check 286358af11c34836b75d20bdb304dff4d26345e7...HEAD
⚠️ nix develop --command bash -c 'cmake --build build --target check-lit' — could not run because nix is not installed in this environment.

View task →

raghav198 · 2026-07-27T20:22:31Z

+const llvm::APInt &ConstrainAlgebraizer::primeOf(Type type) {
+  auto [it, inserted] = primes.try_emplace(type);
+  if (inserted) {
+    FeltType feltType = llvm::cast<FeltType>(type);


This cast might fail if the type passed in isn't actually a !felt.type, right? Can we have this method just take a FeltType and require the caller to check the cast instead?

Similar comments elsewhere llvm::cast<FeltType>(...) is used

Seconding this suggestion

0xddom · 2026-07-28T13:28:06Z

+      %self = struct.new : <@MixedXor>
+      function.return %self : !struct.type<@MixedXor>
+    }
+    function.def @constrain(%self: !struct.type<@MixedXor>, %a: !F, %b: !F) attributes {function.allow_constraint, function.allow_non_native_field_ops} {


Since this pass removes all the operations enabled by this attribute, we could also remove it from the function.

0xddom · 2026-07-28T13:30:53Z

@@ -0,0 +1,29 @@
+// RUN: llzk-opt -llzk-algebraize-felt-ops %s > /dev/null


Is this test a TODO?

0xddom · 2026-07-28T13:44:07Z

+const llvm::APInt &ConstrainAlgebraizer::primeOf(Type type) {
+  auto [it, inserted] = primes.try_emplace(type);
+  if (inserted) {
+    FeltType feltType = llvm::cast<FeltType>(type);


Seconding this suggestion

0xddom · 2026-07-28T13:50:48Z

+  for (unsigned i = 0, e = sBits.size(); i < e; ++i) {
+    llvm::APInt cMinus1 = toExactWidthAPInt(curPow2 - 1, constBits);
+    Value scaled = b.create<MulFeltOp>(loc, sBits[i], feltConst(loc, type, cMinus1));


nit: i is not used anywhere else in this loop

Suggested change

for (unsigned i = 0, e = sBits.size(); i < e; ++i) {

llvm::APInt cMinus1 = toExactWidthAPInt(curPow2 - 1, constBits);

Value scaled = b.create<MulFeltOp>(loc, sBits[i], feltConst(loc, type, cMinus1));

for (auto &sBit : sBits) {

llvm::APInt cMinus1 = toExactWidthAPInt(curPow2 - 1, constBits);

Value scaled = b.create<MulFeltOp>(loc, sBit, feltConst(loc, type, cMinus1));

0xddom · 2026-07-28T13:59:36Z

+/// Records the bound proven by an asserted range guard
+/// `constrain.eq(cast.tofelt(bool.cmp lt/le/gt/ge(x, c)), 1)` — the pattern
+/// frontends emit to pin blackbox input widths. Only guards at the top level
+/// of the body may be harvested: a guard inside a conditional region holds
+/// only on its branch.


What's the purpose of these guards in relation to the ops converted by this pass? Because, when converting an op inside a conditional block, wouldn't we be missing a range constraint for that op if it was also defined inside the same block?

0xddom · 2026-07-28T14:10:46Z

+  for (unsigned i = 1, e = bits.size(); i < e; ++i) {
+    Value term = b.create<MulFeltOp>(loc, bits[i], feltConst(loc, type, weight));


nit: similar comment about i

Suggested change

for (unsigned i = 1, e = bits.size(); i < e; ++i) {

Value term = b.create<MulFeltOp>(loc, bits[i], feltConst(loc, type, weight));

for (auto &bit : bits.drop_front()) {

Value term = b.create<MulFeltOp>(loc, bit, feltConst(loc, type, weight));

0xddom · 2026-07-28T14:35:23Z

+  for (Operation &op : fn.getBody().front()) {
+    if (auto eq = llvm::dyn_cast<EmitEqualityOp>(&op)) {
+      harvestRangeGuard(eq.getLhs(), eq.getRhs());
+      harvestRangeGuard(eq.getRhs(), eq.getLhs());
+    }
+  }


Suggested change

for (Operation &op : fn.getBody().front()) {

if (auto eq = llvm::dyn_cast<EmitEqualityOp>(&op)) {

harvestRangeGuard(eq.getLhs(), eq.getRhs());

harvestRangeGuard(eq.getRhs(), eq.getLhs());

}

}

fn.walk([this](EmitEqualityOp eq) {

harvestRangeGuard(eq.getLhs(), eq.getRhs());

harvestRangeGuard(eq.getRhs(), eq.getLhs());

});

0xddom · 2026-07-28T14:36:16Z

+  // rewritten op's result bound (set by cacheResultBits) feeds later ops.
+  // The snapshot keeps the loop off the ops the rewrites create.
+  SmallVector<Operation *> ops;
+  fn.walk([&](Operation *op) { ops.push_back(op); });


nit: prefer to pass only the bindings actually used by the lambda

Suggested change

fn.walk([&](Operation *op) { ops.push_back(op); });

fn.walk([&ops](Operation *op) { ops.push_back(op); });

0xddom · 2026-07-28T14:39:26Z

+  // One pass in program order: operands are defined before uses, so bounds
+  // are propagated before the ops consuming them are rewritten, and a
+  // rewritten op's result bound (set by cacheResultBits) feeds later ops.
+  // The snapshot keeps the loop off the ops the rewrites create.
+  SmallVector<Operation *> ops;
+  fn.walk([&](Operation *op) { ops.push_back(op); });
+
+  for (Operation *op : ops) {


Instead of iterating over all the operations twice you could run the algorithm in the first pass, accumulating the to-be-removed ops along with their replacement. Then do another loop that actually removes and replaces the ops.

0xddom · 2026-07-28T14:41:25Z

  }];
 }

+def AlgebraizeFeltOpsPass : LLZKPass<"llzk-algebraize-felt-ops"> {


The pass could be made an operation pass for function.def. We don't need a whole-world pass for this and will allow running in parallel.

krushimir requested a review from a team as a code owner July 23, 2026 16:14

krushimir force-pushed the krushimir/algebraize-felt-ops branch from db87d75 to a3adba9 Compare July 23, 2026 16:19

Add llzk-algebraize-felt-ops pass

b9540cf

krushimir force-pushed the krushimir/algebraize-felt-ops branch from a3adba9 to b9540cf Compare July 24, 2026 05:50

Merge branch 'main' into krushimir/algebraize-felt-ops

7c91c0b

krushimir mentioned this pull request Jul 24, 2026

Arithmetize constraint-side scf.if operations #643

Open

raghav198 reviewed Jul 27, 2026

View reviewed changes

0xddom reviewed Jul 28, 2026

View reviewed changes

		@@ -0,0 +1,29 @@
		// RUN: llzk-opt -llzk-algebraize-felt-ops %s > /dev/null

		for (unsigned i = 1, e = bits.size(); i < e; ++i) {
		Value term = b.create<MulFeltOp>(loc, bits[i], feltConst(loc, type, weight));

	fn.walk([&](Operation *op) { ops.push_back(op); });
	fn.walk([&ops](Operation *op) { ops.push_back(op); });

Uh oh!

Conversation

krushimir commented Jul 23, 2026

Uh oh!

iangneal commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Jul 24, 2026

Review

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

iangneal commented Jul 24, 2026 •

edited

Loading