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

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

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

LoLa's REAL 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 REAL 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 lola examples/t2/lowpass.lola
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 lola examples/t2/lowpass.lola --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 lola examples/t2/lowpass.lola --profile float64 --target st
$ python -m lola examples/t2/lowpass.lola --profile float64 --target rust

REAL 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 lola examples/t2/lowpass.lola --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 REAL/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.

Common failure modes¶

REAL/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.

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 .lola file. The lowpass.lola 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.