Assurance model — what LoLa's proofs actually guarantee¶

Audience: engineer or auditor who wants to understand precisely what "proved" and "assumed" mean in LoLa, and what can and cannot be concluded from a successful compilation.\ Language Reference: §8 Contracts, §16 Proof obligations, §17 Profiles.

The fundamental claim¶

When LoLa compiles a programme and prints Compilation succeeded, it has discharged one or more of the following proof obligations using Z3:

Initial-state invariant — every INVARIANT holds when all registers are at their power-on defaults (typically 0 / FALSE).
Inductive-step invariant — if every INVARIANT holds at the start of a scan, it still holds at the end, for every possible combination of inputs.
Function contract — every FUNCTION's ENSURE is derivable from its body and REQUIRE clauses, for all valid inputs.
Partial-operation safety — divisors are non-zero and dynamic array indices are in range, at every point they are evaluated.
Priority consistency — no two equal-priority rules can fire simultaneously with conflicting results.

These are mathematical theorems about the LoLa source model, proved by Z3 over the domain stated in the type system (integers modulo 2^n, ℝ for REAL, etc.).

What a successful compilation does not guarantee without additional evidence: - That the generated ST or Rust code computes the same thing the model does (backend correctness is a separate assurance gate — G3 in the assurance vocabulary) - That the specification captures the engineer's true intent (specification completeness is an engineering responsibility — the classic "pump off forever" hole) - That the deployed hardware matches the model (physical assumptions are declared, not proved)

One-step induction: why it is complete¶

The inductive proof for INVARIANT P:

Base case: P holds in the initial state.
Inductive step: P(state_k) → P(state_{k+1}) for all inputs at scan k.

By induction over the natural numbers, P holds at every scan k ≥ 0, regardless of the input sequence. This is the "row of dominoes" argument: if the first domino falls (base case) and each knocks over the next (step), all of them fall — no matter how long the sequence.

Z3 encodes both cases as quantifier-free SMT formulae (for the boolean and integer types; for REAL, as linear arithmetic) and checks them with a complete decision procedure. A counterexample is a concrete state that violates the obligation; an UNSAT result is a proof.

One-step induction is complete for safety properties: if a property can be violated, Z3 will find the violation. It is not complete for general liveness (properties of the form "eventually X" under all environments).

For SSFC charts, structural liveness is checked via the C-LIVE claim: a LIVENESS FROM S EVENTUALLY T; declaration causes the compiler to verify that a T-containing marking is reachable from any S-containing marking in the exact marking graph. This is sound for bounded SSFCs but does not account for guard satisfiability (a structurally reachable path may be blocked by guards).

The assurance vocabulary¶

LoLa uses a closed vocabulary to label every proof obligation and its basis:

Label	Meaning
proved	Discharged by Z3 (or, for EXTERN, by the artifact's mechanical proof) with no unresolved premises. The mathematical claim holds.
assumed	Declared as an engineering fact without mechanical verification. The compiler accepts it but labels it. An `ASSUME` is the source-level mechanism.
validated	Behaviour checked against a reference (e.g. matiec executing the generated ST) for a declared input/timing slice. Does not generalise beyond the slice.
tested	Exercised in a test suite. Covers the tested inputs; says nothing about others.
audited	Reviewed under stated conditions by a named reviewer. Stronger than assumed; weaker than proved.
experimental	Available outside the stable profile; not covered by assurance gates.
unsupported	Rejected by the active profile. Fail-closed.

These labels are not interchangeable. An INVARIANT that rests on an ASSUME is proved given the assumption — its label in the output is proved for the logical step, but the overall guarantee is only as strong as the assumption. The compiler traces this: an invariant that rests on any ASSUME or on an EXTERN artifact with audited warrant is annotated with its weakest dependency.

Never read "verified" as "proved". In LoLa documentation, "verified" is informal shorthand for "the verification toolchain was applied"; the specific claim and its basis are always in the assurance label.

The provenance chain¶

Every proof obligation has a provenance — the chain of steps that justifies it.

For a pure LoLa proof with no EXTERN:

INVARIANT P  →  proved  (Z3, no premises)

For a proof that uses an ASSUME:

ASSUME u >= -1.0  (assumed: engineering declaration)
INVARIANT s >= -1.0  →  proved given (u >= -1.0)

For a proof through an EXTERN contract:

EXTERN FUNCTION abs_sat(x) ENSURE abs_sat >= 0; BY abs_sat_i16
  →  abs_sat_i16: proved (exhaustive enumeration, Rust)
INVARIANT y >= 0  →  proved via EXTERN abs_sat_i16 [rust: proved]

For a numerical error bound:

[physical_errors] u = "1/100"  (assumed: sensor specification)
[sampling.s] period = "10ms", jitter = "1ms"  (assumed: deployment)
E_∞ = 0.27  →  proved-under-assumptions

The compiler prints the provenance chain in its output. The Engineering Error Report lists every declared assumption. A successful output with all obligations labelled proved and no assumed premises is the strongest possible claim. Most real programmes will have some assumed premises — physical reality is not something a formal tool can prove.

Assurance gates: G1 through G4¶

LoLa uses a structured set of assurance gates to track coverage:

Gate	Question	Closed when
G1	Is the model proof sound?	Z3 proves all invariants and function contracts for the PILOT profile subset
G2	Is the specification complete?	Contract matrix reviewed; no "legally pump-off-forever" holes found
G3	Do the backends compute the same function?	Reference simulator = Z3 model = executed ST = compiled Rust, over a stated input slice
G4	Does the deployed system match the model?	Hardware/timing/sensor assumptions verified in deployment

G1 and G3 are partially automated (test suite, CBMC/Kani harnesses). G2 and G4 require engineering judgement and cannot be mechanically discharged.

G1 is not G3. A proof in the Z3 model says nothing about the generated code unless G3 validation covers the same constructs. The PILOT profile enforces that both ST and Rust backends are required, and that CBMC/Kani validates the Rust output for the admitted construct set.

What the specification does and does not capture¶

Formal verification proves that the implementation is consistent with the specification. It does not prove that the specification captures the engineer's true intent.

The classic example: INVARIANT Pressure < 10.0 has a simple proof where the pump is always off and the valve is always open. The invariant is satisfied. The plant is useless.

LoLa makes this problem visible rather than hiding it behind test coverage: a proof success on a weak specification is a precise signal that the specification is incomplete, not that the design is correct. The counterexample for a missing liveness property is not a state the solver found — it is a valid execution the solver has no reason to rule out.

The engineer's job is not only to write rules the compiler can prove, but to write a specification complete enough that a proof of it is actually meaningful. The ASSUME/INVARIANT distinction forces this question: every premise the block relies on is named explicitly and carries a warrant.

Profiles as assurance floors¶

A profile is a named set of compiler gates that defines a minimum assurance level:

default — all features available; experimental features accepted; no floor.
pilot — a curated subset where G1 is closed: experimental features rejected; both ST and Rust required; EXTERN warrants must be proved; fresh evidence checked.
float64 — enables the Representation Boundary; same floor as default.

The PILOT profile is designed to make G3 tractable: by restricting the allowed constructs to those with validated backends, the scope of the validation matrix is finite and maintainable. Features that remain experimental in DEFAULT are either pending validation or known to have unsound backend behaviour.

See Language Reference §17 for the full gate table.