Count verification goals with the predicate that matches the check mode

[repowazdogz-droid]

Count verification goals with the predicate that matches the check mode

Repository: strata-org/Strata-CLI
Branch: fix/bugfinding-reporting
Base commit: 2fbbdfc (rebased onto main)

Companion change in strata-org/Strata, branch fix/bugfinding-reporting, which fixes the per-goal labels. This PR fixes the counts and the exit code. Neither is complete alone.

What I ran

A Core program that charges k against a meter capped at 100 and asserts meter <= 100, verified in each of the three check modes. Full reproduction and the second, deliberately racy, program are in the Strata PR.

Observed, before the change

$ strata verify charge_cap.core.st --check-mode bugFinding
Successfully parsed.
charge_cap.core.st(14, 2) [cap_holds]: ❓ satisfiable
charge_cap.core.st(15, 2) [monotone]: ❓ satisfiable
charge_cap.core.st(35, 2) [callElimAssert_k_nonneg_12]: ❓ satisfiable
charge_cap.core.st(35, 2) [callElimAssert_meter_in_range_13]: ❓ satisfiable
charge_cap.core.st(36, 2) [callElimAssert_k_nonneg_4]: ❓ unknown
charge_cap.core.st(36, 2) [callElimAssert_meter_in_range_5]: ❓ unknown
charge_cap.core.st(32, 2) [cap_holds_cumulative]: ❓ unknown
Finished with 0 goals passed, 7 failed.
EXIT=2

Expected: exit 0 and no failures. The program is correct, --check-mode deductive proves all seven goals on the same commit, and docs/VerificationModes.md:11 in the Strata repository states

• bugFinding — Find bugs assuming incomplete preconditions: only definite bugs are errors.

Root cause

StrataMainLib.lean:643 and :649-650:

      let success := vcResults.all Core.VCResult.isSuccess
      ...
        let provedGoalCount := (vcResults.filter Core.VCResult.isSuccess).size
        let failedGoalCount := (vcResults.filter Core.VCResult.isNotSuccess).size

with the exit code driven by !r.isSuccess at :654. VCResult.isSuccess reduces to VCOutcome.isPass, which requires the validity query to have returned unsat. --check-mode bugFinding runs the satisfiability query only, so isPass is false on every goal regardless of the program, isNotSuccess is true on every goal, and the exit code is 2 whatever was verified.

VCResult.isBugFindingSuccess and isBugFindingFailure exist for this at Strata/Languages/Core/Verifier.lean:1316-1324, referenced from Strata/Transform/CoreSpecification.lean:398 and from nothing in the reporting path.

Fix

Select the predicate from opts.checkMode:

      let goalPassed : Core.VCResult → Bool :=
        match opts.checkMode with
        | .bugFinding => Core.VCResult.isBugFindingSuccess
        | _ => Core.VCResult.isSuccess
      let goalFailed : Core.VCResult → Bool :=
        match opts.checkMode with
        | .bugFinding => Core.VCResult.isBugFindingFailure
        | _ => Core.VCResult.isNotSuccess

bugFindingAssumingCompleteSpec stays on the deductive predicates on purpose. Any counterexample is an error in that mode, isSuccess already expresses it, and isBugFindingSuccess does not: routing that mode through the bug-finding predicates reports a real violation as a pass with exit 0. A first version of this patch matched on | _ => and did exactly that to the racy program from the Strata PR, turning exit 2 into exit 0.

Failure and exit are now driven by goalFailed rather than by the negation of success, so a goal that is neither a definite bug nor a proven pass no longer forces a non-zero exit.

Result

$ strata verify charge_cap.core.st --check-mode bugFinding
charge_cap.core.st(14, 2) [cap_holds]: ✅ no definite bug
charge_cap.core.st(15, 2) [monotone]: ✅ no definite bug
charge_cap.core.st(35, 2) [callElimAssert_k_nonneg_12]: ✅ no definite bug
charge_cap.core.st(35, 2) [callElimAssert_meter_in_range_13]: ✅ no definite bug
charge_cap.core.st(36, 2) [callElimAssert_k_nonneg_4]: ❓ unknown
charge_cap.core.st(36, 2) [callElimAssert_meter_in_range_5]: ❓ unknown
charge_cap.core.st(32, 2) [cap_holds_cumulative]: ❓ unknown
Finished with 4 goals passed, 0 failed.
EXIT=0

Deductive mode is unchanged on both the correct and the racy program, All 7 goals passed with exit 0 and 0 goals passed, 1 failed with exit 2 respectively. bugFindingAssumingCompleteSpec is unchanged on both, including exit 2 on the racy program.

lake build succeeds, 568 jobs, on macOS 15.7.3 arm64 with Lean 4.29.1.

Second commit: reporting the undecided goals

The note below said the pass and fail counts no longer sum to the goal total,
and offered to report the remainder. e9b14c1 does that.

bugFinding has three outcome categories rather than two.
docs/VerificationModes.md classifies the nine satisfiability/validity cells
per mode, and its bugFinding column reads pass on two cells, error on
three, and note on four. The two counters mapped those nine cells onto two
buckets, so the four note cells were split: (sat, sat) and (sat, unknown)
were counted as passed, while (unknown, sat) and (unknown, unknown) matched
neither predicate and were counted in neither place. Outer .error results,
which is where a solver timeout or an encoding failure lands, matched neither
either.

Counting the remainder as a third bucket:

$ strata verify charge_cap.core.st --check-mode bugFinding --solver-timeout 1
Finished with 4 goals passed, 0 failed, 3 undecided (of 7 goals).

The bucketing moved into countGoals, which counts the remainder positively
rather than as size - passed - failed. The two forms agree on every input any
current mode produces, because the predicates each mode supplies are disjoint.
They differ if a future mode ever supplies overlapping predicates: the
subtraction truncates at zero under Nat and silently loses goals, while the
filter makes the total exceed the goal count where a guard can see it.

#guards pin the bucketing invariant and the nine cells, including the two
that satisfy neither bugFinding predicate. I checked that they are not
vacuous by breaking each one and confirming the build goes red: asserting that
(unknown, unknown) is a bugFindingSuccess fails, and so does substituting
the subtraction form of countGoals.

What I ran for this commit

Twenty-seven combinations, three programs by three check modes by three check
levels, comparing the summary line and the exit code before and against the
change on the same tree.

Mode	Combinations byte-identical
deductive	9 / 9
bugFindingAssumingCompleteSpec	9 / 9
bugFinding	6 / 9

The three that changed are the runs with undecided goals, and each now sums to
the goal count:

- Finished with 4 goals passed, 0 failed.
+ Finished with 4 goals passed, 0 failed, 3 undecided (of 7 goals).

- Finished with 1 goals passed, 0 failed.
+ Finished with 1 goals passed, 0 failed, 1 undecided (of 2 goals).

No exit code changed in any of the twenty-seven. An undecided goal is
inconclusive, which AGENTS.md records as exit 0.

Verified on 2fbbdfc, which this branch is now rebased onto, with dependencies
resolved by lake update as lake-manifest.json declares them (inputRev: main). The rebased tree is byte-identical to the tree those runs were made
against. The Strata revision used was upstream main, which does not contain
#1448, so the counts here are correct without the companion change. The per-goal
labels still need it.

Building against the committed rev pins rather than inputRev fails, but that
is not specific to this branch: main fails the same way, with the same errors,
and its own Build run on 2026-07-29 is red for that reason. fix/cli-manifest-pin
is the fix for it and is deliberately not folded in here.

Companion PR: strata-org/Strata#1448

[repowazdogz-droid]

I pushed the undecided-goal counter and requested review on 1 August, so this is a note that I am still around for it rather than a nudge.

The branch is behind main. I will rebase it if that is useful, otherwise I will leave it where it is.

If there is anything you would like changed before review, say so and I will pick it up.

[MikaelMayer]

Hey thank you very much for your help in setting things right and ensuring reporting is consistent and helpful. I agree we need to do something.

pass / fail / unknown is something relevant for the deductive analysis (and most of the time it's only pass / unknown unless we can prove that there is a true counter-example)
For bugFinding without deductive verification, we should have only fail / unknown. We can never prove that the assertion "passes" which means is always true.

So, "✅ no definite bug" could be misleading. Please refer to the classification of the icons we used for VCOutcome to be consistent.
https://github.com/strata-org/Strata/blob/b1acfb6a4b17752d368754e865397f61d1a4ec50/StrataTest/Languages/Core/VCOutcomeTests.lean#L109

When doing bug finding, instead of summarizing the results with pass / fail / unknown, I think we should summarize them with bugs founds / satisfiable and reachable / unknown.
This this is a CLI change, could you please make that change as part of your PR?

[repowazdogz-droid]

Thanks. I agree, and I will switch the non-deductive bugFinding path from pass / fail / unknown to bugs found / satisfiable and reachable / unknown, classified against the VCOutcome table rather than the deductive predicates.

One correction before I start, because a CLI-only change will not fully cover what you flagged. "✅ no definite bug" is not in Strata-CLI. It is in strata-org/Strata, in label and emoji in Strata/Languages/Core/Verifier.lean, and it is not on main either: those lines are added by #1448. The CLI half is the summary line in StrataMainLib.lean that reports the counts. So the change lands across both PRs, with the vocabulary and icons in #1448 and the summary line plus exit codes here. I am happy to do both. Say if you would rather they went in one PR, or in a particular order.

Three boundary questions before I write anything. I have stated what I would do by default, so you can correct only the ones you disagree with. Names below are the predicates in Verifier.lean.

1. Which cells count as bugs found. I would use alwaysFalseAndReachable (❌) and alwaysFalseReachabilityUnknown (✖️), which together are isAlwaysFalse. The second is a definite falsity with unknown reachability, and it is a SARIF error in bugFinding, so I read it as a bug found rather than as unknown. Correct me if you want it in unknown.

2. Where dead code goes. bugFindingFailure currently also includes unreachable (✅❗). Unreachable code is a SARIF error, but it is not a bug in the assertion, so I would not report it under bugs found. It does not fit satisfiable and reachable or unknown either. Do you want a fourth category for it, or should it fold into unknown?

3. Where passReachabilityUnknown goes (✔️, always true if reached). It is currently in bugFindingSuccess, through the second disjunct of isSatisfiable || passReachabilityUnknown. It is not satisfiable, and isReachable is false for it, so I would move it into unknown. Correct me if you would rather it stayed with the satisfiable and reachable group.

Separately, on the CI here. Both failing jobs are a pre-existing build break rather than anything in this branch. StrataMainLib.lean does not compile against the Strata revision pinned in lake-manifest.json: parseVerifyOptions and parseLaurelVerifyOptions no longer take inputFile, Strata.Core.verify no longer takes pipelineCtx, and VerifyOptions.keepAllFilesPrefix and Dialect.passInsertLoopInvariantAsserts are gone. The same errors are on main, in run 30859154245 on 3 August and run 30483980917 on 29 July. They are also outside this PR's diff: the two hunks here start at line 567, and several of the errors are above that. Run 30715359180 is the first CI execution this branch has had, since the two earlier ones stopped at action_required.

I put the fix up separately as #8. It is a three-line lake-manifest.json bump and touches no source. No CI has run on it, so I cannot say it goes green, only that it is the intended fix. If you are able to look at it, it should unblock CI here.

I can implement the vocabulary change as soon as the three questions above are settled. The bucket counting added in this PR carries over without rework: the buckets and the guards that pin the total stay as they are, and only the labels and the choice of which predicate feeds which bucket change.