zqel 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
21. SSFC — Super Sequential Function Charts
22. PROGRAM — Root Cyclic POU

---

1. Scope, Conformance Language, and Notation

This document is the normative reference for the zqel 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	zqel 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 .zqel 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 zqel 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 zqel <file> --project <toml> --target check (see §12 and the CLI Reference).

3.2 FUNCTION_BLOCK

FUNCTION_BLOCK <name> [ "<" <type-param> { "," <type-param> } ">" ]
  [ CONST      <const-decls> END_CONST ]
  [ PARAMETER  <param-decls> END_PARAMETER ]
  [ VAR_INPUT  <var-decls> END_VAR ]
  [ VAR_OUTPUT <var-decls> END_VAR ]
  [ VAR        <var-decls> END_VAR ]
  [ CONTINUOUS_REFERENCE <ode-decls> END_CONTINUOUS_REFERENCE ]
  [ WIRING
      { composition-binding | output-forwarding }
    END_WIRING ]
  [ CONTRACT
      { register-rules
      | INVARIANT <bool-expr> ;
      | ASSUME    <bool-expr> ;
      | REQUIRE   <bool-expr> ;
      | RULE      <expr>      ; }
    END_CONTRACT ]
  [ ASSURANCE
      { OUTPUT_ERROR <name> <= <expr> ;
      | STATE_ERROR  <name> <= <expr> ; }
    END_ASSURANCE ]
  [ IMPLEMENTATION
      { derived-definition | register-rules | BY <artifact-id> ; }
      { INVARIANT <bool-expr> ;
      | ASSUME   <bool-expr> ;
      | REQUIRE  <bool-expr> ;
      | RULE     <expr>      ; }
    END_IMPLEMENTATION ]
END_FUNCTION_BLOCK

The order above is positional and normative. The parser accepts each section only in its own place, so a source file that transposes two of them does not merely read oddly — it fails to parse. The three VAR_* blocks are the one exception: they may appear in any order, and each may appear more than once. tests/fixtures/reference/block_layout.zqel is this skeleton written out as a source file; a test parses it, so the order given here is checked rather than asserted.

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.

CONTRACT holds what the block MUST do; IMPLEMENTATION holds how it does it. Both may carry register rules, and the difference is not stylistic: a register in CONTRACT is reference semantics, and a register in IMPLEMENTATION for an output that CONTRACT also names is a candidate which the compiler admits only after proving the two step functions equal on every state and input (§8.0). A block that has no CONTRACT section behaves as before — its IMPLEMENTATION registers carry contract identity themselves.

ASSURANCE is the numeric acceptance policy: the error a MATHREAL-valued output or state is permitted to accumulate against its exact-real meaning (§8.8). It is a separate channel from the proof clauses on purpose — the clauses say what is true in ℝ, the policy says how far the machine may be from it.

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 | BY <artifact-id> ; }
      { 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. zqel run <file.zqel> compiles the PROGRAM to a native Rust binary, links it against zqel-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

zqel 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 zqel 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 zqel/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 zqel'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 of the previous cycle — a one-scan delay, NOT the identity (as this table used to claim). The compiler stores the input in a hidden register (_pre_<name>, rule SET <name> OTHERWISE) and every reading of the program — the Z3 model, an invariant's step check, a derived output and the emitted code for every type — reads that register at the pre-state (#205). For an INVERTED input the register stores the logical value (SET NOT <name>), so PRE(x) of a normally-closed contact reads "not pressed" in the first scan, from the positive default. PRE(PRE(x)) is a two-scan delay through a second register (_pre2_<name>: SET _pre_<name> OTHERWISE); a third level is refused (pre-too-deep)
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.0 The four ways to define an output, and what each one means

Four forms may stand at an output position. They are four different speech acts, not four spellings of one — but the difference is in what each claims and where the value lives, not always in the code that comes out.

Form	Speech act	Storage	Claim
y: SET … OTHERWISE …; (§7.1)	a prioritised register transition	stored state	none beyond the transition itself
y := e; (§7.5)	a combinatorial definition	derived, no storage	none
RULE y = e; (§8)	a scan postcondition	—	that an executed scan relates y and e
RULE y IFF c; (§8, NS-1.8)	an author-chosen definition, stated relationally	derived	that y holds exactly when c does

Three consequences that are easy to miss:

A register and a derived value can compute the same thing and still differ. y: SET a WHEN b PRIO 1; SET FALSE OTHERWISE; and y := IF b THEN a ELSE FALSE; produce the same arithmetic, but the first is stored state and the second is not. Storage decides whether PRE(y) exists (§6.16), whether the power-up obligation applies, and what an artifact check can address.

A plain RULE y = e does not by itself implement y. It states what an executed scan relates. If nothing else defines y, y becomes a synthesis target and an implementation may be derived; if y already has one, the same RULE is a verify-only obligation. IFF is the one form that says "this right side IS the definition" and is materialised directly, without a candidate search.

Writing both is an idiom, not a redundancy. y := a; together with RULE y = a; is the intended way to say "here is the implementation, and here is the property it must satisfy" — the compiler checks the two against each other and refuses a mismatch with a counterexample.

A RULE is also exempt from the power-up obligation, because it speaks about an executed scan and says nothing about the state before the first one. A hand-written INVARIANT keeps that obligation (§8).

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 evaluated this cycle. It holds no persistent state.

What it reads is not uniformly the start-of-cycle state, and §6.16 states the rule correctly: a derived expression sees registers at their freshly computed (next-state) value, and other derived values likewise, ordered by the dependency DAG. That is precisely why PRE exists — it is the cycle cut. To read the previous cycle's value, ask for it: PRE(x).

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

The scan. Scan k reads the inputs I_k and starts from the stored state S_k. The transition definitions — every SET, ON, OFF, HOLD and every guard — hold simultaneously and together determine the post-state S_{k+1}. They are equations, not statements: nothing is executed in the order written.

Meaning is fixed per read site, not per phase. Which value a name denotes depends on where the name stands:

Context	A register r	An input x	A derived value d
rule guard / rule value (a transition definition)	S_k — the start-of-scan value	I_k — this scan's input	d's value for this scan
derived definition (:=)	S_{k+1} — freshly computed	I_k	per the dependency DAG
PRE(…), anywhere	S_k	I_{k-1} — the previous scan's input (§6.16)	invalid — a derived value has no stored pre-state

The whole block is one simultaneous system. The compiler solves it along the dependency DAG and refuses a cycle; that refusal is what §6.16 calls the combinational loop, and PRE is the cut that breaks it.

Inside a transition definition, source order carries no meaning. Every direct register read there is S_k — the register being defined and every other one, written above or below. a: SET b; together with b: SET a; exchanges the two values, in either order; neither observes the other's new value.

In an ordinary value expression of a transition definition, PRE(register) is value-equal to the bare read — where that expression position admits PRE at all. n: SET n + 1 and n: SET PRE(n) + 1 are the same program, with the same trace and the same register set. The examples in this repository write the explicit form, because it names the intended state at the point of use.

Two positions are not ordinary value expressions and keep the short form:

• the signal argument of HELD / ELAPSED (§11). That argument is identity-bearing and history-bearing — the timer keys on the signal it watches — so HELD(PRE(q), pt) is not HELD(q, pt) read at the pre-state, and is refused.
• an argument of a FUNCTION call. PRE is not typeable inside a FUNCTION expression today; since a FUNCTION is inlined (§9), that is a gap rather than a rule, and it is tracked as one.

PRE over an input is not redundant. n: SET n + s and n: SET n + PRE(s) are different programs: the second reads the previous scan's input and pays a hidden register for it (§6.16). Inside a transition definition a bare x and a PRE(r) are both observations at the start of this scan — PRE(x) is the one form that reaches back past it.

Transitions are free of textual order, not of same-scan dependencies. A derived name is a post-scan signal, not a textual macro, and a transition definition may read one — so it may reach a freshly computed register value transitively. Pulling a subexpression out into a := definition can change the phase in which it is evaluated and is therefore not a generally valid refactoring. Measured over the same input sequence:

n: SET n + 1;   m: SET n * 10;            // m = 0, 10, 20, 30
d := n * 10;    n: SET n + 1;  m: SET d;  // m = 10, 20, 30, 40
n: SET n + 1;   m: SET PRE(n) * 10;       // m = 0, 10, 20, 30

The first and third are the same program. The second reads n's post-state through d and therefore runs one scan ahead of them — while remaining independent of the order in which its three lines are written.

This section used to say that all expressions read start-of-cycle values. That is true of a rule block's view of registers and false of everything else; it also contradicted §6.16, which explains that derived outputs see the freshly computed values and gives that as the reason PRE exists. Measured: for a register r and d := r, the compiler lowers d to r's next-state expression, and a trace shows d following r in the same cycle rather than a cycle later.

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.

7.7 Which scan each form speaks about

The forms of §7.0 differ not only in what they claim but in when the claim is required to hold. That phase is part of the meaning, not an implementation detail.

Form	Speaks about
transition definition (SET, ON, OFF, HOLD)	the step from S_k to S_{k+1}
derived definition (:=)	a value of scan k, read at the post-state
RULE (§8.6)	only an executed scan — it says nothing about the state before the first one
INVARIANT (§8.1)	every executed scan and power-up
ASSUME / REQUIRE (§8.2, §8.3)	a premise, at the phase its own section defines
WIRING (§3.6)	no scan at all — it is structural elaboration, evaluated once when the composition is flattened

The RULE/INVARIANT difference is observable and not a nuance. For a derived output q := a, the claim RULE q = a; is admitted, and the same claim written INVARIANT q = a; is refused with invariant-init: at power-up no scan has run, q has no computed value, and the invariant has nothing to stand on. A RULE is exempt precisely because it never speaks about that moment.

WIRING carries no claim of its own for the same reason in the other direction: there is no scan in which it could be evaluated. What it does is decide structure — which instance is connected to which — and the clauses of the connected blocks then speak in the phases above.

---

8. Contracts and Proof

8.0 Where a clause lives — CONTRACT and IMPLEMENTATION

A FUNCTION_BLOCK may carry its proof clauses and its transition registers in either of two sections, and the choice is not stylistic.

CONTRACT
    <register-rules>
    { INVARIANT <bool-expr> ;
    | ASSUME    <bool-expr> ;
    | REQUIRE   <bool-expr> ;
    | RULE      <expr>      ; }
END_CONTRACT

CONTRACT states what the block MUST do. A register rule inside it is reference semantics: it defines the transition the block is required to make, and it is what the contract digest is taken over.

IMPLEMENTATION states how the block does it. A register rule there for an output that CONTRACT does not name carries contract identity itself — this is the ordinary single-section block, and it is unaffected by everything in this subsection. A register rule for an output that CONTRACT does name is a realization candidate: the compiler admits it only after proving the two step functions equal on every state and input, and rejects it on a countermodel and on unknown or timeout alike.

CONTRACT
    run:
        ON WHEN cmd;
        OFF OTHERWISE;
    INVARIANT (NOT run) OR PRE(cmd);
END_CONTRACT

Constraints on the section:

• An output MUST NOT have two register rules inside CONTRACT; a second one for the same name is rejected rather than merged.
• Typed relational clauses (ONLY_WHEN, IMPLIES, IFF, EXCLUDES, §8.6a) are not admitted in CONTRACT. NS-1.4 leaves that surface deliberately open; a RULE carrying one is refused there.
• A CONTRACT register on an output that also has a realization candidate does not disappear from the model: both are kept, and both are rewritten by the same passes.

See the realization ladder (concept) for how a candidate is requested and accepted; the ladder rungs are workflow states, never syntax.

8.0.1 A clause's section is organisational; a register rule's is not

Everything above is about register rules. For a clause — ASSUME, REQUIRE, INVARIANT, RULE — the section is a filing decision and nothing more. Measured by moving one clause from CONTRACT to IMPLEMENTATION and compiling both spellings: the ledger definitions and occurrences, the deployment obligations, the proof phases, the assurance seal, the boundary routing and the emitted artifact are identical. Only ast_digest and ledger_digest differ, because the source differs.

Both placements therefore stay legal, and the recommendation is a style rule rather than a constraint:

Put a clause that states what the block promises to the outside — ASSUME, REQUIRE, and the INVARIANT a caller is entitled to rely on — in CONTRACT. Put a clause that exists to check the implementation against itself — a RULE paired with a := or a rule block, an INVARIANT about a local — in IMPLEMENTATION.

The test is who the clause is addressed to. A reader who wants to know what a block guarantees should be able to read CONTRACT alone and stop there.

This recommendation is not enforced today. A lint may enforce it later; until then a clause in the other section is legal, unremarkable, and produces the same artifact.

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.

Why not, and what to write instead — the mirror register

An INVARIANT is proved by induction: it holds before the first scan, and every scan preserves it. That is a statement about a state.

HELD(c, T) reads like a statement about a trace — what was true for a stretch of time — and that reading used to be the stated reason for the refusal: a trace statement needs k-induction or an explicit trace model. That reason is withdrawn (ADR TX-2.2), and it is worth naming the correction rather than quietly dropping it, because the wrong reason pointed at a much more expensive fix than the real one.

HELD is not a free-floating trace formula. It is a state bit backed by timer registers — started, active, and the clock. Measured (ADR TMR-1, 2026-09-03): with the refusal lifted locally, four ordinary statements proved green under one step of induction, an INVARIANT over a HELD among them.

What actually fails is that the timers' own laws are not part of the step relation, and that is wrong in both directions at once:

statement	truth	today's verdict
INVARIANT NOT HELD(Trip, T#30s)	false — hold Trip for 30 s	green — the step never advances the clock
HELD(Trip, T#30s) IMPLIES HELD(Trip, T#1s)	true	red — two timers over one condition may be assigned independently

So the rule stands and its reason changes: HELD/ELAPSED are refused in an invariant until the timer laws are in the initial and step formulas and clause timers are interned (ADR TMR-1.1 to TMR-1.3). Admitting them is that work, not a change of proof procedure.

What is expressible today is the same fact one step lower: mirror the temporal predicate into a register, and state the invariant over the register.

VAR
    alarm_seen : BOOL;                  // the mirror
END_VAR
IMPLEMENTATION
    alarm_seen:
        ON WHEN HELD(pressure > Limit, T#500ms) PRIO 1;
        HOLD OTHERWISE;

    INVARIANT alarm_seen OR NOT shutdown;   // a STATE claim about the mirror
END_IMPLEMENTATION

The register turns "was true for 500 ms" into "is true now", and the induction then has something it can carry. The cost is explicit and worth naming: the invariant now speaks about the mirror, not about the temporal predicate — if the mirror is reset elsewhere, the claim changes with it.

Whether HELD/ELAPSED become directly admissible in an INVARIANT is decided in ADR TX-2 (issue #173): yes, once TMR-1 is built, and by ordinary base and step induction over the lowered state — not by widening this rule and not by a new proof procedure. The same ADR settles what stays out: general EVENTUALLY for cyclic function blocks, unbounded UNTIL/SEQUENCE, and any claim whose observer state exists only inside the solver.

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 zqel 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 · How-to: verified functions

---

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.

8.8 ASSURANCE — the numeric acceptance policy

ASSURANCE
    { OUTPUT_ERROR <output-name> <= <numeric-literal> ;
    | STATE_ERROR  <name>        <= <numeric-literal> ; }
END_ASSURANCE

ASSURANCE is a separate channel from the clauses in §8.1–§8.6a, and the separation is the point. A RULE or INVARIANT says what is true in exact ℝ. An ASSURANCE bound says how far the machine result may be from that — the roundoff a proof over ℝ cannot see. Changing a bound therefore moves the policy identity of a compilation and leaves its theorem identity alone.

An empty ASSURANCE ... END_ASSURANCE is not part of the grammar; a block that declares no bound omits the section.

OUTPUT_ERROR

OUTPUT_ERROR y <= τ is accepted when the compilation carries a proved error envelope for y whose absolute bound is at most τ. Three outcomes, and none of them is silence:

Situation	Result
Proved envelope, abs_error_bound <= τ	accepted
Proved envelope, abs_error_bound > τ	RequirementViolation — the proof succeeded, the acceptance policy failed
No proved envelope for that name	[assurance-policy-unprovable]
τ is not a numeric literal	[assurance-policy-not-constant]

The third row is the one to know about in practice: a numeric envelope exists only where a representation does. Under the DEFAULT profile MATHREAL is exact ℝ and carries no error to bound, so a policy declared there has nothing to compare against and is refused. Compile under FLOAT64_REPR (§17.3), or a project configuration that sets a representation, and the bound becomes checkable. Until 2026-09-04 this case passed quietly, which meant a bound of 1e-30 on an output provable only to 3.06e-15 compiled clean.

STATE_ERROR

STATE_ERROR is reserved and refused: [state-error-unsupported].

The keyword parses, so that sources written against it keep a stable diagnosis, but this language version has no proved state envelope for such a bound to refer to. A state bound needs its own reference point, instant, and accumulation rule, and those are not defined. The clause is therefore rejected rather than carried unchecked — before 2026-09-04 it was accepted, entered the realization request and the digests, and was read by nothing.

---

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

The first argument is a signal reference

HELD and ELAPSED share one timer, one evaluation phase, and therefore one rule about what may stand in their first position. It is a signal reference, not an arbitrary value expression: the timer keys on the identity of the signal it watches, and the claim is about that signal's own continuous history.

Two ways to violate it, with two causes and two diagnostics:

written	refused with	why
HELD(d, pt) / ELAPSED(d, pt) over a derived d	temporal-derived-signal	a timer condition is evaluated before the derived section; a derived value has no start-of-cycle value to watch (§14.5, §15.2)
HELD(PRE(q), pt) / ELAPSED(PRE(q), pt)	temporal-signal-reference-required	PRE(q) is a value-level read of a signal that is already there; it names no signal the timer can key
a condition containing an expression the timer cannot key — a type conversion, a wide bit-string literal	temporal-signal-reference-required	only signal reads, literals and the operators over them name a signal; compute the value into a register or a derived name first

Dropping the PRE in this position loses nothing, wherever the operator stands: a timer condition is lowered on its own path and reads the start of the scan — in a transition definition and in a derived definition alike. Measured: e := ELAPSED(q, pt) written as a derived definition starts its timer one scan after q turns on, exactly when HELD(q, pt) in a transition does. So the register is written plainly here — the one place in the language where the explicit form of §7.6 is not available.

PRE(x) over an input is admitted, and the asymmetry is the rule rather than an exception to it: over an input PRE is materialised as its own shadow register (§6.16), so it denotes a distinct signal with an identity the timer can key. Over a register it denotes no new signal at all.

When both violations are present — HELD(PRE(d), pt) — the invalid signal reference is reported, because removing the PRE would not make the argument admissible.

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.

ELAPSED shares its timer with HELD(cond, pt) and therefore shares the signal-reference rule of §11.1 in full — the same two refusals, for the same reasons.

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 (zqel/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;

REQUIRE on an EXTERN — the caller's obligation

The grammar accepts REQUIRE clauses before the ENSURE clauses of an EXTERN FUNCTION. They state the artifact's domain — the conditions under which its ENSURE is guaranteed — and they are an obligation on the caller, exactly as for an ordinary FUNCTION (§9.2).

EXTERN FUNCTION fast_scale(x : LREAL) -> LREAL
    REQUIRE x >= -1.0;
    REQUIRE x <= 1.0;
    ENSURE fast_scale = 0.1 * x + 0.2;
    BY fast_scale_f64;

At every call site the compiler substitutes the actual arguments into each REQUIRE and proves it from the calling block's ASSUME and REQUIRE premises. A call that cannot establish it fails with function-require-violated, naming the clause. In the block above, the domain is discharged by the caller's own ASSUME x >= -1.0 and ASSUME x <= 1.0; delete either and exactly the matching REQUIRE is refused.

Until 2026-09-04 none of this happened: the clauses were parsed, filed separately, and read by nothing, so a precondition silently stopped applying the moment a function was marked EXTERN — the one place it matters most, because the body cannot be inspected to find out what it assumes.

What this slice covers, and what it refuses. The obligation is proved for direct calls in the block's own register rules and derived definitions. Two positions are outside it, and both are refused rather than skipped:

• an EXTERN call inside an ordinary FUNCTION body — refused by the contract pass, since the extern has no body to encode;
• an EXTERN call in a specification clause — refused as extern-spec-call (EX-3): an EXTERN contract is not a spec premise.

Anything else that reaches the check but cannot be decided — a clause that does not encode, a solver unknown — is refused as extern-require-undecided rather than counted as discharged. Undecided is not proved.

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.

This section is about BY on an EXTERN FUNCTION — a function contract. The same keyword also appears inside an IMPLEMENTATION, where it binds a whole block's transition semantics. That is a different construct with its own laws; see §12.6.

12.4 Manifest and Warrant Levels

The Verified Library manifest at zqel/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 zqel source parameter names). The entailment solver checks whether the declared ENSURE clauses imply the manifest's lola_contract.

12.5 zqel extern Toolchain

The zqel extern sub-command manages the Verified Library:

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

See the CLI Reference for full option documentation.

---

12.6 BY on an IMPLEMENTATION — the realization switch

BY inside an IMPLEMENTATION replaces the block's statements with a binding to a registered artifact:

IMPLEMENTATION
    BY trip_latch_rust;
END_IMPLEMENTATION

This is not the EXTERN FUNCTION form of §12.3. There, BY discharges the ENSURE clauses of one function. Here it discharges the complete transition semantics of the block, state included — every output the CONTRACT names, in every scan, not merely an invariant that happens to hold.

The laws below are enforced, and each names the refusal you get for breaking it.

L2 — statements or BY, never both. An IMPLEMENTATION that names a register or a derived definition may not also carry BY. The realization switch is exactly one line, so that no reader has to work out which half of a block is authoritative:

FB-wide BY and inline statements are mutually exclusive (CRS L2) — the realization switch is exactly one line

L4 — only a registered, proved artifact binds, fail-closed. An unknown artifact id is not a warning and not an auto-resolve; it is a refusal:

BY realization 'x' is not registered as a proved artifact — FB-wide BY binds only registered, proved implementation warrants (CRS L4, fail-closed)

The warrant must cover the transitions, not the invariant. An artifact whose warrant proves only the block's INVARIANT is refused, by name:

transition coverage missing: its warrant binds only [...], but a BY artifact must satisfy the complete transition semantics, not only the invariant

Every contract output must be covered. A warrant that omits one of the outputs the CONTRACT names is refused with the missing outputs listed.

The warrant must be measured, and measured against THIS contract. An unmeasured registration cannot bind (no sealed code<->transition warrant), and a warrant measured against a different canonical transition projection is refused even when the artifact is otherwise registered and proved:

its transition warrant binds a DIFFERENT canonical transition projection than this contract

The warrant must be a proved EQUIVALENCE_THEOREM. Any other verdict or classification is refused, with both values printed.

What BY does not prove

BY does not make the block's contract true, and it does not verify the artifact. It transfers a proof obligation onto a warrant that was established elsewhere and sealed. The compiler's part is to refuse every binding whose warrant does not answer exactly this contract — which is why each law above is a refusal rather than a check that can be waived.

Two consequences worth stating plainly:

• A green compile of a BY block asserts that a sealed, proved equivalence warrant exists for this contract's transition projection. It asserts nothing about code that never entered that warrant.
• BY under snapshot= is refused rather than approximated: artifacts are consumed from the ProjectSnapshot, and process-global registration may never influence snapshot semantics.

The binding needs a live registration

A BY block does not carry its warrant in the source file. The warrant is looked up by artifact id at compile time, and at the compiler version in this repo that lookup reads a process-local registration — there is no manifest entry that makes a transition warrant persistent the way §12.4 does for EXTERN function artifacts.

The practical consequence is worth stating, because it is easy to mistake for a bug: stdlib/TripLatch.zqel compiled on its own is refused, not accepted.

$ zqel --target check stdlib/TripLatch.zqel
verification failed:
  [crs-realization] TripLatch: BY realization 'trip_latch_rust' is not
  registered as a proved artifact — FB-wide BY binds only registered, proved
  implementation warrants (CRS L4, fail-closed)

That is L4 doing its job: no warrant in scope, so no binding.

stdlib/TripLatch.zqel is therefore a test-backed reference specimen under an active registration, not a standalone runnable example. Read it together with tests/test_stdlib_triplatch.py, which registers the measured warrant and then exercises both the acceptance and every refusal above. Nothing in examples/ uses IMPLEMENTATION BY, and that is a consequence of the paragraph above rather than an oversight.

13. MATHREAL Semantics

13.1 MATHREAL = ℝ (Mathematical Model)

In the zqel 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; zqel 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 zqel 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 (zqel/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 does not raise and claims nothing: the verdict is inconclusive (conclusive=False, neither target reported safe). The fixed-point check does not apply to binary64. The finite-range decision is made by the float64 range gate (RangeReport.verdict and may_emit), which refuses emission when a value can leave the finite binary64 range

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

Inside a rule guard or rule value, a direct register reference denotes its value at the beginning of the cycle, so a rule block needs no ordering: the rules hold simultaneously and may be written in any sequence.

Order-freedom is not the same as freedom from same-cycle dependencies, and only the first follows from the rule above. A transition definition may read a derived name, and a derived name reads registers freshly (§7.6) — so a transition can observe another register's new value transitively, through a := definition. Extracting a subexpression into a derived name is therefore not a meaning-preserving rewrite; §7.6 carries the measured three-way comparison.

A derived assignment is not subject to that rule. It reads registers and other derived values at their freshly computed value, ordered by the dependency DAG (§6.16, §7.6). PRE(x) is how a derived expression asks for the start-of-cycle value instead.

A consequence: if output A depends on output B and B on A, that is a semantic non-issue for registers — they read their pre-state — but a circular dependency for derived assignments. The compiler detects and rejects combinatorial cycles in derived definitions, and PRE is the documented way to cut one.

15.3 Atomic Commit

After all rule and derived expressions are evaluated — each reading what §15.2 says it reads — the stored registers are updated simultaneously. A register's new value is visible to another register's rule only in the next cycle when that rule reads it directly; a rule reading it through a derived definition sees it in this one (§7.6, §15.2).

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 zqel/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.

Scope note. The productions below are checked against zqel/parser.py where they are reachable from a FUNCTION_BLOCK source file. Four of them had drifted and were corrected on 2026-09-04: the source-file production (one root POU, not a list of blocks — §3.1), the section list of function_block, the shape of register_rule (which showed braces the lexer does not have), and a rule production naming a keyword GENERATES that no version of the language has had.

source_file      ::= { function_def | extern_function_def } root_pou
root_pou         ::= function_block | program_block | ssfc_block
                   (* an EXTERN_REAL_CONTRACT file has its own form, §3.1(d) *)

function_block   ::= FUNCTION_BLOCK IDENT [ type_param_header ]
                       [ const_block ]
                       [ parameter_block ]
                       { var_block }
                       [ continuous_reference ]
                       [ wiring ]
                       [ contract ]
                       [ assurance ]
                       [ implementation ]
                     END_FUNCTION_BLOCK
                   (* the order is positional; only the var_block group
                      may repeat and may be given in any order *)

const_block      ::= CONST { IDENT ":" scalar_type ":=" expr ";" } END_CONST
parameter_block  ::= PARAMETER
                       { IDENT ":" scalar_type ";" | require }
                     END_PARAMETER

wiring           ::= WIRING { instance_wire | forward_assign } END_WIRING
forward_assign   ::= IDENT ":=" ( IDENT | IDENT "." IDENT ) ";"

contract         ::= CONTRACT { register_rule | contract_clause } END_CONTRACT
contract_clause  ::= invariant | assume | require | rule

assurance        ::= ASSURANCE assurance_clause { assurance_clause }
                     END_ASSURANCE
assurance_clause ::= ( OUTPUT_ERROR | STATE_ERROR ) IDENT "<=" expr ";"
                   (* STATE_ERROR parses and is refused, §8.8 *)

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 { guard_rule }
guard_rule       ::= action ( WHEN expr [ PRIO INT_LIT ] | OTHERWISE ) ";"
action           ::= ON | OFF | HOLD | SET expr

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 expr ";"
                   | RULE expr ( ONLY_WHEN | IMPLIES | IFF | EXCLUDES )
                          expr ";"        (* §8.6a; not admitted in CONTRACT *)

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 zqel/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. The list is the content of zqel.lexer.KEYWORDS, and tests/test_reference_reserved_words.py holds it to that: a keyword added to the lexer without being named here would silently take a name away from every program that used it.

Block structure: FUNCTION_BLOCK, END_FUNCTION_BLOCK, FUNCTION, END_FUNCTION, EXTERN, BY, CONST, END_CONST, PARAMETER, END_PARAMETER, VAR_INPUT, VAR_OUTPUT, VAR, VAR_STATE, END_VAR, WIRING, END_WIRING, IMPLEMENTATION, END_IMPLEMENTATION, CONTINUOUS_REFERENCE, END_CONTINUOUS_REFERENCE, PROGRAM, END_PROGRAM, EXTERN_REAL_CONTRACT, END_EXTERN_REAL_CONTRACT, SEMANTICS, END_SEMANTICS

Contracts: INVARIANT, ASSUME, RULE, REQUIRE, ENSURE, VARIANT, ONLY_WHEN, IMPLIES, IFF, EXCLUDES, REQUIRES, WITHIN, LIVENESS, EVENTUALLY

Ports: INVERTED

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, PARALLEL, END_PARALLEL, REGION, END_REGION, JOIN, EN, DU, EX

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

19.1 Context words — spelled like keywords, reserved like nothing

The following are matched by identifier text in one specific position and are not reserved: outside that position they are ordinary names, and a variable may be called any of them.

CONTRACT, END_CONTRACT, ASSURANCE, END_ASSURANCE, OUTPUT_ERROR, STATE_ERROR, TO, FROM, MOD, ARRAY, OF, SORT, IN, SUM, COUNT, ALL, ANY, EXISTS, MIN, MAX, DER, SORTED, PERMUTATION_OF

That CONTRACT and ASSURANCE are context words is deliberate and not an oversight: the two sections were added to a language that already had programs in the field, and reserving those names would have renamed variables in sources nobody was editing.

---

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

When EN and EX write the same output

EX runs at step 4 and EN at step 7 (§21.8), so in a scan where a transition fires, the EN of the entered state overwrites what the EX of the departing state wrote. The scan table already fixes the order; this states what the order means for an output both blocks assign, which is otherwise something each reader has to derive.

It has one consequence worth stating outright, because the natural first attempt runs into it.

A pulse written in the departing state's EX never fires.

  STATE Drin
    EX: Passiert := TRUE;          (* never observed *)
    TRANSITION TO Bereit WHEN Nach;
  END_STATE

The target's EN (or DU) assigns Passiert in the same scan and wins. Nothing downstream ever sees the pulse — a counter fed from it stays at zero.

The one-scan pulse is a dedicated step. Give the event its own state whose EN raises the signal, and leave that state unconditionally:

  STATE Drin
    TRANSITION TO Fertig WHEN Nach;
  END_STATE

  STATE Fertig
    EN: Passiert := TRUE;
    TRANSITION TO Bereit WHEN TRUE;
  END_STATE

Passiert is TRUE for exactly the scan spent in Fertig, and the successor's EN/DU clears it on the way back. A counter fed from it counts one per pass. Both shapes are pinned in tests/test_ssfc_pulse_semantics.py.

Leaving out the unconditional transition gives a state rather than a pulse: the signal then stands for as long as the chain does, which is the right shape for "finished, waiting to be acknowledged" and the wrong one for an edge.

Two practical notes:

• The state may not be called Done if an output is called done — identifiers are case-insensitive, and the collision is rejected with state name collides with variable declared at line 7.
• A state left only by an input guard draws the usual No possible stuck state warning. That is a true statement about the model and not specific to this idiom; the unconditional form above does not draw it.

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 zqel Language Reference.