Spark DSL Verifier enforcing mathematical 1-Safe Soundness on Ash state machine resources at compile-time.
If an Ash resource defines to_workflow_net/0, this verifier compiles the reachability graph
and proves:
- Option to complete (liveness)
- Proper completion (no lingering tokens in sink place)
- No dead transitions (fireability)
- 1-Safety (no place contains > 1 token)
If any invariant fails, compilation immediately halts with a Spark.Error.DslError.