LoLa CLI Reference¶

Normative for all command-line behaviour at the compiler version in this repository.

Contents¶

lola — compile and check
lola run — compile and execute a PROGRAM
lola guided — GS-next candidate request
lola extern — Verified Library toolchain
Exit status
Output format
Profiles and their effect on compilation
Targets and their effect on output
Failure modes

1. lola — compile and check¶

Synopsis¶

lola <file.lola> [--target st|rust|check] [--profile default|pilot|float64]
                 [--project <file.toml>] [--strict]

Arguments¶

`file`¶

Path to a .lola source file. The file must contain either a normal program (one or more FUNCTION/EXTERN FUNCTION definitions followed by one FUNCTION_BLOCK) or a single EXTERN_REAL_CONTRACT declaration (§3.5 of the Language Reference).

`--target st|rust|check`¶

Select the output mode. Default: check.

Value	Effect
`check`	Verify the programme and print a structured summary. No code is emitted.
`st`	Emit IEC 61131-3 Structured Text to stdout.
`rust`	Emit a Rust `struct` + `impl step()` to stdout.

When --target check, the compiler additionally runs representation analysis and overflow analysis (numerical assurance chain, if applicable). These analyses are skipped when emitting code directly with --target st or --target rust.

`--profile default|pilot|float64`¶

Select the assurance profile. Default: default.

Value	Meaning
`default`	Development baseline. All features available; experimental features accepted.
`pilot`	Verified core (G1-closed at documented commit). Rejects experimental features; requires both ST and Rust backends; requires `proved` EXTERN warrants.
`float64`	Enables global `REAL`/`LREAL` → IEEE 754 binary64 representation. Same restrictions Same restrictions as `default`; adds Float64 lowering at codegen.

See Language Reference §17 for the full gate table.

When --project is also given, [representation] real = "float64" in the TOML sets the profile to float64 unless --profile pilot is explicitly given on the command line (CLI profile takes precedence for pilot; TOML takes precedence for float64).

`--project <file.toml>`¶

Load a project configuration file (see Project Configuration Reference). Enables the full numerical assurance chain:

REAL/LREAL machine representation (from [representation])
Sampling models and discretisation bounds ([sampling.*])
Physical input error bounds ([physical_errors])
Algebraic rewrite policy ([rewrite])
External mathematical contracts and implementation warrants ([external_contracts], [external_implementations.*])

Without --project, numerical assurance analyses are not performed and REAL/LREAL programmes emit only under --profile float64.

When the source file contains an EXTERN_REAL_CONTRACT declaration, --project loads the implementation warrants declared in the TOML and prints them alongside the contract digest.

`--strict`¶

Treat warnings as errors. Compilation fails (exit code 1) if any warning is generated. Without --strict, warnings are printed to stderr and compilation continues.

Examples¶

# Verify and print assurance summary
lola examples/motor.lola

# Emit Structured Text
lola examples/motor.lola --target st

# Emit Rust
lola examples/motor.lola --target rust

# Full numerical assurance analysis via project file
lola examples/t2/lowpass.lola --project examples/t2/lowpass.toml

# Check a mathematical contract with implementation warrants
lola examples/t2/external_pid.lola --project examples/t2/external_pid.toml

# Verified-core profile
lola examples/motor.lola --profile pilot

# REAL programme — Float64 representation
lola examples/analog/pid.lola --profile float64 --target rust

# Treat warnings as errors in CI
lola examples/pressure.lola --strict

2. lola run — Compile and execute a PROGRAM¶

lola run compiles a PROGRAM to native Rust, links it against lola-runtime-host (or the platform adapter), and starts the scan loop. The process image is shared via two memory-mapped files (mmap), one for inputs and one for outputs. An external process (plant simulator, HMI, supervisory tool) reads and writes those files to exchange data with the running program.

Synopsis¶

lola run <file.lola> [--period-ns NS] [--scans N]
                     [--input PATH] [--output PATH]
                     [--manifest PATH]

Arguments¶

`file`¶

Path to a .lola source file containing exactly one PROGRAM block. If the file contains a FUNCTION_BLOCK instead, lola run rejects it with an error. Sub-blocks referenced by the PROGRAM (FUNCTION_BLOCK, SSFC) are resolved from the same directory as file.

`--period-ns NS`¶

Scan period in nanoseconds. Default: 10000000 (10 ms).

The runtime executes one scan cycle every NS nanoseconds. If a scan takes longer than the period, the next scan starts immediately (no skipped cycles, no accumulated jitter).

`--scans N`¶

Number of scan cycles to run. 0 (the default) runs until the process receives SIGINT (Ctrl-C).

`--input PATH`¶

Path for the input process image file. Default: /tmp/<name>-input.img.

If the file does not exist, lola run creates it with a zeroed payload and a valid header (magic, ABI version, schema hash, payload size). If it already exists, its schema hash is validated on each scan; a mismatch causes the runner to exit.

`--output PATH`¶

Path for the output process image file. Default: /tmp/<name>-output.img.

Created (or overwritten) by the runner on startup; the runner holds an exclusive write lock via a seqlock counter in the header. Readers must perform a seqlock-safe read (check the sequence counter before and after copying the payload).

`--manifest PATH`¶

Path to write the process image schema JSON manifest. Default: <dir>/<name>.io.json in the same directory as --input.

The manifest is written (or overwritten) on every lola run invocation, before the runner starts. It is always up to date with the binary image files. See Process Image Reference for the schema format.

What lola run does¶

Compiles the source with FLOAT64_REPR (MATHREAL → IEEE 754 binary64 on the wire).
Generates a Rust runner binary (content-addressed; cached in ~/.cache/lola/rust/).
Writes the manifest JSON.
Creates the input image if it does not yet exist.
Launches the runner subprocess.

The runner writes output on every scan and reads input at the start of each scan. Both images use a seqlock header (seq field) to allow concurrent reads without a mutex.

Examples¶

# Run the Pasteurizer PROGRAM with a 100 ms scan period
lola run examples/pasteurizer/Pasteurizer.lola --period-ns 100000000

# Run for exactly 1000 scans, then exit
lola run examples/pasteurizer/Pasteurizer.lola --scans 1000

# Custom image paths
lola run my.lola --input /dev/shm/my-in.img --output /dev/shm/my-out.img

# Print manifest to a named file
lola run my.lola --manifest /tmp/my.io.json

Supported I/O types¶

LoLa type	Wire encoding	Size
`BOOL`	`BOOL_U8` (0 or 1)	1 B
`INT`	`INT16_LE`	2 B
`DINT`	`INT32_LE`	4 B
`LINT`	`INT64_LE`	8 B
`UINT`	`UINT16_LE`	2 B
`UDINT`	`UINT32_LE`	4 B
`ULINT`	`UINT64_LE`	8 B
`BYTE`	`UINT8_LE`	1 B
`WORD`	`UINT16_LE`	2 B
`DWORD`	`UINT32_LE`	4 B
`LWORD`	`UINT64_LE`	8 B
`LREAL`	`IEEE754_BINARY64_LE`	8 B
`MATHREAL`	`IEEE754_BINARY64_LE`	8 B

Array types and WSTRING are not yet supported in lola run.

Fields are packed densely in declaration order: VAR_INPUT first, then VAR_OUTPUT, each starting at byte 0 within its own image file.

Runtime-owned values¶

lola run does not expose elapsed scan time as a process image field. Time-dependent constructs (T_elapsed, WITHIN, timer presets) are driven by the runtime clock internally. An external process cannot inject a fake scan period through the process image.

3. lola guided — GS-next candidate request¶

lola guided starts a Rust/Kani or Structured-Text/matiec/CBMC proof-carrying candidate workflow. It accepts either a combinational block whose outputs are constrained by RULE, or the narrow GS-v2-S stateful slice whose LoLa register rules define an exact one-step transition. Creating a request never accepts a candidate or weakens a LoLa proof.

Synopsis¶

lola guided <file.lola> --out <directory> [--target rust|st] [--agent codex|claude] [--model <model>]
                              [--cache-dir <directory>]
                              [--verify-candidate <candidate.json>]
                              [--proof kani|creusot|cbmc]
                              [--kani-unwind <n>]
                              [--cbmc-unwind <n>]
                              [--accept]

The command writes compiler-owned inputs for the candidate boundary:

request.json: port and PARAMETER types, ASSUMEs, caller and PARAMETER REQUIREs, state, invariants, transitions, RULEs, synthesis targets, source digest, and a machine-readable proof_scope;
PROMPT.md: the restricted prompt for a candidate generator.

For the default --target rust, when its smaller optional renderer can lower the same declaration, the command also writes candidate.creusot.rs, a Rust/Creusot skeleton with compiler-owned requires and ensures. Otherwise it writes CREUSOT_UNAVAILABLE.md with the specific unsupported construct; creusot_status.json binds that availability to the source digest. The exact Kani/CBMC request remains usable.

--agent codex calls codex exec in read-only sandbox mode. --agent claude calls Claude Code in non-interactive JSON-schema mode with built-in and MCP tools and project customisation disabled. Both adapters normalise to the same locally validated candidate.json schema; a provider never changes the proof contract or acceptance checks. --codex remains a compatibility alias for --agent codex; --model is passed through to the selected CLI. Every proposal is untrusted: the command does not install it, emit PLC code, or claim a proof. A later proof gate must verify both the compiler-owned contract and the candidate bytes.

After --accept, GS-next stores the candidate and its hash-bound receipt in .lola/guided-cache/ by default. The key is the normalized declaration/proof contract (target, ABI, ports, assumptions, parameter requirements, RULEs, and synthesis targets), not the raw source digest; harmless formatting or comment changes therefore reuse the accepted candidate. A later --agent codex or --agent claude invocation for the same declaration writes that cached proposal to candidate.json without starting an LLM. --cache-dir selects a different local cache. Cache reuse never skips a requested --verify-candidate replay.

--target st writes candidate.st and candidate.cbmc.c. The former is the one compiler-owned IEC function-block shell, the latter is the CBMC harness over the C that matiec generated from that exact ST artifact. ST candidate verification requires --proof cbmc, MATIEC_DIR (containing iec2c and lib/ieclib.txt), and cbmc on PATH; a successful --accept writes candidate_accepted.st.

--verify-candidate injects the proposal's candidate_body into the one compiler-generated hole. For Rust it emits a standalone symbolic Rust harness and proves the LoLa contract with Kani/CBMC (--proof kani), without adding any Cargo dependency to this project. --proof creusot replays the generated Creusot source in a temporary crate when a compatible local Creusot installation exists. Both paths reject obvious escape hatches (unsafe, FFI, macros, filesystem/process access, and panic/TODO placeholders). A successful replay is still only proof evidence; candidate installation and target code emission remain a separate acceptance gate. Passing --accept after a successful replay writes the executable candidate_accepted.rs and acceptance.json; the latter binds the LoLa source, candidate body, proof backend, proof harness, and the original RULEs by SHA-256.

Kani checks loop-unwinding assertions; --kani-unwind controls the default bound (32). --cbmc-unwind applies the same fail-closed unwinding check to loops in an ST candidate (matiec→C→CBMC). Raise either only for a candidate with a known larger static loop bound; an unwinding failure is not a proof.

The current exact Kani ABI covers combinational BOOL, all fixed-width IEC integer/bit-string types, TIME comparisons, statically sized/static-indexed arrays, IEC wrapping arithmetic, conversions, conditionals, and bounded aggregates. It normalises CONSTs and bounded LoLa FUNCTIONs and quantifies PARAMETER values under their REQUIREs. MATHREAL/LREAL and WSTRING representation boundaries, PRE/timer state, composition/wiring, EXTERN calls, and large SORT artifacts are not approximated; the proof_scope records those exclusions and rejects a source until its dedicated transition or representation ABI exists.

The separate lola-gs-*-stateful-v1 ABI covers one-step BOOL and fixed-width integer register state with explicit priority and HOLD. Its proof harnesses separate the unconditional initial relation from the inductive transition relation; invariants in this first slice therefore read retained state only. Timer state, arrays, derived outputs, composition, REAL/LREAL, WSTRING, and EXTERN remain fail-closed boundaries.

Example¶

lola guided examples/pumpbank.gs --out build/pumpbank-proof --agent codex

lola guided examples/pumpbank.gs --target st --out build/pumpbank-st-proof \
  --verify-candidate build/pumpbank-st-proof/candidate.json --proof cbmc --accept

4. lola extern — Verified Library toolchain¶

Sub-commands for authoring, verifying, and registering external function artifacts.

Synopsis¶

lola extern <command> [options]

2.1 lola extern check¶

lola extern check

Validates the Verified Library (lola/verified/manifest.json):

All artifact entries have a lola_contract field.
All target entries have a file field pointing to an existing source.
SHA-256 digests match the stored source files.
All clause entries have a valid status (proved or audited).
All recipe_id references resolve to entries in witness_recipes._REGISTRY.

Output. Prints a count of artifacts and targets, then lists issues (errors) and pending scaffolds (non-errors from lola extern init) separately. Advisory lines note when a reverification tool is unavailable in PATH.

Exit status. 0 if no issues; 1 if any issue was found.

2.2 lola extern verify¶

lola extern verify <artifact-id> --target rust|st

Runs the verification recipe for the named artifact on the named backend target. Does not write to the manifest (read-only). Use lola extern register to seal the result.

Arguments:

Argument	Description
`artifact-id`	Artifact key in `manifest.json` (e.g. `sat_add_i16`).
`--target rust\\|st`	Backend target. Must match a target entry in the manifest.

Output. Prints artifact id, target, clause, recipe, tool, truncated sha256, then the verification result (proved ✓ or failed ✗). On success, prints a suggested lola extern register command.

Effect. On success, writes a temporary .verify_<id>_<target>.json cache file in lola/verified/. This cache is reused (if fresh — within 10 minutes) by a subsequent lola extern register to avoid re-running the recipe.

Exit status. 0 on proved; 1 on failure or error.

2.3 lola extern register¶

lola extern register <artifact-id> --target rust|st [--audit <reason>]

Seals a verification warrant into the manifest. The only write path to the registry.

Arguments:

Argument	Description
`artifact-id`	Artifact key in `manifest.json`.
`--target rust\\|st`	Backend target.
`--audit <reason>`	Bypass recipe; record a manual audit with the given reason string. Sets clause status to `audited`.

Behaviour without --audit.

Looks for a fresh verify result (from a recent lola extern verify run).
If not found, re-runs the recipe automatically.
Checks that lola_contract has not changed since the verify result was produced.
Checks that the artifact source file has not changed since the verify result.
Writes sha256 and clause status/witness into the manifest atomically.
Deletes the verify cache file.

Behaviour with --audit <reason>.

Records the current sha256 and sets clause status to audited with the given reason and a timestamp. No recipe is executed.

Exit status. 0 on success; 1 on error.

2.4 lola extern init¶

lola extern init <contract-name> --target rust|st [--by <artifact-id>] [--ensures <clause>]

Scaffolds a new artifact entry. Creates:

A source stub in lola/verified/<artifact-id>.<ext>.
A manifest entry in lola/verified/manifest.json.
A recipe stub function in lola/witness_recipes.py.

Existing files are not overwritten.

Arguments:

Argument	Description
`contract-name`	Human function name (e.g. `abs_nonneg`). Used as the stub function name.
`--target rust\\|st`	Backend target for the scaffold.
`--by <artifact-id>`	Artifact key to use in the manifest. Default: `<contract-name>_i16`.
`--ensures <clause>`	Pre-fill the `lola_contract` ENSURE clause in the manifest. Default: placeholder `ENSURE ...`.

Output. Lists created and already-existing files. Prints next-step instructions (implement stub → verify → register → check).

Exit status. Always 0.

3. Exit Status¶

Code	Meaning
`0`	Success. For `lola <file>.lola --target check`, verification passed and all assurance gates cleared. For `lola --target st/rust`, code was emitted successfully.
`1`	Failure. Compilation error (type error, verification failure, ambiguity, profile gate), OS error (file not found), or parse error. Error details printed to stderr.

4. Output Format (`--target check`)¶

When --target check (the default), lola prints a structured summary to stdout.

Always printed¶

Compilation succeeded: <BlockName>
G2: <verdict>
Claims: <n>

G2 is the gate verdict from the contract assurance check: passed, not-required, or unrated. Claims is the count of step-phase proof obligations.

Printed when REAL representations are active¶

REAL representations (Z3-certified range -> fixed-point width):
  <var>: [-12.345, 12.345] -> Q7.8  [proved]

Printed when overflow analysis runs¶

REAL overflow-safety (DT <= 1s): safe [proved]

Or, if findings exist:

REAL overflow-safety (DT <= 1s): findings
  <finding description>

Printed when Engineering Error Report is available (--project)¶

── Engineering Error Report (<var>) ─────────────────────────────
<formatted report>

Printed when EXTERN evidence is available¶

EXTERN <artifact-id>/<target>[,<target>] [<worst-warrant>]

or (legacy EXTERN array path):

EXTERN array '<output>': realised by <file> [<status>], discharging `<contract>`
  witness: <witness>

Printed when REQUIRE premises exist¶

Caller action: discharge or monitor <id1>, <id2>, ...

EXTERN_REAL_CONTRACT check output (--project with contract file)¶

EXTERN_REAL_CONTRACT <Name>
  digest:  <16-hex-chars>
  inputs:  <var1>, <var2>
  outputs: <var1>
  states:  <var1>           (only printed if states exist)
  implementations (<n>):
    <backend>: [<status>] <impl-id>  ε_out={<var>≤<val>}  ε_st={<var>≤<val>}

5. Profiles and Their Effect on Compilation¶

See Language Reference §17 for the full gate table. Quick reference:

Feature	`default`	`pilot`	`float64`
WSTRING	experimental	rejected	experimental
Bitstring arithmetic	experimental	rejected	experimental
TIME inputs/outputs	experimental	rejected	experimental
Variable timer presets	experimental	rejected	experimental
REAL overflow	advisory	hard error	advisory
REAL backends	requires `float64`	requires `float64` + overflow-safe	enabled
Required targets	—	st + rust	—
EXTERN warrant floor	—	proved	—
Fresh EXTERN evidence	—	required	—

6. Targets and Their Effect on Output¶

Target	stdout	stderr	EXTERN behaviour
`check`	Assurance summary	Warnings	Entailment check + warrant lookup
`st`	IEC 61131-3 ST source	Warnings	ST artifact embedded in output
`rust`	Rust struct + impl	Warnings	Rust artifact embedded in output

When --target st or --target rust, the programme must already pass check semantics (the compiler verifies before emitting). An EXTERN with no artifact for the chosen backend raises NotImplementedError and compilation fails.

7. Failure Modes¶

Error	Exit	Cause
Parse error	1	Syntax error in the source file
Sema error	1	Type error, duplicate declaration, undefined reference, malformed expression
`invariant-init`	1	Initial state violates an INVARIANT
`invariant-step`	1	A cycle can violate an INVARIANT (counterexample printed)
Ambiguity	1	Two equal-priority rules can fire simultaneously with different results
Division obligation	1	Cannot prove divisor ≠ 0
Profile gate	1	Source uses a feature rejected by the active profile
Backend EXTERN missing	1	`EXTERN FUNCTION` with `BY` key not found, or no artifact for the chosen backend
File not found	1	Source file or `--project` TOML does not exist
Warning (strict)	1	Any warning when `--strict` is active

Errors are printed to stderr. stdout receives code only on success with --target st or --target rust.

LoLa CLI Reference¶

Contents¶

1. lola — compile and check¶

Synopsis¶

Arguments¶

file¶

--target st|rust|check¶

--profile default|pilot|float64¶

--project <file.toml>¶

--strict¶

Examples¶

2. lola run — Compile and execute a PROGRAM¶

Synopsis¶

Arguments¶

file¶

--period-ns NS¶

--scans N¶

--input PATH¶

--output PATH¶

--manifest PATH¶

What lola run does¶

Examples¶

Supported I/O types¶

Runtime-owned values¶

3. lola guided — GS-next candidate request¶

Synopsis¶

Example¶

4. lola extern — Verified Library toolchain¶

Synopsis¶

2.1 lola extern check¶

2.2 lola extern verify¶

2.3 lola extern register¶

2.4 lola extern init¶

3. Exit Status¶

4. Output Format (--target check)¶

Always printed¶

Printed when REAL representations are active¶

Printed when overflow analysis runs¶

Printed when Engineering Error Report is available (--project)¶

Printed when EXTERN evidence is available¶

Printed when REQUIRE premises exist¶

EXTERN_REAL_CONTRACT check output (--project with contract file)¶

5. Profiles and Their Effect on Compilation¶

6. Targets and Their Effect on Output¶

7. Failure Modes¶

`file`¶

`--target st|rust|check`¶

`--profile default|pilot|float64`¶

`--project <file.toml>`¶

`--strict`¶

`file`¶

`--period-ns NS`¶

`--scans N`¶

`--input PATH`¶

`--output PATH`¶

`--manifest PATH`¶

4. Output Format (`--target check`)¶