`verif` to `smt` conversion by iangneal · Pull Request #549 · project-llzk/llzk-lib

iangneal · 2026-06-17T00:28:07Z

Adds pass for fixpoint scalarization
Adds a pass for converting scalarized verif contracts to smt
Adds a pass pipeline for scalarizing and converting verif to smt
Generalizes some function and call specific conversions to accept contracts and includes, since contracts are function-like and includes are call-like

…o-smt

github-actions · 2026-06-17T00:33:20Z

Test Results

0 files - 2 0 suites - 2 0s ⏱️ - 5m 12s
0 tests - 259 0 ✅ - 253 0 💤 - 6 0 ❌ ±0
0 runs - 518 0 ✅ - 506 0 💤 - 12 0 ❌ ±0

Results for commit 06f2bf6. ± Comparison against base commit 3196c35.

♻️ This comment has been updated with latest results.

tim-hoffman · 2026-06-17T16:23:48Z

+def AggregateScalarizationPass : LLZKPass<"llzk-aggregate-scalarization"> {
+  let summary =
+      "Repeatedly scalarize array/pod aggregates until the module stabilizes";
+  let description = [{
+    Repeatedly runs the existing array-to-scalar and pod-to-scalar passes,
+    followed by canonicalization, until the module reaches a fixpoint. This is
+    intended as a reusable preprocessing step for pipelines that need
+    array/pod-free IR.
+  }];
+  let options = [];
+}


I've been thinking about this a bit and I think we can augment array-to-scalar to split arrays within a pod (just create N pod records, similar to how splitting an array-type struct member) so that a single pass of array-to-scalar then pod-to-scalar can remove all.

Since that'll take a bit more effort, can we add that as a TODO and keep this solution for now?

Update, Raghav needed all pod types removed without also removing array types so this PR increases the capabilities of pod-to-scalar such that running it should be able to remove all pod.type even within an array so pipelines can just run it before array-to-scalar.

tim-hoffman · 2026-06-18T19:39:33Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1febe215c7

ℹ️ 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".

tim-hoffman

I have a few files to go through still but here's my feedback so far

iangneal · 2026-06-19T03:43:50Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 375f7a624e

ℹ️ 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".

iangneal · 2026-06-19T04:14:46Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ab98bea16b

ℹ️ 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".

iangneal · 2026-06-19T04:50:59Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 38478589cd

ℹ️ 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

The verif to smt pass needs some work. A cleaner approach is to let the different dialects define how to lower to smt, similar to how lowering to LLVM works in upstream MLIR. The pass' name hints that is going to lower only operations from the verif dialect, but it lowers everything that is meant to be lowered to smt. The pass may probably be better renamed to -llzk-to-smt.

The current lowering logic is pretty fragile. If we add new ops (like bool.forall coming soon) then we need to change this pass as well to support it. If the implementation for converting from LLZK to SMT is defined by the ops or the dialect, then we only need to change the dialect or the op, a change probably closer to where the other changes that break the pass are happening.

The code as it stands right now is a good prototype for getting the demo working for yesterday but that's about it.

0xddom · 2026-06-23T09:45:10Z

@@ -201,7 +224,7 @@ class FunctionTypeConverter {
 public:
  virtual ~FunctionTypeConverter() = default;

-  void convert(function::FuncDefOp op, mlir::RewriterBase &rewriter) {
+  template <typename FunctionLikeOp> void convert(FunctionLikeOp op, mlir::RewriterBase &rewriter) {


Change the docstring of the class now that it works on any function-like thing

0xddom · 2026-06-23T09:50:24Z

+template <typename MatchType, typename NextMatchType, typename... MatchTypes, typename R>
+inline static bool walkContains(R &root) {
+  return root
+      .walk([](mlir::Operation *op) {
+    return llvm::isa<MatchType, NextMatchType, MatchTypes...>(op) ? mlir::WalkResult::interrupt()


Why do you need typename MatchType, typename NextMatchType? That forces callers to check for at least 2 possibilities.

0xddom · 2026-06-23T09:57:50Z

+  static constexpr bool supportsResultAttrs() {
+    return requires(FunctionLikeOp op, ArrayAttr attrs) {
+      op.getResAttrsAttr();
+      op.setResAttrsAttr(attrs);
+    };


This pattern is used in LLZKConversionUtils.h as well so we could move the function there to share it.

0xddom · 2026-06-23T10:03:29Z

  void rewrite(CallOp op, OpAdaptor adaptor, ConversionPatternRewriter &rewriter) const override {
    // Create new CallOp with split results first so, then process its inputs to split types
    CallOp newCall = newCallOpWithSplitResults(op, adaptor, rewriter);
+    rewriter.setInsertionPoint(newCall);


This is such that whatever is created next in processInputOperands is inserted before newCall, right? Don't we need to recover the previous insertion point after that? Otherwise it will continue inserting before the call unless the conversion engine saves the insertion point internally before calling a pattern's rewrite function.

0xddom · 2026-06-23T10:17:51Z

+    if (auto structDef = dyn_cast<StructDefOp>(op)) {
+      llvm::SmallVector<Type> memberTypes;
+      for (MemberDefOp member : structDef.getMemberDefs()) {
+        memberTypes.push_back(member.getType());
+      }
+      if (failed(collectAggregateProfileForTypes(memberTypes, structDef, tables, profile))) {
+        return WalkResult::interrupt();
+      }
+    } else if (auto funcDef = dyn_cast<FuncDefOp>(op)) {
+      llvm::SmallVector<Type> types;
+      llvm::append_range(types, funcDef.getArgumentTypes());
+      llvm::append_range(types, funcDef.getResultTypes());
+      if (failed(collectAggregateProfileForTypes(types, funcDef, tables, profile))) {
+        return WalkResult::interrupt();
+      }
+    } else if (auto contract = dyn_cast<ContractOp>(op)) {
+      llvm::SmallVector<Type> types;
+      llvm::append_range(types, contract.getArgumentTypes());
+      llvm::append_range(types, contract.getResultTypes());
+      if (failed(collectAggregateProfileForTypes(types, contract, tables, profile))) {
+        return WalkResult::interrupt();
+      }
+    } else if (auto createArray = dyn_cast<CreateArrayOp>(op)) {
+      if (failed(collectAggregateProfileForTypes(
+              ArrayRef<Type> {createArray.getType()}, createArray, tables, profile
+          ))) {
+        return WalkResult::interrupt();
+      }
+    } else if (auto newPod = dyn_cast<NewPodOp>(op)) {
+      if (failed(collectAggregateProfileForTypes(
+              ArrayRef<Type> {newPod.getType()}, newPod, tables, profile
+          ))) {
+        return WalkResult::interrupt();
+      }
+    }
+    return WalkResult::advance();


You can use llvm::TypeSwitch here instead of chaining if-then-elses

0xddom · 2026-06-23T11:19:50Z

+  /// Convert a felt constant attribute into the equivalent SMT integer literal.
+  IntegerAttr toIntAttr(FeltConstantOp op) {
+    return IntegerAttr::get(
+        builder.getContext(), toAPSInt(toDynamicAPInt(op.getValue().getValue()))
+    );
+  }


The docstring and the function argument are at odds with each other. Is the function meant to take an op or an attribute?

0xddom · 2026-06-23T11:25:33Z

+  /// Lower signed division or remainder over field elements via signed representatives.
+  Value emitSignedDivOrRem(Location loc, Value lhs, Value rhs, FeltType type, bool isDiv) {
+    Value signedLhs = emitSignedRepresentative(loc, lhs, type);
+    Value signedRhs = emitSignedRepresentative(loc, rhs, type);
+    Value quotient = emitTruncatingSignedDivision(loc, signedLhs, signedRhs);
+    if (isDiv) {
+      return emitCanonical(loc, quotient, type);
+    }
+    Value product =
+        builder.create<smt::IntMulOp>(loc, ValueRange {signedRhs, quotient}).getResult();
+    Value remainder = builder.create<smt::IntSubOp>(loc, signedLhs, product).getResult();
+    return emitCanonical(loc, remainder, type);
+  }
+
+  /// Lower signed integer division over field elements.
+  Value emitSignedIntDivValue(Location loc, Value lhs, Value rhs, FeltType type) {
+    return emitSignedDivOrRem(loc, lhs, rhs, type, /*isDiv=*/true);
+  }
+
+  /// Lower signed remainder over field elements.
+  Value emitSignedModValue(Location loc, Value lhs, Value rhs, FeltType type) {
+    return emitSignedDivOrRem(loc, lhs, rhs, type, /*isDiv=*/false);
+  }


emitSignedDivOrRem doesn't seem to be used anywhere else so this looks over-complicated for no reason

0xddom · 2026-06-23T11:30:48Z

+    if (op == constrainFunc.getOperation() || isa<ReturnOp, scf::YieldOp>(op) ||
+        isa<constrain::EmitEqualityOp>(op) || isa<CallOp>(op)) {


Suggested change

if (op == constrainFunc.getOperation() || isa<ReturnOp, scf::YieldOp>(op) ||

isa<constrain::EmitEqualityOp>(op) || isa<CallOp>(op)) {

if (op == constrainFunc.getOperation() || isa<ReturnOp, scf::YieldOp, constrain::EmitEqualityOp, CallOp>(op)) {

0xddom · 2026-06-23T11:42:27Z

The organization in this file is confusing me

0xddom · 2026-06-23T11:46:01Z

Are we planning to support lowering the loop invariant ops in this PR?

iangneal · 2026-06-23T15:09:31Z

The verif to smt pass needs some work. A cleaner approach is to let the different dialects define how to lower to smt, similar to how lowering to LLVM works in upstream MLIR. The pass' name hints that is going to lower only operations from the verif dialect, but it lowers everything that is meant to be lowered to smt. The pass may probably be better renamed to -llzk-to-smt.

Problem is we already have a lowering pass called that, but it's specifically for @Product aligned programs. We can rename that pass, perhaps, but that would require an LLEQ change. @raghav198

Otherwise I agree.

The code as it stands right now is a good prototype for getting the demo working for yesterday but that's about it.

Correct. I think there are some PRs that actually need to be split off from this one and merged separately or removed. For example, there's a scalarization workaround that I believe needs to be reverted once #565 is merged.

I'm just going to mark this as a draft until I'm done restructuring this, but I haven't had a chance to yet.

iangneal added 15 commits June 11, 2026 20:16

Initial verif to smt transform

b070386

Refine translation some

a7922ed

POD and array handling

c92faed

Simplify implementation

452d4a3

Add solver checks

99c481f

Restructure output format

2c6abe8

Update docs

15c8ff9

Merge remote-tracking branch 'origin/main' into iangneal/init-verif-t…

92a2e1f

…o-smt

Update pass machinery

dc845c5

Update docs

ce3240d

Revert formatting change

7fdaead

Update docs in SMT lowering

72269aa

Refactor

ff0d3e3

Refactor

e13b2bb

Add walk utility

aa8b98d

iangneal requested a review from a team as a code owner June 17, 2026 00:28

iangneal and others added 4 commits June 16, 2026 20:38

Update format

a489f1a

Merge branch 'main' into iangneal/init-verif-to-smt

b977c1d

Fix variable shadowing

4b1609c

Fix typo

321d782

tim-hoffman reviewed Jun 17, 2026

View reviewed changes

iangneal and others added 3 commits June 17, 2026 12:37

Remove structs after translation, don't ignore empty functions

61ec110

Add support for remaining felt ops

4313aae

Merge branch 'main' into iangneal/init-verif-to-smt

1febe21

chatgpt-codex-connector Bot reviewed Jun 18, 2026

View reviewed changes

tim-hoffman reviewed Jun 18, 2026

View reviewed changes

iangneal added 2 commits June 18, 2026 23:02

Minor cleanups

92aa419

Address code review comments

8ec3e97

iangneal and others added 2 commits June 18, 2026 23:32

Merge branch 'main' into iangneal/init-verif-to-smt

2d71f0f

Fix merge and format

375f7a6

chatgpt-codex-connector Bot reviewed Jun 19, 2026

View reviewed changes

Comment thread lib/Transforms/LLZKVerifToSmtPass.cpp Outdated

Comment thread lib/Transforms/LLZKVerifToSmtPass.cpp Outdated

Address code review

ab98bea

chatgpt-codex-connector Bot reviewed Jun 19, 2026

View reviewed changes

Comment thread lib/Transforms/LLZKVerifToSmtPass.cpp Outdated

Comment thread lib/Transforms/LLZKVerifToSmtPass.cpp Outdated

iangneal added 2 commits June 19, 2026 00:47

Address code review comments

8cd9cd8

Fix formatting

3847858

chatgpt-codex-connector Bot reviewed Jun 19, 2026

View reviewed changes

Comment thread lib/Transforms/LLZKVerifToSmtPass.cpp Outdated

iangneal added 6 commits June 19, 2026 01:02

Address code review, fix test

4348367

Fix format

673c1fe

Fix the format yet again

8531bfc

Why do I have to keep fixing the format

fd194dc

Tweak test

4158948

Reuse prime

06f2bf6

0xddom requested changes Jun 23, 2026

View reviewed changes

iangneal marked this pull request as draft June 23, 2026 15:09

		if (op == constrainFunc.getOperation() \|\| isa<ReturnOp, scf::YieldOp>(op) \|\|
		isa<constrain::EmitEqualityOp>(op) \|\| isa<CallOp>(op)) {

Uh oh!

Conversation

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

Uh oh!

Uh oh!

github-actions Bot commented Jun 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Test Results

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!

tim-hoffman commented Jun 18, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tim-hoffman left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

iangneal commented Jun 19, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

iangneal commented Jun 19, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

iangneal commented Jun 19, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

0xddom left a comment

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

iangneal commented Jun 17, 2026 •

edited

Loading

github-actions Bot commented Jun 17, 2026 •

edited

Loading