How to add and use verified functions¶

Audience: developer adding a verified operation to LoLa or a LoLa block that uses one.\ Prerequisites: familiarity with LoLa's FUNCTION_BLOCK and INVARIANT as shown in the Introduction by Example.\ Language Reference: §9 Functions, §12 EXTERN semantics.

There are three ways a "verified function" reaches a LoLa program, and they differ in who does the proving.

Route	Who proves it	Add without touching LoLa's code?
1. LoLa `FUNCTION` with a contract	the LoLa compiler (Z3 / CHC)	Yes — write it and go
2. External artifact (`SORT`)	an external tool (Creusot, CBMC)	via Route 3
3. `EXTERN … BY <artifact>`	an external tool, dispatched by contract	Yes — manifest entry + `EXTERN`, no compiler code

If your goal is "add more verified operations from the user side", Route 1 (prove it in LoLa) and Route 3 (bring an external proof in by contract) are both open today.

Route 1 — a verified `FUNCTION`, proved by the compiler¶

A LoLa FUNCTION is a compile-time-inlined, side-effect-free operation over its parameters. Give it a contract and the compiler proves the contract before it inlines the function — no external tool, no changes to LoLa itself.

The contract vocabulary:

REQUIRE <bool>; — a precondition the caller must earn.
ENSURE <bool>; — a postcondition the function guarantees. Inside ENSURE the function's own name denotes the result.
VARIANT <int>; — a termination measure for a recursive function (see below).
ENSURE PERMUTATION_OF(a); — an intrinsic postcondition: the result rearranges the array a (proved structurally, not as an SMT formula).

1a. A postcondition with a precondition¶

FUNCTION clamp3(x : INT, lo : INT, hi : INT) -> INT
  REQUIRE lo <= hi;
  ENSURE  clamp3 >= lo;
  ENSURE  clamp3 <= hi;
  IF x < lo THEN lo ELSE IF x > hi THEN hi ELSE x
END_FUNCTION

The compiler proves that the body establishes both ENSUREs given the REQUIRE. Now use it, and the postconditions become facts you can rely on:

FUNCTION_BLOCK Limiter
VAR_INPUT v : INT; a : INT; b : INT; END_VAR
VAR_OUTPUT y : INT; END_VAR
IMPLEMENTATION
    y := clamp3(v, a, b);
    ASSUME a <= b;                    -- discharge clamp3's REQUIRE at the call site
    INVARIANT y >= a AND y <= b;      -- PROVEN, straight from clamp3's ENSURE
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The INVARIANT is proved because the call site honours clamp3's REQUIRE (ASSUME a <= b) and inherits its ENSURE. Drop the ASSUME and the block no longer compiles — the precondition is not earned.

1b. Recursion — `VARIANT` makes termination explicit and checked¶

Recursion is allowed only when it terminates by compile-time unrolling: some measure must strictly decrease, so the recursion bottoms out. VARIANT states that measure, and the compiler verifies it.

FUNCTION countdown(n : INT) -> INT
  REQUIRE n >= 0;
  ENSURE  countdown = 0;
  VARIANT n;
  IF n <= 0 THEN 0 ELSE countdown(n - 1)
END_FUNCTION

VARIANT n declares that every recursive call decreases n by a positive constant; the compiler checks it (a wrong measure is a hard error, see §1e). The real, worked example of recursion + VARIANT + PERMUTATION_OF is examples/algorithms/insertion_sort.lola: bubble and isort each carry VARIANT k, prove sortedness, and promise PERMUTATION_OF(a).

1c. Named predicates — a `FUNCTION` that returns `BOOL`¶

You do not need a special "predicate" construct: a FUNCTION -> BOOL is a named predicate, usable in any INVARIANT, REQUIRE, ENSURE, or RULE.

FUNCTION nonneg(a : ARRAY[0..3] OF INT) -> BOOL
  ALL(i IN 0..3 : a[i] >= 0)
END_FUNCTION

FUNCTION_BLOCK Gate
VAR_INPUT xs : ARRAY[0..3] OF INT; END_VAR
VAR_OUTPUT ok : BOOL; END_VAR
IMPLEMENTATION
    ok := nonneg(xs);
    ASSUME ALL(i IN 0..3 : xs[i] >= 0);
    INVARIANT ok = TRUE;              -- PROVEN via the inlined predicate
END_IMPLEMENTATION
END_FUNCTION_BLOCK

1d. `PERMUTATION_OF` — a rearrangement promise¶

ENSURE PERMUTATION_OF(a) says the result is a permutation of the array parameter a. It is proved structurally (the compiler lifts the index witness off the syntax), not as an SMT formula — because a symbolic permutation predicate is the one shape that makes the solver explode. You use it exactly like the other ENSUREs; see insertion_sort.lola.

1e. When a contract is wrong — the diagnosis¶

A contract is a proof obligation, so a wrong one is a compile error that names the clause, the line, and the failing state. A postcondition the body does not establish:

FUNCTION bad(x : INT) -> INT
  ENSURE bad > x;                     -- false: the body returns x, not x+something
  x
END_FUNCTION

contract-ensure: FUNCTION 'bad' does not establish ENSURE (bad > x) (line 3)

A measure that does not actually decrease:

FUNCTION loop(n : INT) -> INT
  ENSURE loop >= 0;
  VARIANT n;
  IF n <= 0 THEN 0 ELSE loop(n)       -- n does not decrease
END_FUNCTION

contract: declared VARIANT 'n' of FUNCTION 'loop' does not strictly decrease
          by a positive constant in every recursive call

And a call that does not earn the callee's REQUIRE is blamed at the call site (contract-require), not inside the callee — so you know whether you fed garbage in or the function produced garbage out.

Watch for INT overflow. INT is 16-bit and wraps. A contract like ENSURE f >= a over a + n is not provable if a + n can overflow — and the compiler is right to reject it. Bound the inputs with REQUIRE/ASSUME, or state an overflow-safe contract.

Route 2 — an external verified artifact (`SORT`, now dispatched by Route 3)¶

Some operations are proved by an external tool and shipped as a verified artifact. The worked one is s := SORT(a): above a size threshold the compiler does not build a compare-swap network; it emits a call to a Rust lola_sort whose sortedness and permutation are proved by Creusot, and records the warrant in the registry.

No longer hard-wired. SORT is now the first user of Route 3: the large-SORT output is bound to the sort_i16 artifact through the generic EXTERN mechanism. The one thing kept special is the model encoding of the sorted-permutation contract (the permutation witness that must not reach the solver as a formula) — irreducible, and the same code whether SORT or a future array artifact uses it.

The registry — identity and warrant, not a wish¶

lola/verified/manifest.json + lola/verified.py pin down two separable things:

Identity — is the file on disk the one that was attested? A SHA-256 answers that.
Warrant — what was actually established, and by what? A closed status vocabulary (audited < tested < proved), and proved is only allowed with a reproducible witness.

Warrants are per clause. The sort contract is sorted(out) AND PERMUTATION_OF(out, src), and the two clauses can be discharged by different means:

sort_i16 (Rust) : sorted  proved (Creusot)   permutation proved (Creusot)   -> proved
sort_n8  (ST)   : sorted  proved (CBMC)       permutation audited (by network construction) -> audited

so verified.check(minimum="proved") accepts the Rust sort but refuses the ST one — the registry will not launder a half-covered contract as fully proved.

Why you cannot (yet) add a new one purely from the user side¶

Wiring SORT into the language is compiler code, not a manifest entry: arrays._build_sort decides when to use the intrinsic, smt._encode_sortelem constrains the model, and lola/backends/rust.py emits the call. Adding a genuinely new external operation this way means touching those. The registry is user-extensible for identity and warrant; the language binding is not — yet.

Route 3 — `EXTERN … BY <artifact>` (the elegant generalisation, built)¶

You declare an operation by its contract, and LoLa dispatches to a registry artifact whose guarantee matches — no bespoke compiler code per operation. The worked, tested example is examples/extern/saturating_abs.lola:

EXTERN FUNCTION abs_sat(x : INT) -> INT
  ENSURE abs_sat >= 0;
  BY abs_sat_i16;        -- discharged by the registry artifact, not a LoLa proof

FUNCTION_BLOCK SaturatingAbs
VAR_INPUT  v : INT; END_VAR
VAR_OUTPUT y : INT; END_VAR
IMPLEMENTATION
    y := abs_sat(v);
    INVARIANT y >= 0;    -- PROVEN by ASSUMING abs_sat_i16's warrant, not re-deriving
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Why this is a genuine EXTERN and not a Route-1 FUNCTION: LoLa cannot prove >= 0 for its own IF v < 0 THEN -v ELSE v, because -v overflows at v = -32768. The Rust saturating_abs clamps that one case to 32767, so it really is >= 0 for every i16 — and abs_sat_i16 is warranted exhaustively (all 65536 inputs; a complete proof on a bounded domain). EXTERN lets that external proof flow into the LoLa model.

The key move that makes this tractable:

the model ASSUMES the ENSURE (justified by the artifact's warrant), instead of encoding and proving it.

Three registry-driven layers, all live:

Model — ASSUME the ENSURE: the result is a fresh value pinned only by the postcondition. INVARIANT y >= 0 above is discharged from that assumption; INVARIANT y >= 5 would be rejected, because the warrant is >= 0 and no wider.
Backend — the Rust backend ships the artifact verbatim (with its warrant as a banner) and emits the call; the ST backend refuses (no ST artifact yet).
Match + warrant — the declared ENSURE must match the artifact's lola_contract and its signature, checked at compile time. A wrong signature, a missing artifact, or a drifted contract is a hard error.

What is now fully user-side: a new artifact for a contract shape (a binary_search, a saturating_add, a sort for another element type) needs only a reference implementation, a verification recipe, and an EXTERN declaration — no change to the parser, the model, or the backends.

A second operation, sat_add (examples/extern/saturating_add.lola), was added touching only the registry (a manifest entry + one verified.REFERENCE line), the artifact file, and a test — zero language code. Its contract is multi-argument and references the arguments:

EXTERN FUNCTION sat_add(a : INT, b : INT) -> INT
  ENSURE NOT (a >= 0 AND b >= 0) OR sat_add >= 0;
  ENSURE NOT (a <= 0 AND b <= 0) OR sat_add <= 0;
  BY sat_add_i16;

The honest caveats:

The trust boundary is the warrant — and it is traced, not hidden. The compiler labels every INVARIANT that rests on an assumed EXTERN contract with the artifact warrant it inherits, and flags any that rest on less than a full proof ([!] rests on an AUDITED warrant). An invariant that reads no EXTERN output is a genuine LoLa proof and carries no such label.
Matching is by named contract + type signature, not by semantic implication. The match is on the normalised contract string (RESULT, arg0, …) plus the signature — exact, not inferred.
Backend coverage is explicit. An artifact may cover several backends: abs_sat_i16 ships both a Rust artifact (proved) and an ST one (audited). Where an artifact has no binding for a backend, that backend refuses rather than emit an undefined call.

Adding a new artifact — the `lola extern` toolchain¶

The full flow, from nothing to a sealed registry entry:

python -m lola extern init <contract-name> --target rust|st [--ensures "ENSURE ..."]

init creates three things and touches nothing else:

Created	What it is
`lola/verified/<artifact_id>.<ext>`	source stub — implement this
entry in `manifest.json`	ArtifactDescriptor placeholder (no sha256, no status yet)
function in `witness_recipes.py`	harness stub — complete the assertion

Then implement and verify:

# edit lola/verified/<artifact_id>.rs   (replace the todo!())
# edit lola/witness_recipes.py          (complete the harness assertion)

python -m lola extern verify <artifact_id> --target rust

verify runs the recipe against the source file and reports the result. It does not write to the registry.

Then seal:

python -m lola extern register <artifact_id> --target rust

register is the only command that writes sealed entries. It checks that the contract and source hash match what was verified, then sets sha256, status, and witness in the manifest.

Finally, check the whole registry:

python -m lola extern check

check validates hash integrity, recipe availability, and structural consistency for every registered artifact. Scaffold-pending entries (from init, not yet registered) are reported as advisory notices, not errors. Run it in CI.

Trust rules¶

register is the only writer. Never set sha256 or status manually.
verify must pass before register will seal a proved warrant.
A contract change after verify is detected at register time and rejected.
A source change after verify is detected by hash mismatch and rejected.

Error table¶

What `check` or `register` reports	Cause	Fix
`sha256 mismatch`	Source changed after `register`	Re-run `verify`, then `register`
`contract mismatch since verify`	`lola_contract` changed after `verify`	Restore contract, re-run `verify`
`recipe not in _REGISTRY`	Harness stub not yet added	Re-run `init` or add it by hand
`source not found`	`lola/verified/<id>.ext` missing	Re-run `init` or restore the file
`recipe failed`	Harness assertion failed	Fix implementation or harness
`scaffold-pending` (advisory)	`init` run, not yet registered	Implement and register to resolve

For the underlying domain model (Contract, Artifact, Target, Warrant, trust chain), see adr-registry-domain-model.md.

How to add and use verified functions¶

Route 1 — a verified FUNCTION, proved by the compiler¶

1a. A postcondition with a precondition¶

1b. Recursion — VARIANT makes termination explicit and checked¶

1c. Named predicates — a FUNCTION that returns BOOL¶

1d. PERMUTATION_OF — a rearrangement promise¶