LoLa Language Reference — Documentation Coverage Inventory

D1 snapshot. Updated whenever the compiler changes a public surface.

This table maps every user-visible language feature to its canonical source locations and its documentation status in docs/reference/language.md.

Legend: - Lexer — defined in lola/lexer.py - Parser — recognized by lola/parser.py - Sema — enforced by lola/sema.py - SMT — encoded by lola/smt.py - Types — defined in lola/types.py - Operators — defined in lola/operators.py - Status: ✅ documented · 🔲 stub · ❌ missing

---

Program-structure keywords

Feature	Lexer token	Parser production	Ref §	Tutorial example	Status
FUNCTION_BLOCK	FUNCTION_BLOCK	parse_function_block	§3.2	intro §2	✅
END_FUNCTION_BLOCK	END_FUNCTION_BLOCK	same	§3.2	—	✅
FUNCTION	FUNCTION	parse_function	§3.3, §9	intro §8	✅
END_FUNCTION	END_FUNCTION	same	§3.3, §9	—	✅
EXTERN FUNCTION	EXTERN	parse_extern_function	§3.4, §12	intro §9	✅
BY	BY	extern function	§12.3	extern/ examples	✅
VAR_INPUT	VAR_INPUT	_parse_var_block	§4.1	intro §2	✅
VAR_OUTPUT	VAR_OUTPUT	same	§4.2	intro §2	✅
VAR	VAR	same	§4.3	intro §5	✅
VAR_STATE	VAR_STATE	EXTERN_REAL_CONTRACT only	§4.4, §3.5	t2/external_pid	✅
END_VAR	END_VAR	all var blocks	§4	—	✅
IMPLEMENTATION	IMPLEMENTATION	parse_function_block	§3.2	intro §2	✅
END_IMPLEMENTATION	END_IMPLEMENTATION	same	§3.2	—	✅
CONTINUOUS_REFERENCE	CONTINUOUS_REFERENCE	parse_function_block	§13.5	t2/lowpass.lola	✅
END_CONTINUOUS_REFERENCE	END_CONTINUOUS_REFERENCE	same	§13.5	—	✅
EXTERN_REAL_CONTRACT	EXTERN_REAL_CONTRACT	parse_extern_real_contract	§3.5	t2/external_pid	✅
END_EXTERN_REAL_CONTRACT	END_EXTERN_REAL_CONTRACT	same	§3.5	—	✅
SEMANTICS	SEMANTICS	EXTERN_REAL_CONTRACT	§3.5	t2/external_pid	✅
END_SEMANTICS	END_SEMANTICS	same	§3.5	—	✅

---

Contract keywords

Feature	Lexer token	Parser production	Ref §	Tutorial example	Status
INVARIANT	INVARIANT	FB / ERC	§8.1	intro §4	✅
ASSUME	ASSUME	FB	§8.2	intro §7	✅
REQUIRE	REQUIRE	FB / FUNCTION / ERC	§8.3	guide-verified	✅
ENSURE	ENSURE	FUNCTION / EXTERN FUNCTION	§8.4, §9.2	guide-verified	✅
VARIANT	VARIANT	FUNCTION	§8.5, §9.3	algorithms/	✅
RULE	RULE	FB	§8.6	—	✅

---

State-transition keywords

Feature	Lexer token	Parser production	Ref §	Tutorial example	Status
ON	ON	_parse_output_rules	§7.2	motor.lola	✅
OFF	OFF	same	§7.2	motor.lola	✅
HOLD	HOLD	same	§7.2	motor.lola	✅
SET	SET	same	§7.2	counter.lola	✅
WHEN	WHEN	same	§7.3	motor.lola	✅
OTHERWISE	OTHERWISE	same	§7.3	motor.lola	✅
PRIO	PRIO	same	§7.4	motor.lola	✅
:= (derived)	ASSIGN	parse_function_block	§7.5	intro §5	✅

---

Expression keywords

Feature	Lexer token	Parser production	Ref §	Tutorial example	Status
AND	AND	_parse_and	§6.3	motor.lola	✅
OR	OR	_parse_or	§6.3	motor.lola	✅
XOR	XOR	_parse_xor	§6.3	bits/	✅
NOT	NOT	_parse_not	§6.3, §6.5	motor.lola	✅
TRUE	TRUE	_parse_primary	§2.3.1	—	✅
FALSE	FALSE	_parse_primary	§2.3.1	—	✅
IF/THEN/ELSE	IF, THEN, ELSE	_parse_primary	§6.6	pressure.lola	✅
HELD	HELD	_parse_primary	§11.1	two_timers.lola	✅
ELAPSED	ELAPSED	_parse_primary	§11.2	—	✅
CLAMP	CLAMP	_parse_primary	§6.13	intro §10	✅
LEN	LEN	_parse_primary	§6.14	strings/	✅
DT	DT	_parse_primary	§6.15	intro §9	✅
MOD	identifier by text	_parse_mul	§6.2	—	✅

---

Primitive types

Type	Width	Family	Lexer token	Ref §	Tutorial example	Status
BOOL	—	BOOL	BOOL	§5.1	motor.lola	✅
SINT	8 signed	INTEGER	SINT	§5.2	t1/sint_saturate	✅
INT	16 signed	INTEGER	INT	§5.2	counter.lola	✅
DINT	32 signed	INTEGER	DINT	§5.2	dint/dint_scale	✅
LINT	64 signed	INTEGER	LINT	§5.2	algorithms/	✅
USINT	8 unsigned	INTEGER	USINT	§5.3	t1/unsigned_counters	✅
UINT	16 unsigned	INTEGER	UINT	§5.3	t1/unsigned_counters	✅
UDINT	32 unsigned	INTEGER	UDINT	§5.3	t1/unsigned_counters	✅
ULINT	64 unsigned	INTEGER	ULINT	§5.3	t1/unsigned_counters	✅
BYTE	8 bitstring	BITSTRING	BYTE	§5.4	bits/quality_byte	✅
WORD	16 bitstring	BITSTRING	WORD	§5.4	bits/status_word	✅
DWORD	32 bitstring	BITSTRING	DWORD	§5.4	mtp/anaview	✅
LWORD	64 bitstring	BITSTRING	LWORD	§5.4	t1/lword_flags	✅
REAL	—	REAL	REAL	§5.5, §13	t2/lowpass	✅
LREAL	—	REAL	LREAL	§5.5, §13	—	✅
TIME	—	TIME	TIME	§5.6	iec/ton	✅
WSTRING	—	WSTRING	WSTRING	§5.7	strings/device_tag	✅

---

Named constants

Constant	Value	Ref §	Status
SINT_MIN	−128	§2.3.4	✅
SINT_MAX	127	§2.3.4	✅
INT_MIN	−32768	§2.3.4	✅
INT_MAX	32767	§2.3.4	✅
DINT_MIN	−2147483648	§2.3.4	✅
DINT_MAX	2147483647	§2.3.4	✅
LINT_MIN	−9223372036854775808	§2.3.4	✅
LINT_MAX	9223372036854775807	§2.3.4	✅
USINT_MIN	0	§2.3.4	✅
USINT_MAX	255	§2.3.4	✅
UINT_MIN	0	§2.3.4	✅
UINT_MAX	65535	§2.3.4	✅
UDINT_MIN	0	§2.3.4	✅
UDINT_MAX	4294967295	§2.3.4	✅
ULINT_MIN	0	§2.3.4	✅
ULINT_MAX	18446744073709551615	§2.3.4	✅

---

Type conversion builtins

Function	src → dst	Ref §	Status
SINT_TO_INT	SINT → INT	§5.10	✅
INT_TO_SINT	INT → SINT	§5.10	✅
INT_TO_DINT	INT → DINT	§5.10	✅
DINT_TO_INT	DINT → INT	§5.10	✅
INT_TO_LINT	INT → LINT	§5.10	✅
LINT_TO_INT	LINT → INT	§5.10	✅
DINT_TO_LINT	DINT → LINT	§5.10	✅
LINT_TO_DINT	LINT → DINT	§5.10	✅
SINT_TO_USINT	SINT → USINT	§5.10	✅
USINT_TO_SINT	USINT → SINT	§5.10	✅
INT_TO_UINT	INT → UINT	§5.10	✅
UINT_TO_INT	UINT → INT	§5.10	✅
DINT_TO_UDINT	DINT → UDINT	§5.10	✅
UDINT_TO_DINT	UDINT → DINT	§5.10	✅
LINT_TO_ULINT	LINT → ULINT	§5.10	✅
ULINT_TO_LINT	ULINT → LINT	§5.10	✅
USINT_TO_UINT	USINT → UINT	§5.10	✅
UINT_TO_USINT	UINT → USINT	§5.10	✅
UINT_TO_UDINT	UINT → UDINT	§5.10	✅
UDINT_TO_UINT	UDINT → UINT	§5.10	✅
UDINT_TO_ULINT	UDINT → ULINT	§5.10	✅
ULINT_TO_UDINT	ULINT → UDINT	§5.10	✅

---

Binary operators (operator matrix)

Operator	Permitted types	Ref §	Status
+	signed int, unsigned int, REAL/LREAL, bitstring (exp.)	§6.2	✅
-	same	§6.2	✅
*	same	§6.2	✅
/	same	§6.2	✅
MOD	signed int, unsigned int, bitstring (exp.) — NOT REAL	§6.2	✅
AND	BOOL, bitstrings	§6.3	✅
OR	BOOL, bitstrings	§6.3	✅
XOR	BOOL, bitstrings	§6.3	✅
=	all primitives	§6.4	✅
<>	all primitives	§6.4	✅
<	numeric (not BOOL, not WSTRING)	§6.4	✅
<=	numeric	§6.4	✅
>	numeric	§6.4	✅
>=	numeric	§6.4	✅

Unary operators

Operator	Permitted types	Ref §	Status
NOT	BOOL, bitstrings	§6.3, §6.5	✅
unary -	signed int, REAL/LREAL	§6.5	✅

---

Aggregate and constructor expressions

Feature	Syntax	Ref §	Example	Status
SUM	SUM(i IN lo..hi : body)	§6.10	arrays/threshold_stats	✅
COUNT	COUNT(i IN lo..hi : body)	§6.10	arrays/	✅
ALL	ALL(i IN lo..hi : body)	§6.10	arrays/	✅
ANY	ANY(i IN lo..hi : body)	§6.10	arrays/	✅
EXISTS	EXISTS(i IN lo..hi : body)	§6.10	—	✅
MIN (agg)	MIN(i IN lo..hi : body)	§6.10	arrays/	✅
MAX (agg)	MAX(i IN lo..hi : body)	§6.10	arrays/	✅
ARRAY (ctor)	ARRAY(i IN lo..hi : body)	§6.11	arrays/	✅
SORT	SORT(array-name)	§6.12	algorithms/decl_sort	✅
CLAMP	CLAMP(x, lo, hi)	§6.13	analog/	✅
LEN	LEN(wstr)	§6.14	strings/	✅
DT	DT	§6.15	intro §9	✅
HELD	HELD(cond, pt)	§11.1	iec/ton	✅
ELAPSED	ELAPSED(cond, pt)	§11.2	—	✅
IF expr	IF c THEN a ELSE b	§6.6	pressure.lola	✅

---

Profiles

Profile	CLI flag	Ref §	Status
DEFAULT	--profile default	§17.1	✅
PILOT	--profile pilot	§17.2	✅
FLOAT64_REPR	--profile float64	§17.3	✅

---

SSFC keywords

Added in D7 (2026-08-17). These keywords extend the language surface covered by §21 of reference/language.md and by the docs/concepts/ and docs/how-to/ pages below.

Feature	Lexer token	Parser production	Ref §	Tutorial example	Status
SSFC	SSFC	parse_ssfc	§21	intro §21.1	✅
END_SSFC	END_SSFC	same	§21	—	✅
INITIAL STATE	INITIAL, STATE	_parse_state	§21.1	intro §21.1	✅
STATE … END_STATE	STATE, END_STATE	same	§21.1	intro §21.1	✅
TERMINAL STATE	TERMINAL	same	§21.6	intro §21.6	✅
SUPERSTATE … END_SUPERSTATE	SUPERSTATE	_parse_superstate	§21.4	intro §21.4	✅
TRANSITION TO … WHEN	TRANSITION, TO, WHEN	_parse_transition	§21.1	intro §21.1	✅
EN: / DU: / EX:	EN, DU, EX	_parse_lifecycle	§21.2	intro §21.2	✅
PARALLEL … END_PARALLEL	PARALLEL	_parse_parallel	§21.5	intro §21.5	✅
REGION … END_REGION	REGION	same	§21.5	intro §21.5	✅
JOIN FROM … TO	JOIN, FROM	same	§21.5	intro §21.5	✅
WIRING … END_WIRING	WIRING	_parse_wiring	§21.7	intro §21.7	✅
inst* (star-wiring)	—	_parse_wiring	§21.7	how-to/compose-components	✅
State.X	.X field	sema	§21.3	intro §21.3	✅
State.T_elapsed	.T_elapsed field	sema	§21.3	intro §21.3	✅
__ssfc_dt	identifier	_parse_wiring	§21.7	how-to/compose-components	✅
ASSUME (SSFC)	ASSUME	parse_ssfc	§21.6	intro §21.9	✅
INVARIANT (state)	INVARIANT	_parse_state	§21.6	—	✅

---

A1 ownership analysis terms

These terms appear in lola/ssfc_ownership.py and are documented in reference/assurance.md and concepts/ownership-and-effects.md.

Term	Source	Concepts page	How-to	Assurance ref	Status
OwnershipClass	ssfc_ownership.py	concepts/ownership-and-effects.md	how-to/audit-signal-ownership.md	reference/assurance.md	✅
SINGLE_WRITER	same	same	same	same	✅
EXCLUSIVE_MULTI_WRITER	same	same	same	same	✅
COMPATIBLE_MULTI_WRITER	same	same	same	same	✅
CONFLICTING	same	same	same	same	✅
UNKNOWN	same	same	same	same	✅
analyze_ownership()	same	same	same	same	✅
OwnershipReport	same	same	same	same	✅
ComponentEffect	same	same	same	same	✅
conflict_free()	same	same	same	same	✅
analysis_complete()	same	same	same	same	✅
is_clean()	same	same	same	same	✅

---

A2 recovery analysis terms

These terms appear in lola/ssfc_recovery.py and are documented in reference/assurance.md and concepts/recovery-and-progress.md.

Term	Source	Concepts page	How-to	Assurance ref	Status
EvidenceStrength	ssfc_taxonomy.py	concepts/recovery-and-progress.md	—	reference/assurance.md	✅
PROVED	same	same	—	same	✅
PROVED-CONDITIONAL	same	same	—	same	✅
NOT-PROVED	same	same	—	same	✅
NOT-REFUTED	same	same	—	same	✅
UNKNOWN	same	same	—	same	✅
ASSUMED	same	same	—	same	✅
analyze_recovery()	ssfc_recovery.py	same	how-to/prove-safe-recovery.md	same	✅
RecoveryClaim	same	same	same	same	✅
RecoveryEvidence	same	same	same	same	✅
RecoveryReport	same	same	same	same	✅
PossibleSucc(M)	same	same	—	same	✅
no_stall(M)	same	same	—	same	✅
Universal attractor	same	same	—	same	✅
Attractor rank / bound_scans	same	same	same	same	✅
Deletion test (assumptions_used)	same	same	same	same	✅

---

D7 documentation files

Pages added in the D7 documentation track (2026-08-17).

File	Type	Covers
reference/assurance.md	Reference	EvidenceStrength, all T4.5–T7 structural claims, A1 OwnershipClass + API + policy gates, A2 claim levels + formulas + RecoveryClaim fields
concepts/component-model.md	Explanation	FB/SSFC equal-rank composition, WIRING block, persistent semantics, dt forwarding
concepts/ownership-and-effects.md	Explanation	A1: lifecycle co-activation, OwnershipClass meanings, transitive component effects, conflict_free() vs analysis_complete()
concepts/recovery-and-progress.md	Explanation	A2: four claim levels, PossibleSucc, universal attractor construction and soundness, BOUNDED rank, deletion test
how-to/compose-components.md	How-to	FB-in-FB, FB-in-SSFC WIRING, star-wiring, SSFC-in-SSFC with __ssfc_dt
how-to/audit-signal-ownership.md	How-to	Run A1, read classifications, fix CONFLICTING, transitive effects, CI gate
how-to/prove-safe-recovery.md	How-to	7-step: choose states, declare ASSUME, run A2, read four levels, inspect assumptions_used, BOUNDED for WCRT, NOT_PROVED as design finding

---

Known gaps

All previously-listed gaps were closed in the post-T2 documentation pass (2026-08-14):

Feature	Section	Status
Composition (VAR, instance, wiring)	§10	✅ documented (§10.1–10.6)
Array OF FB	§10.4	✅ documented
WSTRING capacity constraint proof	§4.5	✅ Z3-axiom semantics added
Physical unit validation	§4.7	✅ text was complete; stub label removed
Grammar BNF	§18	✅ full BNF derived from parser
REAL overflow analysis / gate	§13.4	✅ gate table + fail-closed semantics
Engineering Error Report	§13.6	✅ new section with budget decomposition
Definedness obligations (div/mod)	§6.2	✅ table + path-sensitivity
PERMUTATION_OF proof obligations	§9.5	✅ four forms + comprehension proof