Executable test machines

The Milestone B acceptance tests (planning/tm-infrastructure.md): concrete machine codes whose runs are evaluated inside the kernel — every example … := by decide below both pins the expected behaviour as a regression test and certifies that the whole evaluation path (Code.toTM, Code.actionAt, Turing.transitionIndex, MultiInputTM.step/configs/outputString) is genuinely executable, with no Fintype.elems, choice, or noncomputable anywhere in it (decision D5). No native_decide is used.

Machines (all at arity one, alphabet size two):

1. defaultRejectCode i — output 0 and halt (arity-generic; the total-decoding default of Milestone C);
2. copyBit — copy the first input bit;
3. moveLeftTwice — walk onto the left blank boundary and verify clamping;
4. moveRightTwice — walk past the last symbol and verify clamping;
5. workTapeRoundTrip — write a symbol, move away, come back, reread it, output it;
6. loopForever — a two-state machine that never halts.

The probe helpers project decidable data (states, head positions, output bits, tape windows) out of configurations, whose tape fields are functions and therefore not themselves comparable.

The default reject machine

def Turing.Code.defaultRejectAction (i : ℕ) : RawAction

The action of the default reject machine: touch nothing, output 0, halt.

Equations

• Turing.Code.defaultRejectAction i = { inputMoves := Array.replicate i Turing.Move.stay, workActions := #[], output := some false, nextState := none }

def Turing.Code.defaultRejectCode (i : ℕ) : Code i

The default reject machine: two symbols, one state, no work tapes; on its first transition it outputs 0 (i.e. false) and halts, regardless of the observation. This is the total interpretation of malformed descriptions in Milestone C.

Equations

• One or more equations did not get rendered due to their size.

Probe helpers

def Turing.Code.stateAt {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) : Option ℕ

The state (as a raw number) after t steps on bit inputs x.

Equations

• c.stateAt x t = Option.map Fin.val (Turing.MultiInputTM.configs (Turing.MultiInputTM.initCfg (c.bitInputs x)) t).state

def Turing.Code.inputPosAt {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) (j : Fin i) : ℕ

The position of input head j after t steps on bit inputs x.

Equations

• c.inputPosAt x t j = ↑((Turing.MultiInputTM.configs (Turing.MultiInputTM.initCfg (c.bitInputs x)) t).inputPos j)

def Turing.Code.inputSymbolAt {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) (j : Fin i) : Option ℕ

The symbol (as a raw number) under input head j after t steps.

Equations

• c.inputSymbolAt x t j = Option.map Fin.val ((Turing.MultiInputTM.configs (Turing.MultiInputTM.initCfg (c.bitInputs x)) t).inputSymbol j)

def Turing.Code.workWindow {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) (d : Fin c.workTapeCount) (lo : ℤ) (len : ℕ) : List (Option ℕ)

A window of len cells of work tape d, starting at position lo, after t steps.

Equations

• One or more equations did not get rendered due to their size.

def Turing.Code.outBitsAt {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) : List Bool

The bits output during the first t steps on bit inputs x.

Equations

• c.outBitsAt x t = c.decodeBitOutput (c.toTM.outputString (Turing.MultiInputTM.initCfg (c.bitInputs x)) t)

def Turing.Code.spaceAt {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) : ℕ

The work-tape space used up to step t on bit inputs x.

Equations

• c.spaceAt x t = Turing.MultiInputTM.spaceUsed (Turing.MultiInputTM.initCfg (c.bitInputs x)) t

1: output 0 and halt

2: copy the first input bit

def Turing.Code.copyBit : Code 1

Copy the first input bit: one state; on reading a symbol output it and halt, on reading the blank boundary output 0 and halt.

Equations

• One or more equations did not get rendered due to their size.

3: move left onto the blank boundary

def Turing.Code.moveLeftTwice : Code 1

Move the input head left twice (the second move is clamped at the left boundary), then halt.

Equations

• One or more equations did not get rendered due to their size.

4: move right past the final symbol

def Turing.Code.moveRightTwice : Code 1

Move the input head right twice (the second move is clamped at the right boundary), then halt.

Equations

• One or more equations did not get rendered due to their size.

5: write, move, return, and reread a work-tape symbol

def Turing.Code.workTapeRoundTrip : Code 1

Write symbol 1 on the work tape, move the work head right, move it back left, reread the written symbol, output it as a bit, and halt. Observation digits are inputDigit * 3 + workDigit; in state 2 the entries with work digit 2 (symbol 1 under the work head) output true.

Equations

• One or more equations did not get rendered due to their size.

6: a two-state machine that never halts

def Turing.Code.loopForever : Code 1

Bounce between two states forever, never halting.

Equations

• One or more equations did not get rendered due to their size.

Display demos (#eval doubles as an executability check)