feat: add #simulate command

Examples/Simulate/CheckpointLeaseFailover.lean

@@ -0,0 +1,93 @@
+import Veil
+
+/-
+Original source/reference:
+- Local modeling analogues:
+  - Examples/Ivy/DecentralizedLock.lean (epoched authority transfer)
+  - Examples/TLA/Raft.lean (leader failover)
+- Production inspiration: etcd lease checkpoint persistence across leader
+  failover (etcd-io/etcd#13508)
+
+Bug/race shape:
+A leader checkpoints a lease's reduced remaining TTL. After failover, the new
+leader forgets that checkpointed TTL and reconstructs the lease from the older
+grant state, reviving a lease that should already be considered expired.
+
+Why #simulate here:
+The violating trace is short, but exhaustive search must branch over leaders,
+leases, epochs, and recovery schedules.
+-/
+
+veil module CheckpointLeaseFailover
+
+type node
+type epoch
+type lease
+
+instantiate epochOrd : TotalOrder epoch
+
+individual leader : node
+immutable individual initial_leader : node
+immutable individual initial_epoch : epoch
+relation current_epoch (e : epoch)
+relation granted_until (l : lease) (e : epoch)
+relation checkpointed_until (l : lease) (e : epoch)
+relation active_on_leader (l : lease)
+
+#gen_state
+
+after_init {
+  leader := initial_leader
+  current_epoch E := E == initial_epoch
+  granted_until L E := false
+  checkpointed_until L E := false
+  active_on_leader L := false
+}
+
+action grantLease (l : lease) (expiry : epoch) {
+  require ∀ now, current_epoch now -> ¬ epochOrd.le expiry now
+  granted_until l E := E == expiry
+  active_on_leader l := true
+}
+
+action checkpointRemainingTTL (l : lease) (expiry : epoch) {
+  require active_on_leader l
+  require ∀ now, current_epoch now -> ¬ epochOrd.le expiry now
+  checkpointed_until l E := E == expiry
+}
+
+action failover (newLeader : node) (newEpoch : epoch) {
+  require newLeader != leader
+  require ∀ oldEpoch, current_epoch oldEpoch -> ¬ epochOrd.le newEpoch oldEpoch
+  leader := newLeader
+  current_epoch E := E == newEpoch
+  active_on_leader L := false
+}
+
+action recoverLeaseFromGrant (l : lease) (expiry : epoch) {
+  require granted_until l expiry
+  active_on_leader l := true
+}
+
+invariant [one_current_epoch]
+  ∀ (e1 e2 : epoch), current_epoch e1 ∧ current_epoch e2 -> e1 = e2
+
+safety [checkpointed_expiry_respected]
+  ∀ (l : lease) (expiry now : epoch),
+    checkpointed_until l expiry ∧ current_epoch now ∧ epochOrd.le expiry now ->
+      ¬ active_on_leader l
+
+#gen_spec
+
+-- model_check must branch over failovers, recovery choices, and many lease/epoch combinations.
+-- set_option veil.violationIsError false in
+-- #model_check { node := Fin 12, epoch := Fin 8, lease := Fin 8 }
+--   { initial_leader := (0 : Fin 12), initial_epoch := (0 : Fin 8) }
+
+-- simulate quickly finds the stale-recovery bug after failover.
+set_option veil.violationIsError false in
+#simulate { node := Fin 12, epoch := Fin 8, lease := Fin 8 }
+  { initial_leader := (0 : Fin 12), initial_epoch := (0 : Fin 8) }
+  (seed := 23) (maxTraces := 2000) (maxSteps := 10)
+
+end CheckpointLeaseFailover

Examples/Simulate/LeaseKeepaliveRace.lean

@@ -0,0 +1,85 @@
+import Veil
+
+/-
+Original source/reference:
+- Closest local modeling analogue: Examples/Ivy/DecentralizedLock.lean
+- Production reference: etcd KeepAlive vs lease-expiry revocation race
+  (etcd-io/etcd#21389, issue #14758)
+
+Bug/race shape:
+A client still has keys attached to a lease when revocation starts. A late
+keepalive succeeds after revocation has already removed the keys, so the client
+appears renewed even though its data is gone.
+
+Why #simulate here:
+The bad trace is only a handful of steps, but exhaustive search must branch over
+clients, keys, revoke timing, and keepalive interleavings.
+-/
+
+veil module LeaseKeepaliveRace
+
+type client
+type key
+
+relation lease_alive (c : client)
+relation revoke_started (c : client)
+relation keepalive_succeeded (c : client)
+relation key_attached (c : client) (k : key)
+relation key_present (k : key)
+
+#gen_state
+
+after_init {
+  lease_alive C := false
+  revoke_started C := false
+  keepalive_succeeded C := false
+  key_attached C K := false
+  key_present K := false
+}
+
+action grantLease (c : client) {
+  require !(lease_alive c)
+  lease_alive c := true
+  revoke_started c := false
+  keepalive_succeeded c := false
+}
+
+action attachKey (c : client) (k : key) {
+  require lease_alive c
+  key_attached c k := true
+  key_present k := true
+}
+
+action startRevoke (c : client) {
+  require lease_alive c
+  revoke_started c := true
+  lease_alive c := false
+}
+
+action deleteKey (c : client) (k : key) {
+  require revoke_started c
+  require key_attached c k
+  key_present k := false
+}
+
+action keepAlive (c : client) {
+  require revoke_started c
+  keepalive_succeeded c := true
+  lease_alive c := true
+}
+
+safety [renewal_keeps_keys_live]
+  ∀ (c : client) (k : key), keepalive_succeeded c ∧ key_attached c k -> key_present k
+
+#gen_spec
+
+-- model_check must branch over clients, keys, revoke order, and late keepalives.
+-- set_option veil.violationIsError false in
+-- #model_check { client := Fin 8, key := Fin 8 } {}
+
+-- simulate usually hits the keepalive-after-revoke race in a short trace.
+set_option veil.violationIsError false in
+#simulate { client := Fin 8, key := Fin 8 } {}
+  (seed := 11) (maxTraces := 300) (maxSteps := 12)
+
+end LeaseKeepaliveRace

Examples/Simulate/ReliableBroadcast.lean

@@ -0,0 +1,73 @@
+import Veil
+
+/-
+Original source/reference:
+- Local analogue: Examples/Ivy/ReliableBroadcast.lean
+- External family reference: tlaplus/Examples/specifications/bcastByz/bcastByz.tla
+
+Bug/race shape:
+This simulate-focused variant keeps the initial/echo/vote/deliver structure, but
+intentionally uses weak quorum rules. An equivocating originator can get two
+different values delivered by different receivers.
+
+Why #simulate here:
+The violating trace is short, but exhaustive search must branch over broadcast,
+echo, vote, and delivery orderings across many nodes and values.
+-/
+
+veil module ReliableBroadcastSim
+
+type node
+type value
+
+immutable individual originator : node
+
+relation initial_msg (src : node) (dst : node) (v : value)
+relation echo_msg (src : node) (dst : node) (v : value)
+relation vote_msg (src : node) (dst : node) (v : value)
+relation delivered (dst : node) (v : value)
+
+#gen_state
+
+after_init {
+  initial_msg S D V := false
+  echo_msg S D V := false
+  vote_msg S D V := false
+  delivered D V := false
+}
+
+action initialSend (dst : node) (v : value) {
+  require ∀ V, !(initial_msg originator dst V)
+  initial_msg originator dst v := true
+}
+
+action echo (src : node) (v : value) {
+  require initial_msg originator src v
+  echo_msg src D v := true
+}
+
+action vote (observer : node) (v : value) {
+  require ∃ (n1 n2 : node), n1 != n2 ∧ echo_msg n1 observer v ∧ echo_msg n2 observer v
+  vote_msg observer D v := true
+}
+
+action deliver (observer : node) (v : value) {
+  require ∃ (n1 n2 : node), n1 != n2 ∧ vote_msg n1 observer v ∧ vote_msg n2 observer v
+  delivered observer v := true
+}
+
+safety [agreement]
+  ∀ (n1 n2 : node) (v1 v2 : value), delivered n1 v1 ∧ delivered n2 v2 -> v1 = v2
+
+#gen_spec
+
+-- model_check must enumerate many broadcast, echo, vote, and delivery schedules.
+-- set_option veil.violationIsError false in
+-- #model_check { node := Fin 10, value := Fin 2 } { originator := (0 : Fin 10) }
+
+-- simulate quickly finds an equivocation trace with the weak quorum rules above.
+set_option veil.violationIsError false in
+#simulate { node := Fin 10, value := Fin 2 } { originator := (0 : Fin 10) }
+  (seed := 41) (maxTraces := 2000) (maxSteps := 24)
+
+end ReliableBroadcastSim

Examples/TLA/MutexViolation.lean

@@ -345,8 +345,8 @@ termination [AllDone] ∀s ≠ NONE, pc s Done = true
 #time #gen_spec
 -- NOTE: comment out the line containing `BUG:` to fix the violation
 
--- set_option veil.violationIsError false in
 /- `Fin n` means `n-1` valid threads.-/
+set_option veil.violationIsError false in
 #model_check { process := Fin 10 } { NONE := 0 }
 
 end MutexViolation

Veil/Base.lean

@@ -97,4 +97,14 @@ register_option veil.smt.timeout : Nat := {
   descr := "Timeout for the SMT solver in seconds. Default is 60 seconds."
 }
 
+register_option veil.simulate.maxTraces : Nat := {
+  defValue := 10000
+  descr := "Maximum number of traces to generate during simulation. Default is 10000."
+}
+
+register_option veil.simulate.maxSteps : Nat := {
+  defValue := 100
+  descr := "Maximum number of steps per trace during simulation. Default is 100 (same as TLC)."
+}
+
 end Veil

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

@@ -111,6 +111,8 @@ def findReachable {ρ σ κ : Type} {m : Type → Type}
   | some (.earlyTermination (.reachedDepthBound _)) =>
     -- No violation found within depth bound; report number of states explored
     return ModelCheckingResult.noViolationFound distinctCount (.earlyTermination (.reachedDepthBound ctx.completedDepth))
+  | some (.earlyTermination (.reachedTraceLimit maxTraces)) =>
+    return ModelCheckingResult.noViolationFound distinctCount (.earlyTermination (.reachedTraceLimit maxTraces))
   | some (.earlyTermination .cancelled) =>
     -- Search was cancelled by the user
     return ModelCheckingResult.cancelled

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

@@ -236,6 +236,7 @@ def checkViolationsAndMaybeTerminate
   let earlyTermination := params.earlyTerminationConditions.findSome? fun
     | .foundViolatingState => if safetyViolation then some (.foundViolatingState fpSt safetyViolations) else none
     | .reachedDepthBound bound => if completedDepth >= bound then some (.reachedDepthBound bound) else none
+    | .reachedTraceLimit _ => none
     | .deadlockOccurred => if deadlock then some (.deadlockOccurred fpSt) else none
     | .assertionFailed => assertionFailures.head?.map fun (exId, _) => .assertionFailed fpSt exId
     | .cancelled => none  -- Cancellation is handled externally via cancel token, not through early termination conditions
@@ -258,6 +259,7 @@ def BaseSearchContext.processState
       match x with
       | .foundViolatingState fp violations => {ctx with finished := some (.earlyTermination (.foundViolatingState fp violations))}
       | .reachedDepthBound bound => {ctx with finished := some (.earlyTermination (.reachedDepthBound bound))}
+      | .reachedTraceLimit maxTraces => {ctx with finished := some (.earlyTermination (.reachedTraceLimit maxTraces))}
       | .deadlockOccurred fp => {ctx with finished := some (.earlyTermination (.deadlockOccurred fp))}
       | .assertionFailed fp exId => {ctx with finished := some (.earlyTermination (.assertionFailed fp exId))}
       | .cancelled => {ctx with finished := some (.earlyTermination .cancelled)}

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

@@ -82,6 +82,14 @@ structure Progress where
   allActionLabels : List String := []
   /-- Time-series history for charting progress over time -/
   history : Array ProgressHistoryPoint := #[]
+  /-- Whether this progress entry is for `#simulate` rather than `#model_check`. -/
+  isSimulation : Bool := false
+  /-- Number of traces completed so far (simulation only). -/
+  tracesRun : Nat := 0
+  /-- Configured maximum trace budget (simulation only). -/
+  maxTraces : Nat := 0
+  /-- Depth reached in the current/last trace (simulation only). -/
+  simulationDepth : Nat := 0
   deriving ToJson, FromJson, Inhabited, Repr
 
 /-- Refs for tracking progress of a single model checker instance. -/
@@ -90,6 +98,8 @@ structure ProgressRefs where
   resultRef : IO.Ref (Option Lean.Json)
   /-- Cancellation token for this instance. -/
   cancelToken : IO.CancelToken
+  /-- Cancellation token for background compilation, when default handoff is active. -/
+  compilationCancelTokenRef : IO.Ref (Option IO.CancelToken)
   /-- Set by compilation task to signal interpreted mode to stop for handoff. -/
   handoffRequested : IO.Ref Bool
   /-- Set by interpreted mode when a violation is found (prevents handoff). -/
@@ -125,6 +135,7 @@ def allocProgressInstance (allActionLabels : List String := []) : IO (Nat × IO.
     progressRef := ← IO.mkRef { startTimeMs := ← IO.monoMsNow, status := "Running...", isRunning := true, allActionLabels }
     resultRef := ← IO.mkRef none
     cancelToken := cancelTk
+    compilationCancelTokenRef := ← IO.mkRef none
     handoffRequested := ← IO.mkRef false
     violationFound := ← IO.mkRef false
   }
@@ -174,6 +185,33 @@ def updateStatus (instanceId : Nat) (status : String) : IO Unit := withRefs inst
   let now ← IO.monoMsNow
   refs.progressRef.modify fun p => { p with status, elapsedMs := now - p.startTimeMs }
 
+/-- Update progress for a simulation run. -/
+def updateSimulationProgress (instanceId : Nat) (status : String)
+    (tracesRun maxTraces depth : Nat) : IO Unit := do
+  let now ← IO.monoMsNow
+  if let some refs ← getProgressRefs instanceId then
+    refs.progressRef.modify fun p =>
+      { p with
+        status
+        elapsedMs := now - p.startTimeMs
+        isSimulation := true
+        tracesRun
+        maxTraces
+        simulationDepth := depth }
+  if ← compiledModeEnabled.get then
+    let startTime ← compiledModeStartTime.get
+    let p : Progress := {
+      status := status
+      isRunning := true
+      startTimeMs := startTime
+      elapsedMs := now - startTime
+      isSimulation := true
+      tracesRun := tracesRun
+      maxTraces := maxTraces
+      simulationDepth := depth
+    }
+    IO.eprintln (toJson p).compress
+
 /-- Mark progress as complete for a given instance ID. -/
 def finishProgress (instanceId : Nat) (resultJson : Lean.Json) : IO Unit := withRefs instanceId fun refs => do
   let now ← IO.monoMsNow
@@ -199,7 +237,15 @@ def isCancelled (instanceId : Nat) : IO Bool := do
   | none => return false
 
 /-- Request cancellation for an instance. -/
-def requestCancellation (instanceId : Nat) : IO Unit := withRefs instanceId (·.cancelToken.set)
+def requestCancellation (instanceId : Nat) : IO Unit := withRefs instanceId fun refs => do
+  refs.cancelToken.set
+  let compilationCancelToken? ← refs.compilationCancelTokenRef.get
+  if let some compilationCancelToken := compilationCancelToken? then
+    compilationCancelToken.set
+
+/-- Register or clear the background compilation cancellation token for an instance. -/
+def setCompilationCancelToken (instanceId : Nat) (cancelToken? : Option IO.CancelToken) : IO Unit :=
+  withRefs instanceId fun refs => refs.compilationCancelTokenRef.set cancelToken?
 
 /-- Mark progress as cancelled for a given instance ID. -/
 def cancelProgress (instanceId : Nat) : IO Unit := withRefs instanceId fun refs => do

Veil/Core/Tools/ModelChecker/ExecutionOutcome.lean

@@ -21,7 +21,7 @@ inductive ExecutionOutcome (ε σ : Type) where
   | assertionFailure (error : ε) (state : σ)
   /-- The action diverged (did not terminate). -/
   | divergence
-deriving Repr, BEq, Inhabited
+deriving Repr, BEq, DecidableEq, Inhabited
 
 namespace ExecutionOutcome