The variable format of the describer

The binary format of the variables of the Cook–Levin tableau of the interpreter machine U (planning/succinct-cook-levin.md, S3). An index is a list of m bits, least significant first. With its top bit set it is structured: a tag (3 bits), the time t (W bits), the tape d (4), the position p (W), the cell value v (3), the state q (Qb), the thirteen window centers (13 W) and the gate g (Gb); tags 0..6 are cell, head, state, emitOne, emitBad, emitted, aux. With its top bit clear and value j < 4T it is an answer variable: the cell at position j' / 2 + 3 of tape A (for j < 2T, j' = j) or B (j' = j - 2T), with the value blank for j' even and 1 for j' odd, so that the first 4T variables are the tapeBits of the two answers.

fieldsOf reads the fields of an index, decodeVar the tableau variable they denote (if any), and encodeVar is the structured index of a variable; decodeVar_encodeVar is the round trip. The circuit computes exactly fieldsOf on its input bits (FieldFml.lean).

Codes of symbols, tapes and states

def MIPRE.TM.CookLevin.Desc.symCode : CellVal Interp.Sym → ℕ

The code of a cell value.

Equations

• MIPRE.TM.CookLevin.Desc.symCode (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.zero) = 0
• MIPRE.TM.CookLevin.Desc.symCode (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.one) = 1
• MIPRE.TM.CookLevin.Desc.symCode (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.sep) = 2
• MIPRE.TM.CookLevin.Desc.symCode (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.fr) = 3
• MIPRE.TM.CookLevin.Desc.symCode (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.en) = 4
• MIPRE.TM.CookLevin.Desc.symCode MIPRE.TM.CookLevin.CellVal.blank = 5
• MIPRE.TM.CookLevin.Desc.symCode MIPRE.TM.CookLevin.CellVal.bdry = 6

def MIPRE.TM.CookLevin.Desc.symOfCode : ℕ → Option (CellVal Interp.Sym)

The cell value of a code.

Equations

• MIPRE.TM.CookLevin.Desc.symOfCode 0 = some (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.zero)
• MIPRE.TM.CookLevin.Desc.symOfCode 1 = some (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.one)
• MIPRE.TM.CookLevin.Desc.symOfCode 2 = some (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.sep)
• MIPRE.TM.CookLevin.Desc.symOfCode 3 = some (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.fr)
• MIPRE.TM.CookLevin.Desc.symOfCode 4 = some (MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.en)
• MIPRE.TM.CookLevin.Desc.symOfCode 5 = some MIPRE.TM.CookLevin.CellVal.blank
• MIPRE.TM.CookLevin.Desc.symOfCode 6 = some MIPRE.TM.CookLevin.CellVal.bdry
• MIPRE.TM.CookLevin.Desc.symOfCode x✝ = none

theorem MIPRE.TM.CookLevin.Desc.symOfCode_symCode (v : CellVal Interp.Sym) : symOfCode (symCode v) = some v

theorem MIPRE.TM.CookLevin.Desc.symCode_lt (v : CellVal Interp.Sym) : symCode v < 7

theorem MIPRE.TM.CookLevin.Desc.symOfCode_eq_some {k : ℕ} {v : CellVal Interp.Sym} (h : symOfCode k = some v) : symCode v = k

def MIPRE.TM.CookLevin.Desc.tapeCode : Tape 7 6 → ℕ

The code of a tape: the input tapes 0..6, the work tapes 7..12.

Equations

• MIPRE.TM.CookLevin.Desc.tapeCode (Sum.inl j) = ↑j
• MIPRE.TM.CookLevin.Desc.tapeCode (Sum.inr j) = 7 + ↑j

def MIPRE.TM.CookLevin.Desc.tapeOfCode (d : ℕ) : Option (Tape 7 6)

The tape of a code.

Equations

• MIPRE.TM.CookLevin.Desc.tapeOfCode d = if h : d < 7 then some (Sum.inl ⟨d, h⟩) else if h' : d < 13 then some (Sum.inr ⟨d - 7, ⋯⟩) else none

theorem MIPRE.TM.CookLevin.Desc.tapeOfCode_tapeCode (d : Tape 7 6) : tapeOfCode (tapeCode d) = some d

theorem MIPRE.TM.CookLevin.Desc.tapeCode_lt (d : Tape 7 6) : tapeCode d < 13

theorem MIPRE.TM.CookLevin.Desc.tapeOfCode_eq_some {k : ℕ} {d : Tape 7 6} (h : tapeOfCode k = some d) : tapeCode d = k

@[irreducible]

def MIPRE.TM.CookLevin.Desc.QC : ℕ

The number of states, including the halting state. Irreducible: a definitional unfolding evaluates Fintype.card (Option Ctl), which does not terminate in practice.

noncomputable def MIPRE.TM.CookLevin.Desc.qCode (q : Option Interp.Ctl) : ℕ

The code of a state.

Equations

• MIPRE.TM.CookLevin.Desc.qCode q = ↑((Fintype.equivFin (Option MIPRE.TM.Interp.Ctl)) q)

noncomputable def MIPRE.TM.CookLevin.Desc.qOfCode (k : ℕ) : Option (Option Interp.Ctl)

The state of a code.

Equations

• MIPRE.TM.CookLevin.Desc.qOfCode k = if h : k < MIPRE.TM.CookLevin.Desc.QC then some ((Fintype.equivFin (Option MIPRE.TM.Interp.Ctl)).symm ⟨k, h⟩) else none

theorem MIPRE.TM.CookLevin.Desc.qOfCode_qCode (q : Option Interp.Ctl) : qOfCode (qCode q) = some q

theorem MIPRE.TM.CookLevin.Desc.qCode_lt (q : Option Interp.Ctl) : qCode q < QC

theorem MIPRE.TM.CookLevin.Desc.qOfCode_eq_some {k : ℕ} {q : Option Interp.Ctl} (h : qOfCode k = some q) : qCode q = k

Widths and offsets

@[irreducible]

def MIPRE.TM.CookLevin.Desc.Qb : ℕ

The width of the state field.

Equations

• MIPRE.TM.CookLevin.Desc.Qb = MIPRE.TM.CookLevin.Desc.QC.size

theorem MIPRE.TM.CookLevin.Desc.QC_lt_two_pow_Qb : QC < 2 ^ Qb

def MIPRE.TM.CookLevin.Desc.W (e : ℕ) : ℕ

The width of the time, position and center fields: W = e + 4, where S = 2^e.

Equations

• MIPRE.TM.CookLevin.Desc.W e = e + 4

def MIPRE.TM.CookLevin.Desc.Sof (e : ℕ) : ℕ

The tableau length.

Equations

• MIPRE.TM.CookLevin.Desc.Sof e = 2 ^ e

def MIPRE.TM.CookLevin.Desc.Gb (G : ℕ) : ℕ

The width of the gate field for a check circuit of G gates.

Equations

• MIPRE.TM.CookLevin.Desc.Gb G = G.size

theorem MIPRE.TM.CookLevin.Desc.G_lt_two_pow_Gb (G : ℕ) : G < 2 ^ Gb G

def MIPRE.TM.CookLevin.Desc.tagOff : ℕ

The offsets of the fields of a structured index.

Equations

• MIPRE.TM.CookLevin.Desc.tagOff = 0

def MIPRE.TM.CookLevin.Desc.tOff : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.tOff = 3

def MIPRE.TM.CookLevin.Desc.dOff (e : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.dOff e = 3 + MIPRE.TM.CookLevin.Desc.W e

def MIPRE.TM.CookLevin.Desc.pOff (e : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.pOff e = 7 + MIPRE.TM.CookLevin.Desc.W e

def MIPRE.TM.CookLevin.Desc.vOff (e : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.vOff e = 7 + 2 * MIPRE.TM.CookLevin.Desc.W e

def MIPRE.TM.CookLevin.Desc.qOff (e : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.qOff e = 10 + 2 * MIPRE.TM.CookLevin.Desc.W e

def MIPRE.TM.CookLevin.Desc.jsOff (e d : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.jsOff e d = 10 + 2 * MIPRE.TM.CookLevin.Desc.W e + MIPRE.TM.CookLevin.Desc.Qb + d * MIPRE.TM.CookLevin.Desc.W e

def MIPRE.TM.CookLevin.Desc.gOff (e : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.gOff e = 10 + 15 * MIPRE.TM.CookLevin.Desc.W e + MIPRE.TM.CookLevin.Desc.Qb

def MIPRE.TM.CookLevin.Desc.flagOff (e G : ℕ) : ℕ

Equations

• MIPRE.TM.CookLevin.Desc.flagOff e G = 10 + 15 * MIPRE.TM.CookLevin.Desc.W e + MIPRE.TM.CookLevin.Desc.Qb + MIPRE.TM.CookLevin.Desc.Gb G

def MIPRE.TM.CookLevin.Desc.mOf (e G : ℕ) : ℕ

The index width.

Equations

• MIPRE.TM.CookLevin.Desc.mOf e G = 11 + 15 * MIPRE.TM.CookLevin.Desc.W e + MIPRE.TM.CookLevin.Desc.Qb + MIPRE.TM.CookLevin.Desc.Gb G

theorem MIPRE.TM.CookLevin.Desc.flagOff_eq (e G : ℕ) : flagOff e G = mOf e G - 1

Bit strings and numbers

theorem MIPRE.TM.CookLevin.Desc.bitsOfNat_zero (i : ℕ) : SAT.bitsOfNat 0 i = []

theorem MIPRE.TM.CookLevin.Desc.bitsOfNat_succ (m i : ℕ) : SAT.bitsOfNat (m + 1) i = decide (i % 2 = 1) :: SAT.bitsOfNat m (i / 2)

theorem MIPRE.TM.CookLevin.Desc.bitsVal_bitsOfNat (m i : ℕ) : Cost.bitsVal (SAT.bitsOfNat m i) = i % 2 ^ m

theorem MIPRE.TM.CookLevin.Desc.bitsOfNat_bitsVal (l : Cost.BitStr) : SAT.bitsOfNat (List.length l) (Cost.bitsVal l) = l

def MIPRE.TM.CookLevin.Desc.bitField (ib : Cost.BitStr) (off w : ℕ) : ℕ

The value of the bits off .. off + w of a bit string.

Equations

• MIPRE.TM.CookLevin.Desc.bitField ib off w = MIPRE.Cost.bitsVal (List.take w (List.drop off ib))

The fields of an index

structure MIPRE.TM.CookLevin.Desc.Fields : Type

The fields read from an index: the top bit, the structured fields, and for an answer index the decoded tape, position and value with the range check ansOk.

• flag : Bool
• tag : ℕ
• t : ℕ
• d : ℕ
• p : ℕ
• v : ℕ
• q : ℕ
• js : Fin 13 → ℕ
• g : ℕ
• ansOk : Bool

def MIPRE.TM.CookLevin.Desc.fieldsOf (e G T : ℕ) (ib : Cost.BitStr) : Fields

The fields of the index ib (a bit string of length m), for the answer length T.

Equations

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

Decoding

noncomputable def MIPRE.TM.CookLevin.Desc.decodeVar (e G : ℕ) (F : Fields) : Option (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G)

The tableau variable denoted by the fields of an index, if any.

Equations

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

Encoding

def MIPRE.TM.CookLevin.Desc.nbits (w n : ℕ) : Cost.BitStr

The w-bit binary representation of n, least significant bit first.

Equations

• MIPRE.TM.CookLevin.Desc.nbits w n = MIPRE.SAT.bitsOfNat w n

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_nbits (w n : ℕ) : List.length (nbits w n) = w

theorem MIPRE.TM.CookLevin.Desc.bitsVal_nbits (w n : ℕ) : Cost.bitsVal (nbits w n) = n % 2 ^ w

theorem MIPRE.TM.CookLevin.Desc.bitsVal_nbits_of_lt {w n : ℕ} (h : n < 2 ^ w) : Cost.bitsVal (nbits w n) = n

def MIPRE.TM.CookLevin.Desc.jsPack (w : ℕ) (js : ℕ → ℕ) : ℕ → ℕ → Cost.BitStr

The w-bit fields js a, …, js (a + n - 1), concatenated.

Equations

• MIPRE.TM.CookLevin.Desc.jsPack w js x✝ 0 = []
• MIPRE.TM.CookLevin.Desc.jsPack w js x✝ n.succ = MIPRE.TM.CookLevin.Desc.nbits w (js x✝) ++ MIPRE.TM.CookLevin.Desc.jsPack w js (x✝ + 1) n

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_jsPack (w : ℕ) (js : ℕ → ℕ) (a n : ℕ) : List.length (jsPack w js a n) = n * w

theorem MIPRE.TM.CookLevin.Desc.jsPack_add (w : ℕ) (js : ℕ → ℕ) (a n k : ℕ) : jsPack w js a (n + k) = jsPack w js a n ++ jsPack w js (a + n) k

def MIPRE.TM.CookLevin.Desc.packFields (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : Cost.BitStr

The structured index with the given fields.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.length_packFields (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : List.length (packFields e G tag t d p v q js g) = mOf e G

theorem MIPRE.TM.CookLevin.Desc.bitField_of_eq (ib pre mid post : Cost.BitStr) (off w : ℕ) (h : ib = pre ++ (mid ++ post)) (hoff : List.length pre = off) (hw : List.length mid = w) : bitField ib off w = Cost.bitsVal mid

Reading a field out of a concatenation.

theorem MIPRE.TM.CookLevin.Desc.getD_of_eq (ib pre post : Cost.BitStr) (b : Bool) (off : ℕ) (h : ib = pre ++ b :: post) (hoff : List.length pre = off) : List.getD ib off false = b

theorem MIPRE.TM.CookLevin.Desc.packFields_flag (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : List.getD (packFields e G tag t d p v q js g) (flagOff e G) false = true

theorem MIPRE.TM.CookLevin.Desc.packFields_tag (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) tagOff 3 = tag % 2 ^ 3

theorem MIPRE.TM.CookLevin.Desc.packFields_t (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) tOff (W e) = t % 2 ^ W e

theorem MIPRE.TM.CookLevin.Desc.packFields_d (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) (dOff e) 4 = d % 2 ^ 4

theorem MIPRE.TM.CookLevin.Desc.packFields_p (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) (pOff e) (W e) = p % 2 ^ W e

theorem MIPRE.TM.CookLevin.Desc.packFields_v (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) (vOff e) 3 = v % 2 ^ 3

theorem MIPRE.TM.CookLevin.Desc.packFields_q (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) (qOff e) Qb = q % 2 ^ Qb

theorem MIPRE.TM.CookLevin.Desc.packFields_js (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g k : ℕ) (hk : k < 13) : bitField (packFields e G tag t d p v q js g) (jsOff e k) (W e) = js k % 2 ^ W e

theorem MIPRE.TM.CookLevin.Desc.packFields_g (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g : ℕ) : bitField (packFields e G tag t d p v q js g) (gOff e) (Gb G) = g % 2 ^ Gb G

theorem MIPRE.TM.CookLevin.Desc.fieldsOf_packFields (e G tag t d p v q : ℕ) (js : ℕ → ℕ) (g T : ℕ) : fieldsOf e G T (packFields e G tag t d p v q js g) = { flag := true, tag := tag % 2 ^ 3, t := t % 2 ^ W e, d := d % 2 ^ 4, p := p % 2 ^ W e, v := v % 2 ^ 3, q := q % 2 ^ Qb, js := fun (k : Fin 13) => js ↑k % 2 ^ W e, g := g % 2 ^ Gb G, ansOk := false }

The fields of a structured index are the packed values (reduced modulo their widths).

def MIPRE.TM.CookLevin.Desc.jsFun (e : ℕ) (js : Tape 7 6 → Center (Sof e)) (k : ℕ) : ℕ

The window centers of an aux variable as a function on tape codes.

Equations

• MIPRE.TM.CookLevin.Desc.jsFun e js k = match MIPRE.TM.CookLevin.Desc.tapeOfCode k with | some d => ↑(js d) | none => 0

theorem MIPRE.TM.CookLevin.Desc.jsFun_tapeCode (e : ℕ) (js : Tape 7 6 → Center (Sof e)) (d : Tape 7 6) : jsFun e js (tapeCode d) = ↑(js d)

noncomputable def MIPRE.TM.CookLevin.Desc.encodeVar (e G : ℕ) : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G → Cost.BitStr

The structured index of a tableau variable.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.head t d p) = MIPRE.TM.CookLevin.Desc.packFields e G 1 (↑t) (MIPRE.TM.CookLevin.Desc.tapeCode d) (↑p) 0 0 (fun (x : ℕ) => 0) 0
• MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.state t q) = MIPRE.TM.CookLevin.Desc.packFields e G 2 (↑t) 0 0 0 (MIPRE.TM.CookLevin.Desc.qCode q) (fun (x : ℕ) => 0) 0
• MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.emitOne t) = MIPRE.TM.CookLevin.Desc.packFields e G 3 (↑t) 0 0 0 0 (fun (x : ℕ) => 0) 0
• MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.emitBad t) = MIPRE.TM.CookLevin.Desc.packFields e G 4 (↑t) 0 0 0 0 (fun (x : ℕ) => 0) 0
• MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.emitted t) = MIPRE.TM.CookLevin.Desc.packFields e G 5 (↑t) 0 0 0 0 (fun (x : ℕ) => 0) 0
• MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.aux t js g) = MIPRE.TM.CookLevin.Desc.packFields e G 6 (↑t) 0 0 0 0 (MIPRE.TM.CookLevin.Desc.jsFun e js) ↑g

theorem MIPRE.TM.CookLevin.Desc.length_encodeVar (e G : ℕ) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) : List.length (encodeVar e G v) = mOf e G

theorem MIPRE.TM.CookLevin.Desc.numCells_lt_two_pow_W (e : ℕ) : numCells (Sof e) < 2 ^ W e

S < 2^W and 2S + 7 < 2^W.

theorem MIPRE.TM.CookLevin.Desc.Sof_lt_two_pow_W (e : ℕ) : Sof e < 2 ^ W e

theorem MIPRE.TM.CookLevin.Desc.decodeVar_encodeVar (e G T : ℕ) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) : decodeVar e G (fieldsOf e G T (encodeVar e G v)) = some v

Decoding inverts encoding.