StrataCLI

The strata command-line interface for Strata. This package builds the main executable that users interact with to parse, transform, and analyze Strata programs.

Building

lake build

This produces the strata executable. The package depends on the parent Strata library (via lakefile.toml).

Usage

lake exe strata <command> [flags...]
lake exe strata --help
lake exe strata <command> --help

Commands

Core

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

Python

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

Laurel

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

Code Generation

Command	Description
javaGen <dialect> <package> <output-dir>	Generate Java source files to represent the language defined by a DDM dialect

Common Flags

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, 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.

Exit Codes

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).

Exception: laurelInterpret / laurelInterpretBinary

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.

File Structure

Strata-CLI/
├── StrataMain.lean       # Entry point (dispatches to runCommandMap)
├── StrataMainLib.lean    # All command definitions, flag parsing, utilities
├── lakefile.toml         # Lake build configuration
├── lean-toolchain        # Lean version pin
└── lake-manifest.json    # Dependency lock file

Examples

# 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