The strata command-line interface for Strata. This package builds the main executable that users interact with to parse, transform, and analyze Strata programs.
lake buildThis produces the strata executable. The package depends on the parent Strata library (via lakefile.toml).
lake exe strata <command> [flags...]
lake exe strata --help
lake exe strata <command> --help| Command | Description |
|---|---|
verify <file> |
Verify a Strata program (.core.st, .csimp.st, or .b3.st) |
transform <file> |
Apply one or more transforms to a Core program |
check <file> |
Parse and validate a Strata file |
toIon <input> <output> |
Convert a Strata text file to Ion binary format |
print <file> |
Pretty-print a Strata file to stdout |
diff <file1> <file2> |
Compare two program files for syntactic equality |
| Command | Description |
|---|---|
pyAnalyzeLaurel <file> |
Verify a Python Ion program via the Laurel pipeline |
pyResolveOverloads <python_path> <dispatch_ion> |
Identify overloaded service modules a Python program uses |
pySpecs <source_dir> <output_dir> |
Translate Python spec files to DDM Ion format |
pySpecToLaurel <python_path> <strata_path> |
Translate a PySpec Ion file to Laurel declarations |
pyAnalyzeLaurelToGoto <file> |
Translate Python Ion through Laurel to GOTO JSON |
pyAnalyzeToGoto <file> |
Translate Python Ion directly to GOTO JSON |
pyTranslateLaurel <file> |
Translate Python Ion through Laurel to Core, print to stdout |
pyInterpret <file> |
Concretely interpret a Python Ion program |
| Command | Description |
|---|---|
laurelAnalyze <file> |
Analyze a Laurel source file with verification |
laurelAnalyzeBinary |
Verify Laurel Ion programs from stdin |
laurelAnalyzeToGoto <file> |
Translate Laurel to GOTO JSON |
laurelInterpret <file> |
Concretely interpret a Laurel Ion program |
laurelInterpretBinary |
Concretely interpret Laurel Ion programs from stdin |
laurelParse <file> |
Parse a Laurel source file (no verification) |
laurelPrint |
Read Laurel Ion from stdin, print concrete syntax |
laurelToCore <file> |
Translate Laurel to Core, print to stdout |
| Command | Description |
|---|---|
lake exe laurelJavaGen <package> <output-dir> |
Generate Java source files for Laurel AST types (standalone Lake executable) |
Most verification commands accept:
| Flag | Description |
|---|---|
--solver <name> |
SMT solver executable (default: cvc5) |
--solver-timeout <seconds> |
Solver timeout (default: 10) |
--verbose |
Enable verbose output |
--quiet |
Suppress warnings |
--profile |
Print elapsed time per pipeline step |
--sarif |
Write results as SARIF |
--no-solve |
Generate SMT files without invoking the solver |
--vc-directory <dir> |
Store VCs in SMT-Lib format |
--check-mode <mode> |
Verification mode (deductive, bugFinding, etc.) |
--incremental |
Use incremental solver backend |
--parallel <N> |
Number of parallel solver workers |
--include <path> |
Add a dialect search path |
The interpret commands are the exception: laurelInterpret and laurelInterpretBinary
execute the program concretely and never invoke a solver, so they accept only
--fuel, --entry, --interpreter, and the Laurel translate flags. Passing a solver-oriented
flag from the table above (--solver, --check-mode, --sarif, …) is rejected as
an unknown option rather than silently ignored. Note that laurelAnalyze still
accepts the full set, so flag lists cannot be shared verbatim across the two.
--interpreter core (the default) translates the program to Core and runs the Core
interpreter. --interpreter laurel resolves the program against the prelude and runs the Laurel
interpreter on it directly, with no translation to Core; it rejects --keep-all-files.
Like the Core path it skips assumes and checks the preconditions and postconditions of
calls (free conditions are not checked); neither checks modifies frames. With --entry P,
the Core path calls P from an entry point it adds: P's requires is assumed, but its
postconditions are checked and an exception escaping it is a failed check. The Laurel path runs
P's body as the entry point. A program the verify pipeline would reject (a resolution error, a
not-yet-supported construct, or a source name starting with $) is an error.
--fuel bounds the steps of each entry procedure (default 100000, a different unit from
the Core interpreter's per-call fuel), so a divergent program, including plain unbounded
recursion, ends out of fuel. An unsupported construct, an uncaught throw or running out of fuel ends
that entry with exit 2; assertion failures recorded before an uncaught throw or
out-of-fuel are still reported.
The Laurel commands (laurelAnalyze, laurelAnalyzeBinary, laurelInterpret,
laurelInterpretBinary, laurelToCore, laurelAnalyzeToGoto) also accept:
| Flag | Description |
|---|---|
--phases <names> |
Run these Laurel phases, in this order (comma-separated) |
--skip-phases <names> |
Run the default Laurel phase order without these phases |
--display-phases |
Print the available Laurel phases and the default order |
--display-phase-contracts |
Print the shape lifeline table for the chosen order |
These flags select Laurel phases only. --phases runs exactly the phases given, in that order,
and --skip-phases removes each name from the default order, e.g.
--skip-phases CoroutineElaboration,YieldElim,InferHoleTypes,EliminateDeterministicHoles. An
unknown name is an error, and a phase may be named only once. Transparency, Ordering and
LaurelToCoreSchema always run and cannot be named; a phase that runs before Transparency
cannot follow one that runs after it.
An order is checked against the phases' NodeKind declarations before anything runs, keeping
apart two origins of a shape that is still present when a phase declaring it unsupported runs. A
shape some phase in the order creates is an error in the order itself, whatever the input. A
shape that can only have come from the input is a requirement on the input instead: after
resolution the input is checked not to contain it, and is refused if it does, naming the phase
that would remove it. The input check does not model the Pseudo kinds, so a requirement on one
is an error in the order instead, naming the phase that would remove it.
--display-phases lists the phases with a pasteable --phases line for the default order, and
the phases that always run. Given without an input file, --phases / --skip-phases only report
whether the order composes and which shapes the input must not contain. Given with an input
file, --display-phases and --display-phase-contracts print and exit before the file is read.
| Code | Category | Meaning |
|---|---|---|
| 0 | Success | Analysis passed, inconclusive, or --no-solve completed |
| 1 | User error | Bad input: invalid arguments, malformed source |
| 2 | Failures found | Analysis completed and found assertion violations |
| 3 | Internal error | SMT encoding failure, solver crash, or translation bug |
| 4 | Known limitation | Intentionally unsupported language construct |
Codes 1-2 are user-actionable (fix the input or the code under analysis). Codes 3-4 are tool-side (report as a bug or wait for support).
laurelInterpret and laurelInterpretBinary intentionally exit 0 even when assertions fail (mirroring laurelAnalyzeBinary for Java Front-End diagnostic parsing). Assertion failures are reported as stdout diagnostics under the ==== DIAGNOSTICS ==== sentinel. Callers must parse stdout for ==== DIAGNOSTICS ==== and the <path>:<start>-<stop>: <message> lines that follow it, rather than relying on a non-zero exit code to detect violations. Exit codes 1/3/4 still apply for user errors, internal errors, and known limitations; exit 2 is used only for OutOfFuel and other opaque runtime errors with no associated source diagnostic.
The message carries the failing property's kind, matching laurelAnalyzeBinary: assertion does not hold for a source assert, and precondition does not hold / postcondition does not hold for a contract obligation the translator inserted. Treat the message as opaque text keyed off the line shape — do not match on assertion does not hold alone, which misses every contract violation.
Because Laurel's assume is verification scaffolding with no runtime meaning, the interpreter skips assumes rather than halting on them. A free (assume-only) contract condition therefore produces no interpret diagnostic and no non-zero exit, even where the verifier would report it: free requires false on a callee emits no call-site check, so a run whose only obligation was that condition exits 0 with an empty diagnostics section.
Strata-CLI/
├── StrataMain.lean # Entry point (dispatches to runCommandMap)
├── StrataMainLib.lean # Registers the Python and Laurel frontends
├── lakefile.toml # Lake build configuration
├── lean-toolchain # Lean version pin
└── lake-manifest.json # Dependency lock file
# Verify a Core program
lake exe strata verify program.core.st
# Verify with verbose output and custom solver timeout
lake exe strata verify --verbose --solver-timeout 30 program.core.st
# Apply transforms to a program
lake exe strata transform program.core.st --pass inlineProcedures --pass loopElim
# Inline specific procedures then filter
lake exe strata transform program.core.st \
--pass inlineProcedures --procedures helper,util \
--pass filterProcedures --procedures main
# Parse and validate without verification
lake exe strata check program.core.st
# Analyze Python via Laurel pipeline
lake exe strata pyAnalyzeLaurel program.python.st.ion --spec-dir ./specs