Binary serialization of machine codes

The normative description format (planning/tm-infrastructure.md, Milestone C):

encodeCode c = encodeNat 0 (version) · workTapeCount · alphabetSize · stateCount · startState · table entries in transitionIndex order

with every natural in the self-delimiting code of MIPRE.TM.Code.Encoding.Nat, and per entry: the i input moves (stay = 0, right = 10, left = 11), the w work actions (write keep = 0, blank = 10, symbol s = 11·encodeNat s, then the move), the output (none = 0, some b = 1·b), and the successor (none = 0, some q = 1·encodeNat q). The arity i is external, matching the paper's [α]_i.

decodeCodeExact parses, demands full consumption, and gates on the executable well-formedness checker; the three theorems at the end are Milestone C's exact-codec package: decodeCodeExact_encodeCode (round trip), encodeCode_injective, and decodeCodeExact_sound (canonicality: every accepted string is the canonical encoding of its parse). Every parser is paired with a prefix lemma and a soundness lemma, so soundness composes field by field (decision D11); everything is structurally recursive (decision D10).

Field codecs

def Turing.encodeMove : Move → List Bool

Encode a head movement: stay = 0, right = 10, left = 11.

Equations

• Turing.encodeMove Turing.Move.stay = [false]
• Turing.encodeMove Turing.Move.right = [true, false]
• Turing.encodeMove Turing.Move.left = [true, true]

def Turing.parseMove : List Bool → Option (Move × List Bool)

Parse a head movement.

Equations

• Turing.parseMove (false :: r) = some (Turing.Move.stay, r)
• Turing.parseMove (true :: false :: r) = some (Turing.Move.right, r)
• Turing.parseMove (true :: true :: r) = some (Turing.Move.left, r)
• Turing.parseMove x✝ = none

@[simp]

theorem Turing.parseMove_encodeMove (m : Move) (rest : List Bool) : parseMove (encodeMove m ++ rest) = some (m, rest)

theorem Turing.parseMove_sound {s : List Bool} {m : Move} {rest : List Bool} : parseMove s = some (m, rest) → s = encodeMove m ++ rest

def Turing.encodeWrite : RawWrite → List Bool

Encode a write action: keep = 0, blank = 10, symbol s = 11·encodeNat s.

Equations

• Turing.encodeWrite Turing.RawWrite.keep = [false]
• Turing.encodeWrite Turing.RawWrite.blank = [true, false]
• Turing.encodeWrite (Turing.RawWrite.symbol s) = true :: true :: Turing.encodeNat s

def Turing.parseWrite : List Bool → Option (RawWrite × List Bool)

Parse a write action.

Equations

• Turing.parseWrite (false :: r) = some (Turing.RawWrite.keep, r)
• Turing.parseWrite (true :: false :: r) = some (Turing.RawWrite.blank, r)
• Turing.parseWrite (true :: true :: r) = match Turing.parseNat r with | some (s, r') => some (Turing.RawWrite.symbol s, r') | none => none
• Turing.parseWrite x✝ = none

@[simp]

theorem Turing.parseWrite_encodeWrite (w : RawWrite) (rest : List Bool) : parseWrite (encodeWrite w ++ rest) = some (w, rest)

theorem Turing.parseWrite_sound {s : List Bool} {w : RawWrite} {rest : List Bool} : parseWrite s = some (w, rest) → s = encodeWrite w ++ rest

def Turing.encodeOutput : Option Bool → List Bool

Encode an optional output bit: none = 0, some b = 1·b.

Equations

• Turing.encodeOutput none = [false]
• Turing.encodeOutput (some b) = [true, b]

def Turing.parseOutput : List Bool → Option (Option Bool × List Bool)

Parse an optional output bit.

Equations

• Turing.parseOutput (false :: r) = some (none, r)
• Turing.parseOutput (true :: b :: r) = some (some b, r)
• Turing.parseOutput x✝ = none

@[simp]

theorem Turing.parseOutput_encodeOutput (o : Option Bool) (rest : List Bool) : parseOutput (encodeOutput o ++ rest) = some (o, rest)

theorem Turing.parseOutput_sound {s : List Bool} {o : Option Bool} {rest : List Bool} : parseOutput s = some (o, rest) → s = encodeOutput o ++ rest

def Turing.encodeNextState : Option ℕ → List Bool

Encode an optional successor state: none = 0, some q = 1·encodeNat q.

Equations

• Turing.encodeNextState none = [false]
• Turing.encodeNextState (some q) = true :: Turing.encodeNat q

def Turing.parseNextState : List Bool → Option (Option ℕ × List Bool)

Parse an optional successor state.

Equations

• Turing.parseNextState (false :: r) = some (none, r)
• Turing.parseNextState (true :: r) = match Turing.parseNat r with | some (q, r') => some (some q, r') | none => none
• Turing.parseNextState x✝ = none

@[simp]

theorem Turing.parseNextState_encodeNextState (o : Option ℕ) (rest : List Bool) : parseNextState (encodeNextState o ++ rest) = some (o, rest)

theorem Turing.parseNextState_sound {s : List Bool} {o : Option ℕ} {rest : List Bool} : parseNextState s = some (o, rest) → s = encodeNextState o ++ rest

def Turing.encodeWorkAction (wa : RawWorkAction) : List Bool

Encode one work-tape action: the write, then the move.

Equations

• Turing.encodeWorkAction wa = Turing.encodeWrite wa.write ++ Turing.encodeMove wa.move

def Turing.parseWorkAction (s : List Bool) : Option (RawWorkAction × List Bool)

Parse one work-tape action.

Equations

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

@[simp]

theorem Turing.parseWorkAction_encodeWorkAction (wa : RawWorkAction) (rest : List Bool) : parseWorkAction (encodeWorkAction wa ++ rest) = some (wa, rest)

theorem Turing.parseWorkAction_sound {s : List Bool} {wa : RawWorkAction} {rest : List Bool} (h : parseWorkAction s = some (wa, rest)) : s = encodeWorkAction wa ++ rest

Fixed-count sequences

def Turing.encodeListWith {α : Type u_1} (enc : α → List Bool) (l : List α) : List Bool

Concatenate elementwise encodings; the element count is protocol context (the parser is told how many to read), not part of the string.

Equations

• Turing.encodeListWith enc l = List.flatMap enc l

@[simp]

theorem Turing.encodeListWith_nil {α : Type u_1} (enc : α → List Bool) : encodeListWith enc [] = []

@[simp]

theorem Turing.encodeListWith_cons {α : Type u_1} (enc : α → List Bool) (a : α) (l : List α) : encodeListWith enc (a :: l) = enc a ++ encodeListWith enc l

def Turing.parseCount {α : Type u_1} (p : List Bool → Option (α × List Bool)) : ℕ → List Bool → Option (List α × List Bool)

Parse exactly k elements.

Equations

• Turing.parseCount p 0 x✝ = some ([], x✝)
• Turing.parseCount p k.succ x✝ = match p x✝ with | some (a, s') => match Turing.parseCount p k s' with | some (l, s'') => some (a :: l, s'') | none => none | none => none

theorem Turing.parseCount_encodeListWith {α : Type u_1} {p : List Bool → Option (α × List Bool)} {enc : α → List Bool} (l : List α) (henc : ∀ a ∈ l, ∀ (rest : List Bool), p (enc a ++ rest) = some (a, rest)) (rest : List Bool) : parseCount p l.length (encodeListWith enc l ++ rest) = some (l, rest)

Prefix property for fixed-count sequences; the elementwise prefix property is only required on the members of the encoded list.

theorem Turing.parseCount_encodeListWith' {α : Type u_1} {p : List Bool → Option (α × List Bool)} {enc : α → List Bool} (henc : ∀ (a : α) (rest : List Bool), p (enc a ++ rest) = some (a, rest)) (l : List α) (rest : List Bool) : parseCount p l.length (encodeListWith enc l ++ rest) = some (l, rest)

Uniform-codec version of parseCount_encodeListWith.

theorem Turing.parseCount_sound {α : Type u_1} {p : List Bool → Option (α × List Bool)} {enc : α → List Bool} (hp : ∀ {s : List Bool} {a : α} {rest : List Bool}, p s = some (a, rest) → s = enc a ++ rest) {k : ℕ} {s : List Bool} {l : List α} {rest : List Bool} : parseCount p k s = some (l, rest) → s = encodeListWith enc l ++ rest ∧ l.length = k

Soundness for fixed-count sequences.

Actions

def Turing.encodeAction (a : RawAction) : List Bool

Encode one transition-table entry.

Equations

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

def Turing.parseAction (i w : ℕ) (s : List Bool) : Option (RawAction × List Bool)

Parse one transition-table entry of an i-input, w-work-tape machine.

Equations

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

@[simp]

theorem Turing.parseAction_encodeAction {i w : ℕ} (a : RawAction) (hmoves : a.inputMoves.size = i) (hworks : a.workActions.size = w) (rest : List Bool) : parseAction i w (encodeAction a ++ rest) = some (a, rest)

theorem Turing.parseAction_sound {i w : ℕ} {s : List Bool} {a : RawAction} {rest : List Bool} (h : parseAction i w s = some (a, rest)) : s = encodeAction a ++ rest ∧ a.inputMoves.size = i ∧ a.workActions.size = w

Machine codes

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

Encode a raw machine description (version 0, header, dense table in canonical order).

Equations

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

def Turing.encodeCode {i : ℕ} (c : Code i) : List Bool

The canonical binary description of a machine code — the paper's α.

Equations

• Turing.encodeCode c = Turing.encodeRawCode c.raw

def Turing.parseRawCode (i : ℕ) (s : List Bool) : Option (RawCode i × List Bool)

Parse a raw machine description: version, header, then exactly the canonical number of table entries.

Equations

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

def Turing.decodeCodeExact (i : ℕ) (s : List Bool) : Option (Code i)

Exact decoding: parse, demand full consumption, and check well-formedness.

Equations

• Turing.decodeCodeExact i s = match Turing.parseRawCode i s with | some (raw, []) => if h : raw.wellFormedB = true then some { raw := raw, wf := ⋯ } else none | x => none

theorem Turing.parseRawCode_encodeRawCode {i : ℕ} (c : RawCode i) (hwf : c.WellFormed) (rest : List Bool) : parseRawCode i (encodeRawCode c ++ rest) = some (c, rest)

Prefix property at the raw level (for well-formed codes, whose entries have the arities the parser expects).

theorem Turing.parseRawCode_sound {i : ℕ} {s : List Bool} {c : RawCode i} {rest : List Bool} (h : parseRawCode i s = some (c, rest)) : s = encodeRawCode c ++ rest

Soundness at the raw level: every accepted prefix is the canonical encoding.

@[simp]

theorem Turing.decodeCodeExact_encodeCode {i : ℕ} (c : Code i) : decodeCodeExact i (encodeCode c) = some c

Round trip: exact decoding inverts encoding.

theorem Turing.decodeCodeExact_sound {i : ℕ} {s : List Bool} {c : Code i} (h : decodeCodeExact i s = some c) : encodeCode c = s

Canonicality: every accepted description is exactly the canonical encoding of the code it parses to.

theorem Turing.encodeCode_injective {i : ℕ} : Function.Injective encodeCode

Canonical descriptions are unique.