How the Turmac-to-Kondey backend works
======================================

<!--
SPDX-FileCopyrightText: This work was generated by Claude Opus 4.8 in 2026.

SPDX-License-Identifier: LicenseRef-No-Human-Authorship
-->

_This document was generated by Claude Opus 4.8, and it shows._

This is a walkthrough of `src/Language/Turmac/Backend/Kondey.hs`, the module
that turns a Turing machine into a Kondey program. It is a companion to
`doc/Turing-completeness-of-Burro.md`, but the two have different jobs:

  * that document **proves** the translation is correct (it is a dense
    bisimulation proof);
  * this document just **explains how the code works**, one piece at a time,
    so you can read the module without holding the whole proof in your head.

I assume you're comfortable with brainfuck, with Burro (especially its
`(a/b)` conditional and its group/`inverse` property), with Turing machines,
and with what Turing-completeness means. I do *not* assume you can juggle
six moving parts at once — so every section ends where it began, and the
diagrams are the part you should actually read.

There is only one hard rule in this whole design, and almost every decision
in the module is a consequence of it. I'll state the representation first,
then that rule, then watch the rest fall out.


The pipeline, in one picture
----------------------------

The compiler is one stage in a small pipeline:

    Turmac text  ──normalize──▶  IR tree  ──▶  Kondey text  ──▶  Burro
    (a TM, as a                            ▲
     rule table)                           │
                                    THIS MODULE
                                (Kondey.hs: IR ──▶ Kondey)

We only care about the one boxed stage. Everything to its left (parsing the
`.turmac` rule table, renumbering states/symbols so they're `0,1,2,…`) is
already done; the module receives a clean **IR tree** shaped exactly like the
machine:

    Program
      └─ CondState                  -- "dispatch on the current state"
           0 → CondSymbol           -- "in state 0, dispatch on the symbol"
                0 → WriteMoveGoto …  -- write a symbol, move, go to a state
                1 → WriteMoveGoto …
           1 → CondSymbol
                0 → WriteMoveGoto …
                …

The module's whole task is to emit Kondey text that, **when run once, performs
one step of that machine.** It does *not* write the loop. Burro supplies the
loop for free: its `run` construct re-executes the program body, over and
over, until a halt flag says stop.

    ┌──────────────────────────────────────────┐
    │  Burro's run loop                         │
    │                                           │
    │    ┌─────────────────────────────┐        │
    │    │  the compiled program body  │  ◀──┐  │
    │    │  = exactly one TM step      │     │  │
    │    └─────────────────────────────┘     │  │
    │            │                            │  │
    │       halt flag set?  ── no ────────────┘  │
    │            │ yes                           │
    │            ▼                               │
    │           stop                             │
    └──────────────────────────────────────────┘

So: **read this module as "how do I do one TM step in Burro?"** The looping,
the halting, the not-halting — those are Burro's problem, and the module only
has to nudge the halt flag correctly.


The representation: one TM cell = one "CellStruct"
--------------------------------------------------

Here is the central idea. Each cell of the TM's tape is represented by a
fixed-size run of consecutive Burro cells, called a **CellStruct**:

    ┌───────┬──────────────────┬──────┬──────────────────┬───────┐
    │ state │ tmps_1 .. tmps_n │ cell │ tmpc_1 .. tmpc_m │ carry │
    └───────┴──────────────────┴──────┴──────────────────┴───────┘
        0      1 ..          n    n+1    n+2 ..       n+m+1  n+m+2

where `n` = number of TM states and `m` = number of TM symbols. The whole
struct is `K = n + m + 3` Burro cells wide. Only two of those fields hold
"real" data:

  * **`state`** — the TM state (only meaningful in the CellStruct the head
    is currently inside);
  * **`cell`**  — the TM symbol written on this tape square.

The rest are workspace:

  * **`tmps_*`** — scratch cells the state-dispatch cascade walks through;
  * **`tmpc_*`** — scratch cells the symbol-dispatch cascade walks through;
  * **`carry`**  — a one-cell relay used to carry the move direction out of
    the dispatch (more on this later).

Now the insight that makes the whole scheme cheap:

> **There is no "head position" stored anywhere. The TM's head is simply
> whichever CellStruct the Burro tape head is currently sitting inside.**

Picture the Burro tape as a row of CellStructs, with the Burro head parked in
one of them:

    … ┌───────────┐ ┌───────────┐ ┌───────────┐ ┌───────────┐ …
      │ CellStruct│ │ CellStruct│ │ CellStruct│ │ CellStruct│
      │  (cell-1) │ │  (cell 0) │ │  (cell+1) │ │  (cell+2) │
      └───────────┘ └───────────┘ └───────────┘ └───────────┘
                         ▲
                    Burro head here
                = TM head is on tape cell 0

Moving the TM head one square left or right just means moving the Burro head
one *whole CellStruct* (`K` cells) left or right.

And there's a lovely bonus: **a blank Burro tape (all zeros) is already a
valid starting configuration.** Every CellStruct reads `state = 0`,
`cell = 0`, all scratch `= 0` — i.e. "the TM is in state 0, this square is
blank." That's exactly the TM's initial configuration, so the compiler emits
no initialization code at all.


Numbers are stored doubled (the even/odd trick)
-----------------------------------------------

One small convention, needed before we go further. State and symbol values
are stored **doubled**: TM state `q` is stored as `2q`, symbol `s` as `2s`.
So at rest, `state` and `cell` always hold **even** numbers (`0, 2, 4, …`).

Why? Because to *dispatch* on a value we run it through Burro's `Test`, and
`Test` can only tell "positive vs. non-positive" — it needs a nonzero value,
and the cascade that follows counts down by 2s. So right before dispatching,
the code bumps the value up by one with a single `+`, turning `2q` into the
**odd** number `2q+1`. After dispatch it's restored to even.

    at rest:   state = 2q   (even)
      bump +:  state = 2q+1 (odd)  ── now dispatchable
     dispatch runs, then it's put back to even

Keep this in the back of your mind: *even = data lying at rest, odd = a value
mid-flight through a conditional.*


The one hard rule
-----------------

Everything above is representation. Here is the single constraint that
dictates the *shape* of the emitted code:

> **Inside a `{a/b/c/…}` dispatch, no branch may move the tape head (on
> net).** Every branch must return the head to where it started.

Why? Recall how Kondey's extensible conditional is built (see
`Language.Kondey.Compiler`): it's a **cascade** of Burro `Test`s that walks
*rightward*, one scratch cell at a time. Each `Test` leaves a "work value" in
the next cell for the following `Test` to read:

    {branch0 / branch1 / branch2}   compiles to, roughly:

      Test──▶ work ──▶ Test──▶ work ──▶ Test──▶ …
      (reads   in       (reads   in      (reads
       cell C) cell C+1  cell C+1) C+2    cell C+2)

The cascade only stays in sync if, after each branch's payload runs, the head
is back on the cell the *next* `Test` expects. If some branch displaced the
head — even by one cell — every following `Test` would read the wrong cell,
and later branches would fire (or not) at random.

So: **a dispatch branch may compute and write all it likes, but it must leave
the head exactly where it found it.** Hold onto this. The next three sections
are all just "…and here's how we obey that rule."


What one TM step has to do
--------------------------

A single TM transition — "in state `q` reading symbol `s`, write `s′`, move
direction `d`, go to state `q′`" — breaks into five jobs:

    1. read the current state  (q)      ┐ figure out *which*
    2. read the current symbol (s)      ┘ transition applies
    3. write the new symbol s′ into this cell
    4. write the new state q′ into the *destination* cell
    5. move the head one square in direction d
    (plus: keep Burro's loop going, unless we're halting)

Now line these up against the one hard rule. Jobs 1–4, and the halt-flag
nudge, are all things we can do **without a net head move**: read a value,
write a delta here, reach over to a neighbor and reach back. But job 5, the
move, is *inherently* a net head displacement — it is the one thing the rule
forbids inside a dispatch.

That tension is the entire architecture. The module splits the step into two
phases:

    ┌─ PHASE 1 ──────────────────────────────────┐   ┌─ PHASE 2 ─────────┐
    │ Identify (state, symbol) via nested         │   │ Do the one move,  │
    │ dispatch, and do jobs 3, 4, and the halt    │   │ as a single 2-way │
    │ nudge — all net-zero head movement.         │   │ Test. (job 5)     │
    │ Also: stash the move direction in `carry`.  │──▶│                   │
    └─────────────────────────────────────────────┘   └───────────────────┘

Phase 1 lives entirely inside the dispatch and obeys the rule. Phase 2 is the
*last thing the body does* — nothing is chained after it — so it's finally
safe to move the head. Let's take them in turn.


Phase 1: find the leaf, do the writing
--------------------------------------

Phase 1 is a **nested dispatch**: an outer `{…}` on the state, and inside each
state's branch, an inner `{…}` on the symbol. Reaching the inner-inner leaf
means we've identified the exact `(state, symbol)` pair — i.e. exactly which
transition applies.

Three functions build it. Read them as an outline:

  * `compileToKondey` — the outermost frame: bump the state, emit the outer
    state-dispatch, then hand off to phase 2.
  * `compilePhase1State` — one branch of the state-dispatch: walk over to
    `cell`, bump it, emit the inner symbol-dispatch, walk back.
  * `compilePhase1Symbol` — one leaf: the actual transition work.

### Head movement in phase 1

The thing to watch is the head, so here's its whole journey through phase 1,
drawn inside one CellStruct (using `n=2` states, `m=2` symbols, so
`K = 7`):

    ┌───────┬────────┬────────┬──────┬────────┬────────┬───────┐
    │ state │ tmps_1 │ tmps_2 │ cell │ tmpc_1 │ tmpc_2 │ carry │
    └───────┴────────┴────────┴──────┴────────┴────────┴───────┘

    start:   head on `state`
       │
       │  compileToKondey:  `+`  bump state to odd
       │  emit outer {…} dispatch on state  ───────────────┐
       │                                                   │
       ▼   (inside the matching state branch —             │
           compilePhase1State:)                            │
           `>>>`   move to `cell`  (n+1 = 3 cells right)    │
           `+`     bump cell to odd                         │
           emit inner {…} dispatch on symbol  ──────┐      │
                                                    ▼      │
                (inside the matching symbol branch —       │
                 compilePhase1Symbol: the leaf. see below) │
                                                    │      │
           `<<`    recenter over inner branches      ◀──────┘
           `<<<`   move back to `state`                     │
       ◀───────────────────────────────────────────────────┘
       │  `<<`     recenter over outer branches
       ▼
     head back on `state` — net zero. ✔

Every step out is matched by a step back. The two "recenter" moves (`<<` each)
undo the rightward drift the cascades leave behind (recall: each cascade walks
one cell right per branch). The upshot: **phase 1 as a whole returns the head
to `state`,** obeying the rule.

### What the leaf actually does (`compilePhase1Symbol`)

Now zoom into the leaf, where we know the transition is "write `s′`, move `d`,
go to `q′`." The head is parked on `cell`. Four actions happen, each carefully
net-zero:

  1. **Write the new symbol.** Emit `s′` (doubled) as a plain `+`/`-` delta
     into `cell`. This is safe because Burro's `Test` has just freshly reset
     `cell` to 0 before the leaf runs, so a delta writes an absolute value.

  2. **Write the new state at the destination** (`writeNewStateAtDest`). Reach
     out to the *neighbor* CellStruct we're about to move into — one whole
     CellStruct left or right, per direction `d` — write `q′` (doubled) as a
     delta into its `state`, and reach back. Safe because an unvisited
     CellStruct always has `state = 0`. *Skipped entirely if the transition
     halts* — there's no next state to store, and Burro stops before that
     neighbor would ever be read.

         this CellStruct        destination CellStruct
         ┌──────┬─────┐         ┌───────┬─────┐
       … │ cell │ …   │  ────▶  │ state │ …   │ …   write q′ here, reach back
         └──────┴─────┘         └───────┴─────┘

  3. **Stash the move direction in `carry`.** Reach over to this CellStruct's
     `carry` and write `+1` (move right) or `-1` (move left). Phase 2 will
     read it. (There's a subtlety here — the `++(</)` "launder" gadget you'll
     see in the code — which we defer to its own section below; ignore it for
     now.)

  4. **Nudge the halt flag.** Emit `!` to keep Burro's loop going — *unless*
     this transition enters the halt state `H`, in which case emit nothing, so
     the flag stays set and Burro stops after this body execution.

All four reach-and-return, so the leaf is net-zero, so the inner dispatch is
net-zero. Good.

### Why the writes don't get scrambled by all the *other* branches

Here's the part that feels like magic but is just Burro's group property. In a
cascade, it's not only the matching branch that runs — *every branch up to the
matching one runs its payload*, and each one first **undoes its predecessor**
using Burro's exact `inverse`. So all the spurious writes to `cell`, to
destinations, to `carry`, and all the spurious `!` toggles from non-matching
branches, cancel out in inverse/redo pairs. What survives is **exactly the one
leaf that logically fired.** You get to write each branch as if it were the
only one; the cascade's undo machinery collapses them to the real one.


Phase 2: the one real move
--------------------------

After phase 1, the head is back on `state`, and `carry` holds `+1` or `-1`.
`compileToKondey` now walks right to `carry` and emits the move
(`phase2Move`):

    (  >>…>  /  <<…<  )
       ^^^^     ^^^^
       then      else
    carry > 0   carry < 0
    move RIGHT  move LEFT
    one struct  one struct

This is a plain 2-way Burro `Test` on `carry`. Two things make it legal to
move the head here, where it was forbidden before:

  * It's a **2-way** `Test`, not a cascade. A 2-way `Test` never re-reads its
    pivot, so there's no following comparison to knock out of sync.
  * It's the **very last thing** in the body. Nothing is chained after it, so
    its head displacement can't corrupt anything downstream.

So this is the single sanctioned head move — exactly job 5 — and it moves the
head one whole CellStruct in the transition's direction.

### The overshoot-by-one trick

One detail. Burro's `Test` has a quirk: after the chosen branch runs, it swaps
a value back onto the tape *at wherever the head ended up*. If a branch of
`phase2Move` landed precisely on the destination's `state` cell, that swap
would clobber the `q′` we so carefully wrote there in phase 1.

The fix: each branch deliberately **overshoots the target `state` cell by one**,
landing on a harmless scratch cell of the destination. The `Test`'s swap-back
then splats onto *that* scratch cell instead of onto `state`. Then
`compileToKondey` emits one uniform `<` to step back onto `state`:

    phase2Move lands here (one past state) ─┐
                                            ▼
              destination CellStruct:  ┌───────┬────────┬─ …
                                       │ state │ tmps_1 │
                                       └───────┴────────┘
                                          ▲       swap-back clobbers this
                        final `<` steps   │       (a scratch cell — harmless)
                        back onto state ──┘

As a bonus, because this displacing `Test`'s swap-back lands at the
destination rather than back on `carry`, it leaves `carry` reset to 0, ready
for next time. (Mostly. See the next section for the "mostly.")


The `carry` wrinkle: why `++(</)` is in the code
------------------------------------------------

*You can skip this on a first read.* It's a correctness patch for a subtle bug,
not part of the main idea — but it's staring at you in the emitted code, so
here's what it's for.

The problem: `carry` is **not reliably 0** when phase 1 goes to write the
direction into it. On the third-and-later visit to the same CellStruct, the
displacing `Test` of phase 2 (via that swap-back quirk again) has deposited
stale junk into `carry` — specifically an old, always-positive value left over
from a previous visit. If phase 1 then just wrote the direction as a delta
onto that junk, `-1` could come out `≥ 0`, turning every intended *left* move
into a *right* move (or no move). This actually happened; it was caught by
`bisim-check-turmac` on `eg/bouncing-infinite.turmac` at step 8. Two earlier
test machines never visited any cell three times, so it stayed hidden.

The fix is the gadget `++(</)`, emitted in the leaf just before the direction
is written. It uses the *same* swap-back quirk deliberately, to **launder
`carry` back to exactly 0**:

  * `++` makes `carry` reliably positive (the junk is provably `≥ -1`, so
    `+2` makes it `≥ 1`);
  * `(</)` is a displacing 2-way `Test` whose `then` branch steps one cell
    left. Because the head displaces, the `Test`'s swap-back deposits the
    *stack* value — which is provably 0 at this depth — into `carry`.

Net effect: `carry := 0`, the garbage is dumped into a scratch cell that
provably never matters, and the following delta writes a clean `±1`. (The full
argument for why the stack cell is 0 here, and why the discarded garbage is
inert, is in `Turing-completeness-of-Burro.md` — that's the proof's job.)


End to end: `write-one` compiled
--------------------------------

To make it concrete, here's the smallest real machine.
`eg/write-one.turmac` is a single rule:

    state,read,write,dir,newstate
    S0,_,1,R,H          -- in state 0 reading blank: write 1, move right, halt

It has `n = 1` state and `m = 2` symbols (`_` and `1`), so `K = 6`:

    ┌───────┬────────┬──────┬────────┬────────┬───────┐
    │ state │ tmps_1 │ cell │ tmpc_1 │ tmpc_2 │ carry │
    └───────┴────────┴──────┴────────┴────────┴───────┘
       0        1       2       3        4        5

Running `burro compile-turmac eg/write-one.turmac` gives (annotated):

    +                    phase 1: bump `state` odd, then dispatch on state…
    {>>                    outer {…}, branch for state 0:
                             `>>` move to `cell` (offset 2)
    +                        bump `cell` odd, then dispatch on symbol…
    {++                        inner {…}, branch for symbol 0 (blank):
                                 `++` write new symbol 1 (doubled = 2) into cell
                                 (new state is H, so writeNewStateAtDest emits nothing)
    >>>                          move to `carry` (3 cells right of cell)
    ++(</)                       launder `carry` to 0
    >                            step back to `carry`
    +                            write direction +1 (move right) into carry
    <<<                          move back to `cell`
                                 (halting, so no `!` — Burro will stop)
    }                          end inner dispatch
    <                          recenter over inner branch
    <<                       `<<` move back to `state`
    }                      end outer dispatch
    <                      recenter over outer branch
    >>>>>                phase 2: walk to `carry` (offset 5)
    (>>/<<<<<<<<<<)         the move: carry>0 → right; here overshoot by `>>`
    <                      step back onto the destination's `state`

Run this once and Burro is left with `cell = 2` (symbol `1`) in the original
CellStruct and the head sitting one CellStruct to the right — and because we
never emitted `!`, the halt flag stays set and `run` stops. One step, one
halt, done. Exactly the machine.


Cheat sheet
-----------

Keep this next to the code:

**The CellStruct** (`K = n + m + 3` Burro cells; `n` states, `m` symbols):

    ┌───────┬──────────────────┬──────┬──────────────────┬───────┐
    │ state │ tmps_1 .. tmps_n │ cell │ tmpc_1 .. tmpc_m │ carry │
    └───────┴──────────────────┴──────┴──────────────────┴───────┘

  * `state`, `cell` — real data, stored **doubled** (even at rest, bumped odd
    to dispatch).
  * `tmps_*`, `tmpc_*` — scratch for the state / symbol dispatch cascades.
  * `carry` — relay holding the move direction (`+1`/`-1`) between phases.
  * TM head position = **which CellStruct the Burro head is in**. Blank tape =
    valid start state, no init needed.

**Offsets** (`cellOffset`, `carryOffset`, `cellStructSize` in the module):

    state = 0    cell = n+1    carry = n+m+2    width K = n+m+3

**The one rule:** inside a `{…}` dispatch, no branch may move the head on net.

**The two phases** (per TM step = per body execution):

    Phase 1  compileToKondey / compilePhase1State / compilePhase1Symbol
             nested {state}{symbol} dispatch, all net-zero:
               • write new symbol into `cell`
               • write new state into the destination CellStruct
               • launder + set `carry` to the move direction
               • toggle `!` (unless halting)
    Phase 2  phase2Move
             one 2-way Test on `carry`: move the head one CellStruct,
             overshoot by one, then a uniform `<` back onto `state`.

**Whom to blame for what:** this document explains the *mechanism*;
`Turing-completeness-of-Burro.md` proves it's *correct*; `bisim-check-turmac`
*checks* it step-by-step on real machines.