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

@@ -142,4 +142,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

@@ -91,13 +91,7 @@ def findReachable {ρ σ κ : Type} {m : Type → Type}
     setViolationFound progressInstanceId
     return ModelCheckingResult.foundViolation 0 (.assumptionFailure assumptionViolations) none
   -- Create a "filtered" version of the system
-  let sys := if params.stateConstraints.isEmpty then sys else {
-    initStates := sys.initStates.filter (params.satisfiesConstraints th)
-    tr := fun th' s => (sys.tr th' s).filter (fun (_, o) => match o with
-      | .success s' => params.satisfiesConstraints th s'
-      | .assertionFailure _ s' => params.satisfiesConstraints th s' -- assertion failures should satisfy constraints to be considered
-      | .divergence => true) -- well
-  }
+  let sys := Veil.ModelChecker.restrictSystemByStateConstraints sys params th
   let (ctx, distinctCount) ← match parallelCfg with
     | some cfg => do
       let mctx ← breadthFirstSearchParallel params sys cfg progressInstanceId cancelToken
@@ -115,6 +109,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

@@ -192,16 +192,16 @@ def BaseSearchContext.initial (initialStates : List σ) : BaseSearchContext σ 
 -- achieve zero additional memory allocation here?
 
 /-- Partition a list of `(label × ExecutionOutcome)` pairs into two components:
-a list of successful transitions, and a list of transitions where exceptions
-were raised. The divergence part is discarded. -/
+a list of successful transitions, and a list of labeled transitions where
+exceptions were raised. The divergence part is discarded. -/
 def partitionExecutionOutcome (outcomes : List (κ × ExecutionOutcome Int σ)) :
-  List (κ × σ) × List (Int × σ) :=
+  List (κ × σ) × List (κ × Int × σ) :=
   outcomes.foldr
     (init := ([], []))
     (fun (label, outcome) (succs, exns) =>
       match outcome with
       | .success st => ((label, st) :: succs, exns)
-      | .assertionFailure exId st => (succs, (exId, st) :: exns)
+      | .assertionFailure exId st => (succs, (label, exId, st) :: exns)
       | .divergence => (succs, exns))
 
 theorem partitionExecutionOutcome.fst_spec {κ σ : Type} (outcomes : List (κ × ExecutionOutcome Int σ)) :
@@ -213,16 +213,24 @@ theorem partitionExecutionOutcome.fst_spec {κ σ : Type} (outcomes : List (κ 
   | nil => simp
   | cons x l ih => rcases x with ⟨l, _ | _ | _⟩ <;> grind
 
+theorem partitionExecutionOutcome.snd_spec {κ σ : Type} (outcomes : List (κ × ExecutionOutcome Int σ)) :
+  ∀ (label : κ) (exId : Int) (st : σ),
+    (label, exId, st) ∈ (partitionExecutionOutcome outcomes).snd ↔
+    (label, ExecutionOutcome.assertionFailure exId st) ∈ outcomes := by
+  introv ; unfold partitionExecutionOutcome
+  induction outcomes with
+  | nil => simp
+  | cons x l ih => rcases x with ⟨l, _ | _ | _⟩ <;> grind
+
 -- NOTE: If this function is put inside `BaseSearchContext.checkViolationsAndMaybeTerminate`,
 -- `specialize` of `List.filterMap` may not exhibit
 def checkViolationsAndMaybeTerminate
   (completedDepth : Nat)
   (hasSuccessfulTransition : Bool)
-  (assertionFailures : List (Int × σ)) :
+  (assertionFailures : List (κ × Int × σ)) :
   List (σₕ × ViolationKind) × Option (EarlyTerminationReason σₕ) :=
   -- 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 := violatedInvariantNames params th curr
   let safetyViolation := !safetyViolations.isEmpty
   let deadlock := !hasSuccessfulTransition && !params.terminating.holdsOn th curr
 
@@ -231,13 +239,14 @@ def checkViolationsAndMaybeTerminate
     (if safetyViolation then [(fpSt, .safetyFailure safetyViolations)] else []) ++
     (if deadlock then [(fpSt, .deadlock)] else []) ++
     -- NOTE: This should be further optimized to avoid extra memory allocation
-    (assertionFailures.map fun (exId, _) => (fpSt, .assertionFailure exId))
+    (assertionFailures.map fun (_, exId, _) => (fpSt, .assertionFailure exId))
 
   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
+    | .assertionFailed => assertionFailures.head?.map fun (_, exId, _) => .assertionFailed fpSt exId
     | .cancelled => none  -- Cancellation is handled externally via cancel token, not through early termination conditions
   (newViolations, earlyTermination)
 
@@ -258,6 +267,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)}