Synthesis — from RULE contract to proven implementation¶

LoLa inverts the usual relationship between specification and code. In a conventional PLC project the implementation is the source of truth and tests approximate the spec; in LoLa the ASSUME/RULE contract is the source of truth and the implementation is derived from it — synthesized, or supplied and then proved against it. This document explains the three paths an output can take, why they exist, where their boundaries are, and how synthesized blocks compose.

Target classification¶

Inside IMPLEMENTATION, every output is classified by what defines it:

Definition	Classification	Obligation
`y := expr;` and no RULE mentions `y`	explicit	none beyond the usual semantic checks
`y := expr;` and RULEs mention `y`	verify-only	Z3 proves every RULE against the explicit definition
only RULEs mention `y`	synthesis	the compiler must find an implementation and prove it
neither	underconstrained	compile error

The classification is per output, so one block can mix paths — the LM solver LM_Cramer2x2 defines d_sol explicitly and carries two RULEs that Z3 verifies (Ad·d_sol = −g under det > 0), while LM_GramMatrix next to it is RULE-only and fully synthesized.

Bounded synthesis¶

For synthesis targets the compiler runs a bounded search (Z3-backed CEGIS) over candidate expressions up to a fixed node budget, then proves the winning candidate against the RULEs. Two properties matter:

The proof is the product. The search is a heuristic; whatever candidate it finds is only accepted after Z3 proves it satisfies every RULE for all inputs admitted by the ASSUMEs. A lucky guess and an exhaustive search produce the same evidence.
Exhaustion is not unrealizability. synthesis-bound-exhausted means the budget ran out, not that no implementation exists. The answer to it is either a bigger budget, an explicit implementation (verify-only), or the guided path below.

Aggregates (SUM, COUNT, ALL, ANY, MIN, MAX) over statically bounded ranges keep the search space small: RULE ALL(k IN 0..3 : JtJ[k] = SUM(i IN 0..1 : J[i*2 + k/2] * J[i*2 + k MOD 2])) describes sixteen multiply-accumulate expressions in one line, and the synthesizer materializes the per-element implementations mechanically.

Composition of synthesized blocks¶

A RULE-only block can be instantiated inside another block or a PROGRAM like any explicit one. During compilation, every closure child that carries synthesis targets is synthesized in place (same search, same proof) before flattening; verify-only children keep their RULEs, which flattening turns into proof obligations of the parent.

Child ASSUMEs follow the assume-guarantee discipline. A child assumption whose inputs are wired straight to parent inputs propagates upward and becomes part of the parent's contract; one wired to computed values becomes a proof obligation the parent must discharge. The LM composition shows why this is more than bookkeeping: LM_Cramer2x2 assumes det(Ad) > 0, Ad is wired to JᵀJ + λI, and the compiler proves the obligation symbolically from λ ≥ 1 — the classical positive-definiteness argument of the LM method, executed as an actual Z3 proof at composition time rather than cited in a comment.

The type-domain boundary¶

Every proof path has a native domain, and respecting the boundary is what keeps the evidence meaningful:

RULEs over BOOL/INT are finite-domain statements. Both Z3 and a bounded model checker (Kani, CBMC) decide them exactly, so bounded synthesis and the guided path are interchangeable provers.
RULEs over MATHREAL/LREAL are exact ℝ statements. Z3 proves them over the reals. A bounded model checker running the candidate in f64 proves a different theorem — one about machine arithmetic — and the two differ precisely by the roundoff. The guided path therefore refuses REAL ports by design.
The bridge is the envelope machinery: Gappa separately proves |machine − exact| ≤ ε per output under the contract ranges, and these envelopes compose across block boundaries into end-to-end bounds. The ℝ proof says the algorithm is right; the envelope says the binary64 execution stays within ε of it. Neither substitutes for the other.

The LM chain carries all three: synthesized ℝ-proved blocks (Gram, gradient, damping, update), a verify-only ℝ-proved solver (Cramer), and a composed Gappa envelope |x̂_new − x_new| ≤ 9/2⁴³ ≈ 1.02e-12 across the four block boundaries.

Guided synthesis¶

When the search budget is exhausted and the domain is finite (BOOL/INT), the guided path turns an untrusted candidate — hand-written or LLM-generated — into the same class of evidence: the contract is rendered into a proof harness, the candidate fills the single designated hole, Kani (Rust) or matiec/CBMC (ST) proves it against the unrolled ASSUMEs and RULEs, and a content-addressed GuidedSynthesisWarrant binds contract, candidate and proof bytes. Compilation accepts the warrant in place of CEGIS and records it in the assurance report.

Conceptually this is the EXTERN trust model applied to synthesis: the implementation lives outside the LoLa compiler, and what crosses the boundary is not code trust but a checkable receipt. See Guided synthesis and EXTERN for that framing, and the how-to for the lola guided workflow.