Basic array lowering by raghav198 · Pull Request #729 · project-llzk/llzk-lib

raghav198 · 2026-09-14T20:02:29Z

No description provided.

github-actions · 2026-09-14T20:15:21Z

Test Results

2 files ±0 2 suites ±0 1m 29s ⏱️ -12s
484 tests ±0 480 ✅ ±0 4 💤 ±0 0 ❌ ±0
968 runs ±0 960 ✅ ±0 8 💤 ±0 0 ❌ ±0

Results for commit 838ea69. ± Comparison against base commit 49d478f.

♻️ This comment has been updated with latest results.

raghav198 · 2026-09-14T20:18:15Z

@codex review

chatgpt-codex-connector · 2026-09-14T20:18:28Z

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-07T16:32:24.015967Z	`1c5a8f2`	Manual request

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: a985467fae

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

chatgpt-codex-connector · 2026-09-14T20:24:24Z

+  addConversion([this, ctx](array::ArrayType arrType) {
+    return smt::ArrayType::get(ctx, smt::IntType::get(ctx), convertType(arrType.getElementType()));
+  });


Preserve one SMT array layer per LLZK dimension

For any LLZK array with rank greater than one, this creates only a single SMT array whose range is the scalar element type. smtReadArray nevertheless emits one smt.array.select per index, so a read from !array.type<2,2 x !felt.type> attempts the second select on the !smt.int returned by the first one and produces invalid IR. Construct a nested SMT array type for every LLZK dimension, or flatten the indices consistently.

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-09-14T20:24:24Z

+  patterns.add<WriteArrayConverter>(converter, context, [](Value) -> ArrayWriteMode {
+    return ArrayWriteMode::WriteOnce;


Reject arrays that do not satisfy the write-once policy

This policy classifies every array as write-once without performing any analysis. For a valid mutable-array program that writes different values to the same index twice, the lowering emits assertions equating the original SMT array element to both values instead of letting the second write replace the first, silently changing satisfiability. Detect and reject overwrites or implement the Overwrite encoding rather than unconditionally selecting WriteOnce.

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-09-14T20:24:24Z

+  addConversion([this, ctx](array::ArrayType arrType) {
+    return smt::ArrayType::get(ctx, smt::IntType::get(ctx), convertType(arrType.getElementType()));
+  });


Avoid converting arrays without patterns in the naive pass

The type converter is shared with SMTNaiveLoweringPass, but that pass does not register ReadArrayConverter, WriteArrayConverter, or IndexConstConverter. Consequently, a naive-lowering input with an array of felts now has its function argument changed to !smt.array while its array.read/array.write operations and index producers remain in their original forms; with materializations disabled, the pass fails or leaves verifier-invalid operands. Either add equivalent array patterns to the naive strategy or scope this conversion to the optimized pass.

Useful? React with 👍 / 👎.

raghav198 · 2026-09-23T18:50:23Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b5ffc08274

ℹ️ 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 · 2026-09-24T18:43:48Z

-// CHECK-NEXT:      %[[VAL_44:[0-9a-zA-Z_\.]+]] = arith.constant 0 : index
-// CHECK-NEXT:      %[[VAL_45:[0-9a-zA-Z_\.]+]] = arith.constant 1 : index
-// CHECK-NEXT:      %[[VAL_46:[0-9a-zA-Z_\.]+]] = arith.constant 8 : index
+// CHECK-NEXT:      %[[I0:[0-9a-zA-Z_\.]+]] = smt.int.constant 0
+// CHECK-NEXT:      %[[VAL_44:[0-9a-zA-Z_\.]+]] = builtin.unrealized_conversion_cast %[[I0]] : !smt.int to index
+// CHECK-NEXT:      %[[I1:[0-9a-zA-Z_\.]+]] = smt.int.constant 1
+// CHECK-NEXT:      %[[VAL_45:[0-9a-zA-Z_\.]+]] = builtin.unrealized_conversion_cast %[[I1]] : !smt.int to index
+// CHECK-NEXT:      %[[I8:[0-9a-zA-Z_\.]+]] = smt.int.constant 8
+// CHECK-NEXT:      %[[VAL_46:[0-9a-zA-Z_\.]+]] = builtin.unrealized_conversion_cast %[[I8]] : !smt.int to index
 // CHECK-NEXT:      scf.for %[[VAL_47:[0-9a-zA-Z_\.]+]] = %[[VAL_44]] to %[[VAL_46]] step %[[VAL_45]] {
-// CHECK-NEXT:        %[[VAL_48:[0-9a-zA-Z_\.]+]] = array.read %[[VAL_1]]{{\[}}%[[VAL_47]]] : <8 x !felt.type>, !felt.type
-// CHECK-NEXT:        %[[VAL_49:[0-9a-zA-Z_\.]+]] = builtin.unrealized_conversion_cast %[[VAL_48]] : !felt.type to !smt.int
-// CHECK-NEXT:        %[[VAL_50:[0-9a-zA-Z_\.]+]] = array.read %[[VAL_3]]{{\[}}%[[VAL_47]]] : <8 x !felt.type>, !felt.type
-// CHECK-NEXT:        %[[VAL_51:[0-9a-zA-Z_\.]+]] = builtin.unrealized_conversion_cast %[[VAL_50]] : !felt.type to !smt.int
-// CHECK-NEXT:        %[[VAL_52:[0-9a-zA-Z_\.]+]] = smt.eq %[[VAL_49]], %[[VAL_51]] : !smt.int
+// CHECK-NEXT:        %[[IDX:[0-9a-zA-Z_\.]+]] = builtin.unrealized_conversion_cast %[[VAL_47]] : index to !smt.int
+// CHECK-NEXT:        %[[VAL_48:[0-9a-zA-Z_\.]+]] = smt.array.select %[[VAL_0]]{{\[}}%[[IDX]]] : !smt.array<[!smt.int -> !smt.int]>
+// CHECK-NEXT:        %[[VAL_50:[0-9a-zA-Z_\.]+]] = smt.array.select %[[VAL_1]]{{\[}}%[[IDX]]] : !smt.array<[!smt.int -> !smt.int]>
+// CHECK-NEXT:        %[[VAL_52:[0-9a-zA-Z_\.]+]] = smt.eq %[[VAL_48]], %[[VAL_50]] : !smt.int


Does more need to be done about these unrealized_conversion_cast to/from index?

I'm not sure, but I don't think so? LLEQ (and I'm pretty sure the SMTLIB emitter) know how to see through those, and I think they're only there because scf.for needs the ivar to be an index.

tim-hoffman · 2026-09-24T18:45:06Z

+}
+
+WriteArrayConverter::WriteArrayConverter(
+    mlir::TypeConverter &converter, mlir::MLIRContext *context, ArrayWritePolicy writePolicy,


remove mlir:: prefix

raghav198 added this pull request to stack #731 September 14, 2026 20:17

chatgpt-codex-connector Bot reviewed Sep 14, 2026

View reviewed changes

raghav198 marked this pull request as ready for review September 14, 2026 20:38

raghav198 requested a review from a team as a code owner September 14, 2026 20:38

raghav198 marked this pull request as draft September 14, 2026 20:38

raghav198 removed this pull request from stack #731 September 14, 2026 20:39

raghav198 changed the base branch from main to raghav/smt-member-read-write-array September 14, 2026 20:39

raghav198 added this pull request to stack #733 September 14, 2026 20:39

raghav198 force-pushed the raghav/smt-array-policy branch from c8bc13c to a09159b Compare September 14, 2026 22:17

raghav198 force-pushed the raghav/smt-array-policy branch from 10e7c42 to 3ca4d8c Compare September 17, 2026 16:31

raghav198 force-pushed the raghav/smt-array-policy branch from 3ca4d8c to cd26713 Compare September 21, 2026 17:40

raghav198 force-pushed the raghav/smt-array-policy branch from fb08efb to 341bad9 Compare September 23, 2026 16:44

raghav198 force-pushed the raghav/smt-array-policy branch 2 times, most recently from 4c933e5 to b5ffc08 Compare September 23, 2026 18:50

chatgpt-codex-connector Bot reviewed Sep 23, 2026

View reviewed changes

Comment thread backends/smt/lib/Conversions/SMTLoweringPass.cpp Outdated

Comment thread backends/smt/lib/Conversions/SMTLoweringCommon.cpp

raghav198 force-pushed the raghav/smt-array-policy branch from b5ffc08 to 38b5977 Compare September 24, 2026 15:50

raghav198 marked this pull request as ready for review September 24, 2026 18:23

tim-hoffman reviewed Sep 24, 2026

View reviewed changes

Raghav Malik added 27 commits October 9, 2026 16:28

Maybe correctly emit quantified array range assertions

6788f4b

Updated to handle struct.writem correctly

f68dd53

Redundant

230c2c5

Shadow

ab259e8

Fixed Codex comments

85b42c7

Add ndarray test

7e19db3

Changelog

351f5df

Get rid of unnecessary namespacing

f8b6016

Formatting clean up

2f8199b

Move fields

212128e

Other miscellanea

4de8291

Fixed from LLVM upgrade

d14d96b

Fixed array type conversion

49d478f

Basic array lowering

4f4e37e

Update array-overwrite error message to be more consistent

833c058

Update function name

832bd34

Infer array write policy

42583db

Update to use emitter

6a43e23

Review comments + updating the tests

227ed3d

comments

7f83d77

Updated for LLVM 23 upgrade

4e98585

Addressed comments

c3eae9b

Updated test

57cb166

Changelog?

2f1fa9b

Fixed signed vs unsigned max int

542aa97

Properly constrain array args

d1de8f5

format

838ea69

raghav198 force-pushed the raghav/smt-array-policy branch from 437f29d to 838ea69 Compare October 9, 2026 20:28

Base automatically changed from raghav/smt-member-read-write-array to main October 21, 2026 17:30

		patterns.add<WriteArrayConverter>(converter, context, [](Value) -> ArrayWriteMode {
		return ArrayWriteMode::WriteOnce;

Conversation

raghav198 commented Sep 14, 2026

Uh oh!

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

Uh oh!

Test Results

Uh oh!

raghav198 commented Sep 14, 2026

Uh oh!

chatgpt-codex-connector Bot commented Sep 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codex Review Summary

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

raghav198 commented Sep 23, 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!

tim-hoffman Sep 24, 2026

Choose a reason for hiding this comment

Uh oh!

raghav198 Sep 24, 2026

Choose a reason for hiding this comment

Uh oh!

tim-hoffman Sep 24, 2026

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Sep 14, 2026 •

edited

Loading

chatgpt-codex-connector Bot commented Sep 14, 2026 •

edited

Loading