Enforce model-checking depth bounds at the frontier

Veil/Core/Tools/ModelChecker/Concrete/Checker.lean

@@ -112,9 +112,16 @@ def findReachable {ρ σ κ : Type} {m : Type → Type}
     return ModelCheckingResult.foundViolation fingerprint .deadlock (some (← recoverTrace sys ctx fingerprint))
   | some (.earlyTermination (.assertionFailed fingerprint exId)) => do
     return ModelCheckingResult.foundViolation fingerprint (.assertionFailure exId) (some (← recoverTrace sys ctx fingerprint (some exId)))
-  | some (.earlyTermination (.reachedDepthBound _)) =>
-    -- No violation found within depth bound; report number of states explored
-    return ModelCheckingResult.noViolationFound distinctCount (.earlyTermination (.reachedDepthBound ctx.completedDepth))
+  | some (.earlyTermination (.reachedDepthBound bound)) => do
+    if !ctx.violatingStates.isEmpty then
+      let (fingerprint, violation) := ctx.violatingStates.head!
+      let assertionExId := match violation with
+        | .assertionFailure exId => some exId
+        | _ => none
+      return ModelCheckingResult.foundViolation fingerprint violation
+        (some (← recoverTrace sys ctx fingerprint assertionExId))
+    -- No violation found within depth bound; report the configured bound.
+    return ModelCheckingResult.noViolationFound distinctCount (.earlyTermination (.reachedDepthBound bound))
   | some (.earlyTermination .cancelled) =>
     -- Search was cancelled by the user
     return ModelCheckingResult.cancelled

Veil/Core/Tools/ModelChecker/Concrete/Core.lean

@@ -217,14 +217,20 @@ theorem partitionExecutionOutcome.fst_spec {κ σ : Type} (outcomes : List (κ 
 -- `specialize` of `List.filterMap` may not exhibit
 def checkViolationsAndMaybeTerminate
   (completedDepth : Nat)
+  (currentStateDepth : Nat)
   (hasSuccessfulTransition : Bool)
   (assertionFailures : List (Int × σ)) :
   List (σₕ × ViolationKind) × Option (EarlyTerminationReason σₕ) :=
+  let outsideDepthBound := params.earlyTerminationConditions.any fun
+    | .reachedDepthBound bound => currentStateDepth > bound
+    | _ => false
   -- Compute all violation conditions once
-  let safetyViolations := params.invariants.filterMap fun p =>
-    if !p.holdsOn th curr then some p.name else none
+  let safetyViolations := if outsideDepthBound then [] else
+    params.invariants.filterMap fun p =>
+      if !p.holdsOn th curr then some p.name else none
   let safetyViolation := !safetyViolations.isEmpty
-  let deadlock := !hasSuccessfulTransition && !params.terminating.holdsOn th curr
+  let deadlock := !outsideDepthBound && !hasSuccessfulTransition && !params.terminating.holdsOn th curr
+  let assertionFailures := if outsideDepthBound then [] else assertionFailures
 
   -- Collect all violations to add in a single list
   let newViolations : List (σₕ × ViolationKind) :=
@@ -249,8 +255,10 @@ def BaseSearchContext.processState
   let (successfulTransitions, assertionFailures) := partitionExecutionOutcome outcomes
   let hasSuccessfulTransition := !successfulTransitions.isEmpty
   let completedDepth := ctx.completedDepth
+  let currentStateDepth := ctx.currentFrontierDepth
   let (newViolations, earlyTermination) :=
-    checkViolationsAndMaybeTerminate params th fpSt curr completedDepth hasSuccessfulTransition assertionFailures
+    checkViolationsAndMaybeTerminate params th fpSt curr completedDepth currentStateDepth
+      hasSuccessfulTransition assertionFailures
   let ctx := {ctx with violatingStates := newViolations ++ ctx.violatingStates}
   -- Check for violations, record them, and determine if we should terminate early
   let ctx := match earlyTermination with

Veil/Core/Tools/ModelChecker/Concrete/MapReduce.lean

@@ -137,10 +137,11 @@ theorem MapReduceSearchContextLocalInvariants.processState_progress
 
   dsimp [MapReduceSearchContextLocal.processState]
   fun_cases BaseSearchContext.processState params th fpSt curr (sys.tr th curr) ctx
-  rename_i succs exns h_eq_part hasSuccessfulTransition completedDepth newViolations
+  rename_i succs exns h_eq_part hasSuccessfulTransition completedDepth currentStateDepth newViolations
     earlyTermination h_eq_checkvio ctx' ctx''
-  subst completedDepth ; dsimp only
-  revert h_eq_checkvio ; fun_cases checkViolationsAndMaybeTerminate params th fpSt curr ctx.completedDepth hasSuccessfulTransition exns
+  subst completedDepth currentStateDepth ; dsimp only
+  revert h_eq_checkvio ; fun_cases checkViolationsAndMaybeTerminate params th fpSt curr
+    ctx.completedDepth ctx.currentFrontierDepth hasSuccessfulTransition exns
   rename_i safetyViolations safetyViolation deadlock tmp1 tmp2
   intro htmp ; injection htmp with h_eq_newvio h_eq_earlyterm ; subst tmp1 tmp2
   -- see if early termination happened
@@ -234,11 +235,13 @@ def bfsBigStep
   (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) ℤ κ (List (κ × ExecutionOutcome ℤ σ)) th)
   (globalSeen : ShardedTreeSetUSize σₕ)
   (completedDepth : Nat)
+  (currentFrontierDepth : Nat)
   (queue : List (MapReduceQueueItem σₕ σ))
   (h_inqueue_reachable : ∀ item ∈ queue, sys.reachable item.state) :
   m (LawfulMapReduceSearchContextLocal (κ := κ) sys params globalSeen (· ∈ queue)) :=
   let lctx : LawfulMapReduceSearchContextLocal sys params globalSeen (fun _ => False) :=
-    ⟨MapReduceSearchContextLocal.initial completedDepth, MapReduceSearchContextLocalInvariants.initial sys params globalSeen completedDepth⟩
+    ⟨MapReduceSearchContextLocal.initial completedDepth currentFrontierDepth,
+      MapReduceSearchContextLocalInvariants.initial sys params globalSeen completedDepth currentFrontierDepth⟩
   let res := lctx.processWorkQueue queue processWorkQueue.subproof6 h_inqueue_reachable
   pure res
 
@@ -575,12 +578,14 @@ def breadthFirstSearchParallel {m : Type → Type}
         let numLarge := tovisitLen % numSplits
         let splitLists := ListSplit.splitList numSplits chunkSize numLarge tovisit
         let completedDepth := base.completedDepth
+        let currentFrontierDepth := base.currentFrontierDepth
         -- Map step: spawn parallel tasks
         -- **CAVEAT**: The call to `IO.asTask` **SHOULD NOT** be put in this procedure,
         -- as that might cause parallelism to vanish!!! Instead, the call should be defined
         -- in some other file.
         let tasks ← IteratedProd.taskSplit splitLists fun subList h_sublist_in =>
-          LawfulMapReduceSearchContextLocal.bfsBigStep params sys globalSeen completedDepth subList
+          LawfulMapReduceSearchContextLocal.bfsBigStep params sys globalSeen completedDepth
+            currentFrontierDepth subList
             (breadthFirstSearchParallel.subproof1 h_mctx.queue_sound splitLists
               (fun item hm => (ListSplit.splitList_mem_iff numSplits chunkSize numLarge tovisit item).mp hm) _ h_sublist_in)
         let results ← IteratedProd.mapM

Veil/Core/Tools/ModelChecker/Concrete/MapReduceLemmas.lean

@@ -14,13 +14,14 @@ def MapReduceSearchContextMain.initial (initStates : List σ) (numShards : Nat)
     tovisit := tovisit,
     globalSeen := ShardedTreeSetUSize.ofListFastByHash fps numShards h_pos h_small }
 
-/-- Create an empty local context with the given `completedDepth`. -/
-def MapReduceSearchContextLocal.initial (completedDepth : Nat) : MapReduceSearchContextLocal σ κ σₕ asm :=
+/-- Create an empty local context for the frontier currently being processed. -/
+def MapReduceSearchContextLocal.initial
+    (completedDepth currentFrontierDepth : Nat) : MapReduceSearchContextLocal σ κ σₕ asm :=
   ({ log := Std.HashMap.emptyWithCapacity,
      violatingStates := [],
      finished := none,
      completedDepth := completedDepth,
-     currentFrontierDepth := completedDepth + 1,
+     currentFrontierDepth := currentFrontierDepth,
      statesFound := 0,
      actionStatsMap := ActionStatUpdate.empty (κ := κ) }, [])
 
@@ -36,9 +37,9 @@ theorem MapReduceSearchContextMainInvariants.initial [Std.TransOrd σₕ] [Std.L
 theorem MapReduceSearchContextLocalInvariants.initial
   (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th)
   (params : SearchParameters ρ σ)
-  (globalSeen : ShardedTreeSetUSize σₕ) (completedDepth : Nat) :
+  (globalSeen : ShardedTreeSetUSize σₕ) (completedDepth currentFrontierDepth : Nat) :
   MapReduceSearchContextLocalInvariants sys params globalSeen (fun _ => False)
-    (MapReduceSearchContextLocal.initial (fp := fp) completedDepth) := by
+    (MapReduceSearchContextLocal.initial (fp := fp) completedDepth currentFrontierDepth) := by
   simp [MapReduceSearchContextLocal.initial]
   constructor ; on_goal 1=> constructor
   all_goals (try solve | intros ; grind)

Veil/Core/Tools/ModelChecker/Concrete/Sequential.lean

@@ -54,7 +54,11 @@ def SequentialSearchContext.processState
   (newFrontierDepth : Nat) :
   SequentialSearchContext σ κ σₕ asm :=
   let (ctx, sq) := sctx
-  let (ctx', outcomesOpt) := ctx.processState params th fpSt curr outcomes
+  let ctxAtDepth := { ctx with
+    completedDepth := newCompletedDepth
+    currentFrontierDepth := newFrontierDepth
+  }
+  let (ctx', outcomesOpt) := ctxAtDepth.processState params th fpSt curr outcomes
   match outcomesOpt with
   | none =>
     -- Early termination case: processState returned none, meaning we're terminating early
@@ -167,24 +171,26 @@ theorem SequentialSearchContext.bfsStep_preserves_invs
   rw [tmp] ; clear tmp
   -- now process the state
   dsimp [SequentialSearchContext.processState]
-  fun_cases BaseSearchContext.processState params th fpSt curr (sys.tr th curr) ctx
-  rename_i succs exns h_eq_part hasSuccessfulTransition completedDepth newViolations
+  fun_cases BaseSearchContext.processState params th fpSt curr (sys.tr th curr)
+    { ctx with completedDepth := newCompleteDepth, currentFrontierDepth := newFrontierDepth }
+  rename_i succs exns h_eq_part hasSuccessfulTransition completedDepth currentStateDepth newViolations
     earlyTermination h_eq_checkvio ctx' ctx''
-  subst completedDepth ; dsimp only
-  revert h_eq_checkvio ; fun_cases checkViolationsAndMaybeTerminate params th fpSt curr ctx.completedDepth hasSuccessfulTransition exns
+  subst completedDepth currentStateDepth
+  revert h_eq_checkvio ; fun_cases checkViolationsAndMaybeTerminate params th fpSt curr
+    newCompleteDepth newFrontierDepth hasSuccessfulTransition exns
   rename_i safetyViolations safetyViolation deadlock tmp1 tmp2
   intro htmp ; injection htmp with h_eq_newvio h_eq_earlyterm ; subst tmp1 tmp2
   -- see if early termination happened
   rcases earlyTermination with _ | earlyTermination
   on_goal 2=>
     -- early termination case
-    subst ctx' ctx'' ; dsimp
+    subst ctx' ctx''
     cases earlyTermination
     all_goals (try solve
       | dsimp
         constructor ; on_goal 1=> constructor
         all_goals dsimp only at * ; (try solve | assumption | grind))
-  subst ctx' ctx'' ; dsimp ; rw [h_not_finished]
+  subst ctx' ctx'' ; rw [h_not_finished]
   -- normal case, in transit
   apply SequentialSearchContextInvariants.finish_stateInTransit (curr := curr)
   · apply SequentialSearchContext.processSuccessors_preserves_invs

VeilTest/Regression/ModelCheckDepthBound.lean

@@ -0,0 +1,72 @@
+import Veil.Core.Tools.ModelChecker.Concrete.Checker
+
+open Veil Veil.ModelChecker Veil.ModelChecker.Concrete
+
+private def chainSystem :
+    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 []
+}
+
+private def searchParameters (maxDepth : Nat) : SearchParameters Unit Nat := {
+  invariants := [{ name := `belowFour, property := fun _ st => st < 4 }]
+  earlyTerminationConditions := [
+    .foundViolatingState,
+    .assertionFailed,
+    .deadlockOccurred,
+    .reachedDepthBound maxDepth
+  ]
+}
+
+private def checkDepthBound
+    (parallelCfg : Option ParallelConfig)
+    (maxDepth : Nat)
+    (expectViolation : Bool) : IO Unit := do
+  let token ← IO.CancelToken.new
+  let result ← findReachable (asm := ActionStatsMap Nat)
+    chainSystem (searchParameters maxDepth) parallelCfg 999999 token
+  match expectViolation, result with
+  | false, .noViolationFound _ (.earlyTermination (.reachedDepthBound bound)) =>
+    unless bound == maxDepth do
+      throw <| IO.userError s!"reported depth bound {bound}, expected {maxDepth}"
+  | true, .foundViolation _ (.safetyFailure [`belowFour]) (some trace) =>
+    unless trace.steps.size == 4 do
+      throw <| IO.userError s!"violation trace has {trace.steps.size} steps, expected 4"
+  | _, _ =>
+    throw <| IO.userError s!"unexpected model-checking result: {repr result}"
+
+private def initialViolationParameters : SearchParameters Unit Nat := {
+  invariants := [{ name := `initialIsPositive, property := fun _ st => st > 0 }]
+  earlyTerminationConditions := [
+    .foundViolatingState,
+    .assertionFailed,
+    .deadlockOccurred,
+    .reachedDepthBound 0
+  ]
+}
+
+private def checkInitialViolation (parallelCfg : Option ParallelConfig) : IO Unit := do
+  let token ← IO.CancelToken.new
+  let result ← findReachable (asm := ActionStatsMap Nat)
+    chainSystem initialViolationParameters parallelCfg 999999 token
+  match result with
+  | .foundViolation _ (.safetyFailure [`initialIsPositive]) (some trace) =>
+    unless trace.steps.isEmpty do
+      throw <| IO.userError s!"initial-state violation trace has {trace.steps.size} steps, expected 0"
+  | _ =>
+    throw <| IO.userError s!"expected a depth-0 initial-state violation, got: {repr result}"
+
+#eval checkDepthBound none 3 false
+#eval checkDepthBound none 4 true
+#eval checkInitialViolation none
+
+private def parallelConfig : ParallelConfig := {
+  numSubTasks := 2
+  thresholdToParallel := 1
+  numSubSteps := 1
+}
+
+#eval checkDepthBound (some parallelConfig) 3 false
+#eval checkDepthBound (some parallelConfig) 4 true
+#eval checkInitialViolation (some parallelConfig)