Skip to content

How to diagnose and fix proof failures

Audience: developer reading a LoLa compiler error message and wanting to fix it.\ Prerequisites: familiarity with INVARIANT, ASSUME, rules, and priorities from the Introduction by Example.\ Language Reference: §16 Proof obligations, §15 Dynamic/synchronous semantics.

Every proof failure produces a stable diagnostic identifier and a concrete counterexample. This guide walks through the five most common categories.

Quick reference

Diagnostic What it means First thing to check
invariant-init Invariant false at power-on Initial values; derived outputs not yet evaluated
invariant-step Inductive step fails Rules missing a saturation/bound case; INT wrap
division-by-zero Divisor may be zero Add IF b <> 0 THEN … ELSE … or ASSUME b <> 0
array-index-out-of-bounds Dynamic index not proven in range Add ASSUME sel >= lo; ASSUME sel <= hi
ambiguous-priority Two equal-priority rules can conflict Assign different priorities or make guards exclusive
contract-require Caller does not earn callee's REQUIRE Add ASSUME at the call site
contract-ensure Function body does not establish ENSURE Check INT overflow; tighten the body

1. invariant-init — the initial state violates the invariant

The compiler checks that every INVARIANT holds before the first scan, when all registers are at their power-on defaults (0 / FALSE).

A block that fails it:

FUNCTION_BLOCK Counter
VAR_INPUT
    Reset : BOOL;
    Count : BOOL;
END_VAR
VAR_OUTPUT
    Value : INT;
END_VAR
IMPLEMENTATION
    Value:
        SET 0         WHEN Reset       PRIO 30;
        HOLD          WHEN Value >= 10 PRIO 20;
        SET Value + 1 WHEN Count       PRIO 10;
        HOLD OTHERWISE;
    INVARIANT Value >= 1;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The error:

verification failed:
  [invariant-init] invariant does not hold in the power-up state,
  before the first scan has run (every output and local at its default):
  (Value >= 1)
      counterexample: Count=0, Reset=0, Value=0

Common cause: the invariant requires a minimum value that 0 does not satisfy.

Fix options:

  1. Weaken the invariant: Value >= 0 is true at power-on; Value >= 1 is not.
  2. Or add an initialisation rule that fires once to set the minimum: 
    Value:
    SET 1 WHEN NOT Initialized PRIO 30;
    ...

Important caveat — derived outputs. Outputs defined by := are not evaluated before the initial-state check. Only register values (at their defaults) are visible. So INVARIANT y >= lo where y := clamp(x, lo, hi) will fail at init if lo is not 0 — y is undefined at that moment. Use a register rule for y or add an initial-state assumption:

ASSUME lo <= 0;   -- so clamp at y=0 satisfies y >= lo

See Language Reference §16.1 for the exact init-check semantics.

2. invariant-step — the inductive step fails (the most common failure)

The compiler checks that if an invariant holds at the start of a scan, it also holds at the end. A failure means there exists a start-state that the invariant holds in, but after one update it no longer holds.

Typical error:

verification failed:
  [invariant-step] invariant can be violated after one cycle: (Value <= 10)
      counterexample: Count=1, Value=10

Reading the counterexample: "Start a scan with Value = 10 (invariant holds) and Count = 1. After one update, Value becomes 11, so Value <= 10 is now false."

Common causes:

Missing saturation rule

Value:
    SET Value + 1 WHEN Count PRIO 10;   -- no upper bound!
    HOLD OTHERWISE;
INVARIANT Value <= 10;

Fix: add a saturate-at-limit rule at higher priority:

Value:
    HOLD          WHEN Value >= 10 PRIO 20;   -- freeze at the limit
    SET Value + 1 WHEN Count       PRIO 10;
    HOLD OTHERWISE;

INT overflow (the silent bug)

INT is 16-bit and wraps: 32767 + 1 = -32768. An invariant like Value >= 0 on a counter fails at Value = 32767. The counterexample will show exactly this:

counterexample: Count=1, Value=32767

Fix: bound the counter before it reaches the overflow point:

HOLD WHEN Value >= MAX_SAFE PRIO 20;

Or widen the type: DINT (32-bit) or LINT (64-bit) push the wrap point much further. See Language Reference §5 for integer widths.

Missing case in the rule set

If OTHERWISE is absent, the output is undefined in uncovered cases. The compiler warns; with --strict it errors. A missing case can silently leave a register in a state that violates an invariant on the next scan.

Pre-state semantics surprise

Inside a rule block, a reference to another register reads its start-of-scan (old) value. Inside a := definition it reads the new (just-computed) value. If your invariant reasoning assumes the opposite, the counterexample will seem paradoxical. See Introduction by Example §3 and Language Reference §15.

3. Division and array-index proof obligations

LoLa treats division and dynamic array indexing as partial operations: they are only valid when the divisor is non-zero / the index is in bounds. These become proof obligations.

division-by-zero

[division-by-zero] cannot prove the divisor is non-zero: b may be 0 where a / b is
evaluated. Guard it, e.g. IF b <> 0.0 THEN ... ELSE ...

Fix with a path-sensitive guard:

rate := IF DT <> 0.0 THEN (x - x_prev) / DT ELSE 0.0;

Inside the THEN branch the compiler knows DT <> 0.0 and discharges the obligation. Or discharge it with an ASSUME:

ASSUME b <> 0;
result := a / b;

array-index-out-of-bounds

[array-index-out-of-bounds] Channel[sel] can be reached with sel = -32768

A runtime index sel requires proof that sel >= lo AND sel <= hi. Add explicit bounds:

ASSUME sel >= 0;
ASSUME sel <= 7;
selected := Channel[sel];

Or guard path-sensitively:

selected := IF sel >= 0 AND sel <= 7 THEN Channel[sel] ELSE 0.0;

Constant indices (Channel[3]) are checked at compile time and never require a runtime proof.

4. ambiguous-priority — conflict between equal-priority rules

If two rules with the same priority can both be active and demand different results, the compiler reports a conflict with a counterexample:

[ambiguous-priority] Motor can be set to both ON and OFF by two rules with
the same priority (5) when: Start=1, Stop=1

Fix options:

  1. Different priorities: give one rule a higher priority than the other. This makes the design decision explicit — which condition wins?
  2. Mutual exclusion: make the guards exclusive so both cannot be true at once. The compiler verifies the mutual exclusion claim.

Do not rely on text order to resolve conflicts — it is not defined.

5. contract-require and contract-ensure — function contract failures

contract-require — call site does not earn the precondition

[contract-require] call to clamp3 at line 12 does not satisfy REQUIRE (lo <= hi)
    counterexample: a=5, b=3

The compiler blames the call site, not the function. Fix: add the missing ASSUME or ensure the arguments satisfy the precondition by construction:

ASSUME a <= b;   -- this earns clamp3's REQUIRE lo <= hi
y := clamp3(v, a, b);

contract-ensure — function body does not establish the postcondition

[contract-ensure] FUNCTION 'f' does not establish ENSURE (f >= 0)
    counterexample: x=-32768

Check for INT overflow (the most common cause on INT and SINT). A function that looks correct over ℤ may fail over 16-bit wraparound arithmetic. Either: - Bound inputs with REQUIRE so the overflow cannot occur - Adjust the ENSURE to what the body actually guarantees - Use a wider integer type

6. Profile gates

[profile-gate] feature 'wstring' is rejected by the active profile (pilot)

A feature is gated in the active profile. Either: - Switch to a profile that allows the feature (--profile default) - Remove the feature use if it is not needed

See Language Reference §17 for the full gate table and CLI Reference §5 for the profile × feature grid.

General debugging strategy

  1. Read the counterexample literally. It is a specific input/state combination, not a vague "something might go wrong". Start from the values shown.
  2. Identify which case the counterexample hits. Trace through your rules with those values by hand.
  3. Fix the logic (add a missing rule, tighten the bounds) rather than weakening the invariant. Weakening the invariant is usually the wrong move; the counterexample is telling you a real gap.
  4. If the counterexample seems "technically legal but absurd", that is the tool telling you your specification has a hole — add the missing constraint. See Introduction by Example §5 ("the specification hole disguised as a proof success").

See also