From ab55ccc818b4173b3000884ddd6ccf37d1984226 Mon Sep 17 00:00:00 2001 From: wazdogz <233830950+repowazdogz-droid@users.noreply.github.com> Date: Fri, 24 Jul 2026 10:33:22 +0100 Subject: [PATCH 1/2] Count verification goals with the predicate that matches the check mode `verifyCommand` computed the pass count, the fail count and the exit code with `VCResult.isSuccess`/`isNotSuccess` in every mode. Those require the validity check to have returned unsat, and `--check-mode bugFinding` runs the satisfiability check only, so a correct program reported "0 goals passed, N failed" and exited 2. Select the predicate from `opts.checkMode`: `bugFinding` uses `isBugFindingSuccess`/`isBugFindingFailure`, everything else keeps `isSuccess`/`isNotSuccess`. `bugFindingAssumingCompleteSpec` is deliberately left on the deductive predicates, because any counterexample is an error in that mode and the bug-finding predicates would report it as a pass. Requires the matching Strata change to `VCOutcome.label`/`emoji`. Co-Authored-By: Claude Opus 4.8 (1M context) --- StrataMainLib.lean | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/StrataMainLib.lean b/StrataMainLib.lean index 05426dc..f62390c 100644 --- a/StrataMainLib.lean +++ b/StrataMainLib.lean @@ -656,18 +656,33 @@ def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Com let posStr := Imperative.MetaData.formatFileRangeD vcResult.obligation.metadata (some inputCtx.fileMap) println! f!"{posStr} [{vcResult.obligation.label}]: \ {vcResult.formatOutcome}" - let success := vcResults.all Core.VCResult.isSuccess + -- Success/failure are mode-specific. `bugFinding` treats only a definite + -- bug as an error (docs/VerificationModes.md), and runs the + -- satisfiability check alone, so the deductive predicate reported every + -- goal of a correct program as failed with a non-zero exit. Only + -- `bugFinding` is remapped here: `bugFindingAssumingCompleteSpec` runs + -- both checks and any counterexample is an error there, which is what + -- `isSuccess`/`isNotSuccess` already express. + 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 + let success := vcResults.all goalPassed if success && !opts.checkOnly then println! f!"All {vcResults.size} goals passed." else if success && opts.checkOnly then println! f!"Skipping verification." else - let provedGoalCount := (vcResults.filter Core.VCResult.isSuccess).size - let failedGoalCount := (vcResults.filter Core.VCResult.isNotSuccess).size + let provedGoalCount := (vcResults.filter goalPassed).size + let failedGoalCount := (vcResults.filter goalFailed).size -- Encoding failures, solver crashes, or per-check SMT errors (exit 3) let hasImplError := vcResults.any (fun r => r.isImplementationError || r.hasSMTError) -- Assertion violations that are not timeouts or internal errors (exit 2) - let hasFailure := vcResults.any (fun r => !r.isSuccess && !r.isTimeout && !r.isImplementationError && !r.hasSMTError) + let hasFailure := vcResults.any (fun r => goalFailed r && !r.isTimeout && !r.isImplementationError && !r.hasSMTError) println! f!"Finished with {provedGoalCount} goals passed, {failedGoalCount} failed." if hasImplError then IO.Process.exit ExitCode.internalError From 04777bcd469ba9d79cb567399bb9aee0755f7439 Mon Sep 17 00:00:00 2001 From: wazdogz <233830950+repowazdogz-droid@users.noreply.github.com> Date: Sat, 1 Aug 2026 20:22:48 +0100 Subject: [PATCH 2/2] Report goals that the check mode leaves undecided The pass and fail predicates a check mode supplies are independent, not complements. `bugFinding` uses `isBugFindingSuccess`/`isBugFindingFailure`, and a goal whose satisfiability check comes back `unknown`, times out, or fails to encode satisfies neither, so counting only passes and failures dropped it from a line that carries no total. A seven-goal run of a correct program printed "Finished with 4 goals passed, 0 failed." Count that remainder as a third bucket and report it, with the goal total, when it is non-empty. `deductive` and `bugFindingAssumingCompleteSpec` supply complementary predicates, so the bucket is empty and their output is unchanged. Bucketing moves into `countGoals`, which counts the remainder positively rather than as `size - passed - failed`, so that overlapping predicates would show up as a total exceeding the goal count instead of being truncated away by `Nat` subtraction. `#guard`s pin that bucketing never drops or double-counts a goal, and pin which of the two `bugFinding` predicates holds in each of the nine satisfiability/validity cells of docs/VerificationModes.md, including the two cells that satisfy neither. Exit codes are unchanged. An undecided goal is inconclusive, which AGENTS.md records as exit 0. Co-Authored-By: Claude Opus 5 (1M context) --- StrataMainLib.lean | 125 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 122 insertions(+), 3 deletions(-) diff --git a/StrataMainLib.lean b/StrataMainLib.lean index f62390c..db368ad 100644 --- a/StrataMainLib.lean +++ b/StrataMainLib.lean @@ -567,6 +567,115 @@ def transformCommand : Command where | .ok (program, _) => IO.print (Core.formatProgram program) | .error e => exitFailure s!"Transform failed: {e}" +/-- The three buckets the verification summary line reports. + + The pass and fail predicates a check mode supplies are independent, not + complements. In `bugFinding` they are `isBugFindingSuccess` and + `isBugFindingFailure`, and a goal whose satisfiability check came back + `unknown`, timed out, or failed to encode satisfies neither, so it belongs + to `undecided`. `deductive` and `bugFindingAssumingCompleteSpec` pass + complementary predicates, so `undecided` is 0 for them. -/ +structure GoalCounts where + passed : Nat + failed : Nat + undecided : Nat + deriving Repr, DecidableEq + +/-- Bucket every element of `xs` by a pass and a fail predicate, counting the + remainder positively. Counting `undecided` as its own filter rather than as + `xs.size - passed - failed` keeps predicate overlap visible: overlapping + predicates make `total` exceed `xs.size` instead of being truncated away by + `Nat` subtraction. -/ +def countGoals {α : Type} (passed failed : α → Bool) (xs : Array α) : GoalCounts := + { passed := (xs.filter passed).size + failed := (xs.filter failed).size + undecided := (xs.filter (fun x => !passed x && !failed x)).size } + +/-- The count the summary line divides into buckets. -/ +def GoalCounts.total (c : GoalCounts) : Nat := c.passed + c.failed + c.undecided + +/-! ### Guards for the goal accounting + +`docs/VerificationModes.md` classifies each of the nine satisfiability/validity +outcomes per mode, and `bugFinding` is the mode with three categories rather +than two: `pass`, `error`, and `note`. The summary line has to account for all +three, so these guards pin (1) that bucketing never drops or double-counts an +element, and (2) which of the two `bugFinding` predicates holds in each of the +nine cells. -/ + +section GoalCountGuards + +/-- Stand-ins for `(goalPassed r, goalFailed r)`, covering the overlap case that + no current mode produces, so that the invariant below is not vacuous. -/ +private def predicatePairs : Array (Bool × Bool) := + #[(true, false), (false, true), (false, false), (true, true)] + +private def tallyOf (xs : Array (Bool × Bool)) : GoalCounts := + countGoals Prod.fst Prod.snd xs + +-- Disjoint predicates: the three buckets partition the input. +#guard (tallyOf #[(true, false), (false, true), (false, false)]) + = { passed := 1, failed := 1, undecided := 1 } +#guard (tallyOf #[(true, false), (false, true), (false, false)]).total = 3 + +-- The `bugFinding` shape from a real run: some passed, none failed, the rest +-- undecided. Before the `undecided` bucket existed this reported 4 and 0 for a +-- seven-goal program. +#guard (tallyOf (Array.replicate 4 (true, false) ++ Array.replicate 3 (false, false))) + = { passed := 4, failed := 0, undecided := 3 } +#guard (tallyOf (Array.replicate 4 (true, false) ++ Array.replicate 3 (false, false))).total = 7 + +-- Overlap is reported, not hidden. Both an element matching both predicates +-- and a genuine remainder have to be present for this to bite: computing +-- `undecided` as `xs.size - passed - failed` truncates to 0 here and loses the +-- remaining element, which is why it is a filter and not a subtraction. +#guard (tallyOf #[(true, true), (false, false)]) + = { passed := 1, failed := 1, undecided := 1 } +#guard (tallyOf #[(true, true), (false, false)]).total = 3 + +-- Every combination is accounted for exactly once when the predicates are +-- disjoint, and the empty run is empty. +#guard (tallyOf #[]).total = 0 + +open Strata.SMT in +/-- The nine outcome cells of `docs/VerificationModes.md`, as + (satisfiability, validity) pairs. -/ +private def outcomeCell (sat val : Imperative.SMT.Result (Ident := Core.Expression.Ident)) + : Core.VCOutcome := + { satisfiabilityProperty := sat, validityProperty := val } + +private def satR : Imperative.SMT.Result (Ident := Core.Expression.Ident) := .sat [] +private def unsatR : Imperative.SMT.Result (Ident := Core.Expression.Ident) := .unsat +private def unknownR : Imperative.SMT.Result (Ident := Core.Expression.Ident) := .unknown + +-- `bugFinding` errors: the three `unsat`-satisfiability cells (always false +-- and reachable, always false if reached, unreachable). +#guard (outcomeCell unsatR satR).bugFindingFailure +#guard (outcomeCell unsatR unknownR).bugFindingFailure +#guard (outcomeCell unsatR unsatR).bugFindingFailure + +-- `bugFinding` passes and notes that `bugFindingSuccess` accepts. +#guard (outcomeCell satR unsatR).bugFindingSuccess +#guard (outcomeCell unknownR unsatR).bugFindingSuccess +#guard (outcomeCell satR satR).bugFindingSuccess +#guard (outcomeCell satR unknownR).bugFindingSuccess + +-- The two cells that satisfy neither predicate. These are the goals the +-- summary line used to drop; they are what `undecided` counts. +#guard !(outcomeCell unknownR satR).bugFindingSuccess + && !(outcomeCell unknownR satR).bugFindingFailure +#guard !(outcomeCell unknownR unknownR).bugFindingSuccess + && !(outcomeCell unknownR unknownR).bugFindingFailure + +-- No cell is both a success and a failure, which is what makes the three +-- buckets a partition in `bugFinding`. +#guard [ outcomeCell satR satR, outcomeCell satR unsatR, outcomeCell satR unknownR + , outcomeCell unsatR satR, outcomeCell unsatR unsatR, outcomeCell unsatR unknownR + , outcomeCell unknownR satR, outcomeCell unknownR unsatR, outcomeCell unknownR unknownR + ].all (fun o => !(o.bugFindingSuccess && o.bugFindingFailure)) + +end GoalCountGuards + def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where name := "verify" args := [ "file" ] @@ -677,13 +786,23 @@ def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Com else if success && opts.checkOnly then println! f!"Skipping verification." else - let provedGoalCount := (vcResults.filter goalPassed).size - let failedGoalCount := (vcResults.filter goalFailed).size + -- `goalPassed` and `goalFailed` are independent predicates, not + -- complements, so a goal can satisfy neither. Reporting only two counts + -- dropped those goals from a line that carries no total: a seven-goal + -- `bugFinding` run printed "4 goals passed, 0 failed". + let counts := countGoals goalPassed goalFailed vcResults -- Encoding failures, solver crashes, or per-check SMT errors (exit 3) let hasImplError := vcResults.any (fun r => r.isImplementationError || r.hasSMTError) -- Assertion violations that are not timeouts or internal errors (exit 2) let hasFailure := vcResults.any (fun r => goalFailed r && !r.isTimeout && !r.isImplementationError && !r.hasSMTError) - println! f!"Finished with {provedGoalCount} goals passed, {failedGoalCount} failed." + -- `deductive` and `bugFindingAssumingCompleteSpec` supply complementary + -- predicates, so `undecided` is 0 and this line is unchanged for them. + if counts.undecided == 0 then + println! f!"Finished with {counts.passed} goals passed, {counts.failed} failed." + else + println! f!"Finished with {counts.passed} goals passed, \ + {counts.failed} failed, {counts.undecided} undecided \ + (of {vcResults.size} goals)." if hasImplError then IO.Process.exit ExitCode.internalError else if hasFailure then