Many values at once

13. Arrays and bounded repetition

Every signal so far has been a single value. Real controllers watch banks of them: eight temperature sensors, sixty-four samples, four PID channels. You could of course write out T1, T2, … T8 and eight near-identical rules — and that is exactly what the early hand-written examples looked like. It was miserable, and it hid the intent. zqel gives you arrays and aggregates so you state the result over the whole array at once:

Before the first example, here is the minimal vocabulary:

Syntax	Meaning
ARRAY[lo..hi] OF T	an array type with fixed compile-time bounds
a[i]	read element i of array a
ARRAY(i IN lo..hi : e)	build a new array by computing each element
OP(i IN lo..hi : e)	aggregate over a fixed index range (ALL, ANY, COUNT, SUM, MIN, MAX)

The important point is that lo..hi is not runtime data. It is part of the source and therefore known at compile time. That is why zqel can admit arrays while still forbidding open-ended loops.

VAR_INPUT
    T   : ARRAY[1..8] OF MATHREAL<degC>;   // the 8 sensor readings
    Lim : MATHREAL<degC>;                  // the alarm threshold
END_VAR
VAR_OUTPUT
    all_ok  : BOOL;   any_hot : BOOL;   n_alarm : INT;
    hottest : MATHREAL<degC>;              average : MATHREAL<degC>;
END_VAR
IMPLEMENTATION
    all_ok  := ALL  (i IN 1..8 : T[i] <= Lim);
    any_hot := ANY  (i IN 1..8 : T[i] >  Lim);
    n_alarm := COUNT(i IN 1..8 : T[i] >  Lim);
    hottest := MAX  (i IN 1..8 : T[i]);
    average := SUM  (i IN 1..8 : T[i]) / 8.0;
    ...

(Full example: examples/arrays/sensor_monitor.zqel.)

An aggregate has the shape OP(i IN lo..hi : body): it folds body, evaluated for each index in the range, with OP. The vocabulary:

Aggregate	Result	Reads like
ALL(i IN … : p)	BOOL	every element satisfies p
ANY / EXISTS	BOOL	at least one satisfies p
COUNT(i IN … : p)	INT	how many satisfy p
SUM(i IN … : e)	number	the total
MIN / MAX	number	the extreme value

The crucial constraint — and it is the whole reason arrays are allowed at all — is that the index range is a compile-time constant set. ARRAY[1..8] has exactly eight elements, known now. That is the Bounded-Cycle principle: every valid program has a statically proven finite per-scan execution. An aggregate over a static range keeps that promise — the work per scan is known up front, never a loop the PLC has to run an unknown number of times.

What the compiler makes of it

_r0 := TRUE;
FOR i := 1 TO 8 DO
    _r0 := _r0 AND (T[i] <= Lim);
END_FOR;
all_ok := _r0;

_r2 := 0;
FOR i := 1 TO 8 DO
    _r2 := _r2 + SEL((T[i] > Lim), 0, 1);      (* COUNT: a sum of 0/1 *)
END_FOR;
n_alarm := _r2;

A plain accumulator loop with a statically known trip count — the shape a PLC programmer would have written by hand, except you did not have to.

Two views of the same aggregate. Here is a distinction worth holding on to. What you just saw is the emitted code, and it is a loop. What the prover sees is something else: ALL/ANY become a quantifier (∀i/∃i), SUM/COUNT a recurrence, MIN/MAX a value pinned by two axioms (it bounds every element, and one element attains it). The proof therefore does not grow with the range: ALL over 256 elements is under 20 formula nodes rather than 256 terms.

Why care? Because if the proof secretly expanded the aggregate while the emitted code showed a tidy loop, then the day a large array made verification slow, nothing in the visible artifact would point at the cause. Keeping both views structured keeps the cost attributable.

Because the prover reasons about the aggregate as a whole rather than element by element, the operating envelope — itself an aggregate — proves the block's guarantees directly:

    ASSUME ALL(i IN 1..8 : T[i] <= 200.0);
    ASSUME ALL(i IN 1..8 : T[i] >= -50.0);
    INVARIANT hottest <= 200.0;   INVARIANT average <= 200.0;

✅ Proven: hottest and average stay within [-50, 200] — a MAX and a mean never escape the readings. The same magnitude bounds are what the float64 range gate uses to certify that the SUM behind average stays inside the finite binary64 range on either target.

---

14. Indexing as a partial operation

In §9 you met the idea that some operations are partial: division is only defined when the divisor is non-zero, so it carries a proof obligation. A dynamic array index — a[k] where k is a runtime value, not a constant — is the very same idea. Channel[sel] is only defined when sel is in bounds, so it carries the obligation array-index-out-of-bounds, discharged exactly like division-by-zero:

FUNCTION_BLOCK Selector
VAR_INPUT
    Channel : ARRAY[0..7] OF MATHREAL;
    sel     : INT;
END_VAR
VAR_OUTPUT selected : MATHREAL; END_VAR
IMPLEMENTATION
    selected := Channel[sel];
    ASSUME sel >= 0;
    ASSUME sel <= 7;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

(Full example: examples/arrays/selector.zqel.)

Drop either ASSUME and compilation fails — not with a warning, with a concrete counterexample:

[array-index-out-of-bounds] Channel[sel] can be reached with sel = -32768

Just like division, the bound may instead be proven path-sensitively from an enclosing IF 0 <= sel AND sel <= 7 THEN …. A constant index (Channel[3]) is free: the compiler checks it against the declared range at compile time, no proof needed.

What the compiler makes of it

Once the index is proven in range, the backends index their native arrays directly — which is sound precisely because of the proof:

selected := Channel[sel];      (* native ST array access, proven in-range *)

In the Z3 model the same read is a loop-free nested ITE over the eight element constants, so the model stays quantifier-free and decidable.

Rule of thumb. A constant index is free. A computed index costs you a bound — the exact same bargain as /. If you cannot prove the index is in range, zqel will not let the block compile, because on the plant it would read past the array.

---

15. Building arrays: the MAP

Arrays have been inputs so far. You can also produce one as an output, element by element, with an ARRAY(…) constructor — a MAP over a range:

VAR_OUTPUT
    Bar    : ARRAY[0..7] OF MATHREAL<bar>;  // conditioned pressures (a MAP result)
    worst  : MATHREAL<bar>;   n_high : INT;
END_VAR
IMPLEMENTATION
    Bar    := ARRAY(i IN 0..7 : Raw[i] * gain);   // MAP: scale every channel
    worst  := MAX  (i IN 0..7 : Bar[i]);          // REDUCE over the built array
    n_high := COUNT(i IN 0..7 : Bar[i] > 10.0);
    ...

(Full example: examples/arrays/conditioning.zqel.)

Bar is a first-class array on the block's interface, not a bag of scalars: the ST backend emits ARRAY[0..7] OF LINT, the Rust backend [i64; 8]. Each element is a derived value, and you can immediately aggregate over the array you just built — worst and n_high fold Bar, so a MAP feeds a REDUCE.

The constructor itself is worth reading slowly:

ARRAY(i IN 0..7 : Raw[i] * gain)

• i is a local index variable that exists only inside this expression.
• 0..7 is the fixed compile-time range over which the array is built.
• Raw[i] * gain is the value of the resulting element at position i.

So ARRAY(...) is not a mutable fill loop. It is an array-valued expression: “build me the whole array whose i-th element is ...”.

What the compiler makes of it

Bar[0] := ((Raw[0] * gain) / 1000);
Bar[1] := ((Raw[1] * gain) / 1000);
…                                       (* one derived assignment per element *)
worst  := SEL(…);                        (* the compare-swap MAX chain over Bar *)

Units flow elementwise: Raw is dimensionless counts, gain is bar-per-count, so each Bar[i] is checked to be bar. The magnitude ASSUMEs keep every product inside the finite binary64 range, so the whole block is provably emission-safe on both targets.

---

16. Three ways to say “sorted”

Sorting is the textbook “I obviously need a loop” task — so it is the sharpest test of a language that has none. zqel gives you three ways to obtain a sorted array, all loop-free, all statically finite, and each more declarative than a hand-written bubble sort. (Forcing bubble was the wrong instinct in the first place: in Prolog you would never encode a particular sorting algorithm to say what “sorted” means.)

16.1 State the result — SORT

The least you can say is: s is a, sorted.

VAR_OUTPUT s : ARRAY[0..4] OF MATHREAL; END_VAR   // a, sorted non-decreasing
IMPLEMENTATION
    s := SORT(a);
END_IMPLEMENTATION

(Full example: examples/arrays/sort5.zqel.)

As a language element, SORT means exactly this:

• its argument must be a fixed-size array;
• its result has the same element type and shape;
• it specifies the sorted version of that array, not a particular algorithm;
• the current implementation is intentionally bounded in size, because the proof cost grows with the network.

The compiler realises SORT as a compare-swap sorting network — which network, and how it is later optimised, is the compiler's concern, not the source's. Two guarantees come for free:

• permutation, by construction — every network step is a compare-swap (the min/max of a pair), which can only rearrange values;
• sortedness, proven — Z3 auto-adds and discharges s[0] <= s[1] <= …. If the network were wrong, compilation would fail with a counterexample.

✅ Proven: s[0] <= s[1], s[1] <= s[2], s[2] <= s[3], s[3] <= s[4] — the sortedness invariants, auto-generated and discharged over the realised network.

Because the sortedness proof is the expensive part (not the code — the shared network is emitted compactly via memoised DAG walks and backend CSE), SORT is capped at 8 elements (~3 s to prove).

16.2 Constrain the result — RULE

Stronger still: give sorted no := definition at all, and pin it down purely by stating what it must be.

VAR_OUTPUT sorted : ARRAY[0..3] OF INT; END_VAR   // defined only by the RULEs
IMPLEMENTATION
    RULE permutation(xs, sorted);
    RULE ALL(i IN 0..2 : sorted[i] <= sorted[i + 1]);
END_IMPLEMENTATION

(Full example: examples/arrays/decl_sort.zqel.)

This is where students most often need a hard conceptual separation:

• := says how a value is computed.
• INVARIANT says what must always be true of code you already wrote.
• RULE says what value is allowed, even if you did not write the computation.

So RULE is not a “stronger invariant”. It plays a different role in the language: it participates in defining the solution.

This is the contract/implementation split made into language. permutation(xs, sorted) says sorted is a rearrangement of xs; the compiler realises it as a compare-swap network, so the permutation holds by construction. The ALL(…) RULE says sorted is ordered; that is proven on the realised network — and it is what actually pins sorted to the one sorted order. The RULEs are the what, the network is a how the compiler chose, and Z3 proves the how meets the what. An unsatisfiable RULE (say, the opposite order) is a compile error.

✅ Proven: sorted[0] <= sorted[1] <= sorted[2] <= sorted[3] — discharged against the network the compiler synthesised for the permutation RULE. No runtime solver runs; everything is compiled and proven ahead of time.

Recall §5: an INVARIANT is a property proven about code you wrote. A RULE turns that around — you write only the property, and the compiler finds code that satisfies it and proves it does. That is the shift from verification to synthesis.

16.3 Define the computation — a bounded recursive FUNCTION

Sometimes you do want to spell out the algorithm. zqel lets you — with a FUNCTION and bounded recursion — and still forbids the unbounded loop:

Start with the simplest mental model. A function has the shape

FUNCTION name(arg1 : T1, arg2 : T2, ...) -> R
    expression
END_FUNCTION

and means:

• it is stateless: a function has no VAR, no hidden memory, no scan-to-scan state;
• its body is an expression, not a statement list;
• calling it just means substitute, inline, simplify at compile time;
• recursion is allowed only when the compiler can prove it terminates on a static decreasing measure.

Before the sorting example, a tiny non-recursive one:

FUNCTION clamp01(x : MATHREAL) -> MATHREAL
    IF x < 0.0 THEN 0.0 ELSE IF x > 1.0 THEN 1.0 ELSE x
END_FUNCTION

This already shows the intended reading: a FUNCTION is a pure expression-level abbreviation. It does not “run later at runtime with its own stack frame” in the usual programming-language sense.

FUNCTION swap(a : ARRAY[0..5] OF INT, i : INT, j : INT) -> ARRAY[0..5] OF INT
    ARRAY(p IN 0..5 : IF p = i THEN a[j] ELSE IF p = j THEN a[i] ELSE a[p])
END_FUNCTION

FUNCTION bubble(a : ARRAY[0..5] OF INT, k : INT) -> ARRAY[0..5] OF INT
    IF k <= 0 THEN a
    ELSE IF a[k - 1] <= a[k] THEN a
    ELSE bubble(swap(a, k - 1, k), k - 1)
END_FUNCTION

FUNCTION isort(a : ARRAY[0..5] OF INT, k : INT) -> ARRAY[0..5] OF INT
    IF k <= 0 THEN a
    ELSE bubble(isort(a, k - 1), k)
END_FUNCTION
...
    sorted := isort(xs, 5);

(Full example: examples/algorithms/insertion_sort.zqel.)

A FUNCTION is a compile-time macro: the compiler inlines it and unrolls the recursion completely, leaving a loop-free expression. The one hard rule makes that always possible: recursion must reduce a static measure — here the index k, known at each call site by constant folding — so it bottoms out at compile time. A PLC scan has bounded WCET; a recursion on a runtime measure would not, and is a compile error.

✅ Verified four ways: reference simulator = Z3 model = executed ST = compiled Rust, over the whole unrolled chain (tests/test_functions.py). Unlike SORT, nothing is auto-proven sorted here — you defined the computation, so it scales further than the proof-bounded SORT.

Design choice — synthesis vs. definition, one model. SORT and RULE state a property and let the machine find and prove a realisation (synthesis); the recursive FUNCTION gives the computation and lets the machine prove the unrolled chain. All three end at the same proven Z3 model, and the same backends print it. The unrolled network is a shared-object DAG — memoised, then CSE'd into temporaries computed once — so the emitted code stays compact even though each recursive step conceptually rebuilds the array.

---