Repository navigation
Conversation
2c1f736 to
736bd74
Compare
83df4f3 to
1e47961
Compare
|
@codex review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 33303d172b
ℹ️ 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".
| loc, *extents, | ||
| [this, &loc, &lhs, &builder, &lhsRange, &rhsRange, &prefix](ValueRange indices) -> Value { | ||
| auto lhsElement = emitter->emitArraySelect(loc, lhs, indices, builder); | ||
| auto rhsElement = emitter->emitArraySelect(loc, lhs, indices, builder); |
There was a problem hiding this comment.
For every statically shaped array write or array-valued constrain.eq, the quantified predicate selects both elements from lhs; rhs is never referenced. In the common canonical-range case this emits lhs[i] == lhs[i], so a struct.writem no longer connects the witness array to the value being written and the solver can accept incorrect witnesses. The second selection must use rhs.
Useful? React with 👍 / 👎.
| addConversion([this, ctx](array::ArrayType arrType) { | ||
| return smt::ArrayType::get(ctx, smt::IntType::get(ctx), convertType(arrType.getElementType())); |
There was a problem hiding this comment.
For an array with rank greater than one, such as !array.type<2,3 x !felt.type>, this conversion creates only one !smt.array layer, while emitArraySelect later performs one select per source dimension. The first select therefore returns !smt.int, and the second attempts to use that integer as an SMT array, causing verification/lowering failure for valid multidimensional array members. Build nested SMT array types for all dimensions or consistently flatten the indices.
Useful? React with 👍 / 👎.
| for (auto memberDef : structDef.getMemberDefs()) { | ||
| if (!isa<felt::FeltType>(memberDef.getType())) { | ||
| continue; | ||
| } | ||
| // if (!isa<felt::FeltType>(memberDef.getType())) { | ||
| // continue; | ||
| // } |
There was a problem hiding this comment.
When a struct contains an unused non-felt member, such as another struct or an array of non-felt elements, the pass now processes it even though only felt and array-of-felt reads/writes are supported. convertType leaves unsupported types unchanged, after which they are used as the result type of smt.declare_fun, whose result must be an SMT type; consequently modules that previously lowered by ignoring such unused members now produce invalid SMT IR. Retain a filter that admits only felt and supported array-of-felt members.
Useful? React with 👍 / 👎.
7ca26bf to
8d17b09
Compare
94910f1 to
9723ba6
Compare
tim-hoffman
left a comment
tim-hoffman
left a comment
There was a problem hiding this comment.
LGTM; leaving final approval to @shankarapailoor
75325b2 to
4ba30c5
Compare
4ba30c5 to
d21bb5c
Compare
This branch has not been deployed
2 participants
Add support for SMT lowering for
struct.readmandstruct.writemwhen the type of the member being read from/written to is an array of felt:writem, emit a quantified assertion over the array boundsreadm, maybe quantify constrain uses?