diff --git a/Examples/Simulate/CheckpointLeaseFailover.lean b/Examples/Simulate/CheckpointLeaseFailover.lean new file mode 100644 index 00000000..2ebc2f38 --- /dev/null +++ b/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 diff --git a/Examples/Simulate/LeaseKeepaliveRace.lean b/Examples/Simulate/LeaseKeepaliveRace.lean new file mode 100644 index 00000000..7b12f17c --- /dev/null +++ b/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 diff --git a/Examples/Simulate/ReliableBroadcast.lean b/Examples/Simulate/ReliableBroadcast.lean new file mode 100644 index 00000000..9c33183b --- /dev/null +++ b/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 diff --git a/Examples/TLA/MutexViolation.lean b/Examples/TLA/MutexViolation.lean index 3b962025..74da3964 100644 --- a/Examples/TLA/MutexViolation.lean +++ b/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 diff --git a/Veil/Base.lean b/Veil/Base.lean index dcd9d679..5a78d767 100644 --- a/Veil/Base.lean +++ b/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 diff --git a/Veil/Core/Tools/ModelChecker/Concrete/Checker.lean b/Veil/Core/Tools/ModelChecker/Concrete/Checker.lean index ec4721f6..9ddc37e7 100644 --- a/Veil/Core/Tools/ModelChecker/Concrete/Checker.lean +++ b/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 diff --git a/Veil/Core/Tools/ModelChecker/Concrete/Core.lean b/Veil/Core/Tools/ModelChecker/Concrete/Core.lean index 92769266..a144bad5 100644 --- a/Veil/Core/Tools/ModelChecker/Concrete/Core.lean +++ b/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)} diff --git a/Veil/Core/Tools/ModelChecker/Concrete/Progress.lean b/Veil/Core/Tools/ModelChecker/Concrete/Progress.lean index 10a77d10..86386be0 100644 --- a/Veil/Core/Tools/ModelChecker/Concrete/Progress.lean +++ b/Veil/Core/Tools/ModelChecker/Concrete/Progress.lean @@ -59,7 +59,14 @@ structure ProgressHistoryPoint where queue : Nat deriving ToJson, FromJson, Inhabited, Repr -/-- Progress information for model checking, using TLC-style terminology. -/ +/-- Progress information for a simulation run. -/ +structure SimulationProgress where + tracesRun : Nat := 0 + maxTraces : Nat := 0 + depth : Nat := 0 + deriving ToJson, FromJson, Inhabited, Repr + +/-- Progress information for model checking or simulation. -/ structure Progress where status : String := "Initializing..." /-- Length of the longest behavior found so far (BFS depth) -/ @@ -82,6 +89,8 @@ structure Progress where allActionLabels : List String := [] /-- Time-series history for charting progress over time -/ history : Array ProgressHistoryPoint := #[] + /-- Progress information for `#simulate`; absent for `#model_check`. -/ + simulation : Option SimulationProgress := none deriving ToJson, FromJson, Inhabited, Repr /-- Refs for tracking progress of a single model checker instance. -/ @@ -90,6 +99,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 +136,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 +186,27 @@ 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 + simulation := some { tracesRun, maxTraces, depth } } + if ← compiledModeEnabled.get then + let startTime ← compiledModeStartTime.get + let p : Progress := { + status := status + isRunning := true + startTimeMs := startTime + elapsedMs := now - startTime + simulation := some { tracesRun, maxTraces, 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,14 +232,22 @@ 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 +def cancelProgress (instanceId : Nat) (resultJson : Lean.Json := Json.mkObj [("result", "cancelled")]) : IO Unit := withRefs instanceId fun refs => do let now ← IO.monoMsNow refs.progressRef.modify fun p => { p with status := "Cancelled", isRunning := false, isCancelled := true, elapsedMs := now - p.startTimeMs } - refs.resultRef.set (some (Json.mkObj [("result", "cancelled")])) + refs.resultRef.set (some resultJson) /-- Wait for model check to complete and return the result JSON. -/ partial def waitForResult (instanceId : Nat) (pollIntervalMs : Nat := 100) : IO (Option Lean.Json) := do diff --git a/Veil/Core/Tools/ModelChecker/ExecutionOutcome.lean b/Veil/Core/Tools/ModelChecker/ExecutionOutcome.lean index 96fb3da7..f01f2c0c 100644 --- a/Veil/Core/Tools/ModelChecker/ExecutionOutcome.lean +++ b/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 @@ -33,36 +33,6 @@ def toPostState : ExecutionOutcome ε σ → Option σ | .assertionFailure _ _ => .none | .divergence => .none -/-- Check if the outcome is a successful transition. -/ -@[inline] -def isSuccess : ExecutionOutcome ε σ → Bool - | .success _ => true - | _ => false - -/-- Check if the outcome is an assertion failure. -/ -@[inline] -def isAssertionFailure : ExecutionOutcome ε σ → Bool - | .assertionFailure _ _ => true - | _ => false - -/-- Check if the outcome is divergence. -/ -@[inline] -def isDivergence : ExecutionOutcome ε σ → Bool - | .divergence => true - | _ => false - -/-- Extract the state from a successful outcome. -/ -@[inline] -def getSuccessState? : ExecutionOutcome ε σ → Option σ - | .success st => some st - | _ => none - -/-- Extract the error and state from an assertion failure. -/ -@[inline] -def getAssertionFailure? : ExecutionOutcome ε σ → Option (ε × σ) - | .assertionFailure e st => some (e, st) - | _ => none - /-- Extract just the exception ID from an assertion failure. -/ @[inline] def exceptionId? : ExecutionOutcome ε σ → Option ε diff --git a/Veil/Core/Tools/ModelChecker/Interface.lean b/Veil/Core/Tools/ModelChecker/Interface.lean index 31f88e0b..fb845a27 100644 --- a/Veil/Core/Tools/ModelChecker/Interface.lean +++ b/Veil/Core/Tools/ModelChecker/Interface.lean @@ -51,6 +51,7 @@ inductive EarlyTerminationCondition where | deadlockOccurred | assertionFailed | reachedDepthBound (depth : Nat) + | reachedTraceLimit (maxTraces : Nat) | cancelled deriving Inhabited, Hashable, BEq, Repr @@ -61,13 +62,14 @@ inductive EarlyTerminationReason (σₕ : Type) where | deadlockOccurred (fp : σₕ) | assertionFailed (fp : σₕ) (exceptionId : Int) | reachedDepthBound (depth : Nat) + | reachedTraceLimit (maxTraces : Nat) | cancelled deriving Inhabited, Hashable, BEq, Repr /-- Check if the termination reason represents a violation that should prevent handoff. -/ def EarlyTerminationReason.isViolation {σₕ : Type} : EarlyTerminationReason σₕ → Bool | .foundViolatingState _ _ | .deadlockOccurred _ | .assertionFailed _ _ => true - | .reachedDepthBound _ | .cancelled => false + | .reachedDepthBound _ | .reachedTraceLimit _ | .cancelled => false instance [ToJson σₕ] : ToJson (EarlyTerminationReason σₕ) where toJson @@ -75,6 +77,7 @@ instance [ToJson σₕ] : ToJson (EarlyTerminationReason σₕ) where | .deadlockOccurred fp => Json.mkObj [("kind", "deadlock_occurred"), ("state_fingerprint", toJson fp)] | .assertionFailed fp exId => Json.mkObj [("kind", "assertion_failed"), ("state_fingerprint", toJson fp), ("exception_id", toJson exId)] | .reachedDepthBound depth => Json.mkObj [("kind", "reached_depth_bound"), ("depth", toJson depth)] + | .reachedTraceLimit maxTraces => Json.mkObj [("kind", "reached_trace_limit"), ("max_traces", toJson maxTraces)] | .cancelled => Json.mkObj [("kind", "cancelled")] inductive TerminationReason (σₕ : Type) where @@ -279,6 +282,29 @@ def SearchParameters.violatedAssumptions (params : SearchParameters ρ σ) (th : params.assumptions.filterMap fun p => if p.holdsOn th then none else some p.name +/-- Create a filtered transition system that explores only states satisfying +state constraints. -/ +@[inline] +def restrictSystemByStateConstraints {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) (th : ρ) : + EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀ := + if params.stateConstraints.isEmpty then sys else { + initStates := sys.initStates.filter (params.satisfiesConstraints th) + tr := fun th' st => (sys.tr th' st).filter fun (_, outcome) => + match outcome with + | .success st' => params.satisfiesConstraints th st' + -- Assertion failures should satisfy constraints to be considered. + | .assertionFailure _ st' => params.satisfiesConstraints th st' + -- Divergence has no successor state to constrain. + | .divergence => true + } + +@[inline] +def violatedInvariantNames {ρ σ : Type} + (params : SearchParameters ρ σ) (th : ρ) (st : σ) : List Lean.Name := + params.invariants.filterMap fun p => + if !p.holdsOn th st then some p.name else none -- class ModelChecker (ts : TransitionSystem ρ σ l) where -- isReachable : SearchParameters ρ σ → Option ParallelConfig → ModelCheckingResult ρ σ l σₕ diff --git a/Veil/Core/Tools/ModelChecker/Simulation.lean b/Veil/Core/Tools/ModelChecker/Simulation.lean new file mode 100644 index 00000000..146ab9ae --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation.lean @@ -0,0 +1 @@ +import Veil.Core.Tools.ModelChecker.Simulation.Checker diff --git a/Veil/Core/Tools/ModelChecker/Simulation/Basic.lean b/Veil/Core/Tools/ModelChecker/Simulation/Basic.lean new file mode 100644 index 00000000..27b0e6d1 --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation/Basic.lean @@ -0,0 +1,42 @@ +import Veil.Core.Tools.ModelChecker.Interface + +namespace Veil.ModelChecker.Simulation +open Lean + +structure SimulateConfig where + maxTraces : Nat := 10000 + maxSteps : Nat := 100 + seed : Nat := 0 +deriving Inhabited, Repr + +inductive SimulationResult (ρ σ κ : Type) where + | cancelled + | foundViolation (violation : ViolationKind) (viaTrace : Trace ρ σ κ) +deriving Inhabited, Repr + +def SimulationResult.depth {ρ σ κ : Type} : SimulationResult ρ σ κ → Nat + | .foundViolation _ trace => trace.steps.size + if trace.failingStep.isSome then 1 else 0 + | .cancelled => 0 + +inductive SimulationTerminationReason where + | noInitialStates +deriving Inhabited, Hashable, BEq, Repr + +instance : ToJson SimulationTerminationReason where + toJson + | .noInitialStates => Json.mkObj [("kind", "no_initial_states")] + +structure SimulateResult (ρ σ κ : Type) where + result : Option (SimulationResult ρ σ κ) + tracesRun : Nat + maxTraces : Nat + elapsedMs : Nat + seed : Nat + terminationReason : Option SimulationTerminationReason := none + +def SimulateResult.depth {ρ σ κ : Type} (result : SimulateResult ρ σ κ) : Nat := + match result.result with + | some result => result.depth + | none => 0 + +end Veil.ModelChecker.Simulation diff --git a/Veil/Core/Tools/ModelChecker/Simulation/Checker.lean b/Veil/Core/Tools/ModelChecker/Simulation/Checker.lean new file mode 100644 index 00000000..6aaa1b19 --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation/Checker.lean @@ -0,0 +1,7 @@ +import Veil.Core.Tools.ModelChecker.Simulation.Runtime +import Veil.Core.Tools.ModelChecker.Simulation.Result +import Veil.Core.Tools.ModelChecker.Simulation.Soundness + +namespace Veil.ModelChecker.Simulation + +end Veil.ModelChecker.Simulation diff --git a/Veil/Core/Tools/ModelChecker/Simulation/Path.lean b/Veil/Core/Tools/ModelChecker/Simulation/Path.lean new file mode 100644 index 00000000..3984b30b --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation/Path.lean @@ -0,0 +1,103 @@ +import Veil.Core.Tools.ModelChecker.Simulation.Basic +import Veil.Core.Tools.ModelChecker.Concrete.Core + +namespace Veil.ModelChecker.Simulation + +theorem randNat_lt_length {α : Type} (xs : List α) (h : xs ≠ []) (gen : StdGen) : + (let p := randNat gen 0 (xs.length - 1); p.1 < xs.length) := by + have hlen : 0 < xs.length := by simpa [List.length_pos_iff_ne_nil] using h + have hk : xs.length - 1 + 1 = xs.length := Nat.sub_add_cancel (Nat.succ_le_of_lt hlen) + unfold randNat + simp [Nat.not_lt.mpr (Nat.zero_le (xs.length - 1)), hk] + exact Nat.mod_lt _ hlen + +@[inline, specialize] +def simulateOnceLoop {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (stepsLeft : Nat) + (currSt : σ) + (trace : Trace ρ σ κ) + : StateM StdGen (Option (SimulationResult ρ σ κ)) := do + match stepsLeft with + | 0 => return none + | stepsLeft + 1 => + let outcomes := sys.tr th currSt + let (nexts, assertionFailures) := Veil.ModelChecker.Concrete.partitionExecutionOutcome outcomes + match assertionFailures with + | (label, exId, st) :: _ => + let failedTrace := { trace with failingStep := some { transitionLabel := label, nextState := st } } + return some (.foundViolation (.assertionFailure exId) failedTrace) + | [] => + match nexts with + | [] => + if !params.terminating.holdsOn th currSt then + return some (.foundViolation .deadlock trace) + else + return none + | hd :: tl => + let nexts := hd :: tl + have hNonempty : nexts ≠ [] := by simp + let gen ← get + let p := randNat gen 0 (nexts.length - 1) + let idx := p.1 + let gen' := p.2 + have hlt : idx < nexts.length := by + dsimp [idx, p] + exact randNat_lt_length nexts hNonempty gen + set gen' + let (label, nextSt) := nexts.get ⟨idx, hlt⟩ + let trace := trace.push { transitionLabel := label, nextState := nextSt } + let violations := violatedInvariantNames params th nextSt + if !violations.isEmpty then + return some (.foundViolation (.safetyFailure violations) trace) + else + simulateOnceLoop sys params th stepsLeft nextSt trace +termination_by stepsLeft + +@[inline, specialize] +def simulateOnce {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (maxSteps : Nat) + : StateM StdGen (Option (SimulationResult ρ σ κ)) := do + let initStates := sys.initStates + match initStates with + | [] => return none + | hd :: tl => + let initStates := hd :: tl + have hNonempty : initStates ≠ [] := by simp + let gen ← get + let p := randNat gen 0 (initStates.length - 1) + let idx := p.1 + let gen' := p.2 + have hlt : idx < initStates.length := by + dsimp [idx, p] + exact randNat_lt_length initStates hNonempty gen + set gen' + let initSt := initStates.get ⟨idx, hlt⟩ + let initTrace : Trace ρ σ κ := { theory := th, initialState := initSt, steps := #[] } + let initViolations := violatedInvariantNames params th initSt + if !initViolations.isEmpty then + return some (.foundViolation (.safetyFailure initViolations) initTrace) + else + simulateOnceLoop sys params th maxSteps initSt initTrace + +/-- +Simulates the trace identified by `traceIndex` using seed `cfg.seed + traceIndex`. +Returns the first violation found by that trace. +-/ +def simulateTraceAtIndex {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (cfg : SimulateConfig) + (traceIndex : Nat) + : Option (SimulationResult ρ σ κ) := + let traceSeed := cfg.seed + traceIndex + let (maybeResult, _) := (simulateOnce sys params th cfg.maxSteps).run (mkStdGen traceSeed) + maybeResult + +end Veil.ModelChecker.Simulation diff --git a/Veil/Core/Tools/ModelChecker/Simulation/Result.lean b/Veil/Core/Tools/ModelChecker/Simulation/Result.lean new file mode 100644 index 00000000..62aba82b --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation/Result.lean @@ -0,0 +1,35 @@ +import Veil.Core.Tools.ModelChecker.Simulation.Basic + +namespace Veil.ModelChecker.Simulation +open Lean + +private def resultToJson {ρ σ κ : Type} [ToJson ρ] [ToJson σ] [ToJson κ] + (result : Option (SimulationResult ρ σ κ)) : Json := + match result with + | some (.foundViolation violation trace) => + toJson (ModelCheckingResult.foundViolation Json.null violation (some trace) : ModelCheckingResult ρ σ κ Json) + | some .cancelled => + toJson (ModelCheckingResult.cancelled : ModelCheckingResult ρ σ κ Json) + | none => Json.mkObj [("result", "no_violation_found")] + +private def metadataToJsonFields {ρ σ κ : Type} (r : SimulateResult ρ σ κ) : List (String × Json) := + let reasonField := r.terminationReason.map fun reason => ("termination_reason", Lean.toJson reason) + [ + ("traces_run", Lean.toJson r.tracesRun), + ("max_traces", Lean.toJson r.maxTraces), + ("elapsed_ms", Lean.toJson r.elapsedMs), + ("seed", Lean.toJson r.seed), + ("depth", Lean.toJson r.depth) + ] ++ reasonField.toList + +/-- Flatten the result object while keeping simulation metadata at the top level. -/ +def SimulateResult.toDisplayJson {ρ σ κ : Type} [ToJson ρ] [ToJson σ] [ToJson κ] + (r : SimulateResult ρ σ κ) : Json := + match resultToJson r.result with + | Json.obj kvs => Json.mkObj <| kvs.toList ++ metadataToJsonFields r + | other => Json.mkObj <| ("result", other) :: metadataToJsonFields r + +instance instToJsonSimulateResult {ρ σ κ : Type} [ToJson ρ] [ToJson σ] [ToJson κ] : ToJson (SimulateResult ρ σ κ) where + toJson r := SimulateResult.toDisplayJson r + +end Veil.ModelChecker.Simulation diff --git a/Veil/Core/Tools/ModelChecker/Simulation/Runtime.lean b/Veil/Core/Tools/ModelChecker/Simulation/Runtime.lean new file mode 100644 index 00000000..bf99f3c7 --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation/Runtime.lean @@ -0,0 +1,211 @@ +import Veil.Core.Tools.ModelChecker.Simulation.Path +import Veil.Core.Tools.ModelChecker.Simulation.Soundness +import Veil.Core.Tools.ModelChecker.Concrete.Progress + +namespace Veil.ModelChecker.Simulation + +private def noInitialStatesResult {ρ σ κ : Type} (cfg : SimulateConfig) : SimulateResult ρ σ κ := { + result := none + tracesRun := 0 + maxTraces := cfg.maxTraces + elapsedMs := 0 + seed := cfg.seed + terminationReason := some .noInitialStates +} + +private def hasNoInitialStates {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) : Bool := + sys.initStates.isEmpty + +private structure SimulationHooks (m : Type → Type) where + shouldStop : Nat → m Bool + onTraceProgress : Nat → m PUnit + onViolation : m PUnit + +private def simulateLoopM {m : Type → Type} [Monad m] {ρ σ κ : Type} {th₀ : ρ} + (hooks : SimulationHooks m) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (cfg : SimulateConfig) + (remaining : Nat) + (traceIndex : Nat) + : m (SimulateResult ρ σ κ) := do + if ← hooks.shouldStop traceIndex then + return { + result := some .cancelled + tracesRun := traceIndex + maxTraces := cfg.maxTraces + elapsedMs := 0 + seed := cfg.seed + } + match remaining with + | 0 => + return { + result := none + tracesRun := cfg.maxTraces + maxTraces := cfg.maxTraces + elapsedMs := 0 + seed := cfg.seed + } + | remaining + 1 => + hooks.onTraceProgress traceIndex + match simulateTraceAtIndex sys params th cfg traceIndex with + | some result => + hooks.onViolation + return { + result := some result + tracesRun := traceIndex + 1 + maxTraces := cfg.maxTraces + elapsedMs := 0 + seed := cfg.seed + } + | none => + simulateLoopM hooks sys params th cfg remaining (traceIndex + 1) +termination_by remaining + +@[inline, specialize] +def simulateCommandSemantics {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (shouldStop : Nat → Bool) + (cfg : SimulateConfig) + : SimulateResult ρ σ κ := + let sys := restrictSystemByStateConstraints sys params th + if hasNoInitialStates sys then + noInitialStatesResult cfg + else + simulateLoopM + ({ shouldStop := fun traceIndex => shouldStop traceIndex + onTraceProgress := fun _ => () + onViolation := () } : SimulationHooks Id) + sys params th cfg cfg.maxTraces 0 + +@[inline, specialize] +def simulateCore {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (cfg : SimulateConfig) + : SimulateResult ρ σ κ := + simulateCommandSemantics sys params th (fun _ => false) cfg + +@[inline, specialize] +def simulateWithProgress {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (cfg : SimulateConfig) + (progressInstanceId : Nat) + (cancelToken : IO.CancelToken) + : IO (SimulateResult ρ σ κ) := do + let actualSeed ← if cfg.seed == 0 then IO.rand 0 0xFFFFFFFFFFFFFFFF else pure cfg.seed + let cfg := { cfg with seed := actualSeed } + let startMs ← IO.monoMsNow + let sys := restrictSystemByStateConstraints sys params th + if hasNoInitialStates sys then + let simResult := { noInitialStatesResult cfg with elapsedMs := (← IO.monoMsNow) - startMs } + Veil.ModelChecker.Concrete.updateSimulationProgress progressInstanceId + "Complete" + simResult.tracesRun simResult.maxTraces simResult.depth + return simResult + let lastStatusUpdateRef ← IO.mkRef startMs + let simResult ← simulateLoopM + { shouldStop := fun _ => Veil.ModelChecker.Concrete.shouldStop cancelToken progressInstanceId + onTraceProgress := fun tracesRun => do + let now ← IO.monoMsNow + let lastStatusUpdate ← lastStatusUpdateRef.get + if now - lastStatusUpdate ≥ 100 then + Veil.ModelChecker.Concrete.updateSimulationProgress progressInstanceId + s!"Running random traces ({tracesRun}/{cfg.maxTraces})" + tracesRun cfg.maxTraces 0 + lastStatusUpdateRef.set now + onViolation := do + Veil.ModelChecker.Concrete.setViolationFound progressInstanceId } + sys params th cfg cfg.maxTraces 0 + let simResult := { simResult with elapsedMs := (← IO.monoMsNow) - startMs } + match simResult.result with + | some .cancelled => pure () + | _ => + Veil.ModelChecker.Concrete.updateSimulationProgress progressInstanceId + "Complete" + simResult.tracesRun simResult.maxTraces simResult.depth + return simResult + +@[inline, specialize] +def simulate {ρ σ κ : Type} {th₀ : ρ} + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) + (th : ρ) + (cfg : SimulateConfig) + : IO (SimulateResult ρ σ κ) := do + let cancelToken ← IO.CancelToken.new + simulateWithProgress sys params th cfg 0 cancelToken + +private theorem simulateLoopM_id_sound {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] + [Inhabited σ] [Inhabited (κ × σ)] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) + (cfg : SimulateConfig) + (shouldStop : Nat → Bool) : + ∀ remaining traceIndex, + ReportedViolationSound sys params + (SimulateResult.result + (simulateLoopM + ({ shouldStop := fun traceIndex => shouldStop traceIndex + onTraceProgress := fun _ => () + onViolation := () } : SimulationHooks Id) + sys params th cfg remaining traceIndex)) := by + intro remaining + induction remaining with + | zero => + intro traceIndex + cases hStop : shouldStop traceIndex <;> + simp [simulateLoopM, hStop, ReportedViolationSound, Id.instMonad] + | succ remaining ih => + intro traceIndex + cases hStop : shouldStop traceIndex with + | true => + simp [simulateLoopM, hStop, ReportedViolationSound, Id.instMonad] + | false => + by_cases hTrace : simulateTraceAtIndex sys params th cfg traceIndex = none + · simpa [simulateLoopM, hStop, hTrace, Id.instMonad] using ih (traceIndex + 1) + · cases hRun : simulateTraceAtIndex sys params th cfg traceIndex with + | none => contradiction + | some result => + simpa [simulateLoopM, hStop, hRun, Id.instMonad] using + simulateTraceAtIndex_sound th sys params cfg traceIndex result hRun + +theorem simulateCommandSemantics_sound {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] + [Inhabited σ] [Inhabited (κ × σ)] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) + (shouldStop : Nat → Bool) + (cfg : SimulateConfig) : + ReportedViolationSound (restrictSystemByStateConstraints sys params th) params + (SimulateResult.result (simulateCommandSemantics sys params th shouldStop cfg)) := by + let restrictedSys := restrictSystemByStateConstraints sys params th + cases hNoInit : hasNoInitialStates restrictedSys with + | true => + simp [simulateCommandSemantics, restrictedSys, hNoInit, noInitialStatesResult, ReportedViolationSound] + | false => + simpa [simulateCommandSemantics, restrictedSys, hNoInit] using + simulateLoopM_id_sound th restrictedSys params cfg shouldStop cfg.maxTraces 0 + +theorem simulateCore_sound {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] + [Inhabited σ] [Inhabited (κ × σ)] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) + (cfg : SimulateConfig) : + ReportedViolationSound (restrictSystemByStateConstraints sys params th) params + (SimulateResult.result (simulateCore sys params th cfg)) := by + simpa [simulateCore] using simulateCommandSemantics_sound th sys params (fun _ => false) cfg + +end Veil.ModelChecker.Simulation diff --git a/Veil/Core/Tools/ModelChecker/Simulation/Soundness.lean b/Veil/Core/Tools/ModelChecker/Simulation/Soundness.lean new file mode 100644 index 00000000..fa30ae37 --- /dev/null +++ b/Veil/Core/Tools/ModelChecker/Simulation/Soundness.lean @@ -0,0 +1,297 @@ +import Veil.Core.Tools.ModelChecker.Simulation.Basic +import Veil.Core.Tools.ModelChecker.Simulation.Path +import Veil.Core.Tools.ModelChecker.Concrete.Core + +namespace Veil.ModelChecker.Simulation + +theorem pickedTransition_valid {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (_params : SearchParameters ρ σ) (currSt : σ) + (nexts : List (κ × σ)) + (hNexts : nexts = (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr th currSt)).fst) + (selected : κ × σ) + (hSelected : selected ∈ nexts) : + sys.toRelational.tr th currSt selected.1 selected.2 := by + have hGood : selected ∈ + (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr th currSt)).fst := by + simpa [hNexts] using hSelected + simpa [EnumerableTransitionSystem.toRelational] using + (Veil.ModelChecker.Concrete.partitionExecutionOutcome.fst_spec _ _ _).mp hGood + +theorem pickedInitialState_valid {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (_params : SearchParameters ρ σ) + (initStates : List σ) + (hInitStates : initStates = sys.initStates) + (selectedInit : σ) + (hSelected : selectedInit ∈ initStates) : + ({ theory := th, initialState := selectedInit, steps := #[] } : Trace ρ σ κ).isValid + sys.toRelational := by + refine Trace.isValid_empty sys.toRelational th selectedInit ?_ ?_ + · simp [EnumerableTransitionSystem.toRelational] + · simpa [EnumerableTransitionSystem.toRelational, hInitStates] using hSelected + +def Trace.witnessesSimulationViolation {ρ σ κ : Type} {th₀ : ρ} + [DecidableEq σ] [DecidableEq κ] + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) (trace : Trace ρ σ κ) : ViolationKind → Prop + | .assumptionFailure violates => + trace.isValid sys.toRelational ∧ + params.violatedAssumptions trace.theory = violates ∧ + violates ≠ [] + | .safetyFailure violates => + trace.isValid sys.toRelational ∧ + trace.failingStep = none ∧ + violatedInvariantNames params trace.theory trace.lastState = violates ∧ + violates ≠ [] + | .deadlock => + trace.isValid sys.toRelational ∧ + trace.failingStep = none ∧ + (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr trace.theory trace.lastState)).fst = [] ∧ + (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr trace.theory trace.lastState)).snd = [] ∧ + !params.terminating.holdsOn trace.theory trace.lastState = true + | .assertionFailure exId => + trace.isValid sys.toRelational ∧ + ∃ step, + trace.failingStep = some step ∧ + (step.transitionLabel, ExecutionOutcome.assertionFailure exId step.nextState) ∈ + sys.tr trace.theory trace.lastState + +theorem Trace.witnessesSimulationViolation_valid {ρ σ κ : Type} {th : ρ} + [DecidableEq σ] [DecidableEq κ] + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) (trace : Trace ρ σ κ) (violation : ViolationKind) : + Trace.witnessesSimulationViolation sys params trace violation → + trace.isValid sys.toRelational := by + intro h + cases violation with + | assumptionFailure _ => exact h.1 + | safetyFailure _ => exact h.1 + | deadlock => exact h.1 + | assertionFailure _ => exact h.1 + +def ReportedViolationSound {ρ σ κ : Type} {th₀ : ρ} + [DecidableEq σ] [DecidableEq κ] + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) + (params : SearchParameters ρ σ) (result : Option (SimulationResult ρ σ κ)) : Prop := + match result with + | some (.foundViolation violation trace) => Trace.witnessesSimulationViolation sys params trace violation + | some .cancelled => True + | none => True + +theorem simulateOnceLoop_sound {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] [Inhabited (κ × σ)] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) + (currSt : σ) + (trace : Trace ρ σ κ) + (hTheory : trace.theory = th) + (hValid : trace.isValid sys.toRelational) + (hLast : trace.lastState = currSt) + (hNoFail : trace.failingStep = none) : + ∀ stepsLeft gen result, + ((simulateOnceLoop sys params th stepsLeft currSt trace).run gen).1 = some result -> + ReportedViolationSound sys params (some result) := by + intro stepsLeft + induction stepsLeft generalizing currSt trace with + | zero => + intro gen result h + simp [simulateOnceLoop] at h + | succ steps ih => + intro gen result h + cases hPartition : Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr th currSt) with + | mk nexts assertionFailures => + cases hFailures : assertionFailures with + | cons failure failures => + rcases failure with ⟨label, exId, st⟩ + simp [simulateOnceLoop, hPartition, hFailures] at h + cases h + have hFailureMem : (label, exId, st) ∈ + (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr th currSt)).snd := by + rw [hPartition] + simp [hFailures] + have hMem : (label, ExecutionOutcome.assertionFailure exId st) ∈ + sys.tr th currSt := + (Veil.ModelChecker.Concrete.partitionExecutionOutcome.snd_spec _ _ _ _).mp hFailureMem + let step : Step σ κ := { transitionLabel := label, nextState := st } + let failedTrace := { trace with failingStep := some step } + have hValidFail : failedTrace.isValid sys.toRelational := by + exact { + theorySatisfiesAssumptions := hValid.theorySatisfiesAssumptions + initialStateSatisfiesInit := hValid.initialStateSatisfiesInit + stepsValid := hValid.stepsValid + } + refine ⟨hValidFail, step, rfl, ?_⟩ + have hLastFail : failedTrace.lastState = currSt := by + simpa [failedTrace, Trace.lastState] using hLast + rw [hLastFail] + simpa [failedTrace, step, hTheory] using hMem + | nil => + cases hNexts : nexts with + | nil => + cases hTerminating : !params.terminating.holdsOn th currSt with + | true => + simp [simulateOnceLoop, hPartition, hFailures, hNexts, hTerminating] at h + cases h + have hNoSuccesses : (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr trace.theory trace.lastState)).fst = [] := by + simp [hTheory, hLast, hPartition, hNexts] + have hNoFailures : (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr trace.theory trace.lastState)).snd = [] := by + simp [hTheory, hLast, hPartition, hFailures] + have hDeadlock : !params.terminating.holdsOn trace.theory trace.lastState = true := by + simpa [hTheory, hLast] using hTerminating + exact ⟨hValid, hNoFail, hNoSuccesses, hNoFailures, hDeadlock⟩ + | false => + simp [simulateOnceLoop, hPartition, hFailures, hNexts, hTerminating] at h + | cons hd tl => + let nexts' : List (κ × σ) := hd :: tl + have hNonempty : nexts' ≠ [] := by simp [nexts'] + let p := randNat gen 0 (nexts'.length - 1) + let idx := p.1 + let gen' := p.2 + have hlt : idx < nexts'.length := by + dsimp [idx, p] + exact randNat_lt_length nexts' hNonempty gen + let selected := nexts'.get ⟨idx, hlt⟩ + let trace' := trace.push { transitionLabel := selected.1, nextState := selected.2 } + have hSelected : selected ∈ nexts' := by + dsimp [selected] + exact List.get_mem nexts' ⟨idx, hlt⟩ + have hNextsHd : nexts' = (Veil.ModelChecker.Concrete.partitionExecutionOutcome + (sys.tr th currSt)).fst := by + simp [nexts', hPartition, hNexts] + have hRel : sys.toRelational.tr th currSt selected.1 selected.2 := + pickedTransition_valid th sys params currSt nexts' hNextsHd selected hSelected + have hValid' : trace'.isValid sys.toRelational := by + exact Trace.push_isValid trace { transitionLabel := selected.1, nextState := selected.2 } + sys.toRelational hValid (by simpa [hTheory, hLast] using hRel) + have hTheory' : trace'.theory = th := by + simpa [trace', hTheory] + have hNoFail' : trace'.failingStep = none := by + simpa [trace', hNoFail] + have hLast' : trace'.lastState = selected.2 := by + simp [trace'] + cases hViol : (violatedInvariantNames params th selected.2).isEmpty with + | true => + have hViolNil : violatedInvariantNames params th selected.2 = [] := by + simpa using hViol + have hViolNilRaw : + violatedInvariantNames params th (hd :: tl)[(randNat gen 0 tl.length).1].2 = [] := by + simpa [nexts', p, idx, selected] using hViolNil + have hLoop : ((simulateOnceLoop sys params th steps selected.2 trace').run gen').1 = some result := by + rw [simulateOnceLoop] at h + simp only [hPartition, hFailures, hNexts, StateT.run_bind, Id.instMonad] at h + simpa [nexts', p, idx, gen', hlt, selected, trace', hViolNilRaw] using h + exact ih selected.2 trace' hTheory' hValid' hLast' hNoFail' gen' result hLoop + | false => + have hNonempty : violatedInvariantNames params th selected.2 ≠ [] := by + intro hNil + simp [hNil] at hViol + have hNonemptyRaw : + violatedInvariantNames params th (hd :: tl)[(randNat gen 0 tl.length).1].2 ≠ [] := by + simpa [nexts', p, idx, selected] using hNonempty + have hFound : (some (SimulationResult.foundViolation + (ViolationKind.safetyFailure (violatedInvariantNames params th selected.2)) trace') : + Option (SimulationResult ρ σ κ)) = some result := by + rw [simulateOnceLoop] at h + simp only [hPartition, hFailures, hNexts, StateT.run_bind, Id.instMonad] at h + simpa [nexts', p, idx, gen', hlt, selected, trace', hNonemptyRaw] using h + cases hFound + have hViolEq : violatedInvariantNames params trace'.theory trace'.lastState = + violatedInvariantNames params th selected.2 := by + simp [hTheory', hLast'] + exact ⟨hValid', hNoFail', hViolEq, hNonempty⟩ + +theorem simulateOnce_sound {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] [Inhabited σ] [Inhabited (κ × σ)] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) (gen : StdGen) (maxSteps : Nat) (result : SimulationResult ρ σ κ) : + ((simulateOnce sys params th maxSteps).run gen).1 = some result -> + ReportedViolationSound sys params (some result) := by + intro h + unfold simulateOnce at h + cases hStates : sys.initStates with + | nil => simp [hStates] at h + | cons initSt rest => + let initStates : List σ := initSt :: rest + have hNonempty : initStates ≠ [] := by simp [initStates] + let p := randNat gen 0 (initStates.length - 1) + let idx := p.1 + let gen' := p.2 + have hlt : idx < initStates.length := by + dsimp [idx, p] + exact randNat_lt_length initStates hNonempty gen + let selectedInit := initStates.get ⟨idx, hlt⟩ + let initTrace : Trace ρ σ κ := { theory := th, initialState := selectedInit, steps := #[] } + have hSelectedInit : selectedInit ∈ initStates := by + dsimp [selectedInit] + exact List.get_mem initStates ⟨idx, hlt⟩ + have hInitStates : initStates = sys.initStates := by + simp [initStates, hStates] + have hValid : initTrace.isValid sys.toRelational := by + simpa [initTrace] using + pickedInitialState_valid th sys params initStates hInitStates selectedInit hSelectedInit + have hLast : initTrace.lastState = selectedInit := by + simp [initTrace] + have hNoFail : initTrace.failingStep = none := by + simp [initTrace] + cases hViol : (violatedInvariantNames params th selectedInit).isEmpty with + | true => + have hViolNil : violatedInvariantNames params th selectedInit = [] := by + simpa using hViol + have hViolNilRaw : + violatedInvariantNames params th (initSt :: rest)[(randNat gen 0 rest.length).1] = [] := by + simpa [initStates, p, idx, selectedInit] using hViolNil + have hLoop : ((simulateOnceLoop sys params th maxSteps selectedInit initTrace).run gen').1 = some result := by + rw [hStates] at h + simp only [StateT.run_bind, Id.instMonad] at h + simpa [initStates, p, idx, gen', hlt, selectedInit, initTrace, hViolNilRaw] using h + exact simulateOnceLoop_sound th sys params selectedInit initTrace rfl hValid hLast hNoFail maxSteps gen' result hLoop + | false => + have hNonempty : violatedInvariantNames params th selectedInit ≠ [] := by + intro hNil + simp [hNil] at hViol + have hNonemptyRaw : + violatedInvariantNames params th (initSt :: rest)[(randNat gen 0 rest.length).1] ≠ [] := by + simpa [initStates, p, idx, selectedInit] using hNonempty + have hFound : (some (SimulationResult.foundViolation + (ViolationKind.safetyFailure (violatedInvariantNames params th selectedInit)) initTrace) : + Option (SimulationResult ρ σ κ)) = some result := by + rw [hStates] at h + simp only [StateT.run_bind, Id.instMonad] at h + simpa [initStates, p, idx, gen', hlt, selectedInit, initTrace, hNonemptyRaw] using h + cases hFound + exact ⟨hValid, hNoFail, rfl, hNonempty⟩ + +/-- Any violation reported by a single indexed random trace is sound. -/ +theorem simulateTraceAtIndex_sound {ρ σ κ : Type} + [DecidableEq σ] [DecidableEq κ] [Inhabited σ] [Inhabited (κ × σ)] + (th : ρ) + (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th) + (params : SearchParameters ρ σ) + (cfg : SimulateConfig) + (traceIndex : Nat) + (result : SimulationResult ρ σ κ) : + simulateTraceAtIndex sys params th cfg traceIndex = some result -> + ReportedViolationSound sys params (some result) := by + intro h + unfold simulateTraceAtIndex at h + set traceSeed := cfg.seed + traceIndex + have hSimSome : ((simulateOnce sys params th cfg.maxSteps).run (mkStdGen traceSeed)).1 = some result := by + simpa [traceSeed] using h + exact simulateOnce_sound th sys params (mkStdGen traceSeed) cfg.maxSteps result hSimSome + +end Veil.ModelChecker.Simulation diff --git a/Veil/Core/UI/Trace/TraceDisplay.lean b/Veil/Core/UI/Trace/TraceDisplay.lean index 155e0e9d..1606c242 100644 --- a/Veil/Core/UI/Trace/TraceDisplay.lean +++ b/Veil/Core/UI/Trace/TraceDisplay.lean @@ -88,6 +88,15 @@ def formatTrace (j : Json) (ind : String := " ") : String := Id.run do | .arr states => r ++ (states.toList.map (fmtState · ind) |> "\n".intercalate) | _ => r ++ s!"{ind}(no states)" +private def fmtSeedSuffix (j : Json) : String := + let seed := j.getObjValD "seed" + if seed == .null then "" else s!"\nSeed: {fmtJson seed}" + +private def isNoInitialStatesTermination (j : Json) : Bool := + match j.getObjValD "termination_reason" with + | .obj reason => fmtJson ((Json.obj reason).getObjValD "kind") == "no_initial_states" + | _ => false + def formatModelCheckingResult (j : Json) : MessageData := match fmtJson (j.getObjValD "result") with | "found_violation" => @@ -97,12 +106,17 @@ def formatModelCheckingResult (j : Json) : MessageData := | _ => "" let trace := j.getObjValD "trace" let traceMsg := if trace == .null then "" else s!"\n{formatTrace trace}" - m!"❌ Violation: {fmtJson (v.getObjValD "kind")}{violates}{traceMsg}" + m!"❌ Violation: {fmtJson (v.getObjValD "kind")}{violates}{traceMsg}{fmtSeedSuffix j}" | "no_violation_found" => let trace := j.getObjValD "trace" - if trace != .null then m!"✅ Satisfying trace found\n{formatTrace trace}" - else m!"✅ No violation (explored {fmtJson (j.getObjValD "explored_states")} states)" - | "cancelled" => m!"⚠️ Cancelled" + if trace != .null then m!"✅ Satisfying trace found\n{formatTrace trace}{fmtSeedSuffix j}" + else if isNoInitialStatesTermination j then + m!"✅ No initial states available after applying state constraints{fmtSeedSuffix j}" + else if j.getObjValD "traces_run" != .null then + m!"✅ No violation in {fmtJson (j.getObjValD "traces_run")} traces{fmtSeedSuffix j}" + else + m!"✅ No violation (explored {fmtJson (j.getObjValD "explored_states")} states){fmtSeedSuffix j}" + | "cancelled" => m!"⚠️ Cancelled{fmtSeedSuffix j}" | r => if j.getObjValD "error" != .null then m!"💥 Error: {fmtJson (j.getObjValD "error")}" else m!"Unknown: {r}" end Veil.TraceDisplay diff --git a/Veil/Core/UI/Widget/ProgressViewer.lean b/Veil/Core/UI/Widget/ProgressViewer.lean index 39644ea5..1247f615 100644 --- a/Veil/Core/UI/Widget/ProgressViewer.lean +++ b/Veil/Core/UI/Widget/ProgressViewer.lean @@ -498,8 +498,23 @@ private def metricsHistoryHtml (history : Array ProgressHistoryPoint) : Html := /-- Convert Progress to Html for display, with optional Stop button. Uses TLC-style terminology. -/ -def progressToHtml (p : Progress) (instanceId? : Option Nat := none) : Html := -
+def progressToHtml (p : Progress) (instanceId? : Option Nat := none) : Html := Id.run do + let (progressRows, metricsHistory, actionCoverage) : Array Html × Html × Html := + match p.simulation with + | some sim => + (#[ + statRow "Traces Run:" (toString sim.tracesRun), + statRow "Max Traces:" (toString sim.maxTraces), + statRow "Depth:" (toString sim.depth), + ], .text "", .text "") + | none => + (#[ + statRow "Diameter:" (toString p.diameter), + statRow "States Found:" (toString p.statesFound), + statRow "Distinct States:" (toString p.distinctStates), + statRow "Queue:" (toString p.queue), + ], metricsHistoryHtml p.history, actionCoverageHtml p.actionStats p.allActionLabels) + return
{if p.isRunning then
@@ -518,16 +533,10 @@ def progressToHtml (p : Progress) (instanceId? : Option Nat := none) : Html :=
Done!
} - - {statRow "Diameter:" (toString p.diameter)} - {statRow "States Found:" (toString p.statesFound)} - {statRow "Distinct States:" (toString p.distinctStates)} - {statRow "Queue:" (toString p.queue)} - {statRow "Elapsed time:" (formatElapsedTime p.elapsedMs)} - + {.element "tbody" #[] (progressRows.push (statRow "Elapsed time:" (formatElapsedTime p.elapsedMs)))}
- {metricsHistoryHtml p.history} - {actionCoverageHtml p.actionStats p.allActionLabels} + {metricsHistory} + {actionCoverage} {match p.compilationStatus with | .inProgress ms lines => if lines.isEmpty then .text "" else compilationLogHtml ms lines | .failed err => compilationFailureHtml err diff --git a/Veil/Frontend/DSL/Module/Elaborators.lean b/Veil/Frontend/DSL/Module/Elaborators.lean index 8bbf05c2..78726036 100644 --- a/Veil/Frontend/DSL/Module/Elaborators.lean +++ b/Veil/Frontend/DSL/Module/Elaborators.lean @@ -13,6 +13,7 @@ import Veil.Core.Tools.Verifier.Results import Veil.Core.UI.Verifier.VerificationResults import Veil.Core.UI.Trace.TraceDisplay import Veil.Core.Tools.ModelChecker.Concrete.Checker +import Veil.Core.Tools.ModelChecker.Simulation import Veil.Frontend.DSL.Action.Extract import Veil.Frontend.DSL.Module.Util.Enumeration import Veil.Util.Multiprocessing @@ -606,6 +607,35 @@ def defaultThresholdToParallel : Nat := 20 declare_command_config_elab elabModelCheckerConfig ModelCheckerConfig +declare_command_config_elab elabSimulateConfig ModelChecker.Simulation.SimulateConfig + +/-- +Check whether a particular config field was written explicitly in the command syntax. + +`elabSimulateConfig` returns a complete `SimulateConfig`, so omitted fields are +indistinguishable from fields explicitly written with their structure defaults +after elaboration. Inspect the raw `Parser.Tactic.optConfig` only for this +distinction. A `(config := cfg)` item is an opaque full `SimulateConfig`, so it +is treated as explicitly providing all fields rather than being overlaid with +global options. +-/ +def simulateConfigHasField (cfgStx : Syntax) (fieldName : Name) : Bool := + Lean.Elab.Tactic.mkConfigItemViews (Lean.Parser.Tactic.getConfigItems cfgStx) |>.any + (fun item => + let optionName := item.option.getId.eraseMacroScopes + optionName == fieldName || optionName == `config) + +/-- Return which `#simulate` trace-bound fields were supplied by command syntax. -/ +private def simulateTraceBoundFieldsExplicit (cfgStx : Syntax) : Bool × Bool := + (simulateConfigHasField cfgStx `maxTraces, simulateConfigHasField cfgStx `maxSteps) + +/-- Resolve `#simulate` trace-bound fields, preserving explicit default literals. -/ +def resolveSimulateTraceBounds (cfg0 : ModelChecker.Simulation.SimulateConfig) + (commandHasMaxTraces commandHasMaxSteps : Bool) (optionMaxTraces optionMaxSteps : Nat) : Nat × Nat := + let maxTraces := if commandHasMaxTraces then cfg0.maxTraces else optionMaxTraces + let maxSteps := if commandHasMaxSteps then cfg0.maxSteps else optionMaxSteps + (maxTraces, maxSteps) + /-- Model checking mode: interpreted only, compiled only, or default (both with handoff). -/ inductive ModelCheckingMode where | interpreted @@ -630,6 +660,73 @@ def getModelCheckingMode (modeStx : Syntax) : ModelCheckingMode := | `(modelCheckMode| compiled) => .compiled | _ => .default +/-- Get all action label names for never-enabled action warnings. -/ +private def getActionLabelNames (mod : Module) : CommandElabM (List String) := do + let labelTypeName ← resolveGlobalConstNoOverload labelType + return mod.actions.map (fun a => s!"{labelTypeName}.{a.name}") |>.toList + +/-- Warn if the module contains transitions (which are slow to model check). -/ +private def warnAboutTransitions (mod : Module) : CommandElabM Unit := do + let transitions := mod.procedures.filter (·.info.isTransition) + if transitions.isEmpty then return + let names := ", ".intercalate (transitions.map (·.info.name.toString) |>.toList) + logWarning m!"Explicit state model checking of transitions is SLOW!\n\n\ + The current implementation enumerates all possible states and filters those satisfying \ + the transition relation. Your specification has {transitions.size} \ + transition{if transitions.size > 1 then "s" else ""}: {names}\n\n\ + Consider encoding transitions as imperative actions where possible." + +/-- Get the theory term, defaulting to `{}` if not provided and there are no theory fields. -/ +private def resolveTheoryTerm (cmdName : String) (theoryTermOpt : Option Term) + (mod : Module) (instTerm : Term) : CommandElabM Term := do + match theoryTermOpt with + | some t => pure t + | none => + unless mod.immutableComponents.isEmpty do + let fieldStrs := mod.immutableComponents.map (fun c => s!"{c.name} := ...") + let theoryExample := "{ " ++ ", ".intercalate fieldStrs.toList ++ " }" + throwError "This module has immutable fields, so you must specify the theory instantiation:\n\ + {cmdName} {instTerm} {theoryExample}" + `({}) + +/-- Prepend `name` with `mod.name`. -/ +private def mkIdentWithModName (mod : Module) (name : Name) : Ident := + Lean.mkIdent (mod.name ++ name) + +/-- Build search parameters for model checking / simulation. -/ +private def buildSearchParameters (mod : Module) (config : ModelCheckerConfig) : CommandElabM Term := do + let mkAssumption (sa : StateAssertion) : CommandElabM Term := + `($(mkIdent ``Veil.ModelChecker.TheoryProperty.mk) + ($(mkIdent `name) := $(quote sa.name)) + ($(mkIdent `property) := fun $(mkIdent `th) => $(mkIdentWithModName mod sa.name) $(mkIdent `th))) + -- Build SafetyProperty.mk syntax for a StateAssertion + let mkProp (sa : StateAssertion) : CommandElabM Term := + `($(mkIdent ``Veil.ModelChecker.SafetyProperty.mk) + ($(mkIdent `name) := $(quote sa.name)) + ($(mkIdent `property) := fun $(mkIdent `th) $(mkIdent `st) => $(mkIdentWithModName mod sa.name) $(mkIdent `th) $(mkIdent `st))) + let assumptionList ← `([$((← mod.assumptions.mapM mkAssumption)),*]) + let safetyList ← `([$((← mod.invariants.mapM mkProp)),*]) + -- FIXME: Only recognizing the first termination property might confuse users + let terminatingProp ← match mod.terminations[0]? with + | some t => mkProp t + | none => `($(mkIdent `default)) + let constraintList ← `([$((← mod.stateConstraints.mapM mkProp)),*]) + let earlyTermConds ← do + let base ← `([$(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.foundViolatingState), + $(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.assertionFailed), + $(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.deadlockOccurred)]) + if config.maxDepth > 0 then `($base ++ [$(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.reachedDepthBound) $(quote config.maxDepth)]) + else pure base + `({ $(mkIdent `assumptions):ident := $assumptionList, $(mkIdent `invariants):ident := $safetyList, $(mkIdent `terminating):ident := $terminatingProp, + $(mkIdent `stateConstraints):ident := $constraintList, + $(mkIdent `earlyTerminationConditions):ident := $earlyTermConds }) + +/-- Stable identity for a single compiled command invocation within a file. -/ +private def getCompiledCommandId (cmdName : String) (stx : Syntax) : CommandElabM String := do + let some startPos := stx.getPos? | throwError s!"Unexpected error: {cmdName} has no position" + let some endPos := stx.getTailPos? | throwError s!"Unexpected error: {cmdName} has no end position" + pure s!"{startPos.1}-{endPos.1}" + @[command_elab Veil.modelCheck] def elabModelCheck : CommandElab := fun stx => do -- Use dynamic trace class name for detailed profiling @@ -644,19 +741,6 @@ def elabModelCheck : CommandElab := fun stx => do let cfg := stx[4] elabModelCheckCore stx mode instTerm theoryTermOpt assumptionsHoldBy cfg where - /-- Get the theory term, defaulting to `{}` if not provided and there are no theory fields. - Throws a helpful error if theory fields exist but no term was provided. -/ - getTheoryTerm (theoryTermOpt : Option Term) (mod : Module) (instTerm : Term) : CommandElabM Term := do - match theoryTermOpt with - | some t => pure t - | none => - unless mod.immutableComponents.isEmpty do - let fieldStrs := mod.immutableComponents.map (fun c => s!"{c.name} := ...") - let theoryExample := "{ " ++ ", ".intercalate fieldStrs.toList ++ " }" - throwError "This module has immutable fields, so you must specify the theory instantiation:\n\ - #model_check {instTerm} {theoryExample}" - `({}) - /-- Generate the model source for compilation: 1. Insert `set_option veil.__modelCheckCompileMode true` after imports 2. Keep everything up to the point where the spec was finalized @@ -685,72 +769,21 @@ where let modelCheckCmd := String.Pos.Raw.extract src modelCheckStart modelCheckEnd return beforeImports ++ compileModePreamble ++ afterImportsToSpecFinalized ++ "\n" ++ modelCheckCmd ++ "\n" - /-- Prepend `name` with `mod.name`. Useful when expressions are printed out for debugging. -/ - mkIdentWithModName (mod : Module) (name : Name) : Ident := - Lean.mkIdent (mod.name ++ name) - - /-- Display a TraceDisplayViewer widget with the given result term. -/ - displayResultWidget (stx : Syntax) (resultTerm : Term) : CommandElabM Unit := do - let widgetExpr ← `(open ProofWidgets.Jsx in - ) - let html ← ← liftTermElabM <| ProofWidgets.HtmlCommand.evalCommandMHtml <| ← ``(ProofWidgets.HtmlEval.eval $widgetExpr) - liftCoreM <| Widget.savePanelWidgetInfo - (hash ProofWidgets.HtmlDisplayPanel.javascript) - (return json% { html: $(← Server.rpcEncode html) }) stx - - mkSearchParameters (mod : Module) (config : ModelCheckerConfig) : CommandElabM Term := do - let mkAssumption (sa : StateAssertion) : CommandElabM Term := - `($(mkIdent ``Veil.ModelChecker.TheoryProperty.mk) - ($(mkIdent `name) := $(quote sa.name)) - ($(mkIdent `property) := fun $(mkIdent `th) => $(mkIdentWithModName mod sa.name) $(mkIdent `th))) - -- Build SafetyProperty.mk syntax for a StateAssertion - let mkProp (sa : StateAssertion) : CommandElabM Term := - `($(mkIdent ``Veil.ModelChecker.SafetyProperty.mk) - ($(mkIdent `name) := $(quote sa.name)) - ($(mkIdent `property) := fun $(mkIdent `th) $(mkIdent `st) => $(mkIdentWithModName mod sa.name) $(mkIdent `th) $(mkIdent `st))) - let assumptionList ← `([$((← mod.assumptions.mapM mkAssumption)),*]) - let safetyList ← `([$((← mod.invariants.mapM mkProp)),*]) - -- FIXME: Only recognizing the first termination property might confuse users - let terminatingProp ← match mod.terminations[0]? with - | some t => mkProp t - | none => `($(mkIdent `default)) - let constraintList ← `([$((← mod.stateConstraints.mapM mkProp)),*]) - let earlyTermConds ← do - let base ← `([$(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.foundViolatingState), - $(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.assertionFailed), - $(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.deadlockOccurred)]) - if config.maxDepth > 0 then `($base ++ [$(mkIdent ``Veil.ModelChecker.EarlyTerminationCondition.reachedDepthBound) $(quote config.maxDepth)]) - else pure base - `({ $(mkIdent `assumptions):ident := $assumptionList, $(mkIdent `invariants):ident := $safetyList, $(mkIdent `terminating):ident := $terminatingProp, - $(mkIdent `stateConstraints):ident := $constraintList, - $(mkIdent `earlyTerminationConditions):ident := $earlyTermConds }) - /-- Build the core model checker call syntax (without parallel config). -/ mkModelCheckerCall (mod : Module) (config : ModelCheckerConfig) (instTerm theoryTerm : Term) : CommandElabM Term := do let inst := mkVeilImplementationDetailIdent `inst let th := mkVeilImplementationDetailIdent `th let instSortArgs ← (← mod.uninterpretedParamIdents).mapM fun paramIdent => `($inst.$(paramIdent)) - let sp ← mkSearchParameters mod config + let sp ← buildSearchParameters mod config -- Model checker call with type annotation to help inference -- Note: findReachable takes parallelCfg, progressInstanceId, and cancelToken as the last three args `((let $inst : $instantiationType := $instTerm let $th : $theoryIdent $instSortArgs* := $theoryTerm $(mkIdent ``Veil.ModelChecker.Concrete.findReachable) - ($(mkIdent `inhabσ) := $instInhabitedStateFieldConcreteType) - ($(mkIdentWithModName mod `enumerableTransitionSystem) $instSortArgs* $th) - $sp : _ → _ → _ → IO _)) - - /-- Warn if the module contains transitions (which are slow to model check). -/ - warnAboutTransitions (mod : Module) : CommandElabM Unit := do - let transitions := mod.procedures.filter (·.info.isTransition) - if transitions.isEmpty then return - let names := ", ".intercalate (transitions.map (·.info.name.toString) |>.toList) - logWarning m!"Explicit state model checking of transitions is SLOW!\n\n\ - The current implementation enumerates all possible states and filters those satisfying \ - the transition relation. Your specification has {transitions.size} \ - transition{if transitions.size > 1 then "s" else ""}: {names}\n\n\ - Consider encoding transitions as imperative actions where possible." + ($(mkIdent `inhabσ) := $instInhabitedStateFieldConcreteType) + ($(mkIdentWithModName mod `enumerableTransitionSystem) $instSortArgs* $th) + $sp : _ → _ → _ → IO _)) /-- Check that the provided theory satisfies all module assumptions by elaborating a proof obligation using the assembled `Assumptions` definition. @@ -777,7 +810,6 @@ where dsimp only [$assembledAssumptions:ident] $userTac:tactic) elabVeilCommand proofCmd - /-- Create an error JSON object. -/ errorJson (msg : String) : Json := Json.mkObj [("error", msg)] @@ -791,7 +823,10 @@ where /-- Handle internal mode: define and export the model checker result. -/ elabModelCheckInternalMode (mod : Module) (callExpr : Term) : CommandElabM Unit := do - elabVeilCommand (← `(def $(mkIdent `modelCheckerResult) (pcfg : Option Veil.ModelChecker.ParallelConfig) (progressInstanceId : Nat) (cancelToken : IO.CancelToken) := $callExpr pcfg progressInstanceId cancelToken)) + elabVeilCommand (← `(def $(mkIdent `modelCheckerResult) + (pcfg : Option Veil.ModelChecker.ParallelConfig) (progressInstanceId : Nat) + (cancelToken : IO.CancelToken) : IO Lean.Json := + Lean.toJson <$> $callExpr pcfg progressInstanceId cancelToken)) elabVeilCommand (← `(end $(mkIdent mod.name))) elabVeilCommand (← `(export $(mkIdent mod.name) ($(mkIdent `modelCheckerResult)))) @@ -808,12 +843,10 @@ where ModelChecker.Concrete.finishProgress instanceId (errorJson s!"Binary not found at {binPath}") return none - /-- Run the model checker binary and finish with result. Returns true if completed. -/ - runBinaryAndFinish (binPath : System.FilePath) (parallelCfg : Option ModelChecker.ParallelConfig) - (instanceId : Nat) (cancelToken : IO.CancelToken) - (assertionSources : Std.HashMap AssertionId AssertionSourceInfo) : IO Bool := do + /-- Run the compiled binary and return its JSON result if completed. -/ + runBinaryForJson (binPath : System.FilePath) (args : Array String) + (instanceId : Nat) (cancelToken : IO.CancelToken) : IO (Option Json) := do ModelChecker.Concrete.updateStatus instanceId "Running compiled binary..." - let args := parallelCfg.map (fun p => #[s!"{p.numSubTasks}", s!"{p.thresholdToParallel}"]) |>.getD #[] let child ← IO.Process.spawn { cmd := toString (binPath / "ModelCheckerMain"), args, stdin := .piped, stdout := .piped, stderr := .piped } @@ -826,30 +859,32 @@ where match Json.parse line >>= FromJson.fromJson? (α := ModelChecker.Concrete.Progress) with | .ok p => if let some refs ← ModelChecker.Concrete.getProgressRefs instanceId then refs.progressRef.modify fun old => - let historyPoint : ModelChecker.Concrete.ProgressHistoryPoint := { - timestamp := p.elapsedMs - diameter := p.diameter - statesFound := p.statesFound - distinctStates := p.distinctStates - queue := p.queue - } - { p with allActionLabels := old.allActionLabels, history := old.history.push historyPoint } + let history := match p.simulation with + | some _ => old.history + | none => + let historyPoint : ModelChecker.Concrete.ProgressHistoryPoint := { + timestamp := p.elapsedMs + diameter := p.diameter + statesFound := p.statesFound + distinctStates := p.distinctStates + queue := p.queue + } + old.history.push historyPoint + { p with allActionLabels := old.allActionLabels, history } | .error _ => stderrAccum.modify (· ++ line) let stdoutTask ← IO.asTask (prio := .dedicated) child.stdout.readToEnd let waitTask ← IO.asTask (prio := .dedicated) child.wait -- Monitor for cancellation while !(← IO.hasFinished waitTask) do - if ← checkCancelled cancelToken instanceId then child.kill; return false + if ← checkCancelled cancelToken instanceId then child.kill; return none IO.sleep 100 let stdout ← IO.ofExcept (← IO.wait stdoutTask) let exitCode ← IO.ofExcept (← IO.wait waitTask) let stderr ← stderrAccum.get if exitCode != 0 then ModelChecker.Concrete.finishProgress instanceId (errorJson s!"Binary exited with code {exitCode}{if stderr.isEmpty then "" else s!"\n{stderr}"}") - return true - let json := Json.parse stdout |>.toOption.getD (errorJson s!"Failed to parse output: {stdout.take 500}") - ModelChecker.Concrete.finishProgress instanceId (enrichJsonWithAssertions json assertionSources) - return true + return none + return some (Json.parse stdout |>.toOption.getD (errorJson s!"Failed to parse output: {stdout.take 500}")) /-- Elaborate the interpreted mode computation. Must be called synchronously. -/ elaborateInterpretedComputation (instanceId : Nat) (callExpr : Term) @@ -863,11 +898,6 @@ where Term.synthesizeSyntheticMVarsNoPostponing unsafe Meta.evalExpr (IO Lean.Json) (mkApp (mkConst ``IO) (mkConst ``Lean.Json)) (← instantiateMVars expr) - /-- Get all action label names for never-enabled action warnings. -/ - getActionLabelNames (mod : Module) : CommandElabM (List String) := do - let labelTypeName ← resolveGlobalConstNoOverload labelType - return mod.actions.map (fun a => s!"{labelTypeName}.{a.name}") |>.toList - /-- Log model checking result. -/ logModelCheckResult (stx : Syntax) (resultJson : Json) : CommandElabM Unit := do let msg := TraceDisplay.formatModelCheckingResult resultJson @@ -895,24 +925,43 @@ where logModelCheckResult ctx.stx json ModelChecker.Concrete.finishProgress ctx.instanceId json + modelCheckerCommandSpec : ModelChecker.Compilation.CompiledCommandSpec := { + exportedName := "modelCheckerResult" + supportsParallelConfig := true + } + + simulateCommandSpec : ModelChecker.Compilation.CompiledCommandSpec := { + exportedName := "simulateResult" + } + /-- Run the compiled binary and log the result. -/ runBinaryAndLogResult (ctx : ModelCheckContext) (buildFolder : System.FilePath) - (sourceFile : String) : CommandElabM Unit := do + (sourceFile : String) (command : ModelChecker.Compilation.CompiledCommandSpec) + (commandId : String) : CommandElabM Unit := do let some binPath ← verifyBinaryExists buildFolder ctx.instanceId | return - let _ ← runBinaryAndFinish binPath ctx.parallelCfg ctx.instanceId ctx.cancelToken ctx.assertionSources - ModelChecker.Compilation.markRegistryFinished sourceFile buildFolder + let args := ctx.parallelCfg.map (fun p => #[s!"{p.numSubTasks}", s!"{p.thresholdToParallel}"]) |>.getD #[] + let some json ← runBinaryForJson binPath args ctx.instanceId ctx.cancelToken | return + ModelChecker.Concrete.finishProgress ctx.instanceId (enrichJsonWithAssertions json ctx.assertionSources) + ModelChecker.Compilation.markRegistryFinished sourceFile command commandId buildFolder let some resultJson ← ModelChecker.Concrete.getResultJson ctx.instanceId | return logModelCheckResult ctx.stx resultJson /-- Compile the model. Returns the build folder path if compilation succeeded, none otherwise. -/ compileModel (mod : Module) (sourceFile : String) (modelSource : String) - (instanceId : Nat) : IO (Option System.FilePath) := do - let buildFolder ← ModelChecker.Compilation.createBuildFolder sourceFile modelSource mod.name.toString - ModelChecker.Compilation.markRegistryInProgress sourceFile instanceId buildFolder + (commandId : String) (instanceId : Nat) (cancelToken : IO.CancelToken) + (command : ModelChecker.Compilation.CompiledCommandSpec) : IO (Option System.FilePath) := do + let buildFolder ← ModelChecker.Compilation.createBuildFolder sourceFile modelSource mod.name.toString command commandId + ModelChecker.Compilation.markRegistryInProgress sourceFile command commandId instanceId buildFolder let result ← ModelChecker.Compilation.runProcessWithStatusCallback + sourceFile + command + commandId { cmd := "lake", args := #["build", "ModelCheckerMain"], cwd := buildFolder } + instanceId cancelToken (fun elapsedMs => ModelChecker.Concrete.updateCompilationElapsed instanceId elapsedMs) (fun line isError elapsedMs => ModelChecker.Concrete.updateCompilationLog instanceId elapsedMs line isError) + if result.interrupted then + return none if result.exitCode != 0 then ModelChecker.Concrete.updateCompilationStatus instanceId (.failed (mkCompilationErrorMsg result)) return none @@ -927,7 +976,7 @@ where let mod ← getCurrentModule (errMsg := "You cannot #model_check outside of a Veil module!") mod.throwIfSpecNotFinalized - let theoryTerm ← getTheoryTerm theoryTermOpt mod instTerm + let theoryTerm ← resolveTheoryTerm "#model_check" theoryTermOpt mod instTerm warnAboutTransitions mod let config ← elabModelCheckerConfig cfg @@ -980,13 +1029,15 @@ where -- dbg_trace "elabModelCheckCompiledMode" let ctx ← allocModelCheckContext mod stx parallelCfg let sourceFile ← getFileName + let commandId ← getCompiledCommandId "#model_check" stx let modelSource ← generateModelSource mod stx let compilationComputation ← Command.wrapAsyncAsSnapshot (fun () => do try - let some buildFolder ← compileModel mod sourceFile modelSource ctx.instanceId | return + let some buildFolder ← compileModel mod sourceFile modelSource commandId ctx.instanceId ctx.cancelToken + modelCheckerCommandSpec | return if ← checkCancelled ctx.cancelToken ctx.instanceId then return - runBinaryAndLogResult ctx buildFolder sourceFile + runBinaryAndLogResult ctx buildFolder sourceFile modelCheckerCommandSpec commandId catch e : Exception => handleModelCheckError ctx e ) ctx.cancelToken @@ -1001,6 +1052,7 @@ where -- dbg_trace "elabModelCheckWithHandoff" let ctx ← allocModelCheckContext mod stx parallelCfg let sourceFile ← getFileName + let commandId ← getCompiledCommandId "#model_check" stx let modelSource ← generateModelSource mod stx let ioComputation ← elaborateInterpretedComputation ctx.instanceId callExpr parallelCfg @@ -1022,10 +1074,11 @@ where let compilationCancelTk ← IO.CancelToken.new let compilationComputation ← Command.wrapAsyncAsSnapshot (fun () => do try - let some buildFolder ← compileModel mod sourceFile modelSource ctx.instanceId | return + let some buildFolder ← compileModel mod sourceFile modelSource commandId ctx.instanceId compilationCancelTk + modelCheckerCommandSpec | return -- Skip handoff if violation found or interpreted finished if (← ModelChecker.Concrete.isViolationFound ctx.instanceId) || (← IO.hasFinished interpretedTask) then - ModelChecker.Compilation.markRegistryFinished sourceFile buildFolder + ModelChecker.Compilation.markRegistryFinished sourceFile modelCheckerCommandSpec commandId buildFolder return -- Handoff to compiled binary ModelChecker.Concrete.requestHandoff ctx.instanceId @@ -1033,7 +1086,7 @@ where let _ ← IO.wait interpretedTask let some newCancelToken ← ModelChecker.Concrete.resetProgressForHandoff ctx.instanceId | return let ctxWithNewToken := { ctx with cancelToken := newCancelToken } - runBinaryAndLogResult ctxWithNewToken buildFolder sourceFile + runBinaryAndLogResult ctxWithNewToken buildFolder sourceFile modelCheckerCommandSpec commandId catch e : Exception => ModelChecker.Concrete.updateCompilationStatus ctx.instanceId (.failed s!"{← e.toMessageData.toString}") ) compilationCancelTk @@ -1042,4 +1095,222 @@ where ModelChecker.displayStreamingProgress stx ctx.instanceId +/-- Build the progress-aware simulator runtime call syntax. -/ +private def mkSimulatorRuntimeCall (mod : Module) (instTerm theoryTerm : Term) + (sp : Term) (cfg : ModelChecker.Simulation.SimulateConfig) : CommandElabM Term := do + let inst := mkVeilImplementationDetailIdent `inst + let th := mkVeilImplementationDetailIdent `th + let instSortArgs ← (← mod.uninterpretedParamIdents).mapM fun paramIdent => `($inst.$(paramIdent)) + let cfgTerm ← `($(mkIdent ``Veil.ModelChecker.Simulation.SimulateConfig.mk) + $(quote cfg.maxTraces) $(quote cfg.maxSteps) $(quote cfg.seed)) + `((let $inst : $instantiationType := $instTerm + let $th : $theoryIdent $instSortArgs* := $theoryTerm + $(mkIdent ``Veil.ModelChecker.Simulation.simulateWithProgress) + ($(mkIdentWithModName mod `enumerableTransitionSystem) $instSortArgs* $th) + $sp $th $cfgTerm : _ → _ → IO _)) + +/-- Build the simulator runtime call syntax with progress and cancellation hooks. -/ +private def mkSimulateJsonExpr (resultIdent : Ident) : CommandElabM Term := + `($(mkIdent ``Veil.ModelChecker.Simulation.SimulateResult.toDisplayJson) $resultIdent) + +private def generateCompiledModelSourcePrefix (mod : Module) (stx : Syntax) : CommandElabM String := do + let src := (← getFileMap).source + let afterImportsPos := ModelChecker.Compilation.findPosAfterImports src + let compileModePreamble := "\nset_option veil.__modelCheckCompileMode true\n" + let some specFinalizedAtStx := mod.specFinalizedAtStx + | throwError "Internal error: spec should be finalized before generating model source" + let some commandStart := stx.getPos? | throwError "Unexpected error: command has no position" + let modelCheckTriggeredFinalization := specFinalizedAtStx.getPos? == stx.getPos? + let specFinalizedAtPos := if modelCheckTriggeredFinalization + then commandStart + else specFinalizedAtStx.getTailPos?.getD commandStart + let beforeImports := String.Pos.Raw.extract src 0 afterImportsPos + let afterImportsToSpecFinalized := String.Pos.Raw.extract src afterImportsPos specFinalizedAtPos + return beforeImports ++ compileModePreamble ++ afterImportsToSpecFinalized ++ "\n" + +private def getSourceSlice (stx : Syntax) : CommandElabM String := do + let some startPos := stx.getPos? | throwError "Unexpected error: syntax has no start position" + let some endPos := stx.getTailPos? | throwError "Unexpected error: syntax has no end position" + return String.Pos.Raw.extract (← getFileMap).source startPos endPos + +private def generateSimulateModelSource (mod : Module) (stx : Syntax) + (cfg : ModelChecker.Simulation.SimulateConfig) : CommandElabM String := do + let srcPrefix ← generateCompiledModelSourcePrefix mod stx + let instSrc ← getSourceSlice stx[2] + let theorySrc ← if stx[3].isNone then pure " {}" else do + let raw ← getSourceSlice stx[3][0] + pure s!" {raw}" + let cmd := s!"#simulate {instSrc}{theorySrc} (maxTraces := {cfg.maxTraces}) (maxSteps := {cfg.maxSteps}) (seed := {cfg.seed})" + return srcPrefix ++ cmd ++ "\n" + +private def elaborateSimulateComputation (instanceId : Nat) (callExpr : Term) : CommandElabM (IO Lean.Json) := do + let resultIdent := mkVeilImplementationDetailIdent `simulateRuntimeResult + let jsonExpr ← mkSimulateJsonExpr resultIdent + let resultExpr ← `(do + let some refs ← Veil.ModelChecker.Concrete.getProgressRefs $(quote instanceId) | pure Lean.Json.null + let $resultIdent ← ($callExpr $(quote instanceId) refs.cancelToken) + pure $jsonExpr) + liftTermElabM do + let expr ← Term.elabTerm resultExpr none + Term.synthesizeSyntheticMVarsNoPostponing + unsafe Meta.evalExpr (IO Lean.Json) (mkApp (mkConst ``IO) (mkConst ``Lean.Json)) (← instantiateMVars expr) + +private def simulationResultWasCancelled (combinedJson : Json) : Bool := + match combinedJson.getObjValAs? String "result" |>.toOption with + | some "cancelled" => true + | _ => false + +private def finishWithSimulationResult (ctx : ModelCheckContext) (combinedJson : Json) : CommandElabM Unit := do + if simulationResultWasCancelled combinedJson then + liftIO <| ModelChecker.Concrete.cancelProgress ctx.instanceId combinedJson + else + elabModelCheck.finishWithResult ctx combinedJson + +private def runSimulateBinaryAndLogResult (ctx : ModelCheckContext) (buildFolder : System.FilePath) + (sourceFile : String) (commandId : String) : CommandElabM Unit := do + let some binPath ← elabModelCheck.verifyBinaryExists buildFolder ctx.instanceId | return + let some combinedJson ← elabModelCheck.runBinaryForJson binPath #[] ctx.instanceId ctx.cancelToken | return + ModelChecker.Compilation.markRegistryFinished sourceFile elabModelCheck.simulateCommandSpec commandId buildFolder + finishWithSimulationResult ctx combinedJson + +private def elabSimulateInternalMode (mod : Module) (callExpr : Term) : CommandElabM Unit := do + let resultIdent := mkVeilImplementationDetailIdent `simulateRuntimeResult + let jsonExpr ← mkSimulateJsonExpr resultIdent + elabVeilCommand (← `(def $(mkIdent `simulateResult) + (progressInstanceId : Nat) (cancelToken : IO.CancelToken) : IO Lean.Json := do + let $resultIdent ← ($callExpr progressInstanceId cancelToken) + pure $jsonExpr)) + elabVeilCommand (← `(end $(mkIdent mod.name))) + elabVeilCommand (← `(export $(mkIdent mod.name) ($(mkIdent `simulateResult)))) + +private def elabSimulateInterpretedMode (mod : Module) (stx : Syntax) (callExpr : Term) : CommandElabM Unit := do + let ctx ← elabModelCheck.allocModelCheckContext mod stx none + let ioComputation ← elaborateSimulateComputation ctx.instanceId callExpr + let computation ← Command.wrapAsyncAsSnapshot (fun () => do + try + if ← elabModelCheck.checkCancelled ctx.cancelToken ctx.instanceId then return + let combinedJson ← IO.ofExcept (← ioComputation.toIO') + finishWithSimulationResult ctx combinedJson + catch e : Exception => + elabModelCheck.handleModelCheckError ctx e + ) ctx.cancelToken + let task ← BaseIO.asTask (computation ()) (prio := .dedicated) + Command.logSnapshotTask { stx? := none, cancelTk? := ctx.cancelToken, task } + ModelChecker.displayStreamingProgress stx ctx.instanceId + +private def elabSimulateCompiledMode (mod : Module) (stx : Syntax) + (cfg : ModelChecker.Simulation.SimulateConfig) : CommandElabM Unit := do + let ctx ← elabModelCheck.allocModelCheckContext mod stx none + let sourceFile ← getFileName + let commandId ← getCompiledCommandId "#simulate" stx + let modelSource ← generateSimulateModelSource mod stx cfg + let compilationComputation ← Command.wrapAsyncAsSnapshot (fun () => do + try + let some buildFolder ← elabModelCheck.compileModel mod sourceFile modelSource commandId ctx.instanceId ctx.cancelToken + elabModelCheck.simulateCommandSpec | return + if ← elabModelCheck.checkCancelled ctx.cancelToken ctx.instanceId then return + runSimulateBinaryAndLogResult ctx buildFolder sourceFile commandId + catch e : Exception => + elabModelCheck.handleModelCheckError ctx e + ) ctx.cancelToken + let compilationTask ← BaseIO.asTask (compilationComputation ()) (prio := .dedicated) + Command.logSnapshotTask { stx? := none, cancelTk? := ctx.cancelToken, task := compilationTask } + ModelChecker.displayStreamingProgress stx ctx.instanceId + +private def elabSimulateWithHandoff (mod : Module) (stx : Syntax) (callExpr : Term) + (cfg : ModelChecker.Simulation.SimulateConfig) : CommandElabM Unit := do + let ctx ← elabModelCheck.allocModelCheckContext mod stx none + let sourceFile ← getFileName + let commandId ← getCompiledCommandId "#simulate" stx + let modelSource ← generateSimulateModelSource mod stx cfg + let ioComputation ← elaborateSimulateComputation ctx.instanceId callExpr + let compilationCancelTk ← IO.CancelToken.new + liftIO <| ModelChecker.Concrete.setCompilationCancelToken ctx.instanceId (some compilationCancelTk) + let finishCompilation (buildFolder : System.FilePath) : IO Unit := do + ModelChecker.Compilation.markRegistryFinished sourceFile elabModelCheck.simulateCommandSpec commandId buildFolder + ModelChecker.Concrete.setCompilationCancelToken ctx.instanceId none + let interpretedComputation ← Command.wrapAsyncAsSnapshot (fun () => do + try + let combinedJson ← IO.ofExcept (← ioComputation.toIO') + match (← ctx.cancelToken.isSet, ← ModelChecker.Concrete.checkHandoffRequested ctx.instanceId) with + | (true, false) => + if simulationResultWasCancelled combinedJson then + finishWithSimulationResult ctx combinedJson + else + ModelChecker.Concrete.cancelProgress ctx.instanceId + | (false, _) => finishWithSimulationResult ctx combinedJson + | (true, true) => pure () + catch e : Exception => + elabModelCheck.handleModelCheckError ctx e + ) ctx.cancelToken + let interpretedTask ← BaseIO.asTask (interpretedComputation ()) (prio := .dedicated) + Command.logSnapshotTask { stx? := none, cancelTk? := ctx.cancelToken, task := interpretedTask } + let compilationComputation ← Command.wrapAsyncAsSnapshot (fun () => do + try + let some buildFolder ← elabModelCheck.compileModel mod sourceFile modelSource commandId ctx.instanceId compilationCancelTk + elabModelCheck.simulateCommandSpec | do + ModelChecker.Concrete.setCompilationCancelToken ctx.instanceId none + return + if (← ModelChecker.Concrete.isViolationFound ctx.instanceId) || (← IO.hasFinished interpretedTask) || + (← ModelChecker.Concrete.isCancelled ctx.instanceId) then + finishCompilation buildFolder + return + ModelChecker.Concrete.requestHandoff ctx.instanceId + ctx.cancelToken.set + let _ ← IO.wait interpretedTask + if (← ctx.cancelToken.isSet) && !(← ModelChecker.Concrete.checkHandoffRequested ctx.instanceId) then + ModelChecker.Concrete.cancelProgress ctx.instanceId + finishCompilation buildFolder + return + if (← ModelChecker.Concrete.getResultJson ctx.instanceId).isSome || (← ModelChecker.Concrete.isCancelled ctx.instanceId) then + finishCompilation buildFolder + return + let some newCancelToken ← ModelChecker.Concrete.resetProgressForHandoff ctx.instanceId | return + ModelChecker.Concrete.setCompilationCancelToken ctx.instanceId none + let ctxWithNewToken := { ctx with cancelToken := newCancelToken } + runSimulateBinaryAndLogResult ctxWithNewToken buildFolder sourceFile commandId + catch e : Exception => + ModelChecker.Concrete.setCompilationCancelToken ctx.instanceId none + ModelChecker.Concrete.updateCompilationStatus ctx.instanceId (.failed s!"{← e.toMessageData.toString}") + ) compilationCancelTk + let compilationTask ← BaseIO.asTask (compilationComputation ()) (prio := .dedicated) + Command.logSnapshotTask { stx? := none, cancelTk? := compilationCancelTk, task := compilationTask } + ModelChecker.displayStreamingProgress stx ctx.instanceId + +@[command_elab Veil.simulate] +def elabSimulate : CommandElab := fun stx => do + withTraceNode `veil.perf.elaborator.simulate (fun _ => return "#simulate") do + let mode := getModelCheckingMode stx[1] + let instTerm : Term := ⟨stx[2]⟩ + let theoryTermOpt : Option Term := if stx[3].isNone then none else some ⟨stx[3][0]⟩ + let assumptionsHoldBy : Option (TSyntax `Lean.Parser.Tactic.tacticSeq) := + if stx[5].isNone then none else some ⟨stx[5][0][1]⟩ + let mod ← getCurrentModule (errMsg := "You cannot #simulate outside of a Veil module!") + mod.throwIfSpecNotFinalized + let theoryTerm ← resolveTheoryTerm "#simulate" theoryTermOpt mod instTerm + warnAboutTransitions mod + let simulateCfgStx := stx[4] + let cfg0 ← elabSimulateConfig simulateCfgStx + let opts ← getOptions + let (hasMaxTraces, hasMaxSteps) := simulateTraceBoundFieldsExplicit simulateCfgStx + let optionMaxTraces := veil.simulate.maxTraces.get opts + let optionMaxSteps := veil.simulate.maxSteps.get opts + let (maxTraces, maxSteps) := resolveSimulateTraceBounds cfg0 hasMaxTraces hasMaxSteps + optionMaxTraces optionMaxSteps + let seed ← liftIO <| if cfg0.seed == 0 then IO.rand 0 0xFFFFFFFFFFFFFFFF else pure cfg0.seed + let cfg : ModelChecker.Simulation.SimulateConfig := { cfg0 with maxTraces, maxSteps, seed } + let mcCfg : ModelCheckerConfig := { maxDepth := 0, sequential := false, parallelCfg := none } + if assumptionsHoldBy.isSome && !(← isModelCheckCompileMode) && !mod.assumptions.isEmpty then + elabModelCheck.checkTheorySatisfiesAssumptions mod instTerm theoryTerm assumptionsHoldBy + mod.ensureExecutableModelCheckerDefinitions + let sp ← buildSearchParameters mod mcCfg + let runtimeCallExpr ← mkSimulatorRuntimeCall mod instTerm theoryTerm sp cfg + if ← isModelCheckCompileMode then + elabSimulateInternalMode mod runtimeCallExpr + return + let effectiveMode := if (← liftIO isVeilOnlineEnv) then .interpreted else mode + match effectiveMode with + | .interpreted => elabSimulateInterpretedMode mod stx runtimeCallExpr + | .compiled => elabSimulateCompiledMode mod stx cfg + | .default => elabSimulateWithHandoff mod stx runtimeCallExpr cfg end Veil diff --git a/Veil/Frontend/DSL/Module/Syntax.lean b/Veil/Frontend/DSL/Module/Syntax.lean index 81b84348..d5a32ca2 100644 --- a/Veil/Frontend/DSL/Module/Syntax.lean +++ b/Veil/Frontend/DSL/Module/Syntax.lean @@ -373,4 +373,27 @@ scoped syntax (name := crFunction) kw_function : concreteRepField scoped syntax (name := concreteRepresentationDecl) "veil_set_field_representation " concreteRepField ident : command +/-- Run random-walk simulation on the current module. + Explores random traces to find shallow invariant violations quickly. + +## Execution Modes + +**Default behavior** (`#simulate`): +- Runs interpreted mode immediately and shows streaming progress +- Starts compilation in background +- When compilation finishes before interpreted mode does, restarts with the + compiled binary using the same chosen seed + +**Interpreted-only mode** (`#simulate interpreted`): +- Runs only interpreted mode without background compilation + +**Compiled-only mode** (`#simulate compiled`): +- Builds and runs the compiled binary directly + +Seed defaults to a generated value if omitted; the chosen seed is always shown +in output for reproducibility and reused consistently across mode handoff. + +Example: `#simulate {}` or `#simulate compiled {} (maxTraces := 100, seed := 42)` -/ +scoped syntax (name := simulate) "#simulate " (modelCheckMode)? term:max (term:max)? Parser.Tactic.optConfig (assumptionsHoldBy)? : command + end Veil diff --git a/Veil/Frontend/DSL/Module/Util/ForModelChecker.lean b/Veil/Frontend/DSL/Module/Util/ForModelChecker.lean index 795ca921..74bfc012 100644 --- a/Veil/Frontend/DSL/Module/Util/ForModelChecker.lean +++ b/Veil/Frontend/DSL/Module/Util/ForModelChecker.lean @@ -19,17 +19,43 @@ inductive Status | finished (buildDir : System.FilePath) deriving Inhabited -/-- Global state tracking compilation status for multiple models. -Keyed by the source file path (absolute path). -Uses `Std.Mutex` to prevent race conditions when multiple tasks access the registry. -/ -initialize compilationRegistry : Std.Mutex (Std.HashMap String Status) ← +/-- Description of a command that can be compiled into a generated executable. -/ +structure CompiledCommandSpec where + /-- Name of the generated definition that the compiled executable calls. -/ + exportedName : String + /-- Whether the generated definition accepts an optional parallel configuration. -/ + supportsParallelConfig : Bool := false + +/-- Registry key for one compiled command invocation. -/ +structure CompilationKey where + /-- Source file containing the compiled command invocation. -/ + sourceFile : String + /-- Generated definition called by the compiled executable. -/ + exportedName : String + /-- Identity of the specific command invocation within `sourceFile`. -/ + commandId : String + deriving BEq, Hashable, Inhabited + +/-- Global state tracking compilation status for multiple compiled commands. + Keyed by source file path, exported command name, and command identity so + different command invocations in the same file do not supersede each other. + Uses `Std.Mutex` to prevent race conditions when multiple tasks access the registry. -/ +initialize compilationRegistry : Std.Mutex (Std.HashMap CompilationKey Status) ← Std.Mutex.new {} @[inline] -def stillCurrentCont (sourceFile : String) (instanceId : Nat) (k : Std.AtomicT (Std.HashMap String Status) IO Unit) : IO Bool := +def mkCompilationKey (sourceFile : String) (command : CompiledCommandSpec) (commandId : String) : CompilationKey := { + sourceFile, + exportedName := command.exportedName, + commandId, +} + +@[inline] +def stillCurrentCont (sourceFile : String) (command : CompiledCommandSpec) (commandId : String) (instanceId : Nat) + (k : Std.AtomicT (Std.HashMap CompilationKey Status) IO Unit) : IO Bool := compilationRegistry.atomically fun ref => do let registry ← ref.get - match registry[sourceFile]? with + match registry[mkCompilationKey sourceFile command commandId]? with | some info => match info with | .inProgress id _ => if id == instanceId then k ref ; pure true else pure false @@ -37,27 +63,30 @@ def stillCurrentCont (sourceFile : String) (instanceId : Nat) (k : Std.AtomicT ( | none => pure false /-- Mark compilation as finished in the registry. -/ -def markRegistryFinished (sourceFile : String) (buildFolder : System.FilePath) : IO Unit := +def markRegistryFinished (sourceFile : String) (command : CompiledCommandSpec) (commandId : String) + (buildFolder : System.FilePath) : IO Unit := compilationRegistry.atomically fun ref => - ref.modify fun registry => registry.insert sourceFile (.finished buildFolder) + ref.modify fun registry => + registry.insert (mkCompilationKey sourceFile command commandId) (.finished buildFolder) /-- Mark compilation as in progress in the registry. -/ -def markRegistryInProgress (sourceFile : String) (instanceId : Nat) (buildFolder : System.FilePath) : IO Unit := +def markRegistryInProgress (sourceFile : String) (command : CompiledCommandSpec) (commandId : String) + (instanceId : Nat) (buildFolder : System.FilePath) : IO Unit := compilationRegistry.atomically fun ref => - ref.modify fun registry => registry.insert sourceFile (.inProgress instanceId buildFolder) + ref.modify fun registry => + registry.insert (mkCompilationKey sourceFile command commandId) (.inProgress instanceId buildFolder) /-- Base directory for model checker build folders. This is an absolute path. -/ def getBuildBaseDir : IO System.FilePath := do let pwd ← IO.currentDir return pwd / ".lake" / "model_checker_builds" -/-- Generate a build folder name based on the source file name, so that for the -same source file we get the same build folder. -/ -def generateBuildFolderName (sourceFile : String) : IO System.FilePath := do - -- Use the source file's stem (filename without extension) for readability +/-- Generate a build folder name based on the source file and exported command. -/ +def generateBuildFolderName (sourceFile : String) (command : CompiledCommandSpec) (_commandId : String) : IO System.FilePath := do let stem := System.FilePath.mk sourceFile |>.fileStem.getD "unrecognized_model" + let suffix := toString (hash (sourceFile ++ ":" ++ command.exportedName)) let baseDir ← getBuildBaseDir - return baseDir / stem + return baseDir / s!"{stem}_{command.exportedName}_{suffix}" /-- Template for the `lakefile.lean` in the temp project. Note that it does not only require the parent Veil project, but also *all the dependencies*; @@ -93,7 +122,7 @@ lean_exe ModelCheckerMain where /-- Template for the ModelCheckerMain.lean in the temp project. Takes the namespace of the specification to open scoped instances. -/ -def modelCheckerMainTemplate (specNamespace : String) : String := +def modelCheckerMainTemplate (specNamespace : String) (command : CompiledCommandSpec) : String := "import Model set_option maxHeartbeats 6400000 @@ -129,25 +158,29 @@ def main (args : List String) : IO Unit := do -- Instance ID is not used in compiled mode, pass 0 -- Cancel token is created locally; cancellation is handled by killing the process from outside let cancelTk ← IO.CancelToken.new - let res ← modelCheckerResult pcfg 0 cancelTk - IO.println s!\"{Lean.toJson res}\" + let res ← " ++ + (if command.supportsParallelConfig + then command.exportedName ++ " pcfg 0 cancelTk" + else command.exportedName ++ " 0 cancelTk") ++ " + IO.println s!\"{res}\" flushStdoutAndStderr IO.Process.forceExit 0 " /-- Create the temp build folder with all necessary files. -Returns the absolute path to the build folder. -/ -def createBuildFolder (sourceFile : String) (modelSource : String) (specNamespace : String) : IO System.FilePath := do +Returns the absolute path to the build folder. Generated inputs are overwritten +on each call while preserving the Lake build cache in the folder. -/ +def createBuildFolder (sourceFile : String) (modelSource : String) (specNamespace : String) + (command : CompiledCommandSpec) (commandId : String) : IO System.FilePath := do let veilPath ← IO.currentDir - let buildFolder ← generateBuildFolderName sourceFile - -- Create the build folder + let buildFolder ← generateBuildFolderName sourceFile command commandId IO.FS.createDirAll buildFolder -- Write the lakefile IO.FS.writeFile (buildFolder / "lakefile.lean") lakefileTemplate -- Write the model source (renamed to Model.lean) IO.FS.writeFile (buildFolder / "Model.lean") modelSource -- Write the ModelCheckerMain.lean - IO.FS.writeFile (buildFolder / "ModelCheckerMain.lean") (modelCheckerMainTemplate specNamespace) + IO.FS.writeFile (buildFolder / "ModelCheckerMain.lean") (modelCheckerMainTemplate specNamespace command) -- Create a minimal lean-toolchain file (copy from parent) let toolchainPath := veilPath / "lean-toolchain" if ← toolchainPath.pathExists then @@ -155,12 +188,6 @@ def createBuildFolder (sourceFile : String) (modelSource : String) (specNamespac IO.FS.writeFile (buildFolder / "lean-toolchain") toolchain return buildFolder -/-- Update elapsed time status for a progress instance. -/ -def updateElapsedTimeStatus (instanceId : Nat) (statusPrefix : String) : IO Unit := do - if let some refs ← ModelChecker.Concrete.getProgressRefs instanceId then - let elapsed := ModelChecker.formatElapsedTime (← refs.progressRef.get).elapsedMs - ModelChecker.Concrete.updateStatus instanceId s!"{statusPrefix} ({elapsed})" - /-- Result of running a compilation process. -/ structure ProcessResult where exitCode : UInt32 @@ -169,41 +196,11 @@ structure ProcessResult where interrupted : Bool := false deriving Inhabited -/-- Run a process with status updates, checking if compilation is still current or cancelled. - Returns the exit code, stdout, stderr, and whether it was interrupted. -/ -def runProcessWithStatus (sourceFile : String) (cfg : IO.Process.SpawnArgs) - (instanceId : Nat) (statusPrefix : String) (cancelToken : IO.CancelToken) : IO ProcessResult := do - let proc ← IO.Process.spawn { cfg with stdin := .piped, stdout := .piped, stderr := .piped } - -- Start reading stdout/stderr in background tasks to avoid blocking - let stdoutTask ← IO.asTask (prio := .dedicated) proc.stdout.readToEnd - let stderrTask ← IO.asTask (prio := .dedicated) proc.stderr.readToEnd - let waitTask ← IO.asTask (prio := .dedicated) proc.wait - let mut interrupted := false - while !(← IO.hasFinished waitTask) do - -- Check for explicit cancellation request - if ← cancelToken.isSet then - proc.kill - interrupted := true - break - -- Check if this compilation is still current (not superseded) - let current? ← stillCurrentCont sourceFile instanceId do - updateElapsedTimeStatus instanceId statusPrefix - unless current? do - proc.kill - interrupted := true - break - IO.sleep 100 - let stdout ← IO.ofExcept (← IO.wait stdoutTask) - let stderr ← IO.ofExcept (← IO.wait stderrTask) - match ← IO.wait waitTask with - | .ok exitCode => return { exitCode, stdout, stderr, interrupted } - | .error err => return { exitCode := 1, stdout, stderr := s!"{stderr}\nIO error: {err}", interrupted } - -/-- Run a process with callbacks for status updates and line-by-line output capture. - - `statusCallback` is called periodically (every 500ms) with the elapsed time in ms. - - `lineCallback` is called for each line of output (content, isError, elapsedMs). - This variant does not check for cancellation - it runs to completion. -/ -def runProcessWithStatusCallback (cfg : IO.Process.SpawnArgs) +/-- Run a process with callbacks for status updates and line-by-line output capture, +checking both explicit cancellation and whether this compilation is still current. -/ +def runProcessWithStatusCallback (sourceFile : String) (command : CompiledCommandSpec) (commandId : String) + (cfg : IO.Process.SpawnArgs) + (instanceId : Nat) (cancelToken : IO.CancelToken) (statusCallback : Nat → IO Unit) (lineCallback : String → Bool → Nat → IO Unit := fun _ _ _ => pure ()) : IO ProcessResult := do @@ -221,14 +218,24 @@ def runProcessWithStatusCallback (cfg : IO.Process.SpawnArgs) let stdoutTask ← IO.asTask (prio := .dedicated) (readLines proc.stdout stdoutAccum false) let stderrTask ← IO.asTask (prio := .dedicated) (readLines proc.stderr stderrAccum true) let waitTask ← IO.asTask (prio := .dedicated) proc.wait + let mut interrupted := false while !(← IO.hasFinished waitTask) do - statusCallback ((← IO.monoMsNow) - startTime) + if ← cancelToken.isSet then + proc.kill + interrupted := true + break + let current? ← stillCurrentCont sourceFile command commandId instanceId do + statusCallback ((← IO.monoMsNow) - startTime) + unless current? do + proc.kill + interrupted := true + break IO.sleep 500 let _ ← IO.wait stdoutTask let _ ← IO.wait stderrTask match ← IO.wait waitTask with - | .ok exitCode => return { exitCode, stdout := ← stdoutAccum.get, stderr := ← stderrAccum.get, interrupted := false } - | .error err => return { exitCode := 1, stdout := ← stdoutAccum.get, stderr := s!"{← stderrAccum.get}\nIO error: {err}", interrupted := false } + | .ok exitCode => return { exitCode, stdout := ← stdoutAccum.get, stderr := ← stderrAccum.get, interrupted } + | .error err => return { exitCode := 1, stdout := ← stdoutAccum.get, stderr := s!"{← stderrAccum.get}\nIO error: {err}", interrupted } -- /-- Clean up all build folders older than the specified age (in milliseconds). -/ -- def cleanupOldBuildFolders (maxAgeMs : Nat := 24 * 60 * 60 * 1000) : IO Nat := do diff --git a/VeilTest/Regression/CompilationRegistryKey.lean b/VeilTest/Regression/CompilationRegistryKey.lean new file mode 100644 index 00000000..92c173a2 --- /dev/null +++ b/VeilTest/Regression/CompilationRegistryKey.lean @@ -0,0 +1,57 @@ +import Veil + +open Veil.ModelChecker.Compilation + +#eval do + let sourceFile := "/tmp/compilation-registry-key.lean" + let modelCheckCommand : CompiledCommandSpec := { + exportedName := "modelCheckerResult" + supportsParallelConfig := true + } + let simulateCommand : CompiledCommandSpec := { + exportedName := "simulateResult" + } + let modelCheckFolderA ← generateBuildFolderName sourceFile modelCheckCommand "model-check-a" + let modelCheckFolderB ← generateBuildFolderName sourceFile modelCheckCommand "model-check-b" + let simulateFolderA ← generateBuildFolderName sourceFile simulateCommand "simulate-a" + assert! (toString modelCheckFolderA == toString modelCheckFolderB) + assert! (toString modelCheckFolderA != toString simulateFolderA) + let modelCheckBuildDirA := System.FilePath.mk "build/model-check-a" + let modelCheckBuildDirB := System.FilePath.mk "build/model-check-b" + let simulateBuildDirA := System.FilePath.mk "build/simulate-a" + let simulateBuildDirB := System.FilePath.mk "build/simulate-b" + let simulateBuildDirC := System.FilePath.mk "build/simulate-c" + markRegistryInProgress sourceFile modelCheckCommand "model-check-a" 1 modelCheckBuildDirA + markRegistryInProgress sourceFile modelCheckCommand "model-check-b" 2 modelCheckBuildDirB + markRegistryInProgress sourceFile simulateCommand "simulate-a" 3 simulateBuildDirA + markRegistryInProgress sourceFile simulateCommand "simulate-b" 4 simulateBuildDirB + markRegistryInProgress sourceFile simulateCommand "simulate-c" 5 simulateBuildDirC + assert! (← stillCurrentCont sourceFile modelCheckCommand "model-check-a" 1 (pure ())) + assert! (← stillCurrentCont sourceFile modelCheckCommand "model-check-b" 2 (pure ())) + assert! (← stillCurrentCont sourceFile simulateCommand "simulate-a" 3 (pure ())) + assert! (← stillCurrentCont sourceFile simulateCommand "simulate-b" 4 (pure ())) + assert! (← stillCurrentCont sourceFile simulateCommand "simulate-c" 5 (pure ())) + markRegistryFinished sourceFile modelCheckCommand "model-check-a" modelCheckBuildDirA + markRegistryFinished sourceFile modelCheckCommand "model-check-b" modelCheckBuildDirB + markRegistryFinished sourceFile simulateCommand "simulate-a" simulateBuildDirA + markRegistryFinished sourceFile simulateCommand "simulate-b" simulateBuildDirB + markRegistryFinished sourceFile simulateCommand "simulate-c" simulateBuildDirC + +#eval do + let sourceFile := "/tmp/compilation-build-folder-cache.lean" + let command : CompiledCommandSpec := { + exportedName := "simulateResult" + } + let firstSource := "namespace CacheFirst\nend CacheFirst\n" + let secondSource := "namespace CacheSecond\nend CacheSecond\n" + let firstFolder ← createBuildFolder sourceFile firstSource "CacheFirst" command "simulate-cache" + let cacheDir := firstFolder / ".lake" / "build" + IO.FS.createDirAll cacheDir + let cacheSentinel := cacheDir / "cache-sentinel" + IO.FS.writeFile cacheSentinel "cached" + let secondFolder ← createBuildFolder sourceFile secondSource "CacheSecond" command "simulate-cache" + assert! (toString firstFolder == toString secondFolder) + assert! (← cacheSentinel.pathExists) + assert! ((← IO.FS.readFile (secondFolder / "Model.lean")) == secondSource) + assert! ((← IO.FS.readFile (secondFolder / "ModelCheckerMain.lean")) == modelCheckerMainTemplate "CacheSecond" command) + assert! ((← IO.FS.readFile (secondFolder / "lakefile.lean")) == lakefileTemplate) diff --git a/VeilTest/Regression/MultipleSimulate.lean b/VeilTest/Regression/MultipleSimulate.lean new file mode 100644 index 00000000..e32fd814 --- /dev/null +++ b/VeilTest/Regression/MultipleSimulate.lean @@ -0,0 +1,28 @@ +import Veil + +veil module MultipleSimulate + +type node + +relation flag : node -> Bool + +after_init { + flag N := false +} + +action set_flag (n : node) { + flag n := true +} + +invariant [bounded] ∀ n, flag n -> flag n + +#guard_msgs(drop warning) in +#gen_spec + +#guard_msgs(drop info) in +#simulate interpreted { node := Fin 2 } {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +#guard_msgs(drop info) in +#simulate interpreted { node := Fin 2 } {} (seed := 2) (maxTraces := 1) (maxSteps := 1) + +end MultipleSimulate diff --git a/VeilTest/Regression/SimulateAssertionFailure.lean b/VeilTest/Regression/SimulateAssertionFailure.lean new file mode 100644 index 00000000..baeb7bba --- /dev/null +++ b/VeilTest/Regression/SimulateAssertionFailure.lean @@ -0,0 +1,39 @@ +import Veil + +set_option linter.unusedVariables false + +veil module SimulateAssertionFailure + +type node + +relation pending : node -> node -> Bool + +#gen_state + +after_init { + pending M N := false +} + +action send (n next : node) { + assert false + pending n next := true +} + +invariant true + +/-- error: This assertion might fail when called from send -/ +#guard_msgs in +#gen_spec + +/-- +error: ❌ Violation: assertion_failure + State 0 (via init): + pending = [] + State 1 (via send(n=0, next=0)): + pending = [] +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 2 } {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +end SimulateAssertionFailure diff --git a/VeilTest/Regression/SimulateAssumptions.lean b/VeilTest/Regression/SimulateAssumptions.lean new file mode 100644 index 00000000..f27a36d4 --- /dev/null +++ b/VeilTest/Regression/SimulateAssumptions.lean @@ -0,0 +1,119 @@ +import Veil + +set_option linter.unusedVariables false + +veil module SimulateAssumptionsTest + +type node + +immutable relation leader : node → Bool +relation flag : node → Bool + +#gen_state + +assumption ∀ (n1 n2 : node), leader n1 ∧ leader n2 → n1 = n2 + +after_init { + flag N := false +} + +action do_something (n : node) { + require leader n + flag n := true +} + +invariant true + +#gen_spec + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 3 } { leader := fun n => n == (0 : Fin 3) } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + assumptions_hold_by native_decide + +/-- +error: Tactic `native_decide` evaluated that the proposition + assumption_0 { leader := fun n => n == 0 || n == 1 } +is false +--- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 3 } { leader := fun n => n == (0 : Fin 3) || n == (1 : Fin 3) } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + assumptions_hold_by native_decide + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 3 } { leader := fun n => n == (0 : Fin 3) || n == (1 : Fin 3) } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 3 } { leader := fun n => n == (0 : Fin 3) } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + assumptions_hold_by decide + +#guard_msgs(drop info, drop warning) in +#simulate interpreted { node := Fin 3 } { leader := fun n => n == (0 : Fin 3) } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + assumptions_hold_by native_decide + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 3 } { leader := fun n => n == (0 : Fin 3) } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + assumptions_hold_by native_decide + +end SimulateAssumptionsTest + +veil module SimulateAssumptionsCustomProof + +type node + +immutable function weight : node → Nat + +relation active : node → Bool + +#gen_state + +assumption ∀ (n : node), 0 < weight n +assumption ∀ (n1 n2 : node), weight n1 = weight n2 → n1 = n2 + +after_init { + active N := false +} + +action activate (n : node) { + active n := true +} + +invariant true + +#gen_spec + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { node := Fin 3 } { weight := fun (n : Fin 3) => n.val + 1 } + (seed := 1) (maxTraces := 1) (maxSteps := 1) + assumptions_hold_by + constructor <;> decide + +end SimulateAssumptionsCustomProof diff --git a/VeilTest/Regression/SimulateCompiledSmoke.lean b/VeilTest/Regression/SimulateCompiledSmoke.lean new file mode 100644 index 00000000..3d5c65b8 --- /dev/null +++ b/VeilTest/Regression/SimulateCompiledSmoke.lean @@ -0,0 +1,24 @@ +import Veil + +veil module SimulateCompiledSmoke + +individual flag : Bool + +#gen_state + +after_init { + flag := false +} + +action set_flag { + flag := true +} + +invariant [safe_flag] true + +#gen_spec + +#guard_msgs(drop info, drop warning) in +#simulate compiled {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +end SimulateCompiledSmoke diff --git a/VeilTest/Regression/SimulateConfigDefaults.lean b/VeilTest/Regression/SimulateConfigDefaults.lean new file mode 100644 index 00000000..2e460444 --- /dev/null +++ b/VeilTest/Regression/SimulateConfigDefaults.lean @@ -0,0 +1,85 @@ +import Veil + +open Veil.ModelChecker.Simulation + +example : + Veil.resolveSimulateTraceBounds + { maxTraces := 10000, maxSteps := 100, seed := 0 } + true true 7 3 = (10000, 100) := rfl + +example : + Veil.resolveSimulateTraceBounds + { maxTraces := 10000, maxSteps := 100, seed := 0 } + false false 7 3 = (7, 3) := rfl + +example : + Veil.resolveSimulateTraceBounds + { maxTraces := 10000, maxSteps := 100, seed := 0 } + true false 7 3 = (10000, 3) := rfl + +example : + Veil.resolveSimulateTraceBounds + { maxTraces := 10000, maxSteps := 100, seed := 0 } + false true 7 3 = (7, 100) := rfl + +veil module SimulateConfigDefaults + +individual flag : Bool +individual tripped : Bool + +#gen_state + +after_init { + flag := false + tripped := false +} + +action set_flag { + require !flag + flag := true +} + +action trip { + require flag + tripped := true +} + +invariant [still_safe] ¬ tripped + +#gen_spec + +set_option veil.simulate.maxSteps 1 in +/-- +error: ❌ Violation: safety_failure (violates: still_safe) + State 0 (via init): + flag = false + tripped = false + State 1 (via set_flag): + flag = true + tripped = false + State 2 (via trip): + flag = true + tripped = true +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 100) + +set_option veil.simulate.maxSteps 1 in +/-- +error: ❌ Violation: safety_failure (violates: still_safe) + State 0 (via init): + flag = false + tripped = false + State 1 (via set_flag): + flag = true + tripped = false + State 2 (via trip): + flag = true + tripped = true +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (config := { maxTraces := 1, maxSteps := 100, seed := 1 }) + +end SimulateConfigDefaults diff --git a/VeilTest/Regression/SimulateDeadlock.lean b/VeilTest/Regression/SimulateDeadlock.lean new file mode 100644 index 00000000..15d36852 --- /dev/null +++ b/VeilTest/Regression/SimulateDeadlock.lean @@ -0,0 +1,31 @@ +import Veil + +veil module SimulateDeadlock + +individual stuck : Bool + +#gen_state + +after_init { + stuck := true +} + +invariant true +termination false = true + +/-- +warning: you have not defined any actions for this specification; did you forget? +-/ +#guard_msgs in +#gen_spec + +/-- +error: ❌ Violation: deadlock + State 0 (via init): + stuck = true +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +end SimulateDeadlock diff --git a/VeilTest/Regression/SimulateEmptyFilteredInitStates.lean b/VeilTest/Regression/SimulateEmptyFilteredInitStates.lean new file mode 100644 index 00000000..0af484bc --- /dev/null +++ b/VeilTest/Regression/SimulateEmptyFilteredInitStates.lean @@ -0,0 +1,26 @@ +import Veil + +veil module SimulateEmptyFilteredInitStates + +after_init { + pure () +} + +invariant true + +state_constraint [no_initial_states] False + +/-- +warning: you have not defined any actions for this specification; did you forget? +-/ +#guard_msgs in +#gen_spec + +/-- +info: ✅ No initial states available after applying state constraints +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 5) (maxSteps := 1) + +end SimulateEmptyFilteredInitStates diff --git a/VeilTest/Regression/SimulateEmptySpec.lean b/VeilTest/Regression/SimulateEmptySpec.lean new file mode 100644 index 00000000..f3958ec5 --- /dev/null +++ b/VeilTest/Regression/SimulateEmptySpec.lean @@ -0,0 +1,24 @@ +import Veil + +veil module SimulateEmptySpec + +after_init { + pure () +} + +invariant true + +/-- +warning: you have not defined any actions for this specification; did you forget? +-/ +#guard_msgs in +#gen_spec + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted { } {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +end SimulateEmptySpec diff --git a/VeilTest/Regression/SimulateModes.lean b/VeilTest/Regression/SimulateModes.lean new file mode 100644 index 00000000..bb0f3e38 --- /dev/null +++ b/VeilTest/Regression/SimulateModes.lean @@ -0,0 +1,51 @@ +import Veil + +veil module SimulateModes + +individual flag : Bool + +#gen_state + +after_init { + flag := false +} + +action set_flag { + flag := true +} + +invariant [safe_flag] true + +#gen_spec + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +#guard_msgs(drop info, drop warning) in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +set_option veil.simulate.maxTraces 1 in +set_option veil.simulate.maxSteps 1 in +#guard_msgs(drop info, drop warning) in +#simulate interpreted {} + +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +set_option veil.simulate.maxTraces 2 in +/-- +info: ✅ No violation in 1 traces +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (config := { maxTraces := 1, maxSteps := 1, seed := 1 }) + +end SimulateModes diff --git a/VeilTest/Regression/SimulateResultJson.lean b/VeilTest/Regression/SimulateResultJson.lean new file mode 100644 index 00000000..8f9744d1 --- /dev/null +++ b/VeilTest/Regression/SimulateResultJson.lean @@ -0,0 +1,70 @@ +import Veil + +open Veil.ModelChecker +open Veil.ModelChecker.Simulation + +/-- +info: {"depth":0,"elapsed_ms":0,"max_traces":3,"result":"no_violation_found","seed":1,"traces_run":3} +-/ +#guard_msgs in +#eval IO.println <| (Lean.toJson ({ + result := none + tracesRun := 3 + maxTraces := 3 + elapsedMs := 0 + seed := 1 +} : SimulateResult Unit Unit Unit)).compress + +/-- +info: {"depth":0,"elapsed_ms":0,"max_traces":3,"result":"no_violation_found","seed":1,"traces_run":3} +-/ +#guard_msgs in +#eval IO.println <| (SimulateResult.toDisplayJson ({ + result := none + tracesRun := 3 + maxTraces := 3 + elapsedMs := 0 + seed := 1 +} : SimulateResult Unit Unit Unit)).compress + +/-- +info: {"depth":0,"elapsed_ms":0,"max_traces":3,"result":"no_violation_found","seed":1,"termination_reason":{"kind":"no_initial_states"},"traces_run":0} +-/ +#guard_msgs in +#eval IO.println <| (Lean.toJson ({ + result := none + tracesRun := 0 + maxTraces := 3 + elapsedMs := 0 + seed := 1 + terminationReason := some .noInitialStates +} : SimulateResult Unit Unit Unit)).compress + +/-- +info: {"depth":0,"elapsed_ms":12,"max_traces":10,"result":"cancelled","seed":7,"traces_run":5} +-/ +#guard_msgs in +#eval IO.println <| (Lean.toJson ({ + result := some .cancelled + tracesRun := 5 + maxTraces := 10 + elapsedMs := 12 + seed := 7 +} : SimulateResult Unit Unit Unit)).compress + +/-- +info: {"depth":2,"elapsed_ms":0,"max_traces":3,"result":"found_violation","seed":1,"state_fingerprint":null,"trace":{"states":[{"fields":"()","index":0,"transition":"after_init"},{"fields":"()","index":1,"transition":"()"},{"failing":true,"fields":"()","index":2,"transition":"()"}],"theory":"()"},"traces_run":1,"violation":{"exception_id":5,"kind":"assertion_failure"}} +-/ +#guard_msgs in +#eval IO.println <| (Lean.toJson ({ + result := some (.foundViolation (.assertionFailure 5) ({ + theory := () + initialState := () + steps := #[{ transitionLabel := (), nextState := () }] + failingStep := some { transitionLabel := (), nextState := () } + } : Trace Unit Unit Unit)) + tracesRun := 1 + maxTraces := 3 + elapsedMs := 0 + seed := 1 +} : SimulateResult Unit Unit Unit)).compress diff --git a/VeilTest/Regression/SimulateViolationModes.lean b/VeilTest/Regression/SimulateViolationModes.lean new file mode 100644 index 00000000..2cdae613 --- /dev/null +++ b/VeilTest/Regression/SimulateViolationModes.lean @@ -0,0 +1,47 @@ +import Veil + +veil module SimulateViolationModes + +individual flag : Bool + +#gen_state + +after_init { + flag := false +} + +action set_flag { + flag := true +} + +invariant [safe_flag] ¬ flag + +#gen_spec + +/-- +error: ❌ Violation: safety_failure (violates: safe_flag) + State 0 (via init): + flag = false + State 1 (via set_flag): + flag = true +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +#guard_msgs(drop info, drop warning) in +set_option veil.violationIsError false in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +/-- +error: ❌ Violation: safety_failure (violates: safe_flag) + State 0 (via init): + flag = false + State 1 (via set_flag): + flag = true +Seed: 1 +-/ +#guard_msgs in +#simulate interpreted {} {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + +end SimulateViolationModes diff --git a/VeilTest/RequiresGenSpec.lean b/VeilTest/RequiresGenSpec.lean index cb4fcf73..31d448bc 100644 --- a/VeilTest/RequiresGenSpec.lean +++ b/VeilTest/RequiresGenSpec.lean @@ -3,8 +3,9 @@ import Veil /-! # Tests that commands requiring finalized spec throw errors without #gen_spec -These tests verify that `#check_invariants`, `#model_check`, and `sat trace`/`unsat trace` -all throw an appropriate error message when called before `#gen_spec`. +These tests verify that `#check_invariants`, `#model_check`, `#simulate`, and +`sat trace`/`unsat trace` all throw an appropriate error message when called +before `#gen_spec`. -/ veil module TestCheckInvariants @@ -49,6 +50,25 @@ invariant ¬ flag end TestModelCheck +veil module TestSimulate + +individual flag : Bool + +#gen_state + +after_init { flag := false } + +action set_flag { flag := true } + +invariant ¬ flag + +/-- error: The specification of module TestSimulate has not been finalized. Please call #gen_spec first! -/ +#guard_msgs in +#simulate interpreted { } + +end TestSimulate + + veil module TestSatTrace individual flag : Bool diff --git a/VeilTest/UninterpretedParameter.lean b/VeilTest/UninterpretedParameter.lean index 417a3d76..1ab4e343 100644 --- a/VeilTest/UninterpretedParameter.lean +++ b/VeilTest/UninterpretedParameter.lean @@ -34,4 +34,7 @@ invariant [bounded] ∀ (x : node), counter x ≤ n #model_check interpreted { node := Fin 2, n := 1, color := Fin 2, m := ⟨1, by decide⟩ } {} +#guard_msgs(drop info) in +#simulate interpreted { node := Fin 2, n := 1, color := Fin 2, m := ⟨1, by decide⟩ } {} (seed := 1) (maxTraces := 1) (maxSteps := 1) + end TestParameter diff --git a/widget/src/traceDisplay.tsx b/widget/src/traceDisplay.tsx index 32d4a6f1..c7856fe1 100644 --- a/widget/src/traceDisplay.tsx +++ b/widget/src/traceDisplay.tsx @@ -45,13 +45,17 @@ interface Violation { } interface EarlyTerminationCondition { - kind: "found_violating_state" | "deadlock_occurred" | "reached_depth_bound"; + kind: "found_violating_state" | "deadlock_occurred" | "reached_depth_bound" | "reached_trace_limit"; depth?: number; + traces_run?: number; + max_traces?: number; } interface TerminationReason { - kind: "explored_all_reachable_states" | "early_termination"; + kind: "explored_all_reachable_states" | "early_termination" | "reached_trace_limit" | "no_initial_states"; condition?: EarlyTerminationCondition; + traces_run?: number; + max_traces?: number; } interface TraceData { @@ -71,15 +75,22 @@ type ModelCheckingResult = result: "found_violation"; violation: Violation; trace: TraceData | null; + seed?: number; } | { result: "no_violation_found"; - explored_states: number; - termination_reason: TerminationReason; + explored_states?: number; + termination_reason?: TerminationReason; + traces_run?: number; + max_traces?: number; trace?: TraceData | null; + seed?: number; } | { result: "cancelled"; + traces_run?: number; + max_traces?: number; + seed?: number; } | { // Trace-only data without a result (for displaying execution traces) @@ -297,15 +308,30 @@ const ResultHeader: React.FC<{ violation?: Violation; exploredStates?: number; terminationReason?: TerminationReason; -}> = ({ resultType, violation, exploredStates, terminationReason }) => { + tracesRun?: number; + maxTraces?: number; + seed?: number; +}> = ({ resultType, violation, exploredStates, terminationReason, tracesRun, maxTraces, seed }) => { + const seedDetails = seed !== undefined ? ( +
+ Seed: {seed} +
+ ) : null; + if (resultType === "cancelled") { + const details = tracesRun !== undefined && maxTraces !== undefined + ? `Checked ${tracesRun}/${maxTraces} traces before cancellation` + : tracesRun !== undefined + ? `Checked ${tracesRun} traces before cancellation` + : 'Run was cancelled before completion'; return (
⊘ Cancelled
- Model checking was cancelled before completion + {details}
+ {seedDetails}
); } @@ -344,6 +370,7 @@ const ResultHeader: React.FC<{ Location: {violation.assertion_info.moduleName}.{violation.assertion_info.procedureName} (line {violation.assertion_info.line}, column {violation.assertion_info.column})
)} + {seedDetails}
); } @@ -353,10 +380,32 @@ const ResultHeader: React.FC<{ const countSuffix = count !== undefined ? ` (explored ${count} states)` : ''; const countText = count !== undefined ? `Explored ${count} states` : null; - if (!reason) return countText; + if (!reason) { + if (tracesRun !== undefined && maxTraces !== undefined) { + return `Checked ${tracesRun}/${maxTraces} traces`; + } + if (tracesRun !== undefined) { + return `Checked ${tracesRun} traces`; + } + return countText; + } if (reason.kind === "explored_all_reachable_states") { return count !== undefined ? `Explored all reachable states (${count})` : `Explored all reachable states`; } + if (reason.kind === "reached_trace_limit") { + const tracesRun = reason.traces_run; + const maxTraces = reason.max_traces; + if (tracesRun !== undefined && maxTraces !== undefined) { + return `Checked ${tracesRun}/${maxTraces} traces`; + } + if (tracesRun !== undefined) { + return `Checked ${tracesRun} traces`; + } + return `Checked configured trace budget`; + } + if (reason.kind === "no_initial_states") { + return `No initial states available after applying state constraints`; + } if (reason.kind === "early_termination" && reason.condition) { switch (reason.condition.kind) { case "found_violating_state": @@ -365,6 +414,17 @@ const ResultHeader: React.FC<{ return `Stopped: deadlock occurred${countSuffix}`; case "reached_depth_bound": return `Reached depth bound ${reason.condition.depth}${countSuffix}`; + case "reached_trace_limit": + if (tracesRun !== undefined && maxTraces !== undefined) { + return `Checked ${tracesRun}/${maxTraces} traces`; + } + if (reason.condition.traces_run !== undefined && reason.condition.max_traces !== undefined) { + return `Checked ${reason.condition.traces_run}/${reason.condition.max_traces} traces`; + } + if (reason.condition.traces_run !== undefined) { + return `Checked ${reason.condition.traces_run} traces`; + } + return `Checked configured trace budget`; default: return `Early termination${countSuffix}`; } @@ -383,6 +443,7 @@ const ResultHeader: React.FC<{ {terminationText}
)} + {seedDetails} ); }; @@ -784,17 +845,26 @@ const ModelCheckerView: React.FC = ({ {'result' in result && ( <> {result.result === "cancelled" ? ( - + ) : result.result === "no_violation_found" ? ( ) : ( )}