Well-formed machine codes

RawCode.WellFormed pins down when a raw description denotes a machine: alphabet of size at least two (symbols 0/1 are the I/O bits), a nonempty state set containing the start state, a dense transition table of exactly the canonical size stateCount * (alphabetSize + 1) ^ (i + workTapeCount) (Turing.transitionIndex), and per-entry arity and range constraints.

The predicate comes with an executable checker RawCode.wellFormedB and the equivalence RawCode.wellFormedB_iff (decision D3 of planning/tm-infrastructure.md); through it, WellFormed is decidable, so concrete literals can be certified by decide. The Milestone C parser will run the same checker.

Code i bundles a raw code with its well-formedness proof; by proof irrelevance it is just as first-order as RawCode i (Code.ext, DecidableEq). Code.actionAt is the canonical table lookup, and the Code.actionAt_* lemmas expose the well-formedness facts about the entry it returns — every later consumer of table entries (the interpretation of Milestone B, the serialization of Milestone C, the universal machine of Milestones E–G) goes through this single, dependency-free access point.

The well-formedness predicate

def Turing.RawWrite.checkB : RawWrite → ℕ → Bool

Executable check that a write action only writes symbols below the alphabet size.

Equations

• (Turing.RawWrite.symbol s).checkB x✝ = decide (s < x✝)
• x✝¹.checkB x✝ = true

theorem Turing.RawWrite.checkB_eq_true_iff {w : RawWrite} {σ : ℕ} : w.checkB σ = true ↔ ∀ (s : ℕ), w = symbol s → s < σ

def Turing.nextStateCheckB (Q : ℕ) : Option ℕ → Bool

Executable check that a successor state, if any, is below the state count.

Equations

• Turing.nextStateCheckB Q none = true
• Turing.nextStateCheckB Q (some q) = decide (q < Q)

theorem Turing.nextStateCheckB_eq_true_iff {Q : ℕ} {o : Option ℕ} : nextStateCheckB Q o = true ↔ ∀ q ∈ o, q < Q

def Turing.RawCode.WellFormed {i : ℕ} (c : RawCode i) : Prop

A raw code denotes a machine: the alphabet has at least the two I/O symbols, there is at least one state, the start state is in range, the transition table has exactly the canonical dense size, and every entry has the right arities and only in-range symbols and successor states.

Equations

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

def Turing.RawCode.wellFormedB {i : ℕ} (c : RawCode i) : Bool

The executable well-formedness checker; RawCode.wellFormedB_iff proves it decides RawCode.WellFormed. The Milestone C parser accepts exactly the descriptions passing this check.

The table loops run over toList with List.all (not Array.all) deliberately: List.all is structurally recursive, so the kernel can evaluate this checker and concrete literals can be certified by decide; Array.all does not kernel-reduce on this toolchain.

Equations

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

theorem Turing.RawCode.wellFormedB_iff {i : ℕ} {c : RawCode i} : c.wellFormedB = true ↔ c.WellFormed

The executable checker decides well-formedness.

@[instance_reducible]

instance Turing.instDecidablePredRawCodeWellFormed {i : ℕ} : DecidablePred RawCode.WellFormed

Equations

• Turing.instDecidablePredRawCodeWellFormed c = decidable_of_iff (c.wellFormedB = true) ⋯

Named accessors for the conjuncts

theorem Turing.RawCode.WellFormed.two_le_alphabetSize {i : ℕ} {c : RawCode i} (h : c.WellFormed) : 2 ≤ c.alphabetSize

theorem Turing.RawCode.WellFormed.stateCount_pos {i : ℕ} {c : RawCode i} (h : c.WellFormed) : 0 < c.stateCount

theorem Turing.RawCode.WellFormed.startState_lt {i : ℕ} {c : RawCode i} (h : c.WellFormed) : c.startState < c.stateCount

theorem Turing.RawCode.WellFormed.table_size {i : ℕ} {c : RawCode i} (h : c.WellFormed) : c.table.size = c.stateCount * (c.alphabetSize + 1) ^ (i + c.workTapeCount)

theorem Turing.RawCode.WellFormed.inputMoves_size {i : ℕ} {c : RawCode i} {a : RawAction} (h : c.WellFormed) (ha : a ∈ c.table) : a.inputMoves.size = i

theorem Turing.RawCode.WellFormed.workActions_size {i : ℕ} {c : RawCode i} {a : RawAction} (h : c.WellFormed) (ha : a ∈ c.table) : a.workActions.size = c.workTapeCount

theorem Turing.RawCode.WellFormed.write_lt {i : ℕ} {c : RawCode i} {a : RawAction} (h : c.WellFormed) (ha : a ∈ c.table) {wa : RawWorkAction} (hwa : wa ∈ a.workActions) {s : ℕ} (hs : wa.write = RawWrite.symbol s) : s < c.alphabetSize

theorem Turing.RawCode.WellFormed.nextState_lt {i : ℕ} {c : RawCode i} {a : RawAction} (h : c.WellFormed) (ha : a ∈ c.table) {q : ℕ} (hq : q ∈ a.nextState) : q < c.stateCount

The type of well-formed codes

structure Turing.Code (i : ℕ) : Type

A well-formed machine code: a raw description together with its well-formedness proof. By proof irrelevance, Code i is as first-order as RawCode i itself.

• raw : RawCode i

  The underlying raw description.

• wf : self.raw.WellFormed

  The well-formedness certificate.

theorem Turing.Code.ext {i : ℕ} {c₁ c₂ : Code i} : c₁.raw = c₂.raw → c₁ = c₂

Codes with equal raw descriptions are equal (proof irrelevance).

theorem Turing.Code.ext_iff {i : ℕ} {c₁ c₂ : Code i} : c₁ = c₂ ↔ c₁.raw = c₂.raw

@[instance_reducible]

instance Turing.instDecidableEqCode {i : ℕ} : DecidableEq (Code i)

Equations

• Turing.instDecidableEqCode c₁ c₂ = decidable_of_iff (c₁.raw = c₂.raw) ⋯

@[reducible, inline]

abbrev Turing.Code.workTapeCount {i : ℕ} (c : Code i) : ℕ

The number of work tapes of a coded machine.

Equations

• c.workTapeCount = c.raw.workTapeCount

@[reducible, inline]

abbrev Turing.Code.alphabetSize {i : ℕ} (c : Code i) : ℕ

The alphabet size of a coded machine (at least 2).

Equations

• c.alphabetSize = c.raw.alphabetSize

@[reducible, inline]

abbrev Turing.Code.stateCount {i : ℕ} (c : Code i) : ℕ

The number of states of a coded machine (at least 1).

Equations

• c.stateCount = c.raw.stateCount

@[reducible, inline]

abbrev Turing.Code.startState {i : ℕ} (c : Code i) : ℕ

The start state of a coded machine (in range by well-formedness).

Equations

• c.startState = c.raw.startState

def Turing.Code.actionAt {i : ℕ} (c : Code i) (q : Fin c.stateCount) (as : Fin i → Option (Fin c.alphabetSize)) (bs : Fin c.workTapeCount → Option (Fin c.alphabetSize)) : RawAction

The canonical table lookup: the entry of the dense transition table at the normative position transitionIndex q as bs. All later consumers of table entries go through this single access point.

Equations

• c.actionAt q as bs = c.raw.table[↑(Turing.transitionIndex q as bs)]

theorem Turing.Code.actionAt_mem {i : ℕ} (c : Code i) (q : Fin c.stateCount) (as : Fin i → Option (Fin c.alphabetSize)) (bs : Fin c.workTapeCount → Option (Fin c.alphabetSize)) : c.actionAt q as bs ∈ c.raw.table

theorem Turing.Code.actionAt_inputMoves_size {i : ℕ} {c : Code i} {q : Fin c.stateCount} {as : Fin i → Option (Fin c.alphabetSize)} {bs : Fin c.workTapeCount → Option (Fin c.alphabetSize)} : (c.actionAt q as bs).inputMoves.size = i

theorem Turing.Code.actionAt_workActions_size {i : ℕ} {c : Code i} {q : Fin c.stateCount} {as : Fin i → Option (Fin c.alphabetSize)} {bs : Fin c.workTapeCount → Option (Fin c.alphabetSize)} : (c.actionAt q as bs).workActions.size = c.workTapeCount

theorem Turing.Code.actionAt_write_lt {i : ℕ} {c : Code i} {q : Fin c.stateCount} {as : Fin i → Option (Fin c.alphabetSize)} {bs : Fin c.workTapeCount → Option (Fin c.alphabetSize)} {wa : RawWorkAction} (hwa : wa ∈ (c.actionAt q as bs).workActions) {s : ℕ} (hs : wa.write = RawWrite.symbol s) : s < c.alphabetSize

theorem Turing.Code.actionAt_nextState_lt {i : ℕ} {c : Code i} {q : Fin c.stateCount} {as : Fin i → Option (Fin c.alphabetSize)} {bs : Fin c.workTapeCount → Option (Fin c.alphabetSize)} {q' : ℕ} (hq' : q' ∈ (c.actionAt q as bs).nextState) : q' < c.stateCount