Code from elsewhere

17. Reusable operations: FUNCTION contracts

A FUNCTION is a compile-time-inlined, side-effect-free operation — no memory, no scan-to-scan state. You have already seen functions used as helpers inside sorting (§16). Give a function a contract and the compiler proves it before anything calls it.

Contract vocabulary:

• REQUIRE <bool>; — a precondition the caller must earn; the compiler checks it at every call site.
• ENSURE <bool>; — a postcondition the function guarantees; inside ENSURE, the function's own name stands for its return value.
• VARIANT <int>; — a termination measure for a recursive function; the compiler verifies it strictly decreases.

A precondition and a postcondition

A saturating clamp is only meaningful when the bounds are correctly ordered:

FUNCTION clamp3(x : INT, lo : INT, hi : INT) -> INT
  REQUIRE lo <= hi;
  ENSURE  clamp3 >= lo;
  ENSURE  clamp3 <= hi;
  IF x < lo THEN lo ELSE IF x > hi THEN hi ELSE x
END_FUNCTION

The compiler proves the body establishes both ENSUREs given the REQUIRE. The call site must earn that precondition:

FUNCTION_BLOCK Limiter
VAR_INPUT v : INT; a : INT; b : INT; END_VAR
VAR_OUTPUT y : INT; END_VAR
IMPLEMENTATION
    y := clamp3(v, a, b);
    ASSUME a <= b;  // earns clamp3's REQUIRE at this call site
    INVARIANT y >= a AND y <= b;  // PROVEN from clamp3's ENSURE
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Drop the ASSUME and the block no longer compiles — the precondition is not earned. The error is blamed at the call site (contract-require), not inside clamp3 — so you know immediately whether the function or its caller is at fault.

Watch for INT overflow. INT is 16-bit and wraps. A contract like ENSURE f >= a over a + n is only provable when a + n cannot overflow. Bound inputs with REQUIRE, or state an overflow-safe contract.

Recursion: VARIANT makes termination explicit and checked

Recursion is allowed only when a strictly decreasing measure makes it terminate. VARIANT names that measure; the compiler verifies it:

FUNCTION countdown(n : INT) -> INT
  REQUIRE n >= 0;
  ENSURE  countdown = 0;
  VARIANT n;
  IF n <= 0 THEN 0 ELSE countdown(n - 1)
END_FUNCTION

VARIANT n declares that every recursive call decreases n; a measure that does not strictly decrease is a hard error. The real worked example is examples/algorithms/insertion_sort.zqel: bubble and isort both carry VARIANT k, prove sortedness, and promise ENSURE PERMUTATION_OF(a).

Named predicates

A FUNCTION -> BOOL is a named predicate, usable in any INVARIANT, ASSUME, REQUIRE, or ENSURE:

FUNCTION nonneg(a : ARRAY[0..3] OF INT) -> BOOL
  ALL(i IN 0..3 : a[i] >= 0)
END_FUNCTION

FUNCTION_BLOCK Gate
VAR_INPUT xs : ARRAY[0..3] OF INT; END_VAR
VAR_OUTPUT ok : BOOL; END_VAR
IMPLEMENTATION
    ok := nonneg(xs);
    ASSUME ALL(i IN 0..3 : xs[i] >= 0);
    INVARIANT ok = TRUE;  // PROVEN via the inlined predicate
END_IMPLEMENTATION
END_FUNCTION_BLOCK

ENSURE PERMUTATION_OF(a) is the one intrinsic postcondition: it says the result is a rearrangement of array parameter a. It is proved structurally (the index-witness approach from §16), not as an SMT formula — because a symbolic permutation predicate sends the solver into an explosion; see insertion_sort.zqel.

---

18. Calling externally verified code: EXTERN … BY

Some operations cannot be proved inside zqel, but can be verified by an external tool. EXTERN FUNCTION … BY <artifact> lets that external proof enter the model.

The motivating example: saturating absolute value

Consider absolute value for INT. The obvious attempt fails:

FUNCTION abs_attempt(x : INT) -> INT
  ENSURE abs_attempt >= 0;  // REJECTED by the compiler
  IF x < 0 THEN -x ELSE x
END_FUNCTION

The compiler is right. INT is 16-bit; -(-32768) overflows and wraps to -32768, a negative number. The body does not establish >= 0 for every input. No pure zqel proof exists.

The registry ships a Rust implementation (abs_sat_i16) that saturates the one overflow case: abs_sat(-32768) = 32767. It is proved exhaustively over all 65536 i16 inputs by an external harness. EXTERN lets that warrant flow in:

EXTERN FUNCTION abs_sat(x : INT) -> INT
  ENSURE abs_sat >= 0;
  BY abs_sat_i16;

FUNCTION_BLOCK SaturatingAbs
VAR_INPUT  v : INT; END_VAR
VAR_OUTPUT y : INT; END_VAR
IMPLEMENTATION
    y := abs_sat(v);
    INVARIANT y >= 0;  // PROVEN by assuming abs_sat_i16's warrant
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The BY abs_sat_i16 clause names a specific artifact. It is optional: without it, the compiler selects an implementation automatically from all registered artifacts whose contract matches the ENSURE clause. BY is a selection hint — the contract always holds regardless of which artifact is chosen.

How it works:

• The model ASSUMEs abs_sat >= 0 at every call site — justified by the artifact's warrant, not re-derived by Z3. An INVARIANT y >= 5 would be rejected because the warrant is >= 0 and no wider.
• The Rust backend ships the abs_sat_i16 artifact verbatim and emits the call. The ST backend reads its own ST artifact from the same registry entry.

The trust boundary — explicit and traced

EXTERN is honest by construction. The compiler labels every INVARIANT that rests on an EXTERN contract with the artifact and warrant it inherits:

INVARIANT y >= 0 : assumed via EXTERN abs_sat_i16 {rust: proved, st: audited}

An invariant that reads no EXTERN output is a pure zqel proof and carries no such label. audited and proved are distinct; a [!] flag appears on any invariant that rests on a less-than-proved warrant. The PILOT profile (minimum_extern_warrant = "proved") enforces this at compile time and refuses to build if the weakest attained warrant falls below proved across the required targets.

A second operation: sat_add

A second artifact — sat_add_i16, a saturating signed addition — was added to the registry by writing only a manifest entry and a reference implementation; the parser, model, and backends were not touched. Its contract is multi-argument and references the inputs:

EXTERN FUNCTION sat_add(a : INT, b : INT) -> INT
  ENSURE NOT (a >= 0 AND b >= 0) OR sat_add >= 0;
  ENSURE NOT (a <= 0 AND b <= 0) OR sat_add <= 0;
  BY sat_add_i16;

With ASSUME x >= 0; ASSUME y >= 0;, the invariant s >= 0 on s := sat_add(x, y) is discharged by threading the ASSUMEs into the assumed postcondition. This is a guarantee zqel's own wrapping + cannot make: 20000 + 20000 overflows and becomes a negative number; the saturating version clamps it to 32767.

The pattern generalises: a new externally-verified operation needs a reference implementation, a VerificationRecipe, and an EXTERN declaration — no compiler code, no parser change. The zqel extern toolchain (init / verify / register / check) manages the registry side; see how-to/verified-functions.md if you want to add one. For the worked examples as zqel programs, see examples/extern/.

---

19. Where the representation comes from (advanced)

You do not infer the representation; you declare it. A MATHREAL is ℝ, and ℝ has no width — so a block with MATHREAL signals proves fine and refuses to emit code until a profile states a Representation Boundary:

$ python -m zqel examples/analog/integrator_bounded.zqel --profile float64
Compilation succeeded: IntegratorBounded
  4 output properties verified
  Overflow safety: decided by the float64 range gate, not here
    conditional on the deployment holding the cycle time to 1s — REQUIRED, not enforced (#168)
  MATHREAL/LREAL with Float64 policy: the fixed-point gate does not apply. …

--profile float64 is that declaration: it lowers MATHREAL to LREAL, IEEE 754 binary64. What the bounds you stated still buy you is the assurance — the float64 range gate uses your invariants, ASSUMEs and CLAMPs to decide whether every value stays inside the finite binary64 range, and refuses the emission if it cannot.

Earlier versions of zqel did something else here: they ran Z3 to certify a range per signal and picked the smallest fixed-point integer width that held it. That analysis was removed with #161, and it is not coming back — the width is a declared choice now, bounded by an assurance envelope, not an inferred one.

When the search space explodes — and what to do about it

Formal methods are not magic. Some formulations are easy to prove; others are logically equivalent but make the search blow up. In practice, three patterns are the usual culprits:

• Huge symmetric choice spaces. “Find me some arrangement” is much harder than “here is the construction; prove it works”. That is why SORT and permutation(...) are compiler-guided realisations rather than open-ended synthesis problems.
• Symbolic indexing and nested case splits. Expressions like a[f(i)] or deeply nested conditionals generate large proof terms quickly; they ask the solver to reason about many possible data routes at once.
• Unbounded or weakly bounded arithmetic. A proof gets much easier once the block states its operating envelope (ASSUME, CLAMP, units, invariants) instead of leaving every signal mathematically unconstrained.

What helps in practice:

• Write the operating envelope down. Bounds on inputs, gains, limits, pressures, temperatures, selector ranges. They are not “extra decoration”; they are what turns an open world into an engineering problem.
• Prefer structured declarative operators over hand-coded search. ALL, ANY, COUNT, SUM, MIN, MAX, ARRAY(...), SORT, and RULE give the compiler a known semantic shape. An ad-hoc imperative encoding of the same idea is often much harder to analyse.
• Separate safety from optimisation. First prove the block cannot do the wrong thing; only then worry about whether it does the most useful thing. If you mix both at once, the proof problem becomes larger and the diagnosis worse.
• Strengthen the spec when the counterexample is “technically legal but absurd”. That is not the solver being annoying; it is the tool telling you what your current words still permit.

The practical rule is simple:

Do not ask the solver to guess structure you could have stated directly.

The better you expose bounds, intent and structure in the source, the smaller the search space and the better the diagnostics.

---

19b. Guided synthesis: when the solver needs a hand

Some blocks — schedulers, arbiters, ranking algorithms — have the right kind of specification (RULE constraints) but a search space too large for the bounded synthesiser to explore directly. The answer is guided synthesis: you supply a candidate implementation and a bounded model checker proves it correct.

Here is a 2-pump scheduler whose RULE ties the running pump to accumulated hours:

FUNCTION_BLOCK Relay
VAR_INPUT
    demand : INT;
    ok     : ARRAY[0..1] OF BOOL;
    hours  : ARRAY[0..1] OF DINT;
END_VAR
VAR_OUTPUT
    run : ARRAY[0..1] OF BOOL;
END_VAR
IMPLEMENTATION
    ASSUME demand >= 0;
    ASSUME demand <= 1;
    ASSUME COUNT(i IN 0..1 : ok[i]) >= demand;
    RULE COUNT(i IN 0..1 : run[i]) = demand;
    RULE ALL(i IN 0..1 : (NOT run[i]) OR ok[i]);
    RULE ALL(i IN 0..1 : ALL(j IN 0..1 :
        (NOT (run[i] AND ok[j] AND (NOT run[j]))) OR (hours[i] <= hours[j])
    ));
END_IMPLEMENTATION
END_FUNCTION_BLOCK

This block has synthesis targets (run[0], run[1]) but no := definitions. The bounded synthesiser might not find candidates within its node budget when the third rule (the hours-ranking condition) couples both outputs.

Step 1 — Build the proof request:

zqel guided relay.zqel --out build/proof/

This writes proof_request.json and the Kani harness skeleton candidate.creusot.rs.

Step 2 — Propose a candidate (LLM-assisted or hand-written):

zqel guided --agent claude relay.zqel --out build/proof/

The LLM receives the proof request (inputs, outputs, ASSUME and RULE texts) and writes a Rust candidate body. An example correct body for the 2-pump relay:

let run0 = input.demand >= 1 && input.ok[0]
    && (!input.ok[1] || input.hours[0] <= input.hours[1]);
let run1 = input.demand >= 1 && input.ok[1]
    && (!input.ok[0] || input.hours[1] < input.hours[0]);
Relay { run: [run0, run1] }

Note the asymmetry: <= for index 0 (wins ties), < for index 1 (loses ties). This is not decoration — it is what makes the scheduling deterministic.

Step 3 — Accept (prove) the candidate:

zqel guided accept relay.zqel \
    --candidate build/proof/candidate_response.json \
    --backend kani --out build/proof/

Kani runs symbolic exhaustion over all input combinations. If it reports VERIFICATION SUCCESSFUL, it writes acceptance.json — a GuidedSynthesisWarrant. If it finds a counterexample, you fix the candidate and retry.

Step 4 — Compile with the warrant:

import json
from zqel import compiler
from zqel.guided_synthesis import make_guided_synthesis_warrant

warrant = make_guided_synthesis_warrant(json.loads(open("build/proof/acceptance.json").read()))
comp = compiler.compile_source(source, guided_synthesis_warrants={"Relay": warrant})
assert comp.report.ok

The compiler checks that the warrant's declaration_sha256 matches the current source contract, skips CEGIS synthesis, and records the warrant in program.assurance.guided_synthesis_warrants.

The connection to EXTERN

This is the same trust structure as EXTERN, applied to a full block rather than a single function:

EXTERN	Guided synthesis
ENSURE + artifact	RULE + acceptance.json
Compiler ASSUMEs the ENSURE	Warrant discharges the RULE proof goal
ExternalImplementationWarrant	GuidedSynthesisWarrant

The difference is that EXTERN applies to individual function calls (one result value), while guided synthesis covers an entire block's output set with a joint proof.

→ Full workflow details: How-to: Realize a contract\ → Trust model: Concept: Guided synthesis and EXTERN

19c. Real arithmetic: where synthesis meets numerics

Everything above stayed in BOOL/INT territory, where a RULE is a finite-domain statement and any of the provers decides it exactly. RULEs over LREAL are different: they are statements about exact real numbers, proved by Z3 over ℝ — while the running code computes in binary64. Those are two different claims, and zqel keeps them separate on purpose: the ℝ proof says the algorithm is right, and a separately proved error envelope (|machine − exact| ≤ ε, via the Gappa prover) says how far the binary64 execution can drift from it. This is why the original free-form Rust/Kani and ST/CBMC guided paths refuse LREAL outputs: a model checker running the candidate in f64 would prove a subtly different theorem than the RULE states. GS-v2-N instead accepts a narrow zqel candidate, proves its RULE over exact reals, emits both machine backends from that same compilation, and accepts only if the Static Numerical Core publishes a proved binary64 error envelope for every numeric output. Its first slice is intentionally combinational: state, PRE, DT, timers, calls, arrays, wiring, templates, and continuous references remain excluded.

The showcase for all of this at once is the Levenberg–Marquardt example: twelve RULE-only LREAL blocks synthesized from one-line contracts (Gram matrix, gradient, damping, updates), one verify-only solver whose Cramer RULEs Z3 proves under det > 0, a composed LM_Step block whose positive-definiteness precondition the compiler discharges symbolically from λ ≥ 1, a runnable PROGRAM fitting a calibration curve live on the Rust runtime — and an end-to-end proved bound |x̂_new − x_new| ≤ 1.02e-12 across all four block boundaries.

→ Worked vertical: examples/algorithms/lm_step/\ → Concept: Synthesis — from RULE contract to proven implementation

---

20. Using the compiler

From a source checkout, invoke as python -m zqel. The four modes you have seen in this guide:

python -m zqel FILE.zqel                     # verify only (default): prove all properties
python -m zqel FILE.zqel --target st         # emit IEC 61131-3 Structured Text
python -m zqel FILE.zqel --target rust       # emit Rust
python -m zqel FILE.zqel --profile float64   # enable MATHREAL → Float64 (required for LREAL code)
python -m zqel FILE.zqel --strict            # treat warnings as errors (CI mode)

The golden rule: verification always runs first, and the backends only ever see a program that passed. ST and Rust are generated from the same proven model, so they agree by construction.

For the full option table — --project, --profile pilot, zqel extern, exit codes, and output formats — see the CLI Reference.

---