Skip to content

Looking back

22. What zqel is — and is not

It helps to know the shape of the box you are working in. zqel is a synchronous, reactive state-transition language for control logic — not a general-purpose, Turing-complete programming language. A block reads inputs, computes its next state from the current state, and writes outputs, once per scan. Computation unfolds over time (across scans), never as an unbounded loop within a scan.

The single boundary that draws the box is the Bounded-Cycle-Theorem: every valid zqel program has a statically proven, finite per-scan execution. This — not a list of banned features — is the real admission test. It is exactly why CBMC is complete on the generated code and why Z3 decides the model. Everything you have met either is, or is not, admissible by that one criterion:

  • Arrays and repetition are allowed — but only at statically fixed size. An aggregate or a MAP over 1..8 is bounded repetition with a statically known trip count (§13–15). A SORT, a RULE-defined array, a recursive FUNCTION are all admitted because they unroll to a finite expression whose size is known now (§16–17). What is not admissible is a loop or an array whose length is a runtime value.
  • Unsafe operations are allowed — but only with a discharged proof. Division and a dynamic array index are partial; they compile only when the divisor / index is proven safe (§9, §14).
  • INT has + - * but no division or modulo (only the real types divide, as a guarded partial operation).

These are not oversights — they are the price and the enabler of the “prove all states” guarantee. The boundary is easiest to feel with three examples in examples/algorithms/:

  • Fibonacci (fibonacci.zqel) fits naturally — it is a state machine: two registers, (a, b) → (b, a + b), one number per scan. (Registers have no custom init, so a seeded flag sets a = 0, b = 1 on the first scan; INT is 16-bit, so it wraps after F(24).)
  • Sorting fits at a fixed size — and §16 shows the declarative way to say it: SORT, a RULE spec, or a bounded recursive isort. The early bubble_sort5.zqel hand-unrolled a compare-swap network; its successors state the result instead. What all of them share is the fixed size — arbitrary-length sorting needs a runtime-bounded loop, which is not expressible.
  • is_prime(n) (is_prime.zqel) fits only bounded: with no modulo or loops, compositeness is an aggregate — n is composite iff ANY(a, b : a·b = n) over a bounded product range. Unbounded primality needs unbounded computation zqel deliberately cannot express.

The rule of thumb: if a construct has a statically finite execution, it fits — whether that is a bounded state machine, a statically bounded aggregate, a synthesised network, or a bounded recursion. If it needs runtime-unbounded data or iteration, it does not. If you find yourself wanting a for loop whose trip count only the plant knows, you have stepped outside what a verifiable PLC block is — and that is by design.

23. The whole language, on one page

  • You declare the what, not the how. Outputs are defined by prioritised rules (registers, which have memory) or by := (derived, combinational). The compiler synthesises the formula and prints it as ST or Rust.
  • Priority is explicit. The highest-priority active rule wins; the order you wrote the rules is irrelevant; equal-priority conflicts are compile-time errors, and dead rules are reported as warnings (or as errors in --strict mode).
  • Reading time is defined. Inside a register's rules, other registers read their old (start-of-scan) value; through a := definition they read their new value. All outputs update simultaneously (the _next staging).
  • Properties are proven, not tested. INVARIANT is proven by induction over all states; timers are symbolic, so timing properties hold for all timings; a failed proof comes with a concrete counterexample.
  • Unsafe operations carry obligations. Division and a dynamic array index require a proof (or a path-sensitive IF guard) that the divisor is non-zero / the index is in range.
  • Repetition is bounded and static. Arrays have a compile-time size; aggregates (ALL ANY COUNT SUM MIN MAX) and the ARRAY(…) MAP emit as loops with statically known bounds, and are proven structurally (quantifier, recurrence, or witness axioms) rather than by expanding them. A SORT or a permutation RULE is synthesised into a compare-swap network and its sortedness proven; a FUNCTION may recurse only on a static measure, so it unrolls fully. Everything obeys the Bounded-Cycle-Theorem: a statically proven, finite per-scan execution.
  • Template blocks scale structure without runtime generics. FUNCTION_BLOCK Vec<N: UINT> is a compile-time recipe: each instantiation (Vec<3>, Vec<4>) is monomorphized into a separate concrete type with concrete array bounds, its own proof, and its own generated code — the static-size invariant never bends.
  • Contracts scale. ASSUME states caller obligations; under composition a child premise either bubbles up to the caller (wired to parent inputs) or is discharged by the parent as a proof obligation (wired to internal logic); child invariants are preserved.
  • Functions carry their own contracts. A FUNCTION with REQUIRE/ENSURE is proved by the compiler before any call site sees it; the ENSUREs become available facts at every call, and the compiler blames the call site if the REQUIRE is not earned (§17).
  • External proofs join by contract. An EXTERN FUNCTION … BY <artifact> lets a warrant from an external tool (exhaustive enumeration, Creusot, CBMC) flow into the model as an assumed postcondition. Every invariant that rests on it is labelled with the artifact and its warrant — audited or proved — so nothing is silently promoted (§18).
  • Units and ranges are static. Dimensional analysis is checked then erased; certified ranges choose the numeric representation — all without changing behaviour.
  • One source of truth. Every rule above is defined once, in the Z3 model. The ST and Rust backends are pretty-printers over it and cannot diverge from the proof or from each other.

For the normative specification of every construct above — syntax, semantics, proof obligations, and diagnostics — see the Language Reference.

24. Four mental checkpoints

Before you write a zqel block, ask yourself these four questions:

  1. What is state, and what is just a fresh calculation? If it must remember across scans, it is a register (rules). If it is just computed from this scan's results, it is :=.
  2. What happens if two conditions are true at once? Write the priorities so the conflict is explicit. Do not rely on text order.
  3. What must never happen? Those are candidates for INVARIANT.
  4. What must the environment promise me? Those are candidates for ASSUME.
  5. What can the compiler prove itself, and what needs an external warrant? If a pure zqel FUNCTION can establish the property (§17), use that. If the operation has a soundness gap zqel cannot close — overflow, a domain-specific algorithm, a Creusot/CBMC proof — declare it EXTERN … BY <artifact> (§18) and the compiler will label every invariant that rests on it with the warrant it inherits.

That is zqel: you write intent and safety requirements; a machine proves them and writes the code. Your job shifts from ”did I code it right?” to ”did I specify the right thing?” — and the compiler guarantees the rest.

Every example in the repository

The sections above walk through the examples that teach something in order. This is all of them — every file under examples/, grouped by what it carries rather than by when it was written. It is a map for when you already know roughly what you are looking for, not a second reading of the pages above.

Two groups repay a look before you need them. The exercises under examples/rias/ come with their original task statement beside the model, so you can read what the requirements said before anyone thought about proof. And examples/algorithms/lm_step/ is the largest thing here: a numerical kernel split into blocks that are each proven separately, with their error envelopes composed.

Two models named in the plan for this page are not in the repository yet — the pedestrian-crossing SSFC and the badge reader. They are listed here so their absence is visible rather than silently skipped; they follow separately.

Starting points

The blocks the sections above are built on.

  • counter.zqel — A bounded up-counter. Value stays in [0, 10]; the invariant is proven
  • const_limit.zqel — the same counter with its bound NAMED: a CONST is substituted before the proof, so the rule and the invariant cannot drift apart
  • motor.zqel — Two interlocked motors. MotorA has priority; MotorB must yield to it
  • motor_conflict.zqel — the symmetric interlock — it looks correct and the proof finds the cycle in which both motors start
  • motor_contract.zqel — the same interlock as motor.zqel, written as a CONTRACT — same rules, different standing
  • pressure.zqel — Pressure guard with a delayed shutdown
  • rs_latch.zqel — a set-dominant RS latch; the priorities make the tie-break explicit instead of implying it
  • two_timers.zqel — two independent HELD timers with different durations, and why their states cannot be confused

The IEC 61131-3 standard blocks

Every standard function block, expressed in zqel rather than assumed. Timers carry a variable PT and report ET; the counters keep their edge state hidden, as the standard requires.

  • ctd.zqel — down counter — the edge state is a hidden VAR, and Q is derived, so it does not lag a scan
  • ctu.zqel — up counter, IEC-conformant: variable preset, and the load path in its standard order
  • ctu_edge.zqel — the same counter built by composition — an edge detector instance instead of an inline previous value
  • ctud.zqel — up/down counter; both outputs derived, so neither lags
  • f_trig.zqel — falling-edge detector; the memory bit is internal, not a port
  • r_trig.zqel — rising-edge detector; the memory bit is internal, not a port
  • rs.zqel — reset-dominant bistable — priority is what makes RESET win, and it is written down
  • sr.zqel — set-dominant bistable — the same block with the priorities the other way round
  • tof.zqel — off-delay timer with variable preset and elapsed-time output
  • ton.zqel — on-delay timer, complete: variable preset as a TIME input, elapsed time as an output
  • tp.zqel — pulse timer — the pulse starts on the rising edge and runs its preset out

Composition

One block built from others — and the array-of-blocks form, where N identical channels are composed and proven together.

  • Channel.zqel — one channel of a bank — the block an array of instances holds N of
  • ChannelBank.zqel — an array of blocks: N identical channels composed and proven together, once
  • RS.zqel — a reset-dominant bistable, reused as a sub-block by StartStop.zqel
  • StartStop.zqel — a start/stop station built from that bistable — composition at its smallest

Arrays and aggregates

The declarative side: what the values must satisfy, not the loop that produces them.

  • conditioning.zqel — eight raw ADC channels conditioned by stating what the results must satisfy
  • decl_sort.zqel — sorting as pure constraints — the strongest declarative form, no network at all
  • fir4.zqel — a four-tap FIR filter written as a dot product over the window
  • linearize.zqel — an elementwise map: eight raw counts into engineering units
  • selector.zqel — a multiplexer — pass channel sel through, stated as a property of the result
  • sensor_monitor.zqel — eight temperature sensors monitored without a loop and without an index variable
  • sort5.zqel — sorting stated as a property rather than spelled out as a network
  • threshold_stats.zqel — reductions over an array, emitted as accumulator loops on the target

Algorithms

Where the declarative form is doing real work — recursion with a termination measure, an unrolled network, a property with no formula.

  • bubble_sort5.zqel — bubble sort unrolled into a fixed compare-swap network of five inputs
  • fibonacci.zqel — a new Fibonacci number each scan — a state machine, not a loop
  • insertion_sort.zqel — insertion sort defined recursively, with the termination measure that makes it bounded
  • is_prime.zqel — primality for 0..100 without modulo and without division

Code that stands in for a block

The transition semantics comes from a registered, proved artifact instead of from rules written in the file. What the compiler checks before it binds is the point: the artifact's sealed warrant must have been proved against this contract's canonical transition projection, and nothing else binds.

  • TripLatchBy.zqel — IMPLEMENTATION BY: a latch whose step function is a verified Rust artifact, registered in the manifest

A verified numerical kernel

One damped Gauss-Newton step, decomposed into blocks that are each proven separately and composed with their error envelopes. This is the largest thing in the repository and the one that exercises the numerical assurance chain end to end.

Analog signal processing

Continuous quantities on a discrete scan: integrators, a differentiator, and PID with anti-windup.

  • differentiator.zqel — A discrete differentiator: d = (x - x_prev) / DT
  • flow_totalizer.zqel — a totalizer with physical units: volumetric flow integrated into a volume
  • integrator.zqel — A clamped integrator: y accumulates x over time (DT = elapsed seconds from the
  • pid.zqel — A PID controller with output saturation and integral anti-windup

Three of those state the mathematics for any input, which is what makes them reference examples — and exactly what a machine representation cannot promise. Choosing Float64 adds an obligation ℝ does not have: every value the programme evaluates has to fit in a binary64, and y + x * DT is evaluated before CLAMP ever sees it. So each has a sibling that declares the caller's operating envelope, and that is the one a deployment emits:

  • integrator_bounded.zqel — the clamped integrator under a declared input span and band ceiling
  • differentiator_bounded.zqel — the differentiator under an input span; note that the span alone is not enough, because IF DT <> 0.0 proves the division happens, not that its result is representable — the profile has to state a minimum scan interval too
  • pid_bounded.zqel — the same controller under a declared envelope on gains, error and band
  • pid_system.zqel — a concrete instance with its gains fixed
  • assurance_policy.zqel — an ASSURANCE bound: the programme is right in ℝ, and this says how far the machine may be from it. Compiled under a representation, because an error envelope only exists where one is chosen

PID as a composition

The same controller again, this time split into blocks and closed around a plant — the pair to read when composition is the question.

  • PID.zqel — A PID controller with output saturation and integral anti-windup. The
  • pid_loop.zqel — Closed-loop: first-order plant + inline PID (flat, no composition)
  • pid_system.zqel — a concrete instance with its gains fixed
  • plant.zqel — First-order plant: ẏ = -2y + 2u (pole at -2 rad/s, T = 0.5 s)

Control loops with a certificate

A closed loop whose stability is proven, not simulated.

  • Loop.zqel — the closed loop as a composition — Plant and PController wired together
  • PController.zqel — Proportional controller with actuator saturation: u = clamp(-K*x, -umax, umax)
  • Plant.zqel — PT1 plant as its own FB. It guarantees its state stays in [-10,10] PROVIDED
  • closed_loop.zqel — A closed control loop in a single block, with a proven Lyapunov certificate

Discretisation

A continuous reference (CONTINUOUS_REFERENCE) beside its discrete implementation, so the gap between them can be bounded.

  • external_pid.zqel — a PID whose continuous reference is declared beside it, so the discretisation gap can be bounded
  • lowpass.zqel — a first-order lowpass derived from its own ODE by forward Euler

Sequential function charts

SSFC in its own right: a minimal chart, a chart with parallel regions and a JOIN, and a full batch process.

A complete plant

The batch pasteuriser as a PROGRAM: an SSFC for the sequence, a PI controller for the temperature, composed into one root.

Counting and access control

A works car park, first written straight and then as a composition — the pair that shows what composition buys.

Industrial exercises, as they were set

Teaching exercises modelled unchanged, each with its original task statement beside it. Their value is that the requirements were written before anyone thought about proof.

  • AxleCounter.zqel — axle counting in a track section — the difference between entering and leaving axles is the occupancy
  • AxleGate.zqel — one sensor pair of that axle counter, on its own
  • ConveyorInterlock.zqel — two conveyors with an interlock between them
  • StirredReactor.zqel — a batch reactor as a sequence — the one exercise in this set that is a chart
  • TunnelCount.zqel — a single-bore tunnel: count the cars inside and drive the signals from that count
  • TwoHandPress.zqel — a press with two-hand interlocking — and the proof that found a real fault in the first draft

EXTERN — operations zqel does not implement

A contract without a body, discharged by a registered artifact.

  • sat_add_u8.zqel — a typed external contract over unsigned parameters
  • saturating_abs.zqel — an external contract by example — an operation zqel does not implement itself
  • saturating_add.zqel — a second external operation, added entirely from the user side
  • saturating_sub.zqel — saturating subtraction, the complement to the addition above
  • scale.zqel — saturating multiply-divide, the shape analog I/O scaling actually needs

Realization: contracts without an implementation

RULE-only blocks whose implementation is supplied afterwards and then proved against them.

  • affine_real_gs.zqel — an exact-real contract with a proved binary64 error envelope beside it
  • arg_max4_gs.zqel — arg-max over four values as three RULEs — the indexed one is admitted only after its own index bounds are proved
  • clamp_gs.zqel — clamp, stated once as a conditional RULE under ASSUME lo <= hi
  • debounce_gs.zqel — a stateful debounce: the candidate receives the pre-state and returns output plus next state
  • hysteresis_int_gs.zqel — integer hysteresis, the second stateful slice
  • sat_add_gs.zqel — saturating addition as a single RULE over the exact sum
  • sort4_semantic_gs.zqel — sorting stated as meaning, not as a network: SORTED(s) and PERMUTATION_OF(s, a)

The integer and bit-string types

The IEC types beyond INT, and what their ranges mean for a proof.

  • lword_flags.zqel — sixty-four independent boolean signals packed into one word
  • sint_saturate.zqel — the signed byte type, and what saturating at its range means for a proof
  • unsigned_counters.zqel — the unsigned integer family, and where their ranges differ from the signed ones

Bit strings as status words

BYTE, WORD, DWORD as what they are on a real bus.

  • quality_byte.zqel — BYTE as an eight-bit status word, the way a real bus carries it
  • status_word.zqel — WORD and DWORD as status words of sixteen and thirty-two bits

Strings

WSTRING as a carrier — compared and passed, not computed on.

  • device_tag.zqel — WSTRING as a carrier — compared and passed on, not computed with

Wider intermediate arithmetic

Scaling that would overflow in INT, done in DINT and proven not to.

  • dint_scale.zqel — ADC scaling that would overflow in INT, done in DINT and proven not to

Interoperability

A block transferred from an MTP standard project, kept as a compatibility reference.

  • anaview.zqel — a block transferred from an MTP standard project, kept as a compatibility reference

A test holds this list complete: every .zqel file under examples/ must appear above, or stand in an explicit exclusion list with a reason. That is the only way a page like this stays true — the previous version of it named 21 of the 106.

Where to go next

You want to… Go to
Look up a keyword, type, or operator Language Reference
Look up SSFC syntax and semantics Language Reference §21 — SSFC
Look up ownership and recovery claim definitions and EvidenceStrength Assurance Reference
See all CLI options and output formats CLI Reference
Configure MATHREAL representation or sampling Project Configuration Reference
Model a sequential process with SSFC How-to: Model a Sequential Machine
Model concurrent sequences with JOIN How-to: Model Parallel Regions
Compose an SSFC with FB or SSFC child components How-to: Compose Components
Check which state owns each output How-to: Audit Signal Ownership
Prove safe recovery within N scans How-to: Prove Safe Recovery
Add an externally-verified function How-to: Verified Functions
Configure MATHREAL / Float64 representation How-to: Configure MATHREAL Representation
Diagnose a proof failure How-to: Diagnose Proof Failures
Understand pre-state semantics and priorities Concepts: Synchronous semantics
Understand SSFC scan model and assurance scope Concepts: SSFC Semantics
Understand FB/SSFC composition and WIRING Concepts: Component Model
Understand signal ownership analysis Concepts: Ownership and Effects
Understand recovery and progress analysis Concepts: Recovery and Progress
Understand MATHREAL = ℝ and the numerical assurance chain Concepts: Numerical semantics
Understand what "proved" guarantees Concepts: Assurance model
Understand EXTERN warrant inheritance Concepts: EXTERN trust model
Understand guided synthesis and its relationship to EXTERN Concepts: EXTERN trust model §guided-synthesis
Accept and use a guided synthesis candidate How-to: Realize a contract
Look up GuidedSynthesisWarrant fields Reference: GuidedSynthesisWarrant
Read the compiler internals Architecture