State a timer condition in a contract¶

You want a safety claim about a timer: the drive must not run once a hand button has been held for 30 seconds. Written the obvious way, the compiler refuses:

FUNCTION_BLOCK TwoHandRejected
VAR_INPUT T1 : BOOL; T2 : BOOL; END_VAR
VAR_OUTPUT PA : BOOL; END_VAR
CONTRACT
    INVARIANT (NOT PA) OR NOT (HELD(T1, T#30s) OR HELD(T2, T#30s));
END_CONTRACT
IMPLEMENTATION
    PA := T1 AND T2;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

verification failed:
  [sema-error] line 5: HELD/ELAPSED may not appear inside an INVARIANT: the
  timers' own laws are not yet part of the step relation (ADR TMR-1). Mirror
  the condition into a register and state the claim over that (ADR TX-1.2), or
  use them in rule guards / definitions.

This page shows the way that works, and — more usefully — the two ways that look like they should and do not.

Why the refusal¶

An INVARIANT is a predicate over a single state, discharged by one-step induction: it holds initially, and if it holds in a state it holds in the next. PRE(x) widens that by exactly one register. A running timer is not a state predicate — it is a statement about how long something has been true, which one-step induction cannot see.

That is a deliberate boundary, not a gap. Admitting timers would require k-induction, an unrolling bound, and counterexamples far longer than the two states you get today.

The pattern that works¶

Mirror the timer condition into a register, and state the claim over that register:

FUNCTION_BLOCK TwoHand
VAR_INPUT T1 : BOOL; T2 : BOOL; END_VAR
VAR_OUTPUT PA : BOOL; KL : BOOL; END_VAR
CONTRACT
    INVARIANT (NOT PA) OR (NOT KL);
END_CONTRACT
IMPLEMENTATION
    KL:
        ON WHEN HELD(T1, T#30s) OR HELD(T2, T#30s);
        OFF OTHERWISE;
    PA:
        ON WHEN T1 AND T2 AND NOT (HELD(T1, T#30s) OR HELD(T2, T#30s));
        OFF OTHERWISE;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Compilation succeeded: TwoHand
  1 output property verified

ON WHEN X; OFF OTHERWISE; sets the register to the current value of X, so KL in the successor state is exactly the timer condition at the decision instant — which is what the safety claim is about. No sharpness is lost.

Two variants that look right and are not¶

Both of these were written first, and both are rejected. They are worth knowing, because the reason is the same in each case and it is easy to miss.

The drive as a plain definition¶

    PA := T1 AND T2 AND NOT KL;

Rejected:

verification failed:
  [invariant-output] invariant over a derived/output value is not implied
  by the register invariants: (NOT PA OR NOT KL)

An invariant over a derived value has to follow from what the registers guarantee. PA here is recomputed from inputs every scan, so the claim about it is not anchored in any register invariant the prover can induct over.

The drive reading the mirror register¶

    PA:
        ON WHEN T1 AND T2 AND NOT KL;
        OFF OTHERWISE;

Rejected, and this counterexample is the instructive one:

verification failed:
  [invariant-step] invariant can be violated after one cycle:
  (NOT PA OR NOT KL)
      counterexample: KL=0, PA=0, T1=1, T2=1, now=30000, started_0=0

Both registers update from the same previous state. In the scan where the timer matures, PA still sees KL = 0 and switches on, while KL switches on as well — and in the successor state both are set. The register you mirrored into cannot guard the very output that is updated beside it.

So the guard names the condition, not the mirror:

    PA:
        ON WHEN T1 AND T2 AND NOT (HELD(T1, T#30s) OR HELD(T2, T#30s));
        OFF OTHERWISE;

KL then exists for the contract to speak about, and both registers see the same instant.

What stays out of reach¶

Named so the absence is a known boundary rather than a suspected gap:

Properties over a running timer inside INVARIANT — rejected outright, as above.
Relating an input event to a state change more than one step back. PRE reaches back exactly one step; a property needing two steps of history cannot be written.
Liveness ("eventually"), which needs a fairness notion the model does not have.

The first is a compiler error. The other two are silently inexpressible — you simply cannot write them down, which is why they are listed here.

docs/adr-temporal-expressiveness.md — the limit and why it is where it is
docs/adr-timer-wellformedness.md — what makes a timer usable in a proof