Architecture¶

For conceptual background on semantics, assurance, and trust models, see docs/concepts/. This document covers the compiler's internal structure.

Scope of a zqel claim (read this first). zqel currently delivers a proof in the Z3 model under explicit assumptions. A statement about the target code holds only for the specific validated combination of language subset × backend × toolchain version × runtime. See docs/review-iec61131-fb.md § Assurance Gates for the gates that must be closed before a pilot, and for the per-feature validation status. Do not read "verified" as "the emitted program is proven equivalent" — read it as "the model is proven, and this backend/toolchain slice has been checked to the stated degree."

G1 status (2026-07-23). G1 is internally closed for the immutable canonical PILOT profile at code commit a8e686ba75f6ebf59c994b0dcf2971d0c253327f. This is a deliberately smaller ST+Rust core, not an independent external acceptance and not pilot readiness: DEFAULT remains experimental and G2–G4 remain open.

The one rule¶

The Z3 model is the single source of truth for semantics. No backend invents its own meaning: new language features are modelled in the AST, defined in the SMT layer, and flow into every backend from there — never implemented in one code generator. The parser carries no logic.

But the backends are not "pure pretty-printers". They transform: total Ites may lower to eager IEC SEL, while an Ite protecting a partial operation lowers to lazy statement control flow; defense guards remain around divisors/indices. They map a HELD to a native timer; they narrow MATHREAL widths. Those transformations are part of the semantic trusted computing base (TCB) today — parser, typing, normalisation, the core IR and the SMT encoding are trusted, and the backends + EXTERN artifacts are validation- reducible but not yet trusted-out (CBMC/Kani check the emitted artifact for a bounded slice; that lowers the trust needed, it does not remove the backend from the TCB). A small certificate-checking core is a good long-term goal, not a licence for a stronger claim today.

For the plan-covered Ite/Reduce/CSE/computed-array cases, they no longer decide evaluation placement and emission scheduling. After verification, zqel/emission.py builds one backend-neutral, integrity-checked EmissionPlan snapshot: re-rolled forms, materialised Ite/Reduce nodes, guard scopes, per-sink reachability, CSE order, computed-array order and neutral names. The plan is bound to every next-state root and timer (name, cond, pt) of the concrete Program; stale, foreign or accidentally modified plans fail before either backend reads an EXTERN artifact or mutates renderer state. scopes.plan_for is an internal placement subpass of that compiler boundary, not an API a backend may call. This removes duplicate scheduling truth for those cases; renderer phase order and target-specific expression, timer, representation and ABI lowering remain backend responsibilities. ST/Rust therefore stay in the semantic TCB described above and require the G3 validation matrix. The digest is an internal consistency check, not a cryptographic boundary against a caller already executing arbitrary Python inside the compiler process (such a caller is part of the TCB and can patch the backend).

One deliberate exception: time. A HELD is verified against the Z3 reference semantics, but each backend maps it to a native timer (ST TON, Rust monotonic deadline). HELD does not expose that timer's internal state or elapsed delta through the function block interface; DT is a separate, explicit runtime value (and an ST cycle_dt input). In the IR a HELD is therefore an opaque Held node. Backend timer correctness is assured separately by reference/Z3/ST/Rust timed traces, including real matiec TON execution for the admitted slice; it is not derived from the Z3 formula alone.

Phases¶

Phase	Module	Responsibility
1 Lex	`zqel/lexer.py`	source → tokens
1 Parse	`zqel/parser.py`	tokens → AST (syntax only)
2 Sema	`zqel/sema.py`	names, types, symbol table
2b Dim	`zqel/dimension.py`	physical-unit check (erased after)
3 SMT	`zqel/smt.py`	AST → canonical Z3 model (the meaning)
4 Verify	`zqel/verify.py`	reachability, invariant proofs
5 Lower	`SemanticModel.to_ir`	controlled Z3→IR or type/control-flow-preserving AST→IR → common backend IR
5b Repr	`zqel/represent.py`	Z3-certified MATHREAL ranges → width (opt-in)
5c Ovfl	`zqel/overflow.py`	per-target MATHREAL overflow safety (mandatory/hard in PILOT; advisory in DEFAULT)
5d Plan	`zqel/emission.py`	one integrity-checked, backend-neutral emission schedule
6 Emit	`zqel/backends/`	IR → ST / Rust text

Why there are two controlled paths into one IR¶

The Z3 model remains the normative meaning. For the total boolean/INT core, SemanticModel._encode_rules folds priority rules into nested Ifs, z3.simplify minimizes them, and _z3_to_ir converts the result to the common IR. For expressions where simplification can erase information needed for faithful target lowering — notably MATHREAL, bit strings, WSTRING and partial or temporal sinks — SemanticModel.to_ir deliberately preserves the typed/control-flow AST and lowers it to the same IR. Both paths are compiler-owned and both backends consume their result; a backend may not choose the semantic path.

        priority rules (AST)
                │  _encode_rules  (nested If, folded by explicit PRIO; default = PRE)
                ▼
        Z3 next-state expr
                │  z3.simplify
                ▼
        minimized Z3 expr  ──_z3_to_ir──────────────┐
                                                    ├──► common IR ──► ST / Rust
        typed AST ── type/control-flow AST lowering ┘

Explicit priorities¶

Every WHEN rule carries an explicit PRIO n; OTHERWISE is the priority-less fallback. Among the rules whose guards fire, the highest PRIO decides the output — text order is irrelevant. _encode_rules folds the nested If by descending priority (highest ends up outermost). Two design guarantees, both checked by Z3 in verify.py:

No silent tie-breaks. If two equal-PRIO rules can fire together with different results, that is an ambiguous-priority error with a counterexample. Equal priority with matching values (e.g. several OFF rules) is fine.
Dead rules surfaced. A rule always dominated by a higher-priority rule is reported as an unreachable-rule warning.

This replaces the old implicit "first rule in the text wins" semantics: priority is now something the author states, never something the compiler infers.

Atomic update in the backends¶

Outputs may reference each other's pre-values, so a naive sequential assignment would break the simultaneous-update semantics. Both backends stage every output into a temporary/local first, then commit — a faithful rendering of atomicity, not added logic.

Sharing in the IR is identity-based: a subexpression is emitted once when it is literally the same node, and twice when two structurally equal trees were built independently. The obvious next step — hash-consing at IR construction, or a structural CSE pass in the backend — was measured and declined.

The measurement was taken before anything was changed, on the two heaviest numeric blocks:

Block	DAG nodes	Ceiling for structural CSE
`LMFit.zqel`	341	74 nodes (21.7 %)
`LM_Step.zqel`	33	0 nodes (0.0 %)

That is an upper bound, not a projection: it counts every structurally equal subtree as if hoisting it were free and lossless. The largest repetitions in these programs are already shared by identity, so what remains is the tail.

Against that, two costs are real rather than hypothetical:

Readability of the emitted ST. These programs are read by PLC engineers, and an inline expression beats a chain of _t7 := … bindings that must be traced back before the logic is visible. The generated code is not only an artifact for a compiler; it is evidence a human is expected to check.
Target tolerance for temporaries. matiec and the target systems have limits on temporary variables, and a pass that manufactures them trades a bounded emission gain for an unbounded portability risk.

Decision. Identity sharing stays; no additional structural CSE. This is a design decision, not an omission, and it is written down here so the question does not have to be re-litigated from scratch each time someone notices a duplicated subtree in generated output.

When to reopen. Only on a concrete problem, not on the aesthetics of the emitted code: an artifact that exceeds a size limit, or a backend compiler that fails on the duplication. Then the ceiling above is the number to re-measure first, because 21.7 % on the worst block is what is available to win.

Testing contract¶

The target contract is feature-specific: parser and model tests are broad; ST/Rust differential, exhaustive and artifact-level checks exist for documented slices. G3 must record the exact feature × backend × toolchain × runtime coverage. No generic statement that every emitted program was run over all reachable states is currently justified.

Types¶

zqel	Z3 sort	codegen (Rust / ST)	notes
`BOOL`	`Bool`	`bool` / `BOOL`
`INT`	`BitVec(16)`	`i16` (`wrapping_*`) / `INT` with per-operation narrowing	signed wrap after every operation; real matiec boundary, chain and loop coverage
`BYTE`	`BitVec(8)`	`u8` / `BYTE`	carrier, equality, unsigned comparison and bitwise ops in PILOT; arithmetic experimental
`WORD`	`BitVec(16)`	`u16` / `WORD`	carrier, equality, unsigned comparison and bitwise ops in PILOT; arithmetic experimental
`DWORD`	`BitVec(32)`	`u32` / `DWORD`	carrier, equality, unsigned comparison and bitwise ops in PILOT; arithmetic experimental
`MATHREAL`	`Real` (exact ℝ)	none without a Representation Boundary	code emission is refused until a profile declares one (T2.1+)
`LREAL`	`Real` (exact ℝ)	`f64` / `LREAL`	under `FLOAT64_REPR`; the gap between ℝ and binary64 is the float64 range gate's obligation, not the overflow gate's
`TIME`	`Int` milliseconds, constrained `0..i64max`	`i64` ms / native `TIME`	PILOT admits literals/internal timer semantics but rejects TIME I/O and variable PT
`WSTRING[n]`	uninterpreted sort + `LEN`	`String` / `WSTRING`	experimental carrier; rejected by PILOT

INT is a bit-vector, and Rust renders explicit 16-bit wrapping operations. ST narrows after every semantic operation with INT_TO_INT; a physical FOR counter is DINT and each binder read is narrowed back to INT. Real matiec tests cover boundary wraparound, chained intermediates and the INT_MAX loop case. TIME literals are typed; a dimensionless number is rejected.

BYTE is the IEC bit-string type for status and quality codes, where individual bits carry meaning. It is an 8-bit value with its own literal syntax (BYTE#255, BYTE#16#FF) and — crucially — unsigned semantics, distinct from INT's signed ones. Both are bit-vectors, so the model dispatches on the SORT WIDTH: at width 8 a comparison is bvult/… (not signed bvslt) and division is bvudiv/bvurem, so BYTE#255 > BYTE#1 holds (255, not −1). It supports:

bitwise AND / OR / XOR / NOT — the operators are polymorphic (IEC overloads them): logical on BOOL, bitwise on BYTE, dispatched by operand type. XOR is new, and on BOOL it is exactly inequality.
8-bit wraparound arithmetic + − * / MOD in the experimental DEFAULT profile — / and MOD are unsigned; arithmetic wraps at 256 the way INT wraps at 2¹⁶. The canonical PILOT profile rejects this target-unvalidated slice.
unsigned ordering < <= > >= and equality = <>.

Mixing BYTE with INT is rejected — there are no implicit casts. Meaning lives in the model (ir.Byte* nodes, lowered via the type-aware AST path because z3.simplify rewrites 8-bit ops into Concat/Extract the INT→IR path can't map back) and flows to u8 in Rust and BYTE in ST. The 4-way equivalence (reference ≡ Z3 ≡ executed ST ≡ compiled Rust) covers it; see examples/bits/quality_byte.zqel. Note: Bit-string arithmetic examples are not yet in the matiec/OpenPLC conformance set — IEC splits bit-string and unsigned-integer arithmetic across different types, so faithful matiec emission for BYTE/WORD/DWORD arithmetic is deferred (bitwise/comparison are native). The carrier/equality/unsigned-comparison/bitwise slice has real matiec coverage. Arithmetic remains available only in the experimental DEFAULT profile and cannot receive a PILOT stamp.

`WSTRING`: a wide-string carrier (AP-30)¶

A WSTRING[n] is the IEC wide-string type for tag names and descriptions (MTP TagName/TagDescription). zqel's value is SMT-provable behaviour, and for a string that fragment is deliberately narrow but real: equality (=/<>), selection (IF-branches and wiring), passthrough, and a length bound (LEN(s) <= n). No content transformation is modelled — this is a carrier, not a string-manipulation library. In Z3 a WSTRING is an uninterpreted-sort element (two strings are equal iff the same element), LEN is an uninterpreted function into INT, and each WSTRING[n] variable carries the standing fact 0 <= LEN(v) <= n (like a type range) — which is what makes the capacity invariant provable. Literals ("SIMULATION") are distinct constants pinned to their length. Backends realise it concretely: Rust a String (cloned on read; LEN = .chars().count()), ST a native WSTRING with LEN. The 4-way equivalence carries actual strings through reference ≡ Z3 ≡ executed ST ≡ compiled Rust (the Z3 stepper maps each concrete string to its sort element and back); see examples/strings/device_tag.zqel. Deferred honestly (v1): concatenation, substring, ordering, per-character content, and matiec/OpenPLC conformance.

State kinds: inputs, registers, locals, derived¶

An output or local is defined either by priority rules (a register: it has a pre-value and is stored) or by a single name := expr; (a derived value: combinational, not stored).

In a register rule, a reference to another register is its pre-value (start-of-cycle snapshot) — this is what edge detection needs (M = previous CLK).
In a derived definition, a reference to a register is its next value (freshly computed this cycle) — this is what a counter's Q := CV >= PV needs (no one-cycle lag). References form a DAG; a combinational cycle is a compile error (CombinationalCycle).

VAR ... END_VAR declares hidden state (registers or derived) that never appears in the public interface. In the backends a register becomes a struct field / ST VAR; a derived output is computed each cycle and returned, never stored.

Composition¶

VAR r : RS; instantiates another function block. r(In := expr, ...) wires its inputs and r.Out reads its output. At compile time RS.zqel is resolved from the source file's directory (zqel/compose.py) and inlined: the instance's registers/derived become hidden locals r__<name>, its inputs are replaced by the wired expressions, and r.Out becomes a derived alias so it reads the instance's fresh output (same fresh-read semantics as :=). After flattening the program is an ordinary flat FB, so sema/SMT/verification/backends are unchanged. Recursive instantiation is rejected. This is parse → flatten → sema → …. A sub-instance keeps its own INVARIANTs (they are carried into the flattened block), and a parent may state invariants over a sub-instance output (inst.Out).

Invariants: inductive vs. consequence¶

Invariants that reference only registers are proven inductively (base case + one-step preservation). Invariants that reference a derived/output value — including inst.Out and a combinational output like a PID's clamped u — are proven as a consequence: assuming the register invariants at the current state, the derived invariant must hold there. A derived value is a function of the state, so no separate induction is needed; this needs no k-induction.

Closed-loop certificates (Lyapunov as an invariant set)¶

Stability is a property of the whole loop, so the plant is modelled as its own FB (a difference equation, e.g. a PT1). A Lyapunov argument then rides on the same one-step induction, expressed as a positively invariant sublevel set — a box |x| <= M, a single-state predicate the existing INVARIANT machinery proves (base + preservation). The plant FB carries its box invariant under an input ASSUME (e.g. |u| <= 10), and closing the loop discharges that assumption via the controller's saturation — assume-guarantee composition doing the work. zqel checks a supplied certificate; it does not discover one. Linear loops and box invariants are decidable and cheap; a nonlinear V = x² is possible but expensive. See examples/control/.

`ASSUME`: environment premises (assume-guarantee)¶

INVARIANT is a proof obligation the block must discharge; ASSUME is a hypothesis the caller must guarantee. An ASSUME may reference inputs only (the environment controls them; assuming anything about internal state would be unsound), so it is sound to add as a premise to every verification query — division safety, ambiguity, invariants, all of it. This is what lets a reusable block take its limits as parameters instead of hard-coding magic numbers: the clamped integrator takes a Limit input and states ASSUME Limit >= 0, and its anti-windup bound is then proven for every valid band. The premises must be jointly satisfiable — contradictory assumptions (which would make every property hold vacuously) are a contradictory-assume error.

An ASSUME may reference inputs only — never internal state, and never the DT clock primitive (the runtime clock is not environment-controlled, so its value must not be assumed away).

Under composition a child's ASSUME is rewritten over the wiring, then split by what the wiring makes it reference:

resolves to the parent's own inputs → it bubbles up as a parent ASSUME (the child's Limit >= 0, wired to a parent input cap, becomes cap >= 0); the obligation is pushed to the parent's caller.
fixed by the parent's internal logic (a local, register or constant) → the parent must discharge it, so it becomes a proof obligation (an INVARIANT). Wiring the assumed input to D where D := TRUE compiles; wiring it to FALSE (or a constant that violates the premise) fails, as it must.

This is a first-cut assume-guarantee contract: a premise the caller controls bubbles up; one the block establishes itself is proven on the spot. The split is syntactic — decided by which names the wired premise references — so it is sound but not complete. A premise that mixes free inputs with internal state becomes an invariant over those free inputs and is (correctly) rejected rather than decomposed. The fully general form — discharge every premise against the parent's own ASSUMEs and lift only the residual it cannot establish — is a planned refinement (AP-17 in the roadmap).

`REQUIRE`: a caller precondition on a `FUNCTION_BLOCK` (AP-27)¶

A REQUIRE on a FUNCTION_BLOCK is the same input-only, BOOL hypothesis as an ASSUME — sound to add as a premise everywhere, so the block may rely on it while proving its own INVARIANTs — but it declares a different intent and earns a different diagnosis. Where an ASSUME states what the environment happens to guarantee, a REQUIRE is a contract the caller must earn: AnaView declares REQUIRE VNormMin <= VNormMax, and a reversed band is then a compile error at the call site, not silent nonsense at runtime. INVARIANT stays the guarantee language; the three failure modes are kept distinct because they send the fix to three different people:

fb-require-violated — a sub-instance's REQUIRE, once its wiring is resolved, is not established by the parent. The blame is at the wiring; the message names the clause, the block that declared it, and the offending instance (REQUIRE (10 <= 5) of 'AnaView' (via instance 'av') is not established by the wiring).
fb-require-contradictory — the preconditions cannot all hold at once, so every guarantee would be vacuous. The block is at fault; the message lists the clauses.
a failed INVARIANT (invariant-*) — the block's own guarantee is unproven. A third, separate story from a precondition problem.

Under composition a REQUIRE travels like an ASSUME, carrying its provenance (which block declared it, through which instance it entered the parent). Whether a rewired clause is still a premise (reads only the parent's inputs — it bubbles up, so the parent's caller inherits the duty) or has become the parent's obligation (reads a local/register/constant — the parent must discharge it) is decided by what the clause reads — with the subtlety that a clause composition folded to a variable-free constant (10 <= 5 from wiring VNormMin:=10, VNormMax:=5) is fully determined inside the parent and so is an obligation, not a vacuously-input-only premise. An obligation is proven against the parent's standing premises and its register invariants (dropped if those are themselves contradictory, so a broken bubbled invariant cannot mask the real culprit). See zqel/verify.py _check_requires and examples/mtp/anaview.zqel.

Physical units (`MATHREAL<m3/h>`)¶

A numeric declaration may carry a physical unit — flow : MATHREAL<m3/h>, p : MATHREAL<bar> — on inputs, outputs and internal VAR. A dedicated pass (zqel/dimension.py) infers a dimension (an exponent vector over the seven SI base dimensions, zqel/units.py) for every expression and rejects inconsistent programs: a dimension-mismatch is a compile error in the same spirit as division-by-zero. +/-/comparison need compatible dimensions (equal, or one side dimensionless — a bare literal or an unannotated value adapts); *// add/subtract the exponent vectors; DT is time. This proves, for instance, that integrating a flow (m3/h) over DT (s) yields a volume (m3) — the two time dimensions cancel — so accumulating it into a MATHREAL<m3> type-checks while assigning a raw flow to it does not.

Units are a static contract only: the pass never mutates the AST, so the Z3 model and the generated ST/Rust are byte-identical with or without annotations (units are erased). Only the exponent vector is checked — the numeric scale of a unit (h vs s, bar vs Pa) is intentionally ignored here; choosing a better-conditioned internal representation from that information is AP-14. Raw hardware values stay dimensionless until an explicit mapping gives them meaning, mirroring how HELD made time explicit.

Representation: chosen by a profile, not inferred (AP-14 removed, #161)¶

There was an analysis here that picked a minimal fixed-point width per signal: zqel/represent.py ran Z3's Optimize over each REAL signal to certify a [min, max], and the Rust backend stored the narrowed type. It is gone.

MATHREAL is ℝ. The representation is not inferred from the program; it is declared, by a profile that states a Representation Boundary — today FLOAT64_REPR, which lowers MATHREAL to LREAL (IEEE 754 binary64, f64 in Rust). What used to be a width choice is now an assurance question, answered by the float64 range gate.

Both remnants refuse rather than answer, and deliberately so:

represent.analyze() raises NotImplementedError instead of returning [] — an empty list would read like "no signal needed one", which is the worst available answer to a question about certified ranges.
compile_source(..., analyze_representations=True) refuses first, ahead of parsing and proving, so the request never produces a seeming result: no obligation discharged, no acceptance record minted, nothing cached, on a path whose answer could only ever be empty.

Overflow safety: who decides, per type (T2.0)¶

Two gates answer "can the emitted code leave the representable range", and they are answered for different types by different machinery. Saying which is the whole content of this section, because getting it wrong reads as a gap.

`INT` / `BOOL` / `TIME` — the overflow gate decides¶

zqel/overflow.py bounds atomic inputs and registers with Z3 and propagates products and sums structurally (|a·b| ≤ |a|·|b|, side-stepping nonlinear objectives), certifying per target that every value and every arithmetic intermediate fits. Storage and +/- are 64-bit on both backends; only the *// intermediate differs (ST 64-bit, Rust 128-bit), so a block can be Rust-safe yet ST-unsafe, and the report says which.

DT is unbounded in the model — that is what makes the timing-independent proofs possible — and bounded here by a runtime-guaranteed maximum cycle time dt_max (default 1 s). DEFAULT keeps the gate advisory; PILOT runs it mandatorily and fails compilation unless both ST and Rust receive a complete safe verdict.

A clean programme says nothing at all: the gate runs, finds no finding, and the CLI prints no overflow line. Silence here is a verdict, not an omission.

`MATHREAL` / `LREAL` — the overflow gate refuses, and says so¶

It does not analyse them. overflow.py states it in its own first line — "Fixed-point overflow analysis — stubbed for T2.0" — and gate() raises for any programme carrying a MATHREAL-valued signal. There is no machine representation to fit a value into until a Representation Boundary declares one (T2.1+).

The finite-range question for those types belongs to the float64 range gate, which answers it through RangeReport.verdict and RangeReport.may_emit. The CLI says as much rather than leaving the reader to infer it:

Overflow safety: decided by the float64 range gate, not here
MATHREAL/LREAL with Float64 policy: the fixed-point gate does not apply. …

Why this section used to say something else¶

It described the interval analysis as covering REAL "per target", which was true while REAL was a fixed-point integer. T2.0 made MATHREAL mathematical ℝ, the fixed point went away with #161, and the analysis that rested on it went with it — but the prose stayed, claiming a certificate for exactly the types the gate now refuses. Measured and corrected in #288.

Timers (`HELD`)¶

HELD(cond, duration) is a declarative temporal primitive — "cond has held continuously for ≥ duration". A shared lowering pass (zqel/lower.py) assigns each syntactically distinct HELD a stable timer_id and deduplicates identical (condition, duration) pairs, so ST, Rust and Z3 all agree.

Reference semantics (Z3, absolute monotone time). A single clock now advances each cycle (now_next ≥ now). HELD exposes no elapsed-time delta of its own; the separate DT runtime primitive remains observable. Per timer, state active and started_at:

active_next     = cond
started_at_next = if cond then (if active then started_at else now) else 0
HELD            = cond and (now − started_at_next ≥ duration)

The auto-invariant active ⇒ 0 ≤ started_at ≤ now is proven and assumed during induction, so now − started_at ranges over all of [0, ∞) — the universal quantification that makes the safety proof timing-independent. HELD is disallowed inside INVARIANT — not because of the induction depth, but because the timers' own laws are not yet part of the step relation (ADR TMR-1, and TX-2.2 for why the older "that would need k-induction" reading was withdrawn) — and may not be nested in another HELD's condition.

Variable PT and ET. In the experimental DEFAULT profile, PT may be a TIME literal (2s) or a TIME variable and ELAPSED(cond, PT) exposes the elapsed continuous-true time capped at PT (IEC TON.ET). The canonical PILOT profile rejects variable PT and all scalar/array TIME inputs and outputs; it admits typed literals and internal timer/BOOL semantics only. TIME is a constrained non-negative integer in the model and i64 milliseconds in Rust; it never serves as the cycle-time delta.

Native backends. In the output formulas HELD/ELAPSED are opaque proxies (ir.Held bool, ir.Elapsed TIME); to_ir splices them back. The ST backend emits a non-retentive TON instance (IN := cond, PT := <preset>, read via .Q / .ET); the Rust backend emits a HeldTimer<I> storing started_at from a monotonic clock (InstantOps::elapsed_ms_since), driven by now passed to cycle(&mut self, now, input) -> Outputs. The monotonic runtime clock is not a process value. DEFAULT can still expose TIME-typed process I/O; PILOT cannot.

Translation validation covers BOTH halves of the induction¶

INVARIANT is proved on the model as a base case (sm.zero_init) plus an inductive step. On the generated artefacts only the STEP used to be re-proved, which leaves a gap that looks like nothing and is not: the step says "from any valid state, one cycle preserves the invariant" and never asks whether the state the generated code STARTS in is valid. An induction whose base case is unchecked on the artefact says nothing about the running program.

Measured, on both backends: an initialiser that starts the counter at 99 is caught by the base-case check and is completely invisible to the step check, which reports "INVARIANT preserved".

C (cbmc_tv.verify_init) calls matiec's real {FBN}_init__ -- not the memset the step harness uses to fabricate a start state -- on deliberately uninitialised memory, so init must establish the invariant by itself rather than inherit it from a conveniently zeroed buffer.
Rust (kani_tv.verify_init) checks Default::default(). That is where drift is likeliest: Default is derived for untimed blocks but hand-written for timed ones.

Both leave INPUTS free under the ASSUME premises, mirroring the model's base case. Checking an input only at its initialised value would prove strictly less.

A claim over the previous state (#209). In the post-state, where a claim is asserted, fb.q is already overwritten; PRE(q) means the value at the start of the scan. So the claim plan (zqel/assurance_harness.py) carries a second axis on every access — ArtifactAccess(symbol, storage, view) with the view PRE_STATE / POST_STATE / CURRENT — because one claim may read q and PRE(q) at once, and snapshot_plan(program) names the registers a step harness must save, once each, by canonical ordinal. Each harness takes those snapshots after the pre-state assumptions and before the call (let lola_tv_pre_state_k = Clone::clone(&fb.q) in Rust, __typeof__(...) in C) and reads them in the assertions; the premise reads the field before the call, the base case the default — the model's cur[q] in all three. A generated PRE-input shadow (_pre_x) is the delayed input and is read at the pre-state wherever it appears; the plan knows it from Program.pre_input_registers. A RULE has no base phase: the model proves it for every executed scan, never at the initial state.

Bounded recursion: contracts, not unfolding (`zqel/chc.py`)¶

A FUNCTION may recurse as long as a parameter decreases by a positive constant (chc.measure_of enforces it), so every call terminates. Proving a property about one used to mean unfolding the recursion — correct, but the obligation grows with the bound, and it says nothing about the bound left free.

REQUIRE / ENSURE change that. They are deliberately separate from INVARIANT because their polarity differs: REQUIRE is an assumption for the body and an obligation for the caller, ENSURE the reverse. prove_contract_modular cuts every call at that boundary — evaluate the arguments, make the callee's REQUIRE an obligation here, mint a fresh symbolic result, assume the callee's ENSURE about it.

For a recursive call the callee is the function itself, so the assumed ENSURE is exactly the induction hypothesis. The body is then acyclic: with the call reduced to a blackbox there is no recursion left to see, and what remains is a Hoare triple an SMT solver discharges directly. The measure therefore never has to be instantiated — the proof holds for it left free.

Two things this does not buy:

Contracts must be inductive. A contract can be true and still too weak to re-establish itself across the call; the unfolding path hides that by looking inside the callee, the modular one rejects it. Strengthening is real work.
Vacuous truth. An unsatisfiable REQUIRE makes REQUIRE ⇒ ENSURE hold for any postcondition whatsoever. Both proving entry points check that the assumption context is satisfiable and raise by default; treating a vacuous proof as success is the failure mode the check exists for.

When a contract fails, the report carries a counterexample in zqel's own names, not a solver dump. Z3 returns an array as a Store chain or an as-array function value — a record of how the memory was written — so the model is read out index by index over the declared bounds and reassembled into a list.

zqel/contracts.py runs this as a compile step, between flattening and inlining — a contract is a statement about a function boundary, and the inliner dissolves exactly that boundary. Failures come back as three distinct codes, because they mean three different things to whoever has to fix them: contract-ensure (the body does not keep its own promise), contract-require (a call does not establish the callee's precondition — blame at the call site), contract-vacuous.

Proofs run in bv mode, zqel's real BitVec16 semantics. The CHC path could not afford that — Spacer needed idealised Int to find invariants over array indices — but cutting the recursion removes Spacer from the picture, and plain SMT handles the bit-faithful encoding. A compiler-proved contract is therefore a claim about the code the backends emit.

When a contract fails the report is a diagnosis, not a verdict: WHICH promise broke (one query per ENSURE rather than one over their conjunction), at which line, in which state, and along which branch. The branch trace needs no instrumentation -- a zqel FUNCTION body is a pure expression tree, so with a full assignment in hand the path through it is deterministic; the compiler walks it, evaluates each condition in the model, and follows only the branch taken.

Note what is absent: there is no SSA-name mapping table, because the language never creates the problem. A FUNCTION body is one expression over its parameters -- no locals, no intermediate states -- so the parameter list IS the complete state, and the usual question of which variables to show in a counterexample does not arise.

Unary FUNCTION `PERMUTATION_OF`: the property that must not reach the solver¶

Sortedness alone leaves a hole: an isort returning all zeros is perfectly sorted. Closing it looks like one more ENSURE clause, and that is the trap. As a formula, "the result is a permutation of a" needs a witness with result[p] = a[f(p)], and indexing an array at a SYMBOLIC position is the one shape that makes the solver fall over -- a[f(p)] unrolls to a k-deep ITE chain per element, and composing two of them squares it. Neither the quantifier nor bijectivity is the cost (measured: bijectivity alone 0.04s at k=20, the value equation 7.2s; a histogram encoding is worse still). zqel/permutation.py carries the numbers.

So ENSURE PERMUTATION_OF(a) is a compiler INTRINSIC, held in its own AST field so no later phase can mistake it for a predicate and build the term it must not build. It is discharged structurally: in a comprehension the witness is written down -- element p of ARRAY(p IN 0..5 : IF p = i THEN a[j] ELSE ...) reads a at IF p = i THEN j ELSE ... -- so the compiler lifts that index off the syntax, the value equation holds by construction, and the only query left is the cheap half (Distinct plus range). Above the leaf it is closure, not proof: the array itself, an IF over permutations, or a call to something that promises one. That last rule keeps it modular -- isort uses bubble's promise without looking inside it.

Well-foundedness stays mandatory precisely here: assuming a recursive call's ENSURE is an induction hypothesis, and without a decreasing measure it is circular.

GS-v2-C adds a deliberately different binary expression, PERMUTATION_OF(result, source), for concrete fixed arrays in contracts. It is encoded as exact equality of bounded element multiplicities and is practical for small guided examples such as Sort4. The two forms must not be conflated: the unary FUNCTION postcondition remains structural and scalable, while the binary relation spends solver effort explicitly and has a correspondingly narrow fixed-array ABI. Neither form uses sum/XOR/hash fingerprints.

`EXTERN … BY <artifact>`: a contract discharged by an external proof (AP-31)¶

Some operations are proved by a tool zqel does not host (Creusot, an exhaustive enumeration), and the honest thing is to trust that proof by contract rather than re-derive it. EXTERN FUNCTION f(..) -> T ENSURE ..; BY key; declares an operation purely by its postcondition and binds it to the registry artifact key. The model then ASSUMES the ENSURE (a fresh result pinned only by the postcondition, smt._encode_extern) instead of encoding a body — which is both the generic move and the one that sidesteps the PERMUTATION_OF wall above: what an external tool already proves need not be re-encoded.

Three registry-driven layers, none of them per-operation compiler code:

Match — at compile time the declared ENSURE must equal the artifact's lola_contract and its signature, in a normalised form (RESULT, arg0, …), so the match is exact, not an undecidable implication check (verified.extern_contract). A missing artifact, wrong signature, or drifted contract is a hard error.
Model — the postcondition is assumed, so a downstream INVARIANT that follows from it is discharged, and one that asks for more than the warrant is rejected.
Backend — Rust ships the artifact verbatim with its warrant as a banner and emits the call; ST refuses when no ST artifact covers the contract (backend coverage is explicit, exactly as with a large SORT).

The trust boundary is the warrant: assuming the ENSURE makes the artifact's per-clause warrant (audited < tested < proved) the soundness, recorded in the registry, not laundered. Adding a new operation is a manifest entry + a small reference implementation (verified.REFERENCE, for the simulator/stepper) + an EXTERN declaration — no change to the parser, model, or backends. The worked case is abs_sat (saturating absolute value: zqel cannot prove >= 0 for its own -x, which overflows at -32768; the Rust saturating_abs can, warranted exhaustively). See examples/extern/saturating_abs.zqel and docs/how-to/verified-functions.md Route 3.

The large SORT is the first user. Above the native network threshold, s := SORT(a) binds the whole-array output to the sort_i16 artifact through this same mechanism: fb.extern_arrays records s -> ("sort_i16", "a"), the Rust backend ships and calls the artifact by its registry calling convention (array_in_place -> lola_sort(&mut copy)), ST refuses, and the reference simulator + Z3 stepper both realise it from verified.reference. What stays deliberately untouched is the model encoding (SortElem / _encode_sortelem, the sorted-permutation witness the model assumes) — the proof path hangs off the SortElem node, not the dispatch dict, so the migration unified dispatch/warrant/emission without disturbing the Creusot-proved core. The permutation witness is irreducible and stays; only the SORT-specific plumbing (the old sort_intrinsics dict, the hard-wired lola_sort emission) is gone.

Roadmap¶

Gated. Feature growth is frozen behind the Assurance Gates (G0–G5, see docs/review-iec61131-fb.md § Assurance Gates). The items below are after a pilot-ready core, not before it.

DINT (32-bit INT), more TON/TOF/TP timer shapes pass the G3 validation matrix (feature × backend × toolchain × runtime), not a free pretty-printer