How to configure MATHREAL representation and run the numerical assurance chain¶

Audience: engineer using MATHREAL/LREAL variables and wanting to emit runnable code or obtain a quantitative error bound.\ Prerequisites: familiarity with zqel's MATHREAL, INVARIANT, and ASSUME as shown in the Introduction by Example §8.\ Language Reference: §13 MATHREAL semantics, §17 Profiles.\ CLI Reference: --project, --profile.

The problem: MATHREAL is ℝ, not a machine type¶

zqel's MATHREAL is mathematical ℝ. A proof that INVARIANT s >= -1.0 holds is a theorem about real numbers, valid for any value the inputs can take. This is precise and strong — but it says nothing about IEEE 754.

To run a MATHREAL programme you must choose a Representation Boundary: the machine arithmetic that will approximate ℝ. Without one, the compiler verifies the programme but refuses to emit code:

$ python -m zqel examples/t2/lowpass.zqel
verification failed:
  [overflow] REAL/LREAL overflow gate (default): REAL/LREAL programs require a
  Representation Boundary before overflow analysis (T2.1+). ...

The mathematical proof succeeded; only code emission is gated.

Step 1 — verify the mathematical programme¶

Even before choosing a representation, verify that the programme is mathematically correct. This is the cheapest check and the foundation everything else rests on:

$ python -m zqel examples/t2/lowpass.zqel --profile float64
Compilation succeeded: LowpassFilter
G2: unrated
Claims: 2
REAL overflow-safety (DT <= 1s): ST ✓, Rust ✓

--profile float64 enables Float64 representation and lifts the overflow gate. The programme passes all claims over ℝ and passes the overflow analysis for the Float64 representation.

Step 2 — emit code¶

With Float64 representation active, both backends are available:

$ python -m zqel examples/t2/lowpass.zqel --profile float64 --target st
$ python -m zqel examples/t2/lowpass.zqel --profile float64 --target rust

MATHREAL lowers to LREAL in Structured Text and f64 in Rust. The proven invariants appear as comments in the generated output; DT becomes the cycle_dt runtime argument; CLAMP becomes nested SEL calls.

Both targets are generated from the same proven ℝ model, so they compute the same mathematical function.

Step 3 — quantify the error with a project file¶

--profile float64 is a shorthand for code emission. For a quantitative error bound — how far can the machine result deviate from the ℝ result? — you need a project configuration file that declares the deployment context.

The canonical example is examples/t2/lowpass.toml:

[representation]
real = "float64"

[sampling.s]
period = "10ms"
method = "forward-euler"
jitter = "1ms"
horizon = 100

[sampling.s.input_derivatives]
u = "0"

[physical_errors]
u = "1/100"

[rewrite]
policy = "min_abs_roundoff"

Run with the project file:

$ python -m zqel examples/t2/lowpass.zqel --project examples/t2/lowpass.toml

The compiler prints the Engineering Error Report — a bound on how far the deployed implementation can deviate from the exact mathematical model across an N-step trajectory:

── Engineering Error Report (s) ─────────────────────────────
Per-step error budget:
  Machine roundoff ε_m           0.000000  [proved]
  Physical input  ε_p            0.000200  [proved-under-assumptions]
  Discretization  ε_d            0.000495  [proved-under-assumptions]
  Jitter          ε_j            0.004090  [proved-under-assumptions]
  ─────────────────────────────────────────────────────────
  Combined ε_combined             0.004785

Trajectory bound:
  E_N (100 steps)  : 0.222600
  E_∞              : 0.265826

E_∞ is the steady-state bound on |s_machine − s_exact| under the declared assumptions. Items marked proved-under-assumptions depend on the declared [physical_errors], [sampling.*], and [jitter] values — these are engineering assumptions about the deployment, not mathematical proofs.

What each TOML field contributes¶

Field	What it declares	Assurance effect
`[representation] real`	Machine arithmetic for MATHREAL/LREAL	assumed gap between ℝ and Float64
`[sampling.*] period`	Nominal scan period	assumed deployment fact
`[sampling.*] method`	Discretisation method	assumed engineering choice
`[sampling.*] jitter`	Timing uncertainty bound	assumed deployment fact
`[sampling.*] input_derivatives]`	Rate of change of inputs between samples	assumed physical fact
`[physical_errors]`	Sensor/actuator error bound	assumed sensor specification
`[rewrite] policy`	Algebraic expression selection	codegen choice; no assurance effect

Every field introducing an assumption is labelled in the Engineering Error Report's "Declared assumptions" section. The overall status is the weakest warrant in the chain: proved < audited < proved-under-assumptions < assumed.

For the full field reference, see the Project Configuration Reference.

What the boundary obliges you to prove¶

Choosing Float64 says the machine values are IEEE 754 binary64, and that carries an obligation the exact-ℝ semantics does not have: every value the programme actually evaluates has to fit. In ℝ there is no such thing as overflow, so this obligation does not exist under the default profile and is not imposed there.

The compiler discharges it in two halves, because a register carries state across cycles and a single-step argument cannot bound an accumulator:


base	the power-up state is finite
step	the profile premise, the proved invariants and the inductive hypothesis together bound every evaluated intermediate — and the next state

Only proved invariants may be premises. An invariant that failed or came back unknown would be assuming the conclusion, and a clamped integrator would then be indistinguishable from an unbounded one.

The verdict has four states, not two:

Verdict	Emits?	Grounds acceptance?
`PROVED`	yes	yes
`CONDITIONAL`	yes	no
`VIOLATED`	no	no
`UNDECIDED`	no	no

CONDITIONAL is the common one, and it is not a weaker PROVED. It means the obligation discharged under declared assumptions that nothing enforces — every ASSUME the block makes, and every ASSUME it inherited through composition. Those are listed with the block that declared them and the instance path they arrived through, and they are exactly what a deployment has to honour for the verdict to mean anything. See Language Reference §17 and issue #168 for why a condition that is printed but enforced by nothing is a hazard rather than a reassurance.

If the block reads DT, the proof also leans on the profile's scan-time window — 0 <= DT <= dt_max, or with a declared floor DT = 0 OR dt_min <= DT <= dt_max. That window is enforced by nothing, so it is listed as an obligation of its own and the stamp prints the window itself rather than a count: a reader has to be able to check it against the PLC the code will run on. A block that never reads DT carries no such condition.

VIOLATED and UNDECIDED both refuse, and they refuse before any backend runs, so a refused programme leaves no artefact behind. They keep separate codes on purpose: float64-range-violated means a counterexample exists, and float64-range-undecided means nobody found out. Those are different facts, and only the first one is about your programme.

Common failure modes¶

MATHREAL/LREAL programs require a Representation Boundary
Add --profile float64 or [representation] real = "float64" in a project file.

INVARIANT fails with --profile float64 but not before
The mathematical proof passed, but overflow analysis found a counterexample. The programme is correct over ℝ but not over Float64. Common causes: unbounded accumulation without a CLAMP, or arithmetic that goes outside the safe Float64 range before CLAMP takes effect. Add tighter ASSUMEs on inputs or restructure the update rule.

float64-range-violated on a block that looks bounded
Three causes account for nearly all of them.

A register inherits no bound. The inductive hypothesis says only finite; the tighter bound has to stand as an INVARIANT and be proved. An accumulator that is "obviously" bounded by how it is used is not bounded by anything the compiler can see. Compare examples/analog/integrator.zqel with integrator_bounded.zqel.

CLAMP bounds its result, not its argument. In u := CLAMP(-4.0 * x, -10.0, 10.0) the product is evaluated before the clamp sees it, so an unconstrained x leaves the range on the way in. examples/control/PController.zqel is the smallest illustration.

A quotient by elapsed time needs a floor, not just <> 0. IF DT <> 0.0 proves definedness, not magnitude: a quotient by an arbitrarily small DT leaves binary64 however tightly its numerator is bounded. FLOAT64_REPR deliberately leaves dt_min_ns unset, because a minimum cycle time is not a property of the language. A profile that wants it discharged declares one — see profiles.FLOAT64_DT_MIN_1US, under which pid_bounded.zqel and differentiator_bounded.zqel do discharge. Declaring a floor does not make the quotient safe; it makes the condition explicit and visible as a deployment obligation.

float64-range-undecided
Not a softer violated. The solver did not decide, or the node is not encodable. "Nobody could tell" and "it is safe" are different sentences, and a tool that says the second while meaning the first is the defect this state exists to prevent.

Engineering Error Report shows E_∞ is large
The dominant term is usually jitter (high ε_j) or a weak physical error spec (high ε_p). To tighten: reduce jitter, reduce [physical_errors] values (if your hardware supports it), or add a CONTINUOUS_REFERENCE block to let the ODE-based discretisation analysis produce tighter ε_d.

CONTINUOUS_REFERENCE block required for sampling analysis
Some numerical assurance steps require a DER(<var>) = <expr>; ODE declaration in the .zqel file. The lowpass.zqel example shows the pattern. The ODE does not affect the programme's execution semantics; it is engineering knowledge used only by the numerical assurance analysis.