LoLa Language Reference

Normative for all user-visible language behaviour at the compiler version in this repository. When this document and compiler source disagree, compiler source is authoritative; file a documentation issue.

All sections are normatively complete as of 2026-08-17.

---

Contents

1. Scope, Conformance Language, and Notation
2. Lexical Structure
3. Program Structure
4. Declarations and Storage
5. Type System
6. Expressions
7. State Transitions
8. Contracts and Proof
9. Functions and Recursion
10. Composition
11. Timers and Temporal Constructs
12. EXTERN Semantics
13. MATHREAL Semantics
14. Static Semantics
15. Dynamic/Synchronous Semantics
16. Proof Obligations
17. Profiles and Implementation-Defined Features
18. Grammar Appendix
19. Reserved Words
20. Cross-Reference Index

---

1. Scope, Conformance Language, and Notation

This document is the normative reference for the LoLa language — its syntax, type system, and semantics as defined by the Z3 SMT model and enforced by the compiler.

Assurance vocabulary. Claims in this document distinguish:

Term	Meaning
proved	Discharged by the stated proof mechanism (Z3 or exhaustive testing)
assumed	Explicit premise / declared engineering fact
validated	Target/toolchain behaviour checked against a reference for a stated slice
tested	Exercised, not proved
audited	Reviewed under stated conditions
experimental	Available outside stable/supported profile; no coverage guarantee
unsupported	Rejected/fail-closed — the compiler refuses programs that rely on it

Conformance language. MUST means required by the language definition and enforced by the compiler. SHOULD means the compiler may emit a warning. MAY means permitted. Absent these words, normative prose holds unconditionally.

Notation. Grammar rules use name := body BNF. Terminal symbols appear in MONOSPACE. Optional elements are [bracketed]. Alternatives are A | B. Kleene star {A} means zero or more repetitions.

---

2. Lexical Structure

2.1 Whitespace and Comments

Whitespace (space, tab, carriage return, newline) is insignificant except as a token separator. Two comment forms are recognised:

// line comment — extends to end of line
(* block comment — extends to the next *)  *)

Block comments do not nest. A block comment that is not terminated is a lexical error.

2.2 Identifiers

identifier := letter { letter | digit | '_' }
letter     := 'A'..'Z' | 'a'..'z' | '_'
digit      := '0'..'9'

Identifiers are case-insensitive: Motor, MOTOR, and motor refer to the same declaration. A collision between two names that differ only in case is a static error (see §14).

Keywords (§19) share the same lexical form. A token matches a keyword if its upper-cased form equals the keyword text exactly.

2.3 Literals

2.3.1 Boolean literals

TRUE and FALSE denote the two BOOL values.

2.3.2 Untyped integer literals

A bare decimal integer without a type prefix is an untyped integer literal. Its type is resolved at parse time by value:

Value range	Inferred token type	LoLa type
0 – 32 768	INTLIT	INT
32 769 – 2 147 483 647	DINTLIT	DINT
> 2 147 483 647	Lexical error	—

Note: 32 768 is included in the INT range so that Neg(IntLit(32768)) produces INT_MIN = −32 768 without out-of-range promotion.

2.3.3 Typed integer literals

Signed integer literals carry an explicit type prefix and #:

SINT#<digits>    — 0..127 (negatives via SINT_MIN / unary minus)
DINT#<digits>    — 0..2147483647
LINT#<digits>    — 0..9223372036854775807

INT has no typed literal form; use bare integer literals or INT_MIN/INT_MAX.

Typed unsigned integer literals:

USINT#<digits>   — 0..255
UINT#<digits>    — 0..65535
UDINT#<digits>   — 0..4294967295
ULINT#<digits>   — 0..18446744073709551615

Typed bit-string literals use the same syntax with bit-string type names:

BYTE#<digits>    — 0..255
WORD#<digits>    — 0..65535
DWORD#<digits>   — 0..4294967295
LWORD#<digits>   — 0..18446744073709551615

All typed literal prefixes also accept a 16# hexadecimal suffix:

BYTE#16#FF       — 255
LWORD#16#FFFFFFFFFFFFFFFF  — all 64 bits set

A value outside the declared type range is a lexical error.

2.3.4 Named integer constants

Every fixed-width integer and unsigned integer type has named _MIN and _MAX constants:

SINT_MIN, SINT_MAX, INT_MIN, INT_MAX, DINT_MIN, DINT_MAX, LINT_MIN, LINT_MAX, USINT_MIN, USINT_MAX, UINT_MIN, UINT_MAX, UDINT_MIN, UDINT_MAX, ULINT_MIN, ULINT_MAX

These are keywords that produce typed literals at parse time. For unsigned types, _MIN is 0; for signed types, _MIN is the most-negative value in two's complement.

2.3.5 Real (floating-point) literals

A decimal real literal is a sequence of digits, a mandatory ., and more digits:

FLOATLIT := digit { digit } '.' digit { digit }

Example: 2.5, 0.001, 1.0. The literal is stored as an exact Fraction; no rounding occurs at parse or model-build time. Real literals are of type MATHREAL (§5.5).

2.3.6 Time literals

Two syntactic forms are accepted:

T#<digits><unit>     — IEC prefix form: T#100ms, T#2s
<digits><unit>       — shorthand: 100ms, 2s, 1min, 3h

Units: ms (milliseconds), s (seconds), min (minutes), h (hours). The resulting value is of type TIME (§5.6).

2.3.7 WSTRING literals

A WSTRING literal is a sequence of characters enclosed in double quotes:

'"' { any character except '"' or newline } '"'

No escape sequences are defined in the current version. The literal type is WSTRING (§5.7).

2.4 Operators and Punctuation

Multi-character operators: <=, >=, <>, :=, .., ->.

Single-character operators and punctuation: :, ;, ,, ., [, ], (, ), +, -, *, /, =, <, >.

MOD is matched as an identifier by text comparison, not as a keyword, so it does not collide with identifiers like MODEL.

---

3. Program Structure

3.1 Source file layout

A .lola file contains one of the following forms:

(a) A normal program file:

{ function-definition | extern-function-definition }
function-block-definition

Zero or more FUNCTION and EXTERN FUNCTION definitions appear first, followed by exactly one FUNCTION_BLOCK. Functions defined in the file are available for call within the FUNCTION_BLOCK and by other functions in the same file.

(b) A PROGRAM file:

{ function-definition | extern-function-definition }
program-definition

Zero or more FUNCTION and EXTERN FUNCTION definitions appear first, followed by exactly one PROGRAM. A PROGRAM is a non-instantiable root POU. Use lola run to compile and execute it. See §3.6.

(c) An SSFC file:

{ function-definition | extern-function-definition }
ssfc-definition

Zero or more FUNCTION and EXTERN FUNCTION definitions appear first, followed by exactly one SSFC. The SSFC is compiled, verified, and emitted by the same pipeline as FUNCTION_BLOCK. See §21 for the full SSFC reference.

(d) An EXTERN_REAL_CONTRACT file:

extern-real-contract-definition

A contract file contains exactly one EXTERN_REAL_CONTRACT declaration and no FUNCTION_BLOCK. It is not compiled via the normal backend path; it is consumed by lola <file> --project <toml> --target check (see §12 and the CLI Reference).

3.2 FUNCTION_BLOCK

FUNCTION_BLOCK <name> [ "<" <type-param> { "," <type-param> } ">" ]
  [ VAR_INPUT  <var-decls> END_VAR ]
  [ VAR_OUTPUT <var-decls> END_VAR ]
  [ VAR        <var-decls> END_VAR ]
  [ PARAMETER  <var-decls> END_PARAMETER ]
  [ CONTINUOUS_REFERENCE <ode-decls> END_CONTINUOUS_REFERENCE ]
  [ WIRING
      { composition-binding | output-forwarding }
    END_WIRING ]
  [ IMPLEMENTATION
      { derived-definition | register-rules }
      { INVARIANT <bool-expr> ;
      | ASSUME   <bool-expr> ;
      | REQUIRE  <bool-expr> ;
      | RULE     <expr>      ; }
    END_IMPLEMENTATION ]
END_FUNCTION_BLOCK

A FUNCTION_BLOCK declaration defines a stateful component. Every VAR_OUTPUT and VAR (local) name MUST be defined exactly once — either by a rule block (register), a derived assignment (:=), or an output-forwarding entry in WIRING.

WIRING is the canonical structural composition block (see §10.4). It contains child-input bindings and output forwarding only. Behavioral logic belongs in IMPLEMENTATION. A FUNCTION_BLOCK that hosts no behavioral logic beyond composition needs no IMPLEMENTATION block.

CONTINUOUS_REFERENCE is experimental (DEFAULT profile only). It declares ODEs for continuous-time analysis (numerical assurance chain). See §13.

3.3 FUNCTION

FUNCTION <name> ( [ <param> : <type> { , <param> : <type> } ] ) -> <type>
  { REQUIRE <bool-expr> ; }
  { ENSURE  <bool-expr> ; }
  [ VARIANT <expr> ; ]
  <body-expr>
END_FUNCTION

A FUNCTION is a pure, terminating computation. It has no state and produces no side effects. The body is a single expression. See §9.

3.4 EXTERN FUNCTION

EXTERN FUNCTION <name> ( [ <param> : <type> { , <param> : <type> } ] ) -> <type>
  ENSURE <bool-expr> ;
  { ENSURE <bool-expr> ; }
  [ BY <artifact-id> ; ]

An EXTERN FUNCTION declares a contract without a body. The contract (ENSURE clauses) is modelled as an assumption in the Z3 proof; the artifact named by BY (or auto-resolved from the registry) MUST discharge it. See §12.

3.5 EXTERN_REAL_CONTRACT

EXTERN_REAL_CONTRACT <name>
  [ VAR_INPUT  <var-decls> END_VAR ]
  [ VAR_OUTPUT <var-decls> END_VAR ]
  [ VAR_STATE  <var-decls> END_VAR ]
  SEMANTICS
    { <output> := <real-expr> ;
    | <state>  := <real-expr> ;
    | REQUIRE <range-expr> ; 
    | INVARIANT <range-expr> ; }
  END_SEMANTICS
END_EXTERN_REAL_CONTRACT

Declares a mathematical specification of an external continuous-time component. All variables MUST be typed MATHREAL or LREAL. REQUIRE declares input ranges; INVARIANT declares state invariants. The contract is consumed by the numerical assurance chain, not by compilation of a FUNCTION_BLOCK. See §13 and the Project Configuration Reference.

3.6 PROGRAM

PROGRAM <name>
  [ VAR_INPUT  <var-decls> END_VAR ]
  [ VAR_OUTPUT <var-decls> END_VAR ]
  [ VAR        <var-decls> END_VAR ]
  [ WIRING
      { composition-binding | output-forwarding }
    END_WIRING ]
  [ IMPLEMENTATION
      { derived-definition | register-rules }
      { INVARIANT <bool-expr> ;
      | ASSUME   <bool-expr> ;
      | REQUIRE  <bool-expr> ; }
    END_IMPLEMENTATION ]
END_PROGRAM

A PROGRAM is a non-instantiable root POU. It defines the process image interface of an executable deployment unit:

• VAR_INPUT fields are read from the input process image on each scan.
• VAR_OUTPUT fields are written to the output process image after each scan.
• VAR holds local state that persists across scans.

Restrictions. A PROGRAM MUST NOT: - Be instantiated inside another block (as a VAR declaration). Use a FUNCTION_BLOCK instead. - Declare a PARAMETER block. - Declare VAR_IN_OUT, VAR_EXTERNAL, or VAR_GLOBAL.

Pure composition. A PROGRAM that only wires together child instances and forwards their outputs needs no IMPLEMENTATION block:

PROGRAM Pasteurizer
  VAR_INPUT
    temperature   : MATHREAL;
    start         : BOOL;
    level_high    : BOOL;
    ...
  END_VAR
  VAR_OUTPUT
    heater_command : MATHREAL;
    valve_fill     : BOOL;
    ...
  END_VAR
  VAR
    sequence : BatchPasteurizer(HOLD_TIME := T#30s);
    pid      : TemperaturePID;
  END_VAR

  WIRING
    sequence(start := start, level_high := level_high, ...);
    pid(enable := sequence.heater, actual := temperature, ...);

    heater_command := pid.Output;
    valve_fill     := sequence.valve_fill;
    ...
  END_WIRING
END_PROGRAM

Runtime-owned values. The scan period, elapsed time, and real-time clock are provided by the runtime, not by VAR_INPUT. Time-dependent constructs (T_elapsed, WITHIN, timer presets) are driven by the runtime clock; they cannot be injected through the process image.

Execution. lola run <file.lola> compiles the PROGRAM to a native Rust binary, links it against lola-runtime-core (CyclicProgram trait), and starts the scan loop. See the CLI Reference and Process Image Reference.

---

4. Declarations and Storage

4.1 VAR_INPUT

Input variables are read-only within the block. They are set by the caller before each cycle. Input variables may be arrays (§4.6).

4.2 VAR_OUTPUT

Output variables are the writable state of the block. Each MUST be defined in the IMPLEMENTATION section. Output variables hold their value between cycles.

4.3 VAR (local state)

Local variables (VAR) behave identically to outputs except that they are not exposed at the block boundary and cannot be wired by a parent block. They are state that persists between cycles and are useful for hidden accumulator registers.

4.4 VAR_STATE (EXTERN_REAL_CONTRACT only)

State variables in an EXTERN_REAL_CONTRACT (§3.5) represent continuous internal state. They are typed MATHREAL or LREAL only.

4.5 Scalar variable declarations

var-decl := <name> : <type> ;

All primitive types (§5) are valid scalar types. WSTRING accepts an optional capacity bound:

<name> : WSTRING [ [ <capacity> ] ] ;

The capacity bounds the value of LEN; default 254 (IEC 61131-3). Capacity MUST be in the range 1..32 767 (INT range). This bound is a static semantic constraint, not a runtime buffer limit.

Z3 axiom. A WSTRING[n] declaration adds the axiom 0 ≤ LEN(s) ≤ n to the Z3 model as a type-level fact (not a premise). This makes LEN(s) ≤ capacity provable by Z3 without any INVARIANT or ASSUME. The empty initial value has LEN = 0.

4.6 ARRAY declarations

<name> : ARRAY [ <lo> .. <hi> ] OF <elem-type> ;

lo and hi are signed integer literals (DINT range). Inside a template FUNCTION_BLOCK (§4.10) the bounds may be arbitrary constant expressions over the type parameters (e.g. ARRAY[0..N-1], ARRAY[0..M*K-1]). elem-type is any scalar primitive type (WSTRING not accepted). Array inputs are indexed read-only; array outputs and locals are defined element-by-element in the IMPLEMENTATION.

Local VAR blocks additionally accept ARRAY OF <FBType> to declare an array of composition instances (§10).

4.7 INVERTED — Declared Signal Polarity at a Port

A BOOL port declaration may carry the modifier INVERTED:

VAR_INPUT  Estop : BOOL INVERTED; END_VAR
VAR_OUTPUT Run   : BOOL INVERTED; END_VAR

It declares that the external signal is the negation of the logical meaning — the case of fail-safe wiring, where a normally-closed contact carries TRUE while all is well.

Semantics (POL-1.1). The polarity is a boundary map applied exactly once:

• on an input, the internal value is NOT external, applied at sampling;
• on an output, the external value is NOT internal, applied at write-back.

Inside the block the name always carries its logical meaning. The negation appears in the emitted code at the boundary and nowhere else.

Where it may appear. Ports only, and BOOL scalars only.

Diagnostic	Condition
pol1-bool-only	the port is not a BOOL
pol1-ports-only	the declaration is a local, not a port — a local has no external side
pol1-scalar-only	the port is an aggregate; polarity applies to scalar signals

What it does not affect. Polarity is not part of the behavioural contract. It changes the port schema and the emitted code; it does not change contract_set_sha256. A proof about the block is a proof about its logical meaning, which is the point — the wiring convention belongs to the installation, not to the safety argument.

4.8 Physical unit annotations

A scalar MATHREAL, LREAL, or INT variable declaration may carry a physical unit annotation:

<name> : MATHREAL <m3/h> ;

The unit is a product/quotient of named dimension symbols (e.g. m/s, kg*m/s2, m3/h). Units are validated and resolved to a dimension by a separate pass; dimensionally inconsistent expressions are a static error. Unit annotations are experimental (DEFAULT profile).

4.9 CONST — Named Compile-Time Constants

A CONST block declares named, typed, compile-time constants.

CONST
    <name> : <scalar-type> := <literal> ;
    ...
END_CONST

Placement. The CONST block appears immediately after FUNCTION_BLOCK <name>, before any VAR block.

Allowed types. Any scalar primitive type (BOOL, INT, SINT, DINT, LINT, USINT, UINT, UDINT, ULINT, MATHREAL, LREAL). ARRAY and WSTRING are not supported.

Allowed values. The right-hand side must be a literal of the declared type, or a negated literal (e.g. -100.0). Expressions involving identifiers or arithmetic are not permitted.

Semantics. Constants are inlined by substitution before any other analysis pass. After substitution, no Z3 symbol is emitted for the constant name; it has no state, no proof obligation, and does not appear in generated code as a variable.

Scope. Constant names are visible everywhere in the FB (derived expressions, SET rule bodies and guards, INVARIANT, REQUIRE, ASSUME, wiring expressions). A constant name must not duplicate any variable declaration in the same FB.

Type checking. The declared type is checked against the literal at compile time (strict). Substituted literals obey the same type rules as inlined values.

Example:

FUNCTION_BLOCK PIDController
CONST
    LIM : MATHREAL := 100.0;
    KP  : MATHREAL := 2.0;
END_CONST
VAR_INPUT
    e : MATHREAL;
END_VAR
VAR
    integ : MATHREAL;
END_VAR
VAR_OUTPUT
    u : MATHREAL;
END_VAR
IMPLEMENTATION
    integ: SET CLAMP(integ + 0.1 * e, -LIM, LIM) OTHERWISE;
    u     := CLAMP(KP * e + integ, -LIM, LIM);
    INVARIANT u >= -LIM;
    INVARIANT u <=  LIM;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

After const substitution LIM → 100.0 and KP → 2.0, the block is equivalent to one with all literals written out explicitly. The SMT model never sees LIM or KP as identifiers.

---

4.10 PARAMETER — Configuration-Time Immutable Values

A PARAMETER block declares named, typed values that are fixed once at instantiation time and immutable for the lifetime of the instance.

PARAMETER
    <name> : <scalar-type> ;
    ...
    REQUIRE <bool-expr> ;   -- optional configuration-time constraint
    ...
END_PARAMETER

Placement. The PARAMETER block appears after any CONST block, before the first VAR block.

Allowed types. Any scalar primitive type (BOOL, INT, SINT, DINT, LINT, USINT, UINT, UDINT, ULINT, MATHREAL, LREAL). ARRAY and WSTRING are not supported.

Normative invariants (N1–N3).

• N1 — No scan-cycle evolution. Parameters are not registers; they have no current/next pair and no induction step. Their Z3 symbol is a free constant in every verification query.
• N2 — Immutable. A parameter name may not appear on the left-hand side of any SET rule or derived-output (:=) assignment.
• N3 — Configuration-time REQUIRE. REQUIRE clauses inside the PARAMETER block (param_requires) may only reference other PARAMETER names and literals. VAR_INPUT, registers, and derived values are scan-cycle entities and are not allowed. Diagnostic code: parameter-require-nonconfig-ref.

Scope. Parameter names are visible everywhere in the FB body: derived expressions, SET rule bodies and guards, INVARIANT, and REQUIRE. A parameter name must not duplicate any variable declaration in the same FB.

Verification. PARAMETER REQUIRE constraints are added as unconditional premises to every verification query, parallel to ASSUME clauses. The binder must discharge them at composition time (T3b.3).

REQUIRE referencing parameters. Input-level REQUIRE clauses may reference parameter names alongside input names (e.g. REQUIRE e >= -Lim). Such a REQUIRE is still a caller obligation — the caller knows both the runtime input value and the parameter bound they chose at instantiation.

Example:

FUNCTION_BLOCK ScaledGain
PARAMETER
    Kp  : MATHREAL;
    Lim : MATHREAL;
    REQUIRE Kp  >= 0.0;
    REQUIRE Kp  <= 1.0;
    REQUIRE Lim >  0.0;
END_PARAMETER
VAR_INPUT
    e : MATHREAL;
END_VAR
VAR_OUTPUT
    u : MATHREAL;
END_VAR
IMPLEMENTATION
    u := Kp * e;
    REQUIRE e >= -Lim;
    REQUIRE e <=  Lim;
    INVARIANT u >= -Lim;
    INVARIANT u <=  Lim;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The PARAMETER REQUIREs (Kp >= 0, Kp <= 1, Lim > 0) are configuration-time premises. Together with the input REQUIREs (e >= -Lim, e <= Lim) they let the solver prove the two invariants: Kp * e >= Kp * (-Lim) >= -Lim and Kp * e <= Kp * Lim <= Lim.

4.11 TYPE TEMPLATE PARAMETERS — <N: UINT>

A FUNCTION_BLOCK may declare one or more compile-time UINT parameters in angle brackets immediately after the name:

FUNCTION_BLOCK <name> "<" <param> ":" UINT { "," <param> ":" UINT } ">"

These type template parameters are substituted with concrete UINT literals at every instantiation site. The result is a fully concrete FUNCTION_BLOCK that the normal compilation pipeline handles without any template awareness.

Restrictions.

• Only UINT is supported as the parameter kind in this version.
• Template parameters are not registers, not proof symbols, and not visible in generated code or verification output.
• Array bounds inside the template body may reference type parameters using arithmetic: ARRAY[0..N-1], ARRAY[0..M*K-1].
• Aggregate bounds (SUM(i IN 0..N-1 : …)) may reference type parameters.
• Double-bracket index access a[i][j] for ARRAY OF ARRAY types is not yet supported; use flat row-major layout (a[i*K+j]) instead.

Comparison with CONST. A CONST value is shared by all instances of the same FB; it is a single type with one fixed numeric constant. A type template parameter produces a distinct type per substitution: Vec<3> and Vec<4> are separate types, each with its own verification context and its own generated output variable sizes.

Example — dot product of size N:

FUNCTION_BLOCK Vec<N: UINT>
VAR_INPUT
    a : ARRAY[0..N-1] OF LREAL;
    b : ARRAY[0..N-1] OF LREAL;
END_VAR
VAR_OUTPUT
    dot : LREAL;
END_VAR
IMPLEMENTATION
    dot := SUM(k IN 0..N-1 : a[k] * b[k]);
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Example — flat-layout matrix-vector multiply (M rows × K columns):

FUNCTION_BLOCK MatVec<M: UINT, K: UINT>
VAR_INPUT
    a : ARRAY[0..M*K-1] OF LREAL;   (* row-major: a[i*K+k] is row i, col k *)
    x : ARRAY[0..K-1]   OF LREAL;
END_VAR
VAR_OUTPUT
    y : ARRAY[0..M-1] OF LREAL;
END_VAR
IMPLEMENTATION
    y := ARRAY(i IN 0..M-1 : SUM(k IN 0..K-1 : a[i*K+k] * x[k]));
END_IMPLEMENTATION
END_FUNCTION_BLOCK

To instantiate a template block, append the concrete argument list in angle brackets in the VAR declaration (§10.7):

VAR
    v3 : Vec<3>;
    mv : MatVec<2, 3>;
END_VAR

Static semantics. A template block is not independently compiled; only its monomorphized instances are. The compiler performs monomorphization at the materialize_closure phase: it substitutes all type-parameter references with the concrete values, resolves all symbolic bounds to integer literals, and treats the result as an ordinary concrete FUNCTION_BLOCK. Diagnostic codes:

Code	Condition
structure	Resolver cannot find the template base type
composition	Non-template FB used with <…> syntax
structure	Wrong number of type arguments

---

5. Type System

LoLa has seven primitive type families. Every variable and expression has exactly one primitive type.

5.1 BOOL

The Boolean type. Values: TRUE and FALSE. Supports: AND, OR, XOR, NOT, =, <>. Cannot be used with arithmetic or ordering comparison operators.

In the Z3 model, BOOL is a Bool sort.

Initial value of a BOOL output/local: FALSE.

5.2 Signed Integers — SINT, INT, DINT, LINT

Four signed, fixed-width two's-complement integer types:

Type	Width	Range
SINT	8 bits	−128 .. 127
INT	16 bits	−32 768 .. 32 767
DINT	32 bits	−2 147 483 648 .. 2 147 483 647
LINT	64 bits	−9 223 372 036 854 775 808 .. 9 223 372 036 854 775 807

In the Z3 model, signed integers are BitVec(n) with signed interpretation.

Arithmetic. +, -, *, /, MOD apply to matching same-type operands and produce the same type. Arithmetic wraps modulo 2ⁿ (two's-complement). The compiler issues a definedness obligation for division and MOD (divisor ≠ 0; and for signed MIN/-1 overflow in some paths). Unary minus applies to signed integers.

Comparison. =, <>, <, <=, >, >= apply with signed interpretation.

Negative literals. Signed typed literals (SINT#, DINT#, LINT#) only accept non-negative values (0..MAX). Negative values are written with unary minus (-SINT#5) or using the named minimum constant (SINT_MIN for −128, INT_MIN for −32 768, etc.).

Initial value: 0 (all bits zero).

5.3 Unsigned Integers — USINT, UINT, UDINT, ULINT

Four unsigned, fixed-width integer types:

Type	Width	Range
USINT	8 bits	0 .. 255
UINT	16 bits	0 .. 65 535
UDINT	32 bits	0 .. 4 294 967 295
ULINT	64 bits	0 .. 18 446 744 073 709 551 615

In the Z3 model, unsigned integers are BitVec(n) with unsigned interpretation.

Arithmetic. +, -, *, /, MOD apply with unsigned semantics. Arithmetic wraps modulo 2ⁿ. Unary minus does NOT apply to unsigned integers.

Comparison. =, <>, <, <=, >, >= apply with unsigned interpretation. UINT#32768 > UINT#1 is TRUE; the same bit pattern interpreted as INT would be negative.

Typed literals. USINT#n, UINT#n, UDINT#n, ULINT#n with decimal or 16# hexadecimal. Named constants: USINT_MIN, USINT_MAX, etc.

Initial value: 0.

5.4 Bit Strings — BYTE, WORD, DWORD, LWORD

Four unsigned bit-carrier types. The semantic distinction from unsigned integers is expressional: bit strings participate in bitwise AND/OR/XOR/NOT but not in aggregate reductions (SUM/MIN/MAX). They compare with unsigned ordering.

Type	Width	Range (unsigned)
BYTE	8 bits	0 .. 255
WORD	16 bits	0 .. 65 535
DWORD	32 bits	0 .. 4 294 967 295
LWORD	64 bits	0 .. 18 446 744 073 709 551 615

Operators. AND, OR, XOR, NOT (bitwise). +, -, *, /, MOD (arithmetic wrapping, experimental — rejected by PILOT). =, <>, <, <=, >, >= with unsigned interpretation. Not allowed in SUM/MIN/MAX aggregates.

Typed literals. BYTE#n, WORD#n, DWORD#n, LWORD#n.

Initial value: 0.

5.5 MATHREAL and LREAL

MATHREAL and LREAL both denote the set of mathematical real numbers (ℝ) in the LoLa semantic model. There is no machine representation at the language level; representation is a deployment decision (see §13 and §17).

In the Z3 model, MATHREAL and LREAL values are RealSort (exact arithmetic).

Operators. +, -, *, /, =, <>, <, <=, >, >=, unary minus. MOD, AND, OR, XOR, NOT do not apply.

Type compatibility. MATHREAL and LREAL are considered compatible as outputs of derived assignments (lreal_var := real_expr is accepted). They are not identical; LREAL signals Float64-or-better precision at a future Representation Boundary (see §13.2).

Literals. Decimal float literals (§2.3.5): 2.5, 0.001. Integer literals are NOT automatically promoted to MATHREAL in expressions — use 1.0 not 1.

Initial value: 0.0 (exact zero).

5.6 TIME

A non-negative duration type. Values are in milliseconds. The Z3 model represents TIME as an unbounded non-negative integer (no bit-width). TIME is used for timer presets and elapsed values.

Operators. =, <>, <, <=, >, >= (unsigned ordering). Arithmetic and bitwise operators do not apply to TIME. DT (§6.15) produces a TIME value.

Literals. Time literals (§2.3.6): T#100ms, 2s, 1min.

Profile note. TIME-valued inputs/outputs are experimental (rejected by PILOT). TIME literals and internally accumulated timer state are accepted by all profiles.

Initial value: T#0ms.

5.7 WSTRING

An uninterpreted wide-string carrier. Only equality (=, <>) and LEN (§6.14) apply. No arithmetic, ordering, or bitwise operators. Cannot be used as an array element type.

Literals. Double-quoted string literals (§2.3.7): "RUNNING".

Profile note. WSTRING is experimental (rejected by PILOT).

Initial value: "" (empty string).

5.8 Array Types

ARRAY[lo..hi] OF T where T is a scalar primitive type. Arrays are referenced by index: a[i]. Index expressions must produce INT.

5.9 Type Compatibility

All binary operators require both operands to be of the same type. There is no implicit promotion. Explicit conversion functions (§6.16) must be used to change type width or signedness.

5.10 Type Conversions

Twenty-two built-in conversion functions provide explicit widening, narrowing, and signed/unsigned reinterpretation between fixed-width integer types:

Signed widening (lossless): SINT_TO_INT, INT_TO_DINT, DINT_TO_LINT, INT_TO_LINT, DINT_TO_LINT

Signed narrowing (modulo 2ⁿ, not lossless): INT_TO_SINT, DINT_TO_INT, LINT_TO_INT, LINT_TO_DINT

Unsigned widening (lossless): USINT_TO_UINT, UINT_TO_UDINT, UDINT_TO_ULINT

Unsigned narrowing (modulo 2ⁿ): UINT_TO_USINT, UDINT_TO_UINT, ULINT_TO_UDINT

Signed ↔ Unsigned (same bit pattern, different interpretation): SINT_TO_USINT, USINT_TO_SINT, INT_TO_UINT, UINT_TO_INT, DINT_TO_UDINT, UDINT_TO_DINT, LINT_TO_ULINT, ULINT_TO_LINT

All conversions are syntactically a function call: SINT_TO_INT(expr). The argument MUST have the source type; the result has the destination type.

---

6. Expressions

6.1 Operator Precedence

From loosest to tightest binding:

Level	Operators	Associativity
1	OR	left
2	XOR	left
3	AND	left
4	NOT (unary prefix)	right
5	=, <>, <, <=, >, >=	non-assoc. (one comparison per expr)
6	+, -	left
7	*, /, MOD	left
8	unary -	right
9	primary (literals, calls, indexing, IF...THEN...ELSE, parentheses)	—

Parentheses override precedence. Only one comparison operator may appear per (unparenthesised) expression: a < b < c is a parse error; write a < b AND b < c.

6.2 Arithmetic Operators

+, -, *, /, MOD — both operands MUST be the same type.

Permitted types by operator:

Operator	Permitted types
+, -, *, /	Signed integers, unsigned integers, MATHREAL/LREAL, bit strings (experimental)
MOD	Signed integers, unsigned integers, bit strings (experimental); NOT MATHREAL/LREAL

Arithmetic on integer and bit-string types wraps modulo 2ⁿ in the Z3 model and in emitted code. Overflow is not a Z3 error; the value wraps.

Definedness obligations. Division and MOD are partial operations: the compiler generates a proof obligation that the divisor is non-zero on every evaluation path:

Operation	Obligation
a / b (integer or MATHREAL)	b ≠ 0
a MOD b (integer)	b ≠ 0
a / b where a is a signed integer type and a = INT_MIN	additionally b ≠ -1 (prevents wrap-around trap)
a[i] where i is not a compile-time constant	lo ≤ i ≤ hi (bounds)

Obligations are path-sensitive: a division inside IF c THEN a/b ELSE 0 only requires the non-zero proof on the branch where the division executes. The compiler carries the guarding IF on the AST→IR path and does not hoist partial operations out of their guards (CSE is informed of this classification via lola/definedness.py).

If any obligation cannot be proved from the available INVARIANTs, ASSUMEs, and REQUIREs, the compiler raises a compile error naming the unresolved obligation and the location. No runtime check is emitted; the compiled program is only produced when all obligations are statically discharged.

6.3 Bitwise Operators

AND, OR, XOR (binary), NOT (unary prefix) — both operands MUST be the same type.

Permitted types: BOOL, and any bit-string type (BYTE, WORD, DWORD, LWORD).

NOT on BOOL is logical negation; NOT on a bit string is bitwise complement (all 64 bits inverted for LWORD).

6.4 Comparison Operators

=, <> — equality/inequality. Both operands MUST be the same type. Applies to all primitive types including WSTRING and TIME.

<, <=, >, >= — ordering. Both operands MUST be the same type. Applies to all numeric types (integers, bit strings, MATHREAL/LREAL, TIME) but NOT to BOOL or WSTRING.

Signed integers use signed ordering; unsigned integers and bit strings use unsigned ordering. INT#-1 < INT#0 is TRUE; WORD#0xFFFF < WORD#0 is FALSE (65535 > 0 unsigned).

6.5 Unary Operators

NOT — logical negation (BOOL) or bitwise complement (bit strings). See §6.3.

Unary - — arithmetic negation. Applies to signed integers (SINT, INT, DINT, LINT) and MATHREAL/LREAL. Does NOT apply to unsigned integers or bit strings.

6.6 Conditional Expression (IF … THEN … ELSE)

IF <bool-expr> THEN <expr> ELSE <expr>

The condition MUST be BOOL. Both branches MUST be the same type. The result type is that of the branches. This is an expression (not a statement) and may appear anywhere an expression is accepted.

6.7 Function Calls

<name> ( <expr> { , <expr> } )

name MUST be a FUNCTION or EXTERN FUNCTION declared in the same file (see §9 and §12). Arguments MUST match parameter types positionally. The result type is the declared return type.

6.8 Array Indexing

<array-name> [ <index-expr> ]

array-name MUST be an array input, output, or local. index-expr MUST be of type INT. The result type is the array element type.

Out-of-bounds index behaviour is an unresolved definedness obligation (the compiler may reject programs where an out-of-range index is possible).

6.9 Member Access (Composition)

<instance-name> . <field-name>
<instance-name> . <field-name> [ <index> ]  -- output array element
<array-name> [ <index> ] . <field-name>     -- ARRAY OF FB element output

instance-name MUST be a local composition instance (§4.9, §10). field-name MUST be a declared VAR_OUTPUT of the instance's type. See §10.

6.10 Aggregates (SUM, COUNT, ALL, ANY, EXISTS, MIN, MAX)

<op> ( <ivar> IN <lo> .. <hi> : <body-expr> )

ivar is a fresh loop variable bound to each integer in lo..hi. body-expr is evaluated with ivar substituted; it may reference ivar, inputs, and outputs.

Operator	Body type	Result type
SUM	numeric (not bit string)	same as body
MIN, MAX	numeric (not bit string)	same as body
COUNT	BOOL	INT
ALL, ANY	BOOL	BOOL
EXISTS	any	BOOL (true iff body is ever nonzero/true)

The range lo..hi MUST be statically bounded (literal integers). The number of elements may not exceed the profile's max_aggregate_n (default 256).

EXISTS is experimental.

6.11 Array Constructor (ARRAY)

ARRAY ( <ivar> IN <lo> .. <hi> : <body-expr> )

Constructs an array of length hi - lo + 1. Equivalent to [body[lo], body[lo+1], ..., body[hi]]. The result type is ARRAY[lo..hi] OF T where T is the type of body-expr. Used in derived array definitions.

6.12 Declarative Sort (SORT)

SORT ( <array-name> )

Returns a sorted (ascending) copy of an input array. The result type is the same array type. Sorting order is the natural ordering of the element type. SORT expresses "there exists a permutation that is sorted"; the model adds the PERMUTATION_OF proof obligation automatically.

6.12a Semantic Array Predicates

SORTED ( <array-name> )
PERMUTATION_OF ( <result-array>, <source-array> )

Both forms are BOOL expressions and may be used as RULE, INVARIANT, or ordinary expression clauses. SORTED(a) holds iff every adjacent pair in the array's logical index range is nondecreasing. PERMUTATION_OF(result, source) requires equal element types and identical bounds, and holds iff every value has the same multiplicity in both arrays. It is therefore exact in the presence of duplicates; it is not a sum/XOR/hash approximation.

These binary semantic predicates are distinct from the unary FUNCTION postcondition ENSURE PERMUTATION_OF(array_parameter) in §9.5. The unary form is discharged structurally for modular FUNCTION verification. The binary form is an explicit bounded relation over two concrete fixed arrays and is lowered from one canonical definition into the normal SMT and guided-proof backends.

Guided synthesis GS-v2-C currently accepts the binary predicates only for fixed machine-integer arrays. The ordinary language type checker also requires SORTED elements to have an ordering and rejects mismatched permutation shapes.

6.13 CLAMP

CLAMP ( <x>, <lo>, <hi> )

Equivalent to IF x < lo THEN lo ELSE IF x > hi THEN hi ELSE x. All three arguments MUST be the same numeric type. Result type equals argument type.

6.14 LEN

LEN ( <wstring-expr> )

Returns the length (number of characters) of a WSTRING expression as an INT. The result is always in the range 0..capacity, where capacity is the declared WSTRING capacity (or 254 if not specified). LEN may only be applied to WSTRING.

6.15 DT (Cycle Time)

DT is a zero-argument keyword expression that returns the current cycle time as a TIME value. It represents the actual scan period in the Z3 model as an uninterpreted non-negative constant bounded by the profile's dt_max_ms deployment fact.

DT MUST NOT appear in ASSUME or REQUIRE clauses (assuming the runtime clock is not sound; see §8.2).

DT is experimental in input/output positions (DEFAULT profile).

6.16 PRE (Pre-State Read)

PRE ( <x> )

PRE(x) returns the start-of-cycle (pre-state) value of a stateful signal, regardless of where it appears. It is the cycle-cut operation: it breaks the algebraic loop that LoLa's fresh-read semantics would otherwise create.

Motivation. Derived outputs (:=) see the freshly computed (next-state) values of registers by default. This means u := f(y); y: SET g(u) creates a same-cycle algebraic loop that the compiler rejects as a combinational cycle. With PRE,

u := f(PRE(y));     // reads y from the PREVIOUS cycle
y: SET g(u) OTHERWISE;

is valid: u depends on y_prev (the pre-state), and y_next = g(u) is computed from u in the same cycle. There is no cycle.

Allowed operands:

Operand type	Semantics
VAR register	Returns the stored value at the start of this cycle
VAR_OUTPUT with SET rule	Same — reads the register, not the freshly computed result
VAR_INPUT	Returns the input value (pre-state == current for inputs)
Composition output alias (child.y)	Resolved to the pre-state of the underlying register after flattening

PRE applied to a purely derived output (defined only by :=, no SET rule) is a compile error — derived outputs have no stored pre-state.

SMT model. PRE(x) maps directly to the cur[x] Z3 constant (the pre-state symbol that is always present). It does not trigger the _get_reg path, so no cycle arc is added to the dependency graph.

Backend lowering. ST and Rust backends lower PRE(x) to ir.Ref(x) — reading the register's current (old) value, which both backends already maintain before the update assignments.

Restrictions. PRE is currently limited to simple variable references (PRE(name)) and composition output aliases (PRE(child.field)). It may not be applied to arbitrary expressions.

6.17 Temporal Predicates (HELD, ELAPSED)

See §11.

---

7. State Transitions

7.1 Register Rules

A register rule block defines a VAR_OUTPUT or VAR (local) name by a prioritised set of actions:

<name> :
    <action> [<value>] WHEN <guard> [PRIO <n>] ;
    ...
    <action> [<value>] OTHERWISE ;

guard is a BOOL expression. action is ON, OFF, HOLD, or SET (§7.2). n is an integer priority (§7.4). The OTHERWISE clause is syntactic sugar for an always-true guard.

At least one rule MUST appear. If no OTHERWISE is present and no rule fires, the output holds its pre-cycle value (implicit HOLD).

7.2 Actions

Action	Effect
ON	Set output to TRUE
OFF	Set output to FALSE
HOLD	Keep the pre-cycle value
SET <expr>	Assign the value of <expr>

ON and OFF apply only to BOOL outputs.

HOLD makes the implicit pre-cycle default explicit. It is always valid and carries no semantic difference from the implicit hold.

SET <expr> applies to any output type. expr MUST be of the declared output type.

7.3 Guards (WHEN, OTHERWISE)

WHEN <bool-expr> — the rule fires when bool-expr evaluates to TRUE at the start of the cycle (using start-of-cycle values, §15.2).

OTHERWISE — the rule always fires. Only one OTHERWISE rule is allowed per output. An OTHERWISE rule has no PRIO; it always fires unless superseded by a higher-priority WHEN rule that fires on the same cycle.

7.4 Priority (PRIO)

Every rule has an integer priority. The default priority is 0. If two rules both fire on the same cycle, the one with the higher numerical priority wins.

Rules with equal priority that can simultaneously fire with different effects are an ambiguity: the compiler rejects the program with a counterexample.

A PRIO value may be any non-negative integer in the DINT range.

7.5 Derived Assignments

<name> := <expr> ;

A derived assignment defines a VAR_OUTPUT or VAR as a combinatorial function of the current cycle's inputs and pre-cycle state. The value is computed freshly each cycle from start-of-cycle values; it holds no persistent state.

A derived name MUST NOT be referenced in HELD/ELAPSED conditions (§11, §14.5).

Exactly one of {rule block, derived assignment} may define each output or local.

7.6 Pre-State Semantics and Atomic Commit

All expressions in rule guards, rule values, and derived assignments refer to start-of-cycle values: the inputs and output/local values from the end of the previous cycle. There is no sequencing within a cycle; no register definition can observe a value written by another register in the same cycle.

After all rules and derivations are evaluated, all outputs and locals are updated atomically to their new values. The new state becomes the pre-cycle state for the next cycle.

---

8. Contracts and Proof

8.1 INVARIANT

Syntax

INVARIANT <bool-expr> ;

Context

Inside IMPLEMENTATION ... END_IMPLEMENTATION of a FUNCTION_BLOCK, after all rule and derived definitions.

Static semantics

bool-expr MUST be of type BOOL. HELD and ELAPSED MUST NOT appear in an invariant expression. May reference inputs, outputs, locals, and derived values.

Semantics

An INVARIANT is a proof obligation that the compiler MUST discharge:

1. Power-up obligation: bool-expr holds at the state before the first scan — every output and local at its initial value (§5), inputs unconstrained (or constrained by ASSUME). Derived definitions have not run yet, so a derived output reads as its initial value there, not as the value its definition would produce.
2. Inductive-step obligation: if bool-expr held at the end of the previous cycle, it holds at the end of the current cycle for all possible inputs (or those satisfying ASSUME).

An INVARIANT therefore claims both: at power-up, and after every completed scan. A relation that only holds once a scan has computed it — a combinational identity between inputs and outputs, say — is not an invariant in this sense and belongs in a RULE (§8.6): before the first scan the outputs it relates do not exist yet.

Both obligations are discharged by the Z3 model. If either fails, compilation is rejected with a counterexample (a model assignment that witnesses the violation).

Proof obligations

• Power-up: INVARIANT evaluated at default output values and unconstrained inputs, with derived definitions NOT evaluated.
• Step: INVARIANT at state(t+1) assuming INVARIANT at state(t).

Only an invariant that discharges both becomes a premise for the output obligations. A declared invariant is a claim, not a fact: one whose own proof failed may not certify anything else.

Assurance / dependencies

ASSUME clauses (§8.2) are added as premises to both obligations. REQUIRE clauses (§8.3) are premises for the step check only (a caller REQUIRE is a precondition the environment asserts, not something LoLa proves the environment always satisfies).

Diagnostics

• invariant-init — initial state violates the invariant.
• invariant-step — the step can violate the invariant.

Example

FUNCTION_BLOCK Counter
VAR_INPUT enable : BOOL; END_VAR
VAR_OUTPUT count : INT; END_VAR
IMPLEMENTATION
    count:
        SET count + 1 WHEN enable PRIO 1;
        HOLD OTHERWISE;
    INVARIANT count >= 0;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

See also

Introduction by Example §4 · guide-verified-functions.md

---

8.2 ASSUME

Syntax

ASSUME <bool-expr> ;

Context

Inside IMPLEMENTATION ... END_IMPLEMENTATION, after rule/derived definitions.

Static semantics

bool-expr MUST be BOOL. MUST reference only input variables. HELD, ELAPSED, and DT MUST NOT appear.

Semantics

An ASSUME constrains the environment: the compiler is permitted to assume that bool-expr holds at every cycle when discharging INVARIANT proof obligations. In the Z3 model, the assumption is asserted as a premise unconditionally.

Soundness restriction. ASSUME may only reference inputs because the environment (external caller) controls only inputs. Assuming something about internal state or derived values would allow the model to discharge invariants while the real system violates them.

Example

ASSUME flow >= 0.0;

---

8.3 REQUIRE

Syntax

REQUIRE <bool-expr> ;

Context

Two contexts:

(a) FUNCTION_BLOCK: inside IMPLEMENTATION, after rule/derived definitions. (b) FUNCTION: in the function header, before the body.

Static semantics

In a FUNCTION_BLOCK: bool-expr MUST be BOOL and reference inputs only. In a FUNCTION: bool-expr MUST be BOOL and reference parameters only. HELD, ELAPSED, and DT MUST NOT appear.

Semantics

A REQUIRE is a caller precondition. It differs from ASSUME in intent and proof-obligation propagation:

• The compiler treats it as a premise when proving the block's own INVARIANTs (same as ASSUME).
• When the block is composed (§10), the caller must prove the REQUIRE holds for the values it wires. Composition turns REQUIREs into proof obligations on the wiring.

The compiler reports unmet REQUIREs as caller actions: requirements that the parent block or system integrator must discharge.

Diagnostics

Unmet REQUIRE: reported as "Caller action: discharge or monitor …" in the check output.

---

8.4 ENSURE

Syntax

ENSURE <bool-expr> ;

Context

(a) FUNCTION body: after REQUIRE, before body expression. (b) EXTERN FUNCTION: one or more ENSURE clauses required.

Semantics

In a FUNCTION: an ENSURE is a postcondition that the compiler proves holds for all inputs satisfying REQUIRE, using the function's defined body as the model.

In an EXTERN FUNCTION: an ENSURE is a contract that the compiler assumes as an unconditional premise in the FUNCTION_BLOCK model. The registered artifact MUST discharge it (§12). The name <funcname> refers to the function's return value inside the ENSURE expression.

Special form: ENSURE PERMUTATION_OF

ENSURE PERMUTATION_OF ( <array-name> ) ;

Asserts that the function result is a permutation of the named parameter. Used on sorting functions. See §9.5.

---

8.5 VARIANT

Syntax

VARIANT <expr> ;

Context

FUNCTION header (at most one per function).

Semantics

Declares a termination measure for a recursive function. The expression MUST be of a numeric type and strictly decreasing on each recursive call. The compiler emits a proof obligation that the variant is non-negative at each call and decreases on each recursive call. Without a VARIANT, a recursive function is rejected.

---

8.6 RULE

Syntax

RULE <expr> ;

Context

Inside IMPLEMENTATION, after rule/derived definitions.

Semantics

A RULE states a relation of an executed scan: what holds between the values once the scan has computed them. Unlike an INVARIANT (§8.1) it makes no claim about the power-up state, where the outputs it relates still carry their initial values — which is what a combinational identity such as (live OR faults) = status needs, and why writing one as an INVARIANT is correctly refused.

The exemption follows the construct, not the shape of the claim: the same relation written as an INVARIANT keeps its power-up obligation. It is otherwise proven exactly like one; being exempt from the power-up state does not make a RULE weaker anywhere else.

A RULE is a declarative specification predicate added to the model. Its interaction with INVARIANTs beyond the above is experimental. Use INVARIANT for all standard proof obligations.

Status: experimental.

---

8.6a Typed relational clauses — ONLY_WHEN, IMPLIES, IFF, EXCLUDES

Normative source: ADR NS-1 v3 (docs/adr-necessary-sufficient-clauses.md).

Syntax

RULE <literal> ONLY_WHEN <condition> ;   (* necessary:  literal → condition *)
RULE <condition> IMPLIES <literal> ;     (* sufficient: condition → literal *)
RULE <output> IFF <condition> ;          (* definition: both directions     *)
RULE <source> EXCLUDES <source> ;        (* exclusion:  NOT (a AND b)       *)

<literal> names exactly one declared BOOL output, bare (q) or negated (NOT q); the condition must not reference that base output (ns1-literal-not-output, ns1-condition-references-output). IFF admits only the positive output on the left. EXCLUDES takes two BOOL sources. An untyped RULE <expr>; remains valid and is counted unclassified.

Context

Exactly where RULE is admitted, inside IMPLEMENTATION. Typed clauses are refused in CONTRACT (NS-1.4). The keyword REQUIRES is reserved solely to answer with a did-you-mean-ONLY_WHEN diagnostic; the caller obligation remains REQUIRE.

Semantics

Each clause normalises to exactly the boolean term the equivalent plain RULE produces (ONLY_WHEN/IMPLIES to the disjunction, IFF to the conjunction of both directions, EXCLUDES to NOT (a AND b)), so contract_set_sha256 is unchanged for logically equal contracts. The authored direction survives as provenance and feeds:

• the per-output balance (INFO): ON/OFF × necessary/sufficient, plus defined (IFF), exclusion, and unclassified counts;
• the pair analysis — an explanation, never a verdict: collisions are reported as warning: [ns1-pair-conflict] while the verdict stays with the ordinary proof over the clause set;
• IFF materialisation: an output defined only by RULE q IFF c; becomes the derived q := c (provenance defined), after a fail-closed consistency check against every other clause (ns1-iff-conflict; undecidable fragments refuse as ns1-iff-unknown);
• the temporal rung-1 refusal: a HELD/ELAPSED-carrying clause governing an output without an implementation refuses typed (ns1-temporal-rung1) — provide an implementation and the clause is an ordinary proof obligation.

Status: normative (NS-1 v3).

Task-oriented guide: How to specify an output relationally.

---

8.7 PERMUTATION_OF (in FUNCTION)

See §8.4 (ENSURE PERMUTATION_OF) and §9.5.

---

9. Functions and Recursion

9.1 FUNCTION Definition

FUNCTION <name> ( [ <param> : <type> { , <param> : <type> } ] ) -> <type>
  { REQUIRE <bool-expr> ; }
  { ENSURE  <bool-expr> ; }
  [ VARIANT <expr> ; ]
  <body-expr>
END_FUNCTION

A FUNCTION is a pure, total computation — no side effects, no state. The body is a single expression whose type must match the declared return type. Parameters are read-only.

9.2 REQUIRE and ENSURE in Functions

REQUIRE clauses state preconditions the caller must satisfy.

ENSURE clauses state postconditions the function body must satisfy. The special name <funcname> (the function's own name) refers to the return value inside ENSURE expressions:

FUNCTION clamp(x : INT, lo : INT, hi : INT) -> INT
    REQUIRE lo <= hi;
    ENSURE clamp >= lo;
    ENSURE clamp <= hi;
    IF x < lo THEN lo ELSE IF x > hi THEN hi ELSE x
END_FUNCTION

9.3 Recursion and VARIANT

A function may call itself recursively. A VARIANT MUST be provided for any recursive function. The VARIANT expression MUST:

• be of a numeric type;
• be strictly less at each recursive call than at the current call;
• be non-negative (≥ 0) at every call.

The compiler proves both VARIANT obligations via Z3.

9.4 Array Parameters and Return Types

Functions may accept ARRAY[lo..hi] OF T parameters and return ARRAY[lo..hi] OF T. Array bounds MUST be statically given; hi - lo + 1 elements are passed by value.

9.5 PERMUTATION_OF

ENSURE PERMUTATION_OF ( <array-param-name> ) ;

Asserts that the function's return value is a permutation of the named array parameter — every element appears exactly once, none added or dropped. PERMUTATION_OF is typically combined with element-ordering ENSURE clauses (or INVARIANTs on the result) to prove a full sort contract.

Why a separate construct. The logical encoding of a permutation — "there exists a bijection between result and parameter indices" — requires indexing an array at a symbolic position, which makes the SMT query exponentially expensive (measured: k=20 elements, full encoding >120 s, times out). LoLa avoids the SMT query entirely: instead, it checks the return expression structurally, certifying by construction that no values are invented.

Structurally valid return forms. The compiler accepts exactly four shapes:

Form	Rule
target (the parameter itself)	Identity permutation
IF c THEN perm₁ ELSE perm₂	Both branches must be valid permutations of target
f(…, target_perm_arg, …) where f has ENSURE PERMUTATION_OF(…)	f's promise is used without inspecting its body (modular)
ARRAY(i IN lo..hi : target[<index-expr>])	Comprehension — see below

Any other expression shape (arithmetic, non-permuting call, non-target variable) is a compile error.

Comprehension proof. A comprehension that reads target at a computed index is the one place where the compiler invokes Z3, but only for the cheap half: it proves that the index expressions are in range and pairwise distinct (bounded-range distinctness for k elements takes <0.1 s). The values themselves are shown to be exactly those of target by construction — the comprehension body has the form target[f(i)] where f(i) is the witness, so the value equation holds without a query. The compiler lifts the index expression off the syntax and checks ∀ distinct i,j: f(i) ≠ f(j) and f(i) ∈ [lo, hi].

REQUIRE interaction. If the REQUIRE clause constrains the index range (e.g. REQUIRE k <= 5), the SMT check for the comprehension incorporates that constraint. An index that is in-range only under a REQUIRE is accepted.

Errors. If the structural check fails, the compiler reports the specific element or sub-expression that violates the permutation property. For a comprehension that does not rearrange (an element is duplicated or dropped), the solver produces a witness and the error message shows the concrete index sequence that fails.

---

10. Composition

A FUNCTION_BLOCK or PROGRAM may embed other function blocks as local sub-instances. Composition is resolved at compile time by inlining: the sub-instance's entire Z3 model is substituted into the parent. After flattening the result is an ordinary flat program; the full proof pipeline applies to it.

10.1 Scalar Instance Declaration

VAR
    <name> : <FBType> [ "<" UINT_LIT { "," UINT_LIT } ">" ] ;
END_VAR

FBType is the name of another FUNCTION_BLOCK whose source file (<FBType>.lola) is visible on the search path. Examples:

VAR
    r  : RS;         (* plain instance *)
    v  : Vec<3>;     (* template instantiation — Vec<N: UINT> with N=3 *)
    mv : MatVec<2, 3>; (* two type arguments *)
END_VAR

If the type name carries angle-bracket arguments the compiler performs monomorphization (§4.10) before any other analysis.

10.2 Wiring

10.2a — WIRING block (canonical form)

The canonical way to wire sub-instances is with a top-level WIRING block (see §3.2 for FUNCTION_BLOCK, §3.6 for PROGRAM):

WIRING
    <instance>( <input> := <expr> , … ) ;   (* child-input binding *)
    <output>  := <source> ;                  (* output forwarding *)
END_WIRING

Child-input binding. Every VAR_INPUT of the sub-instance MUST be wired. Binding expressions may reference any value in the parent scope (inputs, locals, derived outputs). No implicit connections; every port is wired explicitly.

Output forwarding assigns a VAR_OUTPUT of the parent block to a source value. The RHS MUST be one of: - A local variable name - An instance output path (inst.port) - A VAR_INPUT passthrough

Arithmetic, boolean, or conditional expressions are not permitted on the RHS of output forwarding. Such computations belong in IMPLEMENTATION as derived assignments (:=), and the result variable is then forwarded.

WIRING
    pid(measurement := temp, setpoint := target, enable := active);
    output := pid.result;    (* forwarding — reference only *)
END_WIRING

10.2b — Legacy IMPLEMENTATION form (deprecated)

Sub-instance wiring may also appear inside IMPLEMENTATION:

IMPLEMENTATION
    <instance>( <input> := <expr> , … ) ;
END_IMPLEMENTATION

This form is accepted with a deprecation warning. Move it to a WIRING block (§3.2). The legacy form will be removed in a future language version.

Every VAR_INPUT of the sub-instance must be wired exactly once. Example:

r(S := set_signal, R := reset_signal);

10.3 Output Access

A scalar sub-instance's outputs are read as member accesses:

<instance>.<output-name>

For example, r.Q reads the Q output of the RS instance r. Members may appear anywhere a normal expression is valid.

An array output of a sub-instance is read as a member with an index:

<instance>.<array-output>[<index>]

10.4 Array of Function Blocks

Local VAR blocks additionally accept arrays of FB instances:

VAR
    <name> : ARRAY [ <lo> .. <hi> ] OF <FBType> ;
END_VAR

All elements share the same type and are wired with a generate statement: the bound variable (written [i] on the call) ranges over the declared index set and the compiler unrolls it:

VAR
    ch : ARRAY[0..3] OF Channel;
END_VAR
IMPLEMENTATION
    ch[i](raw := raw[i], thresh := thresh);

The index variable i is implicitly bound in the wiring; it may appear in any wiring expression on the right-hand side. This is the LoLa equivalent of IEC 61131-3's FOR-GENERATE construct, unrolled at compile time under the Bounded-Cycle rule.

Outputs of array elements are accessed as:

ch[0].margin          // constant index
ch[i].active          // binder from ARRAY / aggregate / comprehension
ARRAY(i IN 0..3 : ch[i].active)   // comprehension over all outputs

10.5 Inlining Semantics

During flattening, the compiler:

1. Compiles the sub-instance FB independently, producing its Z3 model.
2. Prefixes all internal variable names with <instance>__ to create hidden locals (e.g., r__Q, r__state).
3. Substitutes each wired expression for the corresponding sub-instance input symbol throughout the model.
4. Exposes wired outputs as derived aliases in the parent scope.

The result is an ordinary flat program. No runtime representation of the composition boundary exists; it is a compile-time structuring mechanism only.

For ARRAY OF FB, each element is flattened separately, producing one hidden variable per element per sub-instance field.

10.6 Proof Obligation Propagation

Sub-instance REQUIRE clauses become proof obligations at the wiring site. The compiler classifies each wiring using a wiring authority policy:

Authority	Wiring type	Effect
BOUNDARY	A single parent input (or a static element of one) passes through unchanged	Clause propagates upward; parent discharges it at its own REQUIRE level
LOCAL	Any other expression (constant, computed, composite, dynamic index)	Parent must discharge the obligation immediately at the call site

Example — BOUNDARY authority:

// Child FB Channel REQUIRES raw >= 0.
// Wiring passes parent input directly → authority is BOUNDARY.
ch[i](raw := raw_input[i], thresh := thresh);
// The REQUIRE propagates: the parent must declare REQUIRE raw_input[i] >= 0.

Example — LOCAL authority:

// Wiring computes a value → authority is LOCAL.
ch[i](raw := raw_input[i] - offset, thresh := thresh);
// The parent must prove (raw_input[i] - offset >= 0) at the call site, or the
// compilation fails with an unresolved REQUIRE obligation.

Sub-instance INVARIANT clauses are also discharged in the parent's proof context, once per (unrolled) element. An invariant that holds in the sub-instance in isolation holds in the parent by induction, because the inlined model is the same model.

10.7 Template Instantiation

When the type name in a VAR declaration carries angle-bracket arguments (Vec<3>, MatVec<2,3>), the compiler resolves the base name (Vec, MatVec) via the normal file resolver, then monomorphizes the template FB with the supplied arguments (see §4.10). The resulting concrete FB — named Vec<3> in the closure snapshot — is compiled and inlined exactly like any ordinary sub-instance.

A parent that hosts two instantiations of the same template at different sizes gets two independent concrete types, each with its own proof context:

FUNCTION_BLOCK TwoVecs
VAR_INPUT
    p3 : ARRAY[0..2] OF LREAL;  q3 : ARRAY[0..2] OF LREAL;
    p4 : ARRAY[0..3] OF LREAL;  q4 : ARRAY[0..3] OF LREAL;
END_VAR
VAR_OUTPUT
    d3 : LREAL;
    d4 : LREAL;
END_VAR
VAR
    v3 : Vec<3>;
    v4 : Vec<4>;
END_VAR
WIRING
    v3(a := p3, b := q3);
    v4(a := p4, b := q4);
    d3 := v3.dot;
    d4 := v4.dot;
END_WIRING
END_FUNCTION_BLOCK

Wiring template instances. Use the same WIRING syntax as ordinary instances (§10.2a): inst(port := expr, ...) for inputs; out := inst.port for output forwarding. Dot notation inst.port := expr is not accepted.

Closure snapshot. Template FBs are monomorphized once per distinct argument tuple during materialize_closure. The same Vec<3> used by two different parents is resolved and monomorphized only once; the snapshot is reused.

---

11. Timers and Temporal Constructs

11.1 HELD

Syntax

HELD ( <bool-expr>, <pt-expr> )

Semantics

Evaluates to TRUE if bool-expr has held continuously TRUE for at least pt time. pt-expr is a TIME literal or TIME variable (TIME variables are experimental — rejected by PILOT).

In the Z3 model, timers use an absolute monotone-time model; HELD is proved for all possible clock sequences consistent with the profile's dt_max_ms bound.

HELD is emitted as a native TON timer in the ST backend and as a monotonic started_at clock in the Rust backend.

HELD conditions MUST NOT reference derived values (§14.5, §15.2).

Example

active:
    ON  WHEN HELD(sensor, T#2s) PRIO 1;
    OFF OTHERWISE;

11.2 ELAPSED

Syntax

ELAPSED ( <bool-expr>, <pt-expr> )

Evaluates to the accumulated time (as TIME) that bool-expr has been continuously TRUE, clamped at pt. Returns T#0ms when the condition is FALSE. Experimental.

11.3 TIME Variables and Presets

TIME may be declared as a VAR_INPUT or VAR (experimental — rejected by PILOT). A TIME variable may be used as a timer preset (pt). PILOT requires literal presets.

---

12. EXTERN Semantics

12.1 EXTERN FUNCTION Declaration

EXTERN FUNCTION <name> ( [ params ] ) -> <type>
    ENSURE <bool-expr> ;
    { ENSURE <bool-expr> ; }
    [ BY <artifact-id> ; ]

An EXTERN FUNCTION declares a contract without a body. The compiler does not prove the ENSURE clauses; instead it:

1. Adds them as unconditional assumptions in the Z3 model (ASSUME-like premises).
2. Resolves a registered artifact that discharges the contract.

At least one ENSURE is required. BY pins a specific artifact key in the Verified Library (lola/verified/manifest.json). If BY is absent, the resolver auto-selects the best matching artifact at backend-emit time.

The return value is referred to by the function name inside ENSURE expressions:

EXTERN FUNCTION sat_add(a : INT, b : INT) -> INT
    ENSURE sat_add >= a;
    ENSURE sat_add >= b;
    BY sat_add_i16;

12.2 Model Treatment

The Z3 model assumes all ENSURE clauses hold whenever the EXTERN function is called with any arguments. This makes the proof of INVARIANTs that depend on the EXTERN result valid only if the artifact genuinely satisfies the ENSURE clauses. The artifact registration and warrant are what connect the model-level assumption to physical evidence.

12.3 BY (Artifact Binding)

BY <artifact-id> pins the artifact key in manifest.json. The key MUST exist in the registry. The artifact MUST have:

• A lola_contract entry whose ENSURE content is entailed by the declared ENSURE clauses.
• At least one target entry with a non-empty clauses mapping.

If BY is absent, auto-resolve selects the artifact by entailment match.

12.4 Manifest and Warrant Levels

The Verified Library manifest at lola/verified/manifest.json stores:

"<artifact-id>": {
  "signature": { "params": [...], "returns": "..." },
  "lola_contract": "ENSURE (<canonical-form>)",
  "targets": {
    "<backend>": {
      "file": "<artifact>.rs",
      "call": "<fn-name>",
      "sha256": "<hex>",
      "clauses": {
        "<clause-id>": {
          "status": "proved | audited",
          "witness": "..."
        }
      }
    }
  }
}

Warrant levels. An artifact clause carries a status:

Status	Meaning
proved	Discharged by a mechanical proof or exhaustive test
audited	Reviewed under stated conditions; provenance recorded

PILOT requires proved for all EXTERN artifacts. DEFAULT accepts audited.

The lola_contract field uses canonical parameter names arg0, arg1, RESULT (not the LoLa source parameter names). The entailment solver checks whether the declared ENSURE clauses imply the manifest's lola_contract.

12.5 lola extern Toolchain

The lola extern sub-command manages the Verified Library:

Command	Effect
lola extern check	Validate registry structure and hash integrity
lola extern verify <id> --target rust\|st	Run verification recipe (no writes)
lola extern register <id> --target rust\|st [--audit REASON]	Seal warrant into manifest
lola extern init <contract> --target rust\|st [--by ID] [--ensures CLAUSE]	Scaffold new artifact

See the CLI Reference for full option documentation.

---

13. MATHREAL Semantics

13.1 MATHREAL = ℝ (Mathematical Model)

In the LoLa semantic model, MATHREAL and LREAL values are mathematical real numbers (elements of ℝ). Z3's RealSort implements exact rational arithmetic; literals are stored as exact Fraction values. There is no rounding, no overflow, and no infinity at the language level.

This means: - 1.0 / 3.0 * 3.0 = 1.0 is provable (exact arithmetic). - 2.0 ** 10 = 1024.0 requires a proof about the body if written as x * x * ... * x; LoLa has no exponentiation operator. - Mathematical invariants (INVARIANT output >= 0.0) are proved exactly.

Practical implication: If a program uses MATHREAL or LREAL and is compiled without a Representation Boundary, the backends raise a TypeError. The mathematical proof is valid, but no machine code can be emitted. A Representation Boundary must be declared (§13.3) to emit target code.

13.2 LREAL vs MATHREAL

Both MATHREAL and LREAL denote ℝ in the semantic model — they are distinguished only at the Representation Boundary:

• MATHREAL → at least Float32 precision (implementation-dependent).
• LREAL → at least Float64 precision.

In the current compiler, both are lowered to Float64 (IEEE 754 binary64) when FLOAT64_REPR is selected. This is expected to diverge when a Float32 policy is added.

13.3 Representation Boundary

A Representation Boundary separates the mathematical LoLa program semantics from the machine representation chosen for deployment. It is declared in one of two ways:

(a) CLI flag: --profile float64 selects the global Float64 policy.

(b) Project TOML: [representation] section in the project file:

[representation]
policy = "float64"

Without a Representation Boundary, backend emit is rejected for any MATHREAL/LREAL program. This is the correct default: a mathematical proof holds regardless of machine precision, but emitting code requires knowing the precision.

13.4 Float64 Representation and Overflow Gate

When FLOAT64_REPR is selected:

• All MATHREAL and LREAL signals are lowered to f64 (Rust) / LREAL (ST).
• A roundoff obligation is generated: the IEEE 754 representation error |float64(literal) − literal| is bounded for each literal in the program. This is a Gappa-discharged roundoff proof obligation (experimental).
• MATHREAL arithmetic in the backend is IEEE 754 binary64 with round-to-nearest; the model assumes mathematical reals. The gap between model and implementation is a separate assurance concern addressed by the Engineering Error Report (§13.6).

Overflow gate. The compiler runs an overflow gate (lola/overflow.py) on every compilation:

Condition	Result
Program has no MATHREAL/LREAL	Gate passes; overflow is not applicable (integers wrap modulo 2ⁿ, never trap)
Program has MATHREAL/LREAL, no Representation Boundary	Compile error: OverflowError — a mathematical-MATHREAL program cannot be lowered without a declared policy
Program has MATHREAL/LREAL, FLOAT64_REPR selected	Gate passes with verdict "not applicable"; IEEE 754 overflow (±∞) is possible at runtime and is NOT a Z3 error — finite/no-Inf analysis is deferred to the Gappa warrant chain

The gate is fail-closed: the absence of a Representation Boundary is treated as a policy violation, not a safe default. This prevents silent lowering of mathematical-MATHREAL programs to machine types without an explicit assurance commitment.

13.5 CONTINUOUS_REFERENCE

CONTINUOUS_REFERENCE
    DER(<state-var>) = <real-expr> ;
    ...
END_CONTINUOUS_REFERENCE

An optional block in a FUNCTION_BLOCK that declares the ordinary differential equation governing a state variable's continuous-time evolution. It is used by the numerical assurance chain to derive discretization bounds and engineering error reports. It does NOT change the programme's discrete semantics. The DER(...) annotation is consumed by lola ... --project <toml> --target check and does not affect ST/Rust codegen.

CONTINUOUS_REFERENCE is experimental (DEFAULT profile, numerical assurance chain).

13.6 Engineering Error Report

When a project file (§13.3b) activates the numerical assurance chain, lola --project <toml> --target check prints an Engineering Error Report for each state variable that has a CONTINUOUS_REFERENCE and complete warrant coverage.

Printed to stdout:

── Engineering Error Report (s) ─────────────────────────────
Semantics
  LoLa discrete transition    : 0.98 * s + 0.02 * u
  Continuous ODE              : -2*s + 2*u
  Representation              : float64

Timing
  Sample period T_s   : 0.010000 s
  Jitter bound J      : 0.001000 s
  h ∈ [0.009000, 0.011000] s

Per-step error budget
  Machine roundoff ε_m        :  1.23e-15  [proved]
  Physical input error ε_p    :  1.00e-02  [proved-under-assumptions]
  Discretisation error ε_d    :  4.56e-04  [proved-under-assumptions]
  Jitter error ε_j            :  7.89e-05  [proved-under-assumptions]
  ──────────────────────────────────────────────────────────
  Effective per-step error    :  1.07e-02  [proved-under-assumptions]

Trajectory bound
  Machine Lipschitz           :  0.98
  Timing Lipschitz            :  1.00
  Effective Lipschitz         :  0.98  [contractive]
  Asymptotic bound            :  5.35e-01

Assumptions (must hold at deployment)
  SamplingWarrant             : T_s = 1/100 s declared
  JitterBound                 : J = 1/1000 s declared
  PhysicalInputBound          : |u_phys − u_ideal| ≤ 1/100

Proved
  LipschitzBound              : 0.98  [proved]
  StepErrorBudget             : ...   [proved]
  ...

overall_status: proved-under-assumptions

Budget decomposition. The per-step effective error is the triangle sum of four orthogonal components, each sourced from a sealed warrant in the assurance chain:

Component	Source warrant	Meaning
machine_roundoff ε_m	Gappa roundoff proof	IEEE 754 rounding per step
physical_input_error ε_p	Physical input bound (declared)	Declared sensor/actuator error
discretization_error ε_d	ODE discretisation step bound	ODE discretisation via Taylor remainder
jitter_error ε_j	Jitter step error (declared)	Extra error from timing jitter

Trajectory section. The Lipschitz-based trajectory bound describes how errors accumulate over multiple cycles. A contractive system (effective Lipschitz < 1) has a finite asymptotic bound; an expansive system (> 1) shows a horizon and bound at that horizon.

Status semantics. overall_status: proved-under-assumptions means every warrant in the chain is either proved (formally discharged) or proved-under- assumptions (proved given the declared bounds). No warrant is merely asserted. A zero physical-input error is still recorded as an assumption (§13.6 is fail-closed on this point).

JSON export. The same data is available as a structured dict via lola.engineering_formatter.report_to_dict(report). All numeric values are encoded as {"n": numerator, "d": denominator} exact fractions.

When the report is absent. The report is only produced when the full warrant chain is present. If any required warrant (sampling, Lipschitz, step budget, trajectory, jitter) is missing, the compiler raises ValueError rather than printing a report with silent zero-fills.

---

14. Static Semantics

Case-insensitive identifiers. Identifiers are matched case-insensitively. Motor and MOTOR collide; a collision between two declarations is a compile error.

Definition completeness. Each VAR_OUTPUT and VAR MUST be defined exactly once (either a rule block or a derived assignment). Both at once, or neither, is an error.

Type checking. All binary operators require identical operand types (no implicit promotion). All ENSURE/INVARIANT/ASSUME expressions MUST be BOOL.

ASSUME and REQUIRE scope. Both MUST reference inputs only. DT is excluded from both.

HELD condition scope. HELD conditions MUST NOT reference derived values. The timer condition is evaluated at the start of a cycle; derived values are computed during the cycle.

---

15. Dynamic/Synchronous Semantics

15.1 Cycle Model

A LoLa function block implements one step of a state-transition system:

next_state = step(current_inputs, current_state)

One cycle processes one complete application of step. The scan cycle (PLC execution model) repeats this indefinitely.

The formal model:

• State space. A tuple of values for every VAR_OUTPUT and VAR.
• Input space. A tuple of values for every VAR_INPUT.
• Transition function. Determined by the rule blocks and derived assignments.
• Initial state. All outputs and locals at their type's initial value (§5).

15.2 Start-of-Cycle Reads

All identifier references inside an expression — whether in a rule guard, a rule value, or a derived assignment — denote the value at the beginning of the current cycle. There is no sequencing of writes within a cycle.

A consequence: if output A depends on output B and output B depends on A (a combinatorial cycle), this is a semantic non-issue for registers (they read their pre-state), but would be a circular dependency for derived assignments. The compiler detects and rejects combinatorial cycles in derived definitions.

15.3 Atomic Commit

After all rule and derived expressions are evaluated using start-of-cycle values, all outputs are updated simultaneously. The new values are visible only in the next cycle.

15.4 Priority Resolution

When multiple rules for the same output have their guards evaluate to TRUE:

1. The rule with the highest numerical PRIO value wins.
2. If two rules have equal PRIO and fire simultaneously with different effects, the program is ambiguous — the compiler rejects it with a counterexample.

Rules with equal PRIO that always agree on the effect (same action, same value for SET) are not ambiguous and are accepted.

An OTHERWISE guard (always-true) fires at priority 0 unless overridden by a higher-priority WHEN rule.

15.5 Ambiguity Detection

Ambiguity is detected by the Z3 model: the compiler asserts that two equal-priority conflicting rules cannot simultaneously fire. If satisfiable, compilation fails with a counterexample giving the input values and pre-state that trigger the conflict.

This is the fundamental difference from IEC 61131-3 Structured Text, where priority is resolved by textual order silently.

---

16. Proof Obligations

16.1 Initial State

Every INVARIANT is checked against the initial state:

• All VAR_OUTPUT and VAR at their type's initial value.
• VAR_INPUT unconstrained (or constrained by ASSUME).

Important: Derived outputs (:=) are not evaluated before the initial-state check — they are combinatorial functions of the current state. An INVARIANT comparing a derived output to an input can fail in the initial state if the input can be nonzero when all registers default to 0.

Diagnostic: invariant-init.

16.2 Inductive Step

Every INVARIANT is also checked under the assumption that it held at the end of the previous cycle. The compiler must prove that for all valid inputs and all pre-states satisfying INVARIANT, the post-state also satisfies INVARIANT.

ASSUME and REQUIRE are premises in the step check. REQUIRE is NOT a premise in the initial-state check (initial state has no "caller").

Diagnostic: invariant-step.

16.3 Counterexample Reporting

When an obligation fails, the compiler prints a model assignment that witnesses the failure:

verification failed:
  [invariant-step] invariant can be violated after one cycle: NOT (A AND B)
      counterexample: A=0, B=0, StartA=1, StartB=1

The counterexample names all inputs and pre-cycle outputs that exhibit the failure.

---

17. Profiles and Implementation-Defined Features

17.1 DEFAULT Profile

The DEFAULT profile is the baseline for development. All language features are available. Some features are experimental: they are accepted and processed, but no coverage guarantee exists for ST and Rust backends. Experimental features may behave correctly in many cases but have not been validated against real toolchains.

Experimental in DEFAULT:

• WSTRING values and LEN
• Arithmetic on bit-string types (+, -, *, /, MOD on BYTE/WORD/DWORD/LWORD)
• TIME-typed inputs and outputs
• Variable timer presets (TIME variable as pt)
• MATHREAL/LREAL backend emit (requires explicit FLOAT64_REPR or [representation])

17.2 PILOT Profile

The PILOT profile selects the verified core. It rejects programs that rely on any experimental feature and enforces additional assurance gates:

Gate	PILOT requirement
Backend coverage	Both st and rust targets required
WSTRING	Rejected
Bitstring arithmetic	Rejected
TIME outputs/inputs	Rejected
Variable timer presets	Rejected
MATHREAL overflow	Hard error (must prove overflow-safe)
EXTERN warrants	proved required; fresh execution at compile time
Contract assurance	Required (EXTERN programs must carry assurance receipts)

G1 (closed for the PILOT core at commit a8e686b) assurance does not extend beyond programs that pass PILOT validation.

17.3 FLOAT64_REPR Profile

The FLOAT64_REPR profile enables MATHREAL/LREAL backend emit by declaring the global Float64 Representation Boundary (§13.3). It does not impose any PILOT restrictions.

Activated via --profile float64 or [representation] policy = "float64" in a project TOML.

17.4 Custom Profiles

A project TOML may compose individual profile gates (see the Project Configuration Reference). A profile derived by changing only some PILOT gates is labeled custom(<name>), not pilot, to avoid implicit claims of G1-level assurance.

17.5 Unsupported Features (Fail-Closed)

The compiler rejects programmes that use:

• Array element types other than primitive scalars (no ARRAY OF ARRAY, no ARRAY OF WSTRING).
• WSTRING in an ARRAY declaration.
• Bitstring arithmetic in PILOT.
• TIME outputs in PILOT.
• MATHREAL/LREAL without a Representation Boundary at backends.
• EXTERN FUNCTION without at least one ENSURE.
• Bare untyped integer literals outside DINT range.

Rejection is always with a diagnostic; silent truncation or undefined behaviour do not occur.

---

18. Grammar Appendix

The grammar below is derived from lola/parser.py and uses a relaxed BNF notation. { x } = zero or more x; [ x ] = optional x; x | y = alternative. Terminals are in ALL_CAPS or quoted.

program          ::= function_block { function_block }

function_block   ::= FUNCTION_BLOCK IDENT [ type_param_header ]
                       { var_block }
                       [ implementation ]
                     END_FUNCTION_BLOCK

type_param_header ::= "<" type_param { "," type_param } ">"
type_param        ::= IDENT ":" UINT

var_block        ::= var_input | var_output | var_local
var_input        ::= VAR_INPUT { var_decl } END_VAR
var_output       ::= VAR_OUTPUT { var_decl } END_VAR
var_local        ::= VAR { var_decl } END_VAR

var_decl         ::= IDENT ":" type_spec ";"
type_spec        ::= BOOL | SINT | INT | DINT | LINT
                   | USINT | UINT | UDINT | ULINT
                   | BYTE | WORD | DWORD | LWORD
                   | MATHREAL | LREAL
                   | TIME
                   | WSTRING [ "[" INT_LIT "]" ]
                   | ARRAY "[" expr ".." expr "]" OF scalar_type
                   | ARRAY "[" expr ".." expr "]" OF IDENT  (* Array OF FB *)
                   | IDENT [ "<" UINT_LIT { "," UINT_LIT } ">" ]  (* FB instance or template instance *)

implementation   ::= IMPLEMENTATION { impl_stmt } END_IMPLEMENTATION
impl_stmt        ::= register_rule
                   | derived_assign
                   | instance_wire
                   | array_wire
                   | invariant
                   | continuous_reference
                   | function_def

register_rule    ::= IDENT "{"
                       { guard_rule }
                       [ OTHERWISE ":"  { action } ]
                     "}"
guard_rule       ::= WHEN expr ":" { action } [ PRIO int_lit ]
action           ::= SET IDENT [ "=" expr ] ";"
                   | ON  IDENT [ "=" expr ] ";"
                   | OFF IDENT [ "=" expr ] ";"
                   | HOLD IDENT ";"

derived_assign   ::= IDENT ":=" expr ";"

instance_wire    ::= IDENT "(" { wire_arg "," } wire_arg ")" ";"
wire_arg         ::= IDENT ":=" expr
array_wire       ::= IDENT "[" "i" "]" "(" { wire_arg "," } wire_arg ")" ";"

invariant        ::= INVARIANT expr ";"
assume           ::= ASSUME expr ";"
require          ::= REQUIRE expr ";"
ensure           ::= ENSURE expr ";"
                   | ENSURE PERMUTATION_OF "(" IDENT ")" ";"
variant          ::= VARIANT expr ";"
rule             ::= RULE IDENT GENERATES IDENT ";"

continuous_reference ::= CONTINUOUS_REFERENCE
                            { DER "(" IDENT ")" "=" expr ";" }
                          END_CONTINUOUS_REFERENCE

function_def     ::= FUNCTION IDENT
                       "(" { param "," } param ")"
                       ":" return_type
                       { require }
                       { ensure }
                       [ variant ]
                       ":=" expr
                     END_FUNCTION
param            ::= IDENT ":" type_spec
return_type      ::= type_spec

expr             ::= bool_expr
bool_expr        ::= bool_term { ( AND | OR | XOR ) bool_term }
                   | NOT bool_term
bool_term        ::= comparison
comparison       ::= sum [ ( "=" | "<>" | "<" | "<=" | ">" | ">=" ) sum ]
sum              ::= product { ( "+" | "-" ) product }
product          ::= unary { ( "*" | "/" | "MOD" ) unary }
unary            ::= [ "-" ] primary
primary          ::= literal
                   | IDENT
                   | IDENT "." IDENT                 (* member access *)
                   | IDENT "[" expr "]"              (* array index *)
                   | IDENT "[" expr "]" "." IDENT    (* array-FB member *)
                   | IDENT "." IDENT "[" expr "]"    (* member array index *)
                   | IDENT "(" { expr "," } expr ")" (* function call *)
                   | IF expr THEN expr ELSE expr
                   | HELD "(" expr "," expr ")"
                   | ELAPSED "(" expr "," expr ")"
                   | LEN "(" expr ")"
                   | DT
                   | CLAMP "(" expr "," expr "," expr ")"
                   | SORT "(" IDENT ")"
                   | SORTED "(" IDENT ")"
                   | PERMUTATION_OF "(" IDENT "," IDENT ")"
                   | ARRAY "(" IDENT IN int_lit ".." int_lit ":" expr ")"
                   | aggregate "(" IDENT IN int_lit ".." int_lit ":" expr ")"
                   | "(" expr ")"
aggregate        ::= SUM | COUNT | ALL | ANY | EXISTS | MIN | MAX

literal          ::= BOOL_LIT | INT_LIT | REAL_LIT | TIME_LIT | WSTRING_LIT

EXTERN_block     ::= EXTERN FUNCTION IDENT "(" { ext_param "," } ext_param ")"
                     ":" ext_type
                     { ASSUME expr ";" }
                     { ENSURE expr ";" }
                     [ BY STRING_LIT ]
                     END_FUNCTION

EXTERN_REAL_CONTRACT ::= EXTERN_REAL_CONTRACT IDENT
                           [ VAR_INPUT  { var_decl } END_VAR ]
                           [ VAR_OUTPUT { var_decl } END_VAR ]
                           [ VAR_STATE  { var_decl } END_VAR ]
                           SEMANTICS { ASSUME expr ";" | ENSURE expr ";" } END_SEMANTICS
                         END_EXTERN_REAL_CONTRACT

This grammar is a faithful summary; the canonical source is lola/parser.py. Where discrepancies exist, the parser is authoritative.

---

19. Reserved Words

All of the following identifiers are reserved by the lexer and cannot be used as user-defined names:

Block structure: FUNCTION_BLOCK, END_FUNCTION_BLOCK, FUNCTION, END_FUNCTION, EXTERN, BY, VAR_INPUT, VAR_OUTPUT, VAR, VAR_STATE, END_VAR, IMPLEMENTATION, END_IMPLEMENTATION, CONTINUOUS_REFERENCE, END_CONTINUOUS_REFERENCE, EXTERN_REAL_CONTRACT, END_EXTERN_REAL_CONTRACT, SEMANTICS, END_SEMANTICS

Contracts: INVARIANT, ASSUME, RULE, REQUIRE, ENSURE, VARIANT

Types: BOOL, SINT, INT, DINT, LINT, USINT, UINT, UDINT, ULINT, TIME, MATHREAL, LREAL, BYTE, WORD, DWORD, LWORD, WSTRING

Named constants: SINT_MIN, SINT_MAX, INT_MIN, INT_MAX, DINT_MIN, DINT_MAX, LINT_MIN, LINT_MAX, USINT_MIN, USINT_MAX, UINT_MIN, UINT_MAX, UDINT_MIN, UDINT_MAX, ULINT_MIN, ULINT_MAX

Conversion builtins: SINT_TO_INT, INT_TO_SINT, INT_TO_DINT, DINT_TO_INT, INT_TO_LINT, LINT_TO_INT, DINT_TO_LINT, LINT_TO_DINT, SINT_TO_USINT, USINT_TO_SINT, INT_TO_UINT, UINT_TO_INT, DINT_TO_UDINT, UDINT_TO_DINT, LINT_TO_ULINT, ULINT_TO_LINT, USINT_TO_UINT, UINT_TO_USINT, UINT_TO_UDINT, UDINT_TO_UINT, UDINT_TO_ULINT, ULINT_TO_UDINT

State transition (FUNCTION_BLOCK output rules): ON, OFF, HOLD, SET, WHEN, OTHERWISE, PRIO

SSFC: SSFC, END_SSFC, STATE, END_STATE, SUPERSTATE, END_SUPERSTATE, INITIAL, TERMINAL, TRANSITION, TO, PARALLEL, END_PARALLEL, REGION, END_REGION, JOIN, FROM, EN, DU, EX

Expressions: AND, OR, XOR, NOT, TRUE, FALSE, LEN, HELD, ELAPSED, CLAMP, DT, IF, THEN, ELSE

Note: MOD, ARRAY, OF, SORT, IN, SUM, COUNT, ALL, ANY, EXISTS, MIN, MAX, and DER are matched by identifier text comparison in specific contexts; they are NOT reserved words and may be used as variable names outside those contexts.

---

20. Cross-Reference Index

Stub — to be generated from section anchors after prose is complete.

---

21. SSFC — Super Sequential Function Charts

An SSFC (Super Sequential Function Chart) declares a FUNCTION_BLOCK type whose behavior is expressed as a state machine. It is not a separate POU kind: SSFC Foo ... END_SSFC is the canonical compact form for a stateful, instantiable component whose logic is organised into named states, transitions, and lifecycle blocks, rather than into declarative rules. The resulting type Foo can be instantiated, wired, and composed wherever a FUNCTION_BLOCK type is valid.

The SSFC lowers to the same LoLa State/IR that FUNCTION_BLOCK uses; there is no separate runtime. The full synchronous semantics (scan model, pre-state semantics, register-backing) is identical to §15; SSFC extends it with a named-state hierarchy, lifecycle blocks, and structural assurance.

For motivation, worked examples, and conceptual background see: - Tutorial: Introduction by Example §21 - How-to: Model a Sequential Machine - Concepts: SSFC Semantics

---

21.1 Program Structure

(a) SSFC-only file:

ssfc-definition

A .lola file containing a single SSFC / END_SSFC block and no FUNCTION_BLOCK.

(b) Combined file:

{ function-definition | extern-function-definition }
ssfc-definition

Functions defined in the file are available for call within lifecycle block expressions.

Syntax

SSFC <name>
  [ PARAMETER <param-decls> END_PARAMETER ]
  [ VAR_INPUT  <var-decls>  END_VAR ]
  [ VAR_OUTPUT <var-decls>  END_VAR ]
  [ VAR        <var-decls>  END_VAR ]
  [ WIRING { instance-call } END_WIRING ]
  { state-decl | superstate-decl }
END_SSFC

VAR_INPUT, VAR_OUTPUT, and VAR are identical in meaning to §4. PARAMETER is identical to §4.9. Every VAR_OUTPUT and VAR name that appears in any lifecycle block is register-backed (see §21.6).

VAR may declare sub-instances of other FUNCTION_BLOCK or SSFC types (component composition — see §21.14). The optional WIRING block wires those sub-instances' inputs.

Exactly one state or superstate at the root level MUST carry the INITIAL keyword. At least one state MUST be declared.

---

21.2 States

[ INITIAL ] [ TERMINAL ] STATE <name>
  [ EN: <lifecycle-body> ]
  [ DU: <lifecycle-body> ]
  [ EX: <lifecycle-body> ]
  { TRANSITION TO <target> WHEN <guard> [ PRIO <n> ] ; }
END_STATE

• INITIAL: exactly one state per exclusive region MUST be marked INITIAL. It is the active state when the region is first entered.
• TERMINAL: the state is a valid final state. A TERMINAL state with no outgoing transitions suppresses the C-DEAD structural deadlock warning. A TERMINAL state WITH outgoing transitions is valid; those transitions may still fire.
• Lifecycle bodies are described in §21.5.
• TRANSITION declarations are described in §21.7.

A state with no lifecycle blocks and no transitions is legal (empty state); it acts as a stable resting point.

---

21.3 Superstates

[ INITIAL ] SUPERSTATE <name>
  [ EN: <lifecycle-body> ]
  [ DU: <lifecycle-body> ]
  [ EX: <lifecycle-body> ]
  { state-decl | superstate-decl | parallel-block }
  { TRANSITION TO <target> WHEN <guard> [ PRIO <n> ] ; }
END_SUPERSTATE

A superstate contains an exclusive child region (when there is no PARALLEL block) or a parallel block (see §21.4).

• The INITIAL keyword marks this superstate as the initial state of its parent exclusive region.
• Lifecycle blocks of a superstate execute when any child of the superstate is active: EN fires when the superstate is entered (including via a child's explicit entry), DU fires every scan while any child is active, EX fires when the superstate is left.
• Parent-level transitions (TRANSITION TO <target> WHEN <guard>) declared directly inside a superstate are preemption transitions. They fire from any active child of the superstate. They always have implicit higher priority than any child-level transition in the same scan (§21.7.2).
• Superstates may be nested to any depth.

---

21.4 Parallel Regions

A superstate may contain a PARALLEL block instead of a flat list of child states:

SUPERSTATE <name>
  PARALLEL
    { REGION <region-name>
        { state-decl | superstate-decl }
      END_REGION }
    { JOIN FROM <src1>, <src2> [, …] TO <target> [ WHEN <guard> ] ; }
  END_PARALLEL
  { TRANSITION TO <target> WHEN <guard> [ PRIO <n> ] ; }
END_SUPERSTATE

Regions

• Each REGION / END_REGION contains an independent exclusive sub-machine with its own INITIAL state, states, and transitions.
• A region MUST contain exactly one INITIAL state.
• All regions are active simultaneously when the enclosing parallel superstate is active (AND semantics).
• Transitions within a region fire independently; a transition in region A has no effect on region B's marking in the same scan.

Fork (entering the parallel superstate)

Entering the parallel superstate activates the INITIAL state of all regions simultaneously in the same scan. The entry scan runs EN of all initial states (outermost first within each region, regions processed left-to-right in declaration order).

Join

JOIN FROM <src1>, <src2> [, …] TO <target> [ WHEN <guard> ] ;

• A JOIN fires in the scan when all named source states are simultaneously active and the optional WHEN guard evaluates to TRUE.
• Source states MUST be in distinct regions of the same parallel superstate.
• There MUST be at least two sources.
• The target state MUST exist in the enclosing SSFC hierarchy (at any level except inside a source region).
• When a JOIN fires, all source regions exit atomically: EX blocks of all active region leaves fire (in deepest-first, reversed-region-declaration order), the parallel superstate exits, and the target state is entered.
• A JOIN with an always-FALSE guard is flagged by C-DATA-DEAD.

Preemption of parallel superstates

TRANSITION TO <target> WHEN <guard> declared at the parallel superstate level preempts all active regions simultaneously. The exit sequence exits all active region leaves (deepest-first, reversed-region order), then the parallel superstate, then enters the target.

Write-conflict rule

Two or more simultaneously active lifecycle blocks in different regions MUST NOT write the same output variable. The compiler rejects violations as ssfc-cross-region-conflict. Writes in a superstate's own lifecycle blocks (above the PARALLEL block) are not in conflict with region writes, but they share the same register so ordering within the scan is deterministic.

---

21.5 Lifecycle Blocks

lifecycle-body ::=
  { <name> := <expr> ;
  | <name> : <output-rule-list> }

Lifecycle bodies use the same expression language and statement forms as FUNCTION_BLOCK implementation bodies: derived assignments (:=) and output rules (: rule lists, §7) with the complete LoLa expression language inside (arithmetic, boolean logic, PRE(), EXTERN function calls, user-defined functions, IF-THEN-ELSE, array expressions, and state-field reads S.X / S.T_elapsed).

Verification annotations (INVARIANT, ASSUME, REQUIRE) are structural declarations and do not appear in lifecycle bodies. Sub-instance wiring (inst(Input := expr)) is a structural concern; sub-components are declared in the SSFC's VAR block and their outputs are read through variables.

EN — Entry block

Executes exactly once: in the scan the state is entered (the entry scan), after the marking update (step 5) and T_elapsed reset (step 6), before DU (step 8). Order within a transition: outermost-first (the parent superstate's EN executes before the child state's EN).

DU — During block

Executes every scan in which the state is active after the marking update, including the entry scan (after EN). Order: outermost-first.

For states NOT entered in this scan (stable states): DU sees the values written by earlier DU blocks of outer states in this scan.

For states entered in this scan: DU sees values written by their own EN block.

EX — Exit block

Executes exactly once: in the scan the state is left (the exit scan), before the marking update (step 5). Order: deepest-first (the leaf state's EX executes before the parent superstate's EX).

Reading time inside lifecycle blocks

Expression	What it reads
PRE(x)	The pre-state snapshot value (step 1 of this scan). Stable across all lifecycle blocks in this scan.
Direct x	The current value: after earlier lifecycle blocks have written. EX blocks see pre-state via PRE; DU of an outer state sees EN writes of the same state; see §21.8 for the full order.
State.T_elapsed	The time this state has been active. 0s in the entry scan. Only valid for active states.
State.X	TRUE iff the state is currently active. Reflects the marking after step 5 in the same scan.

---

21.6 Register-Backing of SSFC Variables

All VAR_OUTPUT and VAR variables that appear on the left-hand side of any lifecycle block assignment are register-backed. This is identical to the FUNCTION_BLOCK register-backing rule (§3.2).

• A register-backed variable retains its value across scans until overwritten.
• Its PRE(x) value is the snapshot from step 1 of the current scan.
• Its initial value is declared in the VAR initializer (or the type zero value).

Consequence for EN-only outputs: If state S sets valve := TRUE in EN and has no DU block for valve, valve holds TRUE across all subsequent scans until another lifecycle block (EX of S, or EN/DU of another state) writes a different value. This is correct and intentional: EN-set values persist until explicitly changed.

---

21.7 Transitions

Syntax

TRANSITION TO <target> WHEN <guard-expr> [ PRIO <n> ] ;

• target: the name of any state or superstate in the SSFC. For transitions inside a region, the target MUST be within the same region (intra-region) or a state at the parent superstate level or higher (cross-boundary exit).
• guard-expr: a pure Boolean expression. Evaluated at step 2 of the scan against the pre-state snapshot. MUST be side-effect-free. MAY reference VAR_INPUT, PARAMETER values, PRE(x) for any register-backed x, and State.T_elapsed for any active state.
• PRIO n: explicit integer priority. Higher value wins. MUST be declared when two guards of the same state can be simultaneously TRUE. If omitted and two guards are simultaneously TRUE, the compiler issues ssfc-ambiguous-priority (a static error in strict mode).

21.7.1 Guard evaluation timing

All guards are evaluated at step 2 against the pre-state snapshot (step 1). No lifecycle block has executed at the time of guard evaluation. Guards see the same values as PRE(x) calls within lifecycle blocks.

21.7.2 Priority rules

1. Parent-level preemption has highest implicit priority. If a preemption guard (declared at superstate level) and a child guard are both TRUE in the same scan, the preemption transition is selected. No explicit PRIO is needed to express this; the structural priority is part of the semantics.
2. Among transitions of the same state, the highest-PRIO transition whose guard is TRUE is selected. Guards with equal PRIO that are simultaneously satisfiable are an ssfc-ambiguous-priority error unless they are provably disjoint (checked by C-DET).
3. At most one transition fires per scan. If no guard is TRUE, no transition fires and the marking is unchanged (only DU executes in step 8).

21.7.3 LCA-based exit/entry sequence

For a selected transition from active state S to target T:

1. Compute LCA(S, T) — the deepest node common to both paths from S and T to the SSFC root.
2. EX fires for: S, parent(S), …, up to but not including LCA. Order: S first (deepest), ancestors last (outermost).
3. EN fires for: LCA, …, down to T but not including T's own parent (that already fired its EN when the LCA was entered on a prior transition). Wait — more precisely: EN fires for every node between LCA and T that is being entered fresh, outermost first.
4. DU fires for all states active after the marking update (step 5), including the newly entered T and any states in the stable part of the hierarchy.

If the LCA is the SSFC root (transition between two branches of the top-level region), the full EX chain up to the root fires, and the full EN chain down to T fires.

---

21.8 Scan Execution Order (Normative)

The nine steps for one SSFC scan, in order:

Step	Action
1	Pre-State Snapshot. Capture all register-backed values (incl. State.X, State.T_elapsed). PRE(x) reads from this snapshot for the rest of the scan.
2	Guard Evaluation. Evaluate all WHEN guards of all active states and superstates against the step-1 snapshot.
3	Transition Selection. Select at most one transition (priority rules of §21.7.2). If none, skip to step 8.
4	EX Phase. Execute EX blocks of all departing states, deepest-first. For parallel superstates: EX of all active region leaves (reversed-region / deepest-first), then EX of the parallel superstate.
5	Marking Update. Set State.X according to the new marking.
6	T_elapsed Reset. Set T_elapsed := 0 for all newly entered states.
7	EN Phase. Execute EN blocks of all newly entered states, outermost-first.
8	DU Phase. Execute DU blocks of ALL currently active states (including newly entered), outermost-first.
9	Commit. Post-state becomes observable; it is the pre-state of the next scan.

If no transition fires in step 3: skip steps 4–7. Execute only DU (step 8) then Commit (step 9).

---

21.9 Implicit Fields

Every state S exposes two read-only fields:

S.X : BOOL

TRUE iff state S is active in the current scan (after step 5). May be read inside lifecycle blocks of any state in the same SSFC, in TRANSITION guards, and in expressions of a co-located FUNCTION_BLOCK. Writing S.X is a static error.

S.T_elapsed : TIME

The elapsed time since S was most recently entered. In the entry scan it is 0. In subsequent scans it increments by DT each scan (DT is the PLC scan cycle time, implementation-defined and positive).

S.T_elapsed is undefined for inactive states. Reading T_elapsed of an inactive state is a static error.

In the SMT model, T_elapsed is a symbolic TIME value; the prover reasons about all consistent values without fixing a specific scan rate.

---

21.10 Static Errors

Code	Description
ssfc-no-initial	A region or superstate has no INITIAL state
ssfc-ambiguous-priority	Two guards of the same state are simultaneously satisfiable with no PRIO disambiguation
ssfc-cross-region-conflict	Two or more parallel region lifecycle blocks write the same variable
ssfc-unknown-join-source	A JOIN names a state that does not exist
ssfc-duplicate-join-source	A JOIN lists the same source state twice
ssfc-join-too-few-sources	A JOIN declares fewer than 2 sources
ssfc-invalid-path	A hierarchy path (A.B.C) skips a level or references a non-ancestor

---

21.11 Assurance Claims

The compiler runs the following claims automatically. Their verdicts appear in the assurance report. PASS means the claim holds; WARN means a potential issue was found; FAIL means a confirmed violation.

Claim	Kind	What it verifies
C-SAF	Structural	1-Safeness: P-invariant token balance for every (region, transition) pair, including FORK and JOIN.
C-INT	Structural	Region integrity: transitions stay within structural scope; parallel superstates have consistent coverage.
C-DEAD	Structural	No atomic leaf state has zero outgoing transitions (unless marked TERMINAL).
C-GUARD-SAT	SMT	Every WHEN guard is satisfiable over the variable type domain (with REQUIRE constraints assumed).
C-DET	SMT	No two guards of the same state are simultaneously satisfiable without PRIO disambiguation.
C-DATA-DEAD	SMT	No guard is permanently FALSE given types and REQUIRE constraints. Environmental Waiting (EW) is distinguished.
C-REACH	SMT	Every state is reachable from the initial marking via individually-SAT-satisfiable guard sequence. JOIN: all sources must be reachable.
C-HOME	SMT	Over-approximation (⟸ only). For each state, a per-edge-SAT witness path to a nominated home state exists. PASS does not prove simultaneous co-reachability in parallel regions.

C-HOME scope boundary: PASS means the per-place BFS found a witness path where each edge is individually SAT-satisfiable. It does not prove: - That guards along the path are satisfiable in sequence (guard interactions across steps are not verified). - That all regions of a parallel superstate can simultaneously return to home (co-reachability across regions is not verified).

For safety-case use, cite C-SAF and C-INT as exact structural proofs; cite C-REACH and C-HOME as sound-but-incomplete over-approximations.

---

21.14 Component Composition — WIRING Block

An SSFC may declare sub-instances of other FUNCTION_BLOCK or SSFC types in its VAR block (using the same syntax as §8.1):

VAR
  ctr : Counter;
  seq : PasteurizerSequence;
END_VAR

Sub-instance inputs are wired with the WIRING / END_WIRING block, which appears after the last VAR block and before the first state declaration:

WIRING
  ctr(enable := Active.X);
  seq(start := go, __ssfc_dt := __ssfc_dt);
END_WIRING

Each line is an instance call: instance-name(Input := expr, ...).

Auto-wiring (inst*). Appending * to the instance name before the parentheses enables auto-wiring:

WIRING
  inner*(start := Running.X);
END_WIRING

For every child input not named in the explicit list, the compiler looks for a parent-scope variable with the identical name and type and connects it automatically. Explicit bindings always take precedence. A type mismatch is a compile-time error; an unresolved input (no match found and not explicitly wired) is also an error. Every auto-wired connection is listed in the engineering report.

The primary use case is forwarding the scan-period input __ssfc_dt when a parent SSFC contains a child SSFC — the parent's own __ssfc_dt (added by the compiler) matches the child's by name and type, so inner*(start := s) is equivalent to the verbose inner(start := s, __ssfc_dt := __ssfc_dt).

Wire expressions may reference: - SSFC inputs (go, threshold, …) - SSFC state active-markers (Idle.X, Running.X) — these refer to the post-marking value (current-step, after transitions fire) - SSFC state elapsed-time (Active.T_elapsed) - Other VAR scalar variables (read as current-step values)

__ssfc_dt forwarding. When a child is itself an SSFC, its __ssfc_dt input (the scan-period parameter — see §21.8) must be forwarded explicitly:

WIRING
  seq(start := go, __ssfc_dt := __ssfc_dt);
END_WIRING

Sub-instance outputs are read in lifecycle blocks using inst.field notation (see §21.5); the compiler rewrites these to the flattened alias inst__field__out after composition.

All four composition matrix cases are supported: FB ← FB, FB ← SSFC, SSFC ← FB, SSFC ← SSFC.

Invocation and lifecycle semantics (normative)

Component instances are persistent and always-participating. A sub-instance declared in VAR is created once and executes on every parent scan — it is not gated by the parent SSFC's active state. Its WIRING inputs are recomputed each scan; when those inputs reference state-active markers (State.X) the value is zero/FALSE when the corresponding state is inactive, and the sub-instance receives that as an ordinary input value.

This is always-participating synchronous composition: the sub-instance runs unconditionally alongside the parent, and the SSFC lifecycle controls it declaratively by choosing what values to wire to its inputs. There is no notion of "invoke only in state S" at the runtime level; the WIRING expression is simply a combinational function of the current state markers.

Contrast with FUNCTION_BLOCK composition via IMPLEMENTATION (§10): there, an FB can be conditionally called inside an IF guard. In SSFC WIRING there is no such conditional — the full synchronous product runs every scan.

Design guidance. To deactivate a sub-instance while a state is inactive, wire its enabling input to the appropriate state active-marker:

WIRING
  pump(enable := Running.X);
END_WIRING

When Running is inactive, Running.X = FALSE, so pump receives enable = FALSE and suppresses its own action. The instance itself still executes; the parent's lifecycle controls it through the wired value.

---

21.12 Reserved Words Added by SSFC

The following identifiers are reserved by the SSFC lexer extensions and cannot be used as variable or state names:

SSFC, END_SSFC, STATE, END_STATE, SUPERSTATE, END_SUPERSTATE, INITIAL, TERMINAL, TRANSITION, TO, WHEN, PRIO, PARALLEL, END_PARALLEL, REGION, END_REGION, JOIN, FROM, EN, DU, EX, WIRING, END_WIRING

---

21.13 Grammar

ssfc-definition ::=
  "SSFC" IDENT
    [ "PARAMETER" { param-decl } "END_PARAMETER" ]
    [ "VAR_INPUT"  { var-decl } "END_VAR" ]
    [ "VAR_OUTPUT" { var-decl } "END_VAR" ]
    [ "VAR"        { var-decl } "END_VAR" ]
    [ "WIRING" { instance-call } "END_WIRING" ]
    { state-decl | superstate-decl }
  "END_SSFC"

instance-call ::=
  IDENT [ "*" ] "(" { IDENT ":=" expr "," } [ IDENT ":=" expr ] ")" ";"
  -- trailing "*" after the name enables auto-wiring of same-name/same-type inputs

state-decl ::=
  [ "INITIAL" ] [ "TERMINAL" ] "STATE" IDENT
    [ "EN" ":" lifecycle-body ]
    [ "DU" ":" lifecycle-body ]
    [ "EX" ":" lifecycle-body ]
    { transition-decl }
  "END_STATE"

superstate-decl ::=
  [ "INITIAL" ] "SUPERSTATE" IDENT
    [ "EN" ":" lifecycle-body ]
    [ "DU" ":" lifecycle-body ]
    [ "EX" ":" lifecycle-body ]
    ( parallel-block | { state-decl | superstate-decl } )
    { transition-decl }
  "END_SUPERSTATE"

parallel-block ::=
  "PARALLEL"
    { "REGION" IDENT
        { state-decl | superstate-decl }
      "END_REGION" }
    { join-decl }
  "END_PARALLEL"

join-decl ::=
  "JOIN" "FROM" IDENT { "," IDENT } "TO" IDENT [ "WHEN" bool-expr ] ";"

transition-decl ::=
  "TRANSITION" "TO" IDENT "WHEN" bool-expr [ "PRIO" INTLIT ] ";"

lifecycle-body ::=
  { IDENT ":=" expr ";"
  | IDENT ":" output-rule-list }

---

22. PROGRAM — Root Cyclic POU

A PROGRAM is a non-instantiable root POU. It occupies the same syntactic position as a FUNCTION_BLOCK in a source file but is intended as the entry point of a deployed cyclic application — the POU the runtime calls once per scan cycle.

22.1 Syntax

PROGRAM <name>
  [ CONST … END_CONST ]
  [ VAR_INPUT  … END_VAR ]
  [ VAR_OUTPUT … END_VAR ]
  [ VAR        … END_VAR ]
  IMPLEMENTATION
    <body>
  END_IMPLEMENTATION
END_PROGRAM

PARAMETER and VAR_IN_OUT blocks are not permitted inside a PROGRAM.

22.2 Semantics

Inside IMPLEMENTATION … END_IMPLEMENTATION the body follows the same grammar and semantics as a FUNCTION_BLOCK body: derived assignments, sub-instance wiring, and register output rules. Sub-instances (FB or SSFC) are composed with the identical flattening and composition logic used for FUNCTION_BLOCK.

The SMT model, invariant proof, and IR lowering paths are unchanged.

22.3 Instantiation restriction

A PROGRAM cannot be used as a sub-instance type. Attempting to resolve a PROGRAM type through the FileResolver raises a ComposeError.

22.4 Rust backend — CyclicProgram trait

When the compiler emits Rust code for a PROGRAM root POU it emits:

pub trait CyclicProgram {
    type Inputs;
    type Outputs;
    fn scan(&mut self, inputs: &Self::Inputs,
            outputs: &mut Self::Outputs, ctx: &ScanContext);
}

pub struct ScanContext {
    pub now_ns: u64,
    pub dt_ns: u64,
}

and an impl CyclicProgram for <Name> block with the scan() method. The cycle() method used for FUNCTION_BLOCK is not emitted.

22.5 ST backend

When the ST backend emits a PROGRAM root it uses PROGRAM <name> and END_PROGRAM as the enclosing keywords (not FUNCTION_BLOCK / END_FUNCTION_BLOCK). No AT %I* / AT %Q* address annotations are emitted in v1.

---

End of LoLa Language Reference.