EXTERN trust model — bringing external proofs into LoLa¶

Audience: developer who wants to understand why EXTERN exists, how the trust flows from an artifact warrant to an INVARIANT, and what the limits of the model are.\ Language Reference: §12 EXTERN semantics.\ How-to: Verified functions.

Why EXTERN exists¶

LoLa's proof mechanism (Z3 one-step induction) is complete for properties that can be expressed as quantifier-free formulae over the declared types. Some operations cannot be proved this way:

Integer overflow by design. abs(x : INT) using IF x < 0 THEN -x ELSE x is wrong at x = -32768 because -(-32768) wraps to -32768 in 16-bit arithmetic. A Rust implementation that saturates at 32767 is correct, but LoLa cannot prove this by inlining the body — the formula the body generates is exactly >=0 for all inputs except the overflow case, and Z3 finds it.
Domain-specific algorithms. A sorting network, a CRC implementation, or a PID controller tuned for a specific plant may have properties most naturally proved by domain-specific tools (Creusot for Rust, CBMC for C, Gappa for floating-point).
Exhaustive enumeration. For a bounded input domain (all 65536 i16 values), exhaustive testing by a harness is a complete proof — but it is not a Z3 proof.

EXTERN FUNCTION ... BY <artifact> is the mechanism for bringing these external proofs into the LoLa model. It does not extend what Z3 can prove; it lets a justified external result be assumed so that downstream LoLa reasoning can use it.

The ASSUME-the-ENSURE pattern¶

When the compiler encounters an EXTERN FUNCTION call:

It looks up the named artifact in the registry.
It verifies that the artifact's lola_contract matches the declared ENSURE clauses (by normalised string comparison and type signature).
It introduces a fresh SMT variable for the function's result.
It ASSUMEs the ENSURE clauses hold for that variable — justified by the artifact's warrant.
Downstream INVARIANTs are proved using that assumed postcondition.

This is sound if and only if the artifact's warrant is valid. The warrant is the trust boundary: the LoLa proof is only as strong as what the external tool actually established.

The pattern deliberately avoids re-encoding the external property in Z3. For PERMUTATION_OF, for example, a naive SMT encoding would create an existential quantifier (∃ bijection σ …) that makes the solver non-terminating. ASSUME-the-ENSURE sidesteps this: the external tool proved it; Z3 does not re-derive it.

Contract matching: named string + signature¶

The match between an EXTERN FUNCTION declaration and a registry artifact is:

lola_contract string — the normalised form of the ENSURE clauses, with the function name replaced by RESULT, arguments by arg0, arg1, etc.
Type signature — the ordered list of argument types and return type.

Both must match exactly. The match is not semantic implication ("does the artifact prove something that entails the ENSURE?") — that would be undecidable. It is structural equality on the normalised form.

This means: - ENSURE abs_sat >= 0 matches an artifact with lola_contract: "RESULT >= 0". - ENSURE abs_sat > -1 does not match, even though >= 0 implies > -1. You must declare the exact postcondition the artifact proves. - BY abs_sat_i16 is an optional selection hint; without it the compiler searches for any registered artifact whose contract and signature match.

This strictness is intentional. Semantic implication matching would require the compiler to solve an entailment problem for every contract lookup — making compilation non-terminating in the worst case, and opaque in the common case.

Warrant levels and their meaning¶

Every registered artifact has a warrant per target (Rust, ST, etc.) and per clause (each ENSURE):

Level	Meaning	Example
`proved`	The property was mechanically verified by a stated tool (Creusot, CBMC, exhaustive enumeration) with a reproducible recipe	Exhaustive harness over all 2^16 `i16` inputs
`audited`	Reviewed under stated conditions by a named reviewer; not mechanically verified	Network construction argument; domain expert review
`assumed`	Declared without external verification; engineering judgment	`status: "assumed"` in project TOML external implementations

The warrant is the ceiling for any INVARIANT that rests on the artifact. An invariant proved using an audited artifact is only audited overall — the compiler labels it [!] rests on an AUDITED warrant in the output.

The PILOT profile enforces a proved floor: no artifact with audited or assumed status is accepted. This ensures that in a PILOT build, every claim traces back to a mechanical proof.

Backend coverage: per-target separation¶

An artifact may have proofs for some backends but not others:

abs_sat_i16:
  rust: proved  (exhaustive Rust harness)
  st:   audited (network construction argument)

When the compiler emits ST, it uses the ST artifact and reports audited. When it emits Rust, it uses the Rust artifact and reports proved. The two targets share the same LoLa contract but have independent warrants.

An artifact with no entry for a target causes that target to refuse: the compiler cannot emit code for a target that has no verified artifact for the EXTERN operation. This is the fail-closed behaviour: a missing artifact is an error, not a silent gap.

Trust boundary summary¶

EXTERN FUNCTION f(x) ENSURE f >= 0; BY my_artifact;
   ↓ compiler checks: contract match + signature
my_artifact { rust: proved (exhaustive 2^16) }
   ↓ compiler introduces: assume(f_result >= 0) in Z3 model
INVARIANT y >= 0 where y := f(x);
   ↓ Z3 proves: (f_result >= 0) → (y >= 0)
   → INVARIANT y >= 0 : proved via EXTERN my_artifact [rust: proved]

The LoLa proof (the last step) is a genuine theorem: Z3 derives it from the assumed postcondition. The assumed postcondition (the middle step) is justified by the artifact's warrant. The warrant (the first step) is only as strong as the external tool's scope.

What cannot be concluded:

INVARIANT y >= 5 — the artifact proves >= 0; nothing wider is assumed. The compiler rejects this with contract-entailment.
INVARIANT y >= 0 on an ST build where my_artifact has no ST entry — refused.
Any claim about the performance of the artifact (latency, memory usage) — the warrant covers the mathematical contract only.

The registry: identity + warrant¶

The registry (lola/verified/manifest.json) stores two separable things for each artifact:

Identity — SHA-256 of the source file. Checked at every compile to detect drift between what was verified and what will be shipped.
Warrant — per-clause, per-target status and witness. Only lola extern register can write a sealed warrant; manual edits to the manifest are detected at lola extern check time.

This separation means: the warrant cannot be forged without running the verification recipe. If the source file changes after registration, the SHA-256 mismatch is caught before compilation completes.

Guided synthesis as automated EXTERN artifact creation¶

EXTERN and guided synthesis solve related but distinct problems — and they share the same warrant architecture.

The gap EXTERN does not fill¶

EXTERN FUNCTION covers operations that return one value: a result of a declared return type, proved by an external artifact. A full FUNCTION_BLOCK with several coupled outputs — like a pump scheduler where three run[k] flags depend jointly on demand, availability and accumulated hours — does not naturally fit as a single EXTERN call. The coupling between outputs means the proof obligation is a joint constraint, not a per-output one.

Guided synthesis (lola guided) fills this gap. Instead of registering an artifact in the EXTERN registry, the developer (or an LLM) writes a candidate implementation for the synthesis targets of a RULE-only block, and a bounded model checker (Kani or CBMC) verifies the candidate against all RULE and ASSUME constraints.

The structural parallel¶

EXTERN mechanism	Guided synthesis
`ENSURE` clauses	`RULE` + `ASSUME` clauses
Artifact implementation (`saturating_abs.rs`)	`candidate_accepted.rs` / `.st`
`ExternalImplementationWarrant`	`GuidedSynthesisWarrant`
`mathematical_contract_digest`	`declaration_sha256`
`proof_backend: "kani"`	`proof_backend: "kani"`
`compile_source(external_implementation_warrants=...)`	`compile_source(guided_synthesis_warrants=...)`

Both mechanisms share the same epistemological structure:

Contract identity — a SHA-256 that ties the warrant to an exact specification (EXTERN: mathematical_contract_digest; GS: declaration_sha256).
Implementation identity — a SHA-256 of the source that was proved.
Proof provenance — which tool ran, over what harness.
Discharge — the compiler accepts the proof goal as satisfied and skips re-proving it in Z3.

The key difference: no error bounds¶

ExternalImplementationWarrant carries output_error_bounds and state_lipschitz_bounds because the implementation lives in the floating-point representation domain — there is an unavoidable gap between the mathematical contract (MATHREAL) and the concrete type (LREAL / f64). The error bounds quantify that gap and flow through the trajectory analysis.

GuidedSynthesisWarrant carries no error bounds because the synthesis targets are discrete types (BOOL, INT, DINT, arrays thereof). There is no representation boundary: the Kani or CBMC proof runs over the same bit-exact semantics that will execute on the target. The proof is exact, not approximate.

Trust boundary¶

RULE-only FUNCTION_BLOCK PumpBank
    RULE COUNT(run) = demand
    ...
  ↓ lola guided accept --backend kani
candidate_accepted.rs   →   Kani: VERIFICATION SUCCESSFUL
  ↓ acceptance.json (GuidedSynthesisWarrant)
      declaration_sha256: ties warrant to current contract
      candidate_body_sha256: ties warrant to accepted implementation
  ↓ compile_source(guided_synthesis_warrants={"PumpBank": warrant})
      RULE proof goals: discharged via warrant (not Z3)
      program.assurance.guided_synthesis_warrants["PumpBank"] = warrant

What the warrant guarantees:

For every input satisfying the ASSUME clauses, the accepted candidate satisfies all RULE constraints.
The guarantee is as strong as Kani's exhaustive symbolic execution — which, for bounded discrete types, is complete.
If the source contract changes (any input, output, ASSUME or RULE), the declaration_sha256 no longer matches, and the compiler rejects the warrant with a clear error.

What the warrant does not guarantee:

That the candidate is efficient or numerically optimal.
That the runtime behaviour matches if candidate_accepted.rs is edited after acceptance.
Any property of types excluded from Kani's exact domain (MATHREAL, TIME).