Skip to content

Raghav/unsupported warn #61

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 11 commits into from
Sep 1, 2026
Merged

Raghav/unsupported warn #61

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
11 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
304656c
Propagate unsupported errors instead of crashing
Aug 26, 2026
e9b3d29
Script reports unsupported separately from errors
Aug 26, 2026
da7fb6a
logAllUnhandledErrors
Aug 26, 2026
ab75364
CR comment
Aug 31, 2026
6c6305f
Merge branch 'raghav/noir-fixes' into raghav/unsupported-warn
Aug 31, 2026
ac5308c
Use exceptions instead
Aug 31, 2026
307a32c
Remove dead function from header
Aug 31, 2026
aee0470
Merge branch 'main' into raghav/unsupported-warn
raghav198 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
11 changes: 6 additions & 5 deletions include/Verification/WeakestPrecondition.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#include "Verification/TermUtils.h"
#include <cvc5/cvc5.h>

#include <llvm/Support/Error.h>
#include <llvm/Support/LogicalResult.h>
#include <llvm/Support/raw_ostream.h>
#include <llzk/Dialect/Array/IR/Ops.h>
Expand Down Expand Up @@ -42,9 +43,9 @@ class WeakestPreconditionAnalysis {
TermBuilder builder;
mlir::SymbolTableCollection tables;

void calculateWP(mlir::scf::IfOp ifOp, ConjunctionTerm &postcondition);
void calculateWP(mlir::Operation *op, ConjunctionTerm &postcondition);
void calculateWP(mlir::Block *block, ConjunctionTerm &postcondition);
llvm::Error calculateWP(mlir::scf::IfOp ifOp, ConjunctionTerm &postcondition);
llvm::Error calculateWP(mlir::Operation *op, ConjunctionTerm &postcondition);
llvm::Error calculateWP(mlir::Block *block, ConjunctionTerm &postcondition);

mlir::DenseMap<mlir::Value, cvc5::Term> valueExpressions;

Expand All @@ -58,7 +59,7 @@ class WeakestPreconditionAnalysis {
});
}

llvm::FailureOr<cvc5::Term>
llvm::Expected<cvc5::Term>
computeInvariant(mlir::scf::ForOp loop, const ConjunctionTerm &postcondition);

public:
Expand All @@ -70,7 +71,7 @@ class WeakestPreconditionAnalysis {

ImplicationTerm getPostcondition();
void populateVerificationConditions();
cvc5::Term generateVerificationConditions();
llvm::Expected<cvc5::Term> generateVerificationConditions();

@chatgpt-codex-connector chatgpt-codex-connector Bot Aug 31, 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.

P2 Badge Remove or restore the undefined population API

When downstream code uses the installed WeakestPreconditionAnalysis header and calls populateVerificationConditions(), compilation succeeds but linking now fails because this commit deletes the method's only definition while leaving its public declaration (and associated result fields) intact. Either retain an error-aware implementation or remove the obsolete declaration and state from the public API.

Useful? React with 👍 / 👎.


void applyStructContract(llzk::verif::ContractOp contract);
void addEquivalentMember(llzk::component::MemberDefOp memberDef);
Expand Down
155 changes: 91 additions & 64 deletions lib/Verification/WeakestPrecondition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
#include <llvm/ADT/SmallVectorExtras.h>
#include <llvm/ADT/StringMap.h>
#include <llvm/ADT/TypeSwitch.h>
#include <llvm/Support/Error.h>

#include <llvm/Support/Casting.h>
#include <llvm/Support/Debug.h>
Expand Down Expand Up @@ -223,7 +224,7 @@ FailingCore getFailingCore(cvc5::Term invariant,

} // namespace

FailureOr<cvc5::Term> WeakestPreconditionAnalysis::computeInvariant(
llvm::Expected<cvc5::Term> WeakestPreconditionAnalysis::computeInvariant(
scf::ForOp loop, const ConjunctionTerm &postcondition) {
SmallVector<LoopCounterInfo> loopInfo;
auto *body = nestedLoopBody(loop, loopInfo, builder);
Expand Down Expand Up @@ -334,7 +335,9 @@ FailureOr<cvc5::Term> WeakestPreconditionAnalysis::computeInvariant(

// Verify {strengthenedPrecondition} loopBody {postcondition} to show the
// predicate is inductive
calculateWP(body, postcondition);
if (llvm::Error err = calculateWP(body, postcondition)) {
return err;
}
auto isInductive =
mgr.mkTerm(cvc5::Kind::IMPLIES,
{strengthenedPrecondition, postcondition.buildTerm(mgr)});
Expand Down Expand Up @@ -427,17 +430,18 @@ static inline bool valueIsMemberWrite(Value val,
return false;
}

// TODO: Use TermBuilder to populate expressions instead of substitution
void WeakestPreconditionAnalysis::calculateWP(Operation *op,
ConjunctionTerm &postcondition) {
llvm::TypeSwitch<mlir::Operation *, void>(op)
llvm::Error
WeakestPreconditionAnalysis::calculateWP(Operation *op,
ConjunctionTerm &postcondition) {
return llvm::TypeSwitch<mlir::Operation *, llvm::Error>(op)
.Case<component::CreateStructOp>(
[&postcondition](auto) { return postcondition; })
[](auto) { return llvm::Error::success(); })
.Case<MemberWriteOp>([this, &postcondition](MemberWriteOp writeOp) {
postcondition.addAntecedent(builder.assertEqual(
builder.getConstant(writeOp.getMemberDefOp(tables)->get(),
/*isWitness=*/true),
writeOp.getVal()));
return llvm::Error::success();
})
.Case<WriteArrayOp>([this, &postcondition](WriteArrayOp writeOp) {
auto arr = writeOp.getArrRef();
Expand All @@ -448,88 +452,110 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
if (valueIsMemberRead(arr, tables) || valueIsMemberWrite(arr, tables)) {
postcondition.addAntecedent(
builder.assertEqual(builder.arrayRead(arr, indices), value));
return;
return llvm::Error::success();
}
postcondition.substitute(builder.getConstant(arr),
builder.arrayWrite(arr, indices, value));
return llvm::Error::success();
})
.Case<constrain::EmitEqualityOp>(
[this, &postcondition](EmitEqualityOp eqOp) {
postcondition.addAntecedent(
builder.assertEqual(eqOp.getLhs(), eqOp.getRhs()));
return llvm::Error::success();
})
.Case<scf::IfOp>([this, &postcondition](scf::IfOp op) {
calculateWP(op, postcondition);
return calculateWP(op, postcondition);
})
.Case<UnrealizedConversionCastOp>([this](auto) { return; })
.Case<scf::ForOp>([this, &postcondition](scf::ForOp op) {
.Case<UnrealizedConversionCastOp>(
[this](auto) { return llvm::Error::success(); })
.Case<scf::ForOp>([this, &postcondition](scf::ForOp op) -> llvm::Error {
auto invariant = computeInvariant(op, postcondition);
llzk::ensure(succeeded(invariant),
"failed to infer invariant for loop");
if (auto err = invariant.takeError()) {
return err;
}
// It should already be the case that invariant => postcondition
postcondition = ConjunctionTerm::of(*invariant);
return llvm::Error::success();
})
.Case<boolean::AssertOp>([this, &postcondition](boolean::AssertOp op) {
postcondition.addAntecedent(builder.getExpression(op.getCondition()));
return llvm::Error::success();
})
.Case<smt::AssertOp>([this, &postcondition](smt::AssertOp op) {
postcondition.addAntecedent(builder.getExpression(op.getInput()));
return llvm::Error::success();
})
.Case<llzk::function::CallOp>([this, &postcondition](
llzk::function::CallOp call) {
if (call.calleeIsStructConstrain()) {
// @constrain(%subcmp, %args...) => (assert (= %subcmp
// (init-"subcmp" %args...)))
auto target = call.getCalleeTarget(tables);
llzk::ensure(succeeded(target), "failed to resolve callee target");
auto subcmpVal = call.getArgOperands().front();
auto subcmp =
target->get()->getParentOfType<component::StructDefOp>();
SmallVector<Value> args = call.getArgOperands().drop_front();
postcondition.addAntecedent(
builder.assertEqual(subcmpVal, builder.initSubcmp(subcmp, args)));
} else if (call.calleeIsStructCompute()) {
auto expression = builder.getExpression(call.getResult(0));
postcondition.substitute(builder.getConstant(call->getResult(0)),
expression);
} else {
// Technically a call to @product has already aligned the subcomponent
// values so there's nothing to prove
llzk::ensure(call.calleeIsStructProduct(),
"arbitrary function calls not supported");
}
})
.Case<llzk::function::CallOp>(
[this, &postcondition](llzk::function::CallOp call) -> llvm::Error {
if (call.calleeIsStructConstrain()) {
// @constrain(%subcmp, %args...) => (assert (= %subcmp
// (init-"subcmp" %args...)))
auto target = call.getCalleeTarget(tables);
llzk::ensure(succeeded(target),
"failed to resolve callee target");
auto subcmpVal = call.getArgOperands().front();
auto subcmp =
target->get()->getParentOfType<component::StructDefOp>();
SmallVector<Value> args = call.getArgOperands().drop_front();
postcondition.addAntecedent(builder.assertEqual(
subcmpVal, builder.initSubcmp(subcmp, args)));
} else if (call.calleeIsStructCompute()) {
auto expression = builder.getExpression(call.getResult(0));
postcondition.substitute(builder.getConstant(call->getResult(0)),
expression);
} else if (!call.calleeIsStructProduct()) {
// Technically a call to @product has already aligned the
// subcomponent values so there's nothing to prove
return llvm::createStringError(
"Unsupported: arbitrary function calls");

@chatgpt-codex-connector chatgpt-codex-connector Bot Aug 31, 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 Propagate errors before evaluating arbitrary call results

When an unsupported value-returning function call feeds an equality, member write, or another expression, reverse traversal processes that user first and builder.getExpression() enters the function::CallOp handler in TermUtils.cpp, whose ensure still aborts for arbitrary callees. Consequently this new Error branch is never reached for the common case where the call result is used, so those inputs still crash instead of taking the intended graceful unsupported path; unsupported calls need to be detected before expression expansion or represented as a propagated error there as well.

Useful? React with 👍 / 👎.

}
return llvm::Error::success();
})
.Default([this, &postcondition](auto op) {
auto expression = builder.getExpression(op->getResult(0));
postcondition.substitute(builder.getConstant(op->getResult(0)),
expression);
return llvm::Error::success();
});
}

void WeakestPreconditionAnalysis::calculateWP(Block *block,
ConjunctionTerm &postcondition) {
llvm::Error
WeakestPreconditionAnalysis::calculateWP(Block *block,
ConjunctionTerm &postcondition) {
for (auto &op : llvm::iterator_range(block->rbegin(), block->rend())) {
if (&op == block->getTerminator()) {
continue;
}
calculateWP(&op, postcondition);
if (llvm::Error err = calculateWP(&op, postcondition)) {
return err;
}
}
return llvm::Error::success();
}

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

ConjunctionTerm thenBranch{postcondition}, elseBranch{postcondition};
calculateWP(&ifOp.getThenRegion().front(), thenBranch);
calculateWP(&ifOp.getElseRegion().front(), elseBranch);
if (llvm::Error err =
calculateWP(&ifOp.getThenRegion().front(), thenBranch)) {
return err;
}
if (llvm::Error err =
calculateWP(&ifOp.getElseRegion().front(), elseBranch)) {
return err;
}

thenBranch.addAntecedent(condition);
elseBranch.addAntecedent(notCondition);

thenBranch.addConjuncts(elseBranch);
postcondition = thenBranch;
return llvm::Error::success();
}

SmallVector<cvc5::Term> getArrayExtents(array::ArrayType type,
Expand All @@ -552,9 +578,8 @@ SmallVector<cvc5::Term> getArrayExtents(array::ArrayType type,

ImplicationTerm WeakestPreconditionAnalysis::getPostcondition() {

// The caller already checks for zero members, so no need to do it again
auto members = structDef.getMemberDefs();
llzk::ensure(!members.empty(),
"cannot build postcondition for struct with empty members");

SmallVector<cvc5::Term> memberEquivs;
SmallVector<std::optional<Annotation>> annotations;
Expand All @@ -578,31 +603,33 @@ ImplicationTerm WeakestPreconditionAnalysis::getPostcondition() {
return ImplicationTerm{{}, memberEquivs, annotations};
}

void WeakestPreconditionAnalysis::populateVerificationConditions() {
util::ensureProductFunc(structDef->getParentOfType<ModuleOp>(), structDef);

auto postcondition = ConjunctionTerm::of(getPostcondition());
calculateWP(&structDef.getProductFuncOp().getFunctionBody().front(),
postcondition);

verificationConditions = postcondition.buildTerm(mgr);
extraDecls = builder.getExtraDecls(verificationConditions);
declBounds = builder.getDeclBounds(extraDecls, field.prime());
}

cvc5::Term WeakestPreconditionAnalysis::generateVerificationConditions() {
llvm::Expected<cvc5::Term>
WeakestPreconditionAnalysis::generateVerificationConditions() {
util::ensureProductFunc(structDef->getParentOfType<ModuleOp>(), structDef);

if (structDef.getMemberDefs().empty()) {
return llvm::createStringError("Unsupported: struct has no members");
}
auto postcondition = ConjunctionTerm::of(getPostcondition());
calculateWP(&structDef.getProductFuncOp().getFunctionBody().front(),
postcondition);
if (llvm::Error err =
calculateWP(&structDef.getProductFuncOp().getFunctionBody().front(),
postcondition)) {
return err;
}

return postcondition.buildTerm(mgr);
}

void WeakestPreconditionAnalysis::emit(llvm::raw_ostream &os) {
auto verificationConditions = generateVerificationConditions();
auto extraDecls = builder.getExtraDecls(verificationConditions);
llvm::Expected<cvc5::Term> verificationConditions =
generateVerificationConditions();

if (auto err = verificationConditions.takeError()) {
llvm::errs() << err << "\n";
return;

@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 Consume the propagated LLVM error after reporting it

When an unsupported construct reaches this branch in a build with LLVM_ENABLE_ABI_BREAKING_CHECKS enabled, streaming err only logs its payload; it does not consume the llvm::Error. The still-failing error is then destroyed on return and calls fatalUncheckedError(), so the newly supported graceful path aborts instead. Consume it while reporting, for example with llvm::logAllUnhandledErrors(std::move(err), llvm::errs()).

Useful? React with 👍 / 👎.

}

auto extraDecls = builder.getExtraDecls(*verificationConditions);
auto bounds = builder.getDeclBounds(extraDecls, field.prime());

os << "(set-logic ALL)\n";
Expand All @@ -620,7 +647,7 @@ void WeakestPreconditionAnalysis::emit(llvm::raw_ostream &os) {
}

os << "; Verification condition\n";
os << "(assert " << verificationConditions.notTerm().toString() << ")\n";
os << "(assert " << verificationConditions->notTerm().toString() << ")\n";
os << "(check-sat)\n";
os << "(get-model)\n";
}
Expand Down
14 changes: 13 additions & 1 deletion scripts/collect_circom_demo_results.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
SAT_RE = re.compile(r"^\s*sat\s*$", re.MULTILINE)
UNSAT_RE = re.compile(r"^\s*unsat\s*$", re.MULTILINE)
UNKNOWN_RE = re.compile(r"^\s*unknown\s*$", re.MULTILINE)
UNSUPPORTED_PREFIX = "Unsupported:"


def get_benchmarks(benchmark_dir: pathlib.Path) -> list[tuple[str, pathlib.Path, str]]:
Expand Down Expand Up @@ -150,6 +151,16 @@ def run_wp(
return (benchmark, root_struct, "wp", "timeout", f"{elapsed:.6f}", "timeout")

elapsed = time.perf_counter() - start
if not lleq_stdout.strip() and lleq_stderr.startswith(UNSUPPORTED_PREFIX):
message = lleq_stderr.strip()[:500]
return (
benchmark,
root_struct,
"wp",
"unsupported",
f"{elapsed:.6f}",
message,
)
if lleq_proc.returncode != 0:
message = (lleq_stderr or lleq_stdout).strip()[:500]
return (benchmark, root_struct, "wp", "error", f"{elapsed:.6f}", message)
Expand Down Expand Up @@ -291,13 +302,14 @@ def main() -> None:
"counterexample": 0,
"partial": 0,
"timeout": 0,
"unsupported": 0,
"error": 0,
}
for _, _, _, result, _, _ in results:
counts[result] += 1

print(
"verified: {verified}, counterexample: {counterexample}, partial: {partial}, timeout: {timeout}, error: {error}".format(
"verified: {verified}, counterexample: {counterexample}, partial: {partial}, timeout: {timeout}, unsupported: {unsupported}, error: {error}".format(
**counts
)
)
Expand Down
Loading