NOIR fixes - #60
NOIR fixes#60
Conversation
|
@codex review |
![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: e7485d2078
ℹ️ 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".
| .Default([this, &postcondition](auto op) { | ||
| auto expression = builder.getExpression(op->getResult(0)); | ||
| postcondition.substitute(builder.getConstant(op->getResult(0)), | ||
| expression); | ||
| // The default case is just an expression op, but we shouldn't have to | ||
| // do anything here because any places that use the result have already | ||
| // called `builder.getExpression()` on the result so there shouldn't be | ||
| // anything to substitute. |
There was a problem hiding this comment.
When an scf.if condition is produced by an expression such as bool.cmp, calculateWP(scf::IfOp) still inserts builder.getConstant(ifOp.getCondition()) into the branch antecedents. Making the default case a no-op leaves that fresh Boolean unrelated to the comparison; moreover, when the verification query gathers declarations, getDeclBounds attempts to apply _is_mod to this Boolean and aborts with cannot bound non-integral sort modulo. The existing tests/smtlib/disable-store-iszero.llzk flow has exactly this computed-condition shape, so expression-result substitution must be retained or the scf.if handler must use getExpression directly.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
@codex After the new commit, is this still an issue?
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 36c602bd5c
ℹ️ 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".
| .Default([this, &postcondition](auto op) { | ||
| auto expression = builder.getExpression(op->getResult(0)); | ||
| postcondition.substitute(builder.getConstant(op->getResult(0)), | ||
| expression); | ||
| // The default case is just an expression op, but we shouldn't have to | ||
| // do anything here because any places that use the result have already | ||
| // called `builder.getExpression()` on the result so there shouldn't be | ||
| // anything to substitute. |
There was a problem hiding this comment.
When a subcomponent call receives a computed argument, such as a felt.add result, this no-op leaves that result represented by an unrelated fresh constant: TermBuilder::initSubcmp still constructs every uninterpreted-function argument with getConstant(arg) in TermUtils.cpp, rather than getExpression(arg). Consequently, witness and constraint calls computed from equivalent expressions can use unconstrained, independent arguments and yield an incorrect equivalence result; retain the substitution here or expand arguments inside initSubcmp.
Useful? React with 👍 / 👎.
| if (auto constOp = val.getDefiningOp<felt::FeltConstantOp>()) { | ||
| return constOp.getValue().getValue().isOne(); | ||
| } | ||
| return false; |
There was a problem hiding this comment.
Should this one also peer through IntToFeltOp like isBool() does?
2 participants
No description provided.