Classify bugFinding goals with the mode-aware predicates at minimal check level

[repowazdogz-droid]

Classify bugFinding goals with the mode-aware predicates at minimal check level

Repository: strata-org/Strata
Branch: fix/bugfinding-reporting
Base commit: a61d47e5643820dc08a7d119d3226df48d20926b

Related change in strata-org/Strata-CLI #7, branch fix/bugfinding-reporting. The two share a root cause and sit at different call sites, and neither depends on the other.

Below --check-level full, bugFinding runs the satisfiability check and not the validity check (verifySingleEnv, Verifier.lean:1788-1798 on main, the | .bugFinding, _ => (true, false) arm). validityProperty is therefore unknown on every goal in that mode, and a predicate that reads validity misclassifies all of them. This PR changes VCOutcome.label and emoji, which is the per-goal line. #7 changes verifyCommand in StrataMainLib.lean, which is the aggregate counts and the summary line.

Either can land first. #7 does not call anything this PR adds, and the two predicates it does call, VCResult.isBugFindingSuccess and isBugFindingFailure, were on main before either PR opened. Building the CLI branch against upstream Strata main at eabf62d5f, which does not contain this PR, produces the same counts as building it with this PR applied.

What holds is weaker than a dependency: neither PR on its own changes the whole of the reported behaviour. This one changes the labels while the summary still counts every goal as failed, and #7 changes the counts while the per-goal labels stay as they are. That is review context, not an ordering constraint.

What I ran

Two Core programs, one correct and one with a check/update race, verified with the strata CLI built from Strata-CLI at 5441d7d against this repository.

charge_cap.core.st charges k against a meter capped at 100 and asserts meter <= 100, with a second procedure that calls the charge twice and asserts the cap still holds. charge_cap_toctou.core.st reads the meter into a local, lets a second cap-respecting charge land, then applies the update on the basis of the stale local.

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

The same program, same commit, at --check-level full:

$ strata verify charge_cap.core.st --check-mode bugFinding --check-level full
charge_cap.core.st(14, 2) [cap_holds]: ✅ always true and is reachable from declaration entry
charge_cap.core.st(15, 2) [monotone]: ✅ always true and is reachable from declaration entry
...
All 7 goals passed.
EXIT=0

Expected: no errors. docs/VerificationModes.md:11 states

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

and the table at docs/VerificationModes.md:22-32 gives pass in the BugFinding column for both rows this program's goals land on, sat/unsat at line 24 and unknown/unsat at line 31. The program has no definite bug, and the same binary says so at a different check level.

The buggy program produced the same output shape:

$ strata verify charge_cap_toctou.core.st --check-mode bugFinding
charge_cap_toctou.core.st(19, 2) [cap_holds]: ❓ satisfiable
Finished with 0 goals passed, 1 failed.
EXIT=2

A correct program and a program with a real cap violation are indistinguishable at the default check level in the mode whose purpose is to separate them.

Root cause

Strata/Languages/Core/Verifier.lean:1072-1076, in VCOutcome.label:

      else
        match o.satisfiabilityProperty with
        | .sat _ => "satisfiable"
        | .unsat => "fail"
        | .unknown _ | .err _ => "unknown"

and the same shape at Verifier.lean:1108-1112 in VCOutcome.emoji. The branch has no case that reports a goal as passing. bugFinding reaches it with the satisfiability result only, because of the check selection at Verifier.lean:1795-1798:

        | .bugFindingAssumingCompleteSpec, _ => (true, true)
        | .deductive, _ =>
          if obligation.property.passWhenUnreachable then (false, true) else (true, false)
        | .bugFinding, _ => (true, false)

VCOutcome.bugFindingSuccess and bugFindingFailure at Verifier.lean:1022-1028 already encode the correct classification and were unreferenced from the labelling path.

Fix

Add a bugFinding case to both functions that uses those predicates:

      else if checkMode == .bugFinding then
        if o.bugFindingFailure then "fail"
        else if o.bugFindingSuccess then "no definite bug"
        else "unknown"

The label is no definite bug rather than pass. At minimal level in this mode only the satisfiability check has run, so a sat result rules out a definite bug but does not establish that the assertion holds. Calling it pass would claim more than the single query supports.

bugFindingAssumingCompleteSpec keeps its existing branch untouched. It runs both checks and treats any counterexample as an error, which bugFindingSuccess does not express: applying the bug-finding predicates to that mode turns a reported violation into a reported pass. I hit exactly that while writing this patch, with a first version that matched on | _ => instead of .bugFinding, and it silently converted the TOCTOU failure into ✅ pass with exit 0.

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 byte-identical before and after, on both programs: All 7 goals passed with exit 0 for the correct one, and

charge_cap_toctou.core.st(19, 2) [cap_holds]: ❌ fail
Finished with 0 goals passed, 1 failed.
EXIT=2

for the racy one. bugFindingAssumingCompleteSpec is also unchanged on both, including exit 2 on the racy program.

Tests

StrataTest/Languages/Core/VCOutcomeTests.lean exercised label and emoji only at .full .deductive, so the branch this PR changes had no coverage. Added #guards for the minimal labels and emoji in all three modes, including two that pin the bugFindingAssumingCompleteSpec and deductive labels so a future change cannot quietly repeat the mistake described above.

lake build and lake test both pass on the patched tree, 533 jobs and All 2 test file(s) passed, on macOS 15.7.3 arm64 with Lean 4.29.1, cvc5 1.3.4 and z3 4.15.2. The 12 [addPathCondition] Label clash detected warnings in the Laurel end-to-end tests are present in an unpatched build of the same commit at the same count.

Strata/Transform/CoreSpecification.lean:398 already specifies pass for .bugFinding as ∀ r ∈ results, VCResult.isBugFindingSuccess r = Bool.true, so this change moves the reporting path towards that specification rather than away from it. It is a field of a def, not a theorem, so nothing was proved about it either way.

One thing to confirm before merging

This makes plain bugFinding quieter. An assertion that can be violated on some path but not all, the sat/sat row, is a note in the BugFinding column of docs/VerificationModes.md:26, and StrataTest/Languages/Core/VCOutcomeTests.lean:145 already asserts

#guard outcomeToLevel .bugFinding .assert (mkOutcome (.sat []) (.sat [])) = Strata.Sarif.Level.note

so the SARIF path has always treated it that way. After this change the console and the exit code agree with SARIF, which means my racy program is reported as no definite bug with exit 0 under --check-mode bugFinding, and is caught by deductive and by bugFindingAssumingCompleteSpec with exit 2. That follows the documented semantics, but it is a visible behaviour change for anyone currently reading a non-zero exit from bugFinding as a signal, so it is worth an explicit decision rather than my inference from the table.

A second consequence worth naming: in bugFinding the pass and fail counts no longer sum to the goal total, because a goal that is neither a definite bug nor a proven pass is counted in neither. The three unknown goals in the output above are that case. That is a CLI concern rather than one for this PR, and Strata-CLI #7 now adds a third count so the summary accounts for every goal.

Companion PR: strata-org/Strata-CLI#7

[repowazdogz-droid]

Checking in on this one. The branch is behind main now, so I will rebase it and re-run lake build and lake test unless you would rather it stayed as it is.

The change is 17 lines in Verifier.lean, with the 28 lines of #guard coverage in a separate test file, so the tests can be split out or dropped if that makes review easier.

No rush from my side. If there is anything you would like changed before it gets a look, say so and I will pick it up.

[shigoel]

Thanks so much for this PR (and also for the related one on Strata-CLI!).

Quick note that the documentation job in the CI is failing. Could you please fix that?

[MikaelMayer]

I just posted a comment on strata-org/Strata-CLI#7 that when resolved will probably also influence this PR. Thanks a lot.

[repowazdogz-droid]

Thanks for taking a look.

On the documentation job: the failing targets are Strata.DL.SMT.Term and Strata.DL.SMT.DDMTransform.Parse. The first error is Strata/DL/SMT/Term.lean:43:48: failed to synthesize instance of type class, followed by a cascade of unknown-dialect and unknown-attribute errors in Parse.lean. Neither file is in this PR, which only touches Verifier.lean and VCOutcomeTests.lean. The same failure is on main near the point this branch is based on, in run 30642481112 on 31 July.

Current main also fails the documentation job, but for a different reason: a clang bracket nesting level exceeded maximum of 256 in the generated Translate.c, in run 30859181838 on 3 August. So a rebase would trade one documentation failure for another rather than clear it.

This branch is 39 commits behind main. Would you like me to rebase anyway, or leave it until the documentation build on main is sorted out?