Single-tape simulation — correctness internals #
The config-level correspondence Corr between a singleTapeSim N configuration
and an N configuration at a macro-step boundary, and the macro-step
correspondence corr_macroStep (one N-step ↦ several simulator steps,
preserving Corr). The behavioural lemmas (SingleTape.lean) follow by
iterating corr_macroStep over N's computation and translating acceptance.
See docs/A4-SingleTapeSimulation.md. Proof internals only.
Config correspondence. At a macro-step boundary, the singleTapeSim N
configuration c1 corresponds to the N configuration c: same simulated
state, work head parked at cell 0/1, identical input and output tapes, and
the single work tape encodes N's k work tapes (materialized up to M).
c1is at therunphase forN's current state.The single work head is parked at cell 0 (initial) or cell 1 (post-commit).
Input tapes coincide (input is read-only, carried over verbatim).
Output tapes coincide (the simulator writes output exactly as
Ndoes).The single work tape encodes
N'skwork tapes.Each
Nwork tape is blank beyond the materialized region (heads never reached there). Needed to materialize the fresh block at SCATTER.The input tape has
▷only at cell0(input is read-only; cells hold{0,1,□}). Lets the phases keep the input head off▷(the▷-dodge).The output tape has
▷only at cell0(writes useΓw, never▷).
Instances For
Base case. The initial singleTapeSim N configuration corresponds to
N's initial configuration, materialized to M = 0 (empty used region).
Writing back the read symbol preserves whether a cell holds the accept bit
1 (readBackWrite fixes 0/1/□ and maps ▷ ↦ □, never producing a
spurious 1).
The halt step's output action — writeAndMove writing back the read
symbol — preserves the accept bit at cell 1.
Halt correspondence. When N has halted, the simulator (parked at
run N.qhalt) takes one step to SimQ.halt, preserving the accept bit.
Per-macro-step sim-step budget at materialization level M: a generous bound
covering the four sweeps over an ≈ 3k·M-cell region plus the run/commit
steps. The 16·(k+1) constant matches singleTapeSimTime.
Instances For
macroBound k is monotone in the materialization level M.
Per-phase config transitions (building blocks for corr_macroStep) #
Each lemma reduces trace-of-a-phase to the explicit next configuration; the
full macro-step composes them via trace_add_fun.
The run step (1 sim step): from a run q config with q ≠ N.qhalt, the
simulator initialises GATHER (acc = ▷, reads iSym/oSym, sweep at the
start) and repositions the work head to cell 1. Input/output are advanced by
idleDir (the ▷-dodge); the work tape's cells are preserved
(readBackWrite).
The commit step (1 sim step): from a commit (q', oW, oD, iD, iSym, oSym)
config, the simulator applies the deferred output write/move and input move
(accounting for the ▷-dodge via the iSym/oSym guards) and returns to
run q'. The work tape is preserved.
One gather step (trace 1): from a gather d config, the result is the
configuration built from gatherStep's output (the trace step applied to the
gather branch of simDelta). The basis of the gather-sweep induction.
One gather triple (trace 3): starting at slot 0 of tape j's triple
in the encoded region (work head at h), three GATHER steps read the head-bit
(cells h), sym-hi (cells (h+1)), and sym-lo (cells (h+2)) cells, advance
the sweep to the next tape's slot 0, leave the work tape contents unchanged
(read-only sweep, head at h+3), and — if the head-bit is set — record this
tape's decoded symbol into acc. Input/output stay put (off ▷, so idleDir
is stay). The block/sweep inductions iterate this over the k tapes and M
blocks. Code-cell hypotheses (≠ □, ≠ ▷) keep all three steps in the slot
branch (no sentinel) and make readBackWrite cell-preserving.
One GATHER sentinel step (trace 1): reading the □ that ends the used
region fires N.δ (the one meaningful use of the choice bb) and hands the
write/move actions to REWIND, turning the work head leftward.
One non-sentinel GATHER step. Reading a non-□, non-▷ work cell, one
GATHER step stays in GATHER (some evolved data d'), advances the work head
by one with contents intact, and leaves input/output put (idle off ▷). The
inductive step of the per-step sweep characterization.
No sentinel during the GATHER sweep. Starting from the post-run GATHER
config (work head at cell 1, contents materialized at level M), every one
of the first 3*k*M sweep steps keeps the simulator in a GATHER state reading
a non-□ cell — the □ sentinel is reached only at step 3*k*M. This is the
crux of the backward correspondence: within a macro-step, a GATHER-on-□
configuration (the one choice-consuming step) occurs at exactly one position.
The sweep accumulator at B = M is exactly the per-tape reads: a head in
[1, M] had its symbol recorded; a head at 0 reads ▷, which is also the
▷ default the sweep leaves. Uses heads_le (every head ≤ M) and
read_eq_start_of_head_eq_zero (a head at 0 reads ▷).
One rewind step (trace 1): from a rewind d config, the result is the
configuration built from rewindStep's output. Basis of the rewind sweep.
REWIND full sweep (trace (p+1)). From a rewind config with the work
head at cell p (every cell in [1,p] a non-▷ code cell, cell 0 the ▷),
the leftward sweep carries the δ results untouched back to cell 0, then
turns around into SCATTER sweep-1 at cell 1 (empty stay/left carries). Proved
by induction on p (one rewindStep per cell), contents preserved throughout.
REWIND stays in REWIND (per step). Throughout the leftward sweep (head at
p - i ≥ 0, every cell in [1,p] non-▷), each intermediate config keeps the
rewind state (data unchanged — only the head moves). Since rewind ≠ gather,
this supplies the back-phase ¬gather needed by the backward correspondence.
Intermediate work tape after SCATTER sweep-1 (before sweep-2 relocates the
left-movers). For tape t with old tape ct and N.δ action (w, d): the
new symbol w is written at the old head position; the head-bit is placed at
the new position for stay/right movers, but is left at the old position
for left-movers — SCATTER sweep-2 moves those one block left. A head reading
▷ (position 0) is forced right by δ_right_of_start, so it lands at
position 1 (the ▷ symbol write is a no-op at cell 0). Thus head here is
ct.head + 1 for right-movers and ct.head for stay/left-movers.
Equations
Instances For
scatterInterWork only rewrites the old head cell: every other cell is
unchanged. (The new symbol is written at the old head position.)
scatterInterWork preserves cell 0 (the ▷ marker): writing at the head
never touches cell 0 (it's either a no-op there, or the head is ≥ 1).
scatterInterWork keeps every cell ≥ 1 non-▷: untouched cells inherit it
from ct, and the rewritten head cell holds a writable symbol (Γw, which
excludes ▷). The noStart precondition for the post-sweep SimInvAt (M+1).
scatterInterWork's head stays within the materialized region after growth:
a right-mover advances by one (to ≤ M+1), others stay. The heads_le
precondition for the post-sweep SimInvAt (M+1).
scatterInterWork's head value: a right-mover advances by one, every other
move keeps the old head position. (The head half of the intermediate
encoding's head-bit.)
scatterInterWork writes the new symbol at the old head position (when the
head is ≥ 1, where write is not a no-op). The sym half of the
intermediate encoding at the head's block.
The post-SCATTER-sweep-2 work tape: scatterInterWork with a left-mover's head
decremented one cell. This is the actual N.trace 1 image of ct under action wd
— sweep-1 placed stay/right heads, sweep-2 finishes the left-movers. The cells are
identical to scatterInterWork (only the head position changes).
Equations
- One or more equations did not get rendered due to their size.
Instances For
scatterFinalWork has the same cells as scatterInterWork (only the head moves).
scatterFinalWork's head: a left-mover retreats one cell, everything else is as in
scatterInterWork.
scatterFinalWork's head stays within the grown region [0, M+1].
scatterFinalWork preserves cell 0 (the ▷ marker).
Mid-sweep invariant for SCATTER sweep-2, at block boundary b: the work tape
holds the final head-bit encoding (scatterFinalWork — left-movers retreated) on
blocks [b, M+1] already swept (leftward), and the intermediate encoding
(scatterInterWork) on blocks [1, b) not yet reached. Symbol cells are the same in
both (sweep-2 only moves head-bits). The in-flight leftCarry lives in the state. At
b = M+2 it's the sweep-1 output (SimInvAt (M+1) for scatterInterWork); at b = 1
the whole region is scatterFinalWork-encoded.
Cell 0 is the global start marker
▷.- donePart (q : ℕ) : b ≤ q → q ≤ M + 1 → ∀ (j : Fin k), (t.cells (headBitCell k q j) = if (scatterFinalWork (w j) (wact j)).head = q then Γ.one else Γ.zero) ∧ t.cells (symCell k q j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).1 ∧ t.cells (symCell k q j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).2
Blocks
[b, M+1]already swept: final (scatterFinalWork) head-bits. - oldPart (q : ℕ) : 1 ≤ q → q < b → ∀ (j : Fin k), (t.cells (headBitCell k q j) = if (scatterInterWork (w j) (wact j)).head = q then Γ.one else Γ.zero) ∧ t.cells (symCell k q j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).1 ∧ t.cells (symCell k q j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).2
Blocks
[1, b)not yet reached: intermediate (scatterInterWork) head-bits. The sentinel region (block
M+2onward) is blank.
Instances For
▷ uniquely marks cell 0 during SCATTER sweep-2. Every cell ≥ 1 is a head-bit
({0,1}), a code cell (encSymΓ, ≠ ▷), or a sentinel blank — so none is ▷. The
same shape as SimInvAt.materialized_ne_start, dispatched on donePart/oldPart/
sentinel. The per-step read ≠ ▷ precondition for the scatter2 sweep lemmas.
Entering SCATTER sweep-2: the sweep-1 output SimInvAt (M+1) for scatterInterWork
is Scatter2MidInv at b = M+2 (no blocks swept yet — donePart vacuous).
Leaving SCATTER sweep-2 (all blocks swept, b = 1): Scatter2MidInv is SimInvAt (M+1) for the final config scatterFinalWork. The structural fields use the
original work tapes' wfStart/noStart/heads_le.
Within-block partial invariant for the SCATTER sweep-2 block step: like
Scatter2MidInv at boundary p+1, but block p itself is split — its top m
tapes [k-m, k-1] (swept first, leftward) hold the final (scatterFinalWork)
head-bits, the rest still intermediate. … p 0 ⇔ Scatter2MidInv … (p+1); … p k
⇔ Scatter2MidInv … p (see ofMid/toMidPred).
Cell 0 is the global start marker
▷.- donePart (q : ℕ) : p < q → q ≤ M + 1 → ∀ (j : Fin k), (t.cells (headBitCell k q j) = if (scatterFinalWork (w j) (wact j)).head = q then Γ.one else Γ.zero) ∧ t.cells (symCell k q j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).1 ∧ t.cells (symCell k q j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).2
Blocks
(p, M+1]: final (scatterFinalWork) head-bits. - doneTape (j : Fin k) : k - m ≤ ↑j → (t.cells (headBitCell k p j) = if (scatterFinalWork (w j) (wact j)).head = p then Γ.one else Γ.zero) ∧ t.cells (symCell k p j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).2
Block
p, tapes[k-m, k-1]: already final-encoded. - oldTape (j : Fin k) : ↑j < k - m → (t.cells (headBitCell k p j) = if (scatterInterWork (w j) (wact j)).head = p then Γ.one else Γ.zero) ∧ t.cells (symCell k p j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).2
Block
p, tapes[0, k-m): still intermediate. - oldPart (q : ℕ) : 1 ≤ q → q < p → ∀ (j : Fin k), (t.cells (headBitCell k q j) = if (scatterInterWork (w j) (wact j)).head = q then Γ.one else Γ.zero) ∧ t.cells (symCell k q j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).1 ∧ t.cells (symCell k q j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells q)).2
Blocks
[1, p): still intermediate. The sentinel region (block
M+2onward) is blank.
Instances For
▷ uniquely marks cell 0 during a SCATTER sweep-2 block step. Every cell ≥ 1 is a
head-bit ({0,1}), a code cell (encSymΓ, ≠ ▷), or a sentinel blank. Same shape as
Scatter2MidInv.cells_ne_start, dispatching block p on doneTape/oldTape and the
rest on donePart/oldPart/sentinel.
Entering block p (no tapes swept): Scatter2MidInv … (p+1) is Scatter2BlockInv … p 0 (block p still all intermediate).
Leaving block p (all k tapes swept): Scatter2BlockInv … p k is Scatter2MidInv … p (block p now all final).
Block-step cell bookkeeping (pure) for SCATTER sweep-2: advancing the within-block
invariant one tape. Sweep-2 only rewrites a head-bit cell, so if a new tape t' agrees
with t everywhere except block p tape k-1-m's head-bit (now the final value), and
t satisfies Scatter2BlockInv … p m, then t' satisfies Scatter2BlockInv … p (m+1).
The changed cell headBitCell p (k-1-m) is disjoint from every other queried cell
(same-block sym cells differ mod 3; other tapes by index; other blocks by layout).
The SCATTER head triples write the symbol via the writable codec
(encSymW s), but the scatterInterWork target reads it via the
full-alphabet codec applied to the written cell (encSymΓ s.toΓ). They
agree (both route through encSym): this matches a head triple's two symbol
writes to the intermediate encoding at the head's block.
Mid-sweep invariant for SCATTER sweep-1, at block boundary b: the work
tape t holds the intermediate encoding (scatterInterWork) on blocks
[1, b) already swept, and the old encoding (w) on blocks [b, M] not
yet reached, with the ▷ at cell 0 and the sentinel region blank beyond block
M. (The in-flight rightCarry lives in the SCATTER state, not the tape.) The
block step advances this b → b+1; at b = 1 it's the REWIND output (all old),
at b = M+1 the whole region is intermediate-encoded.
Cell 0 is the global start marker
▷.- donePart (p : ℕ) : 1 ≤ p → p < b → ∀ (j : Fin k), (t.cells (headBitCell k p j) = if (scatterInterWork (w j) (wact j)).head = p then Γ.one else Γ.zero) ∧ t.cells (symCell k p j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).2
Blocks
[1, b)already swept: intermediate (scatterInterWork) encoding. - oldPart (p : ℕ) : b ≤ p → p ≤ M → ∀ (j : Fin k), (t.cells (headBitCell k p j) = if (w j).head = p then Γ.one else Γ.zero) ∧ t.cells (symCell k p j) = (encSymΓ ((w j).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((w j).cells p)).2
Blocks
[b, M]not yet reached: the old encoding (SimInvAt M). The sentinel region (block
M+1onward) is blank.
Instances For
Base case of the mid-sweep invariant: the REWIND output (whole region
still old-encoded, SimInvAt M) is Scatter1MidInv at b = 1 (no swept
blocks yet).
Final case of the mid-sweep invariant: once all M blocks are swept
(b = M+1), the whole materialized region is intermediate-encoded — exactly
the SimInvAt M-style facts for scatterInterWork (w j) (wact j) on [1, M].
Within-block partial invariant for the SCATTER sweep-1 block step: like
Scatter1MidInv at boundary b, but block b itself is split — its first
m tapes are already intermediate-encoded (scatterInterWork), the rest still
old. The tape-by-tape block step advances m → m+1; … b 0 is Scatter1MidInv … b and … b k is Scatter1MidInv … (b+1) (see ofMid/toMidSucc).
Cell 0 is the global start marker
▷.- donePart (p : ℕ) : 1 ≤ p → p < b → ∀ (j : Fin k), (t.cells (headBitCell k p j) = if (scatterInterWork (w j) (wact j)).head = p then Γ.one else Γ.zero) ∧ t.cells (symCell k p j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells p)).2
Blocks
[1, b): intermediate (scatterInterWork) encoding. - doneTape (j : Fin k) : ↑j < m → (t.cells (headBitCell k b j) = if (scatterInterWork (w j) (wact j)).head = b then Γ.one else Γ.zero) ∧ t.cells (symCell k b j) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells b)).1 ∧ t.cells (symCell k b j + 1) = (encSymΓ ((scatterInterWork (w j) (wact j)).cells b)).2
Block
b, tapes[0, m): already intermediate-encoded. - oldTape (j : Fin k) : m ≤ ↑j → (t.cells (headBitCell k b j) = if (w j).head = b then Γ.one else Γ.zero) ∧ t.cells (symCell k b j) = (encSymΓ ((w j).cells b)).1 ∧ t.cells (symCell k b j + 1) = (encSymΓ ((w j).cells b)).2
Block
b, tapes[m, k): still old. - oldPart (p : ℕ) : b < p → p ≤ M → ∀ (j : Fin k), (t.cells (headBitCell k p j) = if (w j).head = p then Γ.one else Γ.zero) ∧ t.cells (symCell k p j) = (encSymΓ ((w j).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((w j).cells p)).2
Blocks
(b, M]: still old. The sentinel region (block
M+1onward) is blank.
Instances For
Entering block b (no tapes processed yet): Scatter1MidInv … b is the block
invariant at m = 0. The block-b old facts come from oldPart at p = b.
Leaving block b (all k tapes processed): Scatter1BlockInv … b k is
Scatter1MidInv … (b+1). The new donePart at p = b is the just-finished
doneTape (every j : Fin k satisfies j < k).
Block-step cell bookkeeping (pure). Advancing the within-block invariant
one tape: if a new tape t' agrees with t everywhere except block b tape
m's three cells, which now hold the intermediate (scatterInterWork)
encoding, and t satisfies Scatter1BlockInv … b m, then t' satisfies
Scatter1BlockInv … b (m+1). All other queried cells are untouched (block b
tape m's triple sits at [blockStart b + 3m, +2], disjoint from every other
(p,j) triple, cell 0 and the sentinel region). The five SCATTER triples each
discharge the three value hypotheses; this lemma does the disjointness once.
One scatter sweep-1 step (trace 1): from a scatter1 d config, the
result is the configuration built from scatter1Step's output. Basis of the
SCATTER sweep-1 correctness (the phase that writes N's new configuration and
materializes a fresh block).
A SCATTER sweep-1 non-sentinel step (trace 1): on any cell other than the
□ sentinel, the work head writes scatter1Step's computed symbol and moves
right (input/output idle), landing in scatter1Step's next state. The case
logic (head-bit handling, symbol writes, marker carries) stays packaged inside
scatter1Step for the sweep induction to unfold per cell.
A SCATTER sweep-1 materialize step (trace 1): at the □ sentinel, before
the new block is complete (¬(mat ∧ pos = (0,0))), the head writes the fresh
cell's value (scatter1Step's symbol — a head-bit per rightCarry at slot 0,
□ otherwise) and moves right, growing the region by one cell. Same shape as
scatter1_step_right; the work direction is right because the turn-around
guard is false.
SCATTER sweep-1 materialize slot-0 step: at the □ sentinel, slot 0 of
a fresh block-tape, deposit the head-bit (one if rightCarry t, else zero),
clear that carry, set mat, and advance to slot 1. The right-movers carried out
of the last old block land here.
SCATTER sweep-1 materialize symbol step: at the □ sentinel, slot 1 or 2
of a fresh block-tape, write the blank-symbol code cell (Γw.zero) and advance.
rightCarry/isLeftMover untouched; the new block's symbols are all □.
SCATTER sweep-1 materialize triple (trace 3): materialize one fresh
block-tape (3 blank cells) — deposit the head-bit (one iff rightCarry t),
then two blank-symbol cells (□), clearing rightCarry t and setting mat. The
work head advances by 3 to the next tape's slot 0.
SCATTER sweep-1 no-head slot-0 step: at a head-bit cell with no head
(wH = zero) and no incoming carry (rc t = false), write zero (preserving
the cell) and advance to slot 1. The common case for tapes without a head in
this block.
SCATTER sweep-1 no-head symbol step (slot 1 or 2 with writeFlag = false):
the symbol cell is preserved (readBackWrite) and the sweep advances.
SCATTER sweep-1 no-head triple (trace 3): a tape with no head in this
block (head-bit zero) and no incoming carry (rc = false) is passed through
untouched — its three cells are preserved and the sweep advances to the next
tape, carries/markers unchanged. The common per-tape case in a block.
SCATTER sweep-1 head slot-0, stay step: at a head-bit cell with a head
(wH = one) whose δ action is stay, keep the bit (one, preserving the
cell), set writeFlag (so the symbol cells get the new symbol), advance.
SCATTER sweep-1 head slot-0, left step: a head whose δ action is left
keeps its bit here for now (one, cell preserved) and is recorded in
isLeftMover (sweep-2 moves it one block left); writeFlag is set, advance.
SCATTER sweep-1 head slot-0, right step: a head whose δ action is right
leaves this cell (zero — the bit is cleared, changing the cell), carries the
head one block right via rightCarry, sets writeFlag, and advances.
SCATTER sweep-1 head sym-hi step (slot 1, writeFlag = true): overwrite the
high symbol cell with the new symbol's high bit; writeFlag stays set.
SCATTER sweep-1 head sym-lo step (slot 2, writeFlag = true): overwrite the
low symbol cell with the new symbol's low bit; writeFlag is reset, advancing
to the next tape.
SCATTER sweep-1 head stay triple (trace 3): a tape whose head is in this
block (head-bit one) and stays put writes its new symbol into the two symbol
cells, keeps its head-bit, and advances; carries/markers unchanged.
SCATTER sweep-1 head left triple (trace 3): like the stay triple (writes
the new symbol, keeps the head-bit here), but records the tape in isLeftMover
so sweep-2 will move its bit one block left.
SCATTER sweep-1 head right triple (trace 3): a head moving right clears its
head-bit here (zero), writes its new symbol into the two symbol cells, and
carries the head one block right via rightCarry; three cell writes total.
SCATTER sweep-1 deposit slot-0 step: at a head-bit cell with no head
(wH = zero) but an incoming carry (rc t = true — a head moved right into
this block), deposit the head-bit (write one, clearing the carry); the symbol
cells are not overwritten (writeFlag stays false).
SCATTER sweep-1 deposit triple (trace 3): a no-head tape with an incoming
carry gets its head-bit deposited (write one), symbols preserved, carry
cleared, advance. The right-mover landing case.
The SCATTER sweep-1 → sweep-2 turn-around (trace 1): once the freshly
materialized block is complete (mat, back at tape 0 slot 0, reading the
□ past it), the sweep turns leftward into sweep-2 at the last block's last
cell.
SCATTER block step — no-head tape. Tape m has no head in block b
((c.work m).head ≠ b) and no incoming carry (¬((c.work m).head = b-1 ∧ right),
so rc m = false): its three cells are unchanged — which already IS the
intermediate encoding, since the head neither sits at nor moves into b.
Advances the within-block invariant b m → b (m+1) with rc/ilm unchanged.
SCATTER block step — deposit (right-mover landing). Tape m has no head
in block b but an incoming carry: its head moved right out of b-1
((c.work m).head = b-1 ∧ dir = right, so rc m = true). The deposit writes
the head-bit one at (b,m) (clearing the carry); symbols stay (the new
symbol was written back at b-1). The intermediate head IS at b
(scatterInterWork.head = (b-1)+1 = b). Advances b m → b (m+1), clearing
rc m.
SCATTER block step — head, stay. Tape m has its head at block b
((c.work m).head = b) with δ-action stay: keep the head-bit one, write
the new symbol into the two symbol cells. The intermediate head stays at b
(scatterInterWork.head = b, since stay ≠ right) and the intermediate symbol
at b is the new write (scatterInterWork.cells b = (wact m).1, via
cells_at_head), matched to the triple's encSymW writes by the codec bridge.
Advances b m → b (m+1), rc/ilm unchanged.
SCATTER block step — head, left. Like head_stay (head-bit kept one,
new symbol written) but the δ-action is left: the tape is recorded in
isLeftMover (sweep-2 moves its bit one block left later). The intermediate
head still sits at b (scatterInterWork.head = b, since left ≠ right), so
the SCATTER-1 target is unchanged from stay; only ilm advances.
SCATTER block step — head, right. Tape m's head at b moving right:
clears the head-bit here (zero), writes the new symbol, carries the head one
block right via rc. The intermediate head moves to b+1
(scatterInterWork.head = b+1 ≠ b), so the cleared zero matches; the new
symbol at b (the old head's cell) matches via the codec bridge. Advances
b m → b (m+1), setting rc m.
SCATTER one full block (trace (3*k)). Sweeping all k tapes of block b
advances the mid-sweep invariant Scatter1MidInv … b → … (b+1): the head moves
to blockStart k (b+1), the carry rc updates from the incoming
decide(head = b-1 ∧ right) to the outgoing decide(head = b ∧ right) (= the
incoming carry of block b+1), and ilm records block b's left-movers.
Wraps scatter1_block_aux at m = k between ofMid and toMidSucc.
One non-turnaround SCATTER sweep-1 step stays in scatter1. As long as the
sweep is not at the turnaround trigger (mat = true ∧ pos = (0,0)), one step from
a scatter1 config lands in scatter1 again — scatter1Step only escapes to
scatter2 in that one branch. The condition is on the state data alone (no
head/read needed), so it threads cleanly through a per-step induction.
SCATTER block sweep stays in scatter1 (per step). Within one block of the
sweep-1 phase (mat = false, slot-0 block entry), every micro-step s ≤ 3*k
keeps the simulator in a scatter1 state. Proved by reaching the nearest 3-step
boundary with scatter1_block_aux (whose output is a scatter1, slot-0,
mat = false config — so ¬turnaround) and stepping the remaining s % 3 ≤ 2
micro-steps with scatter1_step_stays (the carried pos/mat never hit the
turnaround trigger).
SCATTER materialize sweep stays in scatter1 (per step). During the
materialize phase (block M+1, 3*k micro-steps), every step s < 3*k keeps the
simulator in scatter1. Mirrors scatter1_block_states: reach the 3-step boundary
with scatter1_mat_aux (slot-0, mat = (m ≠ 0), so the turnaround trigger
mat ∧ pos = (0,0) needs m = 0 — but then mat = false), then step the residual
< 3 micro-steps (pos ≠ (0,0)). The trigger is only at the very end s = 3*k.
SCATTER sweep-1 state discipline. Throughout the entire sweep-1 phase
(all i < 3*k*(M+1) + 1 steps from its start), the simulator's state is never
a gather state. Used to rule out spurious decision points inside the sweep.
SCATTER sweep-1 — target (the crux, proof in progress). From the
REWIND-produced scatter1 config (cell 1, pos (0,0), rightCarry marking
the position-0 heads, all else empty, encoding the old c.work at M), the
sweep runs 3*k*(M+1) + 1 steps and lands in SCATTER sweep-2 with the work
tape encoding the intermediate configuration (scatterInterWork — new
symbols everywhere, right/stay heads relocated, left-movers parked at the old
spot) materialized to M+1, recording the left-movers in isLeftMover. The
work tape is existential (its exact head position is incidental — sweep-2
consumes it). This is the research-grade core; the proof will decompose as
triple → block (rightCarry in→out) → M-block sweep → materialize → turnaround.
One scatter sweep-2 step (trace 1): from a scatter2 d config, the result is
the configuration built from scatter2Step's output. Basis of the SCATTER sweep-2
correctness (the leftward phase that deposits the recorded left-movers).
SCATTER sweep-2 → COMMIT turn-around (trace 1): reading ▷ at cell 0 ends the
leftward sweep, hands the deferred output write/move to COMMIT, and steps the work
head right to cell 1.
A SCATTER sweep-2 symbol step (slot 1 or 2, non-▷): the leftward sweep
only touches head-bit cells, so a symbol cell is read back unchanged and the head
retreats one cell.
A SCATTER sweep-2 clear step (slot 0, head-bit one, this tape is a recorded
left-mover): clear the bit here (zero) and set leftCarry so the bit is re-deposited
one block to the left; the head retreats.
A SCATTER sweep-2 deposit step (slot 0, incoming leftCarry, not itself a
left-mover to clear): deposit the head-bit here (one), clearing both this tape's
isLeftMover mark and the carry; the head retreats. The left-mover lands one block left.
A SCATTER sweep-2 keep step (slot 0, neither a left-mover to clear nor an
incoming carry): the head-bit is read back unchanged and the head retreats.
SCATTER sweep-2 clear triple (trace 3): three leftward steps over a tape whose
head-bit (slot 0) is one and which is a recorded left-mover — two symbol cells read
back unchanged, then the head-bit cleared (zero) with leftCarry set. Head retreats 3.
SCATTER sweep-2 deposit triple (trace 3): three leftward steps over a tape with
an incoming leftCarry (and not itself a clear) — two symbol cells unchanged, then the
head-bit deposited (one), clearing isLeftMover and the carry. Head retreats 3.
SCATTER sweep-2 keep triple (trace 3): three leftward steps over a tape that is
neither a left-mover to clear nor a carry to deposit — all three cells read back
unchanged, head retreats 3.
SCATTER sweep-2 per-tape — keep. Tape k-1-m of block p is neither a
left-mover to clear at p (¬(scatterInterWork.head = p ∧ isLeftMover)) nor a
deposit target (leftCarry ≠ true): its head-bit is read back unchanged. The
intermediate and final head-bits at p agree (hfin), so this already IS the
final encoding. Advances Scatter2BlockInv … p m → … p (m+1).
SCATTER sweep-2 per-tape — clear. Tape k-1-m of block p is a recorded
left-mover whose intermediate head-bit sits at p (hheadp, hlm): clear the
bit here (→ zero, since the left-mover's final head is p-1 ≠ p, hfinne) and
set leftCarry so the bit re-deposits one block left. Advances
Scatter2BlockInv … p m → … p (m+1).
SCATTER sweep-2 per-tape — deposit. Tape k-1-m of block p has an
incoming leftCarry (hlc, set when its left-mover bit was cleared at block
p+1): its intermediate head-bit at p is zero (hninter), but its final head
lands at p (hfineq), so deposit the bit here (→ one), clearing both this
tape's isLeftMover mark and the carry. Advances Scatter2BlockInv … p m → … p (m+1).
SCATTER sweep-2 single block (trace (3*k)). Processing one full block p
(leftward) from the block-(p+1) boundary: after 3*k steps the head sits at
blockStart k p - 1, the isLeftMover/leftCarry flags are updated to their
boundary-p forms, and the tape satisfies Scatter2MidInv … p.
SCATTER sweep-2 stays in scatter2 off ▷ (per step), with tape geometry. One
sweep-2 step from a scatter2 config whose work head is ≥ 1 (so it does NOT read
▷, given the cells below the head are non-▷) stays in scatter2. The new work
head is head - 1 and only the old head cell is overwritten — every other cell is
preserved. This is the per-step lever for the scatter2 sweep ¬gather lemma.
SCATTER sweep-2 block sweep stays in scatter2 (per step). Within one block of the
leftward sweep-2 phase (from the Scatter2MidInv … (p+1) entry), every micro-step
s ≤ 3*k keeps the simulator in a scatter2 state. Proved by reaching the nearest
3-step (per-tape) boundary with scatter2_block_aux (whose output is scatter2 with a
known head ≥ blockStart k p + 2 ≥ 3 and a Scatter2BlockInv tape, so the read is
≠ ▷) and stepping the remaining s % 3 ≤ 2 micro-steps with scatter2_step_stays
(each read is at a cell ≥ 1, hence non-▷ by Scatter2BlockInv.cells_ne_start).
SCATTER sweep-2 — no GATHER step (per micro-step). Over the whole 3*k*(M+1) + 1
sweep-2 phase (from the same entry as scatter2_sweep), no intermediate state is a
gather state — the simulator stays in scatter2 until the final ▷-triggered turn
into commit. Companion to scatter1_sweep_states: it shows the constant-choice trace
has no choice-consuming (gather-on-□) step in this phase, the input to
trace_congr_choices for macroStepCorr_rev. The hypotheses are identical to
scatter2_sweep for call-site uniformity. Decomposes as a scatter2_sweep_aux block
sweep (every 3*k-boundary is scatter2) plus a scatter2_block_states residual.
SCATTER sweep-2 → COMMIT (trace (3*k*(M+1) + 1)). From the sweep-1 output
(scatter2 entry: isLeftMover = decide(left), leftCarry = 0, head at
blockStart (M+2) - 1, the work tape SimInvAt (M+1)-encoding scatterInterWork),
sweep all M+1 blocks leftward (turning each left-mover's head-bit) and then read
▷ to hand off to COMMIT. The work tape now SimInvAt (M+1)-encodes the final
config scatterFinalWork — exactly N's one-step images. Wraps scatter2_sweep_aux
(at B = M+1) between ofSimInv and toSimInv, then scatter2_start.
N's one-step work-tape image (writeAndMove w d) is exactly the SCATTER
final tape scatterFinalWork ct (w, d): both write w at the old head and
then move per d (left ↦ head-1, right ↦ head+1, stay ↦ head). This is the
bridge between N.trace 1 and the SCATTER phases' encoding target.
N.trace 1 in SCATTER-final form. From a non-halted c, one N-step
(choice bitf 0) yields the state/input/output of N.δ and work tapes that are
exactly scatterFinalWork of the old tapes under the δ-action wact (work
write/dir). The encoding-side description that the SCATTER phases produce.
Deterministic front half (run → gather → COMPUTE → rewind). From a
corresponding non-halted config, the simulator (constant choice bit) reaches
the SCATTER sweep-1 entry in 3 + 6*k*M steps: the work tape still encodes
c.work at M (head parked at cell 1), the SCATTER actions wact/oWoD/iD
are read off N.δ bit … (the one COMPUTE use of bit), and the input/output
heads have dodged off ▷.
Decision-point characterization (constant-choice macro-step). Along the
CONSTANT-choice trace of one macro-step (the run → gather → rewind → scatter1 → scatter2 → commit cycle, total length m), a step index i is a
trace_congr_choices decision point — the simulator is in a gather state and
the work head reads the □ sentinel — iff i = p0 = 1 + 3*k*M, the single
GATHER-sentinel (COMPUTE) step. This is the lever that turns trace_congr_choices
and forward corr_macroStep into the backward (arbitrary-choice) correspondence.
Assembled per phase: i = 0 is run (not gather); the gather sweep
[1, p0) reads non-□ (gather_sweep_no_sentinel); i = p0 is the unique
gather-on-□; the rewind sweep keeps rewind (rewind_sweep_states); the
two scatter sweeps keep scatter1/scatter2 (scatter{1,2}_sweep_states); the
final commit step is not gather.
Macro-step correspondence — explicit form. Same content as
corr_macroStep, but with the step count m written out literally (the
macro-step length) and the choice sequence fixed to the constant fun _ => b.
corr_macroStep is a thin existential wrapper around this; macroStepCorr_rev
needs the explicit m so it can invoke macroStep_decision_point_iff (which
is stated over exactly this length) to discharge trace_congr_choices.
Macro-step correspondence (the core obligation). From a corresponding,
non-halted configuration, for any nondeterministic choice bit, the
simulator runs some number m of steps (with a choice sequence that feeds
bit at the COMPUTE sub-step) and lands in a configuration corresponding to
N's one-step image under bit, with the materialized region grown by one,
within macroBound k M sim steps.
This is the heart of the behavioural correctness proof: it is established by
tracing the phase machine run → gather → rewind → scatter1 → scatter2 → commit and showing each phase preserves/advances SimInvAt.
Trace-level choice irrelevance. Two choice sequences that agree at every
step where the simulator is at a GATHER state reading the □ sentinel (the
only step consulting the nondeterministic bit — the COMPUTE sub-step) drive
the simulator to the same configuration. Proved by induction on the step
count, using simDelta_eq_of_forall_ne_blank at each step: where the configuration is
not a □-reading GATHER step the choice is irrelevant, and where it is the
hypothesis forces the two sequences to agree.
Iterated correspondence. Simulating t steps of N (choices g): the
simulator reaches, in some number m of steps (choices from a single
ℕ-indexed F), a configuration corresponding to N.trace t g c (at some
materialization level M'). Proved by induction on t, composing
macro-steps with trace_add_fun; the halted case reuses the previous one.
Forward acceptance. If N accepts x within Tn steps, then
singleTapeSim N accepts x within Tn · macroBound k Tn + 1 steps:
simulate N's accepting run (corr_iterate), then one halted_of_corr step lands in
a halted accepting simulator config; pad via AcceptsInTime.mono.
Reverse direction: arbitrary simulator choices induce an N-run #
The forward theorems (corr_iterate,
acceptsInTime_singleTapeSim_of_acceptsInTime) drive the simulator with a
purpose-built choice stream. The surface lemmas also need the converse flow:
an ARBITRARY simulator stream still walks the macro-step structure, because
each macro-step consults its nondeterministic bit only at one decision point
(macroStep_decision_point_iff), so trace_congr_choices replaces each
arbitrary segment with the constant-choice segment of
corr_macroStep_explicit. Crucially the decision positions are closed-form
(decisionPos — independent of the run), so the induced N-choices can be
read off the stream up front, with no circularity.
Micro-step length of the macro-step at materialization level M (the
explicit count in corr_macroStep_explicit).
Equations
Instances For
Micro-step position of the start of the t-th macro-step (cumulative sum
of the preceding macro-step lengths; the materialization level after t
macro-steps is exactly t).
Equations
Instances For
Position of the single decision point (the GATHER-on-□ COMPUTE sub-step)
inside the t-th macro-step: offset 1 + 3kt from the macro-step start.
Equations
- Complexity.NTM.SingleTape.decisionPos k t = Complexity.NTM.SingleTape.macroPos k t + (1 + 3 * k * t)
Instances For
The N-choice stream induced by a simulator choice stream: the bits the
simulator consults at the (closed-form) decision positions.
Equations
Instances For
Each macro-step's length fits in the per-macro-step budget macroBound.
The macro-step boundary position is bounded by the cumulative budget:
macroPos k t ≤ t * macroBound k t.
Segment choice replacement. Along one macro-step from a corresponding,
non-halted configuration, an arbitrary choice stream drives the simulator to
the same configuration as the constant stream feeding the arbitrary stream's
bit at the macro-step's single decision point (offset 1 + 3kM).
Reverse iterated correspondence. For an ARBITRARY simulator choice
stream ch: as long as N's induced run (inducedChoices) has not halted,
the simulator's configuration at the macro-step boundary macroPos k t
corresponds to N's t-step configuration.
Reverse halting. If the N-run induced by an arbitrary simulator stream
ch halts within Tn steps, the simulator (driven by ch) halts within
Tn * macroBound k Tn + 1 micro-steps, with its accept bit agreeing with
N's output bit. This is the engine behind both surface lemmas: it bounds
EVERY simulator path by the simulated machine's halting bound.