feat: add #simulate command#6
Conversation
|
Thank you, @rnbguy! This looks good. I'll have time to look at this more closely and merge it later in the week, after the OOPSLA deadline. (For future maintainability, I want to make sure However, I'm wondering whether you're running into a bug with By default, the way For me, What do you see when you run 
|
|
hey @dranov ! Good luck with OOPSLA deadline 🍀 I am just playing around with Veil 😄 so, there is no rush. You're correct. I was using CLI I just ran with
Thanks for taking the time to point this out. 🙌🏼 |
rnbguy
force-pushed
the
feat/simulate
branch
2 times, most recently
from
211e20b to
f822ebe
Compare
|
@rnbguy Apologies for the delay. I'll let @zqy1018 handle integrating this. He developed and is in charge of the model checker in Veil. We'd want |
|
hey @zqy1018, the PR is ready for review.
I also re-did the benchmark again from the above.
|
|
Great, thanks! I'll take a look now. |
| deriving Inhabited, Repr | ||
|
|
||
| structure SimulateResult (ρ σ κ : Type) where | ||
| result : ModelCheckingResult ρ σ κ Unit |
There was a problem hiding this comment.
The use of Unit here feels a bit awkward. Would it make more sense to introduce a dedicated inductive type instead? For example, like:
inductive SimulationResult (ρ σ κ : Type) where
| foundViolation (violation : ViolationKind) (viaTrace : Trace ρ σ κ)
| cancelled
Since according to how ModelCheckingResult ρ σ κ Unit is produced in simulateOnceLoop, the noViolationFound constructor is not used.
There was a problem hiding this comment.
yea. it's true that I tried to reuse some types from ModelCheck. I will keep things separate in later commits. For now, I will focus on your individual review comments.
| @[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 |
There was a problem hiding this comment.
There seems to be duplication here: violatedInvariantNames overlaps with how safetyViolations is computed in checkViolationsAndMaybeTerminate from Veil/Core/Tools/ModelChecker/Concrete/Core.lean. Can you move violatedInvariantNames to Veil/Core/Tools/ModelChecker/Interface.lean and use it in checkViolationsAndMaybeTerminate?
| @[inline] | ||
| def filterInitStatesByConstraints {ρ σ κ : Type} {th₀ : ρ} | ||
| (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) | ||
| (params : SearchParameters ρ σ) (th : ρ) : List σ := | ||
| if params.stateConstraints.isEmpty then sys.initStates | ||
| else sys.initStates.filter (params.satisfiesConstraints th) | ||
|
|
||
| @[inline] | ||
| def filterOutcomesByConstraints {ρ σ κ : Type} {th₀ : ρ} | ||
| (sys : EnumerableTransitionSystem ρ (List ρ) σ (List σ) Int κ (List (κ × ExecutionOutcome Int σ)) th₀) | ||
| (params : SearchParameters ρ σ) (th : ρ) (st : σ) : List (κ × ExecutionOutcome Int σ) := | ||
| if params.stateConstraints.isEmpty then | ||
| sys.tr th st | ||
| else | ||
| (sys.tr th st).filter fun (_, outcome) => | ||
| match outcome with | ||
| | .success st' => params.satisfiesConstraints th st' | ||
| | .assertionFailure _ st' => params.satisfiesConstraints th st' | ||
| | .divergence => true |
There was a problem hiding this comment.
This overlaps with the beginning let sys part of findReachable from Veil/Core/Tools/ModelChecker/Concrete/Checker.lean. Actually, the state constraints should only be used once throughout the simulation (and also model checking), namely initially using the state constraints to compute a restricted EnumerableTransitionSystem, and then never touch state constraints in the following code. This is exhibited in the code of findReachable. Can you do the same for simulation?
| private def earlyTerminationReasonToJson (reason : EarlyTerminationReason Unit) : Json := | ||
| match reason with | ||
| | .foundViolatingState _ violates => Json.mkObj [ | ||
| ("kind", "found_violating_state"), | ||
| ("state_fingerprint", Json.null), | ||
| ("violates", toJson violates) | ||
| ] | ||
| | .deadlockOccurred _ => Json.mkObj [ | ||
| ("kind", "deadlock_occurred"), | ||
| ("state_fingerprint", Json.null) | ||
| ] | ||
| | .assertionFailed _ exId => Json.mkObj [ | ||
| ("kind", "assertion_failed"), | ||
| ("state_fingerprint", Json.null), | ||
| ("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")] | ||
|
|
||
| private def terminationReasonToJson (reason : TerminationReason Unit) : Json := | ||
| match reason with | ||
| | .exploredAllReachableStates => Json.mkObj [("kind", "explored_all_reachable_states")] | ||
| | .earlyTermination condition => Json.mkObj [ | ||
| ("kind", "early_termination"), | ||
| ("condition", earlyTerminationReasonToJson condition) | ||
| ] | ||
|
|
||
| private def resultToJson {ρ σ κ : Type} [ToJson ρ] [ToJson σ] [ToJson κ] | ||
| (result : ModelCheckingResult ρ σ κ Unit) : Json := | ||
| match result with | ||
| | .foundViolation _ violation trace => Json.mkObj | ||
| [ ("result", "found_violation") | ||
| , ("violation", toJson violation) | ||
| , ("trace", toJson trace) | ||
| , ("state_fingerprint", Json.null) | ||
| ] | ||
| | .noViolationFound exploredStates reason => Json.mkObj | ||
| [ ("result", "no_violation_found") | ||
| , ("explored_states", toJson exploredStates) | ||
| , ("termination_reason", terminationReasonToJson reason) | ||
| ] | ||
| | .cancelled => Json.mkObj [("result", "cancelled")] |
There was a problem hiding this comment.
These seem to overlap with the ToJson instances from Veil/Core/Tools/ModelChecker/Interface.lean?
| instance instToJsonSimulateResult {ρ σ κ : Type} [ToJson ρ] [ToJson σ] [ToJson κ] : ToJson (SimulateResult ρ σ κ) where | ||
| toJson r := Json.mkObj [ | ||
| ("result", resultToJson r.result), | ||
| ("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) | ||
| ] | ||
|
|
||
| def SimulateResult.toDisplayJson {ρ σ κ : Type} [ToJson ρ] [ToJson σ] [ToJson κ] | ||
| (r : SimulateResult ρ σ κ) : Json := | ||
| match resultToJson r.result with | ||
| | Json.obj kvs => | ||
| Json.mkObj <| kvs.toList ++ [ | ||
| ("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) | ||
| ] | ||
| | other => | ||
| Json.mkObj [ | ||
| ("result", other), | ||
| ("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) | ||
| ] |
There was a problem hiding this comment.
What is the intended distinction between instToJsonSimulateResult and SimulateResult.toDisplayJson? They look very similar. Could this duplication be eliminated?
| structure CompiledCommandSpec where | ||
| exportedName : String | ||
| supportsParallelConfig : Bool := false | ||
|
|
||
| structure CompilationKey where | ||
| sourceFile : String | ||
| exportedName : String | ||
| commandId : String | ||
| deriving BEq, Hashable, Inhabited |
There was a problem hiding this comment.
Can you add some comments to the fields of these two newly introduced structures? It's unclear what they mean just by looking at their names.
| 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) (_statusPrefix : String) (cancelToken : IO.CancelToken) |
There was a problem hiding this comment.
_statusPrefix seems not used anywhere, can we remove it?
| `({}) | ||
|
|
||
| /-- Prepend `name` with `mod.name`. -/ | ||
| private def mkIdentWithModName' (mod : Module) (name : Name) : Ident := |
There was a problem hiding this comment.
What's the meaning of this '?
| /-- Whether this progress entry is for `#simulate` rather than `#model_check`. -/ | ||
| isSimulation : Bool := false | ||
| /-- Number of traces completed so far (simulation only). -/ | ||
| tracesRun : Nat := 0 | ||
| /-- Configured maximum trace budget (simulation only). -/ | ||
| maxTraces : Nat := 0 | ||
| /-- Depth reached in the current/last trace (simulation only). -/ | ||
| simulationDepth : Nat := 0 |
There was a problem hiding this comment.
The current Progress structure feels somewhat monolithic, especially with simulation-specific fields being added directly to it.
Would it make sense to model this as an inductive type instead, with separate constructors for model checking and simulation (each carrying their own payload)? Or were there specific reasons for not structuring it this way?
| {if p.isSimulation then statRow "Traces Run:" (toString p.tracesRun) else statRow "Diameter:" (toString p.diameter)} | ||
| {if p.isSimulation then statRow "Max Traces:" (toString p.maxTraces) else statRow "States Found:" (toString p.statesFound)} | ||
| {if p.isSimulation then statRow "Depth:" (toString p.simulationDepth) else statRow "Distinct States:" (toString p.distinctStates)} | ||
| {if p.isSimulation then .text "" else statRow "Queue:" (toString p.queue)} | ||
| {statRow "Elapsed time:" (formatElapsedTime p.elapsedMs)} | ||
| </tbody> | ||
| </table> | ||
| {metricsHistoryHtml p.history} | ||
| {actionCoverageHtml p.actionStats p.allActionLabels} | ||
| {if p.isSimulation then .text "" else metricsHistoryHtml p.history} | ||
| {if p.isSimulation then .text "" else actionCoverageHtml p.actionStats p.allActionLabels} |
There was a problem hiding this comment.
This seems related to the design of Progress from Veil/Core/Tools/ModelChecker/Concrete/Progress.lean.
The rendering logic here feels somewhat ad-hoc, with many branches of the form if p.isSimulation then ... else .... This may become harder to maintain as the model checking and simulation features evolve independently.
Would it make sense to instead generate the HTML based on the kind of progress (e.g., separate rendering paths), so that the two cases do not share this much conditional logic?
|
Thanks again for the contribution! This is very helpful, and especially for the extensive test cases. Also, apologies for the delay on my side; it took me a while to go through everything carefully. I've left quite a number of inline comments. To clarify the intent:
In particular, for the more structural/design-related comments, I'm totally fine with handling them in follow-up changes if that makes things easier. We can decide together what should be in scope for this PR. There are also a few higher-level points that I didn't put as inline comments: Compilation / temp folder behaviorThe change to assign distinct names to temp folders makes sense in principle, to avoid conflicts across compilations of the same module. However, we've run into a couple of practical issues with this approach:
Given these issues, it might make sense to temporarily avoid introducing random suffixes for temp folders, and revisit this once the underlying problems are resolved. Simulation config / elaborationRegarding the changes in I'm slightly concerned that the current approach may be somewhat hardcoded, or relies on less common Lean mechanisms, which makes it a bit unclear how robust or maintainable it will be in the long run. One possible direction could be to rely more directly on option resolution when defining defaults (e.g., via a small elaboration helper), so that the behavior is more uniform. I also tried a small prototype along these lines; happy to share if useful, but this is definitely out of scope for this PR. Test cases (compilation mode)Thanks again for adding such extensive test cases! This is really valuable. One small note: in our existing test suite, we currently do not include model checking in compilation mode. The main reason is the compilation workflow and binary size issues mentioned above. Given that, would it be possible to temporarily switch those compilation-mode test cases to interpreted mode? We can revisit adding compilation-mode tests once the underlying issues are addressed. On
|
|
hey @zqy1018 ! Many thanks for all the detailed comments. I will respond to all of them this week. |
3 participants
Random-walk state exploration for Veil -- runs random traces checking invariants at each step.
It finds shallow invariant violations faster than
#model_check(exhaustive BFS), but it is not complete.Usage
Benchmark
Search time only (Lean loading overhead subtracted) on my machine:
#model_check interpreted#simulateAll five have known violations.
Disclaimer
Contains LLM generated code.