PROGRESS.md

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 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 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 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 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. 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 composes the existing URM forward theorem through the tape invariant to the represented answer and normal halting. 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 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 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: 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, 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 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 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; 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 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. 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 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 lets, 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 cs 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.

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.

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 Ks 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.

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:

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:

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 rolls 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).