Enforce model-checking depth bounds at the frontier

[hwbehrens]

Summary

• stop checking safety, deadlock, and assertion violations once BFS has crossed the configured depth frontier
• update the sequential context to expose the just-completed frontier before processing the next state
• surface already-recorded in-bound violations even when depth-bound termination wins
• report the configured bound instead of the overshot internal depth
• cover sequential and parallel boundary behavior with an independent linear transition system

Root cause

The checker evaluated violations before honoring reachedDepthBound, and sequential search passed stale completedDepth state into that decision. Consequently a state beyond the requested BFS frontier could be reported as a counterexample. The termination result could also expose the overshot internal frontier instead of the configured bound.

Minimum viable reproduction

Save this as DepthBound.lean. The first bad state is exactly four transitions from the initial state, while the requested bound is three:

import Veil.Core.Tools.ModelChecker.Concrete.Checker

open Veil Veil.ModelChecker Veil.ModelChecker.Concrete

def chain : EnumerableTransitionSystem Unit (List Unit) Nat (List Nat) Int Nat
    (List (Nat × ExecutionOutcome Int Nat)) () := {
  initStates := [0]
  tr := fun _ n => if n < 6 then [(n, .success (n + 1))] else []
}

def params : SearchParameters Unit Nat := {
  invariants := [{ name := `belowFour, property := fun _ n => n < 4 }]
  earlyTerminationConditions := [.foundViolatingState, .reachedDepthBound 3]
}

#eval do
  let token ← IO.CancelToken.new
  let result ← findReachable (asm := ActionStatsMap Nat)
    chain params none 999999 token
  IO.println (repr result)

Run:

$ lake env lean DepthBound.lean

Observed before this PR: the sequential search reports the bad state at depth 4 despite the configured bound of 3 (and the analogous parallel search does the same). Some bounded-safe results report the overshot internal depth.

Expected: the result is .noViolationFound ... (.reachedDepthBound 3). Raising the bound to 4 must instead include and report the depth-4 safety violation. Sequential and parallel modes must agree.

Regression test

VeilTest/Regression/ModelCheckDepthBound.lean builds this independent linear transition system and runs findReachable directly. It asserts, in both sequential and forced-parallel modes, that bound 3 excludes the depth-4 violation and reports exactly 3, while bound 4 includes the violation with a four-step trace. It also checks that bound 0 still reports an invariant violation in the initial state with a zero-step trace. The test throws an IO.userError on any other result, so the file cannot build if either boundary regresses.

Verification

• reproduced the out-of-bound depth-2 counterexample from R2_MaxDepthBoundary.lean
• reran the sequential/parallel linear-chain probe across bounds 0, 2, 3, 4, and 5
• lake build VeilTest.Regression.ModelCheckDepthBound
• lake build VeilTest (1502 jobs)
• git diff --check

[hwbehrens]

Review findings — the frontier fix itself is correct in both drivers (traced: sequential processState now sees a fresh completedDepth via ctxAtDepth, the parallel round-based path was already fresh, and in-bound violations recorded before depth-bound termination are surfaced by the new Checker branch). But the suppression predicate introduces one confirmed regression.

Confirmed regression: depth bound 0 skips all checks on initial states (reproduced)

In Veil/Core/Tools/ModelChecker/Concrete/Core.lean:223-224, checks are suppressed when completedDepth >= bound for .reachedDepthBound bound. Initial states are processed at depth 0 with completedDepth = 0, so with .reachedDepthBound 0 the comparison 0 >= 0 suppresses all safety/deadlock/assertion checks on initial states.

Reproduced failure scenario (both sequential and parallel drivers, on this PR's head): a transition system whose initial state violates an invariant, searched via findReachable with earlyTerminationConditions including .reachedDepthBound 0, returns noViolationFound … (reachedDepthBound 0). On the base branch it returned foundViolation. That is a false SAFE.

Reachability: the #model_check frontend only adds reachedDepthBound when maxDepth > 0 (mkSearchParameters in Veil/Frontend/DSL/Module/Elaborators.lean), so this is reachable only through the direct findReachable API — which is exactly how this PR's own regression test invokes the checker, so the API contract matters.

The underlying off-by-one asymmetry: for every bound b ≥ 1, states at depth b are checked (only depth b+1 is suppressed), but for b = 0, depth-0 states are not checked. The predicate conflates "how many frontiers have completed" with "this state's depth".

Suggested fix: base suppression on the state's actual depth rather than the completed-frontier count — i.e., suppress checks only when the state's depth d > bound (equivalently completedDepth + 1 > bound at the point where a newly dequeued state at depth completedDepth + 1 is processed, but expressing it via the state's own depth is clearer and avoids re-deriving this off-by-one). Then add a regression case: violating initial state + .reachedDepthBound 0 must return foundViolation, and a violation at depth bound + 1 must still be suppressed.

Minor pre-existing note (unchanged by this PR, no action needed): distinctCount in the noViolationFound result still counts enqueued-but-unchecked bound+1 states.