Retry timed-out SMT queries with perturbed seeds; report slowest VCs

Veil/Base.lean

@@ -142,6 +142,58 @@ register_option veil.smt.timeout : Nat := {
   descr := "Timeout for the SMT solver in seconds. Default is 60 seconds."
 }
 
+register_option veil.smt.seed : Nat := {
+  defValue := 0
+  descr := "Random seed for the SMT solver (cvc5 `seed` and `sat-random-seed`). \
+  0 (the default) leaves the solver's own default seed in place; any other \
+  value is passed through. Retry attempts (`veil.smt.retries`) perturb this \
+  to escape seed-dependent e-matching divergence."
+}
+
+register_option veil.smt.retries : Nat := {
+  defValue := 1
+  descr := "How many times to re-dispatch a VC whose SMT query timed out, \
+  before reporting ⏱. Each retry uses a fresh random seed (`veil.smt.seed` = \
+  attempt index) and a budget of `veil.smt.retryTimeout` seconds. Retries \
+  only fire after a *timeout* (not after `sat`, genuine `unknown`, or \
+  errors) and are reported distinctly in the summary so flakiness stays \
+  visible. Set to 0 to disable. Must be set before `#gen_spec`."
+}
+
+register_option veil.smt.retryTimeout : Nat := {
+  defValue := 120
+  descr := "Timeout (in seconds) for retry attempts (see `veil.smt.retries`). \
+  Timeout-then-fast-success is a seed artifact: such queries either finish \
+  quickly under a fresh seed or never, so a short budget avoids burning \
+  another full `veil.smt.timeout` on genuinely divergent queries. \
+  Must be set before `#gen_spec`."
+}
+
+register_option veil.report.slowVCs : Nat := {
+  defValue := 10
+  descr := "Number of slowest verification conditions to list at the end of \
+  `#check_invariants` (ranked by individual discharger time, including failed \
+  attempts, which burn the full timeout). Set to 0 to disable the report."
+}
+
+register_option veil.report.slowVCsMinMs : Nat := {
+  defValue := 5000
+  descr := "Minimum discharge time (in milliseconds) for an attempt to appear \
+  in the slowest-VCs report; when no attempt qualifies, the report is \
+  omitted entirely. The default floor keeps `#check_invariants` output \
+  deterministic for fast specifications (e.g. under `#guard_msgs` in tests) \
+  while still surfacing the tail on long-running sweeps. Lower it to \
+  investigate moderately slow VCs."
+}
+
+register_option veil.report.nearTimeoutPercent : Nat := {
+  defValue := 50
+  descr := "In the slowest-VCs report, flag a discharge attempt as \
+  near-timeout (⚠️) when its time exceeds this percentage of \
+  `veil.smt.timeout`. Near-timeout VCs are divergence candidates: a small \
+  model change (e.g. one added invariant) may push them past the timeout."
+}
+
 register_option veil.experimental.wpCompact : Bool := {
   defValue := true
   descr := "Experimental. If true, compact generated `wp_local_eq.pred` definitions by sharing duplicated postcondition branches with `letEq` and exposing abstract-state conditionals field-wise."

Veil/Core/Tools/Verifier/Manager.lean

@@ -96,6 +96,19 @@ def DischargerResult.kindString (res : DischargerResult ResultT) : String :=
   | .unknown _ _ => "unknown"
   | .error _ _ => "error"
 
+/-- Whether this result represents a solver timeout. Timeouts surface as
+exceptions whose message carries the solver's TIMEOUT marker; this is the same
+classification `exhaustedVCStatus` uses to report `VCStatus.timeout` (⏱), and
+`nextDischarger?` uses it to decide whether retry attempts should fire. -/
+def DischargerResult.isTimeout (res : DischargerResult ResultT) : Bool :=
+  match res with
+  | .error exs _ =>
+    exs.any fun (_, json) =>
+      match json with
+      | .str s => unknownExplanation? s == some .timeout
+      | _ => false
+  | _ => false
+
 instance [ToString ResultT] : ToString (DischargerResult ResultT) where
   toString res :=
     match res with
@@ -134,6 +147,11 @@ structure Discharger (ResultT : Type) where
   /-- Whether this discharger comes from an explicitly tagged interactive proof
   theorem rather than automatic tooling. -/
   isInteractive : Bool := false
+  /-- Attempt index for automatic retry (`veil.smt.retries`). 0 is the primary
+  attempt; attempts > 0 are seed-perturbed retries, which `nextDischarger?`
+  only schedules after an earlier attempt of the same VC *timed out* (they are
+  skipped after `sat`, genuine `unknown`, or non-timeout errors). -/
+  attempt : Nat := 0
   /-- Optionally, a VC discharger can provide term (e.g. a proof script) that
   can be shown to the user, e.g. when a VC's corresponding `theorem` is
   pretty-printed. -/
@@ -469,22 +487,35 @@ def Discharger.startTime (discharger : Discharger ResultT) : BaseIO (Option Nat)
     return none
 
 /-- Find the next discharger to try. Once this function returns `none`, it will
-not return `some` again unless new dischargers are added. -/
+not return `some` again unless new dischargers are added.
+
+Retry attempts (`Discharger.attempt > 0`) are only scheduled when an earlier
+attempt of this VC timed out; after `sat`, genuine `unknown`, or non-timeout
+errors they are skipped permanently (they stay `notStarted`, contributing
+nothing to the VC's aggregate status). -/
 def VerificationCondition.nextDischarger? (vc : VerificationCondition VCMetaT ResultT) : BaseIO (Option (Discharger ResultT)) := do
   match vc.successful with
   | some _ => return .none
   | none =>
     if vc.hasInteractiveDischarger then
       return none
+    let mut sawTimeout := false
     for discharger in vc.dischargers do
       match ← discharger.status with
-      | .notStarted => return some discharger
+      | .notStarted =>
+        if discharger.attempt > 0 && !sawTimeout then
+          continue
+        return some discharger
       -- if the discharger is still running, wait for it to finish
       | .running => return none
       -- if the discharger is finished the VC is proven or disproven, we're done
       | .finished (.proven _ _ _)  | .finished (.disproven _ _) => return none
-      | .finished (.unknown _ _) => continue
-      | .finished (.error _ _) => continue
+      | .finished res@(.unknown _ _) =>
+        sawTimeout := sawTimeout || res.isTimeout
+        continue
+      | .finished res@(.error _ _) =>
+        sawTimeout := sawTimeout || res.isTimeout
+        continue
     return none
 
 def VCManager.readyTasks (mgr : VCManager VCMetaT ResultT)
@@ -510,15 +541,6 @@ def VCManager.cancelAllDischargers (mgr : VCManager VCMetaT ResultT) : BaseIO Un
     for discharger in vc.dischargers do
       discharger.cancelTk.set
 
-private def dischargerErrorIsTimeout (res : DischargerResult ResultT) : Bool :=
-  match res with
-  | .error exs _ =>
-    exs.any fun (_, json) =>
-      match json with
-      | .str s => unknownExplanation? s == some .timeout
-      | _ => false
-  | _ => false
-
 /-- Compute the final status for a VC whose dischargers have been exhausted.
 Concrete outcomes take priority, and among failures a non-timeout `error`
 outranks `unknown`; we only report `timeout` when every recorded error was a
@@ -538,7 +560,7 @@ private def VCManager.exhaustedVCStatus (mgr : VCManager VCMetaT ResultT)
           | .disproven _ _ => (true, hasUnknown, hasError, allErrorsAreTimeout)
           | .unknown _ _ => (hasDisproven, true, hasError, allErrorsAreTimeout)
           | .error _ _ =>
-            (hasDisproven, hasUnknown, true, allErrorsAreTimeout && dischargerErrorIsTimeout result)
+            (hasDisproven, hasUnknown, true, allErrorsAreTimeout && result.isTimeout)
           | .proven _ _ _ => (hasDisproven, hasUnknown, hasError, allErrorsAreTimeout)
     if hasDisproven then
       .disproven

Veil/Core/Tools/Verifier/Results.lean

@@ -38,6 +38,9 @@ structure DischargerResultData (ResultT : Type) where
   name : Name
   /-- True iff this result comes from a theorem tagged with `@[veil]`. -/
   isInteractive : Bool := false
+  /-- Attempt index (see `Discharger.attempt`): 0 is the primary attempt,
+  attempts > 0 are seed-perturbed retries after a timeout. -/
+  attempt : Nat := 0
   /-- The status of the discharger. -/
   status : DischargeStatus ResultT
   /-- The time taken by the discharger (in milliseconds), if available. -/
@@ -58,6 +61,7 @@ instance [ToJson ResultT] : ToJson (DischargerResultData ResultT) where
       ("id", toJson data.id),
       ("name", toJson data.name.toString),
       ("isInteractive", toJson data.isInteractive),
+      ("attempt", toJson data.attempt),
       ("status", Json.str statusStr),
       ("time", match time.orElse (fun _ => data.time) with | some t => toJson t | none => Json.null),
       ("startTime", match data.startTime with | some t => toJson t | none => Json.null),
@@ -169,6 +173,7 @@ def mkDischargerResultData [Monad m] [MonadError m] [MonadLiftT BaseIO m] (mgr :
     id := dischargerId
     name := discharger.id.name
     isInteractive := discharger.isInteractive
+    attempt := discharger.attempt
     status := status
     time := time
     startTime := startTime

Veil/Core/UI/Verifier/VerificationResults.lean

@@ -342,6 +342,62 @@ private def formatFailureDiagnostics (status : Option VCStatus)
       (collectDiagnostics dischargerUnknownReasons vc allVCs)
   | some .proven | some .disproven | none => none
 
+private def formatMs (ms : Nat) : String :=
+  s!"{ms / 1000}.{ms % 1000 / 100} s"
+
+/-- If this cell (primary VC or an active alternative) was proven by a retry
+attempt, the attempt index. Retried successes are reported distinctly (see
+`veil.smt.retries`) so seed-flakiness stays visible instead of being hidden
+by the retry. -/
+private def provenOnRetry? (vc : VCResult VCMetadata SmtResult)
+    (allVCs : Array (VCResult VCMetadata SmtResult)) : Option Nat := Id.run do
+  for relatedVC in activeRelatedVCs vc allVCs do
+    if let some successId := relatedVC.timing.successfulDischargerId then
+      if let some d := relatedVC.timing.dischargers.find? (·.id == successId) then
+        if d.attempt > 0 then
+          return some d.attempt
+  return none
+
+private def retryNote (vc : VCResult VCMetadata SmtResult)
+    (allVCs : Array (VCResult VCMetadata SmtResult)) : String :=
+  match provenOnRetry? vc allVCs with
+  | some k => s!" (retry {k}, seed {k})"
+  | none => ""
+
+/-- The slowest discharge attempts across all non-dormant induction VCs
+(`veil.report.slowVCs` entries, 0 disables). Failed attempts are included:
+they burn the full timeout and are exactly the tail that dominates sweep wall
+time. Only attempts taking at least `veil.report.slowVCsMinMs` are reported
+(none qualifying ⇒ no report), keeping the output deterministic for fast
+specifications. Attempts above `veil.report.nearTimeoutPercent` of
+`veil.smt.timeout` are flagged as near-timeout (the flag compares against
+the timeout option as set at reporting time). -/
+private def formatSlowVCsReport [Monad m] [MonadOptions m]
+    (results : VerificationResults VCMetadata SmtResult) : m (Option MessageData) := do
+  let opts ← getOptions
+  let topN := veil.report.slowVCs.get opts
+  if topN == 0 then return none
+  let minMs := veil.report.slowVCsMinMs.get opts
+  let timeoutMs := veil.smt.timeout.get opts * 1000
+  let nearTimeoutMs := timeoutMs * veil.report.nearTimeoutPercent.get opts / 100
+  let mut attempts : Array (Name × Nat) := #[]
+  for vc in results.vcs do
+    unless vc.metadata.isInduction && !vc.isDormant do continue
+    for d in vc.timing.dischargers do
+      if let .finished res := d.status then
+        if res.time ≥ minMs then
+          attempts := attempts.push (d.name, res.time)
+  if attempts.isEmpty then return none
+  let slowest := attempts.qsort (fun a b => a.2 > b.2) |>.take topN
+  let mut msg := m!"Slowest discharge attempts \
+    (≥ {formatMs minMs}; top {slowest.size} of {attempts.size}):\n"
+  for (name, time) in slowest do
+    let flag := if timeoutMs > 0 && time ≥ nearTimeoutMs then
+      s!" ⚠️ near timeout ({time * 100 / timeoutMs}% of {formatMs timeoutMs})"
+    else ""
+    msg := msg ++ m!"  {formatMs time}  {name}{flag}\n"
+  return some msg
+
 /-- Format verification results as text output for logging. -/
 def formatVerificationResults [Monad m] [MonadOptions m](results : VerificationResults VCMetadata SmtResult) : m MessageData := do
   let includeCounterexamples := veil.printCounterexamples.get (← getOptions)
@@ -360,7 +416,7 @@ def formatVerificationResults [Monad m] [MonadOptions m](results : VerificationR
     for vc in initVCs do
       let .induction m := vc.metadata | continue
       let status := effectiveStatus vc results.vcs
-      msg := msg ++ m!"  {m.property} ... {statusEmoji status}\n"
+      msg := msg ++ m!"  {m.property} ... {statusEmoji status}{retryNote vc results.vcs}\n"
       if includeCounterexamples && status == some .disproven then
         if let some ceMsg := formatCounterexamples vc results.vcs then
           msg := msg ++ ceMsg
@@ -373,12 +429,14 @@ def formatVerificationResults [Monad m] [MonadOptions m](results : VerificationR
       for vc in vcs do
         let .induction m := vc.metadata | continue
         let status := effectiveStatus vc results.vcs
-        msg := msg ++ m!"    {m.property} ... {statusEmoji status}\n"
+        msg := msg ++ m!"    {m.property} ... {statusEmoji status}{retryNote vc results.vcs}\n"
         if includeCounterexamples && status == some .disproven then
           if let some ceMsg := formatCounterexamples vc results.vcs then
             msg := msg ++ ceMsg
         if let some diagnosticMsg := formatFailureDiagnostics status vc results.vcs then
           msg := msg ++ diagnosticMsg
+  if let some slowMsg ← formatSlowVCsReport results then
+    msg := msg ++ slowMsg
   return msg
 
 /-- Check if any VCs have non-proven status. -/

Veil/Frontend/DSL/Module/VCGen/Induction.lean

@@ -67,10 +67,17 @@ private def mkDischargerResult [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT
 
 /-! ## VC Discharger -/
 
-/-- Create a discharger for inductive verification conditions. -/
+/-- Create a discharger for inductive verification conditions.
+
+`attempt > 0` marks a retry discharger (see `veil.smt.retries`): the manager
+only schedules it after an earlier attempt of the same VC timed out
+(`VerificationCondition.nextDischarger?`). The perturbed solver configuration
+is expected to be baked into `term` itself (via `set_option ... in`), so
+witness regeneration replays it unchanged. -/
 def VCDischarger.fromTerm (term : Term) (actName : Name) (vcStatement : VCStatement)
     (dischargerId : DischargerIdentifier)
     (nameSuffix : String := "")
+    (attempt : Nat := 0)
     (ch : Std.Channel (ManagerNotification VCMetadata SmtResult))
     (_cancelTk? : Option IO.CancelToken := none) : CommandElabM (Discharger SmtResult) := do
   let dischargerId :=
@@ -119,6 +126,7 @@ def VCDischarger.fromTerm (term : Term) (actName : Name) (vcStatement : VCStatem
   let mkTask := (mk vcStatement).asTask
   return {
     id := dischargerId,
+    attempt := attempt,
     term := term,
     cancelTk := cancelTk,
     task := Option.none,
@@ -259,11 +267,40 @@ private def Module.actsToCheck (mod : Module) : Array ProcedureSpecification :=
     | .action _ _ | .initializer => true
     | .procedure _ => false)
 
+/-- Retry variants of a discharge tactic, per `veil.smt.retries`: attempt `k`
+re-runs `tac` with the solver seed set to `k` and the short
+`veil.smt.retryTimeout` budget. The perturbed options are baked into the
+returned `by` term via `set_option ... in`, so lazy witness regeneration
+(`#gen_theorems`) replays exactly the configuration that succeeded. -/
+private def mkRetryTerms [Monad m] [MonadQuotation m] [MonadOptions m]
+    (tac : TSyntax `tactic) : m (Array (Nat × Term)) := do
+  let opts ← getOptions
+  let retryTimeout := Syntax.mkNatLit (veil.smt.retryTimeout.get opts)
+  (Array.range (veil.smt.retries.get opts)).mapM fun i => do
+    let k := i + 1
+    let seed := Syntax.mkNatLit k
+    let term ← `(term| by
+      set_option veil.smt.seed $seed:num in
+      set_option veil.smt.timeout $retryTimeout:num in
+      $tac:tactic)
+    return (k, term)
+
+/-- Add `retryTerms` (from `mkRetryTerms`) as retry dischargers of `vcId`. -/
+private def VCManager.addRetryDischargers
+    (mgr : VCManager VCMetadata SmtResult) (vcId : VCId) (actName : Name)
+    (nameSuffix : String) (retryTerms : Array (Nat × Term))
+    : CommandElabM (VCManager VCMetadata SmtResult) :=
+  retryTerms.foldlM (init := mgr) fun mgr (k, term) =>
+    mgr.mkAddDischarger vcId (VCDischarger.fromTerm term actName
+      (nameSuffix := s!"{nameSuffix}_retry{k}") (attempt := k))
+
 /-- Generate doesNotThrow VCs for all actions.
     These VCs check that actions don't throw exceptions assuming the invariants hold. -/
 def Module.generateDoesNotThrowVCs (mod : Module) : CommandElabM Unit := do
   let actsToCheck := mod.actsToCheck
-  let wpTactic ← `(by veil_solve_wp_doesnotthrow)
+  let wpSolve ← `(tactic| veil_solve_wp_doesnotthrow)
+  let wpTactic ← `(by $wpSolve:tactic)
+  let wpRetries ← mkRetryTerms wpSolve
   -- Prepare VC data outside the lock
   let vcData ← actsToCheck.mapM fun act =>
     return (act, ← mkDoesNotThrowVC mod act.name act.declarationKind InductionVCKind.primary)
@@ -273,14 +310,19 @@ def Module.generateDoesNotThrowVCs (mod : Module) : CommandElabM Unit := do
       let mgr ← ref.get
       let (mgr, vcId) := mgr.addVC vc {} #[]
       let mgr ← mgr.mkAddDischarger vcId (VCDischarger.fromTerm wpTactic act.name (nameSuffix := "_WP"))
+      let mgr ← mgr.addRetryDischargers vcId act.name "_WP" wpRetries
       ref.set mgr
 
 /-- Generate invariant preservation VCs for all actions × invariant clauses.
     These VCs check that each action preserves each invariant clause. -/
 def Module.generateInvariantVCs (mod : Module) : CommandElabM Unit := do
   let actsToCheck := mod.actsToCheck
-  let wpTactic ← if mod._useLocalRPropTC then `(by veil_solve_wp) else `(by veil_solve_wp)
-  let trTactic ← `(by veil_solve_tr)
+  let wpSolve ← `(tactic| veil_solve_wp)
+  let trSolve ← `(tactic| veil_solve_tr)
+  let wpTactic ← `(by $wpSolve:tactic)
+  let trTactic ← `(by $trSolve:tactic)
+  let wpRetries ← mkRetryTerms wpSolve
+  let trRetries ← mkRetryTerms trSolve
   -- Prepare all VC data outside the lock
   let vcData ← actsToCheck.foldlM (init := #[]) fun acc act => do
     let clauseVCs ← mod.checkableInvariants.foldlM (init := #[]) fun acc' invClause => do
@@ -304,15 +346,19 @@ def Module.generateInvariantVCs (mod : Module) : CommandElabM Unit := do
           -- fallback, but it no longer drives the normal path for these actions.
           let (mgr, trVCId) := mgr.addVC trVC {} #[]
           let mgr ← mgr.mkAddDischarger trVCId (VCDischarger.fromTerm trTactic act.name (nameSuffix := "_TR"))
+          let mgr ← mgr.addRetryDischargers trVCId act.name "_TR" trRetries
           let (mgr, wpVCId) := mgr.addAlternativeVC wpVC trVCId #[]
-          mgr.mkAddDischarger wpVCId (VCDischarger.fromTerm wpTactic act.name (nameSuffix := "_WP"))
+          let mgr ← mgr.mkAddDischarger wpVCId (VCDischarger.fromTerm wpTactic act.name (nameSuffix := "_WP"))
+          mgr.addRetryDischargers wpVCId act.name "_WP" wpRetries
         else do
           -- Ordinary actions keep the existing WP-first behavior.  TR remains a
           -- fallback counterexample/proof route if the WP VC fails.
           let (mgr, wpVCId) := mgr.addVC wpVC {} #[]
           let mgr ← mgr.mkAddDischarger wpVCId (VCDischarger.fromTerm wpTactic act.name (nameSuffix := "_WP"))
+          let mgr ← mgr.addRetryDischargers wpVCId act.name "_WP" wpRetries
           let (mgr, trVCId) := mgr.addAlternativeVC trVC wpVCId #[]
-          mgr.mkAddDischarger trVCId (VCDischarger.fromTerm trTactic act.name (nameSuffix := "_TR"))
+          let mgr ← mgr.mkAddDischarger trVCId (VCDischarger.fromTerm trTactic act.name (nameSuffix := "_TR"))
+          mgr.addRetryDischargers trVCId act.name "_TR" trRetries
       ref.set mgr
 
 /-- Generate all VCs (both doesNotThrow and invariant preservation). -/