# Progress log

Newest first. Add a dated entry for every substantial batch of work.
Entries describe their dated checkpoints; the temporary separate divergence
interface in the first two proof milestones was superseded by the combined
`TuringComplete` interface below.

## 2026-09-06 — JavaGen Turing completeness and documentation audit

Proved exact terminal serialization and byte decoding, then assembled
`javaGenComplete` from URM answer preservation and all-fuel divergence.
The witness and source-realization theorem use only Lean's standard axioms.
Registered `derivedJavaGen` with the Turpentine CLI and added source-round-trip,
answer, divergence and decoder regressions. A reflexive `csimp` proof lets
the compiler share its declaration index across closure rows.

Updated the spec, proof account and implementation comments. README language
matrices now use consistent notation and alphabetical order. Checked local
links and exact declaration anchors; replaced unavailable source pages with
verified archives. Validation: `lake build`, 1,856 golden tests, five property
groups, 34 javac cases, 315 site checks, and link/axiom audits all pass.


## 2026-09-06: JavaGen source realization proved

Proved `urmSource_realized`: every URM program and input has ordinary JavaGen
text that the existing loader recovers as exactly the total generated
artifact, including its inheritance closure and paths. The
[source renderer](../Langlib/Computability/JavaGen/SourceRealization.lean)
separates tokens with spaces; the existing compact renderer is unchanged.

The lexer proof covers legal identifiers, keywords and punctuation at its
actual source-length guard. The parser proof covers arbitrary token
coordinates, nested unary types, ordered superclass/declaration lists and
the final end-of-input check. Token count plus one is proved sufficient for
all parser recursion. Composition with the existing validation theorem
establishes equality of complete prepared artifacts.

The ordinary runner evaluates the emitted successor example with input `2`
to `3`. The specification and universal compiler account document the exact
renderer and example. Byte-level answer decoding is now the remaining proof
gate before assembling `javaGenComplete`; no completeness witness is claimed.

Validation: `lake build`, all 1,852 golden tests, all five property groups and
34 real-`javac` conformance cases pass. The site passes 315 structural checks,
and all local documentation links and numbered source targets resolve. Both
the syntax round trip and full loader theorem use only standard Lean axioms.


## 2026-09-06: JavaGen compiler totality proved

Proved that the executable URM compiler always returns its generated artifact,
including on divergent inputs. The
[totality proof](../Langlib/Computability/JavaGen/CompilerTotality.lean)
covers shifted register allocation, legal and distinct generated names,
declared constructor arguments, superclass parity, acyclic inheritance and
all finite symbolic lookup obligations. The ordinary indexed validator's
walk succeeds at its own class-count budget; ancestor heads are distinct,
so its diamond filter retains every row and path. The proof applies to the
real validator loops by definitional equality.

`urmPrepared_halting`, `urmPrepared_divergence` and
`urmPrepared_answer_record` now apply to the total artifact without assuming
successful compilation. Divergence still means `.outOfFuel` at every finite
budget, independently of decoding. The answer theorem still concerns the
actual third most recent proof frame.

The full `TuringComplete` witness remains pending: generated-source
realization and the byte-level answer decoder are the remaining proof gates.
No completeness witness or derived Turpentine backend is registered yet.

Validation: `lake build`, all 1,852 golden tests and five property groups
pass. All 34 real-`javac` conformance cases pass with no inconclusive result.
The regenerated site passes 315 structural checks; repository-wide local
links and exact numbered source targets resolve. The totality and unconditional
operational/retained-answer theorems use only Lean's standard logical axioms.


## 2026-09-06: JavaGen arrays and runnable examples

Extended the [Turpentine backend](javagen/compiler.md) to fixed-size integer
and Boolean arrays. Each cell occupies a counter register; computed indices
select through a finite dispatch chain, and nested reads preserve temporary
values. Boolean guards short-circuit, including guarded out-of-bounds reads.
An invalid access loops in the target; the source interpreter reports a
runtime error. The shared FRACTRAN frontend retains its scalar-only default.

Added prefix sums, histogram, Boolean marks and Fibonacci-table examples,
with full source in the [specification](javagen/spec.md#turpentine-array-examples)
and commands in both JavaGen documents. Their answers, `10`, `2`, `3` and
`8`, agree with the Turpentine interpreter. Array tests additionally cover
initialization, adjacent arrays, aliasing, bounds traps and the existing
maximum and sieve examples. Corrected the AST comment to match the reference
evaluator's RHS-before-index order for indexed writes.

Profiling the large sieve exposed repeated linear declaration searches in
JavaGen validation. Indexed names, declarations and superclass heads now
avoid those searches; reverse accumulation also removes repeated copying
of expanding ancestor lists. Closure order and first-path selection for
equal diamonds are preserved.

Validation: all 1,852 golden tests and five property groups pass, including
40 array/source/bounds checks. All 34 real-`javac` conformance cases and 315
site checks pass; the four new examples produce `10`, `2`, `3` and `8`, and
the existing maximum and sieve produce `9` and `15`. All tracked Lean modules
build, including the validator's kernel-checked source-realization examples.

## 2026-09-06: JavaGen URM register-tape simulation and divergence

Proved the unbounded register representation and every complete instruction
sweep in [TapeProof.lean](../Langlib/Computability/JavaGen/TapeProof.lean).
Increment, saturating decrement and both test branches preserve all register
blocks; a return pass restores tape orientation. Every flow instruction has
strictly positive subtype cost, including self-jumps. Arbitrary located
structured-counter executions now simulate in the ordinary target evaluator.

[URMProof.lean](../Langlib/Computability/JavaGen/URMProof.lean) composes the
existing URM forward theorem through the tape invariant to the represented
answer and normal halting. [Divergence.lean](../Langlib/Computability/JavaGen/Divergence.lean)
connects the generated prologue and continuing dispatcher invariant to
all-fuel exhaustion for divergent URM inputs. `compileURM_halting` and
`compileURM_divergence` concern the actual successfully returned artifact.
The latter is independent of output decoding and excludes runtime errors.

[ObservationProof.lean](../Langlib/Computability/JavaGen/ObservationProof.lean)
locates the exact final answer frame in the actual successful execution and
proves its `Letter_1` count equals the arbitrary source answer. Ground
inheritance erases the live query but preserves that frame. Generated-name
validity and injectivity, constructor padding, reversal and unbounded unit
counting are proved separately; textual serialization/decoding remains open.

No `TuringComplete` witness yet: uniform compilation, generated-source
realization and correctness of the textual result decoder remain open.

Validation: the isolated checkpoint passes `lake build`, all 1,813 tests
and five property groups. Real Java conformance passes all 34 probes; the
site passes 315 checks. Documentation links and declaration anchors resolve.
The new main theorems use only `propext`, `Classical.choice` and `Quot.sound`;
there are no proof placeholders or custom axioms.

## 2026-09-06: hand-written Turpentine-to-JavaGen compiler

Implemented [the JavaGen backend](javagen/compiler.md) for closed nonnegative
scalar computations with an integer `answer`. It reuses the lightweight
Turpentine-to-Minsky pass, merges straight-line increments, compacts control
states and emits ordinary JavaGen through the shared sweeper generator.
Compilation does not evaluate the source, including on divergent loops.

Added `--to javagen` / `--via javagen` and standalone `--compiled-answer`.
The answer observation uses the ordinary subtype step with indexed closure
lookup, retaining only the final control tape rather than a full history.
It reads register zero at successful completion. Compiled queries are closed;
the numeric answer-hole certification script remains a separate workflow.
No end-to-end compiler certificate or `--tc` backend is claimed. Source
errors at zero divisors and failed assertions follow the shared counter
pass's existing conventions; tests and documentation record the differences.

Moved the executable sweep generator to the language folder, preserving
compatibility exports for its existing simulation proofs. Added differential
fixtures against the Turpentine reference interpreter, fragment rejection,
nested and infinite loops, assertion behavior and proof-record/answer-mode
agreement. Updated the spec, compiler guide, README status and workplan.

Validation: `lake build` passes. All 1,813 tests and five property groups
pass, including the 65 new compiler/reference/fragment cases. Sum, sum of
squares, factorial, Fibonacci, integer square root and GCD return 10, 30,
120, 55, 4 and 21 respectively. Standalone emitted-source execution passes,
as does Java export and `javac` acceptance of a generated zero program.
The Java conformance suite reports 34 passes, no failures and no inconclusive
results; generated sweeper fixtures are unchanged. All 315 site checks pass.
The documentation audit checks 1,151 local links, including 156 numbered
source links, with no issues. The runtime import graph has no Mathlib or
cslib dependency. The compiler guide records the measured emitted sizes.

## 2026-09-06: JavaGen URM generation and flow/sweep simulation proofs

Added an [experimental executable URM compiler](javagen/universal-compiler.md):
the existing structured-counter translation becomes a finite flow graph,
then a sweeping transducer over unary register blocks, then ordinary JavaGen
source. Loop bodies are emitted once and iterations use control-flow edges;
compilation never executes the source. The compiler uses the ordinary
validator and a decidable certificate for symbolic lookup, the actual initial
query and closed execution mode. The experimental decoder counts output units
in the final control query retained by the existing proof-record evaluator.

Proved the two-step symbol replacement, three-step end turn and three-step
halt against the actual subtype evaluator. The generic sweep simulation
preserves finite halting runs and all-fuel divergence under continuing source
invariants; the checked artifact theorems target `evalPrepared`. A generated
one-state symbol-duplicating sweeper has proved source realization, a checked
lookup certificate and all-fuel divergence despite its changing query/tape.

Proved `flatten_length`, generated instruction/continuation locations,
structured-counter execution preservation through arbitrary nested loops,
and forward URM answers at the flow graph's actual terminal node. These
establish the upper and lower simulation layers. The middle flow/tape
invariant, URM divergence composition, answer-decoder correctness, uniform
compiler success and uniform source realization remain open. No
`javaGenComplete` or certified Turpentine backend is claimed. General numeric
candidate queries for independent Java result certification are also pending;
the existing numeric recurrence examples retain that workflow.

Added compiler-generated source fixtures, a drift-checking Lean generator,
13 counter/URM compiler regression cases plus round trips and divergence
prefixes, and real-Java acceptance probes for two generated counter programs.
Updated the plan, compiler/proof accounts and specification. The current route
reuses existing counter arithmetic with the paper's read/write and turning
mechanism; a separate ordinary Turing-machine adapter is no longer the first
step. Recorded the initial-query/mode certificate obligation in CONTRIBUTING.

Validation: `lake build`, all 1,748 golden tests and all property groups pass,
including the new compiler regressions. All 34 real-`javac` conformance cases
pass on Java 11.0.15. Generated fixtures are current; the documented URM
successor example evaluates to `Except.ok (some 3)`. All 315 generated-site
checks pass. The proof audit uses only Lean's standard axioms, with no
`sorry` or native-evaluation axiom; the documentation/link audit passes.


## 2026-09-06: JavaGen evaluator, numeric answers and real-Java certification

Implemented the [JavaGen specification](javagen/spec.md), total parser,
validated symbolic inheritance closure, pure fuel-based subtype evaluator,
runner and Java exporter. Closed queries retain their successful derivation,
including arguments later erased by ground inheritance. Numeric queries
carry one `answer` hole: symbolic execution infers a padded unary numeral,
then concrete execution checks the original query specialized with it.
The single-command Python driver additionally checks that same computation
with real `javac`, compiling declarations separately and treating resource
exhaustion as inconclusive. Unchecked warnings are errors and annotation
processing is disabled.

Added original Fibonacci(10), factorial(5), summation, positive-input addition,
zero, inheritance and divergence examples, plus 48 golden tests and source
round-trip/stability/payload properties. The arithmetic fixture generator
emits finite recurrence declarations without calculating their answers.
These are not Turpentine compilations or evidence of a universal compiler.
The spec quotes complete examples and documents both the single-command
Fibonacci certification and separate Java export/compilation commands.

The [computability development](javagen/computability.md) now proves
completed-run stability for both modes, `LawfulProgLang`, injectivity of
unbounded natural encodings, source realization of the loop example, and
its positive-cost divergence at every finite fuel. The universal answer
protocol, tape-machine construction, URM bridge and their answer/divergence
proofs remain open. Keep the public URM contract and first use the paper's
tape-machine construction; SKI is possible but requires a new application
and duplication simulation. TC is the next priority, ahead of a direct
Turpentine backend or performance tuning.

Updated the workplan, roadmap, compiler/proof accounts and testing guide.
The README threshold is now met, so added the language README, status rows
and generated-site catalogue entry. Recorded in `CONTRIBUTING.md` why result
certification must retain the original query and check declarations first.

Validation: `lake build` passes; focused JavaGen tests and properties pass;
`difftest.sh` passes, including 32 JavaGen checks on `javac 11.0.15` with
wrong-answer rejection. The Fibonacci certification prints 55; the documented
export and separate `javac` commands succeed. Missing-JDK, zero-fuel and
nonnumeric-query failure paths pass; generated fixtures are current. All
315 generated-site checks pass. The new proof audit uses only standard Lean
axioms, with no `sorry` or native-evaluation axiom. All 1,748 full-suite
tests and the property checks pass. The final documentation audit checks
1,118 local links, including 156 numbered links, with no issues.

## 2026-09-06: JavaGen design started

Created `ilya/java-generics` from `master` and read Radu Grigore's
*Java Generics Are Turing Complete* (POPL 2017), concentrating on the
subtyping machine, Turing-machine reduction and Simper compiler. The
[JavaGen design](javagen/design.md) adopts the unary contravariant core
and replaces Simper with Turpentine through the existing certified URM
pass. It specifies proposed syntax, validation, fuel/rejection behavior,
Java export, module boundaries, testing and staged proof obligations.

The first proof gate is answer retention: the paper's successful subtype
query recognizes halting, but its ground halting rules erase the tape.
The proposed observation retains the successful derivation so a marked
answer block can be decoded; that proposal still needs an executable
experiment and proof. No JavaGen code, runner, compiler or completeness
witness is claimed. Moved JavaGen from the candidate roadmap to active
design and recorded the general recognition-versus-answer obligation in
the contribution checklist. README integration is deferred until the spec,
parser, interpreter, runner and tests are all in place, as requested; this
threshold is now recorded in the project documentation policy.

Validation at the requested commit: `lake build` passed, the documentation
audit found no issues in 1,059 local links, and all 305 generated-site
checks passed. The full `lake test` suite was still running when the user
requested an immediate commit; no failures had been reported at that point.

## 2026-09-06: concise README and documentation links

Both README status tables now link bespoke compiler results to compiler
notes and computational-class results to per-language computability accounts.
Added the missing accounts for Whitespace, Ook! and Brainloller, retaining
Brainloller's pixel-walk proviso. The main README now explains matrix statuses
in bullets and gives shorter accounts of lawful execution and compiler
correctness; the separate bespoke-compiler rationale is folded into the
compiler overview.

Refreshed MU's computability overview with the checked fixed-cell runtime
milestones and current obligations. Recorded the proved returning width
growth and adjacent-fill obstruction, and
updated the audit's completeness contract to include divergence preservation.

## 2026-09-06: separate closed and input-parametrised compiler contracts

`CertifiedCompilerNoIO spec diverges L` now describes closed computations:
`spec : Src → Nat → Ans → Prop`, `diverges : Src → Prop`, and every target
run uses `Input.empty`. There is no `targetInput` parameter. The derived
Turpentine certificates and direct bespoke Subleq/Whitespace certificates
use this interface. The final API also removes `targetInput` from
`TuringComplete`: every compiled URM/input pair runs on `Input.empty`, so
the derived construction needs no input encoding or side condition.

`CertifiedCompiler` retains arbitrary caller input, its explicit encoding,
and completed-trace and divergence preservation. The input-reading Velato
witness is `bespokeVelatoIO`; tests now call it directly. `correct_answer`
forgets traces without losing the input argument. `toClosed` and `toClosedOf`
replace the previous automatic `toCertified` conversions: closing fixes source
input to empty and requires proof that its target encoding is also empty.
The explicitly named `bespokeWhitespaceIOClosed` and `bespokeVelatoIOClosed`
make that restriction visible. Closed means a fixed execution interface,
not a syntactic proof that a program contains no reads.

Documentation, contribution policies and declaration links follow the API.
Historical progress entries below describe earlier interfaces. Finite input
storage and fuel-bounded finite traces are unchanged. Preservation of
observations during divergence is deferred to
[issue #1](https://github.com/ilyasergey/langlib/issues/1); the exploratory
observation-proof file was removed. Infinite input is a separate extension.

The documentation/comment sweep also corrected stale backend restrictions,
finite-trace descriptions, module paths and declaration links. Investigated a
reported repeated rebuild with the Subleq `isqrt.turp` command: unchanged runs
performed zero build jobs, all 3,057 local artifact timestamps stayed unchanged,
and `lake --no-build exe` succeeded. Documented direct executable invocation
for batch compilation to avoid Lake's dependency-graph checks.

Validation: the full library and Turpentine executable build pass. All 784
axiom reports are clean (751 use only the standard logical axioms; 33 use none).
The documentation audit passes 1,053 local links, including 210 numbered links
to 107 distinct declarations. The generated site passed all 305 checks and its
playgrounds passed all 45. All 1,700 golden/compiler tests and both Velato
round-trip checks pass. The branch is ready for the requested commit, push and
fast-forward merge into the repository's default branch, `master`.

## 2026-09-06: uniform proof folders and source divergence foundations

Every language's computability development now lives in its own folder,
with `Main.lean` as its entry point. Shared URM, counter and divergence
infrastructure lives under `Langlib/Computability/Common/`. The certified
Turpentine backend proofs moved to `Turpentine/Compile/Certified/`;
`Compiler/` is not used. All imports, proof links and documentation paths
follow the moves, while declaration namespaces and compiler functions stay
unchanged. Every per-language computability account is linked directly from
its language README and indexed from both main READMEs. Named witnesses and
divergence proofs link to their exact declaration lines. The main README's
`TuringComplete` description is now concise.

`Turpentine/Divergence.lean` defines divergence using the actual source
interpreter's exit at every finite fuel. It proves completed-run stability
and structural divergence inversions for sequences, conditionals and loops,
including the distinction between a divergent loop body and a terminating
body followed by a divergent next iteration. These facts stay free of
Mathlib and do not infer divergence from the absence of a decoded answer.
They are foundations for the requested mandatory compiler-divergence fields
and upgrades of the existing certified fragments.

Validation is in progress for this layout checkpoint; compiler-contract
strengthening remains the next stage.

## 2026-09-06: TuringComplete includes divergence preservation

After committing and pushing the all-eleven proof milestone (`052b87e`),
folded `preserves_divergence` into `TuringComplete` and removed the temporary
extension and duplicate witnesses. All eleven original `<lang>Complete`
names now include both answer and divergence proofs. The generic
`halts_iff`, `result_iff`, `halted_run_result`, `output_valid`, and
`error_free` theorems live in `Langlib.Common.TuringComplete`.

The proof layout avoids circular imports: `<Language>/Simulation.lean`
contains the original compiler, forward proof and language instances;
`<Language>/Divergence.lean` proves continuing execution; the original public
`<Language>.lean` imports both and assembles the witness. Compiler functions,
public import paths and derived Turpentine APIs are retained. The stronger
URM-to-target contract does not automatically strengthen the separate
Turpentine-to-URM forward specification. Brainloller still uses its existing
decoded-program interface, with the pixel-walk proof a separate obligation.
MU's proof terms remain unchanged; its documentation-path comments follow
the moved computability account.

Updated the plan, contribution/proof policies, shared interface and testing
notes, every affected language README/spec, and per-language computability
accounts. All twelve `docs/computability-<language>.md` accounts now live
in `docs/<language>/computability.md`, including the negative and unfinished
claims. Incoming links, relative links within the moved pages and code
comments follow those paths. Every numbered source link in the root docs
and under `docs/` points to its exact declaration line. Old statements that SKI and
Unlambda divergence remained open are corrected. The bounded-storage
explanation now uses halting reflection, while keeping effectiveness of the
compiler an explicit meta-theoretic requirement.

Validation: `lake build` passes all 8,956 jobs, including MU. All 1,700
golden/compiler tests and both Velato round-trip checks pass. All 761 axiom
reports are clean (728 use only the standard logical axioms; 33 use none).
The available external differential suite passes six cases, with unavailable
references/runners skipped. The documentation audit checks 1,099 local links
and 240 numbered links to 116 distinct declarations, with no failures.

The requested continuation is a uniform computability folder layout, followed
by divergence-preserving compiler correctness, the Turpentine-to-URM proof,
and upgrades of the derived and certified bespoke compilers.

## 2026-09-06: all eleven divergence-preserving witnesses

Unlambda now preserves divergence for its unchanged compiler. The decisive
lemma stops an abstracted application just before its call: the guard can
terminate with a branch closure, and the dispatcher body can terminate with
the next encoded state, without assuming the recursive call terminates.
Positive CEK prefixes compose through that call under arbitrary
continuations. An increment-only initialization lemma reaches the loop from
the actual compiled term. `unlambdaDivergencePreserving` inherits
`unlambdaComplete` exactly; all eleven stronger witnesses are now proved.

The next stage was to move divergence preservation into `TuringComplete` and
remove the temporary extension, migrating every client and document. MU’s
Lean sources remain unchanged. Validation of this proof-only milestone:
full build passes (8,945 jobs), and all 770 axiom reports are clean.
The complete test suite will be rerun after the interface refactor.

## 2026-09-06: divergence interface, ten stronger witnesses, and Unlambda groundwork

Added `DivergencePreservingTC` in `Langlib/Common/Computability.lean` as a
separate extension of `TuringComplete`. Its divergence field constrains the
exit itself: every finite target fuel budget on a divergent URM input must
yield `.outOfFuel`. This rules out both errors and spurious normal halts
whose output the decoder rejects; a decoded-result iff alone would not.

Proved `halts_iff`, `result_iff`, `output_valid`, and `error_free`, plus
`halted_run_result` and `TuringComplete.simulates_at_completed_run`. The
latter compares completed runs at a common larger fuel using lawfulness,
so even the old interface excludes early errors on halting source inputs.
The new field supplies the divergent-input case. The consequences, shared
progress helpers, new witnesses and Unlambda groundwork are in the axiom
audit.

All eleven existing TC witnesses, their compilers and derived Turpentine
compilers remain unchanged. Their claim is forward answer preservation;
ten separate divergence-preserving witnesses now inherit them exactly.
Whitespace and Subleq prove positive block progress, FRACTRAN proves
nonempty rule simulation including self-jumps, Thue and Piet continue their
dispatchers, Brainfuck and Velato iterate terminating counter bodies, and
SKI proves positive head reduction plus strictness of compiled continuations.
Ook and Brainloller transport the Brainfuck result, with Brainloller’s
pixel-walk obligation still separate.

Unlambda now has positive fragment-job execution, exact zero-output buffer
preservation, positive strict-fixed-point unfolding under arbitrary
continuations, and unconditional error freedom. Its guard/body path back to
the recursive call still needs an operational proof; no stronger witness is
claimed for it. Progress and this remaining obligation are tracked in
[the migration table](divergence-preservation.md#witness-migration) and
Stage 8 of the plan. The documentation and language READMEs now make this
distinction, and the contribution policy explicitly rejects a decoded-result
iff as a substitute for the execution obligation. MU's proof development is
unchanged; it still has no TC witness to upgrade.

Validation: full `lake build` passes (8,945 jobs). The expanded axiom audit
has 758 reports, all using only `propext`, `Classical.choice`, and
`Quot.sound`, or no axioms. All 1,700 golden/compiler tests and both Velato
round-trip checks pass.
Available external differential tests pass six cases; other sections skip
when their runner or reference interpreter is unavailable.


## 2026-09-06: MU extracts marker bits and branches through reusable code

`LowTrit.lean` extracts the low bit of an arbitrarily wide zero/one marker
with two crazy operations. The first scratch starts at `...2220`; the
second can contain either previous result bit. The first operation collapses
all higher trits, and the second leaves the marker's low bit as natural zero
or one. Running the same operations with an all-ones accumulator restores
the first scratch and leaves one in the second. `pair_call` executes both
operations and the connecting pointer reset in nine real steps, preserving
code, records, both widths and I/O. `test` and `reset` specialize it;
`marker_zeroOne` establishes the extraction precondition throughout a
rotation, and `test_marker` connects an actual call's result to divisibility
of the rotation count by the state's current width.

`BitBranch.lean` proves a conditional jump through a natural bit in two
steps for one and three for zero. The zero path executes the no-op at
address 1 before the stable jump at 2; the one path lands on 1 and proceeds
directly to 2. The extra data-pointer increment selects the other adjacent
continuation word. Both paths encrypt address 1 exactly once within its
`74/70` no-op orbit, preserve both continuation landings, and leave the
accumulator, widths and I/O unchanged. Its frame preserves caller code,
flags and records placed outside addresses 0, 1 and the two target landings.

`bit-branch.mu`, the seventh generated runtime source, initializes that
no-op and tries flags `0,1,1,0`. Each outcome runs in both no-op phases;
the four continuations are reached at instructions 10, 13, 16 and 20,
followed by a halt at 21. Fifteen new tests cover initialization, flags,
records, both phases, untouched nonempty input, strict loading, and the
halt boundary at starting widths 10 and 37. The complete source is given
in sparse transliteration in the spec.

The nine-step extractor's result is adjacent to fixed restoration/return
words, rather than independent branch continuations. `PaddedCrazy.lean`
resolves that record-space conflict: its seven-step working call visits
two no-ops twice, restores every code word, and leaves two free slots
immediately after the result. Two adjacent operand records execute in
fourteen steps without a pointer reset. `LowTrit.test_padded` proves the
marker test through this layout, preserving both branch continuations,
return landings, code, widths, I/O and the remaining memory frame.

This does not yet close a marker scan. The padded test returns with its
data pointer beyond the result and records; the caller must reposition it
for dispatch, restore that move's code on both paths, reload the marker and
all-ones constant, and connect scratch reset to the next iteration.
`CONTRIBUTING.md` records the need to check record compatibility. The plan,
audit and runtime account distinguish these proved primitives from a
terminating scan and the remaining completeness simulation. The new source
tests dispatch on prepared flags; it does not claim to initialize or connect
the extractor.

Validation: full `lake build`, all 1700 `lake test` cases and both Velato
round-trip checks pass. All 672 axiom-audit reports use only standard
logical axioms. The generator's `--check` passes; the new source's sparse
transliteration matches byte for byte. Both documented 21-step runs halt
successfully with no output. The padded-call additions are proof-only and
were built and audited after the unchanged executable regression run.


## 2026-09-06: MU repeatedly grows using one reusable marker

`GrowingMarker.lean` connects rotation, width growth and marker reset in
87 actual MU instructions. A 15-step entry route and an eleven-step return
route connect the existing services. `cycle` doubles the width, regenerates
one in the same marker cell and restores the complete resident invariant.
`repeat_cycles` reaches width `2^n*w`; `unbounded_width` gives actual runs
above every fixed bound, and `neverHalts` covers every fuel prefix. Input,
output, constants, marker-adjacent records and future distant return reads
are preserved. This is unconditional growth; scan exit, carry/borrow,
conditional overflow retry and the completeness simulation remain open.

`MarkerCycle` now supports either its original reset continuation or the
growth continuation, with a precise memory footprint for each. Its original
public interfaces remain available. `Routing.lean` extracts the control-step
lemmas shared by both cycles. The new routes use eighteen additional no-op
cells; kernel-checked encryption orbits describe every reachable phase.

The sixth generated source, `grow-loop.mu`, initializes all 24 runtime
no-ops and the reset constants in a finite startup. It reaches the first
rotation entry at instruction 1331 and returns every 87 steps thereafter.
The default setup reaches width 18, then grows to 36, 72 and 144; starting
at 37 reaches 74, 148 and 296. Seventeen new tests inspect both routes,
restored marker and code, constant values, records, and untouched nonempty
input. The source has 12006 cells; `returns_of_fill` checks the new seed
phase and proves that even the smallest permitted distant read lies beyond
the source. `CONTRIBUTING.md` records this source-size check for future
initializer changes. Finite synthesis identities are proved; the complete
source-to-resident-invariant theorem remains open and is tested by execution.

The runtime account, proof tracker, audit, plan, spec and README now track
this milestone and its remaining obligations. The spec includes a complete
sparse transliteration of the new source.

Validation: full `lake build`, all 1685 `lake test` cases and both Velato
round-trip checks pass. All 654 axiom-audit reports use only standard
logical axioms. The runtime generator's `--check` passes, and the spec's
new transliteration matches the generated source byte for byte. Both
documented 1592-step runs produce the expected fuel diagnostic with exit
status 2 and no program output.


## 2026-09-06: MU rotation and reset share one reusable marker record

`MarkerCycle.lean` closes the routing gap between rotation and marker reset.
A nine-instruction route rotates the marker at 3200 using code at 529,
restores the rotor and router, and enters the existing reset. A seven-step
return route closes the cycle. `cycle` proves the resulting 50 actual MU
steps restore `Ready w`; `repeat_cycles` proves arbitrary repetition;
`neverHalts` covers all fuel prefixes, including those inside a cycle.
Both widths and all input/output state are preserved. The marker's adjacent
records remain `3201:270` and `3202:529` throughout; no fresh marker,
constant or record is consumed.

Address 529 is both a rotation instruction and a reset landing. Preserving
its printability was insufficient to compose the old reset theorem with
this route. `MarkerReset.Traced` now records the exact number of encryptions
there, and `call_traced` proves there are two. `call_rotator` specializes
this to preservation of word 74. The old `call` and `call_power` contracts
remain available. `CONTRIBUTING.md` records the need to track exact phases
when a landing also serves as executable code.

The return route uses three no-ops at 526–528, alternating independently
between 74 and 70. Their closure, decoding, and rejection as direct source
instructions are kernel-checked. `initializer_values` checks the natural
operand pairs that synthesize them. The original `marker-cycle.mu`, generated
by `scripts/gen-mu-runtime.py`, contains 4202 source cells. Initialization
and a bootstrap reset reach the rotation entry after 76 instructions;
subsequent visits occur every 50 steps. The default setup reaches width 16,
and the same source works at 37. Fifteen new tests inspect both routes,
changed no-op phases, restored working words, constants and records through
nine cycles, with nonempty input left unconsumed.

This is a repeating rotation/reset routine, not a terminating scan or an
overflow loop: it has no exit branch and does not enter the growth service.
The symbolic theorem starts from `Ready`; complete loader/prologue
reachability is still tested by execution. The plan, runtime account,
proof tracker, spec and README now distinguish the completed shared-record
routing from integration with growth, scan exit, counter arithmetic,
source initialization and the remaining completeness theorem.

Validation: full `lake build`, all 1668 `lake test` cases and both Velato
round-trip checks pass. All 636 axiom-audit reports use only standard
logical axioms. The runtime generator's `--check` passes, the spec's
complete sparse transliteration matches the generated source byte for byte,
and both documented 526-step runs return the expected fuel diagnostic and
exit status 2 with no program output.


## 2026-09-05: MU regenerates a rotated marker without consuming constants

`Marker.lean` proves a constant-preserving path that clears any natural
containing only zero and one trits and rebuilds one. The initial accumulator
is loaded by rotating an all-ones constant, independently of width. No input
instruction or EOF assumption is needed. `zeroOne_power` admits a marker
`3^k` for any `k`, with no working-width bound.

`MarkerReset.lean` implements that path in 34 actual MU instructions:
six working calls, four pointer resets and two visits to a move/no-op router.
`call` and `call_power` restore the marker to one, preserve the resident
constants and return records, and restore the router phase. The frame also
preserves all memory outside the marker, router and printable continuation
landings. Input, output, output-closed state and both widths are unchanged;
the fixed pointer destinations require only `maxWidth ≥ 8`. These are
execution theorems through `run?`, not hypothetical marker updates.

The new original `marker-reset.mu`, generated by `scripts/gen-mu-runtime.py`,
has 4202 source cells. It bootstraps its constants, rotates the same physical
marker, resets it and halts without output in 103 instructions. At the
default width the setup reaches 16 and the marker becomes `3^15`; at width
37 it becomes `3^36`. The bootstrap enters with the future mask still zero,
so its first pass through the reset is covered by execution tests, not by
`call`. The resident reset entry is reached at instruction 61 and returns
at 95. Eleven new tests check both widths, intermediate marker and constant
values, restored router, unconsumed nonempty input, halt, and strict rejection.

The rotation wrapper is single-use. An unbounded caller still needs to
compose rotation, reset, and growth with compatible return records:
`work_call` binds the operand's adjacent record to the operation's code
address. Restored rotation and crazy-write records cannot simply be treated
as interchangeable. `CONTRIBUTING.md` records this requirement. The runtime
account, proof tracker and plan now distinguish the proved reset from this
integration, runtime scan exit, carry/borrow, source initialization, and the
remaining simulation theorem. There is still no MU completeness witness.

Validation: full `lake build` and all 1653 `lake test` cases pass, as do both
Velato round-trip checks. The axiom audit has 626 reports (606 with explicit
dependencies), all using only standard logical axioms. The generator's
`--check` passes; the spec's complete sparse transliteration matches the
source byte for byte; both documented 103-step runner commands halt with
exit 0 and no output.

## 2026-09-05: MU growth is now a reusable resident service

`ReusableGrowth.lean` proves an eleven-instruction growth call that restores
both working moves, returns through an unconsumed table, and preserves the
code's reusable no-op orbit. `call_resident` preserves a complete `Resident`
invariant: working code, return records, printable continuation landing,
and the distant return read for every future width, not only the current
one. The source operand and all other data and I/O are preserved. This
closes the previous growth-code restoration obligation; supplying a new
rotated one for overflow retry is still the caller's job.

The three middle cells use the closed encryption orbit 41, 102, 96, 60, 51.
All phases decode to no-ops at 437–439, but none is a legal source word there.
Both facts are kernel-checked. `Initialization.lean` supplies
`initialize_cell`, a three-step crazy/move/crazy write with explicit scratch,
target and code separation and width stability. Three checked value
identities instantiate the synthesis used by the example's initializer.
The complete loader/prologue composition remains a regression test, not a
symbolic initialization theorem.

`grow_return_of_read` factors the five-step growth segment around an
extensional distant-read hypothesis; the existing `grow_return` theorem
keeps its old statement as the fill-backed specialization. This lets
`Returns.frame` preserve reads across repeated calls. `Returns.of_fill`
establishes them from the actual natural-seeded fill and a finite source
prefix. `seed_return` checks the concrete example's fill. The loader phases
from the penultimate source address (7000), not the source length (7002).

The new original `grow-twice.mu`, generated by `scripts/gen-mu-runtime.py`,
contains 7002 source cells. It initializes the three no-ops, then calls the
same growth code twice using separate one-markers. Its default-width run
establishes width 18 and grows to 36 and 72; at starting width 37 it grows
to 74 and 148. Both runs halt after 63 instructions without output. Ten
new cases inspect initialization, both returns, code phases, marker values,
return records, the exact halt boundary, and strict-loader rejection.
Distinct prepared markers do not demonstrate unbounded marker reuse.

The runtime account, proof tracker and plan now distinguish the completed
resident service from remaining marker reset, runtime scan exit, carry/borrow,
overflow retry and general source realization. The README and spec include
usage and a complete sparse transliteration, verified against the generated
source. `CONTRIBUTING.md` records the fill-phase and runtime-no-op/source-word
distinctions so subsequent work does not repeat those mistakes.

Validation: full `lake build` passes. The expanded axiom audit passes with
only standard logical axioms in all 600 dependency reports, including all
11 new public results. The generator's `--check` passes, and both documented
63-instruction runner commands halt with exit 0 and no output. `lake test`
passes all 1642 cases and both Velato round-trip checks.

## 2026-09-05: MU fixed-cell runtime foundations replace the rejected tape design

The reworked construction now has five proof modules, described in
[the runtime account](malbolge-unshackled/runtime-proof.md). The interpreter
and existing URM-to-`Counter` compiler remain unchanged. There is still no
`TuringComplete MalbolgeUnshackledLang` witness.

* `Counters.lean` represents finitely many unbounded natural counters in
  fixed cells. Constructive initialization preserves any original fill and
  all cells outside the finite register file. Update and capacity lemmas
  state the arithmetic boundary conditions without pretending to execute MU.
* `Runtime.lean` proves actual three-step rotate/crazy and pointer-reset
  calls: restore the working code, return through preserved tables, expose
  operand changes, and preserve the rest of memory and I/O. Ordinary
  pointer resets explicitly require width stability.
* `Rotation.lean` connects normalized MU values to padded rotation windows.
  It proves full-cycle restoration and the one-marker low-trit test,
  including absence of early return.
* `RotationLoop.lean` gives a concrete six-instruction loop, arbitrary
  repeated passes of that same finite code, and restoration of the operand
  after a full window. There is no assumed pass-existence premise. There
  is also no runtime marker branch: attaching one remains essential.
* `Growth.lean` proves five actual instructions that grow the width and
  return through residue one of untouched fill. It exposes all five code
  writes; restoration for repeated growth remains open.

Two original 3004-cell source examples, `rotation-loop.mu` and
`grow-once.mu`, are generated by `scripts/gen-mu-runtime.py`. Fourteen new
regression cases use the actual loader and evaluator: inspect pointer and
operand restoration over repeated cycles, grow 16 to 32 and 37 to 74,
check the exact halt boundary, and reject the permissive data under strict
loading. The source generator has a drift check, and the spec gives complete
sparse transliterations. These tests do not replace the still-needed
symbolic source initialization theorem.

The plan and tracker distinguish checked foundations from remaining scan
exit, carry/borrow arithmetic, repeated growth, initialization and simulation.
`CONTRIBUTING.md` now records that arbitrary proof-indexed iteration is not
an implemented exit test, and that code restoration alone does not restore
operands or a complete calling convention. The base module's remaining
width-bound and escalator overstatements have been corrected.

Validation: full `lake build` and `lake env lean scripts/axioms.lean` pass;
all 23 new public foundation results are audited, with no nonstandard axioms.
The generator's `--check` passes. The documented runner commands were run:
the loop exhausts 195 instructions with exit 2; both growth runs halt after
17 instructions with exit 0 and no output. `lake test` passes all 1632 cases
and both Velato round-trip checks.

## 2026-09-05: MU proof audit rejects the infinite blank-tail invariant

The MU completeness effort is re-scoped. There is still no
`TuringComplete MalbolgeUnshackledLang` witness, and the previous assessment
that a walk pass was the only substantive missing piece was incorrect.

New kernel-checked results in
`Langlib/Computability/MalbolgeUnshackled/Obstructions.lean`:

* `finite_natural_support` bounds the natural keys of any finite memory map.
* `restTable_adjacent_nonzero_lead` shows that, with natural fill seeds,
  at least one of any adjacent pair of natural addresses has a nonzero
  repeating trit.
* `not_regMem_of_natural_fill` combines these into a contradiction for the
  old `RegMem` invariant, for any positive stride and nonempty register
  file, even after finite writes. It assumes the fill equation; the
  general mutable-loader invariant remains separate work.
* `no_adjacent_two_cycle_crazy` rules out instantiating the three-instruction
  branch as consecutive period-two working cells.
* `flag_branch_mark_reuse` shows that reusing the marked branch's consumed
  operands yields zero instead of its intended target.
* `widthBounded_update_d` makes explicit that the stored-value invariant
  places no restriction on the data pointer. The old inference from a
  finite alphabet to bounded storage was unjustified.

The [proof audit](malbolge-unshackled/proof-audit.md) records the corrected
scope of the existing theorems and a revised fixed-cell counter design.
It draws on Matthias Lutter's MU Brainfuck interpreter, whose source is
copyright-dated 2016, predating the MalbolgeLisp evidence cited before.
The HeLL source, LMFAO 0.1.5, and Johansen's canonical Haskell interpreter
were inspected; source hashes are recorded, and no external code is copied.
The useful runtime mechanisms are a rotation-width scan, carry/borrow
arithmetic, and width growth with a return path. These still need Lean
operational proofs; the audit gives their contracts and composition with
`Counter.counterProgram_spec`.

The plan, tracker, spec, and earlier construction notes now distinguish
these obligations from proved algebra. `CONTRIBUTING.md` records the need
for reachable invariants and source realization when a target uses raw
images: a convenient periodic background is not necessarily loadable.

Validation: `lake build` passes. The global axiom audit passes after fixing
18 pre-existing stale Whitespace references to lemmas moved into
`Langlib.Turpentine.Certified.Shared`; all audited dependencies are standard
Lean axioms. `lake test` passes all 1,618 tests and both Velato round-trip
checks. `git diff --check` is clean.

## 2026-09-03: a hand-written Turpentine backend for Unlambda

`Langlib/Languages/Turpentine/Compile/Unlambda.lean`, the backend
`docs/unlambda/compiler.md` had been describing as the most interesting one
in the library that did not exist. It exists, it takes the whole of
Turpentine — arrays, `readInt`, `readByte`, byte-exact output — and all
twenty conformance programs go through it and agree with the reference
interpreter.

It is the only backend here that does not compile a machine to a machine,
because Unlambda has no machine in it. A state is a nested pair of the
program's variables, a statement is a function from one state to the next,
`;` is composition, `if` is a boolean applied to two thunks, `while` is a
fixed point, an `int` is a sign and a Scott numeral, and an array is a Scott
list. The compiler builds all that as a lambda term with real binders and
then removes the binders by bracket abstraction, which is the step the
completeness proof already knew was delicate.

**What call by value cost.** Three things, one known in advance and two
found by watching a program not finish.

* The textbook clause ``[x] E = `kE`` for an `E` without `x` is unsound: it
  evaluates `E` when the closure is built. `abs` keeps it for *value
  expressions* only, exactly as `Langlib/Computability/Unlambda/Main.lean` does,
  and the `s` expansion everywhere else is what makes a thunk a thunk.
* **Constructors have to be strict.** A pair built as `λf. f (x+1) y`
  captures the expression, not the value, and recomputes it at every
  projection; a loop's state is a chain of such pairs, so the cost of
  reading a variable doubled per iteration. A twenty-iteration loop could
  not finish in 200 million steps.
* **Everything that crosses a binder has to be a value.** The runtime
  library is bound by two dozen `let`s, and a `let` is an applied
  abstraction. A subterm that is not a value cannot be carried past a binder
  with one `k`; it is expanded with `s`, which doubles it. Two dozen
  doublings is sixteen million, and `cat.turp` would not compile. Writing
  each library entry as `λa b. Z F a b` rather than `` `ZF `` makes it a
  lambda, hence a value, hence one `k` per binder; the compiled body goes in
  as a thunk and is forced at the end for the same reason.

**Where `c` is unavoidable.** `?x` and `@` answer `i` or `v`, and `v`
swallows whatever the failing branch would have returned, so there is no way
to see a mismatch from the inside. Every test therefore runs under a
captured continuation and the *match* is what leaves; the code after the
test is the else-branch. `cat.turp` compiles to 22 342 applications with
exactly two `c`s in them, and no `d` anywhere — bracket abstraction over `s`
already delays everything that has to be delayed, which is the same reason
the completeness proof never needed either.

**Bytes, not text.** Unlambda is the one target whose compiled file is not
text: `.x` carries the byte it prints, so a program that prints byte 200
contains byte 200, and a `String` holding it would be written out as its
two-byte UTF-8 encoding and parse back as something else. The backend emits
a `ByteArray`, `Langlib.Unlambda.parseBytes` reads one (new, beside
`parse`), and `Artifact` in the runner grew an optional byte payload for it.
`cat.turp` compiled this way echoes binary input byte for byte.

**Costs.** `hello.turp` is 212 bytes and 412 steps; `99bottles.turp` is
12.4 kB and 8.8 million steps; `power.turp`, which doubles to 16384 an
increment at a time because the arithmetic is unary, is 34.7 million. The
certified route on the same six-line `sum.turp` emits 41 235 167 bytes where
this one emits 3 868. All of it is measured in `docs/unlambda/compiler.md`.

**Also.** `Langlib/Tests/CompileUnlambda.lean` (28 cases, including the ones
where a Turpentine runtime error becomes `e` and the run simply stops);
unlambda added to the conformance suite, which is now 20 programs times 8
runners; `scripts/gen-unl-examples.sh` regenerating three compiled examples
under `Langlib/Examples/Unlambda/compiled/`; `docs/unlambda/compiler.md`
rewritten from a plan into a description.

## 2026-09-03: Malbolge Unshackled gets a walk, and a two-operation branch

Two pieces of the Turing-completeness effort, both in
`Langlib/Computability/MalbolgeUnshackled/Main.lean`, both axiom-clean. There is
still **no `TuringComplete` witness**; the tracker
`docs/malbolge-unshackled/completeness-progress.md` says what is left.

**A branch into two natural addresses, in two crazy operations.** The file
had two branches and neither was the right tool for a loop. `branch_arith`
reaches arbitrary targets in seven operations and consumes four shaping
constants, which a loop must restock every pass. `flag_selects_address`
costs three instructions but lands `d` on address 0 or 1, which is where
execution begins. `flag_branch` pays one crazy operation more than that and
buys those two addresses back: against `...111` and the natural `2 * 3 ^ j`
it sends a blank flag to the address `2 * 3 ^ j` and a mark to `3 ^ j`, for
any `j` the compiler likes, both naturals, both anywhere in memory. The
first constant is the `...111` the ladder and the register probe already
keep. `flagAddr_gadget` runs it in three instructions, two `crazy` cells
and a `movd` that leaves `d` on the cell holding the address.

Two is the least possible, and the argument is the same tritwise one that
runs through the rest of this development. A single column of the crazy
table sends the blank flag to `1` or `2` at *every* trit position, so a
one-operation result repeats `1` or `2` for ever, is not a natural, and a
jump into it lands in the memory fill, which `restTable_not_printable` says
can hang. Two columns composed give seven of the nine possible pairs,
including `(0, 0)` above position `j`, which keeps both targets natural,
and `(2, 1)` at `j`, which makes them differ. This does not contradict
`no_accumulator_flag`: that rules out computing a *uniform* value from the
accumulator, and neither target is uniform.

One asymmetry a gadget author needs. On the blank path the second constant
cell ends holding exactly what it held, so it restores itself; on the mark
path both constants are consumed and a pass must restock them.

**The walk, which was the blocker.** Everything built before this batch
reached statically known addresses; nothing did data-dependent iteration,
and `inc`, `dec` and the loop condition all need it. Two of its three parts
now exist. `walk_iterate` is the induction: `n` passes of a `k`-step pass
cost `k * n` steps, where `n` is a tape length rather than anything the
compiler knows, and the layout makes a pass free of address arithmetic
because `regAddr`'s slot stride *is* the pass length. `walk_branch_target`
is the exit: feeding the cell a walk stands on to `flag_branch` aims
control at `3 ^ j` while marks remain and at `2 * 3 ^ j` at the first
blank, so the walk stops exactly at the tape boundary.

**What a pass finds ahead of itself.** A walk steps into cells no loader
wrote, and `RegMem` asks every cell above a tape's length to be blank.
Untouched cells hold the memory fill, and the fill is never blank:
searching every pair of printable seeds finds no pair putting `...000`
anywhere in the six-value table. That is measured rather than proved, and
`leadAt_even` with `crzTrit_zero_ne_zero` is the structural reason. So a
pass has to normalise the cells it is about to use.

`fillAt_slot` makes that affordable and closes the circularity the first
design runs into. With a slot stride divisible by 6, a given offset holds
the same fill value in every slot, because the fill sees the address only
through its residue mod 6. So the value ahead is a compile-time constant,
`crz_two_steps` converts it in two operations, and a pass can write the
*next* slot's constants using its own. The constant block propagates one
slot per pass, the loader writes slot 0, and the walk carries it forward:
the escalator argument applied to data rather than to addresses.

What is left is one pass — the hypothesis `walk_iterate` takes — with three
concrete jobs in it: re-entry, which `two_sweep` is for, restocking the
branch's constants, and propagating the block. The blocker is now that
narrow.

## 2026-09-03: the Velato backend is verified, input included, and the build is warning-free

**A `TraceLang` for Velato.** `Langlib/Languages/Velato/Trace.lean` proves
the two bookkeeping laws (the trace's output events are the output; its
input events followed by what the cursor has left are the stream) and
`Velato/Faithful.lean` the faithfulness law. Faithfulness needed one idea
the whitespace and subleq proofs did not: Velato's interpreter runs whole
sub-runs rather than single steps, so the two-stream simulation must also
say that the two runs *consume the same bytes*, or a statement could not be
followed by the rest of its block. `Faithful.seq` is that composition, and
`instance : TraceLang VelatoLang` sits beside `ProgLang VelatoLang`.

**The hand-written Velato backend is proved correct on a fragment,
behaviourally.** `Langlib/Languages/Turpentine/Compile/Certified/BespokeVelato.lean`
gives `bespokeVelato : TurpentineCompiler VelatoLang` and `bespokeVelatoIO :
CertifiedCompiler BehavesWithAnswerNulFree VelatoLang` with `encodeInput`
**and** `encodeTrace` both the identity: the compiled program runs on the
source's own stream and performs its events, reads included. It is the
first behaviourally verified backend in the library whose fragment reads.
The fragment is scalar `int`/`bool` with no initialisers, the expression
language without `/` and `%`, `if`, `while`, `print`/`println` of strings,
integers and booleans, and `x := readByte()`. The specification restricts
the stream to one with no NUL byte, because Velato's `Input` stores `0` for
a NUL and at end of stream alike and the backend cannot tell them apart;
that is stated in the specification rather than hidden in `encodeTrace`.
The proof is about the shipped generator: its `partial` was removed and its
`for` loops rewritten as recursion, with no change in behaviour.

**A divergence found on the way.** `printByte` is out of the fragment for
a real reason, not a proof gap: Velato prints a `char` as the UTF-8
encoding of its code point, so `printByte(200)` writes `C3 88` where
Turpentine writes `C8`. `docs/velato/compiler.md` records it and a golden
test pins it.

**Shared source-side lemmas.**
`Langlib/Languages/Turpentine/Compile/Certified/Shared.lean` now holds everything
the certified backends need from Turpentine and nothing about any target:
fragment predicates, evaluator inversion, `evalExpr_hasTy`, the `initEnv`
unfolding, the `answer` epilogue and its decoder, and the two
specifications. `BespokeWhitespace.lean` imports it and shrank from 4449 to
about 3840 lines with no change to what it proves.

**Zero warnings.** The whole project now builds without a single Lean
warning: 183 unused `simp` arguments, unused hypothesis names and a few
never-executed tactics in `Computability/Fractran.lean`, and a local
variable named `S` next to the `S` combinator in `Computability/Ski.lean`.

Tests: 1570, all passing (43 new for the Velato backend).

## 2026-09-02: velato, and a completeness proof that had to work differently

Velato (Daniel Temkin, 2009) is a language whose source code is a MIDI file:
the pitches, in the order the file sounds them, are the program. Commands
are intervals from a command root the composer may move at will, so a
program keeps its meaning under transposition — and a piece of music is, if
the intervals fall right, also a program.

**The language.** `Note.lean` pins the two readings of an interval the
language needs (exact for commands, coarse for expressions, which is what
lets a composer stay in the scale) and the digit encoding that falls out of
reserving the unison and the perfect fifth. `Parser.lean` follows
velato.net's tables, cross-checked against the 2009 C# reference; where the
two disagree the spec page says which we follow and why. The substantive
case is `If`, whose branch in the reference reads no condition, advances an
extra note, and loops on a tautology, so it cannot return.

The parser records what each note turned out to be, in the parser rather
than in a second pass, so the labels under an engraved staff cannot drift
from the grammar that produced them.

**Turing complete, and the proof is the interesting part.** Every other
backend in the library lays the counter machine's registers out side by
side: brainfuck a tape column each, subleq an address, Piet a stack slot.
Velato cannot — a variable is a MIDI note, so a program has at most 128 of
them, while `counterProgram` may ask for arbitrarily many. One register per
variable would be a compiler that works for small programs and fails for
large ones, which is precisely the failure
`docs/agent-brief-completeness.md` warns about.

So the unbounded state lives *inside* a cell rather than across cells. The
whole register file is one number, `2^w0 * 3^w1 * 5^w2 * ...`, in a single
variable — middle C; the other 127 are free. Increment multiplies by the
register's prime, decrement divides by it, and "is register r nonzero" is
"does the r-th prime divide the number". The primes are built by a
Bertrand-bounded search rather than taken from `Nat.nth Nat.Prime`, which is
noncomputable: `TuringComplete.compile` has to be a function that runs, and
the differential tests run it.

**And the theorem stands on a semantic decision, which is stated rather than
assumed.** The encoding needs unbounded integers. The reference compiler
emits C# `int`; under *that* reading Velato has at most 128 variables of
finite width, hence a finite state space, hence a decidable halting problem
and no completeness at all. The specification names no width, so both
readings are defensible; `docs/velato/spec.md` gives three reasons for
taking the unbounded one and states the finite-state converse as an open
proof rather than pretending the question does not arise.

**Compilers.** The hand-written Turpentine backend is the shortest in the
library, because Velato is not a machine: it has `while`, `if`/`else`, named
variables and unbounded integers, so the backend is nearly a direct
translation. Its content is in the four places the languages differ — no
arrays, Euclidean versus truncating division (corrected, which needs
statements, which is why the expression compiler returns a prelude),
short-circuiting that has to survive that prelude, and no boolean type. All
fourteen compilable examples produce byte-identical output to the reference
interpreter. `derivedVelato` is the certified route, one line off the
completeness witness.

**Seeing and hearing it.** A Velato program is music, so the runner engraves
it — the same `Scene` going to PDF, SVG and a raster image, with no
dependency outside Lean, because requiring an SVG rasteriser to look at a
program is a poor trade. It also synthesises audio directly, so
`scripts/velato-audio.sh` plays a program on a bare checkout.

**A finding from the differential tests.** VelatoPy prints a `char` as a
character only for codes in `32 … 127` and prints the number otherwise, so a
program ending in a newline prints a trailing `10` there. The C# compiler
emits a character literal and writes it whatever it is. We follow the C#
reference, which the Python one names as definitive; `docs/TESTING.md`
records it.

**Two claims corrected during the work.** A docstring said the derived
backend's output was "much shorter" than other targets'; it is not —
`sumsq.turp` is 509 kB against subleq's 1.8 kB, because the five statements
carry primes as decimal numerals and Velato spends a note per digit. And a
generated example's header claimed seven of its notes were the shadowed
tune's; three were. Both now report measured numbers, the second computed by
the generator so it cannot rot.

**On hiding a program inside a tune**, which is the obvious game and worth
being precise about: you cannot make a Velato program play an arbitrary
melody, because within a statement the pitch classes are forced. What you
can do is change key at every statement boundary, which is what velato.net
says root changes are for, and that gets about a third of the notes onto
the tune. The examples report what they actually achieved. The reliable
technique is the author's own: the program is the first track and the tune
is the tracks after it, which the language ignores.

1527 tests pass; the axiom audit reports only `propext`,
`Classical.choice` and `Quot.sound`.

## 2026-09-02: one policy file, two names

`AGENTS.md` was a hand-made copy of `CLAUDE.md` and had already drifted: it
was missing the "Example programs" requirement, the whole graphical-languages
policy (derived images, `scripts/render-docs-images.sh`), and the
`Turpentine/Compile/Certified/` section with its warning about name resolution. An
agent that read `AGENTS.md` — Codex, Cursor, Gemini CLI all look for that
name — was working from stale rules.

`AGENTS.md` is now a symbolic link to `CLAUDE.md` (git records it as mode
120000), so the two cannot diverge again: there is one file, reachable under
either name. `CLAUDE.md` opens with a "This file" section saying so, telling
a tool that rewrites the link into a regular file to restore it, and pointing
at `CONTRIBUTING.md` for the contribution checklist, which the conventions
file never referenced before. `CONTRIBUTING.md` points back.

## 2026-08-31: lawfulness is now required, not optional

Follow-up to the entry below: `CertifiedCompilerNoIO`, `CertifiedCompiler`
and `TuringComplete` now **require** `LawfulProgLang` (the I/O-aware one
also `LawfulTraceLang`) instead of offering lawful upgrades on the side.
The reason is semantic, not stylistic: against an unlawful interpreter the
`∃ fuel` conclusion can be satisfied by treating fuel as an input channel —
halt with the right answer exactly at fuels that encode a halting URM
trace — so a language whose programs compute nothing could have claimed a
completeness witness. `halted_stable` pins fuel to its budget role, which
makes the requirement part of what the statements mean. Since every
language already has its instance, nothing else changed: the whole library
rebuilt without touching a single witness or bespoke proof.

## 2026-08-31: lawful languages — the `∃ fuel` guarantee is cashed

An adversarial pass over `Langlib/Common/Compilation.lean` and
`Langlib/Common/Computability.lean` found the definitions sound but with
one structural soft spot and two misleading docstrings, all now fixed.

* **`LawfulProgLang` / `LawfulTraceLang`.** `ProgLang` had no laws, so the
  `∃ m` concluding every correctness statement said nothing about the fuel
  bound a runner actually picks. The new classes state fuel stability (a
  completed run, trace included, is a fixed point of more fuel);
  `CertifiedCompilerNoIO.correct_stable`, `CertifiedCompiler.correct_stable`
  and `TuringComplete.simulates_stable` upgrade every `∃ m` to "every fuel
  from some point on". **Every `ProgLang` tag has an instance** — proved
  per interpreter in `Langlib/Languages/<L>/Stability.lean` by one uniform
  induction (brainfuck's lemma serves Ook! and brainloller too; the bounded
  Befunge-93 core's proof lives next to that model) — and all three
  `TraceLang` languages have the trace counterpart.
* **`TuringComplete` docstring** now says out loud that the proposition
  alone is not the completeness claim: a `Classical.choice` witness could
  inhabit it for Deadfish, no axiom audit would object, and what rules the
  cheat out is the convention that `compile` is a plain `def` that `#eval`
  can apply.
* **`halting_decidable` docstrings** claimed "no `BoundedStorage` witness
  coexists with a `TuringComplete` witness" as if it were a corollary. It
  is a meta-theorem about computable witnesses, and by a subtler argument
  than halting-problem undecidability (the one-directional `simulates`
  breaks the naive reduction; the recursion theorem does the work). Both
  docstrings now say so, and the dangling `docs/computability.md` reference
  points at `docs/agent-brief-completeness.md`.
* **`TraceLang.trace_faithful`.** The trace laws could not stop a trace
  from underreporting its reads; the new third law can: a halting run,
  replayed on any stream sandwiched between the claimed reads and the
  original, is the same run, so omitting a read the behaviour depends on is
  refuted by the truncated stream. Proved for whitespace and subleq by a
  two-stream simulation (`Langlib/Languages/<L>/Faithful.lean`; the line
  reader's half lives in `Langlib/Common/Io.lean` as
  `readLineGo_faithful`), and for FRACTRAN for free. Finding the right
  statement was the work: the law is false for erroring runs — whitespace's
  `readnum` parse error prints the offending line while consuming nothing —
  which is why it covers halting runs only, and the docs say so.

## 2026-08-31: a Turpentine backend for Malbolge itself

`docs/malbolge/compiler.md` used to say **not planned**, and gave a good
reason: Malbolge is 59049 words of 59049 values, so it is not Turing
complete, so no total backend from a Turing-complete source can exist and
any backend would be bounded by the machine rather than by our effort.
That reasoning is still correct. What it got wrong was the conclusion —
the demonstration turns out to be cheap, and it fits more than expected.

`Langlib/Languages/Turpentine/Compile/Malbolge.lean` compiles every
input-free Turpentine program whose output fits. The trick is to give up
on looping in the target: **nothing it emits is executed twice**, so
self-encrypting cells cost nothing (nothing reads them again) and
position-dependent opcodes cost nothing (the assembler picks each cell
after it knows the address). Control flow — loops, `if`, arrays,
arithmetic — is resolved by running the source on Turpentine's own
interpreter at compile time, exactly as the Unshackled backend does.

Three things had to be worked out that Unshackled did not need.

*Getting `c` and `d` apart.* `movd` reads a loaded cell, and a loaded cell
is a **byte**, so nothing in the image can name an address in the data
row. `rotR` is the way out: it is a *cyclic* rotation of the ten-trit
word, so rotating a byte carries its low trits over the top and
manufactures a large value from a small one. The prologue rotates one
cell as many times as the layout needs, and `seeds` tabulates every
address reachable that way. A `jmp` at address 2 skips `c` past addresses
3..125, which is what frees them to hold the pointers at all.

*The cost of a byte.* Constants come from Olmstead's loader oversight —
characters outside `33..126` are stored unchecked — which leaves 163
usable values at every address. Because they are bytes, their top four
trits are zero, and against a zero trit the crazy operation is a fixed
map, so the accumulator's top four trits are not steerable. That would be
fatal if the target were a value; it is not, because `<` writes
`a mod 256` and some 230 of the 59049 words end in any given byte. On the song,
9% of bytes need no operation at all, 35% need one and 56% need two:
**about two and a half cells of code per byte**.

*Where the wall is.* The two rows are the same length, because `d`
advances whether or not the instruction reads memory. So two words go per
word of code and the longest code row the machine has room for is
**29157 cells** — checked in Lean, not asserted. A program that wants more
is refused with the number of bytes that would have fitted:
`the program prints 25592 bytes ... enough for the first 15191`.

**The song fits.** `Langlib/Examples/Malbolge/compiled/99bottles.mal` is
57514 of the 59049 words — 97.4% of the machine — and halts in 28363
cycles, one per code cell, against about fifteen million for Iizawa et
al.'s hand-written `99bottles.mal`, which has real loops where this has
none. They print the same 11459 bytes;
`Langlib/Tests/CompileMalbolge.lean` runs both and compares digests, which
is the prettiest test in the file.

Also checked in: `compiled/hello.mal` (247 cells), `sort.mal` (197),
`primes.mal` (251) and `sieve.mal` (308), all derived files written only
by `scripts/gen-mal-examples.sh`, which verifies each against its source's
output and whose `--check` catches a stale one. `sort.mal` is quoted in
full on the spec page in a stated transliteration and read line by line,
because at 197 cells the whole layout is visible: the descending no-op
ramp, the doubled letters of the rotation loop (`rotr` and `movd` are
adjacent opcodes, so the same character at consecutive addresses means one
then the other), the alternating code row, and the data row of constants
with padding under every `out`. That program never uses the crazy
operation at all — every byte it prints is one ASCII character, and
rotating right is division by three when the low trit is zero, so it
prints `1` by rotating 147.

Input stays out, and not for want of room: `crz` is tritwise, so no chain
of crazy operations against compiled-in constants can produce a value that
*depends* on a byte the compiler has not seen. That is the same
obstruction that stops the Unshackled backend, where there is no size
bound at all.

Registered as the `malbolge` target of `turpentine compile --to` and
`exec --via`; 50 new tests in `Langlib/Tests/CompileMalbolge.lean`;
`docs/malbolge/spec.md`, `docs/README.md`, `docs/PLAN.md`,
`docs/TESTING.md` and the language README updated to match.

## 2026-08-31: Piet programs as PNG, both directions

`docs/piet/spec.md` gained a **Programs as PNG** section. PPM is what the
runner reads and PNG is what everyone else trades, so the section works the
conversion through in both directions: `scripts/ppm-to-png.py` for a
whole-number enlargement (one block per codel, `--no-grid`), `sips` for a
one-pixel-per-codel thumbnail, and `sips -s format pbm` back to a PPM the
interpreter runs at `--codel-size 24`. Every command on the page was run;
the round trip really does print `7`.

The lesson the failures teach is the point of the section: a smoothly
resampled program is not a program. `sips -z` blends the block edges and
the interpreter stops on `unknown colour (127,0,0)` at the second codel,
and the grid-line variant is off in both dimensions besides. Enlarge with
nearest neighbour or not at all.

`docs/piet/img/add.png` is the first PNG on the Piet page and, like every
picture there, a derived file: `scripts/render-docs-images.sh` generates it
with the very command the section quotes, and `--check` now compares PNGs
in the Piet directory as well as SVGs.

## 2026-08-31: the beer song, in Turpentine and compiled to Unshackled

`Langlib/Examples/Turpentine/99bottles.turp` is the whole song, ninety-nine
verses down to none, in thirty-odd readable lines. It exists to be compared
rather than read: its 11459 bytes are byte for byte what Malbolge's
`99bottles.mal` prints and what the hand-built Unshackled port
`99bottles.mu` prints, checked with `cmp` and not by eye. It reads nothing
as written, so unlike `primes-mu.turp` and `sort-mu.turp` it needs no
input-free twin — it is already in the Malbolge Unshackled backend's
fragment.

**Compiled and checked in.** `compiled/99bottles.mu` is the third derived
artifact under `Langlib/Examples/MalbolgeUnshackled/compiled/`, and the
first one big enough to say anything about the backend's cost: 64886 cells,
92602 bytes, verified against the source's own output at rotation widths 10,
37 and 300. It is 82% of the 78790 cells the hand-written port spends on the
same song — the compiler's only direct comparison against a person, and it
comes out ahead. At 32346 code cells for 11459 output bytes it also pins the
cost model down at 2.82 cells per printed byte, the fixed 194-cell overhead
having finally vanished into the rounding (2.85 for the primes, 2.95 for the
greeting, 3.08 for the sort).

**One song, three suites.** The Malbolge suite rebuilt the song privately to
check `99bottles.mal`. That definition moved to `Langlib/Tests/BeerSong.lean`
so the Turpentine golden test can compare against the *same* string rather
than against its own output recorded after the fact — which is the only
thing that makes the new test say something.

**What is not tested by `lake test`.** `compiled/99bottles.mu` is in none of
the compile suites: one run costs some fifteen seconds, because the
interpreter's cost grows with the size of the program. It is checked by
`scripts/gen-mu-examples.sh`, which now compiles all three sources and runs
every program it emits — the same trade the hand-written `99bottles.mu`
already had.

## 2026-08-31: the matrices catch up, and two of them were lying

A documentation pass over every status table, prompted by the Malbolge
Unshackled backend landing without the top-level matrix noticing.

**The matrices.** `README.md`'s row for malbolge-unshackled still said
`planned`; it now names the bespoke backend, its source, and the two facts
that go together — the completeness claim is open, so there is no witness
to derive a compiler from, and the backend cannot compile `read`, because
reading needs the same machinery the completeness proof does. The list of
bespoke targets in the same file said three languages; there are eight, and
six of them are unverified rather than all of them. `Langlib/Languages/Turpentine/README.md`'s
example table was a two-column header over three-column rows, so a third of
it did not render at all; it is now a real third column saying what each
file was written under, with `sum.turp`, `primes-mu.turp` and `sort-mu.turp`
added and `suite/` pointed at.

**Four places still said nothing inhabits `CertifiedCompiler`.**
`bespokeWhitespaceIO` landed in the commit before last, and
`docs/verification.md` was in the odd position of marking whitespace
`**yes**` in its behavioural column and then denying it in the paragraph
underneath. `docs/README.md`, `docs/PLAN.md` and `README.md` had the same
sentence.

**Two places said arrays are outside the certified fragment**, while two
other places in the same two files said they are in. They are in:
`sieve-tc.turp` compiles and answers 15. Checked by running all twelve
`-tc` examples — eleven compile, `sort-tc` alone needs subtraction.

**`docs/TESTING.md` had aged badly.** It said `scripts/axioms.lean` did not
exist (it audits 523 declarations and is clean), that no URM differential
suite existed (there are seven), and it invoked the audit with a `--run`
that is not how it is run. It gained a malbolge-unshackled section — the
one language whose reference interpreter *randomises* the thing a
differential test would compare, which is why a width sweep replaces it —
and a fourth entry for `scripts/gen-mu-examples.sh --check`, the
derived-file check that now sits beside `render-docs-images.sh --check`.

**Line anchors and links.** Every `#L` anchor in the repository was checked
against the file it points into; six had drifted, one by 51 lines. Two
table rows had an unescaped `|` inside a code span — `docs/conformance.md`'s
`||` row and `docs/unlambda/spec.md`'s row for the `|` builtin — which
splits the cell in every markdown renderer, so both rows were rendering
with the wrong number of columns. And the compile example that told a
reader to write `hello.mu` into the repository root now writes it to
`/tmp`, which is what every other language's compile example already did.

Every command quoted in the pass was run: `lake build` and `lake test`
clean (1376 tests), `scripts/gen-mu-examples.sh --check` up to date, and
the axiom audit `sorryAx`-free.

## 2026-08-31: one parser, because two agreed only by accident

Stage 6 milestone 2 opened with a question: do whitespace's `parseNumLine`
and Turpentine's `parseIntLine` accept the same lines and agree on the
value? `docs/whitespace/compiler.md` had asserted they do, and the plan
said finding out was worth the trip.

They did. On every line a reader can produce, by **two accidents that
cancel**. Turpentine trimmed with `String.trimAscii`, which strips newlines
as well as blanks — unobservable, because `readLine?` never leaves a
newline inside a line. And its digits went through `String.toNat!`, which
skips underscores and panics on a non-numeral — unobservable, because the
`all Char.isDigit` guard in front of it rejects `_` first. Two languages
reading a number the same way for reasons neither of them states.

What did not survive was proving it. `String.toNat!` is a
`String.Slice.foldl`, and core ships no lemmas about slice folds at all, so
certifying the coincidence meant developing that theory first — a
disproportionate amount of work to establish something that ought to hold
by construction. So there is now one parser, `Langlib.Common.parseNumLine`,
sitting beside the `readLine?` both languages already shared, and the
agreement is definitional rather than accidental. Turpentine's accepted
language is unchanged on every input a program can be given; the whitespace
and Turpentine golden suites, and the trace suite that runs the two
interpreters against each other, all pass unchanged.

This is the prerequisite for the rest of milestone 2, which is the proof:
`SimS` relating the two cursors, `readInt` joining the fragment, and
`encodeInput` becoming the identity instead of "run the target on nothing".

## 2026-08-31: a compiler proved to behave, not just to answer

`CertifiedCompiler` has an inhabitant. `bespokeWhitespaceIO` is the
hand-written Turpentine-to-whitespace backend proved *behaviourally*
correct on the output fragment, and its `encodeTrace` is the **identity**:
the compiled program does not re-encode the source's I/O into a target
convention, it performs it, byte for byte and in order. §1.4 of
`certified-compilation.md` had been titled "what is proved behaviourally:
nothing, yet" since the definitions landed. It is not called that any more.

Three details decide whether the statement means what it looks like it
means, and all three are in the definition rather than in prose. The
specification is stated at `answerProgram p` — the source *with* the
epilogue the compiler appends — because the epilogue's newline and answer
are events the compiled program really performs, and naming only the
source's own events would describe a different program. `encodeInput`
ignores the source's input stream, which is honest only because the
verified fragment cannot read; when `readInt` joins it, the input events
will have to match too. And the source-side specification is not a trace a
compiler author picked: `behavesWith_wf` says the events it names are a
real run's.

The proof reuses the answer-only one rather than repeating it. The old
end-to-end theorem became `bespokeCompile_core`, which reports the same run
three ways — it halts, its output decodes, and its trace is the body's
trace followed by the epilogue's two events — and both the answer-only and
the behavioural theorems are corollaries. What the behavioural one adds is
an inversion of the epilogue on the *source* side, and that turned up the
one thing worth warning the next person about: `seq` runs its second half
at one less fuel, so `answerProgram`'s two appended statements need two
fuel of their own, and a bound too small to reach them contradicts the
hypothesis that the whole thing halted.

That same fuel arithmetic is why `toCertifiedOf` back to `HaltsWithAnswer`
is **not** in this commit. At equal fuel it is false-shaped: a body that
halts with exactly `n` leaves nothing for the epilogue. Closing it needs
fuel monotonicity for `Turpentine.exec`, which this library deliberately
does without, since `Reaches` carries fuel exactly. Nothing is lost —
`bespokeWhitespace` proves the answer-only statement directly, against a
sharper specification, and `toCertified` gives the erased direction free.

Five new tests compile with the behavioural compiler, run it, and compare
the two event lists outright. Milestone 1 of Stage 6 is done; milestone 2
is `readInt`, and with it the first proof that a compiled program reads
what its source reads.

## 2026-08-31: two compiled Unshackled programs, checked in

`Langlib/Examples/MalbolgeUnshackled/compiled/primes.mu` (348 cells) and
`compiled/sort.mu` (268 cells) are the first Unshackled programs in the
library that nobody wrote and no search found. They are compiler output:
the primes up to 30, and six numbers sorted.

Both sources needed twins. `primes.turp` reads its bound and `sort.turp`
reads its six numbers, so the backend refuses them by name; `primes-mu.turp`
and `sort-mu.turp` fix the bound at 30 and seed the same six literals
`sort-tc.turp` uses. The `-mu` suffix is the `-tc` convention applied to a
different restriction — `-tc` means no I/O at all, `-mu` means no *input* —
and the difference is the point: these keep the streaming output a register
machine cannot produce.

They are derived files on the model of the graphical languages' pictures.
`scripts/gen-mu-examples.sh` is the only thing that may write them, it
checks each compiled program against its source's own output as it goes, and
`--check` fails on a stale one. The division of labour is worth stating,
because it is not the obvious one: the test suite checks that the compiler
produces the right output for both sources (recompiling from scratch) *and*
that the files in the tree are Unshackled programs printing the right thing
(loaded by Unshackled's own loader, run at two rotation widths, with nothing
from the compiler involved) — but only `--check` catches staleness, exactly
as with the images.

Nine new tests, 71 in the file. `sort.mu` is quoted in full in both
`docs/malbolge-unshackled/spec.md` and the compiler page, in a stated
transliteration (a cell in 33..126 as itself, a data cell as its code point
in angle brackets) that is generated and verified to decode back to the file
byte for byte — the first draft of it, typed by hand, was missing the final
character. The whole layout is legible in it: the three-cell prologue, the
descending ramps that padding always makes, the two pointer cells, the data
row, the 64-cell gap and the code row.


## 2026-08-31: the compiled program says what the source says

The hand-written whitespace backend's simulation used to say that a
statement's code reaches the same heap. It now says that it reaches the
same heap *and performs the same I/O events*, and the witness is one list
used on both sides: not "the target's output re-encodes the source's" but
*the compiled program prints the bytes the source prints, in that order*.
`print("...")`, `print(e)` and `println(e)` for an `int` or a `bool` are in
the verified fragment, and thirteen new tests run each of them through the
reference interpreter and through the backend and fail unless the two agree
byte for byte.

Two things fell out of it that were not in the plan.

The **epilogue had to move**. `bespokeCompile` appends a statement to make
the specification's single `Nat` observable, and reading it back used to be
"parse the whole output as a decimal numeral". A program that prints for
itself breaks that, so the epilogue is now `println(""); print(answer);`
and `decodeAnswer` reads the digits after the *last* newline. No extra
restriction on the fragment is needed to justify it: `toString (answer :
Nat)` is all digits, so the epilogue's newline is provably the last one in
the output, whatever the program said first.

The **fragment had to become type-checked**. `print(e)` is the first
construct whose code depends on the expression's static type — `outnum` for
an `int`, a `jz` between two string constants for a `bool` — while the
reference interpreter renders the runtime value. A program that stored a
boolean in an `int` variable would print `true` where its compilation
prints `1`, and nothing ruled that out, because the encoding erases the
difference: a `bool` and the integers `0`/`1` are the same whitespace cell.
So `Agrees` carries the typing as well as the value, `checkFragment`
rejects an assignment whose right-hand side has the wrong type, and
`evalExpr_hasTy` proves static and runtime types agree. That proof is
shorter than it sounds, because the reference semantics does most of it:
`evalBin` throws on operands of the wrong shape, so an addition that
produced a value at all produced an integer. Only three forms need more —
a variable, whose type comes from `Agrees`, and `&&` and `||`, which return
their right operand and so need the induction hypothesis.

Also worth recording: the output is carried through the simulation as the
*string* that was appended, not as raw bytes. That is what keeps the whole
output decodable, since `String.toUTF8` distributes over append, so a run's
output stays the encoding of one string rather than a byte array nobody can
parse. `reaches_bytesCode`, by contrast, deliberately does not name the
bytes it wrote; `Whitespace/Trace.lean` recovers them from the trace.

What is left in Stage 6 milestone 1 is the packaging: `bespokeWhitespaceIO
: CertifiedCompiler`, with `spec` at `answerProgram p` and `encodeTrace`
the identity. `docs/certified-compilation.md` §1.4 still says "nothing,
yet", and will until that instance exists.

## 2026-08-31: Turpentine compiles to Malbolge Unshackled

The library's hardest target has a backend:
`Langlib/Languages/Turpentine/Compile/MalbolgeUnshackled.lean`, over the
programs that do not read input. Written up in
`docs/malbolge-unshackled/compiler.md`.

The surprise was how *small* the assembler is. Unshackled's reputation rests
on the instruction at `c` being `(mem[c] + c) mod 94`, so that code is not
relocatable; but a compiler that only needs a cell to run once can solve that
in one line — `(opcode - addr) mod 94` lands in `0..93`, and adding 94 when
it is below 33 lands in `94..126`, so *every* instruction is printable at
*every* address. The residue arithmetic that dominates hand-written Malbolge
costs nothing here. What is expensive by hand is a cell that has to run
twice, which is a different problem, and not this backend's.

The layout follows from one observation: `c` and `d` both advance by one
after every instruction, so they keep a fixed distance. That gives a **code
row** and a **data row** running in parallel, each crazy cell reading the
data cell directly below it. Three cells of prologue set the distance up, and
the first two of them decide their own contents: `movd` at address 0 *is* the
word 40, so `d` lands on 40 and the pointer cell is address 41 whatever else
the compiler does.

Two things had to be discovered rather than looked up.

*The proof's constants cannot be loaded.* `crz_two_steps` says two crazy
operations take any accumulator to any target and computes the constants, but
`toTwoConst` picks a value whose repeating trit is `2`, and a source
character is a code point, whose repeating trit is `0`. Loadable constants
exist because the crazy operation is tritwise and, *above* both operands,
five of the nine trit pairs work rather than only `(0,0)` — so a constant can
be padded upwards until it lands on a code point the loader accepts.
`twoStep` enumerates those paddings most-significant-first, and a sweep over
all 16384 accumulator/target pairs below 128 at eight address residues finds
one every time, never larger than 6641.

*Data cells are the loader's bug.* A character outside `33..126` is stored
unchecked — Malbolge's accident, Johansen's default, spec decision 5 — and
that is the whole data channel: jump targets and crazy constants ride in as
characters above `~`. The emitted file therefore needs the loader's default
setting; `--strict` rejects it, and a test asserts that it does.

Tests are in six suites, `Langlib/Tests/CompileMalbolgeUnshackled.lean`:
differential against Turpentine's own interpreter (including every byte from
1 to 127 through `printByte`), the same programs at seven starting rotation
widths from 10 to 300 (the backend emits no `*`, so the width must not
matter, and it does not), an audit of every emitted cell read back the way
the loader reads it, pinned cell counts, a straight-line check at a fuel
bound of `n + 4`, and ten refusals.

The gap is input, and it is not more code generation. The first version of
this paragraph got the reason wrong and a parallel session caught it, which
is worth recording because the correct version is sharper. Two crazy
operations against compiled-in constants *can* turn an unknown value into a
uniform one: `crz (crz a ...222) ...000 = ...000`, which is `crz_absorb`
and is the first step of the verified branch pipeline. Individual columns of
the table are non-constant, but two of the nine compositions are. What a
chain of crazy operations cannot produce is a uniform value that *depends*
on the accumulator: `crz` is tritwise, so each output trit sees only the
input trit at its own position, and two inputs differing at one position
agree at every other, while `...000` and `...222` differ everywhere. That
sharper statement is now `no_accumulator_flag` in
`Langlib/Computability/MalbolgeUnshackled/Main.lean`, proved by the session that
caught the error — so a branch flag provably has to be *read* from something
already uniform, which is what forces the unary register encoding rather
than merely recommending it. A comparison still cannot be collapsed without
`*`, and `*` is mandatory anyway for addressing, which is the argument
`widthBounded_step1` actually proves.

One consolation prize, and it works: `crz (crz a k) k` with `k` all ones
below the width of `a` is the identity (the `0 ↔ 1` transposition twice),
and `k` is a plain natural, so it loads. Two crazy operations therefore copy
an unknown accumulator into a memory cell, and a `movd` through that cell
turns the copy into an address. `inputProbe` in the backend is a 2207-cell
hand-built image that does it: it reads one character, dispatches 128 ways
through a table at addresses `v+1`, prints `AAA` for `a` and `CCC` for `c`,
and echoes anything else — with no rotation anywhere, at every rotation
width. It is not wired into `compile`, because one dispatch is not a machine;
it is there so the mechanism the input half needs is checked rather than
sketched. End of input is the interesting failure: above the width of `k` the
column applied is `k`'s lead twice, which sends `2` to `1`, so `...22`
copies to `...1222…2`, whose leading trit is 1, and the jump lands where no
loader ever wrote.

## 2026-08-31: subleq reports its events, and printint is honest

The third and last of the trace semantics, and the shortest: subleq has one
instruction, two of whose forms do I/O. `Subleq.State` records the run's
events, `Langlib/Languages/Subleq/Trace.lean` proves the two `TraceLang` laws
from the same invariant as whitespace's, and `instance : TraceLang
SubleqLang` now sits beside `ProgLang SubleqLang`. Reading at end of input
consumes nothing and so records nothing, which is the honest report: no byte
crossed the boundary.

Both backends the library has proved answer-correct can therefore now be
*stated* behaviourally. That was the whole point of the exercise.

The interesting part is what the tests found. `docs/certified-compilation.md`
has always said `encodeTrace` for the subleq backend is the identity, on the
grounds that it hands the target the bytes the source read and wrote.
Nothing checked it, and there was room to doubt, because subleq does not
have an "print this integer" instruction: it prints integers through the
`printint` runtime routine, which builds a decimal numeral by repeated
doubling on top of a self-modifying calling convention. It emits exactly the
bytes `Value.render` does.

    println(-12345)   turpentine  >45 >49 >50 >51 >52 >53 >10
                      subleq      >45 >49 >50 >51 >52 >53 >10

Ten new tests, three of them that cross-check. The cost was the same as
whitespace's and is worth recording because the next backend will pay it
too: the completeness proof builds machine states with positional `⟨…⟩`
literals, so a fifth field meant threading an events parameter through
thirty-odd of them. They are now stated for an arbitrary prior trace, which
is the more useful form. The subleq input branch also had to be rewritten
from a shared `let` into two branches so that a proof can case on the read —
the third time that pattern has come up, after Turpentine's
`a[i] := readByte()`.

## 2026-08-31: a better register encoding, and the probe

A correction to the encoding committed earlier, and an improvement worth
the change. Blank `...000` with mark `...111` makes set, clear and test one
operation each, but the test is destructive: a mark reads back as `...222`
and needs a second operation to restore. The test is the loop condition, so
it runs on every iteration of every compiled loop, which makes it the one
place worth optimising.

Take **blank = `...000` and mark = `...222`** instead. The accumulator
`...111` then satisfies `crz ...111 b = b` for both values, so testing
leaves the cell exactly as it was, and the value it leaves in the
accumulator is the cell's own content: `Value.zero` for blank, `Value.eof`
for mark. Those are precisely the two flags `branch_arith` consumes, so the
probe feeds the branch with no conversion (`probe_feeds_branch`). The test
accumulator is itself loaded self-restoringly, from a blank accumulator
against a cell holding `...111`, so the whole probe is two chain links and
every cell it touches comes back unchanged.

The price falls on `set`: no single operation takes `...000` to `...222`,
so setting a mark costs two visits to the cell and hence two gadgets.
Paying there to make the loop condition free is the right trade, since the
condition runs once per iteration and `set` once per command. Both
encodings are kept in the file, with this one marked as the one the
compiler uses.

## 2026-08-31: entering a chain, and a whole gadget

Two more layers, and the compiled-command unit now exists.

`enter_chain` is the prologue that positions `d`. `movd` is the only
instruction that moves it, and a re-enterable `movd` must sit at residue 60
or 64 modulo 94 while a chain starts at 82, so the two cannot be adjacent;
one stable `jmp` bridges them. Two instructions: `movd` reads a pointer
cell holding `D - 2` and re-aims `d`, then `jmp` reads the cell at `D - 1`,
holding `A - 1`, and drops control at `A`. Afterwards `c = A` and `d = D`,
exactly what `chain_run` wants, with the accumulator untouched.

`gadget_run` composes prologue and chain: `2 + 2n` steps that position `d`,
fold `n` operands into the accumulator, and leave the result both in the
accumulator and in the last operand cell, every `jmp` cell still standing.
Its hypotheses are stated on the *initial* memory, the prologue's two
writes being transferred across by its frame, so a caller reasons about one
memory rather than a chain of intermediate ones. `chainFold_congr` is the
small congruence that makes that transfer work.

That is the unit a compiled counter-machine command is built from. What
remains is to instantiate it for `inc`, `dec`, `emit` and `loop`, write the
assembler that lays the cells out, and run the induction on `Ev`.

## 2026-08-31: running a chain

`chain_run` composes `n` links, laid out at **stride 94**. The stride is
both forced and convenient: a re-enterable `crazy` must sit at residue 82
or 86 modulo 94, so putting the links 94 apart lands every one of them on
the same residue, and a single word then serves for every `crazy` cell and
a single word for every `jmp`. Link `i` occupies `A + 94i` and
`A + 94i + 1`, jumps to `A + 94i + 93`, and control resumes at
`A + 94(i+1)`; the 92 cells in between are never executed and need no
words. Data sits after the code, operand `i` at `D + 2i` and jump target
`i` at `D + 2i + 1`, since `d` advances two per link.

The theorem runs the chain in `2n` steps: the accumulator folds the
operands (`chainFold`), each operand cell keeps its intermediate, each
`crazy` cell is encrypted once, every `jmp` cell comes back unchanged, and
a frame condition names the only cells touched. That last pair of clauses
is what makes the chain re-enterable and what let the induction go through:
at each step the next link's cells are shown untouched by all the previous
ones.

This is the executor a compiled gadget runs on: straight-line arithmetic of
any length, laid out mechanically, with one induction behind it.

## 2026-08-31: chains, and the end of padding

The layout problem had a solution I had been walking past. Laying a gadget
out as one contiguous row forces padding into the gaps between working
cells, and padding is the awkward part: a re-enterable `crazy` must sit at
residue 82 or 86 modulo 94, while the cells between fall wherever they
fall, including the sixteen residues at which no two-cycle word is harmless
in both phases.

Interleaving removes the problem entirely. Put a `jmp` immediately after
each working cell and let it carry control to the next one. A `jmp` never
encrypts itself, so it is stable for the whole run and the control path is
identical on every pass, while the working cells alternate between their
instruction and a no-op. The cells jumped over are never executed and need
no words at all; only the landing cell is encrypted, and encryption keeps a
printable word printable.

`d` advances two per link, so each link owns two data cells at a known
stride: the operand the `crazy` reads at `D` and the address the `jmp`
reads at `D + 1`, both placed statically. `chain_link` proves one link in
two steps, with a frame condition naming the only three cells it touches
and, crucially, a clause saying the jump cell comes back unchanged. That
clause is what makes a chain re-enterable, and it is `jmp_cell_stable`
cashed out in the form a compiler can actually use.

## 2026-08-31: the source side reports its events too

Turpentine now records its I/O the way whitespace does: an `events` field
on `State`, four recorders, and the same invariant proved in
`Langlib/Languages/Turpentine/Trace.lean` — 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.

Turpentine is not a `ProgLang`, so there is no `TraceLang` instance to
inhabit. What it needs the trace for is to be the `τ` in a specification,
and that is `TurpentineBehavesWith p σ n τ result`: the I/O-aware
refinement of `TurpentineHaltsWith`, naming the input stream and the events
the answer-only version drops. `behavesWith_wf` is the part that keeps it
honest — whatever `τ` a program is specified to perform, its output events
are the bytes a real run emitted and its input events are a prefix of the
stream it was handed. A compiler proved against this is constrained by what
the program does, not by a trace chosen to make a proof go through.

Two wrinkles worth recording. The induction is on the fuel and *then* on
the statement, because `seq` consumes no fuel: `exec (n+1) (s₁; s₂)` runs
`s₁` at the same bound and a smaller statement. And `a[i] := readByte()`
shared its two ends of input through a `let`, which no tactic could case
on; it is now written out as two branches. The semantics is unchanged,
including the part worth being explicit about: a failed store rolls the
read back, and the trace rolls back with it. The run that reports the error
is the run that did not keep the byte.

The payoff is that `encodeTrace = id` stopped being a prediction. Fifteen
new tests, and six of them run a program through the reference interpreter
*and* through the hand-written whitespace backend and fail unless the two
performed the same events in the same order — decimal rendering, boolean
words, `readInt` consuming its line terminator, and reads and writes
interleaved. `docs/PLAN.md` Stage 6 still has to prove it over a fragment.
It is now being checked on every `lake test`.

## 2026-08-30: the register encoding, one operation each

The counter machine wants set, clear and test on a register cell, and the
encoding decides what each costs. Taking **blank = `...000` and mark =
`...111`** makes all three cost exactly one crazy operation, which is the
least the language allows, since `p` is the only instruction that writes.
Reading Olmstead's table by the accumulator trit: against `...000` a blank
becomes a mark; against `...111` a mark becomes a blank; against `...222` a
blank gives `...000` and a mark gives `...222`.

The third row decides the architecture. `p` leaves its result in the
accumulator as well as in the cell, so testing a register cell against
`...222` puts exactly the flag `branch_arith` wants into the accumulator:
`Value.zero` for blank, `Value.eof` for mark. **The zero test costs one
instruction and needs no broadcasting**, which the crazy operation could
not do anyway, being tritwise. That settles the representation question in
favour of unary registers, by the table rather than by taste, after several
candidates that all needed a loop just to test for zero.

The test is destructive on a mark, which reads back as `...222`, but one
more operation against the same constant restores it and a blank survives
both untouched, so the pair is a non-destructive test whichever the cell
held (`register_test_roundtrip`).

## 2026-08-30: the output side, which is nearly free

A short follow-up. `Counter.CState` records only how many bytes were
emitted, because every byte a compiled program emits is the same. So the
output half of the witness costs almost nothing: `emit` becomes a gadget
that sets the accumulator to a fixed printable natural and executes one
`<`, and the answer decoder is `decodeBytes bs = some bs.size`.

The byte is 42, `'*'`: one UTF-8 byte, not `...22` (which would close the
output stream) and not `...21` (a newline), so `doOutput` takes its
ordinary branch. `doOutput_star` and `step1_out` prove the step,
`outClosed_of_step1_out` records that emitting leaves the stream open so
emits compose, and `decodeBytes_append_star` reads the count back.

That settles `emit` and `decodeOutput`, two of the pieces a
`TuringComplete` witness needs. What is left is the register
representation and the gadgets for `inc`, `dec` and `loop`, the assembler
that places them, and the induction on `Ev`.

## 2026-08-30: the two-sweep gadget, and the route to a witness

Two things this batch: the target for the compiler is now fixed, and the
composition obstacle is cleared.

**The target.** `Langlib/Computability/Common/Counter.lean` already carries the
target-independent half of every completeness proof: `counterProgram`
compiles a URM program and its inputs into a structured counter machine
with four commands (`inc`, `dec`, `emit`, `loop`), and
`counterProgram_spec` proves the simulation. So a Malbolge Unshackled
witness does not need a dispatcher or a program counter at all. `Ev` is a
big-step relation with structured control, so the compiled program is
generated by recursion over the command tree, exactly as the Brainfuck
backend does. Two items drop off the remaining list.

**The obstacle.** A compiled loop body is re-entered, and every executed
cell is overwritten by its own encryption. The two-sweep discipline said a
row of two-cycle cells run twice comes back to itself; what was missing was
the wrapper that drives both sweeps. `two_sweep` is it. A row at `b+1 … b+L`
plus one `jmp` at `b+L+1` runs in `2L + 2` steps: the work sweep folds the
operands into the accumulator and leaves every cell encrypted once, the
`jmp` reads the first table entry and lands control back on `b+1`
(encrypting `b`, never itself), the no-op sweep encrypts each cell a second
time and restores the two-cycle words, and the `jmp` reads the second entry
and leaves. Since the row is restored, **the gadget may be entered any
number of times**, so a loop body built from such gadgets is itself
self-restoring, and nesting composes.

Underneath it, `row_run` generalises `crazy_run` and `nop_run` to a mixed
row, which is what a gadget really is: a re-enterable `crazy` cell must sit
at residue 82 or 86 modulo 94, so working cells are spaced and padding fills
the gaps. `rowFold` is the fold it computes, applying the crazy operation at
the working positions and skipping the padding.

Remaining for the witness: the register layout, gadgets for the four
commands built from `two_sweep`, the assembler that places them, and the
induction on `Ev`.

## 2026-08-30: whitespace reports what it read

`cat.ws` copies its input. Nothing the library could say about it
distinguished that from a program that reads everything and then writes
everything, because a `RunResult` records the bytes that came out and
nothing whatever about the bytes that went in. It does now:

    cat.ws on "hi"  ->  <104 >104 <105 >105

`Whitespace.State` carries the run's I/O events, most recent first so
recording a byte stays O(1), and the four I/O instructions push to them.
`Langlib/Languages/Whitespace/Trace.lean` proves the two `TraceLang` laws
from a single invariant on a reachable state: what the trace says was
emitted *is* the output, and what it says was consumed, *followed by what
the cursor has left*, is what the stream started with. The second half is
stronger than the prefix law it implies, and being an equation is exactly
what makes it survive a second read — the residue is what the next read
draws on. Only the four I/O instructions disturb it, so the other twenty-odd
cases of the induction over `exec` are the hypothesis itself, discharged by
`exact`.

`instance : TraceLang WhitespaceLang` now sits beside `ProgLang
WhitespaceLang`, where FRACTRAN's does. FRACTRAN's came free from
`ofInputFree`, since it provably never reads; whitespace's is the library's
first for a language that does.

Two costs that were not in the plan. `ByteArray.toList` is defined in core
by a private loop with no lemmas at all — not even that it is `Array.toList`
of the array inside — and both trace laws are stated about it, so
`Langlib/Common/Io.lean` proves that bridge and the three consequences.
And the whitespace completeness proof builds machine states with positional
`⟨…⟩` literals, so a seventh field meant threading an events parameter
through every block lemma; they are now stated for an arbitrary prior
trace, which is the more useful form anyway.

Eight golden tests pin the interleaving, which is the one thing the two
laws deliberately do not determine: both are satisfied by a trace that
reports every read before every write. The suite re-checks both laws on
each run before comparing, so the tests and the theorems cannot drift.

## 2026-08-30: terminating runs, and a free zero test

`neverHalts_of_invariant` covers loops that must not stop. A simulation
needs the opposite: `TuringComplete` demands the compiled program halt with
the right output whenever the machine it simulates does. Three lemmas give
that shape. `exec_run?_add` splits a run anywhere, so a proof can reason
gadget by gadget and stitch the pieces. `exec_halts_of_run?` is the ending:
a run that arrives at a cell decoding to `halt` reports `Exit.halted` with
the output it accumulated, restated at the language interface as
`image_halts_of_run?`. And `run_of_measure` is the loop rule: an invariant,
a measure that strictly decreases each pass, an exit at zero. In a
simulation the measure is the simulated machine's remaining step count, so
this is what turns "the URM halts" into "the compiled program halts".

An encoding note that saves a whole gadget. `branch_arith` decides on a
cell holding `...000` or `...222`, which are `Value.zero` and `Value.eof`.
A register cell storing a unary digit as blank-or-mark in exactly that
encoding **is** a branch flag, so the zero test costs no instructions
(`branch_on_mark`). That is worth having because the crazy operation is
tritwise and cannot aggregate across trit positions: a zero test on a wide
number would need rotations and a loop, while blank-or-mark needs nothing.
It is an argument for the unary register representation, made by the
arithmetic rather than by taste.

## 2026-08-30: a bespoke Piet backend, and whitespace takes the whole suite

Two things, and the second was easy because of what the first one was not.

### Piet, without going through a register machine

`Langlib/Languages/Turpentine/Compile/Piet.lean`, reachable as
`--to piet --bespoke` and tested in `Langlib/Tests/CompilePiet.lean`. Two
compilers stacked: the first lowers Turpentine to a flat list of **lanes**
— straight-line runs of Piet commands ending in a `goto`, a two-way branch
or a halt — and holds no geometry; the second lays lanes out as corridors
wired with white and holds no Turpentine.

The layout rests on the four facts recorded last commit, each checked
against `evalGrid` rather than reasoned about. Lane `i` is a corridor on
row `2i`; odd rows are white, which is what keeps two corridors from
merging. A jump is one clockwise circuit and no commands at all: right to a
wall, down a wire column, left to the target's entry column, up to its
row, right onto its first block.

**The constraint that is not obvious** is that lanes' end columns strictly
decrease down the picture. A branch's wire falls down its own lane's end
column, crossing every lane below it, and may only do that because a lower
lane ends further left and so cannot reach that column. Getting that
backwards is the one way to build a picture that looks right and runs
wrong.

Halting is the shape the prototype found, and the probe confirmed both
halves: a bar of three entered from above through its middle codel halts,
and the same picture with a bar of one escapes back into the white it
arrived through and runs forever.

Variables live on the stack, reached with `roll` — `O(depth)`, the price of
having no heap. Constants are built rather than spelled out, since a `push`
pushes the block's codel count: 16384 costs 51 codels instead of 16384.
`opFor_advance` proves the generator's colour arithmetic inverts `opFor` on
all 17 commands at all 18 colours, by `decide`, so no Mathlib crosses into
`Langlib/Languages/`. With `colorOfRgb_toRgb` that is both round trips: the
image is the grid the compiler built, and the grid is the commands it
chose. The *layout* is proved by nothing and carried by test.

**Two bugs the tests caught rather than the design avoided.** Lane 0 has to
be the program's, not the trap's, since execution starts on row 0. And the
compile-time stack depth is a property of the program point, not of the
path walked to it: letting the counter run on through both branches of the
division correction put every variable access after a `/` one slot too low,
which surfaced as `gcd.turp` printing 42 where the reference printed 21.
The generator now checks that two joining lanes agree.

All 20 conformance programs compile and match the reference, all four sign
pairs of Euclidean division among them, and Piet is now the suite's seventh
compiled runner. Sizes, measured: `answer := 2` is 98,338 bytes through the
certified route and 8,757 through this one, which also prints its answer.

**Arrays, which were the last refusal.** An array lives on the stack like
the scalars, but the roll amounts stop being literals: reaching `a[i]`
rotates by a distance known only at run time, and `roll` *consumes* the
distance, while the read needs it twice and the write three times.
Recomputing `i` is out (it may be any expression) and a spare copy on the
stack does not survive, because it sits inside the region the rotation
disturbs. The fix is two **scratch slots below every variable**: a rotation
that reaches an array element cannot reach something deeper than every
element, so the scratch slot's index after the rotation is the index it had
before.

Every access is bounds-checked, and has to be — an index off the end would
rotate the wrong distance and silently corrupt the variables below it,
which is worse than stopping. The check fits in **one lane rather than
two**: both halves of `0 ≤ i < n` are a `greater`, both results are 0 or 1
so their conjunction is a product, and neither can trap so there is nothing
to short-circuit. That is worth more than it sounds, because a lane is two
rows and its branch is two wires, and the interpreter's per-step cost grows
with the picture's area: folding the two checks into one took `sieve.turp`
from `410 x 80` codels to `400 x 68`, and the twenty conformance programs
from 73 seconds to 45.

What remains is the price of having no heap: every element access is
`O(depth)`, so a loop over an `n`-element array is quadratic, and
`sieve.turp` is the slowest program in the suite by a factor of three.

### Whitespace takes all twenty

The hand-written half of the conformance suite goes from 4 of 20 to 4 and
20. Whitespace takes the lot, and the reason is the language rather than
the effort: `outnum` prints a *number*, so nothing needs brainfuck's
divide-by-ten printer; cells are unbounded signed integers, so `fact` and
`power` need nothing special; and the heap is integer-addressed, so an
array index is an `add` and a `retrieve`.

Whitespace has no comment syntax because it does not need one — every
character that is not a space, tab or linefeed is ignored — so the `.ws`
files carry a mnemonic in brackets before each instruction's tokens and the
author's prose in braces, and are still exactly what the interpreter runs.
The prose is underscore-joined because a comment may not contain a space, a
tab or a linefeed: all three are code.

Two of the twenty earned their keep. `divmod.ws` is the one program whose
answer whitespace cannot give directly, since its `div` and `mod` floor
where Turpentine's are Euclidean; the hand-written program reaches the same
correction the compiler emits, independently, which is exactly the
agreement the suite exists to notice. And every array program writes each
cell before reading one: our heap defaults to zero and would have let a
lazier program pass, but the authors' `wspace` crashes on a cell that was
never stored.


## 2026-08-30: reading a line is no longer opaque

`Input.readLine?` was a `partial def`, which Lean compiles to a constant
with no equations, so nothing whatever could be proved about the bytes a
line read consumes. Four interpreters call it — whitespace's `readnum`,
Turpentine's `readInt`, Thue and FRACTRAN — and the hole was already
load-bearing: `Langlib/Common/Computability.lean` records it as the reason
the whitespace completeness witness loads its registers from compiled-in
constants instead of from its input stream.

It is now well-founded. `readLineGo` recurses on `data.size - pos`, which
a successful read strictly decreases; `readLineBytes?` returns the raw
bytes, so the numeric-parser lemmas that milestone 2 needs will not have
to go through `String.fromUTF8!`; and `readLine?` is the thin `String`
wrapper the callers already used. Behaviour is unchanged, edge cases
included — an unterminated final line is still returned, the newline is
still consumed, empty lines still come back empty.

The point of the exercise is the three cursor facts, proved for `read?`,
for the worker, and for both readers: reading never swaps the stream out,
the cursor only advances, and it never leaves the data. Those are exactly
what `TraceLang.trace_inputs` needs, and needs for *every* whitespace
program rather than only the fragment a compiler proof covers — a trace
that composes over two reads has to know the second read sees the stream
the first one left. First step of Stage 6's behavioural certification for
whitespace; the plan is in `docs/PLAN.md`.

## 2026-08-30: re-enterable gadgets, by running the row twice

With the architecture settled on a finite self-modifying code region, the
frontier was making a gadget survive repeated entry. The discipline turns
out to be simpler than `loop.mu`'s jump-restore trick, and it needs no
jumps at all.

A cell holding a word of the `70 ↔ 74` cycle alternates instruction,
no-op. So run the gadget row **twice**: the first sweep does the work and
leaves every cell in its no-op phase, the second executes the same cells
as no-ops and returns each to its original word. `crazy_run` was already
the work sweep; `nop_run` is the other, and it constrains `d` not at all,
since a no-op reads no operand. `encrypt_encrypt_two_cycle` and
`row_restored` close the circle.

Getting from one sweep to the next costs one cell: a `jmp`, stable because
it never encrypts itself, reading a target table that `d` walks. The same
cell fires at the end of both sweeps and reads a different entry each
time, back to the top after the work sweep and onward after the no-op
sweep. That is `loop.mu`'s cell 155 doing a job with a name.

Traced against the interpreter, with two `crazy` cells at residues 82
and 86 of one 94-block: both fire on the work sweep, both no-op on the
second, both hold their original words afterwards, and the third sweep
begins identically to the first.

Two facts make the layout easy, and both follow from compiling to an
`Image` rather than to source, where the loader's checks do not apply.
**Padding is universal**: at every one of the 94 residues there is a code
whose whole `xlat2` orbit is harmless, so gaps between working cells cost
nothing. For loadable source only 14 residues work, which is why `loop.mu`
needed 201 cells. And **each instruction has exactly two 2-cycle
residues**, four apart: `crazy` at 82 or 86, `movd` at 60 or 64, `jmp` at
24 or 28. A working row therefore places two cells of a kind per 94-block
and pads the rest, and the assembler's placement problem is short
arithmetic.

Item 1 of the remaining list is now closed. Next: assemble the register
file from the verified primitives, then the dispatcher.

## 2026-08-30: the architecture decision, settled by a theorem

The frontier was re-enterability: a dispatcher re-executes its cells, and
every cell is overwritten by its own encryption. Two architectures were on
the table. (A) A finite self-modifying code region whose `xlat2` orbits are
managed across passes, which `loop.mu` demonstrates at three cells. (B)
Never re-execute a cell at all: run the unbounded computation through fresh
memory. (B) is genuinely available to a *compiler*, which builds its
`Image` directly and so chooses all six entries of `rest`; the
`restTable_not_printable` obstruction binds `load`, not `compile`. So the
choice had to be made on merits.

It is settled against (B), and by arithmetic rather than taste. A virgin
phase is the addresses congruent to `j` modulo 6, all holding one word, so
opcodes run `(w + a) mod 94` across the phase. Addresses in a phase share a
parity, hence so do opcodes, and the split is exact: the even opcodes are
`jmp`, `movd`, `crazy`, `nop`, the odd ones `out`, `inp`, `rotr`, `halt`,
four per phase per 282-cycle and no other option. An all-even background is
a compute engine with no halt, which looks ideal until one notices it has
no `rotr`, and `widthBounded_step1` already proved rotation mandatory for
unbounded storage. A rotating background is an odd background, and then
`rotr_forces_halt`: since `81 - 39 = 42` and 42 is a multiple of 6, a
`rotr` at address `a` puts a `halt` at `a + 42` **in the same phase**.
`halt_forces_rotr` is the converse, so the two are inseparable.

Fresh-memory execution therefore costs a halt-dodge every 42 addresses of
every rotating phase, on top of the computed jump targets the finite route
needs anyway. It is a tax, not a contradiction, and the docs say so; but it
buys no simplification, so the development commits to (A): a finite
self-modifying code region with managed orbits. Both doc pages record the
decision and the reasoning.

The next layer is now well posed: take the eight-instruction branch gadget
and make it survive repeated entry, the way `loop.mu`'s three cells do.

## 2026-08-30: the Malbolge spec, and four more programs from the wild

`docs/malbolge/spec.md` grew from a reference card into something you could
learn the language from, and four example programs joined it, each verified
by running it.

The new examples are `nop.mal` (`DP`, two characters, credited to Ben
Olmstead and apparently the only Malbolge program its author ever wrote),
`answer.mal` (`mtve`, 28 straight-line instructions that print `42`),
`hello-world.mal` (the punctuated hello world that circulates today — which
prints `Hello, world.`, not `Hello, World!` as Wikipedia claims), and
`99bottles.mal` (Iizawa et al., 2005, 22561 instructions, the program that
settled whether Malbolge can branch). The 99-bottles golden test does not
quote its 11459 bytes of output; it regenerates the song from a four-line
Lean function.

Two things in the spec are ours rather than folklore. The first is the
generated memory tail: reading the fill one trit column at a time, the
column map has exactly three cycles, of lengths 2, 2 and 3, so the tail
repeats with period 2, 3 or 6 — and since no cycle is constant, some word
in every period has a nonzero top trit, hence a value of at least 19683,
hence unexecutable. **Running off the end of a Malbolge program always
hangs**, within six steps. (Wikipedia says the fill has period 12; that is
the other operand order, not the reference interpreter's.) The second is
the three worked program analyses — `answer.mal` traced instruction by
instruction, `cat.mal`'s five-address loop with its 9-cycle at address 37
and the jump that re-encrypts the `j` at 60, and `truth.mal`'s branch,
which turns the input byte into a two-entry jump table in seven cycles.
Every claim of that kind was checked against the interpreter before it
went in, and two earlier drafts of those paragraphs were wrong.

Also folded in: the `xlat2` cycle structure (six cycles, lengths
2 + 4 + 5 + 6 + 9 + 68 = 94), the 2-cycle and immutable-no-op address
tables, the store/load idioms as identities about the crazy operation,
a section on normalized Malbolge, and a fuller history — Cooke's account
of the genetic algorithm that stalled at `hello wor` before the beam
search worked, and the pre-2005 "99 bottles" that turned out to be a
straight-line `printf` of a uuencoded gzip. 1168 tests pass.

## 2026-08-30: the bespoke proofs move next to the backends

`Langlib/Computability/` is for Turing-completeness results and their URM
bridges. The two correctness proofs of the hand-written Turpentine
backends were sitting there because that is where the `TurpentineCompiler`
vocabulary happened to be, not because they belong. They now live in
`Langlib/Languages/Turpentine/Compile/Certified/`, one file per target, under the
namespace `Langlib.Turpentine.Certified`.

Two things had to be said out loud for the move to work. First,
`Compile/Certified/` is a documented Mathlib exception under `Langlib/Languages/`,
alongside `Compile/Derived.lean` and the `--tc` half of `Main.lean`: it is
proof-side, and nothing a runner imports may reach it, so the executables
still compile without Mathlib. Second, `Langlib.Turpentine.Certified`
nests inside `Langlib.Turpentine`, and Lean resolves enclosing namespaces
before opened ones, so a bare `exec` in the subleq proof silently became
the *front end's* statement executor. It is now `Langlib.Subleq.exec`, and
`CLAUDE.md` carries the warning for the next proof that moves in.

Everything else is mechanical: imports, the two test modules,
`scripts/axioms.lean`, and every doc link and line anchor. The axiom audit
prints `Langlib.Turpentine.Certified.*` and still shows nothing but
`propext`, `Classical.choice` and `Quot.sound`. 1164 tests pass.

## 2026-08-30: the copy algebra

Short addition completing the value-level primitive set. The crazy
operation has exactly two per-trit bijections: reading a cell through
`...222` (row `x = 2` of the table swaps trits 1 and 2) and writing
through `...111` (column `y = 1` swaps 0 and 1). One read-write hop is
therefore the 3-cycle `0 ↦ 1 ↦ 2 ↦ 0` applied to every trit
(`hop_eq_vmap`), so three hops are an exact copy (`hop_hop_hop`): a value
moves three cells downstream without the program ever knowing what it
was. The constants restore themselves; only the source cell is consumed.

With the mux (`branch_arith`), straight-line rows (`crazy_run`), the
branch gadget, the escalator, and now data movement, every value-level
primitive a register file needs has a verified instance. What remains for
the witness is composition: a re-enterable dispatcher, the register
layout, the assembler, and the URM simulation induction.

## 2026-08-30: the branch gadget runs on the machine

`branch_arith` said seven crazy operations against computable constants
turn any accumulator into either of two jump targets. `branch_gadget` now
runs it: eight instructions, seven `p` cells executing the pipeline while
`d` walks the seven constants, then a `movd` through a pointer cell that
re-aims `d` at the written target. After exactly eight steps the cell
under `d` holds `t₀` or `t₁` by the flag, the accumulator holds the same,
and a frame condition says nothing else changed. The final `jmp` is
generic (`step1_jmp`) and belongs to the caller. Everything is verified
against `step1`, whose only bridge to the reference interpreter is
`step1_sound`, so none of it can drift from `exec`.

The lemma worth keeping is `crazy_run`: a row of `k` consecutive `p`
cells computes a fold of the crazy operation over the operand row, proved
by one induction, with the operand cells holding their intermediates and
the code cells their encryptions afterwards. Straight-line arithmetic of
any length is now one lemma application, not a proof per instruction.
`step1_eq` and per-instruction corollaries (`step1_crazy`, `step1_movd`,
`step1_jmp`, `step1_nop`), plus `run?_add`/`run?_one` for composing runs,
are the step-level kit it runs on.

Not yet done: re-enterability. A gadget executed once leaves its cells
encrypted; inside a dispatcher its orbits must cycle, the problem
`loop.mu` solves for three cells. That, plus restocking the spent
constants, is the dispatcher design problem, and it is the next layer.
Remaining after that, toward `TuringComplete`: the register
representation, the dispatcher itself, an assembler for the mod-94
layout, and the URM simulation induction.

## 2026-08-30: a hand-written FRACTRAN backend

`Langlib/Languages/Turpentine/Compile/Fractran.lean`: Turpentine to a
Minsky machine to fractions, reachable as `--to fractran --bespoke` and
tested in `Langlib/Tests/CompileFractran.lean`. FRACTRAN already had a
certified compiler derived from its completeness witness; what the
hand-written one buys is a fraction list short enough to read — 160
fractions for `sum.turp` where the derived route needs about 3,550 bytes
of them.

Three things the construction turns on, all recorded in
[fractran/compiler.md](fractran/compiler.md).

**No instruction may name its own state.** `inc r; goto s` at state `s`
lowers to `p_r * q_s / q_s`, which reduces to `p_r / 1`, and a denominator
of one divides every state — the rule would fire everywhere. The two
macros that want a self-loop (clearing a register, and the infinite loop a
failed `assert` becomes) use two-state cycles instead, and `toFractions`
rejects a self-reference rather than emitting one.

**The epilogue is measured, not guessed.** A layout reserves scratch for an
expression nesting the program may never reach, and every register the
epilogue clears costs a prime and two states. Compilation runs twice: the
first pass only to learn the highest register the code mentions, the
second to clear exactly those. It halved the output.

**The answer needs no decoding.** `answer` is register zero and gets the
prime two; every other register and every state gets an odd prime; the
final `1 / q_s` consumes the state prime. So the run ends on exactly
`2 ^ answer`, no earlier state is a power of two, and `--out pow2` prints
the answer once, in decimal.

**A correction to that last claim's framing.** The page had said the
certified route leaves the caller to factorise, and that is not true: its
cleanup phase reduces a halting store to `2 ^ R₀` as well, and it keeps a
control marker on an odd prime at every instruction boundary, so
`--out pow2` reads certified output too. Checked rather than reasoned
about — the derived `sumsq.turp` prints `30` under it. What separates the
routes is size (5074 bytes against 2125 on that program), not
decodability, and the page now says so.

**And `primes-tc.turp` finishes.** The page had it filed under "a program
that will not finish"; it halts after 60,872 steps, in about three
seconds, printing `10`. What is expensive there is the size of the
integers, not the number of steps — trial division makes every `%` a
counting loop over a state whose digits grow with the register values. The
section is rewritten around the run that actually happens.


## 2026-08-30: the branch arithmetic, in seven crazy operations

A branch in Malbolge Unshackled is a `jmp` whose target cell holds a
computed address, so the whole difficulty of branching is arithmetic: turn
a data value into one of two chosen targets using only `p`, and do it with
the *same* instruction sequence in both cases, because this language
cannot choose code per-case at runtime. `branch_arith` settles it: seven
crazy operations against constants computed from the two targets send any
accumulator to `t₀` when a flag cell holds `...000` and to `t₁` when it
holds `...222`.

The pipeline is absorb, load, shape. Absorb: `crzTrit (crzTrit x 2) 0 = 0`
for every trit `x`, so two operations against `...222` then `...000`
forget the accumulator entirely (`crz_absorb`), and the second constant is
self-restoring, since the operation writes `...000` over the cell that
held `...000`. Load: one operation, `crz 0 flag`, gives the uniform value
`...111` or `...222`. Shape: the three columns of the crazy table, as maps
of the accumulator trit, compose to every function `{1 ↦ p, 2 ↦ q}` at
depth four, and to only eight of the nine at depth three, missing
`(1, 0)`; the `cols` table holds a kernel-checked witness for each pair,
and the four constants `k1Of` … `k4Of` are built from it per trit
position (`map2`, the tritwise combinator that `crz` itself is an
instance of).

Everything is constructive and runs: for targets 100 and 200 the four
shaping constants evaluate to ordinary naturals (118, 145, …), and `#eval`
confirms the chain from arbitrary accumulators. What remains for a working
branch is the machine half, laying the seven constants along `d`'s walk
and jumping through the written target, which is sequencing of the kind
`loop.mu`'s proof already demonstrates.

## 2026-08-30: the width algebra, and a correction

The Malbolge Unshackled docs said a backend should avoid `*` entirely,
since the rotation width is read by exactly one instruction and dodging it
buys correctness at every legal width. The width algebra, now proved,
shows that advice is right for control and wrong for storage, and the
wrong half matters more.

Three width facts (`width_crz_le`, `width_rot_le`, `width_succ_le`): the
crazy operation never widens a value; successor widens by one trit but
applies only to `c` and `d`, which no instruction can store; rotation is
the one operation that can widen a stored value. Assembled per instruction,
`widthBounded_step1`: a step that does not rotate preserves any width
bound `W ≥ 13` on the accumulator and on all of memory. Bounded-width
values form a finite set, and `j` and `i` read their targets from memory,
so **in a rot-free run every teleport lands in a fixed finite set of
addresses, forever**. Unbounded storage cannot come from stored pointers
in a rot-free program; the only residual route is `d`'s one-cell-per-step
walk with self-extending code at the frontier, which nobody should want
to certify.

The positive half is the escalator, also proved. Rotating the value `1`
at rotation width `w` moves its single set trit to the top of the window:
`rot_one : Value.rot w (Value.ofNat 1) = Value.ofNat (3 ^ (w - 1))`, a
value of width exactly `w` (`width_rot_one`). A `j` through it raises
`maxWidth` to `w` and the rotation width doubles
(`growRotWidth_double`). Rotate `1` again and the next minted address has
width `2w`: widths `10, 20, 40, …` This rot/movd feedback is the
language's only supply of unboundedly many nameable addresses, which is
the mechanism-level meaning of "Unshackled", and it is the allocator of
any compiler targeting the language.

Consequence for the completeness plan, recorded in
`docs/malbolge-unshackled/compiler.md`: control gadgets stay rot-free and
keep every lemma proved so far; the register file cannot, so the witness
will be stated against the reference rotation policy the `ProgLang`
instance pins (start at 10, exact doubling), and correctness at every
legal policy is deferred. Both pages now say this in place of the old
advice.

## 2026-08-30: SKI is Turing complete, and the functional route is closed

`skiComplete : TuringComplete SkiLang`, axiom-clean. Both halves of the
functional route are now proved, and the second did **not** come free from
the first even though the two languages share their combinators. See
[ski/computability.md](ski/computability.md).

**What did not transfer, and why.** Unlambda is call by value and SKI is
normal order, so the compiled terms are different programs, not different
spellings of one. And Unlambda has an output instruction while SKI has
none: a run's whole observable is the normal form it prints, so the answer
has to be a term. It is a tower of `K`s ending in `I`, one `K` per unit,
and `decodeOutput` counts them.

**What normal order gives back.** Nothing has to be forced before it is
stored, so an increment leaves the unevaluated application that computes
it, a loop's branches need no guard, and the ordinary fixed point works.
The register file needs no nil case either, since the counter semantics
only admits indices below the bound, and that takes a binder off every
cell: bracket abstraction triples a body per binder, so the cell a nil case
would need costs about ten times what this one does.

**The lemma the whole file rests on.** `hstep` is the spine-only fragment
of the interpreter's leftmost-outermost step, and it commutes with
application with **no side condition**: applying a term to an argument can
only make a redex at the root if that term is `i`, `k x` or `s x y`, and
all three are head normal forms, so a term a spine step applies to is none
of them. `eval_K` is the only place the proof leaves the spine, and it is
what builds the answer: the normal form of `k X` is `k` applied to the
normal form of `X`.

**Point-free combinators, checked by running them.** There is no bracket
abstraction pass in the file. Every combinator is hand compiled from the
lambda expression its docstring records, and every behavioural lemma is a
fixed number of spine steps with the arguments left opaque, which `rfl`
checks. That works here and did not in Unlambda, because normal order never
inspects an argument it has not reached. A wrong hand compilation cannot
survive: the chain then does not reduce to the term the lemma claims.

**The cost, and what the tests can therefore cover.** `Langlib.Ski.step`
rescans the whole term to find each leftmost redex, so a run costs the size
of the term times the number of steps. The empty URM program compiles to
1004 combinators and finishes in 50 ms; a URM program with one instruction
compiles to 9121 and does not finish in twelve million steps, which take
four minutes. So the tests are in two suites: the URM one covers what runs
end to end, and a counter-machine suite covers the half that is new here,
against an executable counter interpreter, in milliseconds.

`derived skiComplete` is wired as `turpentine exec --via ski --tc`, which
makes SKI the one target in the library that reports an answer without
having an output instruction.

## 2026-08-30: Unlambda is Turing complete, by the functional route

`unlambdaComplete : TuringComplete UnlambdaLang`, axiom-clean. The first
completeness result in the library that is not a machine simulation: the
target has no store and no jumps, so the argument is bracket abstraction
applied to a program written in a lambda notation that exists only inside
the proof. See [unlambda/computability.md](unlambda/computability.md).

**The counter machine is now shared.** The register-machine half of the
brainfuck proof was never about brainfuck. `Cmd`, its big-step semantics,
and the URM-to-counter compiler with `counterProgram_spec` moved to
`Langlib/Computability/Common/Counter.lean`, leaving brainfuck with the tape
layout that is actually its own. Thue already reused them and now says so
by importing the shared module. A new backend therefore has four commands
to interpret and nothing else: increment, decrement, emit a byte, and a
while loop.

**What the second half looks like.** A register is a Scott numeral, the
file holding them is a Scott list with every index unrolled at compile
time, and the answer comes back in unary, one byte per unit of register 0,
which leaves nothing for the decoder to prove. Both data predicates are
behavioural rather than syntactic, because applying the successor to a
numeral gives a term that branches like `m + 1` without being the numeral
literal for it.

**Three things call by value forces**, and they are the content of the
proof rather than incidental:

* The textbook bracket-abstraction clause `[x] e = k e` for an `e` without
  `x` is **unsound**. It evaluates `e` when the closure is built, so an `e`
  that prints prints at the wrong time and an `e` that loops loops
  unconditionally. Restricted to closed *value expressions* it is sound,
  and it is not optional: without it a Scott numeral costs `3 ^ n`
  combinators instead of `4 * n`.
* A loop's zero test has to wrap both branches in an abstraction and force
  the chosen one afterwards. Unguarded, the body runs once on a register
  that is already zero, and then forever.
* `Y` diverges, so the fixed point is the strict variant, defined as a
  substitution instance so that unfolding it is an identity rather than an
  appeal to an extensionality the equivalence does not have.

**Counting the machine's own steps.** `Counter.lean` gained `EvN`, the
same big-step relation with a step count, and `EvN.split`. The `loopS`
premise is a derivation for `b ++ Cmd.loop r b :: cs` whose two halves are
not subderivations of it, and the compiled loop needs them separately;
counting the steps is what lets the simulation recurse on a number.

**And the compiler that comes with it.** `derived unlambdaComplete` is a
verified Turpentine-to-Unlambda compiler with no backend written, reachable
as `turpentine exec --via unlambda --tc`. It is correct and impractical:
adding one to one compiles to 1.4 million combinators and sixteen million
machine steps, and factorial of five does not finish in two billion. The
compiler page now also carries a correction, since it used to recommend
the bracket-abstraction clause the proof has shown to be unsound.

SKI is the open half of the functional route, and Unlambda's witness does
not carry over to it: SKI is normal order rather than call by value, and
it has no output instruction, so its answer has to be a normal form rather
than a stream of bytes.

## 2026-08-30: the crazy operation consumes its operand

A short follow-up with one finding, which sharpens what `crz_two_steps`
buys a backend. `exec_crazy` writes out both memory effects of a `p` step,
and the first is the constraint: **`p` writes its result to `mem[d]`, the
cell it just read the operand from**, so a constant is destroyed by being
used (`crazy_consumes_operand`). A value cannot be built by returning to
one cell and combining against it repeatedly; every crazy operation needs a
fresh constant. The only infinite supply of constants in a loaded image is
the 6-periodic fill, which offers six values, so a loop that builds
arbitrary values has to regenerate its own constants rather than read them
off a table. That is now the sharpest open question for the backend.

The second effect explains a runtime error the test suite already had a
case for. The crazy operation writes at `d` and the encryption that follows
reads at `c`. If the two coincide, the encryption sees the result of the
crazy operation, which is essentially never a printable word, and the
interpreter crashes. `c` and `d` start equal, so a prologue has to separate
them before any arithmetic happens; `rotcrash.mu` is that mistake in three
characters.

## 2026-08-30: two crazy operations reach anything

The compiler page for Malbolge Unshackled argues that a backend should
avoid `*` entirely, since the rotation width is read by exactly one
instruction and dodging it makes a backend correct at every legal width.
That trade is only worth taking if the crazy operation alone computes
enough. It does, and the bound is exact.

`crz_trit` proves the operation is tritwise, at every position and in the
repeating trit, so the question reduces to nine cases of Olmstead's table.
Reading it by rows: an accumulator trit of 0 reaches 1 and 2, one of 1
reaches 0 and 2, one of 2 reaches everything. So **one operation is not
enough** (`crzTrit_zero_ne_zero`: a 0 can never produce a 0) and **two
always are**, because every row reaches 2 and the row for 2 reaches
everything:

```lean
theorem crz_two_steps (a : Value) {t : Value} (h : t.Normalized) :
    ∃ k₁ k₂, Value.crz (Value.crz a k₁) k₂ = t
```

Any value becomes any other in exactly two `p` operations against chosen
constants, and the constants are computed rather than searched for. Since
a compiler owns what sits in memory, that is the primitive a data-driven
branch needs: a branch is a computed jump-table entry, and writing one
costs two crazy operations.

The supporting lemma is value extensionality, `ext_of_trits`: normalised
values with the same repeating trit and the same trits are equal. Without
it a tritwise argument cannot conclude an equation between values, and
`stripLead` and `padTo` both had to be shown invisible to `trit` first.

`docs/malbolge-unshackled/compiler.md` was rewritten in the same batch to
carry all of the Malbolge Unshackled findings in one place: the three
obstacles with the theorem for each, the closed-off route through virgin
memory, the rotation width reclassified from hardest obstacle to avoidable
one, the verified loop a dispatcher can be built on, and what a backend
still has to solve.

## 2026-08-30: a Malbolge Unshackled program that provably never halts

`Langlib/Examples/MalbolgeUnshackled/loop.mu` is a 201-cell program the
loader accepts whose execution settles into a three-step cycle, and
`Langlib.Computability.Unshackled.Loop.neverHalts` proves that cycle runs
for ever: at every fuel bound the interpreter reports `outOfFuel`, so no
halt and no runtime error, ever. It is the first LangLib theorem asserting
anything about a Malbolge Unshackled run of unbounded length.

The cycle is `movd` at 154, then `jmp` at 155 twice:

```text
c=154  d=200  movd      mem[154]=74
c=155  d=198  jmp       mem[154]=70
c=155  d=199  jmp       mem[154]=74   (restored)
```

Three cells carry it, and the reason each works is the point of the entry:

* **155** holds 37, which decodes to `jmp` at an address congruent to 61
  modulo 94. A `jmp` never encrypts itself, so this cell is never written
  for the whole run.
* **154** holds 74, `movd` at an address congruent to 60 modulo 94. It is
  encrypted **twice** per cycle, once by executing and once by being the
  first jump's target, and `74 ↦ 70 ↦ 74` is `xlat2`'s two-cycle. So it is
  restored every pass. **A cell that is both executed and jumped onto
  advances two orbit steps per cycle**, which is what makes a two-cycle
  word survive, and it is the trick the whole construction turns on.
* **153** is the second jump's target, encrypted once per cycle. The
  invariant does not track its word at all: encryption keeps a printable
  word printable, and printable is all this cell has to be.

The jump table is at 198 and 199, read at consecutive `d`, which is the
shortest spacing yesterday's `gap_of_repeated_word` permits; cell 200 holds
197, three below itself, which is what returns `d` each cycle. Designing
around that law is what made the program 201 cells rather than a handful:
the data values have to sit above 126 so the loader stores them unchecked,
and the `movd` residue is 60 modulo 94, so the loop cannot start before
address 154.

The proof is three step lemmas and a disjunction of three phase
predicates, each a few `Memory.get` equations plus the two registers.
Nothing is computed anywhere: `get_set_self` and `get_set_ne` push each
phase to the next, and `neverHalts_of_invariant` finishes. That is the
payoff of writing the invariant with `get` equations instead of memory
equality, and it is the shape an unbounded data-driven loop will need too,
where the reachable set is infinite and computation could not help.

Honest gap: the theorem covers every state in the cycle, but that `loop.mu`
*reaches* one, after a 154-step no-op prologue, is checked by running the
interpreter and by a golden test, not in the kernel. Kernel evaluation is
not a route: ten steps of `run?` on a loaded image takes seconds and does
not reach a normal form, because `load` and `Memory` are built on
`Std.HashMap`. Closing it means proving the prologue symbolically too.

No semantics were changed.

## 2026-08-30: how a Malbolge loop actually works, and the gadget that proves one

Second batch on Malbolge Unshackled, and it corrects the first. Yesterday's
entry said an unbounded loop would need cells from the long `xlat2` orbits
phased so exactly one of a run fires per pass. That is not the mechanism.

The interpreter reads the word to encrypt **after** the instruction has run.
Every instruction leaves `c` where it was, so every instruction overwrites
its own cell, which is what `decode_encrypt_ne` makes bite. `jmp` has
already moved `c` to its target, so the encryption lands on the target and
the jumping cell is untouched. **`jmp` is the only self-preserving
instruction in the language** (`jmp_cell_stable`), and that is the whole
reason anything can loop. The reference semantics knew it: the comment in
`Semantics.lean` says the encryption is "after a jump that is the *target*,
never the jump itself". What was missing was the consequence.

So a loop is a stable `jmp` reading a table of targets while `d` walks
through it. Tracing `cat.mu` against our own interpreter shows exactly that:
from step 38 the control cycle is `37, 38, 60, 61, 61` and back, five steps,
with cell 61 firing `jmp` on two consecutive steps without changing, reading
its table at `d` and `d + 1`.

The full control state repeats with period **3060**, after an 89-step
prologue. That is `lcm 68 9 6 5 4 2`, the lcm of the encryption table's
orbit lengths: the loop closes exactly when every cell it touches has come
back round. `truth.mu` on input `1` has period 408, which is `68 * 6`. Both
are measurements against `Semantics.lean`, flagged as such in the docs.

Consecutive table entries turn out to be nearly forced, and that is a
theorem. Every cell of a loadable program must decode to one of the eight
opcodes at its own address, so if one target value appears at two addresses
`g` apart, `g` is a difference of two opcodes modulo 94
(`gap_of_repeated_word`). Only 43 of 94 gaps qualify, and of the small ones
only 0, 1 and 6. **Not 2** (`no_repeated_word_gap_two`), which rules out the
shortest jump-table loop a compiler would reach for.

The reusable half is `neverHalts_of_invariant`: a set of states closed under
one iteration proves the run consumes every fuel bound without reporting a
result, restated at the language interface as `image_neverHalts` and
`not_halts_of_invariant`. It goes through `step1` and `step1_sound`, whose
only job is to be provably the body of `exec`, so none of this can drift
from the reference semantics. The point of the invariant shape is that the
predicate is written with `Memory.get` equations rather than memory
equality, so discharging one needs neither hash-map comparison nor a long
kernel evaluation; `get_set_self` and `get_set_ne` (via `LawfulBEq Value`
and `LawfulHashable Value`) are the only memory facts required. An
unbounded loop over an unbounded counter will need exactly this shape, since
there the reachable set is infinite and computation would not help.

Still open, and now a bounded task: no `P` has been written down and
discharged for an actual image, so LangLib does not yet assert that any
particular Malbolge Unshackled program runs forever.

No semantics were changed. The only edits outside
`Langlib/Computability/` remain the visibility of five internal helpers
(`natTritsAux`, `padTo`, `succTrits`, `doOutput`, `doInput`, `step`), which
proofs have to be able to name.

## 2026-08-30: Malbolge Unshackled, the ground floor of a completeness proof

Malbolge Unshackled is one of Stage 8's open positive claims.
This is the start of it. There is no `TuringComplete` witness
yet and this entry does not claim one; what landed is
`Langlib/Computability/MalbolgeUnshackled/Main.lean`, axiom-clean, containing the
layer a witness has to be built on and the two theorems that say why the
obvious constructions do not work.

The `ProgLang` instance names the language: a program is a loaded `Image`,
the parser is the loader, the runner is `evalImage` at the default
configuration.

The arithmetic of addresses is proved rather than sampled.
`succ_ofNat` says 3-adic successor is ordinary increment on the naturals,
`modClass_ofNat` says the decreed residue of a natural is `n % 282`, and
`decode_at_ofNat` puts them together: the instruction a cell holds is a
function of its word **and its address**. `exec_hang`, `exec_halt` and
`exec_step` are the three exits from the interpreter's dispatch, and
`exec_of_hang` proves Johansen's `hang` never halts, never errors and never
emits.

Then the two obstructions, which are the point of the entry.

* `decode_encrypt_ne`: `xlat2` has no fixed point and the 94 printable codes
  are 94 consecutive naturals, hence distinct modulo 94, so **no cell
  executes the same non-`nop` instruction on two consecutive executions**. A
  loop whose body is a fixed instruction sequence is not expressible in this
  language. Loops have to be cycles through the encryption table's orbits,
  whose lengths are 68, 9, 6, 5, 4 and 2.
* `restTable_not_printable`: the 6-periodic memory fill that covers the
  addresses the loader never reached produces, at three of its six residues,
  values whose repeating trit is 1. Those are not naturals, so not
  printable, so executing one hangs. **A program cannot walk off its own end
  into an infinite supply of fresh instructions.** That strategy is the one
  thing Unshackled's infinite address space appears to offer over Malbolge,
  it is the first thing one reaches for, and it does not work.

The constructive half is `alternatingCell`, a table of eight cells built
from `xlat2`'s single 2-cycle `70 ↔ 74`, one per instruction, checked in the
kernel. Every instruction is available as a loadable period-2 cell, so
instruction choice is free; the residue is forced modulo 94, so instruction
*placement* is the real cost, and padding is scarcer than instructions
(only 14 of 94 residues admit a cell that both loads and stays harmless
through its whole orbit). The table also shows the phase is forced: an
alternating cell always fires on its first execution, never on its second,
which is why a loop cannot be assembled from two half-bodies of opposite
phase.

One finding is worth flagging because it contradicts the received wisdom in
`docs/PLAN.md`. The free choice of rotation width, described there as
something no other target has an analogue of, is read by exactly one
instruction. A compiler that never emits `*` never observes it, and is then
correct at every legal width rather than only at the reference minimum. The
price is that the crazy operation becomes the only arithmetic, which pushes
registers towards unary counters spread over memory cells, which is exactly
the resource Unshackled has and Malbolge lacks.

Next: loop construction from the longer orbits, phased so exactly one cell
of a run fires per pass. That is the HeLL assembler's technique and
everything else waits on it. `docs/malbolge-unshackled/computability.md`
has the full account, including what is cited rather than proved.

## 2026-08-30: Piet examples that loop, branch, and hang a painting

Every Piet example was straight-line — push, compute, print, stop — which
left the hard half of the language undemonstrated. Control flow in Piet is
geometry: a loop is a closed circuit through a white return corridor, and a
branch is `pointer` rotating the DP into one corridor or the other.

Four new programs in `Langlib/Examples/Piet/`, with golden tests:

* `count.ppm` (40x3) prints 1 to 10. The first example with a cycle in it.
* `truth.ppm` (13x3) is the truth-machine, and at thirty-nine codels the
  whole loop skeleton is legible in one codel map.
* `collatz.ppm` (65x3) reads n and prints its hailstone sequence. The
  Collatz step wants a second branch and does not take one: with r = n mod
  2, both cases are `(n*(1+2r) + r) / (2-r)`, so it costs one `mod`, one
  `div` and two `roll`s instead of a change of direction.
* `mondrian.ppm` (48x34) prints `Piet`, and everything below its top three
  rows is a painting in Mondrian's palette that the pointer never enters —
  which is the point: unreachable blocks cost nothing and constrain
  nothing.

`scripts/gen-piet-examples.py` lays them out, because nobody paints a loop
by hand. It implements the two codel geometries `linearGrid` and `loopGrid`
from `Langlib/Computability/Piet/Main.lean` — the ones the completeness proof
already uses — plus cheap constant building (a square with a correction
beats a block of n codels above about twelve). Its output is checked the
only honest way, by running the programs.

`docs/piet/spec.md` walks all four with their pictures;
`scripts/render-docs-images.sh` renders them, `mondrian` without `--grid`.
`lake test` is green at 1108 tests.

## 2026-08-30: `--to piet` exists

`derivedPiet` had been correct-by-construction since Piet's completeness
proof landed, and unreachable from the command line the whole time: the
`backends` table in `Langlib/Languages/Turpentine/Main.lean` had no `piet`
row, so `--to piet` was the *example of an unknown target* in
`docs/certified-compilation.md`. It is a target now.

**The missing piece was a painter.** The completeness proof produces a
`Grid`, and `Grid` is the parser's output type; nothing in the library went
the other way. `Codel.toRgb` in `Langlib/Languages/Piet/Syntax.lean` is the
inverse of the palette table `colorOfRgb` reads, `Grid.toImage` paints a
whole grid, and `Image.toPpm3` writes it — so the emitted file is ASCII P3
PPM at codel size 1, exactly what `lake exe piet` reads.

Painting a codel and reading it back is proved to be the identity
(`colorOfRgb_toRgb`, twenty cases by `rfl`), which is the codel-level half
of "the image the compiler wrote is the grid it meant". The whole-grid round
trip is carried by test: `Langlib/Tests/DerivedPiet.lean` gained a second
suite that renders the PPM and hands it back to `Piet.run`, so the CLI's
actual path — codegen, renderer, parser, `evalGrid` — is what runs. All
982 tests pass.

**The size and the speed, measured rather than guessed.** A compiled
`answer := 2` is a 3,516-codel image that prints `2` in about two seconds.
`fact-tc.turp` compiles in 1.4 s to `51135 x 3` codels and had printed
nothing after twenty minutes; `sum.turp`, which adds 0 through 4, compiles
to `30501 x 3` and behaves the same way. The cause is not the register
machine: Piet block-finding is a flood fill *per step*, so instruction cost
grows with image size while singleton normalization grows the image with the
program. `docs/piet/compiler.md` says so, with the numbers.

`docs/certified-compilation.md` needed a different unknown target for its
error example (`befunge93` now) and gained a Piet block beside the FRACTRAN
one, since the two are the interesting artifact shapes: a fraction list plus
a starting integer, and a picture.

## 2026-08-30: every spec ends with programs you can read

Documentation and one new script; no Lean touched.

Each of the fifteen `docs/<lang>/spec.md` pages now ends with an
**Example programs** section: three to six complete program texts in the
language, quoted in full, each with a paragraph on how to read it and what
it does. The texts are the files in `Langlib/Examples/<Langname>/` wherever
one fits, and every claimed output was produced by running the program, not
recalled.

**The two graphical languages show their programs.** Piet's and
Brainloller's example sections now carry the rendered picture beside every
text, and each page ends with a "Rendering these pictures" subsection giving
the commands. The pictures were previously produced by hand-run commands
whose parameters lived nowhere; `scripts/render-docs-images.sh` now holds
them, regenerates all ten images byte-for-byte identically to what was
committed, and with `--check` fails if any is stale. `docs/TESTING.md`
records it as a third check alongside `lake test` and `difftest.sh`, and
`CLAUDE.md` makes "images are derived files, regenerated by that script" a
policy. Piet's "The examples, in colour" section was merged into "Example
programs" rather than left to say the same things twice.

Where a program is not text, it is transliterated and the transliteration is
stated:

* **Whitespace** — `S`/`T`/`L` for the three tokens, one instruction per
  line, with the disassembly beside it, since the real files show nothing at
  all in an editor.
* **Piet** — the rendered SVG, the literal P3 PPM for `add.ppm` and
  `square.ppm` (they are eight codels by three), a codel map writing each
  codel as lightness and hue, and the (hue steps, lightness steps) reading
  of every transition.
* **Brainloller** — the rendered PNG, a codel map using the eight brainfuck
  characters plus `↻`/`↺` for the rotation colours, and the PPM for the
  three-by-three `cat.ppm`.

Two things turned up in the writing. `docs/piet/spec.md` claimed `square.ppm`
differs from `add.ppm` by two codels; it is one (`0 192 0` becomes
`192 255 192`, turning `in add` into `dup mul`), now corrected. And the
smallest program that runs and halts in Malbolge and in Malbolge Unshackled
turns out to be two characters, `QC` — `Q` decodes as halt at address 0, and
the second character is there only because the memory fill needs two words.

`CLAUDE.md` records the section as policy, so new languages get one.

## 2026-08-30 (latest, earlier): Turpentine is a language, and compilation has an I/O-aware theory

Three structural changes, no new language and no new compiler.

**Turpentine moved to `Langlib/Languages/Turpentine/`.** It was the one
language in the library living outside `Langlib/Languages/`, for no reason
except that it was written first. The namespace is unchanged
(`Langlib.Turpentine`, exactly like `Langlib.Brainfuck` under
`Langlib/Languages/Brainfuck/`); the module path, the lakefile's executable
root, two `open private ... from` module references and every documentation
link followed.

**`Langlib/Computability/Class.lean` is gone**, replaced by two modules in
`Langlib/Common/` split by what they cost:

* `Common/Compilation.lean` — `ProgLang`, and what it means to compile a
  language correctly. Free of Mathlib and cslib, deliberately, so that a
  hand-written backend can state and prove its own correctness without
  either reaching the interpreters.
* `Common/Computability.lean` — `TuringComplete`, `BoundedStorage`,
  `BoundedRun` and the decidability that follows from a bound. The one
  module in `Common/` that needs cslib, and therefore the one
  `Langlib/Common.lean` does not roll up.

`Derived.lean` moved with the compilers it builds, to
`Langlib/Languages/Turpentine/Compile/Derived.lean`.

**Certified compilation became generic, and acquired an I/O-aware
sibling.** `CertifiedCompilerNoIO spec L` is parameterised by the source
specification, so `agree` and the new `weaken` are proved once for every
source and target; `TurpentineCompiler L` is that type at
`TurpentineHaltsWith` and everything already proved kept working
unchanged.

The new statement is the one the library did not have. A run's observable
behaviour is a `Trace` of interleaved `inp`/`out` events; a language opts
into reporting one with a `TraceLang` instance, subject to two laws tying
the report back to its interpreter; and `CertifiedCompiler` demands that
a compiled program reproduce the source's trace, under an encoding the
compiler declares as data, as well as its answer.
`CertifiedCompiler.toCertified` proves the behavioural notion implies the
answer-only one, so nothing already proved has to be reproved when a
backend is upgraded.

Nothing inhabits `CertifiedCompiler` yet, on purpose. The prerequisite is
per-language: an interpreter has to record its events. FRACTRAN got the
first `TraceLang` instance for free, since its `run` provably ignores the
input stream and `TraceLang.ofInputFree` discharges the side condition by
`rfl`. `docs/PLAN.md` Stage 6 sequences the rest.

`lake build` and `lake test` clean (979 tests); `scripts/axioms.lean` audits
the new definitions and reports the three standard axioms or fewer —
`CertifiedCompilerNoIO.agree` needs none at all.

A consistency pass over the documentation afterwards turned up three stale
spots, none of them caused by the refactor and all of them about which
proofs are done. `docs/README.md`'s legend still described `fractran` and
`piet` as proofs under way; `docs/agent-brief-completeness.md` still told a
new agent to take those two next and listed `thue` as open and `ook` and
`brainloller` as uncollected; and `docs/PLAN.md`'s Stage 8 table applied its
"PROVED" marker to four of the ten languages that have one. All three now
match the code: eight `TuringComplete` witnesses, three decided halting
problems, and `unlambda`/`SKI`, `malbolge-unshackled` and Turpentine itself
still open. Brainfuck's "bespoke correct" cell went from `wip` to `-`, since
no such proof has been started.

## 2026-08-30 (late): every spec names a resource that defines its language

An audit of the fifteen `docs/*/spec.md` headers against the documentation
policy. Eleven already cited a reachable canonical source; the other four
cited something a reader could not follow, and Turpentine cited nothing at
all because it has no external definition.

* **unlambda**: named Madore's page without linking it. Now
  http://www.madore.org/~david/programs/unlambda/, with the distribution
  named as the file the page actually offers (`unlambda-2.0.0.tar.gz`).
* **ski**: had a bibliography with no locators. Schönfinkel and Curry now
  carry page ranges and DOIs.
* **malbolge-unshackled**: claimed a "Malbolge Unshackled page" by
  Johansen. There isn't one. The language is defined by his public-domain
  Haskell interpreter, http://oerjan.nvg.org/esoteric/Unshackled.hs (whose
  header dates it to Feb 2007), plus the deviations described on the
  esolangs page that links it as the reference implementation. The header
  now says so, and gains the **Year** field it was missing.
* **brainfuck**: cited `bf.tar.gz` on Aminet, unlinked. The upload is
  Müller's own, June 1993, and is called `brainfuck-2.lha`:
  http://aminet.net/package/dev/lang/brainfuck-2.
* **subleq**: `mazonka.com` is down (HTTP 523 on every attempt), so the
  tool page now carries a Wayback snapshot beside it, and the
  Mazonka-Kolodin paper gets its arXiv link.
* **turpentine**: not an esoteric language and has no upstream, so the
  header now says explicitly that the page itself is the specification and
  `Langlib/Languages/Turpentine/` the reference implementation, rather than leaving a
  reader to wonder what it was written against.

Every URL in every spec page was fetched: all 34 resolve except
`mazonka.com`, which is the one now archived.

## 2026-08-30 (night, later): Piet proved Turing complete

`pietComplete : TuringComplete PietLang` landed, and with it `derivedPiet`.
The language whose programs are abstract paintings now has a
machine-checked completeness proof, and the proof is stated against
`evalGrid` itself: the DP and CC rules, the eight exits of every colour
block, the white slides and the halt are the ones the reference evaluator
implements, not a paper idealisation of them.

The arithmetic and the primitives landed earlier today. What closed the gap
was composition, and it went in five pieces. `exec_toPivot` runs the
dispatcher body: the corridor, then the `switch` and the `pointer`, which
are exactly the two commands a corridor may not contain, since they move
the chooser and the direction. The two branches out of the pivot were
already proved, so `reaches_iteration` is one whole turn of the loop —
corridor, pivot, `pop`, return corridor, back to the first codel of the
body with the chooser where it started, because the `switch` toggles it
once and the corridor's three blocked turns toggle it once more. `exec_run`
composes those over `Cslib.URM.Steps`, `exec_entry` covers the start slide
and the prologue that loads the register file, and `simulation` assembles
the whole thing and reads the answer out of the decimal the image printed.

Two things had to be said carefully. A program counter that is already past
the end of the source still runs one iteration, so the halted dispatcher
needed its own lemma; and the induction has to know that the intermediate
states of a halting run are *not* halted, which comes from cslib's
`no_step_of_halted`.

Also: `StableCode` now has a lemma per generator, which is what lets the
corridor claim anything at all about the dispatcher's own code.

975 tests. Every language in the library with a positive computational-class
claim now has a machine-checked one, except Malbolge Unshackled, Unlambda
and SKI, which landed as languages today and whose proofs are Stage 8 work.

## 2026-08-30 (night): the Piet dispatcher computes, and the terminal halts

Piet's completeness proof had a shape problem: the command traces were
verified against `execOp`, but nothing said what they *computed*, and the
image-level story was untouched. Both halves moved.

`stackOf` models the dispatcher's stack as a URM register file plus the
three control slots, and `dispatchUpdate_step` proves one dispatcher pass
performs exactly one `Cslib.URM.Step`. The argument is the masking one the
design rests on: a guard of zero makes an instruction the identity, the one
instruction the program counter selects applies its arithmetic, and `J`
writes its target to the fall-through counter exactly when both the guard
and the register comparison hold. `runCode_dispatcherCode` lifts that to a
whole iteration.

The geometry then needed one design change, and it came from a fact worth
writing down: **a singleton colour block can never halt a Piet program**.
Whatever codel the program arrived from is an unblocked neighbour, and one
of the eight selected exits steps straight back into it. The terminal block
is therefore an L of three codels, the smallest shape that can hide its own
entry, which also made its flood fill provable: ten worklist steps over a
symbolic grid, with the visited array tracked through three `set!` calls at
distinct indices. `mkInfo` then computes all eight exits in one `simp`, and
every one of them is blocked.

The white transits are proved too, including the three-turn return
corridor, whose variable-length leg carries the invariant that makes the
interpreter's revisit check fail: every remembered (codel, direction) pair
is either in another direction or strictly to the right of where the slide
now is. The three blocked turns leave the chooser toggled once, which is
exactly what the dispatcher's trailing `switch` was already compensating
for — the layout and the arithmetic agreed before either was proved.

What is left is composition rather than discovery, and
`docs/piet/computability.md` lists it: the two corridor instantiations, the
pivot, the induction over `Cslib.URM.Steps`, and the assembly. The image is
one column narrower than it was.

## 2026-08-30 (later): Malbolge Unshackled, Unlambda and SKI wired in

The three trees the 2026-09-01 handoff note left as "in flight and
INCOMPLETE — verify before trusting: the agents died mid-task and their
examples were never checked" are now finished languages. Everything was
verified rather than assumed, and everything worked, which was not the
expected outcome.

Each of the three gained a `lakefile.toml` runner, an import from
`Langlib.lean`, a golden-test suite in `lake test`, a language README, a
`docs/<lang>/spec.md` with its semantic decisions numbered, and a
`compiler.md`. `Langlib/Languages/MalbolgeUnshackled.lean` had to be
written; the other two root modules already existed.

The interpreters themselves needed no changes. The Unlambda machine
handles `c` and `d` exactly as its docstring claims, `hello.mu` prints
`Hello, world!` at three different rotation widths, and every example in
all three directories runs. Three test expectations of mine were wrong
before the code was: `hello.mu` ends with a newline, and `KKSI` is
`((KK)S)I`, which normalises to `KI` rather than `K`.

The spec pages record what the implementations already decided. The ones
worth naming: Unlambda's `e` exits (the two C interpreters in Madore's
2.0.0 distribution parse it as a second `c`, contradicting the
specification, the Java interpreter and the Scheme one); Unshackled's end
of input is `...22`, which *closes the output stream* rather than printing
a byte; and Unshackled's encryption step can crash, because a rotated word
need not be a printable natural and Johansen's interpreter calls `crash`
where Malbolge would shrug. That last one has its own three-character
example now, `rotcrash.mu`, which is the only Unshackled program here we
wrote ourselves.

Which is the loose end. `hello.mu`, `truth.mu`, `cat.mu` and Unlambda's
`quine.unl` arrived with those unfinished branches and their authorship was
never recorded. They run, but Malbolge's own examples credit Cooke and
Scheffer by name and these credit nobody. Both READMEs say so and ask for
the attribution.

972 tests.

## 2026-08-30: Thue proved Turing complete

`thueComplete : TuringComplete ThueLang` landed, and with it
`derivedThue`, so the string-rewriting language now has a certified
Turpentine compiler like the machine-shaped ones. Post settled the
mathematics in 1947; what was missing was a check that a *deterministic
interpreter* following a *particular* strategy cannot wander off the
intended derivation, and that is where the work went.

The generator, the encodings and the rule-family separation lemmas were
already in place. Three things closed the gap.

The first is small and does all the load-bearing: a phase token plus the
one character next to it determines which rule applies, because every
canonical family reads exactly one adjacent cell (`reaches_phase_right_cell`,
`reaches_phase_left_cell`). Combined with the unique `@` marker, that turns
`Thue.firstMatch` — a search over a thousand rules and every position in the
string — into a function on represented states.

The second is `reaches_exec`, which lifts a whole big-step counter-machine
derivation to a run of the generated rules. Rule availability travels as a
subset of `generate done code suffix`, which shrinks on every step except
`Ev.loopS`, where the continuation becomes `body ++ loop :: rest`. That case
needed `generate_append`: generation is compositional in the code it
traverses, so unrolling a loop asks for no rule the loop did not already
generate. The macros it consumes are `reaches_inc` (which was already there),
`reaches_dec`, both sides of `reaches_zeroTest`, and `reaches_emit`.

The third is dispatch. `reaches_finish` seeks the counter holding
`nextProgramCounter + 1`, counts it down to nothing (which also clears it,
restoring the invariant the next macro needs), picks the destination, and
walks the token home. `outcomes_functional`, proved earlier, is what makes
the pick deterministic: several outcomes can share a unary count, but then
they name the same program counter, so they are the same rule.

Halting came out as the mirror of the control step. `firstMatch_eq_control`
says a source control marker selects that instruction's entry rule;
`firstMatch_control_none` says that once the program counter has run off the
end, *no* generated rule matches anywhere in the string, which is exactly
Thue's halting condition. The final state is then printed by
`Config.finalState` and read by `decodeOutput_encodeState`.

Two smaller things fell out. The left-moving return scan is now stated for an
arbitrary phase, so `backPC` reuses it and `reaches_back_across` and
`reaches_back_home` became corollaries. And the three counter scans share one
`reaches_scan_prefix`.

`scripts/thue-cost.lean` replaces the scratch runner the notes referred to,
so the sizes in `docs/thue/computability.md` are reproducible: the
one-iteration addition program is 1,211 rules, a 17-character initial state
and exactly 1,665 rewrites.

885 tests.

## 2026-08-29: Malbolge's halting problem, decided

The finite-control count from earlier this week said nothing about a
*step*, so it settled nothing. It does now: `malbolgeHaltingDecidable`
decides halting for every loaded Malbolge image, which is the form
incompleteness takes in this library.

Three pieces, and only the first was the one the notes predicted.

`Langlib.Malbolge.exec` recurses at the front and returns early on a halt,
so `exec (n+1)` is not `step (exec n)`. `stepOnce` is the loop body with
the recursive call replaced by "stop here" (`exec_one` is `rfl`), `advance`
makes halting absorbing, and `exec_succ` supplies the missing law.

`RunWF` is the invariant a reachable state satisfies, and `runWF_exec`
carries it through the whole run. This is where the arithmetic lives:
`rotR`, `crz`, `encrypt`, a read byte and `maxWord` each need their own
bound, plus `Array.set!` size preservation.

The configuration drops the output, because it grows without bound and no
instruction reads it, and `config_ext` proves the 59049-word control
determines the rest: memory by array extensionality, registers and cursor
by `Fin` injectivity, the input data because the run fixes it.

Two things fell out on the way. First, `BoundedStorage` demands its
finiteness laws of *every* inhabitant of the configuration type, which
Malbolge's input-dependent cursor cannot satisfy; but reading
`halts_iff_search` shows it only ever uses them at reachable
configurations. So `Class.lean` now also has `BoundedRun`, with the laws
stated there, the pigeonhole proof moved to it, and
`BoundedStorage.toBoundedRun` keeping every existing witness and
`Deadfish.no_boundedStorage` true as stated.

Second, the module could not be imported into a compiled executable at
all. `deriving Fintype` on `MalbolgeCore` produces a top-level *value*,
evaluated when the module loads, and enumerating 59049^59049 memories
overflows the stack immediately. Both `Fintype` instances are now
noncomputable, which is why `Langlib/Tests/BoundedMalbolge.lean` could
finally be wired into `lake test`, where it had never run.

718 tests.

## 2026-09-02: the first certified compilers

`compileToURM` and its correctness theorem landed, which was the piece
everything else waited on, and with it `Langlib/Computability/Derived.lean`:
the `TurpentineCompiler` interface, the `derived` construction, `agree`,
and `derivedWhitespace`. All axiom-clean.

The payoff is the one the design promised. `derived` takes any
`TuringComplete L` and returns a verified compiler, so applying it to
`subleqComplete` gives a certified Turpentine-to-subleq compiler with no
subleq-specific work at all; checked by instantiating it and auditing the
axioms. Two languages now have a certified compiler, and any language
proved complete from here gets one for free.

668 tests.

## 2026-09-02: Subleq proved Turing complete

The second completeness proof, and the easy one, exactly as predicted: a
URM register is one subleq memory cell holding the value directly, because
subleq words are arbitrary-precision and memory is unbounded. No encoding,
no range cap, and not one lemma in the file carries a range side-condition.

The interesting part is the `J` instruction. The URM tests equality;
subleq branches on `<= 0`. Since registers hold naturals, equality is two
`<=` tests on the same difference in both directions, which comes to nine
subleq instructions. Straight-line instructions set their branch target to
the next instruction, so the branch is invisible and no sign reasoning is
needed for `Z`, `S` or `T`.

One documented trade: `decodeOutput` counts output bytes rather than
parsing decimal, because subleq's only output primitive is a single byte
and decimal printing would need a division routine plus a self-modifying
digit buffer, out of proportion to the claim. Byte-counting is a total
function of the output and invents nothing; the cost is output size.

18 differential tests, axiom-clean, 631 tests in the suite.

## 2026-09-01 (later): the certified compilation plan

* `docs/certified-compilation.md` written: the pipeline
  (Turpentine -> URM -> target), the fragment it can accept, a dependency
  graph with dashed arrows for planned work, and the order of construction.
  Everything hangs off one missing piece, `compileToURM`, because the
  second arrow is free: it is the `compile` field of a language's
  `TuringComplete` instance, which exists as soon as somebody proves that
  language complete.
* Verified compilation is being modelled as a bundled
  `TurpentineCompiler L` **structure, not a class**, precisely because we
  want several compilers per target coexisting (a derived one and an
  effective one) and instance resolution is built to pick exactly one.
  Agreement between any two instances is then a theorem about the
  interface rather than a testing practice.
* Recommendation recorded: **keep both kinds of compiler**. The effective
  whitespace backend compiles `gcd.turp` to 532 bytes and accepts the
  whole language including I/O and negative integers; the derived one will
  be orders of magnitude larger and accepts only the I/O-free non-negative
  fragment. Neither subsumes the other.
* `scripts/axioms.lean` added, closing a gap from the previous report: it
  prints the axiom dependencies of every completeness result, since a
  theorem resting on `sorryAx` type-checks perfectly well.

## 2026-09-01: Whitespace proved Turing complete

The first entry in the `TC proved` column.
`Langlib/Computability/Whitespace/Main.lean` compiles cslib's unlimited
register machine into Whitespace and proves the compilation simulates,
yielding `whitespaceComplete : TuringComplete WhitespaceLang`.
`#print axioms` reports only `propext`, `Classical.choice` and
`Quot.sound`: no `sorryAx`, so the theorem is real. Since the URM computes
every partial computable function, so does Whitespace.

It is an instance of the uniform interface from Stage 8 rather than a
one-off theorem, so the next language states its result the same way and
the negative results will use `BoundedStorage` alongside it.

Not yet done for it: `docs/computability.md`, and the differential test
suite that runs compiled URM programs on our Whitespace interpreter. The
agent died before writing either.

## 2026-09-01: handoff state

Where things stand for whoever picks this up next. `lake build` and
`lake test` are green (582 tests), and `./scripts/difftest.sh` passes 14
comparisons against four reference interpreters.

**Done**: eleven esoteric languages with specs, interpreters, runners,
examples and tests (brainfuck, whitespace, malbolge, befunge93, subleq,
fractran, thue, ook, deadfish, piet, brainloller); Turpentine with
arrays; three compiler backends (brainfuck for scalars, whitespace and
subleq for the whole language); the website under `site/`; cslib and
Mathlib as dependencies; a `compiler.md` for every language.

**In flight and INCOMPLETE at the time of writing.** Three agents were
still working, so the following are partial. They compile and do not
break the suite, but they are not finished, not wired into
`Langlib.lean`, `Langlib/Tests/Main.lean` or `lakefile.toml`, and have no
docs pages yet:

* `Langlib/Computability/{Class,URM,Whitespace}.lean`: **the proof is
  finished and axiom-clean** (see the entry above). What is missing is
  `docs/computability.md` and a test suite.
* `Langlib/Languages/MalbolgeUnshackled/`, `Langlib/Languages/Unlambda/`
  and `Langlib/Languages/Ski/`: all four modules of each exist and the
  tree builds, with example directories started. None has tests, docs, a
  `lakefile.toml` entry, or an import from `Langlib.lean`, so none is
  wired in and none has been run end to end. Verify before trusting: the
  agents died mid-task and their examples were never checked.

**To resume**: finish or discard the three items above, then continue
with `docs/PLAN.md`. The open stages are 5 (Velvet examples), 6
(verification proofs, nothing proved yet), 8 (computational class, the
`TC proved` column in `docs/README.md` is all `no`) and 9 (derived
compilers). Stage 4 still wants the IR layer (StackIR, TapeIR, RegIR),
which is what makes the Stage 6 proofs affordable.

**Known loose end**: Befunge-93 is not parametric over cell width. It
hard-codes unbounded `Int` cells, which is why the language we implement
is Turing complete while `bef.c`'s byte-celled one is not. Making the
width a `Config` option would let both computational-class claims be
proved about one implementation, and would let the differential tests run
faithfully against `bef.c`. See `docs/befunge93/spec.md`.

## 2026-09-01

* **The brainfuck backend lands**, the hard one, covering the scalar
  language. Integers are 16-bit two's complement in two cells each, chosen
  by measurement rather than taste: 8 bits cannot run collatz on 27 (peak
  9232) or sumdigits on 9045, and 32 would double every cost for range
  nothing uses. The load-bearing trick is a division-by-two that computes
  quotient and remainder in one linear pass with a constant-size body, so
  byte comparisons are linear instead of quadratic; without it nothing
  runs. All eight scalar examples compile and match the interpreter, and
  collatz(27) prints 111 through 367 kilobytes of generated brainfuck.
  Arrays are not supported yet, and each of the six array constructs
  reports its own name when refused.
* `turpentine exec --via brainfuck` works, with the `--eof zero`
  convention the backend requires wired in. 582 tests.

## 2026-08-31 (evening)

* The status matrix now separates **TC known** from **TC proved**. The
  first is what the literature or our spec page argues, and can be wrong;
  the second is a machine-checked theorem in this repository, with a link.
  Every entry in the second column is currently empty, which is the honest
  state of things and the point of having the column.
* The table also records that **a language cannot host a full compiler
  unless it is Turing complete**. Malbolge gets a bounded fragment, not a
  planned full compiler: it has 59049 words for code and data together, so
  no total translation from a Turing-complete source can exist. Same for
  befunge93 (2000 code cells) and deadfish (no loops).
* Fixed a misattribution that had spread to three files: Malbolge
  Unshackled is Ørjan Johansen's (2007), not Matthias Lutter's. Lutter
  wrote HeLL and the first Malbolge quine.
* Malbolge Unshackled and Unlambda are being implemented, the latter to
  give the library a completeness argument by bracket abstraction rather
  than machine simulation.

## 2026-08-31 (later)

* **cslib and Mathlib are now dependencies**, reversing the
  dependency-free stance. The reason is duplication: without cslib we
  would define our own register machine and Turing machine and then
  re-prove the relationships cslib already has. The pinned revision
  `3951377e` is the last one on Lean v4.33.0, matching our toolchain
  exactly, so nothing had to be upgraded to accept it. Mathlib stays
  confined to `Langlib/Computability/` so the interpreters keep compiling
  fast.
* Marked as future work: restate the completeness results to reuse
  cslib's own machine-model equivalences, so we only ever prove
  simulations and borrow the rest. Deliberately not done yet, since the
  shape of our simulation statements has not settled.

## 2026-08-31

* **Stage 9 planned: derived compilers.** A completeness proof already
  contains a verified compiler (from a register machine into the
  language), so composing it with one Turpentine-to-register-machine
  compiler yields a verified Turpentine compiler for every language proved
  complete, without writing a backend. That makes Stage 8 infrastructure
  rather than scholarship, gives the hard targets (thue, fractran, piet,
  malbolge) a compiler at all, and provides a test oracle for the
  hand-written backends.
* The plan is explicit that derived compilers are correct and unusable,
  and that **effective** compilers stay separate: hand-written, practical,
  and separately verified, with observational agreement between the two
  falling out as a corollary rather than a third theorem. The I/O gap (a
  register machine has none, Turpentine does) is stated up front with the
  preferred resolution, a `URM+IO` extension with an embedding from the
  plain URM.

## 2026-08-30 (night)

* **Array codegen** in both backends, so whitespace and subleq again
  accept the entire language. Whitespace gets arrays nearly free: the heap
  is integer-addressed and an address is an ordinary stack value. Subleq
  cannot name a computed address at all, so the backend does what subleq
  has always done and **patches its own operands before executing them**:
  an indirect load rewrites the `A` field of the very next instruction,
  and an indirect store patches three operand words. That is the reason
  insertion sort and a sieve run on a one-instruction machine.
* Both check bounds and route to their existing traps, using a distinct
  forbidden address from the assert trap so the two failures stay
  distinguishable. 149 compiler tests (up from 105), 508 in total.

## 2026-08-30 (evening)

* Two corrections that came out of being challenged on the claims, both
  worth recording as findings rather than typos:
  * **Malbolge**: I had it as an open question and its compiler as "not
    planned". Both wrong. Malbolge is a bounded-storage machine (59049
    words of 59049 values), so it is decidably not Turing complete; the
    open questions are about Malbolge-T and Unshackled. And people do
    compile to Malbolge (Iizawa et al.'s method, Lutter's HeLL), so a
    backend is planned, via a VM written in Malbolge whose data cells
    never execute and therefore never self-encrypt.
  * **Befunge-93**: the classical "not Turing complete" claim is about
    `bef.c`, whose playfield is `char pg[80*25]` and whose stack is an
    unbounded-depth list of `signed long`: finite control plus a
    finite-alphabet stack, which is a pushdown automaton. Our
    implementation stores unbounded `Int` in both, which makes the
    playfield 2000 unbounded registers and the language Turing complete.
    The deviation was documented; its consequence was not. Both claims are
    now stated, and Stage 8 plans to prove the pair.
* Stage 8 gains a uniform interface: a `ProgLang` class (named `Esolang` until 2026-09-01), a
  `TuringComplete` structure bundling compiler and simulation, and a
  `BoundedStorage` structure with the decidability theorem proved once, so
  the negative results are short instances rather than separate
  developments. The cslib connection is staged: mirror its URM now, bridge
  in a `proofs/` package later, keep `Langlib` dependency-free.

## 2026-08-30 (later)

* Toolchain pinned to **Lean 4.33.0** (down from 4.33.1). Everything
  builds and all tests pass; the downgrade also puts us on the toolchain
  Verso tags, should the site ever want it.
* **Arrays** in Turpentine: fixed-length, one-dimensional, bounds-checked.
  Velvet's `MaxElem` and `InsertionSort` are ported, plus a sieve.
* **Computability becomes a stated goal.** Stage 8 of the plan gives every
  language a claim about its computational class and a route to a proof,
  against cslib's Turing machine and unlimited register machine. The
  README says so, CONTRIBUTING spells out what counts as evidence, and the
  status matrix carries a Turing-complete column. An SKI/Unlambda entry is
  planned so the library also has a completeness argument by bracket
  abstraction rather than machine simulation.
* **An IR layer is planned** (Stage 4): StackIR, TapeIR, RegIR, one per
  target family, so lowering passes and simulation proofs are shared
  rather than repeated per language.
* **Every language now has a `compiler.md`**, describing what was built
  where a backend exists and a concrete plan where one does not, including
  arguments for why a general backend is the wrong thing to build for
  befunge93 (80 by 25 playfield) and malbolge (self-encrypting code).
* **The website landed**: `site/`, its own Lake package, 21 pages
  generated from the docs, three in-browser playgrounds (brainfuck,
  whitespace, deadfish) verified under node.

## 2026-08-30

* Stage 4 opens for real: compilers from Turpentine to **whitespace** and
  to **subleq**, both accepting the entire language rather than a
  fragment. All eight Turpentine examples compile on both backends and
  produce output identical to the reference interpreter, with one
  documented exception (`cat.turp` on whitespace, which cannot test for
  end of input and so dies there by design).
* The interesting gaps are recorded rather than hidden: whitespace floors
  its division while Turpentine is Euclidean, so the backend emits a
  sign-correction sequence, checked against the reference on all 361
  operand pairs in -9..9. Subleq needed none of that, its `-1` EOF
  convention matching Turpentine exactly.
* `lake exe turpentine compile --to <lang> [-o out]` wires the backends
  into the runner. 445 tests, all passing.

## 2026-08-29 (late night)

* Piet and Brainloller landed, the graphical pair. `Langlib/Common/Image.lean`
  adds an RGB image type and a PPM reader (P3 and P6) shared by both.
  Piet implements the colour wheel, DP and CC with the eight-attempt rule,
  white sliding per the 2004 clarification, and the 17 operations; blocks
  are flood-filled once so each step is constant time. Brainloller decodes
  pixels into the brainfuck core and also ships an encoder, so
  `--encode` turns any brainfuck program into a picture.
* 340 golden tests, all passing. Eleven languages plus Turpentine.

## 2026-08-29 (night, later)

* Malbolge landed: the loader with its validity check, the ternary crazy
  operation, rotate, and the post-execution encryption table, all verified
  against a locally compiled `malbolge.c`. Where Olmstead's spec text and
  his interpreter disagree (output and input opcodes are swapped in the
  text, non-printable words spin rather than halt), the interpreter wins,
  as the community holds. Cooke's 2000 hello world and Scheffer's cat run.
* Differential testing now covers brainfuck (Cristofani's sbi), befunge93
  (Pressey's bef) and malbolge (Olmstead's own): 13 cases, all passing.
* 296 golden tests.

## 2026-08-29 (night)

* The front-end language WTF is renamed **Turpentine** (`.turp`), after the
  solvent for a Turing tarpit; the pun is explained in
  `docs/turpentine/spec.md`. Everything moved: `Langlib/Languages/Turpentine/`,
  module `Langlib.Turpentine.*`, examples `Langlib/Examples/Turpentine/`,
  runner `lake exe turpentine`, docs `docs/turpentine/`.
* Thue and Befunge-93 landed (27 and 46 tests). 277 tests, all passing.
* Differential testing works for real: `scripts/get-references.sh` fetches
  and builds reference interpreters into a gitignored `.difftools/`
  (Pressey's bef so far), and `scripts/difftest.sh` prefers them over
  PATH. Befunge-93 now passes 4 differential cases against bef v2.25.
* `docs/verification.md` written: the shared correctness statement,
  per-backend proof structure, proof order, and a scoreboard.
* Stage 4 in flight: compiler agents for Turpentine to brainfuck,
  whitespace, and subleq.

## 2026-08-29 (evening)

* Layout: language implementations moved under `Langlib/Languages/`
  (module names gain the `Languages` segment; Lean namespaces stay
  `Langlib.<Langname>`). Turpentine stays at `Langlib/Languages/Turpentine/` as the front end.
* Runners: no longer block reading a terminal stdin (empty input instead);
  new `--verbose` flag reports how a run ended.
* Stage 3 (Turpentine) core implemented: deep-embedded AST with loop annotations,
  lexer + recursive-descent parser, type checker, pure fuel-based
  interpreter (unbounded ints, Euclidean `/` `%`, short-circuit booleans,
  line/byte I/O), runner with `run`/`check` subcommands, 8 examples (isqrt
  and sumdigits ported from Velvet), 32 golden tests, `docs/turpentine/spec.md`.
* Stage 2 fan-out: parallel agents implementing the remaining languages.
  Landed so far: fractran (24 tests; PRIMEGAME prints primes via
  `--out pow2`) and subleq (27 tests; Mazonka's `-1` I/O convention, label
  assembler). Total test count: 104, all passing. Still in flight:
  whitespace, malbolge, ook+deadfish, thue, befunge93, piet+brainloller.
* Docs: README lists implemented languages and shows how to run programs;
  `docs/README.md` is now a status matrix (parser / interpreter / Turpentine
  compiler / verified compiler per language); `docs/TESTING.md` documents
  the golden-vs-differential policy per language; examples that read input
  carry usage lines in comments.

## 2026-08-29 (later)

* Layout revision per project owner: everything lives under `Langlib/`
  (no separate `Esolang` folder); example/test subfolders are capitalised;
  the front end is spelled Turpentine. `docs/ALTERNATIVES.md` renamed to
  `docs/RELATED.md`; the dead wolflo/esolang-semantics link replaced by the
  live parent repo (ellisonch/esolang-semantics).
* Plan additions: Piet and Brainloller confirmed as a graphical second
  wave; "Java Generics are Turing Complete" (arXiv:1605.05274) added to the
  roadmap; Brainfuck/Whitespace/Malbolge confirmed as must-haves.
* Stage 2 started: shared infrastructure (`Langlib/Common/`: pure
  fuel-based execution model, input stream, runner scaffolding, golden-test
  harness) and the brainfuck exemplar (AST, parser with positioned bracket
  errors, zipper-tape semantics with three EOF conventions, runner
  `lake exe brainfuck`, 9 examples, 21 golden tests, spec page
  `docs/brainfuck/spec.md`, differential-test script skeleton).

## 2026-08-29

* Stage 0: repository scaffolded. Lake project on Lean 4.33.1, single
  library `Langlib` (esolangs, `Common`, `Turpentine`, `Tests`, `Examples` all
  under the `Langlib/` folder), test driver stub. README, CLAUDE.md (project
  policies), CONTRIBUTING, Apache 2.0 LICENSE, .gitignore, docs skeleton
  (PLAN, PROGRESS, ROADMAP, RELATED). Initial language set chosen
  (see PLAN Stage 1).