Fixed-width bit layouts

⚠️ Unreviewed by Bolton

A machine that searches the configuration space of another machine has to hold configurations in registers and step a counter through all of them. Both want the same thing: a fixed-width bit layout, so that a register is a fixed number of cells and the enumeration is one binary counter.

Complexity.BitCodec is that layout, packaged so it can be built up field by field. Each codec carries its width, an encoder, a decoder that is total on every bitstring, and the two facts a caller needs: the encoding has the declared width, and decoding inverts it. The combinators — Complexity.BitCodec.prod, Complexity.BitCodec.fn, Complexity.BitCodec.equiv — discharge those obligations once, so a record layout is assembled rather than proved.

The decoder being total matters. The machine enumerates all bitstrings of the layout's width, not just the ones in the image, so every register value must denote something; the ones outside the image simply denote a configuration that no walk ever reaches.

So does where the head positions go. A machine reads a register by scanning it, so a head stored as a number in its own field would be useless — to check the cell it points at, the scan would have to turn around. Complexity.tapeCodec therefore stores the head as a marker beside each cell: the scan learns at every cell whether the head is there, which is what makes a Complexity.Scanner able to check a transition of the simulated machine without ever counting.

Main definitions

• Complexity.BitCodec — a fixed-width bit layout
• Complexity.BitCodec.fin, .gamma, .bool, .prod, .fn, .equiv — the combinators
• Complexity.tapeCodec — a tape window, with the head marked beside the cell it is on
• Complexity.codeCodec — the layout of a configuration code

Main results

• Complexity.BitCodec.enc_injective — a layout distinguishes what it encodes
• Complexity.codeCodec_width — the width of a configuration code

structure Complexity.BitCodec (α : Type) : Type

A fixed-width bit layout for α: an encoder of constant width, and a decoder that is total on every bitstring and inverts it.

• width : ℕ

  The number of bits an encoded value occupies.

• enc : α → List Bool

  The encoder.

• dec : List Bool → α

  The decoder, total on every bitstring.

• enc_length (a : α) : (self.enc a).length = self.width

  Encodings have the declared width.

• dec_enc (a : α) : self.dec (self.enc a) = a

  Decoding inverts encoding.

theorem Complexity.BitCodec.enc_injective {α : Type} (c : BitCodec α) : Function.Injective c.enc

Leaves

def Complexity.BitCodec.fin (m w : ℕ) [NeZero m] (h : m ≤ 2 ^ w) : BitCodec (Fin m)

A bounded index, little-endian in w bits.

Equations

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

def Complexity.BitCodec.gamma : BitCodec Γ

A tape symbol, in two bits.

Equations

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

def Complexity.BitCodec.bool : BitCodec Bool

A single bit.

Equations

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

Reading a value out of a scan

A scan puts a register's leading bits into a table (Complexity.Scanner.bitsStep). This reads the value they encode back out, which is how a check recovers, say, the simulated machine's state from the parameters it was handed.

def Complexity.BitCodec.ofTable {α : Type} (c : BitCodec α) (f : Fin c.width → Bool) : α

The value a table of bits encodes.

Equations

• c.ofTable f = c.dec (List.ofFn f)

theorem Complexity.BitCodec.ofTable_eq {α : Type} (c : BitCodec α) (a : α) (f : Fin c.width → Bool) (h : ∀ (i : Fin c.width), f i = (c.enc a)[↑i]) : c.ofTable f = a

Combinators

def Complexity.BitCodec.prod {α β : Type} (c : BitCodec α) (d : BitCodec β) : BitCodec (α × β)

Two layouts side by side.

Equations

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

def Complexity.BitCodec.equiv {α β : Type} (e : α ≃ β) (c : BitCodec β) : BitCodec α

Transport a layout along an equivalence.

Equations

• Complexity.BitCodec.equiv e c = { width := c.width, enc := fun (a : α) => c.enc (e a), dec := fun (l : List Bool) => e.symm (c.dec l), enc_length := ⋯, dec_enc := ⋯ }

theorem Complexity.BitCodec.take_drop_flatten {α : Type} (w : ℕ) (L : List (List α)) : (∀ l ∈ L, l.length = w) → ∀ (i : ℕ) (hi : i < L.length), List.take w (List.drop (i * w) L.flatten) = L[i]

The i-th fixed-width chunk of a concatenation.

def Complexity.BitCodec.fn {α : Type} (m : ℕ) (c : BitCodec α) : BitCodec (Fin m → α)

A fixed number of copies of a layout, side by side.

Equations

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

The layout of a configuration code

def Complexity.bitWidth (m : ℕ) : ℕ

Bits enough to index m values.

Equations

• Complexity.bitWidth m = Nat.clog 2 m

theorem Complexity.le_two_pow_bitWidth (m : ℕ) : m ≤ 2 ^ bitWidth m

def Complexity.finCodec (m : ℕ) [NeZero m] : BitCodec (Fin m)

The layout of a bounded index.

Equations

• Complexity.finCodec m = Complexity.BitCodec.fin m (Complexity.bitWidth m) ⋯

@[simp]

theorem Complexity.finCodec_width (m : ℕ) [NeZero m] : (finCodec m).width = bitWidth m

noncomputable def Complexity.qCodec (Q : Type) [Fintype Q] [Nonempty Q] : BitCodec Q

The layout of a machine state.

Equations

• Complexity.qCodec Q = Complexity.BitCodec.equiv (Fintype.equivFin Q) (Complexity.finCodec (Fintype.card Q))

Marking a head position where the scan will meet it

A machine reads a register by scanning it, so a head position stored as a number in its own field is useless: to check the cell it points at, the scan would have to come back. Storing it as a marker beside each cell makes the head local — the scan learns, at each cell, whether the head is there.

def Complexity.markIdx {m : ℕ} (f : Fin m → Bool × Γ) : ℕ

Where the marker sits, or 0 if there is none.

Equations

• Complexity.markIdx f = Complexity.NTM.searchIdx (fun (q : ℕ) => if h : q < m then (f ⟨q, h⟩).1 else false) m

def Complexity.mark {m : ℕ} (p : Fin m × (Fin m → Γ)) : Fin m → Bool × Γ

Mark the cell the head is on. The marker comes first in the chunk, so that a scan knows whether the head is on a cell before it reads that cell's symbol.

Equations

• Complexity.mark p i = (decide (i = p.1), p.2 i)

def Complexity.unmark {m : ℕ} [NeZero m] (f : Fin m → Bool × Γ) : Fin m × (Fin m → Γ)

Read the head position back off the markers. Total: with no marker, or several, it reads the head as sitting at the first cell.

Equations

• Complexity.unmark f = (⟨min (Complexity.markIdx f) (m - 1), ⋯⟩, fun (i : Fin m) => (f i).2)

theorem Complexity.markIdx_mark {m : ℕ} (p : Fin m × (Fin m → Γ)) : markIdx (mark p) = ↑p.1

@[simp]

theorem Complexity.unmark_mark {m : ℕ} [NeZero m] (p : Fin m × (Fin m → Γ)) : unmark (mark p) = p

def Complexity.gammaBits : Γ → Bool × Bool

The two bits a symbol occupies.

Equations

• Complexity.gammaBits Complexity.Γ.zero = (false, false)
• Complexity.gammaBits Complexity.Γ.one = (true, false)
• Complexity.gammaBits Complexity.Γ.blank = (false, true)
• Complexity.gammaBits Complexity.Γ.start = (true, true)

theorem Complexity.gamma_enc_eq (g : Γ) : BitCodec.gamma.enc g = [(gammaBits g).1, (gammaBits g).2]

def Complexity.tapeCodec (m : ℕ) [NeZero m] : BitCodec (Fin m × (Fin m → Γ))

The layout of one work tape's window: each cell beside a bit saying whether the head is on it.

Equations

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

theorem Complexity.tapeCodec_enc_chunk {m : ℕ} [NeZero m] (hd : Fin m) (cl : Fin m → Γ) (p : Fin m) : List.take 3 (List.drop (↑p * 3) ((tapeCodec m).enc (hd, cl))) = [decide (p = hd), (gammaBits (cl p)).1, (gammaBits (cl p)).2]

One chunk of an encoded window: the head marker, then the cell's two symbol bits.

noncomputable def Complexity.codeCodec (Q : Type) [Fintype Q] [Nonempty Q] (k nn S : ℕ) : BitCodec (Code Q k nn S)

The layout of a configuration code.

Equations

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

theorem Complexity.codeCodec_width (Q : Type) [Fintype Q] [Nonempty Q] (k nn S : ℕ) : (codeCodec Q k nn S).width = bitWidth (Fintype.card Q) + (bitWidth (nn + S + 2) + (k * ((S + 1) * 3) + (S + 2) * 3))

The width of a configuration code: a constant for the state, a pointer into the input, and the window itself.

The layout is logarithmically wide

theorem Complexity.bitWidth_le {m w : ℕ} (h : m ≤ 2 ^ w) : bitWidth m ≤ w

theorem Complexity.bitWidth_le_self (m : ℕ) : bitWidth m ≤ m

theorem Complexity.codeCodec_width_le (Q : Type) [Fintype Q] [Nonempty Q] (k C D : ℕ) : ∃ (C' : ℕ) (D' : ℕ), ∀ (nn : ℕ), (codeCodec Q k nn (logWindow C D nn)).width ≤ logWindow C' D' nn

A configuration code is logarithmically wide. Every field is either a constant, a pointer into the input, or a piece of the window, so the whole layout fits in a logarithmic window of its own — which is what lets a machine hold two of them at once and still be a log-space machine.

Combining logarithmic bounds

The machine's space is the largest of its registers, and each register has its own logarithmic bound; these say the family is closed under the operations the accounting needs.

theorem Complexity.logWindow_mono {C C' D D' : ℕ} (hC : C ≤ C') (hD : D ≤ D') (n : ℕ) : logWindow C D n ≤ logWindow C' D' n

theorem Complexity.logWindow_add (C₁ D₁ C₂ D₂ n : ℕ) : logWindow C₁ D₁ n + logWindow C₂ D₂ n = logWindow (C₁ + C₂) (D₁ + D₂) n

theorem Complexity.logWindow_mul (a C D n : ℕ) : a * logWindow C D n = logWindow (a * C) (a * D) n

theorem Complexity.max_logWindow_le (C₁ D₁ C₂ D₂ n : ℕ) : max (logWindow C₁ D₁ n) (logWindow C₂ D₂ n) ≤ logWindow (max C₁ C₂) (max D₁ D₂) n

theorem Complexity.bitWidth_poly_le (A B n : ℕ) : bitWidth (A * (n + 1) ^ B + 1) ≤ logWindow B (A + B + 1) n

A polynomial counter is logarithmically wide. The search counts rounds and codes up to A * (n + 1) ^ B, so its counters fit in a logarithmic number of cells — which is what keeps the whole machine inside a logarithmic window.