Architecture

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

Scope of a LoLa claim (read this first). LoLa 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 REAL 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, lola/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	lola/lexer.py	source → tokens
1 Parse	lola/parser.py	tokens → AST (syntax only)
2 Sema	lola/sema.py	names, types, symbol table
2b Dim	lola/dimension.py	physical-unit check (erased after)
3 SMT	lola/smt.py	AST → canonical Z3 model (the meaning)
4 Verify	lola/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	lola/represent.py	Z3-certified REAL ranges → width (opt-in)
5c Ovfl	lola/overflow.py	per-target REAL overflow safety (mandatory/hard in PILOT; advisory in DEFAULT)
5d Plan	lola/emission.py	one integrity-checked, backend-neutral emission schedule
6 Emit	lola/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 REAL, 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.

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

LoLa	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
REAL	Int fixed-point ×1000	i64 / LINT	PILOT requires a hard ST+Rust overflow verdict for every executable sink
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.lola. 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). LoLa'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.lola. 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.lola is resolved from the source file's directory (lola/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. LoLa 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 lola/verify.py _check_requires and examples/mtp/anaview.lola.

Physical units (REAL<m3/h>)

A numeric declaration may carry a physical unit — flow : REAL<m3/h>, p : REAL<bar> — on inputs, outputs and internal VAR. A dedicated pass (lola/dimension.py) infers a dimension (an exponent vector over the seven SI base dimensions, lola/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 REAL<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 analysis (REAL ranges → width)

Because units are static, the compiler is free to choose each signal's numeric representation — provided it can prove the choice safe. The first step of that is a certified range analysis (lola/represent.py): for every REAL signal it runs Z3's Optimize over the next/fresh value under the register invariants, ASSUME premises and timer facts, obtaining a certified [min, max], and from that picks the minimal signed fixed-point width (i16 / i32 / i64) that holds it without overflow at the scale. A signal whose range cannot be bounded (e.g. a free accumulator) falls back to >i64. A tighter ASSUME/CLAMP yields a narrower type — the same value expression can compile to different widths depending on the stated bounds.

This is a proof, not a rewrite: the model is untouched, so it changes no semantics. It is opt-in (compile_source(..., analyze_representations=True), and the CLI's default check target) because the Optimize queries cost time; the result rides on Program.representations.

When the analysis has run, the Rust backend emits the chosen width: a REAL register/output certified to a narrow range is stored as i16/i32 instead of i64. Fixed-point arithmetic still runs in i64 (with the usual i128 multiply intermediate), so a narrowed field is widened with as i64 on read and narrowed with as i16/as i32 on store — both exact because the certified range proves the stored value fits. Absent the analysis every REAL stays i64, so the default output is byte-for-byte unchanged; when it runs, the narrowed build is validated against the reference by the same equivalence tests. (Per-target float/fixed choice and unit-scale normalisation remain future work.)

Overflow safety (REAL fits the target width)

There is a subtlety the equivalence tests alone cannot see: the Z3 model, the reference simulator and the ST interpreter all compute REAL in unbounded integers, while the compiled backends are finite (ST stores and multiplies in 64-bit LINT; Rust stores in i64 but multiplies through a 128-bit intermediate). So the emitted code can overflow where the model cannot — a blind spot, and a crack in “the model is the single source of truth”. A target analysis (lola/overflow.py) closes it: by interval analysis — bounding only atomic inputs/registers with Z3 (reliable, linear) and propagating products/sums structurally (|a·b| ≤ |a|·|b|, side-stepping the nonlinear objectives Optimize cannot maximise) — it certifies, per target, that every value and every arithmetic intermediate fits that target's width under the ASSUMEs and invariants. Storage and +/- are 64-bit on both; 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 (for the timing-independent safety proofs) but bounded here by a runtime-guaranteed maximum cycle time dt_max (default 1 s). DEFAULT keeps this advisory for backwards compatibility; PILOT runs it mandatorily and fails compilation unless both ST and Rust receive a complete safe verdict. The hard walk covers every executable sink, including BOOL results, rule guards, timer conditions, literals, negation, CLAMP and every prefix of a REAL SUM accumulator. An unbounded input is therefore honestly rejected under PILOT until an ASSUME or invariant supplies a sufficient bound.

REAL in Structured Text (fixed-point LINT)

The ST backend renders REAL as fixed-point in LINT — the same integer semantics as the Z3 model and Rust, not IEC floating-point (float would diverge from the fixed-point proof and break the single-source-of-truth guarantee). A REAL is a LINT scaled by real.SCALE; * and / rescale ((a*b)/1000, (a*1000)/b) using IEC integer division, which truncates toward zero exactly like the model's trunc_div; CLAMP is emitted as the canonical total nested choice (x < lo ? lo : x > hi ? hi : x) rather than target-dependent LIMIT; and DT becomes a runtime-supplied cycle_dt : LINT input (fixed-point elapsed seconds — the ST analogue of Rust's now parameter). This extends the equivalence contract to a four-way check for analog blocks: reference ≡ Z3 ≡ compiled Rust ≡ executed ST (a small independent ST interpreter runs the emitted code and its trace is diffed). The one caveat is width: the LINT multiply intermediate is 64-bit where Rust uses 128-bit, so extreme magnitudes could overflow it — irrelevant for range-certified blocks.

IEC-conformant identifiers. IEC 61131-3 is case-insensitive, reserves its keywords and standard functions/FBs, and forbids consecutive underscores. So the ST backend passes every emitted identifier through st_ident: it collapses the __ that flattening uses as a separator (inst__field → inst_field) and renames any name that then collides case-insensitively with a reserved word, standard function, or standard/extended FB (Limit → Limit_v, PID → PID_v). Non-colliding names are untouched, so ordinary output is unchanged. Before the EmissionPlan, the compiler also validates the complete source/generated namespace against ST case/underscore normalization, Rust snake-case/reserved names, and generated next-state, timer, clock and EXTERN infrastructure. A collision therefore fails before either backend can reinterpret it.

Real-toolchain conformance. Beyond the in-repo interpreter, an opt-in harness (tests/openplc.py, conformance/) compiles the emitted ST with matiec — the ST→C compiler OpenPLC uses — and runs the generated C, diffing its trace against the reference. This is a genuinely independent runtime, and it is what surfaced the identifier rules above — and one more subtlety: IEC's SEL is eager (both arms are evaluated), unlike the Z3 If, so a division guarded by an enclosing IF is still computed on the dead path and traps (SIGFPE) on x86 when the divisor is 0. The ST backend therefore guards every emitted divisor (/ SEL(d = 0, d, 1)); the value is discarded by the guard on that path, so it is semantically transparent. It runs in CI (a job builds matiec) and in a Docker image; analog, control and discrete examples execute bit-for-bit identically for the documented slices. Timer blocks are covered too: the harness drives matiec's native TON by setting the runtime clock __CURRENT_TIME from the now sequence each scan, so HELD/TON behaviour (including reset and independent timers) matches the reference. Native TIME outputs (TON.ET, a timespec struct) are not yet read back; this is a DEFAULT/G3 expansion, because PILOT rejects TIME inputs and outputs throughout the composition closure.

Translation validation (CBMC). Executing the generated code tests that the codegen preserved the semantics; tests/cbmc_tv.py proves it. It compiles the emitted ST with matiec and runs CBMC on the resulting C to re-establish, by an independent verifier, the same INVARIANT LoLa proved on the model — as a single one-step-induction check: a nondeterministic start state that satisfies the register invariants and ASSUMEs, one FB-body call, assert the invariants on the new state (a codegen bug then yields a counterexample). Because the body is loop-free this is a complete, bit-exact check. Every example's invariant is proved on the C in about a second — the fixed-point REAL blocks included, so the heavier deductive route (Frama-C/Why3) is not needed for arithmetic scale yet. As a bonus, CBMC's built-in signed-overflow check independently flags the same int64 overflow as lola/overflow.py (the PID's unbounded gains), one tool confirming the other on the real artifact.

Timers (HELD)

HELD(cond, duration) is a declarative temporal primitive — "cond has held continuously for ≥ duration". A shared lowering pass (lola/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 (that would need k-induction), 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.

Bounded recursion: contracts, not unfolding (lola/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 LoLa'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.

lola/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, LoLa'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 LoLa 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). lola/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 LoLa 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: LoLa cannot prove >= 0 for its own -x, which overflows at -32768; the Rust saturating_abs can, warranted exhaustively). See examples/extern/saturating_abs.lola and docs/guide-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