LoLa Project Configuration Reference¶

Normative for all .toml project configuration fields at the compiler version in this repository.

A project configuration file (.toml) separates engineering and deployment context from programme semantics. The .lola file owns mathematical meaning; the .toml owns representation choices, deployment assumptions, and physical measurement uncertainties.

lola lowpass.lola --project lowpass.toml --target check

All sections are optional. An empty .toml (or no --project flag at all) is valid and equivalent to the default profile with no numerical assurance analyses.

Scope boundary. Fields in this file are assumptions about the deployment environment — not language semantics. Adding a [physical_errors] entry does not make the programme "less correct"; it declares an engineering fact that narrows the error bound an INVARIANT must hold against. The .lola file is unchanged.

Contents¶

[representation]
[sampling.\<var>]
[physical_errors]
[rewrite]
[external_contracts]
[external_implementations.\<Name>.\<backend>]
[ssfc_assurance] — SSFC assurance policy gate
Duration and fraction formats
Assurance vocabulary in this file

[representation]¶

Controls the machine representation policy for REAL and LREAL variables. This is the Representation Boundary (Language Reference §13.3).

[representation]
real = "float64"

Fields¶

`real`¶

Type: string
Allowed values: "float64" · "none" (or omit the field)
Default: "none" (fail-closed — no machine representation)

Value	Effect
`"float64"`	All `REAL` and `LREAL` signals are lowered to IEEE 754 binary64 (`f64` in Rust, `LREAL` in ST). Enables Gappa-based roundoff obligations (experimental).
`"none"` / omitted	No machine representation. Backends refuse to emit REAL/LREAL programmes. Mathematical proofs remain valid.

Assurance effect. Setting real = "float64" introduces a representation assumption: the mathematical model proof holds for ℝ; the gap between ℝ and Float64 is a separate obligation (see how-to/real-numerical-assurance.md). The Engineering Error Report accounts for this gap when it can be bounded (via physical_errors and sampling models).

CLI override. --profile pilot on the command line takes precedence over any [representation] setting. --profile float64 on the command line sets float64 regardless of [representation].

[sampling.\<var>]¶

Declares the sampling model for one state variable <var>. Required for the discretisation bound and Engineering Error Report. One [sampling.<var>] section per state variable; multiple sections are permitted.

The .lola source file MUST contain a CONTINUOUS_REFERENCE block with DER(<var>) = <expr>; for every variable named here. The ODE right-hand side comes from the .lola file; the deployment parameters come from this section.

[sampling.s]
period  = "10ms"
method  = "forward-euler"
jitter  = "1ms"
horizon = 100

[sampling.s.input_derivatives]
u = "0"

Fields¶

`period`¶

Type: duration string
Required: yes
Example: "10ms", "1s", "100ms"

The nominal scan period T_s (seconds). The discretisation bound and Engineering Error Report are computed for this period. See Duration format.

`method`¶

Type: string
Default: "forward-euler"
Allowed values: "forward-euler"

The numerical integration method used to discretise the ODE. Only "forward-euler" is currently supported. Additional methods (e.g. Runge-Kutta, trapezoidal) are planned.

Assurance effect. The method is an engineering assumption — the real implementation must use the declared method. Declaring "forward-euler" when the implementation uses a different integrator would invalidate the bound.

`jitter`¶

Type: duration string
Default: "0" (no jitter)
Example: "1ms"

Upper bound on timing uncertainty: the actual scan period satisfies |T_actual − period| ≤ jitter. This introduces an assumption about the deployment's realtime behaviour. The discretisation bound is widened to account for jitter.

`horizon`¶

Type: integer (number of trajectory steps)
Default: omitted (system default, typically 100)
Example: 100

The finite-horizon length used for the discretisation bound computation. A larger horizon produces tighter asymptotic bounds but requires more computation. Applies globally when present (the last horizon seen across all [sampling.*] sections is used).

`[sampling.\<var\>.input_derivatives]`¶

A sub-table declaring upper bounds on the rate of change of input variables between samples. Keys are input variable names; values are fraction strings.

[sampling.s.input_derivatives]
u = "0"      # u is piecewise-constant (zero derivative between samples)
u = "0.5"    # |Δu/Δt| ≤ 0.5 per second (assumed)

Assurance effect. Each entry is an assumption about the physical input signal. A value of "0" asserts the input is piecewise-constant between samples, which tightens the discretisation error bound considerably. A nonzero value declares a Lipschitz bound on the input trajectory.

[physical_errors]¶

Declares upper bounds on physical sensor and actuator errors for input variables. Keys are input variable names; values are fraction strings representing the absolute error bound ε.

[physical_errors]
u   = "1/100"    # sensor error: |u_measured − u_true| ≤ 0.01
ref = "0.005"    # reference signal error: ±0.005

Assurance effect. Physical errors are deployment assumptions about the quality of physical measurements. They are propagated through the Engineering Error Report. A programme with tight INVARIANTs may require small [physical_errors] to guarantee the bound holds in the real system.

Type. The named variables MUST be REAL or LREAL inputs in the .lola file.

Units. Values are in the same physical units as the variable (engineering units from the .lola unit annotation, if present).

[rewrite]¶

Controls the algebraic rewrite policy for REAL expressions. The compiler can select among algebraically equivalent representations that differ in floating-point roundoff error.

[rewrite]
policy = "min_abs_roundoff"

Fields¶

`policy`¶

Type: string
Default: omitted (no rewrite)
Allowed values: "min_abs_roundoff"

Value	Effect
`"min_abs_roundoff"`	Among all algebraically equivalent forms of each REAL expression, select the one with the smallest IEEE 754 binary64 roundoff error bound. Experimental.
omitted	No rewrite; the programme's expressions are used as written.

Assurance effect. The rewrite policy is a codegen choice — it changes which algebraically equivalent expression appears in the emitted code, not the mathematical programme semantics. The Engineering Error Report reflects the selected form.

[external_contracts]¶

Binds a name to a .lola file containing an EXTERN_REAL_CONTRACT declaration. This connects a mathematical contract to the compilation context so that implementation warrants (§6) can reference it.

[external_contracts]
PidController = "./external_pid.lola"

Keys are component names (arbitrary identifiers). Values are file paths relative to the .toml file's directory.

The referenced .lola file MUST contain exactly one EXTERN_REAL_CONTRACT declaration. All variables in the contract MUST be typed REAL or LREAL.

Requirement. Any name that appears as a key in [external_contracts] MUST also appear as a top-level key in [external_implementations.*] if implementation warrants are to be loaded.

[external_implementations.\<Name>.\<backend>]¶

Declares an implementation warrant for the contract named <Name> on the backend <backend>. <Name> MUST match a key in [external_contracts]. <backend> is a free string (e.g. rust, structured-text, c).

[external_implementations.PidController.rust]
implementation_id = "pid_rust_f64_v1"
representation    = "float64"
status            = "assumed"

[external_implementations.PidController.rust.output_error_bounds]
control = "1/10000"

[external_implementations.PidController.rust.state_transition_error_bounds]
integral = "1/100000"
e_prev   = "0"

[external_implementations.PidController.rust.state_lipschitz_bounds]
integral = "1/5"
e_prev   = "1"

Fields¶

`implementation_id`¶

Type: string
Default: "<Name>_<backend>_v1"
Example: "pid_rust_f64_v1"

A human-readable identifier for this implementation. Appears in the Engineering Error Report and assurance receipts. No structural significance; must be unique enough to distinguish implementations across backends and versions.

`representation`¶

Type: string
Default: "float64"
Example: "float64", "lreal64"

The machine arithmetic representation used by this implementation. Informational — used in error reports.

`status`¶

Type: string
Default: "assumed"
Allowed values: "assumed" · "proved" · "audited"

The warrant level for the error bounds declared in this entry.

Value	Meaning
`"assumed"`	Bounds are declared engineering assumptions. Not mechanically verified. Introduces an assumption in the Engineering Error Report provenance.
`"audited"`	Bounds have been reviewed under stated conditions. Weaker than proved but stronger than assumed.
`"proved"`	Bounds have been mechanically verified (e.g. by Gappa or a formal proof).

Assurance effect. The status is recorded in the Engineering Error Report provenance chain. A final report with status = "assumed" anywhere in its chain carries an assumed provenance for the full bound.

`[external_implementations.\<Name\>.\<backend\>.output_error_bounds]`¶

Declares upper bounds on the absolute error between the mathematical contract's output values and the implementation's output values, per output variable.

[external_implementations.PidController.rust.output_error_bounds]
control = "1/10000"    # |output_impl − output_math| ≤ 0.0001

Keys are output variable names (from the EXTERN_REAL_CONTRACT VAR_OUTPUT block). Values are fraction strings (§7).

Assurance effect. These bounds are deployment assumptions about how closely the implementation tracks the mathematical contract. They propagate into the Engineering Error Report as error contributions.

`[external_implementations.\<Name\>.\<backend\>.state_transition_error_bounds]`¶

Declares upper bounds on the absolute error in state variable updates per step.

[external_implementations.PidController.rust.state_transition_error_bounds]
integral = "1/100000"   # |state_next_impl − state_next_math| ≤ 1e-5
e_prev   = "0"          # exact (lossless) state transition for e_prev

Keys are state variable names (from the EXTERN_REAL_CONTRACT VAR_STATE block). A value of "0" asserts the transition is exact.

`[external_implementations.\<Name\>.\<backend\>.state_lipschitz_bounds]`¶

Declares Lipschitz constants bounding how fast state variables respond to input perturbations (per step). Used by the numerical error propagation bound.

[external_implementations.PidController.rust.state_lipschitz_bounds]
integral = "1/5"    # |Δstate_integral| ≤ (1/5) · |Δinput|
e_prev   = "1"      # |Δe_prev| ≤ 1 · |Δinput|

A Lipschitz bound of "1" is conservative (error propagates at most 1:1); values less than 1 indicate damped response; values greater than 1 are permissible but widen the error bound.

7. Duration and Fraction Formats¶

Duration strings¶

Used in [sampling.*] fields (period, jitter). Format:

<number><unit>

Where <number> is an integer or decimal, and <unit> is one of:

Unit	Meaning
`ms`	milliseconds
`s`	seconds
`min`	minutes
`h`	hours

Examples: "10ms", "1s", "0.5s", "100ms", "2min".

Values are stored as exact fractions (no floating-point rounding at parse time).

Fraction strings¶

Used in [physical_errors], input_derivatives, and error bound tables.

Accepted formats:

Format	Example	Value
Integer	`"0"`	0
Decimal	`"0.005"`	1/200 (exact)
Fraction	`"1/100"`	1/100 (exact)

All values are parsed to exact Fraction objects. Use fraction notation ("1/100000") when precision matters; decimal notation introduces a rational approximation (e.g. "0.1" → 1/10 exactly, but "0.3" → 3/10).

[ssfc_assurance]¶

SSFC Assurance Policy Gate. Gates compilation on a set of SSFC assurance claims passing. When this section is present, check_policy(report, policy) must return passed=True or the compiler rejects the SSFC.

[ssfc_assurance]
# Use a predefined profile (one of: "minimal", "standard", "strict")
profile = "standard"

# Optional: make WARN verdicts on required/conditional claims also fail
forbid_warnings = false

Or specify claims explicitly:

[ssfc_assurance]
required_claims   = ["C-SAF", "C-INT", "C-NO-STUCK-MARKING"]
conditional_claims = ["C-GUARD-SAT", "C-DET", "C-REACH"]
forbid_warnings   = false

Profiles¶

Profile	Required claims	Conditional claims
`minimal`	C-SAF, C-INT, C-DEAD	(none)
`standard`	minimal + C-NO-STUCK-MARKING	C-GUARD-SAT, C-DET, C-DATA-DEAD, C-REACH
`strict`	standard + C-REVERSI	C-SYNC-DEAD, C-HOME, C-NO-STUCK-Z3, C-INV, C-WITHIN, C-ASSUME, C-LIVE

Required claims must be produced AND pass. ABSENT counts as a violation.
Conditional claims must pass if produced; ABSENT is OK (the claim is only generated when the SSFC has the relevant structure, e.g. INVARIANT for C-INV, LIVENESS for C-LIVE, WITHIN for C-WITHIN, guard pairs for C-DET).

Python API¶

from lola import project_config
from lola.ssfc_assurance_policy import check_policy, AssurancePolicyError

toml_data = tomllib.load(open("project.toml", "rb"))
policy = project_config.load_ssfc_policy(toml_data)  # None if absent
if policy is not None:
    result = check_policy(report, policy)
    if not result.passed:
        raise AssurancePolicyError(result.summary())

Fields¶

`profile`¶

Type: string
Allowed values: "minimal" · "standard" · "strict"
Mutually exclusive with required_claims / conditional_claims (explicit lists win).

`required_claims`¶

Type: list of strings
Claim IDs that must be present and pass. Overrides profile.

`conditional_claims`¶

Type: list of strings
Claim IDs that must pass if produced, but ABSENT is not a violation.

`forbid_warnings`¶

Type: bool
Default: false
When true, WARN verdicts on required or conditional claims fail the policy gate.

8. Assurance Vocabulary in This File¶

Every field that introduces a deployment assumption is labelled assumed. Fields derived from mathematical proof are labelled proved. The status of the final Engineering Error Report provenance depends on the weakest link across all fields.

What you declare	Provenance
`[representation] real = "float64"`	assumed (Float64 ≈ ℝ)
`[sampling.*]` bounds	assumed (deployment fact)
`[physical_errors]` bounds	assumed (sensor specification)
`[rewrite] policy`	codegen choice; does not affect provenance
`[external_implementations.*] status = "proved"`	proved
`[external_implementations.*] status = "audited"`	audited
`[external_implementations.*] status = "assumed"`	assumed

A project configuration that sets all warrant statuses to "proved" and all error bounds tightly does not by itself constitute a safety case. It is engineering evidence that can feed into a broader case, alongside G1/G2/G3/G4 verdicts.

LoLa Project Configuration Reference¶

Contents¶

[representation]¶

Fields¶

real¶

[sampling.\<var>]¶

Fields¶

period¶

method¶

jitter¶

horizon¶

[sampling.\<var\>.input_derivatives]¶

[physical_errors]¶

[rewrite]¶

Fields¶

policy¶

[external_contracts]¶

[external_implementations.\<Name>.\<backend>]¶

Fields¶

implementation_id¶

representation¶

status¶

[external_implementations.\<Name\>.\<backend\>.output_error_bounds]¶

[external_implementations.\<Name\>.\<backend\>.state_transition_error_bounds]¶

[external_implementations.\<Name\>.\<backend\>.state_lipschitz_bounds]¶

7. Duration and Fraction Formats¶

Duration strings¶

Fraction strings¶

[ssfc_assurance]¶

Profiles¶

Python API¶

Fields¶

profile¶

required_claims¶

conditional_claims¶

forbid_warnings¶

8. Assurance Vocabulary in This File¶

`real`¶

`period`¶

`method`¶

`jitter`¶

`horizon`¶

`[sampling.\<var\>.input_derivatives]`¶

`policy`¶

`implementation_id`¶

`representation`¶

`status`¶

`[external_implementations.\<Name\>.\<backend\>.output_error_bounds]`¶

`[external_implementations.\<Name\>.\<backend\>.state_transition_error_bounds]`¶

`[external_implementations.\<Name\>.\<backend\>.state_lipschitz_bounds]`¶

`profile`¶

`required_claims`¶

`conditional_claims`¶

`forbid_warnings`¶