The reference evaluator for coded machines

Milestone D (planning/tm-infrastructure.md): the specification-side evaluator against which the universal machine (Milestones E–G) will be verified, independent of its eventual construction language. Everything is definitional over Code.toTM — this file re-implements nothing:

• Code.runFor — the configuration after t steps on bit inputs;
• Code.outputFor — the decoded bit output after t steps;
• Code.evalWithin — total, executable, budgeted evaluation (Code.BoundedResult);
• Code.Produces — the relational input/output semantics.

The three views agree (decision D12): evalWithin_eq_halted_iff and evalWithin_eq_timeout_iff characterize the budgeted evaluator by configurations, evalWithin_halted_mono makes budgeted results stable, and produces_iff_exists_evalWithin ties the relational semantics to the executable one — via the bit-level bridge outputString_isBit/map_bitEmbedding_decodeBitOutput (coded machines only ever emit the two reserved bit symbols, so decoding loses nothing). Produces.unique records that outputs are deterministic.

The BoundedResult bit codec is deliberately deferred to the Milestone F interface.

The step-indexed run

def Turing.Code.runFor {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) : MultiInputTM.Cfg i c.workTapeCount c.Symbol c.State (c.bitInputs x)

The configuration reached by the coded machine c on bit inputs x after t steps.

Equations

• c.runFor x t = Turing.MultiInputTM.configs (Turing.MultiInputTM.initCfg (c.bitInputs x)) t

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

The bits emitted by c on bit inputs x during the first t steps.

Equations

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

@[simp]

theorem Turing.Code.runFor_zero {i : ℕ} (c : Code i) (x : Fin i → List Bool) : c.runFor x 0 = MultiInputTM.initCfg (c.bitInputs x)

theorem Turing.Code.runFor_succ {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) : c.runFor x (t + 1) = MultiInputTM.step (c.runFor x t)

theorem Turing.Code.runFor_add {i : ℕ} (c : Code i) (x : Fin i → List Bool) (a b : ℕ) : c.runFor x (a + b) = MultiInputTM.configs (c.runFor x a) b

theorem Turing.Code.runFor_of_halt {i : ℕ} {c : Code i} {x : Fin i → List Bool} {t : ℕ} (h : (c.runFor x t).state = none) (d : ℕ) : c.runFor x (t + d) = c.runFor x t

Once halted, the run is frozen.

@[simp]

theorem Turing.Code.outputFor_zero {i : ℕ} (c : Code i) (x : Fin i → List Bool) : c.outputFor x 0 = []

theorem Turing.Code.outputFor_succ {i : ℕ} (c : Code i) (x : Fin i → List Bool) (t : ℕ) : c.outputFor x (t + 1) = c.outputFor x t ++ c.decodeBitOutput (MultiInputTM.outputSymbol (c.runFor x t)).toList

theorem Turing.Code.outputFor_of_halt {i : ℕ} {c : Code i} {x : Fin i → List Bool} {t t' : ℕ} (hle : t ≤ t') (h : (c.runFor x t).state = none) : c.outputFor x t' = c.outputFor x t

The output is frozen once the machine has halted.

Budgeted evaluation

inductive Turing.Code.BoundedResult : Type

The result of running a coded machine under a step budget. Its canonical bit codec is deferred to the universal-machine interface (Milestone F).

• timeout : BoundedResult

  The machine was still running when the budget ran out.

• halted (output : List Bool) : BoundedResult

  The machine halted within the budget, with the given output bits.

def Turing.Code.instDecidableEqBoundedResult.decEq (x✝ x✝¹ : BoundedResult) : Decidable (x✝ = x✝¹)

Equations

• Turing.Code.instDecidableEqBoundedResult.decEq Turing.Code.BoundedResult.timeout Turing.Code.BoundedResult.timeout = isTrue ⋯
• Turing.Code.instDecidableEqBoundedResult.decEq Turing.Code.BoundedResult.timeout (Turing.Code.BoundedResult.halted output) = isFalse ⋯
• Turing.Code.instDecidableEqBoundedResult.decEq (Turing.Code.BoundedResult.halted output) Turing.Code.BoundedResult.timeout = isFalse ⋯
• Turing.Code.instDecidableEqBoundedResult.decEq (Turing.Code.BoundedResult.halted a) (Turing.Code.BoundedResult.halted b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Turing.Code.instDecidableEqBoundedResult : DecidableEq BoundedResult

Equations

• Turing.Code.instDecidableEqBoundedResult = Turing.Code.instDecidableEqBoundedResult.decEq

def Turing.Code.instReprBoundedResult.repr : BoundedResult → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Turing.Code.instReprBoundedResult : Repr BoundedResult

Equations

• Turing.Code.instReprBoundedResult = { reprPrec := Turing.Code.instReprBoundedResult.repr }

def Turing.Code.evalWithin {i : ℕ} (c : Code i) (x : Fin i → List Bool) (T : ℕ) : BoundedResult

Budgeted evaluation: run for T steps; report the output if the machine has halted by then, and timeout otherwise. Total and executable.

Equations

• c.evalWithin x T = if (c.runFor x T).state.isNone = true then Turing.Code.BoundedResult.halted (c.outputFor x T) else Turing.Code.BoundedResult.timeout

theorem Turing.Code.evalWithin_eq_halted_iff {i : ℕ} {c : Code i} {x : Fin i → List Bool} {T : ℕ} {y : List Bool} : c.evalWithin x T = BoundedResult.halted y ↔ (c.runFor x T).state = none ∧ c.outputFor x T = y

theorem Turing.Code.evalWithin_eq_timeout_iff {i : ℕ} {c : Code i} {x : Fin i → List Bool} {T : ℕ} : c.evalWithin x T = BoundedResult.timeout ↔ ¬(c.runFor x T).state = none

theorem Turing.Code.evalWithin_halted_mono {i : ℕ} {c : Code i} {x : Fin i → List Bool} {T T' : ℕ} {y : List Bool} (hle : T ≤ T') (h : c.evalWithin x T = BoundedResult.halted y) : c.evalWithin x T' = BoundedResult.halted y

Budgeted results are stable under enlarging the budget.

The relational semantics

def Turing.Code.Produces {i : ℕ} (c : Code i) (x : Fin i → List Bool) (y : List Bool) : Prop

The relational input/output semantics: c on bit inputs x halts with output bits y, in some time and space.

Equations

• c.Produces x y = ∃ (t : ℕ) (s : ℕ), c.toTM.ComputesInTimeAndSpace (c.bitInputs x) (List.map (fun (b : Bool) => c.bitEmbedding b) y) t s

The bit-level bridge

@[simp]

theorem Turing.Code.bitEmbedding_val_beq_one {i : ℕ} (c : Code i) (b : Bool) : (↑(c.bitEmbedding b) == 1) = b

@[simp]

theorem Turing.Code.decodeBitOutput_nil {i : ℕ} (c : Code i) : c.decodeBitOutput [] = []

@[simp]

theorem Turing.Code.decodeBitOutput_cons {i : ℕ} (c : Code i) (s : c.Symbol) (l : List c.Symbol) : c.decodeBitOutput (s :: l) = (↑s == 1) :: c.decodeBitOutput l

theorem Turing.Code.outputString_isBit {i : ℕ} (c : Code i) {input : Fin i → List c.Symbol} (cfg : MultiInputTM.Cfg i c.workTapeCount c.Symbol c.State input) (t : ℕ) (s : c.Symbol) : s ∈ c.toTM.outputString cfg t → ∃ (b : Bool), s = c.bitEmbedding b

Coded machines only ever emit the two reserved bit symbols.

theorem Turing.Code.map_bitEmbedding_decodeBitOutput {i : ℕ} (c : Code i) {l : List c.Symbol} (h : ∀ s ∈ l, ∃ (b : Bool), s = c.bitEmbedding b) : List.map (fun (b : Bool) => c.bitEmbedding b) (c.decodeBitOutput l) = l

Decoding is a section on strings of bit symbols.

theorem Turing.Code.produces_iff_exists_evalWithin {i : ℕ} (c : Code i) (x : Fin i → List Bool) (y : List Bool) : c.Produces x y ↔ ∃ (T : ℕ), c.evalWithin x T = BoundedResult.halted y

The relational and the budgeted views agree: c produces y exactly when some budget suffices to observe it.

theorem Turing.Code.Produces.unique {i : ℕ} {c : Code i} {x : Fin i → List Bool} {y y' : List Bool} (h : c.Produces x y) (h' : c.Produces x y') : y = y'

Outputs are deterministic.

Executable pins (Milestone B machines)