# The verification pipeline

This document designs the correctness story for LangLib's compilers: what
"the compiler is correct" means here, why the statement is shared across
wildly different targets, and in what order to prove it. It is the design
input for Stage 6 of [PLAN.md](PLAN.md); proofs land incrementally, and
this page records what is proved and what is still a plan.

## What the targets have in common

The esoteric languages in this library look nothing alike. One is a tape
of bytes, one a stack machine written in invisible characters, one a list
of fractions, one a single instruction repeated. Yet every interpreter in
LangLib has the same shape, and that is what makes a shared statement
possible:

```lean
run : Source → Input → Fuel → Except ParseError RunResult
RunResult := { output : ByteArray, exit : Exit }
Exit := halted | outOfFuel | error String
```

Three properties hold across all of them, by construction:

1. **Determinism.** Given a program, an input, and a fuel bound, the
   result is a function. Thue is the only language with genuine
   nondeterminism, and its interpreter takes the strategy as configuration,
   so the function is total and deterministic once the strategy is fixed.
2. **Observable behaviour is a byte stream plus an exit.** Nothing else is
   observable: no wall-clock, no interleaving, no allocation.
3. **Fuel monotonicity.** More fuel never changes a completed run. If a
   run halts (or errors) with fuel `n`, it produces the same output and
   exit for every `m ≥ n`; if it runs out of fuel, its output so far is a
   prefix of what more fuel produces.

Fuel monotonicity is now a stated law, not folklore. `ProgLang` itself has
no laws, so "∃ fuel, the run halts with the right output" — the form every
correctness theorem concludes with — would be weaker than it reads: nothing
ties the witness fuel to the bound a runner actually picks.
[`LawfulProgLang`](../Langlib/Common/Compilation.lean) states the missing
law (`halted_stable`: a completed run does not change with more fuel), and
[`LawfulTraceLang`](../Langlib/Common/Compilation.lean) its trace
counterpart; the `correct_stable` corollaries (and
`TuringComplete.simulates_stable`) use them to upgrade every `∃ m` to
"every fuel from some point on". `CertifiedCompilerNoIO`, `CertifiedCompiler`
and `TuringComplete` **require** the classes — an unlawful target could
satisfy the bare `∃ m` by abusing fuel as an input channel, so the
requirement is part of what the statements mean, not a convenience.
Instances are proved once per interpreter,
in `Langlib/Languages/<L>/Stability.lean`, by one induction over `exec`;
**every language with a `ProgLang` instance has one**, and every language
with a `TraceLang` instance (whitespace, subleq, FRACTRAN) has the trace
counterpart. The output-prefix half sketched here earlier (`output_mono`)
has no consumer yet and stays unstated.

## The correctness statement

Let `C` be a compiler from Turpentine to a target language `T`, `⟦·⟧_Turpentine` the Turpentine
reference semantics, and `⟦·⟧_T` the target's. The statement we want, for
every Turpentine program `P` in `C`'s supported fragment and every input `i`:

> Whenever the Turpentine program halts, the compiled program halts with the same
> output.

Formally, with fuel existentially quantified on the target side:

```lean
theorem compile_correct (P : Turpentine.Program) (hP : InFragment C P) (i : Input) (n : Nat)
    (hHalt : (Turpentine.run P i n).exit = .halted) :
    ∃ m, (T.run (C P) i m).exit = .halted ∧
         (T.run (C P) i m).output = (Turpentine.run P i n).output
```

This sketch is the halting half of correctness. Forward simulation alone
leaves non-halting source executions unconstrained and cannot rule out a
spurious target halt with an undecodable answer. Both certified compiler
interfaces additionally require divergence preservation: source execution
that exhausts every finite source budget must exhaust every finite target
budget, excluding runtime errors as well as normal halting.

`InFragment C P` is a decidable predicate defined per compiler (no
`readInt` for a byte-only backend, values within a documented range for
brainfuck's fixed-width cells, and so on). Each compiler already computes
it: `compile` returns `Except.error` outside its fragment, so the predicate
is `(C P).isOk`, and the theorem is stated against the successful case.

### Where this lives in Lean

The sketch above is now a definition rather than prose:
[`CertifiedCompiler`](../Langlib/Common/Compilation.lean#L329) in
`Langlib/Common/Compilation.lean`, generic in the source language, the
answer type and the target. It differs from the sketch in two ways, both
strengthenings.

*The observation is a trace, not an output.* Comparing `output` says the
two runs printed the same bytes; it says nothing about what they *read*, so
a compiled program that ignored its input and printed the right answer
would pass. A `Trace` records consumption and emission as interleaved
events, so the statement pins down how much of the stream was used and in
what order relative to the printing. The trace itself is pinned by three
laws, the third of which (`trace_faithful`) rules out underreporting: a
halting run, replayed on the stream truncated to the reads its trace
claims, must be the same run. Whitespace, subleq and FRACTRAN all satisfy
it; whitespace is why the law covers halting runs only — its `readnum`
parse error prints the offending line while consuming nothing, so an
erroring run can observably depend on bytes no honest trace claims.

*The target's stream and events are the source's under a declared
encoding.* The sketch runs both programs on the same `Input` and demands
identical output, which only makes sense for a backend that passes bytes
through unchanged. The contract parameter `targetInput` and witness field `encodeTrace`
declare how the compiler represents I/O — the identity for a byte-for-byte
backend, something explicit for whitespace's line-oriented numbers — so a
re-encoding backend states a real theorem instead of a weakened one.

Both contracts include the independent divergence obligation.
`CertifiedCompilerNoIO` describes closed computations: its source predicates have
no input argument and the target runs on `Input.empty`.
`CertifiedCompiler` retains the `targetInput : Input → Input` parameter;
both obligations quantify over source input. `correct_answer` forgets traces
without dropping that input, while `toClosed` fixes the source stream to
empty and requires its target encoding to be empty too.
See [the precise contracts and witnesses](certified-compilation.md).

## How each proof is structured

Every backend proof factors the same way, which is the point of routing all
compilation through one small source language:

1. **A state relation `R_T : Turpentine.State → T.State → Prop`.** This is the
   only genuinely target-specific ingredient. For brainfuck it says the
   tape holds each variable's value in its slot in the documented encoding
   and the head is at the home position; for whitespace, that the heap maps
   each variable's address to its value and the stack is empty between
   statements; for subleq, that memory holds the variables at their
   addresses and the accumulator cells are zeroed.
2. **A per-statement simulation lemma.** If `R_T σ τ` and the Turpentine statement
   `s` steps `σ` to `σ'` producing output `o`, then the emitted code
   `C(s)` takes `τ` to some `τ'` with `R_T σ' τ'`, producing the same `o`.
   This is proved by induction on the statement, with an inner lemma per
   expression form.
3. **A composition step.** Sequencing and loops follow from the statement
   lemma plus fuel monotonicity; the final theorem is an induction on the
   Turpentine fuel.

The shared parts (fuel monotonicity, output-prefix reasoning, the
composition scaffolding, and the trace algebra that says "same bytes")
live in `Langlib/Common/` and are proved once. What each backend author
writes is `R_T` and the per-construct lemmas.

## Intermediate representations split the obligation

`docs/PLAN.md` (Stage 4) introduces one IR per target family: StackIR for
whitespace and piet, TapeIR for brainfuck and its re-encodings, RegIR for
subleq and the other OISCs. That refactor changes the shape of the proof
obligation, for the better.

Without an IR, each backend needs its own state relation and its own set
of per-construct lemmas, and the expensive part (representing unbounded
integers in bounded cells, decimal printing, bounds-checked indexing) is
re-proved every time. With an IR, the obligation factors:

```
Turpentine --[hard: encoding lives here]--> IR --[easy: often 1:1]--> target
```

and the composition of two simulations is a simulation, which is a lemma
worth proving once in `Langlib/Common/`. The brainfuck family then costs
one hard proof (Turpentine to TapeIR) plus three nearly mechanical ones
(TapeIR to brainfuck, ook, brainloller), instead of three hard ones.

RegIR is also where this document meets Stage 8: the URM simulation that
establishes Turing completeness for the OISC family and the compiler that
targets it are the same construction, so proving one should discharge
most of the other.

## Two compilers per target, two obligations

[PLAN.md](PLAN.md) Stage 9 and
[certified-compilation.md](certified-compilation.md) split each backend in
two, and the split changes
what has to be proved.

A **derived** compiler is obtained by composing the Turpentine-to-register-machine
compiler with the `compile` field of that language's `TuringComplete`
instance. It carries no new proof obligation at all: its correctness is
the composition of two simulations, and that composition is one lemma
proved once in `Langlib/Common/`:

```lean
theorem simulation_trans {A B C} (f : A → B) (g : B → C)
    (hf : Simulates f) (hg : Simulates g) : Simulates (g ∘ f)
```

An **effective** compiler is the hand-written backend, and it carries the
full obligation described in this document: a state relation and
per-construct simulation lemmas. It is what users actually run.

The two are related only through the specification they share. Their
outputs are entirely different programs, so no refinement statement holds
between them; what holds is observational agreement, and that is a
corollary of the two correctness theorems rather than a third theorem:

```lean
theorem effective_agrees_derived (p) (i) :
    Observes (effective p) i ↔ Observes (derived p) i
```

Before an effective compiler is verified, this agreement is the strongest
test available: two independent implementations of one specification,
compared on every example. That is the practical value of doing Stage 8
before finishing Stage 4, and it is why the scoreboard below tracks the
derived column separately.

## Compiling `assert`

`assert` is Turpentine's only specification construct, and it is the one
statement whose compilation is genuinely constrained by the target rather
than merely awkward. The reference semantics makes a failed assert a
*runtime error*: the run stops, the exit is `Exit.error "assertion
failed"`, and the runner exits 1. A backend must produce something
observably equivalent, and targets differ in what they can express.

Three representative backends handle failed assertions as follows:

| target | mechanism | observed outcome | faithful? |
|---|---|---|---|
| whitespace | `push -1; retrieve` | `heap retrieve at negative address -1`, exit 1 | yes, error class preserved |
| subleq | jump to a `trap` cell holding `-2 -2 ?+1` | `negative address -2 in operand A`, exit 1 | yes, error class preserved |
| brainfuck | `+[]`, a deliberate infinite loop | out of fuel, exit 2 | **no**, see below |

The pattern for the first two is the same: find an operation the target's
own semantics already rejects, and perform it deliberately. Whitespace
forbids negative heap addresses and subleq forbids negative operands, so
each has a cheap, unambiguous way to fail. Both backends reserve a
*different* forbidden address for the array bounds check (`-2` and a
separate trap respectively) so the two failure kinds stay distinguishable
in the message.

**Brainfuck is the outlier and the gap.** Brainfuck has no error
condition at all in our semantics except moving left of cell 0, and that
one is not reachable from a backend that tracks the head position
statically. So a failed assert compiles to `+[]` and the program hangs
until the fuel runs out. That is observably different from the reference:
exit code 2 rather than 1, and no message. It is recorded as a deviation
in `docs/brainfuck/compiler.md`.

Two ways to close it, neither yet taken:

1. **Use the one error there is.** Emit a deliberate move left of cell 0,
   giving `pointer moved left of cell 0` and exit 1. This preserves the
   error class exactly and costs a few instructions. It requires the
   backend to reach cell 0 from wherever the head is, which it can, since
   it knows the position at compile time. This looks like the right fix.
2. **Weaken the specification.** Say that compilers may render a failed
   assert as either an error or divergence, and prove the weaker
   statement. Cheaper, and honest, but it gives up an observable
   distinction for no good reason once option 1 exists.

Whichever is chosen, the correctness statement in this document has to
say what "same observable behaviour" means for a failing run, since the
current phrasing only constrains halting runs. That is the same gap noted
under "Later" for runtime errors generally, and `assert` is its most
common instance.

## Recommended order

1. **Turpentine → whitespace.** The relation is nearly the identity: whitespace
   has arbitrary-precision integers, a heap addressable by index, and
   native numeric I/O, so `R` is "the heap agrees with the environment".
   Fewest encoding lemmas, so it is the right place to build the shared
   scaffolding.
2. **Turpentine → subleq.** Also unbounded words, so no encoding pain, but
   control flow is subtract-and-branch, which exercises the composition
   machinery properly. Decimal printing is a self-contained routine with
   its own correctness lemma (a nice, reusable arithmetic proof).
3. **Turpentine → brainfuck.** The hardest, and the reason for doing the other
   two first: 8-bit cells force a fixed-width encoding, so the relation
   carries a representation invariant and every arithmetic lemma has a
   range side-condition. This is where the fragment predicate earns its
   keep.
4. **Turpentine → ook.** Free: Ook! parses into the brainfuck AST and delegates
   execution, so correctness follows from the brainfuck proof composed
   with the (finite, mechanical) isomorphism lemma `parse ∘ render = id`.

Deadfish gets a compiler for the straight-line output-only fragment and a
correctness proof to match; the joke is funnier when it is verified.
Malbolge, thue, and fractran have no planned compiler (see their spec
pages for why), so they have no proof obligations.

## What is proved today

One thing, and it is not a compiler-correctness result: **Whitespace is
proved Turing complete**
([Whitespace.lean](../Langlib/Computability/Whitespace/Main.lean),
[`whitespaceComplete`](../Langlib/Computability/Whitespace/Main.lean#L24)), by
compiling cslib's unlimited register machine into it and proving the
compilation simulates. `#print axioms` on the result reports only
`propext`, `Classical.choice` and `Quot.sound`.

That proof matters to this document for the reason Stage 9 gives: a
completeness proof contains a verified compiler. The Whitespace instance
therefore already supplies a **derived** compiler from a register machine,
and once Turpentine compiles to a register machine, composition gives a
verified Turpentine-to-Whitespace compiler without touching the effective
backend.

Three effective compilers are now verified, each over a fragment stated as
data rather than as prose: the compiler's own `Except.error` is the
fragment. The table below is the scoreboard; update it in the same commit
as the proof.

| Backend | Effective compiler | Simulation | End-to-end theorem | Derived compiler | Behavioural (I/O) |
|---------|--------------------|------------|--------------------|------------------|-------------------|
| whitespace | yes | [yes](../Langlib/Languages/Turpentine/Compile/Certified/Whitespace/Simulation.lean#L2695) | [yes, scalars and output](../Langlib/Languages/Turpentine/Compile/Certified/Whitespace/Simulation.lean#L3744) | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L100) | [**yes**, output only, `encodeTrace = id`](../Langlib/Languages/Turpentine/Compile/Certified/BespokeWhitespace.lean#L43) |
| subleq | yes | [yes](../Langlib/Languages/Turpentine/Compile/Certified/BespokeSubleq.lean#L656) | [yes, two shapes](../Langlib/Languages/Turpentine/Compile/Certified/BespokeSubleq.lean#L656) | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L104) | - |
| velato | yes | [yes](../Langlib/Languages/Turpentine/Compile/Certified/Velato/Simulation.lean#L1252) | [yes, scalars, output and `readByte`](../Langlib/Languages/Turpentine/Compile/Certified/Velato/Simulation.lean#L1981) | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L163) | [**yes**, input included, `encodeTrace = targetInput = id`, NUL-free streams](../Langlib/Languages/Turpentine/Compile/Certified/BespokeVelato.lean#L24) |
| brainfuck | yes | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L108) | - |
| fractran | - | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L113) | n/a (no I/O) |
| thue | - | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L119) | - |
| piet | - | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L125) | - |
| ook | yes | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L131) | - |
| brainloller | yes | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L136) | - |
| unlambda | yes | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L142) | - |
| ski | - | - | - | [yes](../Langlib/Languages/Turpentine/Compile/Derived.lean#L149) | n/a (no I/O) |
| deadfish | - | - | - | n/a (not complete) | - |
| malbolge | - | - | - | n/a (not complete) | - |

`ski` says `n/a` in the last column for a reason no other row has: the
language has no output instruction at all, so there are no events to record
and a `TraceLang` instance would have nothing to say. Its answer is the
normal form the interpreter prints, which is a property of the final state
rather than of the run.

The last column is otherwise empty on purpose. Whitespace and Velato are
the two rows that have reached the behavioural notion — Velato's with
input, which whitespace's still lacks — and for every other the first step
is not a proof but a `TraceLang` instance: the interpreter has to record
its events.
FRACTRAN has one already, for free, because its `run` provably ignores the
input stream — which is also why its cell says `n/a` rather than `-`.

**Whitespace, subleq and Velato have theirs too, and those are the real
kind.** All three read, so nothing was free: each interpreter records the
run's events, and
[`Whitespace/Trace.lean`](../Langlib/Languages/Whitespace/Trace.lean),
[`Subleq/Trace.lean`](../Langlib/Languages/Subleq/Trace.lean) and
[`Velato/Trace.lean`](../Langlib/Languages/Velato/Trace.lean) prove the two
laws from one invariant — the trace's output events *are* the output, and
its input events *followed by what the cursor has left* are what the stream
started with. Velato's faithfulness law
([`Velato/Faithful.lean`](../Langlib/Languages/Velato/Faithful.lean)) needed
one more idea than the other two, because its interpreter runs whole
sub-runs rather than single steps: the two-stream simulation also has to
say that the two runs consume the *same bytes*, or a statement could not
be followed by the rest of its block. Those are exactly the three backends
with bespoke certified fragments. Extending those fragments needs further
source/target simulation proofs; preservation of observations during divergence
will additionally need trace-prefix monotonicity in the interpreters.

Fuel monotonicity dropped out of the scoreboard as a proof tool — both
proofs use the exact-cost `Langlib.Common.Reaches` and never needed it —
and came back as a stated guarantee: every language's `LawfulProgLang`
instance is what turns each row's `∃ m` theorem into one about every
sufficiently large fuel bound (`correct_stable`).

Whitespace's fragment is scalar `int`/`bool` with the full expression
language including subtraction, unary minus and negative literals, plus
`if`, `while` and `assert`; it leaves out `/`, `%`, arrays and all I/O.
Subleq's is two program shapes. Velato's is whitespace's without `assert`
and with `print`, `println` and `readByte` into an `int` variable; `/`, `%`
and `printByte` stay out, the last because Velato prints a `char` above 127
as two UTF-8 bytes where Turpentine writes one. Note that whitespace's fragment is
**incomparable** with the certified URM one: subtraction and negative
integers are impossible on the register machine, while `/` and `%` are in
the URM fragment and not in this one. `agree` applies on the intersection,
which still contains arithmetic, comparisons, `&&`, `||`, `if`, `while`
and `assert`.

Everywhere a theorem is still missing, the differential tests in
`Langlib/Tests/Compile*` are the evidence: every supported example is run
through the Turpentine interpreter and through the compiled program, and
the outputs must match. That is testing, not proof, and this page exists
to close the gap.

## Divergence-preserving completeness

[`TuringComplete`](divergence-preservation.md) now requires both forward
answer preservation and divergence-preserving URM simulation. All twelve
witnesses prove `.outOfFuel` at **every** finite target fuel on divergent
source inputs, independently of decoding. The shared consequences are
halting and result equivalences, output validity, and error freedom.
An iff about decoded results alone would still permit undecodable halts.

The runnable compilers are unchanged. The Turpentine-to-URM pass now also
preserves divergence, so all twelve derived compiler contracts include both
proofs. The existing certified bespoke Whitespace, Subleq and Velato fragments,
including the Whitespace and Velato I/O witnesses, satisfy the stronger
contracts too. See [certified compilation](certified-compilation.md).

## Later

* **Infinite I/O traces**: divergence preservation is proved for every existing
  certified witness. Matching the emitted/read prefixes of infinite executions
  is a further obligation beyond exhaustion at every finite budget, deferred
  to [issue #1](https://github.com/ilyasergey/langlib/issues/1).
* **Runtime-error correspondence**: Turpentine's `assert` failures and division
  by zero currently have no target-side counterpart (brainfuck cannot
  report an error). Options: compile errors to a documented halting
  signal, or restrict the fragment. Decide when the compilers stabilise.
* **Velvet as the source.** The long-term goal (see `docs/turpentine/spec.md`) is
  to compile a fragment of shallowly-embedded Velvet into Turpentine by relational
  compilation. That adds one more layer to the pipeline, and the layer
  composes: Velvet-to-Turpentine correctness plus Turpentine-to-target correctness gives
  Velvet-to-target. Keeping Turpentine small is what makes that composition
  affordable.