Assembling the successor check #
⚠️ Unreviewed by Bolton
Complexitylib.Classes.Containments.Internal.BlockScan proves what the scans decide, in terms of
what the registers hold. Complexitylib.Models.TuringMachine.GuessAssembly proves what the guess
machinery puts on a register. This file is where the two meet: a block of guesses written onto a
register is a register the scans can read.
Main results #
Complexity.holdsBits_of_guessBlock— a written block of guesses is a register holding those bitsComplexity.ofTable_state— the state a scan reads off a code's state registerComplexity.blockEmit_work,Complexity.blockEmit_output,Complexity.inHeadEmit_code— what each scan says about the code the registers holdComplexity.mem_codeSucc_of_scans— and together: the scans decidecodeSuccmembershipComplexity.HoldsCode.inj— the registers determine the code, so comparing registers compares codesComplexity.codeBlock,Complexity.codeWidth,Complexity.codeRegsOf— the block layout a code guess usesComplexity.holdsCode_of_guessBlocks,Complexity.holdsCode_of_guessStage,Complexity.holdsCode_of_stage— a guess stage can lay down any code, the rewind that follows it does not disturb one, and a stage of a loop lays down the code its stream namesComplexity.codeBlockScan,Complexity.HoldsCodeScan,Complexity.holdsCodeScan_of_blocks— the padded layout the walk's checks read, and that a guess lays it downComplexity.eqScanner,Complexity.eqScanner_decides,Complexity.eqScanner_accepts— one comparison per block, in one scan, deciding that two guesses are the same code — and accepting when they areComplexity.succScanner,Complexity.succScanner_verdicts— and every successor check in one scan, with each component's verdict recoveredComplexity.succScanner_decides— that scan decides a successor stepComplexity.succScanner_accepts— and accepts a genuine one, which is what says the right guess existsComplexity.walkCodeScanner,Complexity.walkCodeScanner_decides— both halves together: one scan whose verdict is exactly one step of the walk, together with the direction the input head is to takeComplexity.walkCodeScanner_accepts_stay,Complexity.walkCodeScanner_accepts_succ— and accepts either kind of genuine stepComplexity.walkStepScanner,Complexity.walkStepScanner_decides,Complexity.walkStepScanner_accepts,Complexity.walkStepScanner_accepts_stay,Complexity.walkStepScanner_accepts_succ— and with the counter, the whole verdict of a step, in both directionsComplexity.rulerBlock,Complexity.scanTape_of_ruler,Complexity.ruler_of_holds— the guessed register that fixes the scan's lengthComplexity.checkedCells,Complexity.checkPhase_hoareTime— the input check and the scan in sequence, with the check's verdict on a register the scan readsComplexity.checkMove_hoareTime— and with the input head's move, the whole guess-free part of a walk stepComplexity.verdictCells,Complexity.verdictCells_acc_one— and the register a verdict is published onComplexity.loopTestScanner,Complexity.loopTestScanner_decides,Complexity.loopTestScanner_of_fail,Complexity.loopTestTM,Complexity.publishTestTM_hoareTime— the loop's test: stop when the counter reaches its target or a check has failed, with the verdict published whereTM.loopTMreads itComplexity.counterStepScanner,Complexity.counterStepScanner_decides,Complexity.counterStepScanner_accepts— the counter check of a step: stay, or advance by oneComplexity.mem_reachCodes_of_pairWalk— a walk of even length reaches whatever a shorter one doesComplexity.DirCodec,Complexity.dirCodec,Complexity.move_head_of_dir— a direction in one cell, and that the input head lands where the code saysComplexity.adjustedDir,Complexity.move_adjusted,Complexity.dirCheckScanner,Complexity.dirCheckScanner_decides,Complexity.dirCheckScanner_accepts— and the direction a head pinned away from the marker must actually take, decided and acceptedComplexity.move_of_walkStep,Complexity.move_of_walkStay,Complexity.walkStep_transports— a step carries the input head to where the next code says, and its code is one step of the walkComplexity.succ_fields_of_eq— a genuine successor's fields are what the checks compare againstComplexity.WalkLayout,Complexity.WalkWidths— which register plays which role in the walk, and how wide each is guessedComplexity.stageBits,Complexity.walkCert— what one stage of the walk must guess into each of them, and the certificate for a whole walkComplexity.stageCells,Complexity.stageCols— the registers a stage leaves, as the scan sees themComplexity.stage_accepts_stay,Complexity.stage_accepts_succ— a stage of a real walk is accepted, whichever kind of step it takesComplexity.guessFrom_after_stage— and the guess tape is left ready for the next stageComplexity.holdsBits_block_of_stage,Complexity.cell_of_stageand their instances for the code tuples, the parameter block, the counters, the direction cells and the ruler — after a stage, each register holds what the certificate namesComplexity.walkReg,Complexity.WalkLoopInv,Complexity.holdsCounter_of_walkLoopInv,Complexity.inSym_of_walkLoopInv,Complexity.guessFrom_of_walkLoopInv— the walk loop's invariant: the counter names the iteration, the registers hold the code, the input head sits where the code says, and the guess tape still holds what the rest of the walk will needComplexity.walkPairTM,Complexity.guessProtocol_walkPairTM— the loop's body: two steps with the code's registers swapping roles, so no register need be copiedComplexity.walkLoopTM,Complexity.guessProtocol_walkLoopTM— the walk as a machine, driven byTM.binaryForTM's own binary counter, and that only its guess stage consumes guessesComplexity.walkCheckTM,Complexity.walkStepTM,Complexity.walkStepTM_hoareTime,Complexity.guessProtocol_walkStepTM— one walk step as a machine: guess, rewind, check the input symbol, scan, move the input head, and conjoin the verdict into the accumulator; its contract, and that it respects the guess protocol. The step holdsrfurther tapes still (TM.liftMany) — the enclosing loops' counters and the accumulator, none of them guessed, none of them scannedComplexity.windowParams_congr,Complexity.walkParams_eq,Complexity.params_of_holds— all of those checks read the same guessed parameters, through either of the two readersComplexity.walkScanLen— a scan length that covers every check of a walk stepComplexity.mem_reachCodes_of_walk— what a walk establishesComplexity.roundList_of_inj— what the counting establishesComplexity.WalkInv,Complexity.counterVal_of_walkInv— the walk loop's invariant, and that the counter reads back the loop's indexComplexity.walkLoop_hoareTime— and the loop itself, given a body that carries it forwardComplexity.HoldsCounter,Complexity.counterLoop_hoareTime— the general counter-driven loop rule the walk and both enumerations shareComplexity.windowScanner— the scanner that checks one tape window against its successorComplexity.outputScanner,Complexity.headScanner— the output-window and input-head checkersComplexity.stateScanner— the state checkerComplexity.dirScanner,Complexity.dirScanner_decides— the checker that pins the guessed input-head direction, the one cellTM.inMoveTMreadsComplexity.inSym_cells,Complexity.inSym_eq_of_inMatch,Complexity.inMatchVerdict_of_inSym— the guessed input symbol opens the parameter register, whereTM.inMatchTMchecks it against the machine's own input tape, in both directionsComplexity.headZeroScanner,Complexity.headNonZeroScannerand their decision lemmas — whether the simulated input head is at the marker, where no tape read is possibleComplexity.parStart_iff— and that the parameter register opens with two ones exactly when the guessed symbol is the markerComplexity.windowScanner_run,Complexity.outputScanner_run,Complexity.headScanner_run,Complexity.stateScanner_run— and what each computesComplexity.windowScanner_decides,Complexity.outputScanner_decides,Complexity.headScanner_decides,Complexity.stateScanner_decides— and what each decides about the code the registers holdComplexity.combineTM,Complexity.combineTM_hoareTime,Complexity.combineTM_verdict— and the machine that combines their verdicts
Main definitions #
Complexity.CodeRegs— which register holds which field of a codeComplexity.HoldsCode— and that they hold a given code
A block of guesses is a register the scans can read. Writing n + 1 guessed bits onto a
register parked at cell one leaves it holding exactly those bits.
Several blocks of guesses give several registers to read. Each target register, parked at cell one, ends up holding the bits guessed for its own block.
Which register holds which field #
The layout of a configuration code across registers: one for the state, one for the input head, one per work window, and one for the output window.
The register holding the state.
The register holding the input head.
The registers holding the work windows.
The register holding the output window.
Instances For
Guessing a whole code #
The raw width of block p of a code: the state, the input head, the kk work windows, then
the output window.
Equations
Instances For
The block width a code guess passes to TM.guessBlocksTM, which writes n + 1 bits for a
block of n. A field of width zero is guessed one bit wide and its (empty) contents read back
off the prefix.
Equations
- Complexity.codeWidth tm nn S p = Complexity.codeWidthRaw tm nn S p - 1
Instances For
The registers determine the code #
The registers determine the code. The same registers cannot hold two different codes, so comparing registers compares codes — which is what the walk's "stay" step and the final comparison need.
Blocks on the right registers are a code.
A guess stage can lay down any code. Given a guess tape whose bits, block by block, are
the code's own encoding, the kk + 3 guessed registers hold that code. Together with
Complexity.NTM.exists_loadTape this is how a nondeterministic step is taken: guess a code, then
check it.
A stage of the loop lays down the code its stream names. The guess-tape clause of the walk's invariant feeds exactly this.
Holding a code depends only on the registers' cells, not on their heads — which is why a rewind between the guess and the checks is harmless.
After a code-guessing stage the registers hold the code. The stage rewinds the guessed registers so the scans can read them; the rewind moves heads, and a code is held in cells.
The layout the walk's scan reads #
A check reads the guessed transition from the first cells of the parameter register, and the fields it checks from the cells after that. So every register except the state's — whose check reads it alongside the parameters — carries a block of padding as wide as the parameter block, and its field begins where the padding ends.
The block widths that layout guesses.
Equations
- Complexity.codeWidthScan tm nn S p = if p = 0 then Complexity.codeWidth tm nn S 0 else (Complexity.succParamsCodec tm.Q kk).width + Complexity.codeWidth tm nn S p + 1
Instances For
The registers hold code a where the walk's scan looks for it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The block ends with a cell carrying no head marker. The window checks need to know that the chunk just past the window is unmarked; rather than reason about untouched tape, the guess writes one more zero and the check reads it.
Blocks in the walk's layout are a code the scan can read.
What each scan says about the code the registers hold #
The state a scan reads off a code's state register.
What the work-window scan says.
What the output-window scan says.
What the input-head scan says.
The successor check, assembled. Every scan verdict says what its field must, and together they say the guessed code is a successor of the held one.
What the loops establish #
The walk and the counting are stated here in the form the loops produce them: a walk as a sequence of codes each either kept or stepped, and a round list as an injective enumeration.
What a walk establishes. A sequence of codes, each either equal to its predecessor or a verified successor of it, lands in the round its length names.
What the counting establishes. Codes enumerated without repetition, each verified to be in the round, and at least as many of them as the round holds, form a round list — which is what licenses concluding that a code not among them is not in the round.
The shape of a loop invariant #
TM.loopTM_hoareTime_indexed asks for a family of tape predicates E j, a step from E j to
E (j + 1), and a stop at E N. For the walk, E j says the counter holds j and the code
registers hold the j-th code of the walk — so the loop's own index is the walk's index.
The reading of a counter register as a number.
Equations
- Complexity.counterVal cnt wc work = Complexity.binValLE (List.ofFn fun (q : Fin wc) => decide ((work cnt).cells (↑q + 1) = Complexity.Γ.one))
Instances For
A tape predicate pinning a counter register to a value. The bound v < 2 ^ wc is part of it:
past that point a fixed-width counter wraps, and a loop rule needs the counter to name its
index.
Equations
- Complexity.HoldsCounter cnt wc v _inp work _out = (v < 2 ^ wc ∧ Complexity.HoldsBits (fun (p : ℕ) (i : Fin (jj + 1)) => (work i).cells p) 0 cnt (Complexity.bitsOfLenLE wc v))
Instances For
The walk loop's invariant. The bound j < 2 ^ wc is part of it: past that point the counter
would wrap, and the loop rule needs the counter to name the index.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The counter reads back the index. This is the idx obligation of the indexed loop rule:
a tape predicate that pins the counter determines the loop's index.
The scanner that checks one window #
Three tapes are scanned: the parameter block, the old window, the new window; the verdict goes to a fourth. The parameters come first, so by the time the windows are reached the transition is known.
The state of a window check: a chunk position, two buffered columns, and the four running checks.
Equations
Instances For
Equality of window states is decidable; the machine need not be computable.
The state a parameter reader accumulates: how many cells it has read, and the bits.
Equations
- Complexity.ParamAcc tm = (Fin ((Complexity.succParamsCodec tm.Q kk).width + 1) × (Fin 1 → Fin (Complexity.succParamsCodec tm.Q kk).width → Bool))
Instances For
The parameters a window check has read.
Equations
- Complexity.paramsOfTable tm a = (Complexity.succParamsCodec tm.Q kk).ofTable (a.2 0)
Instances For
The parameters a window scan reads off the tapes it is given.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What the window checker computes: the block check, with the parameters it read.
The output-window checker. The same scanner as for a work tape, with the transition's output write and direction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What the output checker computes.
The input-head checker. Two tapes are scanned: the parameter block and, after it, the two input-head registers — the direction is known by the time they are reached.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What the input-head checker computes.
The state checks #
Unlike the window and head checks, these read both registers during the parameter phase — a state field is a constant number of cells — so the check lives entirely in the accumulated table and the per-cell state is trivial.
The width a state check scans: enough for the parameter block and for a state field.
Equations
- Complexity.stateWidth tm = max (Complexity.succParamsCodec tm.Q kk).width (Complexity.qCodec tm.Q).width
Instances For
What a state check has accumulated.
Equations
- Complexity.StateAcc tm = (Fin (Complexity.stateWidth tm + 1) × (Fin 2 → Fin (Complexity.stateWidth tm) → Bool))
Instances For
The state a state check has read off the code's register.
Equations
- Complexity.stateOfTable tm a = (Complexity.qCodec tm.Q).ofTable (Complexity.tableSlice a.2 1 (Complexity.qCodec tm.Q).width ⋯)
Instances For
The parameters a state check has read.
Equations
- Complexity.paramsOfStateTable tm a = (Complexity.succParamsCodec tm.Q kk).ofTable (Complexity.tableSlice a.2 0 (Complexity.succParamsCodec tm.Q kk).width ⋯)
Instances For
The state checker. With isNew = false it checks the old code's state against the guessed
one; with isNew = true, the new code's state against the one the transition produces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What a state checker computes.
When the simulated input head is at the marker #
A machine cannot keep its own input head on cell zero: reading ▷ forces that head right on every
step. But it need not — a simulated head at cell zero reads ▷, which the code's own head field
already says. So the input symbol is checked against the tape only when the head field is nonzero;
when it is zero the check is on the parameter register alone.
A string of zeros has value zero.
The zero-head scan decides that the code's input head is at the marker.
The nonzero-head scan decides that the code's input head is off the marker.
The direction the input head takes #
TM.inMoveTM reads the direction to move the input head from a single cell, because a direction
fits in one writable symbol. That cell is guessed, so a check has to pin it against the guessed
transition — and unlike every other check this one reads a raw symbol rather than a bit.
What a direction check accumulates: the parameters, and the symbol it saw on the direction register's first cell.
Equations
Instances For
The direction check's reader: read the parameter block, and capture the direction register's first cell as it goes past.
Equations
- Complexity.dirRead tm a col = (Complexity.Scanner.bitsStep 1 (Complexity.succParamsCodec tm.Q kk).width (fun (x : Fin 1) => 0) a.1 col, if ↑a.1.1 = 0 then col 1 else a.2)
Instances For
The direction checker. It accepts when the direction register's first cell names the way the guessed transition moves the input head.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The parameters a direction check reads.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The direction checker decides that the guessed direction is the one the transition takes.
The symbol under the input head #
Of every field of a guessed transition, this is the one no scan can check: it has to agree with
the machine's own input tape. So it is laid out first in the parameter block, where
TM.inMatchTM reads it.
The input check passes when the guess is right. The converse of
Complexity.inSym_eq_of_inMatch: this is what the completeness direction needs, since the
certificate names the symbol the simulated head is really over.
The input check pins the guessed input symbol. When the machine's own input head sits
where the simulated one does, the verdict of TM.inMatchTM on the parameter register says exactly
that the guess was right.
The parameter register opens with two ones exactly when the guessed symbol is the marker.
What each scanner decides #
The window checker decides the window condition.
The output checker decides the output-window condition.
The input-head checker decides the input-head condition.
The state checker decides the state condition.
The checks as machines #
Each check is TM.checkTM of its scanner: the scanner names the columns it reads, so the checked
registers need not be adjacent and no check needs a private copy of them. The checks never consult
the guess tape — they are built on the register tapes alone, and the guess tape is added once, at
the very end, by TM.liftLast, which is where their TM.GuessProtocol comes from. Only the
stages that write guesses carry advancing states.
Complexity.windowScanner_decides and its siblings are stated about the three columns a check
reads, which is exactly the restriction TM.checkTM_hoareTime leaves in its postcondition, so
they apply to a full-width check unchanged.
Combining the verdicts #
One scan over every tape, looking only at the result registers' first cells. No placement, so the registers need not be adjacent.
The machine that combines the verdicts.
Equations
Instances For
The combining machine's contract.
The bit the combining machine writes: whether every designated register said yes.
The equality and increment checks #
The walk may keep a configuration as well as step it, and keeping is register equality — decided
by the comparison scanner, one register pair at a time. A counter advances the same way: the next
value is guessed into a second register and Complexity.Scanner.plusOne checks it. Both scanners
already take arbitrary register indices at any width, so neither needs TM.checkTM.
One walk step, as a single scan #
A machine has one result tape, so the checks of a walk step run together: one automaton whose
state is the tuple of theirs, each component frozen at its own length by
Complexity.Scanner.upTo and reading its own registers through
Complexity.Scanner.comap.
The width of block p in the walk's layout: the field's own width, and for every register
but the state's the parameter-block padding in front of it.
Equations
- Complexity.blockLen tm nn S p = if p = 0 then Complexity.codeWidthRaw tm nn S 0 else (Complexity.succParamsCodec tm.Q kk).width + (Complexity.codeWidthRaw tm nn S p + 1)
Instances For
The scan that decides that two register tuples hold the same code: one comparison per block, each frozen at that block's width.
Equations
- Complexity.eqScanner tm nn S j j' = Complexity.Scanner.all (kk + 3) fun (p : Fin (kk + 3)) => (Complexity.Scanner.eq jj (j ↑p) (j' ↑p)).upTo (Complexity.blockLen tm nn S ↑p)
Instances For
The scan that checks the guessed input symbol, conditional on where the simulated head is:
against the parameter register alone when the head is at the marker, and against the machine's own
input tape — through TM.inMatchTM's verdict — when it is not.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equality scan decides that two guesses are the same code.
The equality scan accepts two guesses of the same code.
The input-symbol scan decides the guessed symbol.
The input-symbol scan accepts a correct guess.
The scan that decides a successor step: one check per work window, the output window, the input head, and the two state fields — all against the parameters in the same register.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The parameters a check reads depend only on the register it reads them from. Every check of a walk step reads the same parameter register, so they all work against the same guessed transition — which is what lets one guess serve five checks.
Both readers of the parameter register read the same parameters. The window, output and input-head checks read the guessed transition with one reader; the state checks read it with another, over a wider block. When the register holds an encoding, the two agree — which is what lets the state checks be checks against the same guess as the rest.
Every check of a walk step reads the same parameters.
A successor scan's verdict is the verdict of each of its checks. Each component reads its own registers, over its own cells, exactly as it would have alone.
The successor scan accepts a genuine successor. The converse of
Complexity.succScanner_decides: when the registers really do hold a code and the code the
transition makes of it, every check passes. This is the direction a completeness proof needs — it
says the right guess exists.
The successor scan decides a successor step. Given that the parameter register holds a guessed transition, the scan's verdict says exactly that the second code is what that transition makes of the first. What the scan cannot see is left to the caller: the symbol under the simulated input head, which the machine reads from its own input tape, and that the step stays inside the space window.
The counter check of a walk step: the counter either stays as it was or advances by one. Only the second step of a pair advances it, so that the counter names the loop's iteration.
Equations
- Complexity.counterStepScanner cntOld cntNew wc advance = if advance = true then (Complexity.Scanner.plusOne jj cntOld cntNew).upTo wc else (Complexity.Scanner.eq jj cntOld cntNew).upTo wc
Instances For
The counter check decides what it should.
An encoding of directions in two guessed cells that TM.inMoveTM can read back. A guessed
cell holds a bit, so one cell cannot name one of three directions; the first cell says whether to
move at all and the second which way.
Whether the direction moves the head.
Which way it moves, when it does.
And how to read the pair back.
Reading back what was written gives the direction again.
Both cells hold bits, so a guess can write them.
And likewise the direction cell.
Instances For
The direction codec: the first cell is 1 exactly when the head moves, the second 1 for
right and 0 for left.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The direction that takes max h 1 to max (movedIdx d h) 1.
Equations
- Complexity.adjustedDir d h = if h = 0 then Complexity.Dir3.stay else if Complexity.movedIdx d h = 0 then Complexity.Dir3.stay else d
Instances For
The scan that pins the direction register, conditional on both head fields being off the marker.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The direction check pins the register to the direction the machine must actually take.
The direction check accepts the direction the machine must take.
The counter check accepts the move it is meant to.
The code half of a walk step's scan decides a walk step, and says how the input head
moves. The symbol under the simulated input head is not scanned but read from the machine's own
input tape by TM.inMatchTM, whose verdict the scan requires on register res; hg is the
invariant that the machine's input head sits where the simulated one does.
The walk-step scan accepts a step that stays put.
The walk-step scan accepts a step that advances.
One walk step, as a single scan. Either the guessed code repeats the old one and the
input head is told to stay, or it is a successor and the input head is told to move the way the
transition does. The direction is part of the step because the machine's own input head tracks the
simulated one — TM.inMoveTM reads exactly the cell this check pins.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The walk-step scan decides a step of the walk, how the input head moves, and what the counter does.
The walk-step scan accepts a genuine step.
The check phase #
The input check and the scan, in sequence: the check leaves its verdict on a register, and the scan — which reads every register — takes that verdict into account along with everything else.
The input check leaves the scan well formed. It writes one bit on the verdict register, which is never the ruler.
And so does what it holds.
The check phase's contract.
The guess-free half of a walk step: check the guessed input symbol against the machine's own input tape, run the walk-step scan, and move the input head by the direction the scan pinned. The verdict is left on the result register, where the step's last stage conjoins it into the accumulator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The guess-free part of a walk step. The input check, the scan, and the move of the input head.
The registers after the scan's verdict is copied onto the accumulator.
Equations
- Complexity.verdictCells cells acc v = Function.update cells acc (Function.update (cells acc) 1 (Complexity.Γ.ofBool v))
Instances For
One walk step, as a machine #
Guess the next code (and the transition, and the direction), rewind the guessed registers, check the guessed input symbol against the machine's own input tape, run the walk-step scan, and move the input head. The guess tape is last; everything after the guess stage is guess-free and lifted past it.
One walk step as a machine: guess every register, hold the enclosing loops' r tapes still,
check and move, and conjoin the verdict into the accumulator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The contract of a walk step. Guess every register, then check, move, and record. The
guessed tapes are named by TM.guessBlocksTapes; what they contain is the caller's business, and
Complexity.walkStepScanner_decides is what turns the resulting verdict into a step of the walk.
The accumulator is not a register — no guess can reach it — and it only ever loses its one, which
is what makes a single failed check final in a loop that cannot stop early.
Its advancing states: only the guess stage consumes guesses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A walk step respects the guess protocol. Only the guess stage advances the guess head; the checks and the input-head move never consult it.
The loop's test #
TM.loopTM decides whether to continue by reading cell one of the output tape, while a scan
writes its verdict to a work register. So a test is a scan followed by
TM.writeOutputBitTM, which publishes that register's bit on the output tape. The walk's test
compares the counter against the register holding the target count.
The counter and the target agree exactly when they hold the same number.
The loop's test: stop when the counter reaches its target, or when a check has failed. A failed check leaves the loop early, with the counter short of its target, and the comparison afterwards rejects.
Equations
- Complexity.loopTestScanner cnt target acc wc = ((Complexity.Scanner.eq jj cnt target).upTo wc).or ((Complexity.Scanner.isNotConst jj acc Complexity.Γ.one).upTo 1)
Instances For
When the checks have passed, the loop stops exactly when the counter reaches its target.
The loop's test as a machine: the comparison, then the verdict published where TM.loopTM
reads it.
Equations
- Complexity.loopTestTM cnt target acc wc = (Complexity.TM.twoPassTM (Complexity.loopTestScanner cnt target acc wc)).seqTM (Complexity.TM.writeOutputBitTM (Fin.last (jj + 1)))
Instances For
A published test's contract. The scan runs, and the publish step puts its verdict where
TM.loopTM looks for it: cell one of the output tape.
The walk, as a machine #
A walk step guesses every register — that uniformity is what makes the guess stage's output
match the scan's precondition — so the register holding the old code is overwritten each
iteration, and nothing would pin it to the previous iteration's new code. Rather than copy a
register, the loop's body runs two steps with the roles swapped: the first carries the code
from jold to jnew, the second from jnew back to jold. After an iteration the code is where
it started.
Walks of even length lose nothing, because a step may leave the code alone: a walk of any shorter length is one of these padded with stays.
The loop below is built on TM.loopTM, whose test channel is the output tape. That is fine for
reasoning about the walk in isolation, but the machine NL_subset_coNL_of_counting asks for must
be a transducer, and TM.loopTM rewinds the output tape. The final assembly therefore drives the
same body with TM.binaryForTM, whose counter and limit live on binary work tapes and which
IsTransducer.binaryForTM shows to be output-safe.
The body of the walk: two steps, with the code's registers — and the counter's — swapping roles. Only the second step advances the counter, so it names the loop's iteration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Its advancing states.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paired step respects the guess protocol.
The walk as a machine: paired steps, counted by the loop driver's own binary counter.
TM.binaryForTM is output-safe, which TM.loopTM — whose test channel is the output tape — is
not, and the whole machine has to be a transducer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The walk respects the guess protocol. Only the body's guess stage advances the guess head; the loop driver rewrites every tape it does not own and holds its head still.
A walk taken two steps at a time reaches everything a walk of any shorter length does. The machine's loop body is a pair of steps, so its walks have even length; padding with steps that stay put covers the rest.
The input head follows the simulated one #
TM.inMoveTM moves the machine's own input head by the direction the walk step's check pinned.
That direction is the one the simulated transition takes, and a tape's head moves exactly as
Complexity.movedIdx says — including at the left marker, where both a leftward move and
movedIdx stay put.
A tape's head moves as Complexity.movedIdx says.
A walk step's scan accepts a step that stays put.
A walk step's scan accepts a genuine advancing step. Everything the checks need is supplied: the registers' contents, the direction cells, the counter's move, and the input check's verdict.
The ruler register #
A two-pass scan turns around when it meets a blank on register 0, so that register fixes the
scan's length: it must carry non-blank symbols for exactly as many cells as the scan is to read,
and a blank immediately after. The guess writes it like any other register — a block of ones as
wide as Complexity.walkScanLen — which is why register 0 of the layout is a ruler and the
code's registers start at one.
The ruler register's contents: ones for the length of the scan.
Equations
- Complexity.rulerBlock len = List.replicate len true
Instances For
A register of ones as long as the scan makes the scan well formed. The blank just past the ruler is what stops the rightward pass; it is not written by the guess, so it is the one thing a caller must know about the tape rather than about the guess.
Moving a head that is pinned away from the marker #
The machine's input head sits at max h 1, so it must move by the direction that takes
max h 1 to max h' 1 — which is the simulated direction only when both h and h' are off the
marker, and "stay" otherwise. Both conditions are fields of the two codes, so both are decided by
the same scan.
One walk step carries the input head to where the next code says. Whichever branch the
step took, the direction register holds Complexity.adjustedDir of the step's direction, and a
head parked at max h 1 lands parked at max h' 1.
What one walk step establishes about the tapes. Either branch of the step leaves the input head parked where the new code says, and the code itself is one step of the walk.
The fields of a genuine successor #
The completeness direction starts from a walk that really happens and must produce the guesses
that make every check pass. Complexity.paramsOf names the transition a code takes on a given
choice, and its fields are what the checks compare against.
A genuine successor's fields are what the checks want. The clamps are the space discipline: the step must stay inside the window, which is where the codes live.
The walk's register layout #
Every register the walk uses is guessed, so the layout has to name them all and say how wide each block is. The roles are: the ruler that fixes the scan's length, the parameter block, the direction cell, the input check's verdict, the accumulator the loop's test reads, the two counter registers, the target the counter is compared against, and the two code register tuples.
The role a guessed block plays in the walk.
- ruler
{kk : ℕ}
: BlockRole kk
The ruler that fixes the scan's length.
- par
{kk : ℕ}
: BlockRole kk
The guessed transition's parameters.
- mv
{kk : ℕ}
: BlockRole kk
Whether the input head is to move at all.
- dr
{kk : ℕ}
: BlockRole kk
Which way it is to move.
- res
{kk : ℕ}
: BlockRole kk
The input check's verdict.
- acc
{kk : ℕ}
: BlockRole kk
The accumulator the loop's test reads.
- cnt
{kk : ℕ}
: BlockRole kk
The counter.
- cnt'
{kk : ℕ}
: BlockRole kk
The counter's partner.
- target
{kk : ℕ}
: BlockRole kk
The target the counter is compared against.
- codeA
{kk : ℕ}
(p : ℕ)
: BlockRole kk
Block
pof the first code tuple. - codeB
{kk : ℕ}
(p : ℕ)
: BlockRole kk
Block
pof the second.
Instances For
Which register plays which role in the walk, and that the roles are distinct.
What each block is for.
The block index of each register: block
pis written to registerreg p.- blocks : ℕ
The number of blocks, one per register.
Distinct blocks go to distinct registers.
- rulerIdx : ℕ
The ruler's block.
- parIdx : ℕ
The parameter block's.
- mvIdx : ℕ
The move cell's.
- drIdx : ℕ
The direction cell's.
- resIdx : ℕ
The input check's verdict register.
- accIdx : ℕ
The accumulator the loop's test reads.
- cntIdx : ℕ
The counter, and the register it swaps with.
- cnt'Idx : ℕ
The other counter register.
- targetIdx : ℕ
The target the counter is compared against.
The first code tuple's blocks,
kk + 3of them.The second code tuple's blocks.
- scratch : ℕ
How many blocks come before the two code tuples: the scan's scratch. A step guesses the scratch and one code tuple, and leaves the other tuple where the previous step put it — which is what chains the walk.
The old code's blocks follow the scratch.
The new code's follow those.
And nothing follows them.
The ruler is register zero, where a scan looks for its length.
The ruler is scratch.
So is the parameter block.
So is the move cell.
So is the direction cell.
So is the verdict register.
So is the accumulator.
So is the counter.
So is its partner.
So is the target.
The roles agree with the indices.
The parameter block's role.
The move cell's.
The direction cell's.
The verdict register's.
The accumulator's.
The counter's.
Its partner's.
The target's.
Each code block's.
And the other tuple's.
Instances For
The ruler is a block.
The parameter block is a block.
The move cell is a block.
The direction cell is a block.
The verdict register is a block.
The accumulator is a block.
The counter is a block.
So is its partner.
So is the target.
So is each of the old code's blocks.
And each of the new code's.
The blocks one step of the pair guesses: the scratch, and one code tuple. The first step of a pair writes the new code's blocks and leaves the old code's registers alone; the second does the reverse. That is what chains a walk — the check of each step compares its guess against what the previous step really left behind — and what returns every code to its own registers after a pair.
Equations
Instances For
A step's blocks are blocks.
A step guesses each of its blocks once.
The first step guesses none of the old code's blocks.
The second guesses none of the new code's.
The parameter register.
Instances For
The move register.
Instances For
The direction register.
Instances For
The input check's verdict register.
Instances For
The accumulator.
Instances For
The counter.
Instances For
The counter's partner.
Instances For
The target.
Instances For
The verdict register is not a code register.
Nor is the other tuple's.
Nor the parameter block.
Nor the move cell.
Nor the direction cell.
Nor either counter.
Nor the counter's partner.
The widths the layout's blocks are guessed at. A block of width n writes n + 1 bits, so a
one-cell register — the direction, a verdict — has width zero.
How wide each block is guessed.
The ruler spans the whole scan.
The parameter block spans a transition's parameters.
Whether to move is one cell.
A direction is one cell.
So is a verdict.
And so is the accumulator.
The counters and the target span the counter's width.
The counter's partner is the same width.
And so is the target.
A code's blocks are as wide as the walk's layout says.
And the other tuple's the same.
Instances For
How wide that block is guessed. Both steps of a pair guess the same widths — a code's two tuples are laid out alike — so one width function serves both, and the guess stream advances by the same amount at every stage.
Equations
- Complexity.stepWidth L p = L.width (L.stepIdx true p)
Instances For
A code block is guessed at the code's width.
The first step of a pair guesses its blocks at those same widths.
What one stage of the walk must guess: the ruler, the transition's parameters, the two direction cells, the counters and the target, and the two code tuples. Everything else is a verdict register, whose guessed value is overwritten before it is read.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The code blocks a stage guesses are the code's own.
And the other tuple's are the successor's.
The parameter block a stage guesses is the transition's encoding.
The counter a stage guesses holds its value.
The certificate for a whole walk: what every stage guesses, given the codes it visits, the transitions it takes, the directions those imply and the counter values.
Equations
- Complexity.walkCert L x dc Ps ds cOlds cNews tgt f s = Complexity.stageBits L x dc (Ps s) (ds s) (cOlds s) (cNews s) tgt true (f s) (f (s + 1))
Instances For
A stage's code blocks come off the certificate as that stage's codes.
And the other tuple's as the next code's.
Embed a register index into the walk machine's tape set: the registers, then the scan's result tape, then the guess tape.
Equations
- Complexity.walkReg i = (Fin.castAdd r i.castSucc).castSucc
Instances For
How many guess bits an iteration of the walk consumes: one stage per step, two steps to an iteration.
Equations
Instances For
The tape a step's p-th guessed block goes to.
Equations
- Complexity.stepReg L second p = Complexity.walkReg (L.reg (L.stepIdx second p))
Instances For
A block's own bits fit in the width it is guessed at.
After a stage, each register holds the bits the certificate names for it.
What a step's guess leaves on each of its own blocks. The stage version guesses every block; a step guesses only its own, and this says nothing about the rest — which is what lets the other code tuple survive the step untouched.
The old code's registers hold the code the certificate names.
The new code's registers hold the next code.
The parameter register holds the transition the certificate names.
A counter register holds the value the certificate names.
A one-cell register holds the symbol the certificate names.
The move register holds what the certificate names.
The direction register holds what the certificate names.
The ruler register spans the scan. This is what makes the scan's length well defined.
The registers a stage leaves behind, indexed by register.
Equations
- Complexity.stageCells L W i q = (Complexity.TM.guessBlocksTapes (fun (p : ℕ) => Complexity.walkReg (L.reg p)) L.width L.blocks W (Complexity.walkReg i)).cells q
Instances For
The same, as the scan sees them: indexed by cell first.
Equations
- Complexity.stageCols L W q i = Complexity.stageCells L W i q
Instances For
A register that no block is guessed into keeps what it held. This is what chains a walk: the step that guesses the new code leaves the old code's registers alone, so its check compares the guess against what the previous step really left behind, not against a fresh guess.
The registers a step's guess leaves behind: its own blocks as the certificate names them, every other tape exactly as it was.
Equations
- Complexity.stepCells L second W i q = (Complexity.TM.guessBlocksTapes (Complexity.stepReg L second) (Complexity.stepWidth L) L.stepBlocks W (Complexity.walkReg i)).cells q
Instances For
The certificate a step guesses, read through the step's own block numbering. The two codes are given per stage, because which family is the old one alternates along a pair.
Equations
- Complexity.stepCert L x dc Ps ds cOlds cNews tgt aOld aNew second s p = Complexity.stageBits L x dc (Ps s) (ds s) (cOlds s) (cNews s) tgt true (aOld s) (aNew s) (L.stepIdx second p)
Instances For
And so does its certificate.
A register no block of the step is guessed into keeps what it held.
What a stage leaves on the parameter register, as the scan sees it.
And on the old code's registers.
And on the new code's.
And on the counter.
And on the counter's partner.
And on the target the counter is compared against.
And on the move cell.
And on the direction cell.
What the registers hold when a stage's scan runs. The scan cannot tell whether a register was guessed at this stage or left behind by an earlier one, so the acceptance lemmas take this bundle rather than the guess that produced it.
- par : HoldsBits (fun (q : ℕ) (i : Fin (jj + 1)) => cells i q) 0 L.par ((succParamsCodec tm.Q kk).enc (Ps s))
The parameter block names the transition the step takes.
- codeA (p : ℕ) : p < kk + 3 → HoldsBits (fun (q : ℕ) (i : Fin (jj + 1)) => cells i q) 0 (cA p) (codeBlockScan tm x S (f s) p)
The old code's registers hold the code the step starts from.
- codeB (p : ℕ) : p < kk + 3 → HoldsBits (fun (q : ℕ) (i : Fin (jj + 1)) => cells i q) 0 (cB p) (codeBlockScan tm x S (f (s + 1)) p)
The new code's registers hold the code it reaches.
- cnt : HoldsBits (fun (q : ℕ) (i : Fin (jj + 1)) => cells i q) 0 cO (bitsOfLenLE wc (cOlds s))
The counter.
- cnt' : HoldsBits (fun (q : ℕ) (i : Fin (jj + 1)) => cells i q) 0 cN (bitsOfLenLE wc (cNews s))
Its partner, which the step compares it against.
The target the walk is counting towards.
The move cell of the guessed direction.
Its direction cell.
Instances For
When the two counter registers agree, their roles can be exchanged. The walk's counter
registers are vestigial — TM.binaryForTM owns the loop's index — so both steps of a pair check
only that the counter is unchanged, and it does not matter which register plays which role.
A stage's guess establishes the bundle.
A one-cell block of a step's guess.
What a step's registers hold when its scan runs. The step's own blocks come from the certificate; the other code tuple is whatever the previous step left behind, which the caller supplies. That is the chaining — each check compares a guess against a retained code, never two guesses against each other.
The first step of a pair. It guesses the new code's registers and keeps the old code's, so its scan compares its guess against what the step before really left behind.
The second step of a pair. The families have swapped roles: it guesses the old code's registers and keeps the new code's, which is what returns each code to the registers it started in.
A stage of a walk that stays put is accepted. Every hypothesis is now about the walk and the guess tape: the certificate supplies the registers, and the input check leaves them alone.
A stage of a walk that advances is accepted. The input check's verdict is not assumed: it follows, because the certificate names the transition the code really takes, whose input symbol is the one the machine's own head is over.
A step's ruler register spans the scan, which is what makes the scan well formed.
A step's registers make a well-formed scan. The ruler spans the scan, and the blank that stops the scan is the ruler tape's own — the guess writes up to the ruler's width and no further, so a caller only has to know that the tape was blank there to begin with.
A step advances the guess tape by exactly its own consumption, so the guess-tape clause of the walk's invariant is re-established one step further on.
A stage advances the guess tape by exactly its own consumption. So the guess-tape clause of the invariant is re-established one stage further on.
The walk loop's invariant #
After j iterations the counter names j, the code registers hold the 2j-th code of the walk
— two steps per iteration — and the machine's own input head sits where that code's input head
does, which is what lets TM.inMatchTM check the guessed symbol against the real tape.
What holds between the steps of a walk. The registers are parked and the ruler tape's blank still stops the scan; the code the next step will check against sits in the family that step retains; the machine's own input head is where that code says; and the guess tape is positioned at the step's own share of the certificate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The walk loop's invariant after j iterations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The invariant pins the counter, so Complexity.counterLoop_hoareTime applies to the
walk.
The invariant says what symbol the simulated input head is over, whenever that head is
off the marker. At the marker no machine can keep its own head in place, and none needs to: the
symbol there is ▷, which the code's head field already says.
The machine's input head is never on the marker, which is what lets a step read it.
The invariant says what the guess tape still holds, which is what lets an iteration find the guesses it needs.
The blocks an iteration guesses are read off the stream. The first stage of iteration j
starts at j * walkGuessStride w t, the second a stage further on.
The walk loop. Given a body that carries the invariant one step forward, and a test that
halts at N, the loop carries the initial code to the N-th code of the walk. The counter names
the loop's index, which is what makes the rule's variant decrease.
The increment check advances a counter. A loop does not compute its next index: it guesses it into a second register and checks it here.
A counter-driven loop. Any invariant family whose members pin the counter to their index satisfies the indexed loop rule — the counter names the index, so the rule's variant decreases. The walk, the enumeration of codes and the enumeration of rounds all have this shape.