Match-loop ↔ lookup correspondence (pure list level)

The body machine's key scan accepts a desc-tape segment exactly when the abstract table lookup (TMDesc.lookup) would select the entry parsed from that segment. This file proves the correspondence at the pure list level — no machine steps (design appendix 2):

• keyCells / keyCells_get — the six expected key-symbol cells of Body.keyCell, as a Γw list;
• MachMatch — the machine's segment-acceptance predicate (state-field prefix, six key cells, and full value length);
• machMatch_iff_parse — on a □-free segment, MachMatch holds iff the segment parses (parseEntry) with exactly the sought key;
• machFind + machFind_some_find? / machFind_none_find? / firstMatch_lookup / noMatch_lookup — the machine's first matching segment in the takeField split is the find? hit of parseEntries, so its action is exactly TMDesc.lookup's result (and no match ⟺ the default action);
• value_slices — the matched segment's value cells decode (via cellBit/grpΓw/grpDir, the machine's decoders) to the parsed entry's action fields.

theorem Complexity.TM.UTMBody.bitSym_toΓ (b : Bool) : (bitSym b).toΓ = bitCell b

bitSym and bitCell denote the same cell content.

theorem Complexity.TM.UTMBody.bitSym_injective : Function.Injective bitSym

bitSym is injective.

theorem Complexity.TM.UTMBody.bitsToSyms_injective : Function.Injective bitsToSyms

bitsToSyms is injective.

theorem Complexity.TM.UTMBody.bitsToSyms_take (l : List Bool) (n : ℕ) : bitsToSyms (List.take n l) = List.take n (bitsToSyms l)

bitsToSyms commutes with take.

theorem Complexity.TM.UTMBody.bitsToSyms_drop (l : List Bool) (n : ℕ) : bitsToSyms (List.drop n l) = List.drop n (bitsToSyms l)

bitsToSyms commutes with drop.

theorem Complexity.TM.UTMBody.filterMap_symBit?_eq_map_cellBit {l : List Γw} : (∀ s ∈ l, s ≠ Γw.blank) → List.filterMap symBit? l = List.map (fun (s : Γw) => cellBit s.toΓ) l

On a □-free list the (total) bit translation is the machine's cellBit read of each cell.

theorem Complexity.TM.UTMBody.eq_encode_of_decΓ_eq {l : List Bool} (hl : l.length = 2) {s : Γ} (h : decΓ l = s) : l = s.encode

A length-2 bit list is the encoding of the symbol it decΓ-decodes to (decΓ is a bijection on 2-bit patterns).

def Complexity.TM.UTMBody.keyCells (f : VFlags) (v0 v1 v2 : Γ) : List Γw

The six expected key-symbol cells of the scan (Body.keyCell), as a list: the bit symbols of the three simulated reads' encodings.

Equations

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

@[simp]

theorem Complexity.TM.UTMBody.keyCells_length (f : VFlags) (v0 v1 v2 : Γ) : (keyCells f v0 v1 v2).length = 6

theorem Complexity.TM.UTMBody.keyCells_map_toΓ (f : VFlags) (v0 v1 v2 : Γ) : List.map Γw.toΓ (keyCells f v0 v1 v2) = [keyCell f v0 v1 v2 0, keyCell f v0 v1 v2 1, keyCell f v0 v1 v2 2, keyCell f v0 v1 v2 3, keyCell f v0 v1 v2 4, keyCell f v0 v1 v2 5]

keyCells read as Γ cells is exactly keyCell 0 .. keyCell 5.

theorem Complexity.TM.UTMBody.keyCells_get (f : VFlags) (v0 v1 v2 : Γ) (idx : Fin 6) : (keyCells f v0 v1 v2)[↑idx].toΓ = keyCell f v0 v1 v2 idx

Pointwise form: cell idx of keyCells, read as Γ, is keyCell idx.

def Complexity.TM.UTMBody.MachMatch (w : ℕ) (stSyms keyCs seg : List Γw) : Prop

The machine's segment-acceptance predicate: the segment starts with the state-tape symbols (cmpQ's lockstep compare), followed by the six expected key cells (cmpS), and is long enough for the full value copy (copyQ'/copyAct find no early □ — on the □-free segments takeField produces, length is exactly that condition).

Equations

• Complexity.TM.UTMBody.MachMatch w stSyms keyCs seg = (List.take w seg = stSyms ∧ List.take 6 (List.drop w seg) = keyCs ∧ 2 * w + 16 ≤ seg.length)

@[implicit_reducible]

instance Complexity.TM.UTMBody.instDecidableMachMatch (w : ℕ) (stSyms keyCs seg : List Γw) : Decidable (MachMatch w stSyms keyCs seg)

Equations

• Complexity.TM.UTMBody.instDecidableMachMatch w stSyms keyCs seg = id inferInstance

theorem Complexity.TM.UTMBody.machMatch_iff_parse {w q : ℕ} (hq : q < 2 ^ w) (f : VFlags) (v0 v1 v2 : Γ) {seg : List Γw} (hnb : ∀ s ∈ seg, s ≠ Γw.blank) : MachMatch w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) seg ↔ ∃ (e : DescEntry), parseEntry w seg = some e ∧ e.q = q ∧ e.si = simRead f.1 v0 ∧ e.sw = simRead f.2.1 v1 ∧ e.so = simRead f.2.2 v2

The parse bridge: on a □-free segment, the machine's acceptance predicate (state field = the w-bit encoding of q, six key cells = keyCells of the simulated reads, full value length) holds iff the segment parses to an entry whose key is exactly (q, simRead …).

@[irreducible]

def Complexity.TM.UTMBody.machFind (w : ℕ) (stSyms keyCs : List Γw) : List Γw → Option (List Γw)

The machine's segment walk at the list level: the first segment of the takeField split that satisfies MachMatch, stopping (like parseEntries) at the first empty segment.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.UTMBody.machFind w stSyms keyCs [] = none
• Complexity.TM.UTMBody.machFind w stSyms keyCs (Complexity.Γw.blank :: tail) = none

theorem Complexity.TM.UTMBody.machFind_cons_of_ne_blank {s : Γw} (hs : s ≠ Γw.blank) (w : ℕ) (stSyms keyCs rest : List Γw) : machFind w stSyms keyCs (s :: rest) = if MachMatch w stSyms keyCs (takeField (s :: rest)).1 then some (takeField (s :: rest)).1 else machFind w stSyms keyCs (takeField (s :: rest)).2

One-step unfolding of machFind on a segment-headed input.

theorem Complexity.TM.UTMBody.machFind_matches (w : ℕ) (stSyms keyCs R seg : List Γw) : machFind w stSyms keyCs R = some seg → MachMatch w stSyms keyCs seg ∧ ∀ s ∈ seg, s ≠ Γw.blank

What machFind returns is a □-free segment that MachMatches.

def Complexity.TM.UTMBody.keyMatch (q : ℕ) (si sw so : Γ) (e : DescEntry) : Bool

The key predicate of TMDesc.lookup's find?.

Equations

• Complexity.TM.UTMBody.keyMatch q si sw so e = (e.q == q && e.si == si && e.sw == sw && e.so == so)

theorem Complexity.TM.UTMBody.lookup_eq_find? (d : TMDesc) (q : ℕ) (si sw so : Γ) : d.lookup q si sw so = match List.find? (keyMatch q si sw so) d.entries with | some e => e.act | none => d.defaultAct sw so

TMDesc.lookup in terms of keyMatch.

theorem Complexity.TM.UTMBody.find?_parseEntries_eq_machFind (w q : ℕ) (hq : q < 2 ^ w) (f : VFlags) (v0 v1 v2 : Γ) (R : List Γw) : List.find? (keyMatch q (simRead f.1 v0) (simRead f.2.1 v1) (simRead f.2.2 v2)) (parseEntries w R) = (machFind w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) R).bind (parseEntry w)

The first-match correspondence, combined form: the find? hit of the parsed table is exactly the parse of the machine's first MachMatch-ing segment.

theorem Complexity.TM.UTMBody.machFind_some_find? {w q : ℕ} (hq : q < 2 ^ w) (f : VFlags) (v0 v1 v2 : Γ) {R seg : List Γw} (h : machFind w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) R = some seg) : ∃ (e : DescEntry), parseEntry w seg = some e ∧ List.find? (keyMatch q (simRead f.1 v0) (simRead f.2.1 v1) (simRead f.2.2 v2)) (parseEntries w R) = some e ∧ MachMatch w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) seg

(a) The machine's first hit is the lookup's first hit: if the machine's segment walk accepts seg, then seg parses to an entry e, and e is exactly the table's find? hit for the sought key.

theorem Complexity.TM.UTMBody.machFind_none_find? {w q : ℕ} (hq : q < 2 ^ w) (f : VFlags) (v0 v1 v2 : Γ) {R : List Γw} (h : machFind w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) R = none) : List.find? (keyMatch q (simRead f.1 v0) (simRead f.2.1 v1) (simRead f.2.2 v2)) (parseEntries w R) = none

(b) No machine hit ⟺ no lookup hit: if the machine's segment walk rejects every segment, the table's find? misses.

theorem Complexity.TM.UTMBody.firstMatch_lookup {w q : ℕ} (hq : q < 2 ^ w) (f : VFlags) (v0 v1 v2 : Γ) (qs qh : ℕ) {R seg : List Γw} (h : machFind w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) R = some seg) : ∃ (e : DescEntry), parseEntry w seg = some e ∧ MachMatch w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) seg ∧ { w := w, qstart := qs, qhalt := qh, entries := parseEntries w R }.lookup q (simRead f.1 v0) (simRead f.2.1 v1) (simRead f.2.2 v2) = e.act

First-match ⇒ lookup: the action of the entry parsed from the machine's first MachMatch-ing segment is exactly what TMDesc.lookup returns on the table parsed from the same entry region.

theorem Complexity.TM.UTMBody.noMatch_lookup {w q : ℕ} (hq : q < 2 ^ w) (f : VFlags) (v0 v1 v2 : Γ) (qs qh : ℕ) {R : List Γw} (h : machFind w (bitsToSyms (w.toBits q)) (keyCells f v0 v1 v2) R = none) : { w := w, qstart := qs, qhalt := qh, entries := parseEntries w R }.lookup q (simRead f.1 v0) (simRead f.2.1 v1) (simRead f.2.2 v2) = { w := w, qstart := qs, qhalt := qh, entries := parseEntries w R }.defaultAct (simRead f.2.1 v1) (simRead f.2.2 v2)

No match ⇒ default: if the machine's segment walk rejects every segment, TMDesc.lookup on the parsed table falls to the default action.

def Complexity.TM.UTMBody.segBit (seg : List Γw) (i : ℕ) : Bool

The bit value the machine decodes from desc-segment cell i (out-of-range reads default to □, i.e. false; the machine reads the cell as Γ and applies cellBit).

Equations

• Complexity.TM.UTMBody.segBit seg i = Complexity.TM.UTMBody.cellBit (seg.getD i Complexity.Γw.blank).toΓ

theorem Complexity.TM.UTMBody.segBit_eq {seg : List Γw} {i : ℕ} (h : i < seg.length) : segBit seg i = cellBit seg[i].toΓ

In range, segBit is the cellBit read of the cell.

theorem Complexity.TM.UTMBody.value_slices {w : ℕ} {seg : List Γw} {e : DescEntry} (hnb : ∀ s ∈ seg, s ≠ Γw.blank) (hp : parseEntry w seg = some e) : List.take w (List.drop (w + 6) seg) = bitsToSyms (w.toBits e.act.q') ∧ grpΓw (segBit seg (2 * w + 6)) (segBit seg (2 * w + 7)) = e.act.ww ∧ grpΓw (segBit seg (2 * w + 8)) (segBit seg (2 * w + 9)) = e.act.wo ∧ grpDir (segBit seg (2 * w + 10)) (segBit seg (2 * w + 11)) = e.act.di ∧ grpDir (segBit seg (2 * w + 12)) (segBit seg (2 * w + 13)) = e.act.dw ∧ grpDir (segBit seg (2 * w + 14)) (segBit seg (2 * w + 15)) = e.act.dOut

The value decode bridge: on a □-free segment that parses to e, the value cells decode to e.act exactly as the machine reads them — the w-cell state field at offset w+6 is the bit-symbol encoding of e.act.q', and the five 2-cell groups at offsets 2w+6 .. 2w+14 decode via grpΓw/grpDir of the cellBit cell reads to ww/wo/di/dw/dOut.