Skip to content

NOIR fixes #60

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
raghav198 merged 4 commits into from
Aug 31, 2026
+54 −13
Merged

NOIR fixes #60

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e7485d2
NOIR fixes
Aug 24, 2026
36c602b
If condition expr
Aug 26, 2026
48e4fe2
Subcmp arg expr
Aug 26, 2026
ab75364
CR comment
Aug 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions lib/Verification/TermUtils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -201,8 +201,7 @@ cvc5::Sort TermBuilder::_sort_of_type(Type type) {
ensure(it != subcmpSorts.end(), "unknown subcomponent type");
return it->second;
}
if (type.isSignlessInteger() &&
dyn_cast<IntegerType>(type).getIntOrFloatBitWidth() == 1) {
if (type.isSignlessInteger(1)) {
return mgr.getBooleanSort();
}
if (auto arrType = dyn_cast<array::ArrayType>(type)) {
Expand Down Expand Up @@ -520,7 +519,7 @@ cvc5::Term TermBuilder::initSubcmp(component::StructDefOp subcmp,
termArgs.reserve(args.size() + 1);

for (auto arg : args) {
termArgs.push_back(getConstant(arg));
termArgs.push_back(getExpression(arg));
}
return mgr.mkTerm(cvc5::Kind::APPLY_UF, termArgs);
}
Expand Down
62 changes: 52 additions & 10 deletions lib/Verification/WeakestPrecondition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@

#include <llzk/Dialect/Bool/IR/Ops.h>
#include <mlir/IR/BuiltinTypeInterfaces.h>
#define DEBUG_TYPE "weakest-precondition"

#include "Verification/SolverUtils.h"
#include "Verification/Utils.h"
Expand All @@ -23,6 +22,7 @@
#include <llvm/Support/LogicalResult.h>
#include <llvm/Support/raw_ostream.h>
#include <llzk/Dialect/Array/IR/Ops.h>
#include <llzk/Dialect/Cast/IR/Ops.h>
#include <llzk/Dialect/Constrain/IR/Ops.h>
#include <llzk/Dialect/Felt/IR/Ops.h>
#include <llzk/Dialect/Function/IR/Ops.h>
Expand All @@ -40,6 +40,8 @@
#include <optional>
#include <vector>

#define DEBUG_TYPE "weakest-precondition"

using namespace llzk;
using namespace mlir;

Expand Down Expand Up @@ -427,6 +429,36 @@ static inline bool valueIsMemberWrite(Value val,
return false;
}

static inline bool isBool(Value val) {
if (val.getType().isSignlessInteger(1)) {
return true;
}
if (auto castOp = val.getDefiningOp<llzk::cast::IntToFeltOp>()) {
return isBool(castOp.getOperand());
}
return false;
}

static inline bool isConstantOne(Value val) {
if (auto constOp = val.getDefiningOp<felt::FeltConstantOp>()) {
return constOp.getValue().getValue().isOne();
}
if (auto castOp = val.getDefiningOp<cast::IntToFeltOp>()) {
return isConstantOne(castOp.getOperand());
}
return false;
Comment on lines +443 to +449

@tim-hoffman tim-hoffman Aug 27, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this one also peer through IntToFeltOp like isBool() does?

}

static inline FailureOr<Value> getAssertedBool(Value a, Value b) {
if (isBool(a) && isConstantOne(b)) {
return a;
}
if (isBool(b) && isConstantOne(a)) {
return b;
}
return failure();
}

// TODO: Use TermBuilder to populate expressions instead of substitution
void WeakestPreconditionAnalysis::calculateWP(Operation *op,
ConjunctionTerm &postcondition) {
Expand All @@ -453,11 +485,20 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
postcondition.substitute(builder.getConstant(arr),
builder.arrayWrite(arr, indices, value));
})
.Case<constrain::EmitEqualityOp>(
[this, &postcondition](EmitEqualityOp eqOp) {
postcondition.addAntecedent(
builder.assertEqual(eqOp.getLhs(), eqOp.getRhs()));
})
.Case<constrain::EmitEqualityOp>([this,
&postcondition](EmitEqualityOp eqOp) {
// XXX: If one side of the equality is a Bool
// and the other side is a constant `1`, then instead of asserting
// equality just directly assert the Bool. This is a hack until the
// SMT encoding can deal with this correctly.
if (auto assertedBool = getAssertedBool(eqOp.getLhs(), eqOp.getRhs());
succeeded(assertedBool)) {
postcondition.addAntecedent(builder.getExpression(*assertedBool));
} else {
postcondition.addAntecedent(
builder.assertEqual(eqOp.getLhs(), eqOp.getRhs()));
}
})
.Case<scf::IfOp>([this, &postcondition](scf::IfOp op) {
calculateWP(op, postcondition);
})
Expand Down Expand Up @@ -500,9 +541,10 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
}
})
.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.
Comment on lines 543 to +547

@chatgpt-codex-connector chatgpt-codex-connector Bot Aug 25, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Restore substitution for computed branch conditions

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 👍 / 👎.

@raghav198 raghav198 Aug 26, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@codex After the new commit, is this still an issue?

Comment on lines 543 to +547

@chatgpt-codex-connector chatgpt-codex-connector Bot Aug 26, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Preserve substitution for computed subcomponent arguments

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 👍 / 👎.

});
}

Expand All @@ -518,7 +560,7 @@ void WeakestPreconditionAnalysis::calculateWP(Block *block,

void WeakestPreconditionAnalysis::calculateWP(mlir::scf::IfOp ifOp,
ConjunctionTerm &postcondition) {
auto condition = builder.getConstant(ifOp.getCondition());
auto condition = builder.getExpression(ifOp.getCondition());
auto notCondition = mgr.mkTerm(cvc5::Kind::NOT, {condition});

ConjunctionTerm thenBranch{postcondition}, elseBranch{postcondition};
Expand Down
Loading