Cook-Levin: the precomputation, composed with the assembled generator

53 fully proved

Counter-view additions: decrement, multi-target transfer, the power loop

DefinitionUnit targets of a multi-target transfer#✓fully proved

For a list \(y_1, \dots, y_j\) of counters, the list of transfer targets that pushes one unit on each counter \(y_i\), in the same order.

def tg (ys : List C) : List (Σ k, SΓ C k) := ys.map fun y => ⟨.c y, ()⟩

Uses 2 · Used by 4

Statement usesStacks of a counter machine · Alphabets of a counter machine

Used byThe counter program · The statements of one Horner round · Power-loop program · Multi-target transfer

DefinitionCounters after a multi-target transfer#✓fully proved

Given counter values \(F : C \to \mathbb{N}\), a counter \(x \in C\) and a list \(Y\) of counters, the counter values after transferring \(x\) to \(Y\) form the function that sends \(x\) to \(0\), sends every \(z \ne x\) occurring in \(Y\) to \(F(z) + F(x)\), and sends every other \(z\) to \(F(z)\).

def xf (F : C → ℕ) (x : C) (ys : List C) : C → ℕ :=
  fun z => if z = x then 0 else if z ∈ ys then F z + F x else F z

Used by 4

Used byThe counter program's run · One Horner round · The power loop · Multi-target transfer

TheoremMulti-target transfer#✓fully proved

Let \(M\) be a counter machine with counters indexed by \(C\), a Boolean output stack and a Boolean state, let \(x \in C\), and let \(Y\) be a list of distinct counters not containing \(x\). Suppose the instruction at label \(\ell\) is the transfer loop that pops counter \(x\) and pushes one unit on every counter of \(Y\), returning to \(\ell\) while \(x\) is nonempty and continuing at label \(\ell'\) once it is empty. Then for all counter values \(F : C \to \mathbb{N}\), every state bit \(v\) and every output stack \(o\), the machine runs in exactly \(F(x) + 1\) steps from label \(\ell\) with state \(v\), counter values \(F\) and output stack \(o\) to label \(\ell'\) with state false, output stack \(o\) and the counter values after transferring \(x\) to \(Y\): counter \(x\) becomes \(0\), each counter of \(Y\) gains \(F(x)\), and every other counter keeps its value.

theorem xferS {self next : Λ} {x : C} {ys : List C} (hp : M self = xfer (.c x) (tg ys) self next)
    (hnd : ys.Nodup) (hx : x ∉ ys) (F : C → ℕ) (v : Bool) (o : List Bool) :
    Run M (F x + 1) ⟨some self, v, st F o⟩ ⟨some next, false, st (xf F x ys) o⟩

Uses 11 · Used by 3

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Unit targets of a multi-target transfer · Counters after a multi-target transfer · Flag bit of a machine state · Exact-length runs of a TM2 machine · Counter transfer loop

Proof usesAdding units to target stacks · Unary counter · Running a counter transfer

Used byThe counter program's run · One Horner round · The power loop

InductiveStages of the power loop#✓fully proved

The labels of one power-loop site: a head stage, a multiplication stage \(\mathrm{mul}(s)\) for each stage \(s\) of a multiplication site, a drain stage and a move stage.

inductive PW
  | hd
  | mul (s : MS)
  | drn
  | mv
  deriving DecidableEq, Fintype

Uses 1 · Used by 10

Statement usesStages of the multiplication routine

Used byThe reduction machine halts with the emitted formula · The reduction machine · The counter program · The counter program's run · The full program · The full machine as a finite multi-stack Turing machine · Labels of the counter program · The power loop · Power-loop program · The precomputation

DefinitionPower-loop program#✓fully proved

Given six counters \(b\), \(k\), \(p\), \(q\), \(a\), \(t\), a label for each power-loop stage and an exit label, the power loop is the following program on the stages. At the head stage it pops one unit from \(k\); if \(k\) was empty it goes to the exit label, otherwise to the first multiplication stage. The multiplication stages add \(p \cdot b\) to \(q\) (a multiplication site with index counter \(a\) and scratch counter \(t\)) and then go to the drain stage. The drain stage empties \(p\) and goes to the move stage. The move stage moves the contents of \(q\) onto \(p\) and returns to the head stage.

When the six counters are distinct and \(q = a = t = 0\) at the start, each round multiplies \(p\) by \(b\), so the loop replaces \(p\) by \(p \cdot b^k\) and ends with \(k = 0\).

def powS (b kc p q ad t : C) (mk : PW → Λ) (exit : Λ) : PW → TM2.Stmt (SΓ C) Λ Bool
  | .hd => decr (.c kc) exit (mk (.mul .head))
  | .mul s => mulS p ad b q t (fun s => mk (.mul s)) (mk .drn) s
  | .drn => xfer (.c p) [] (mk .drn) (mk .mv)
  | .mv => xfer (.c q) (tg [p]) (mk .mv) (mk .hd)

Uses 9 · Used by 2

Statement usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · The multiplication routine of a counter machine · Stages of the power loop · Unit targets of a multi-target transfer · Flag bit of a machine state · Decrement · Counter transfer loop

Used byThe counter program · The power loop

DefinitionStep budget of the power loop#✓fully proved

For natural numbers \(j\) (the number of rounds), \(p\) (the start value) and \(b\) (the base), the step budget of the power loop is \(j \, (p \, (b + 1)^j \, (3 b + 5) + 5) + 1\).

def powB (j p b : ℕ) : ℕ := j * (p * (b + 1) ^ j * (3 * b + 5) + 5) + 1

Used by 3

Used byStep budget of the counter program · The counter program's run · The power loop

TheoremThe power loop#✓fully proved

Let \(b, k, p, q, a, t\) be pairwise distinct counters of a counter machine \(M\), let \(\mu\) assign a label to each power-loop stage and let \(\nu\) be a label. Suppose that for every power-loop stage \(s\) the label \(\mu(s)\) runs the power-loop program for \(b, k, p, q, a, t\) with stage labels \(\mu\) and exit label \(\nu\) at stage \(s\). Let \(j \in \mathbb{N}\), let \(F\) be counter values with \(F(k) = j\) and \(F(q) = F(a) = F(t) = 0\), let \(v\) be a flag and \(o\) an output. Then \(M\) runs from the head stage \(\mu(\mathrm{hd})\) with flag \(v\), counters \(F\) and output \(o\) to the label \(\nu\) with flag false, output \(o\), and counters \(F\) except that \(p\) holds \(F(p) \cdot F(b)^j\) and \(k\) holds \(0\), within \(j\,(F(p)\,(F(b) + 1)^j\,(3F(b) + 5) + 5) + 1\) steps, the step budget of the power loop for \(j\) rounds, start value \(F(p)\) and base \(F(b)\).

theorem pow_run {b kc p q ad t : C} {mk : PW → Λ} {exit : Λ}
    (hp : ∀ s, M (mk s) = powS b kc p q ad t mk exit s)
    (hnd : [b, kc, p, q, ad, t].Nodup) :
    ∀ (j : ℕ) (F : C → ℕ), F kc = j → F q = 0 → F ad = 0 → F t = 0 → ∀ (v : Bool) (o : List Bool),
      RunLe M (powB j (F p) (F b)) ⟨some (mk .hd), v, st F o⟩
        ⟨some exit, false, st (update (update F p (F p * F b ^ j)) kc 0) o⟩

Uses 20 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Stages of the power loop · Step budget of the power loop · Power-loop program · Runs within a step budget

Proof usesStages of the multiplication routine · The multiplication routine of a counter machine · Counters after a multi-target transfer · Multi-target transfer · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Unary counter · Decrement · Multiplying unary counters · Counter transfer loop · Running a counter transfer

Used byThe counter program's run

Horner evaluation of a polynomial on counters

InductiveStages of a Horner round#✓fully proved

The Horner-round stages are \(\mathsf{mul}(s)\), one for each stage \(s\) of a multiplication site, and the three stages \(\mathsf{drn}\), \(\mathsf{mv}\) and \(\mathsf{add}\). In a Horner round they label the multiplication, draining the accumulator, moving the product into the accumulator, and adding the coefficient.

inductive HW
  | mul (s : MS)
  | drn
  | mv
  | add
  deriving DecidableEq, Fintype

Uses 1 · Used by 12

Statement usesStages of the multiplication routine

Used byThe reduction machine halts with the emitted formula · The reduction machine · The counter program · The counter program's run · The full program · The full machine as a finite multi-stack Turing machine · Horner-round labels indexed by natural numbers · One Horner round · The statements of one Horner round · Horner rounds · Labels of the counter program · The precomputation

DefinitionThe statements of one Horner round#✓fully proved

For counters \(b, \mathit{acc}, q, d, t\), a number \(a \in \mathbb{N}\), stage labels \(\mu\) and an exit label \(\nu\): the statements performing \(\mathit{acc} \leftarrow \mathit{acc} \cdot b + a\) in four stages, each stage reaching the next through \(\mu\). The multiplication stages add \(\mathit{acc} \cdot b\) to \(q\) (with index counter \(d\) and scratch counter \(t\)), then the drain stage empties \(\mathit{acc}\), the move stage transfers \(q\) into \(\mathit{acc}\), and the add stage pushes \(a\) units onto \(\mathit{acc}\) and continues at \(\nu\).

def hornS (b acc q ad t : C) (a : ℕ) (mk : HW → Λ) (next : Λ) : HW → TM2.Stmt (SΓ C) Λ Bool
  | .mul s => mulS acc ad b q t (fun s => mk (.mul s)) (mk .drn) s
  | .drn => xfer (.c acc) [] (mk .drn) (mk .mv)
  | .mv => xfer (.c q) (tg [acc]) (mk .mv) (mk .add)
  | .add => emitR (.c acc) (List.replicate a ()) next

Uses 9 · Used by 4

Statement usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · The multiplication routine of a counter machine · Stages of a Horner round · Unit targets of a multi-target transfer · Flag bit of a machine state · Prepending a constant list · Counter transfer loop

Used byThe counter program · The counter program's run · One Horner round · Horner rounds

DefinitionStep count of one Horner round#✓fully proved

For an accumulator value \(A\) and a base \(b\), the number \(A(2b + 3) + A + 2 + (A + 1) + (Ab + 1) + 1\): the exact number of steps one Horner round takes from \(\mathit{acc} = A\) with base \(b\).

def hornStep (A b : ℕ) : ℕ := A * (2 * b + 3) + A + 2 + (A + 1) + (A * b + 1) + 1

Used by 4

Used byOne Horner round · Step count of the Horner rounds · The Horner step count is polynomial · Horner rounds

TheoremOne Horner round#✓fully proved

Let \(b, \mathit{acc}, q, d, t\) be pairwise distinct counters of a counter machine \(M\), let \(a \in \mathbb{N}\), let \(\mu\) assign a label to each Horner-round stage and let \(\nu\) be a label. Suppose that for every Horner-round stage \(s\) the label \(\mu(s)\) runs the Horner-round statement for \(b, \mathit{acc}, q, d, t, a\) with stage labels \(\mu\) and exit label \(\nu\) at stage \(s\). Let \(F\) be counter values with \(F(q) = F(d) = F(t) = 0\), let \(v\) be a flag and \(o\) an output, and let \(h\) be the step count of one Horner round. Then \(M\) runs from the first multiplication stage \(\mu(\mathrm{mul\ head})\) with flag \(v\), counters \(F\) and output \(o\) in exactly \(h(F(\mathit{acc}), F(b))\) steps to the label \(\nu\) with flag false, output \(o\), and counters \(F\) except that \(\mathit{acc}\) holds \(F(\mathit{acc}) \cdot F(b) + a\).

theorem horn_round {b acc q ad t : C} {a : ℕ} {mk : HW → Λ} {next : Λ}
    (hp : ∀ s, M (mk s) = hornS b acc q ad t a mk next s)
    (hnd : [b, acc, q, ad, t].Nodup) (F : C → ℕ) (hq : F q = 0) (had : F ad = 0)
    (ht : F t = 0) (v : Bool) (o : List Bool) :
    Run M (hornStep (F acc) (F b)) ⟨some (mk (.mul .head)), v, st F o⟩
      ⟨some next, false, st (update F acc (F acc * F b + a)) o⟩

Uses 21 · Used by 1

Statement usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Stages of a Horner round · The statements of one Horner round · Step count of one Horner round · Exact-length runs of a TM2 machine

Proof usesThe multiplication routine of a counter machine · Counters after a multi-target transfer · Multi-target transfer · Flag bit of a machine state · A single step executes the statement at the current label · Adding units to target stacks · Unary counter · Pushing a constant list · Prepending a constant list · Multiplying unary counters · Pushing a list of symbols onto one stack · Counter transfer loop · Running a counter transfer

Used byHorner rounds

DefinitionHorner value#✓fully proved

For a list \(c_1, \dots, c_\ell\) of natural numbers and natural numbers \(b\) and \(A\), the Horner value of \(c_1, \dots, c_\ell\) with base \(b\) from accumulator \(A\) is the number obtained from the starting value \(x = A\) by replacing \(x\) by \(x b + c_i\) for \(i = 1, \dots, \ell\) in turn; for the empty list it is \(A\).

def hornVal (cs : List ℕ) (b A : ℕ) : ℕ := cs.foldl (fun A a => A * b + a) A

Used by 4

Used byThe counter program's run · Horner's rule · Splitting off the starting accumulator in Horner evaluation · Horner rounds

DefinitionStep count of the Horner rounds#✓fully proved

For a list \(cs\) of coefficients, a base \(b\) and an accumulator value \(A\): \(0\) if \(cs\) is empty, and if \(cs\) is \(a\) followed by \(cs'\), the step count \(h(A, b)\) of one Horner round from \(A\) with base \(b\) plus the step count of \(cs'\) with base \(b\) from accumulator \(A b + a\). This is the exact number of steps of the Horner rounds.

def hornT : List ℕ → ℕ → ℕ → ℕ
  | [], _, _ => 0
  | a :: cs, b, A => hornStep A b + hornT cs b (A * b + a)

Uses 1 · Used by 7

Statement usesStep count of one Horner round

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · Step budget of the counter program · The counter program's run · Polynomial time bound of the composed machine · The Horner step count is polynomial · Horner rounds

TheoremHorner rounds#✓fully proved

Let \(b, \mathit{acc}, q, d, t\) be pairwise distinct counters of a counter machine \(M\), let \(c_0, \dots, c_{\ell-1}\) be natural numbers, let \(\mu\) assign a label \(\mu(i, s)\) to each \(i \in \mathbb{N}\) and each Horner-round stage \(s\), and let \(\nu\) be a label. Suppose that for every \(i < \ell\) and every stage \(s\) the label \(\mu(i, s)\) runs, at stage \(s\), the statement of one Horner round for \(b, \mathit{acc}, q, d, t\) and the number \(c_i\), with stage labels \(\mu(i, \cdot)\) and exit label \(\mu(i + 1, \mathrm{mul\ head})\) if \(i + 1 < \ell\) and \(\nu\) otherwise. Then for all \(i, j \in \mathbb{N}\) with \(i + j = \ell\), all counter values \(F\) with \(F(q) = F(d) = F(t) = 0\), every flag \(v\) and every output \(o\), there is a flag \(v'\) such that \(M\) runs in exactly \(h\) steps from the label \(\mu(i, \mathrm{mul\ head})\) if \(i < \ell\) and \(\nu\) otherwise, with flag \(v\), counters \(F\) and output \(o\), to the label \(\nu\) with flag \(v'\), output \(o\), and counters \(F\) except that \(\mathit{acc}\) holds the Horner value of \(c_i, \dots, c_{\ell-1}\) with base \(F(b)\) from accumulator \(F(\mathit{acc})\). Here \(h\) is the step count of the Horner rounds over \(c_i, \dots, c_{\ell-1}\) with base \(F(b)\) from accumulator \(F(\mathit{acc})\).

theorem horner_run {b acc q ad t : C} (cs : List ℕ) {mk : ℕ → HW → Λ} {exit : Λ}
    (hp : ∀ i (hi : i < cs.length) s, M (mk i s) = hornS b acc q ad t cs[i] (mk i)
      (if i + 1 < cs.length then mk (i + 1) (.mul .head) else exit) s)
    (hnd : [b, acc, q, ad, t].Nodup) :
    ∀ (j i : ℕ), i + j = cs.length → ∀ (F : C → ℕ), F q = 0 → F ad = 0 → F t = 0 →
      ∀ (v : Bool) (o : List Bool),
      ∃ v' : Bool, Run M (hornT (cs.drop i) (F b) (F acc))
        ⟨some (if i < cs.length then mk i (.mul .head) else exit), v, st F o⟩
        ⟨some exit, v', st (update F acc (hornVal (cs.drop i) (F b) (F acc))) o⟩

Uses 11 · Used by 1

Statement usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Stages of a Horner round · The statements of one Horner round · Step count of the Horner rounds · Horner value · Exact-length runs of a TM2 machine

Proof usesStep count of one Horner round · One Horner round

Used byThe counter program's run

TheoremSplitting off the starting accumulator in Horner evaluation#✓fully proved

For a list \(c_1, \dots, c_\ell\) of natural numbers and natural numbers \(b\) and \(A\), write \(h(x)\) for the Horner value of \(c_1, \dots, c_\ell\) with base \(b\) from accumulator \(x\): the number obtained from the starting value \(x\) by replacing the current value \(y\) by \(y b + c_i\) for \(i = 1, \dots, \ell\) in turn. Then \(h(A) = A b^{\ell} + h(0)\).

theorem hornVal_eq (cs : List ℕ) (b A : ℕ) :
    hornVal cs b A = A * b ^ cs.length + hornVal cs b 0

Uses 1 · Used by 1

Statement usesHorner value

Used byHorner's rule

DefinitionCoefficient list of a polynomial#✓fully proved

For a polynomial \(p\) with natural-number coefficients and natural degree \(d\) (where \(d = 0\) when \(p = 0\)), the coefficient list of \(p\) is \([p_d, p_{d-1}, \dots, p_1, p_0]\), where \(p_i\) is the coefficient of \(X^i\) in \(p\).

noncomputable def coeffs (p : Polynomial ℕ) : List ℕ :=
  (List.range (p.natDegree + 1)).reverse.map p.coeff

Used by 15

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · The reduction machine · Step budget of the counter program · The counter program · The counter program's run · The full program · The full program on the real generators · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The full machine as a finite multi-stack Turing machine · Horner's rule · Initial configuration of the full machine · The precomputation

TheoremHorner's rule#✓fully proved

For every polynomial \(p\) with natural coefficients and every \(b \in \mathbb{N}\), running Horner rounds with base \(b\) on the coefficients of \(p\) (highest degree first), starting from accumulator \(0\), yields \(p(b)\).

theorem hornVal_coeffs (p : Polynomial ℕ) (b : ℕ) : hornVal (coeffs p) b 0 = p.eval b

Uses 3 · Used by 1

Statement usesCoefficient list of a polynomial · Horner value

Proof usesSplitting off the starting accumulator in Horner evaluation

Used byThe counter program's run

The precomputation's counter program

InductiveScratch counters of the counter program#✓fully proved

The type of the twelve private counters of the precomputation's counter program, with constructors \(N\), \(P\), \(Q\), \(AD\), \(TMP\), \(KC\), \(Mc\), \(B\), \(Tc\), \(Fx\), \(Dd\), \(Hc\).

inductive PS
  | N | P | Q | AD | TMP | KC | Mc | B | Tc | Fx | Dd | Hc
  deriving DecidableEq

Used by 26

Used byStacks to drain · Only the output stack survives the drain · The reduction machine halts with the emitted formula · Running a program, then the drain · The reduction machine · Counters of the counter program · The counter program · The counter program's run · Stack renaming of the counter program · Embedding of the counter program's stacks · Embedding of the host's stacks · Alphabets of the full machine · Start counter values · Counter values after the Horner loop · Counter values before the power loop · Counter values after the power loop · Counter values at the end of the counter program · Stacks of the full machine · Stacks during the read loop · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The full machine as a finite multi-stack Turing machine · Initial configuration of the full machine · The precomputation · The read loop · The read loop's run

InductiveTarget counters of the counter program#✓fully proved

The type of the twelve counters that the precomputation's counter program loads for the host, with constructors \(uT\), \(uH\), \(sT\), \(sH\), \(hT\), \(hH\), \(aT\), \(aH\), \(iT\), \(iX\), \(iE\), \(iF\).

They hold the twelve preloads of the assembled generator's run.

inductive PT
  | uT | uH | sT | sH | hT | hH | aT | aH | iT | iX | iE | iF
  deriving DecidableEq

Used by 14

Used byCounters of the counter program · The counter program · The counter program's run · Stack renaming of the counter program · Embedding of the counter program's stacks · Start counter values · Counter values after the Horner loop · Counter values before the power loop · Counter values after the power loop · Counter values at the end of the counter program · The composed machine, raw input to formula · The precomputation · Host counter of each target · Target counter values

InductiveCounters of the counter program#✓fully proved

A counter of the counter program is either a scratch counter \(s(x)\), for one of the twelve scratch counter names \(x\), or a target counter \(t(y)\), for one of the twelve target counter names \(y\): the counters are the disjoint union of the scratch counters and the target counters.

inductive CC
  | s (x : PS)
  | t (y : PT)
  deriving DecidableEq, Fintype

Uses 2 · Used by 11

Statement usesScratch counters of the counter program · Target counters of the counter program

Used byThe counter program · The counter program's run · Stack renaming of the counter program · Embedding of the counter program's stacks · Start counter values · Counter values after the Horner loop · Counter values before the power loop · Counter values after the power loop · Counter values at the end of the counter program · The full program · The precomputation

InductiveLabels of the counter program#✓fully proved

For \(D \in \mathbb{N}\), the number of Horner rounds, the labels of the counter program are \(p_1\); a label \(\mathrm{hr}(i, s)\) for each round \(i < D\) and each Horner-round stage \(s\); the labels \(x_1, x_2, x_3, x_4, c_1, c_2, x_6, x_7, x_8\); a label \(w_2(s)\) for each power-loop stage \(s\); \(x_9\); a label \(\mathrm{ml}(s)\) for each stage \(s\) of a multiplication site; the labels \(x_{10}, x_{11}, x_{12}, x_{13}, x_{14}\); and \(\mathrm{done}\).

inductive PL (D : ℕ)
  | p1 | hr (i : Fin D) (s : HW) | x1 | x2 | x3 | x4 | c1 | c2 | x6 | x7 | x8 | w2 (s : PW) | x9
  | ml (s : MS) | x10 | x11 | x12 | x13 | x14 | done
  deriving DecidableEq, Fintype

Uses 3 · Used by 11

Statement usesStages of the multiplication routine · Stages of a Horner round · Stages of the power loop

Used byThe reduction machine halts with the emitted formula · The reduction machine · The counter program · The counter program's run · Labels of the full machine · The full program · The full machine as a finite multi-stack Turing machine · Horner-round labels indexed by natural numbers · The precomputation · The read loop · The read loop's run

DefinitionHorner-round labels indexed by natural numbers#✓fully proved

For a number \(D\) of Horner rounds, \(i \in \mathbb{N}\) and a Horner-round stage \(s\): the counter-program label for stage \(s\) of Horner round \(i\) if \(i < D\), and otherwise the label \(x_1\) that follows the Horner rounds.

Indices \(i \ge D\) are never reached.

def hlab {D : ℕ} (i : ℕ) (s : HW) : PL D := if h : i < D then .hr ⟨i, h⟩ s else .x1

Uses 2 · Used by 2

Statement usesStages of a Horner round · Labels of the counter program

Used byThe counter program · The counter program's run

DefinitionThe counter program#✓fully proved

For a polynomial \(k\) with natural-number coefficients, whose coefficient list \(\kappa_0, \dots, \kappa_{D-1}\) has length \(D\), and \(c, e, d \in \mathbb{N}\), the counter program is the program with the labels of the counter program for \(D\) Horner rounds that acts on a Boolean output stack and on the scratch and target counters of the counter program as follows. It runs \(D\) Horner rounds, round \(i\) with coefficient \(\kappa_i\), base \(N\), accumulator \(P\), product counter \(Q\), index counter \(AD\) and scratch counter \(TMP\). It moves \(P\) onto both \(Mc\) and the target \(iE\), moves \(N\) onto both \(Mc\) and the target \(iX\), and adds one unit to each of \(Mc\) and \(iX\). It adds \(Mc\) to \(B\), restoring \(Mc\) through \(TMP\), adds \(c\) units to \(B\), \(e\) units to \(KC\) and one unit to \(Tc\), and runs the power loop with base \(B\), round counter \(KC\), accumulator \(Tc\), product counter \(Q\), index counter \(AD\) and scratch counter \(TMP\). It adds \(d\) units to \(Dd\), adds \(Dd \cdot Tc\) to \(Fx\) (index counter \(AD\), scratch counter \(TMP\)) and adds \(d + 1\) more units to \(Fx\). It moves \(Fx\) onto both \(Hc\) and the target \(iF\) and moves \(Mc\) onto \(Hc\). Finally it moves \(Tc\) onto each of the targets \(uT, sT, hT, aT, iT\), moves \(Hc\) onto each of the targets \(uH, sH, hH, aH\), and halts.

Started with \(n\) on \(N\) and every other counter empty, the program computes \(P = k(n)\) by Horner's rule, \(m = n + 1 + k(n)\) on \(Mc\), \(T = (m + c)^e\) on \(Tc\), \(dT + d + 1\) on \(Fx\) and \(m + dT + d + 1\) on \(Hc\), and so loads the twelve target counters.

Cslib.Complexity.CookLevin.Precompute.cprog · 23 lines

noncomputable def cprog (k : Polynomial ℕ) (c e d : ℕ) :
    PL (coeffs k).length → TM2.Stmt (SΓ CC) (PL (coeffs k).length) Bool
  | .p1 => emitR (.c (s P)) (List.replicate 0 ()) (if 0 < (coeffs k).length then hlab 0 (.mul .head) else .x1)
  | .hr i q => hornS (s N) (s P) (s Q) (s AD) (s TMP) (coeffs k)[i] (hlab i.1)
      (if i.1 + 1 < (coeffs k).length then hlab (i.1 + 1) (.mul .head) else .x1) q
  | .x1 => xfer (.c (s P)) (tg [s Mc, t iE]) .x1 .x2
  | .x2 => xfer (.c (s N)) (tg [s Mc, t iX]) .x2 .x3
  | .x3 => emitR (.c (s Mc)) (List.replicate 1 ()) .x4
  | .x4 => emitR (.c (t iX)) (List.replicate 1 ()) .c1
  | .c1 => xfer (.c (s Mc)) [⟨.c (s B), ()⟩, ⟨.c (s TMP), ()⟩] .c1 .c2
  | .c2 => xfer (.c (s TMP)) [⟨.c (s Mc), ()⟩] .c2 .x6
  | .x6 => emitR (.c (s B)) (List.replicate c ()) .x7
  | .x7 => emitR (.c (s KC)) (List.replicate e ()) .x8
  | .x8 => emitR (.c (s Tc)) (List.replicate 1 ()) (.w2 .hd)
  | .w2 q => powS (s B) (s KC) (s Tc) (s Q) (s AD) (s TMP) PL.w2 .x9 q
  | .x9 => emitR (.c (s Dd)) (List.replicate d ()) (.ml .head)
  | .ml q => mulS (s Dd) (s AD) (s Tc) (s Fx) (s TMP) PL.ml .x10 q
  | .x10 => emitR (.c (s Fx)) (List.replicate (d + 1) ()) .x11
  | .x11 => xfer (.c (s Fx)) (tg [s Hc, t iF]) .x11 .x12
  | .x12 => xfer (.c (s Mc)) (tg [s Hc]) .x12 .x13
  | .x13 => xfer (.c (s Tc)) (tg [t uT, t sT, t hT, t aT, t iT]) .x13 .x14
  | .x14 => xfer (.c (s Hc)) (tg [t uH, t sH, t hH, t aH]) .x14 .done
  | .done => .halt

Uses 18 · Used by 3

Statement usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · The multiplication routine of a counter machine · Counters of the counter program · Stages of a Horner round · Labels of the counter program · Scratch counters of the counter program · Target counters of the counter program · Stages of the power loop · Coefficient list of a polynomial · Horner-round labels indexed by natural numbers · The statements of one Horner round · Power-loop program · Unit targets of a multi-target transfer · Flag bit of a machine state · Prepending a constant list · Counter transfer loop

Used byThe counter program's run · The full program · The precomputation

DefinitionTotal length bound#✓fully proved

For a polynomial \(k\) with natural-number coefficients and \(n \in \mathbb{N}\), the total length bound is \(m = n + 1 + k(n)\).

So a word \(x\) of length \(n + 1\) followed by a word \(y\) has length at most \(m\) exactly when \(y\) has length at most \(k(n)\).

def mOf (k : Polynomial ℕ) (n : ℕ) : ℕ := n + 1 + k.eval n

Used by 16

Used byCorrectness of the reduction · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · The formula emitted on a raw input · Step budget of the counter program · The counter program's run · Counter values before the power loop · Counter values after the power loop · Counter values at the end of the counter program · Step bound of the full machine · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The precomputed time bound · Target counter values · Every NP problem reduces to binary-index CNF-SAT

DefinitionThe precomputed time bound#✓fully proved

For a polynomial \(k\) with natural coefficients and \(c, e, n \in \mathbb{N}\), the time bound is \(T = (m + c)^e\), where \(m = n + 1 + k(n)\).

def TOf (k : Polynomial ℕ) (c e n : ℕ) : ℕ := (mOf k n + c) ^ e

Uses 1 · Used by 13

Statement usesTotal length bound

Used byCorrectness of the reduction · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · The formula emitted on a raw input · Step budget of the counter program · The counter program's run · Counter values after the power loop · Step bound of the full machine · The composed machine, raw input to formula · Polynomial time bound of the composed machine · Target counter values · Every NP problem reduces to binary-index CNF-SAT

DefinitionStart counter values#✓fully proved

For a natural number \(n\), the start counter values of the counter program give the scratch counter \(N\) the value \(n\) and every other counter the value \(0\).

def F0 (n : ℕ) : CC → ℕ
  | .s .N => n
  | _ => 0

Uses 3 · Used by 2

Statement usesCounters of the counter program · Scratch counters of the counter program · Target counters of the counter program

Used byThe counter program's run · The precomputation

DefinitionCounter values after the Horner loop#✓fully proved

For a polynomial \(k\) with natural-number coefficients and \(n \in \mathbb{N}\), this is the assignment of values to the counters of the counter program that gives the scratch counter \(N\) the value \(n\), the scratch counter \(P\) the value \(k(n)\), and every other counter the value \(0\).

The counter program reaches these values after its Horner loop has evaluated \(k(n)\).

def F1 (k : Polynomial ℕ) (n : ℕ) : CC → ℕ
  | .s .N => n
  | .s .P => k.eval n
  | _ => 0

Uses 3 · Used by 1

Statement usesCounters of the counter program · Scratch counters of the counter program · Target counters of the counter program

Used byThe counter program's run

DefinitionCounter values before the power loop#✓fully proved

For a polynomial \(k\) with natural-number coefficients and \(c, e, n \in \mathbb{N}\), write \(m = n + 1 + k(n)\). This is the assignment of values to the counters of the counter program that gives the scratch counters \(\mathit{Mc}\), \(B\), \(\mathit{KC}\) and \(\mathit{Tc}\) the values \(m\), \(m + c\), \(e\) and \(1\), the target counters \(\mathit{iX}\) and \(\mathit{iE}\) the values \(n + 1\) and \(k(n)\), and every other counter the value \(0\).

def F2 (k : Polynomial ℕ) (c e n : ℕ) : CC → ℕ
  | .s .Mc => mOf k n
  | .s .B => mOf k n + c
  | .s .KC => e
  | .s .Tc => 1
  | .t .iX => n + 1
  | .t .iE => k.eval n
  | _ => 0

Uses 4 · Used by 1

Statement usesCounters of the counter program · Scratch counters of the counter program · Target counters of the counter program · Total length bound

Used byThe counter program's run

DefinitionCounter values after the power loop#✓fully proved

For a polynomial \(k\) with natural-number coefficients and \(c, e, n \in \mathbb{N}\), write \(m = n + 1 + k(n)\). This is the assignment of values to the counters of the counter program that gives the scratch counters \(\mathit{Mc}\), \(B\) and \(\mathit{Tc}\) the values \(m\), \(m + c\) and \((m + c)^e\), the target counters \(\mathit{iX}\) and \(\mathit{iE}\) the values \(n + 1\) and \(k(n)\), and every other counter the value \(0\).

def F3 (k : Polynomial ℕ) (c e n : ℕ) : CC → ℕ
  | .s .Mc => mOf k n
  | .s .B => mOf k n + c
  | .s .Tc => TOf k c e n
  | .t .iX => n + 1
  | .t .iE => k.eval n
  | _ => 0

Uses 5 · Used by 1

Statement usesCounters of the counter program · Scratch counters of the counter program · Target counters of the counter program · The precomputed time bound · Total length bound

Used byThe counter program's run

DefinitionTarget counter values#✓fully proved

For a polynomial \(k\) with natural-number coefficients and natural numbers \(c, e, d, n\), let \(m = n + 1 + k(n)\), \(T = (m + c)^e\) and let \(H = m + (T + 1)d + 1\) be the stack cap. The target values on the twelve target counters assign \(T\) to each of \(u_T, s_T, h_T, a_T, i_T\), assign \(H\) to each of \(u_H, s_H, h_H, a_H\), and assign \(n + 1\) to \(i_X\), \(k(n)\) to \(i_E\) and \((T + 1)d + 1\) to \(i_F\).

In particular the value at \(i_F\) is \(H - m\).

def tv (k : Polynomial ℕ) (c e d n : ℕ) : PT → ℕ
  | .uT | .sT | .hT | .aT | .iT => TOf k c e n
  | .uH | .sH | .hH | .aH => Situation.capH (mOf k n) (TOf k c e n) d
  | .iX => n + 1
  | .iE => k.eval n
  | .iF => (TOf k c e n + 1) * d + 1

Uses 4 · Used by 3

Statement usesTarget counters of the counter program · The precomputed time bound · Total length bound · Stack cap

Used byCounter values at the end of the counter program · The composed machine, raw input to formula · The precomputation

DefinitionCounter values at the end of the counter program#✓fully proved

For a polynomial \(k\) with natural-number coefficients and \(c, e, d, n \in \mathbb{N}\), write \(m = n + 1 + k(n)\) and \(T = (m + c)^e\). This is the assignment of values to the counters of the counter program that gives the scratch counters \(B\) and \(\mathit{Dd}\) the values \(m + c\) and \(d\), gives each target counter its target value (\(T\) for \(\mathit{uT}\), \(\mathit{sT}\), \(\mathit{hT}\), \(\mathit{aT}\) and \(\mathit{iT}\); \(m + (T + 1)d + 1\) for \(\mathit{uH}\), \(\mathit{sH}\), \(\mathit{hH}\) and \(\mathit{aH}\); \(n + 1\) for \(\mathit{iX}\); \(k(n)\) for \(\mathit{iE}\); \((T + 1)d + 1\) for \(\mathit{iF}\)), and gives every other scratch counter the value \(0\).

def F4 (k : Polynomial ℕ) (c e d n : ℕ) : CC → ℕ
  | .s .B => mOf k n + c
  | .s .Dd => d
  | .t y => tv k c e d n y
  | _ => 0

Uses 5 · Used by 2

Statement usesCounters of the counter program · Scratch counters of the counter program · Target counters of the counter program · Total length bound · Target counter values

Used byThe counter program's run · The precomputation

DefinitionStep budget of the counter program#✓fully proved

For a polynomial \(k\) with natural-number coefficients and natural numbers \(c, e, d, n\), let \(m = n + 1 + k(n)\), \(T = (m + c)^e\) and \(H = m + (T + 1)d + 1\). The step budget of the counter program at \((k, c, e, d, n)\) is

\[ 1 + h + (k(n) + 1) + (n + 1) + 2 + (2m + 2) + 3 + p + 1 + (d(2T + 3) + d + 2) + 1 + (dT + d + 2) + (m + 1) + (T + 1) + (H + 1), \]

where \(h\) is the exact step count of the Horner rounds over the coefficient list of \(k\) with base \(n\) from accumulator \(0\), and \(p = e\left((m + c + 1)^e (3(m + c) + 5) + 5\right) + 1\) is the step budget of the power loop with \(e\) rounds, start value \(1\) and base \(m + c\).

noncomputable def cB (k : Polynomial ℕ) (c e d n : ℕ) : ℕ :=
  1 + hornT (coeffs k) n 0 + (k.eval n + 1) + (n + 1) + 2 + (2 * mOf k n + 2) + 3 + powB e 1 (mOf k n + c) +
    1 + (d * (2 * TOf k c e n + 3) + d + 2) + 1 + (d * TOf k c e n + d + 2) + (mOf k n + 1) +
    (TOf k c e n + 1) + (Situation.capH (mOf k n) (TOf k c e n) d + 1)

Uses 6 · Used by 7

Statement usesThe precomputed time bound · Coefficient list of a polynomial · Step count of the Horner rounds · Total length bound · Step budget of the power loop · Stack cap

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The counter program's run · Step bound of the full machine · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The precomputation

TheoremThe counter program's run#✓fully proved

Let \(k\) be a polynomial with natural-number coefficients, let \(c, e, d, n\) be natural numbers, and put \(m = n + 1 + k(n)\) and \(T = (m + c)^e\). Start the counter program for \(k, c, e, d\) at its first label with any flag, any output stack \(o\), the scratch counter \(N\) equal to \(n\) and every other counter equal to \(0\). Then, in a number of steps at most the step budget of the counter program at \((k, c, e, d, n)\), it reaches its label \(\mathrm{done}\) with flag false, output stack \(o\), and counter values \(T\) on the targets \(uT, sT, hT, aT, iT\); \(m + (T + 1)d + 1\) on the targets \(uH, sH, hH, aH\); \(n + 1\) on \(iX\); \(k(n)\) on \(iE\); \((T + 1)d + 1\) on \(iF\); \(m + c\) on the scratch counter \(B\); \(d\) on the scratch counter \(Dd\); and \(0\) on every other counter.

theorem cprog_run (k : Polynomial ℕ) (c e d n : ℕ) (v : Bool) (o : List Bool) :
    RunLe (cprog k c e d) (cB k c e d n) ⟨some .p1, v, st (F0 n) o⟩
      ⟨some .done, false, st (F4 k c e d n) o⟩

Uses 44 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Counters of the counter program · Start counter values · Counter values at the end of the counter program · Labels of the counter program · Scratch counters of the counter program · Target counters of the counter program · Step budget of the counter program · Coefficient list of a polynomial · The counter program · Runs within a step budget

Proof usesStages of the multiplication routine · Budgeted runs transport along equal counter values · The multiplication routine of a counter machine · Counter values after the Horner loop · Counter values before the power loop · Counter values after the power loop · Stages of a Horner round · Stages of the power loop · The precomputed time bound · Horner-round labels indexed by natural numbers · The statements of one Horner round · Step count of the Horner rounds · Horner value · Horner's rule · Horner rounds · Total length bound · Step budget of the power loop · The power loop · Counters after a multi-target transfer · Multi-target transfer · Budgeted run · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter · Copying a counter through a scratch stack · Pushing a constant list · Prepending a constant list · Multiplying unary counters · Pushing a list of symbols onto one stack · Counter transfer loop

Used byThe precomputation

The full machine: read loop, counter program, host

InductiveStacks of the full machine#✓fully proved

The full machine has one stack for each host stack, one stack for the raw input, and one stack for each scratch counter of the counter program.

inductive FK
  | h (k : HK)
  | raw
  | pc (x : PS)
  deriving DecidableEq, Fintype

Uses 2 · Used by 24

Statement usesStacks of the Cook–Levin host machine · Scratch counters of the counter program

Used byStacks to drain · Step bound for draining bounded stacks · Only the output stack survives the drain · Step bound of the composed machine · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · Running a program, then the drain · The reduction machine · The composed program · Stack renaming of the counter program · Embedding of the counter program's stacks · Embedding of the host's stacks · Alphabets of the full machine · The full program · Stacks during the read loop · The full program on the real generators · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The full machine as a finite multi-stack Turing machine · Initial configuration of the full machine · The precomputation · The read loop · The read loop's run

AbbreviationAlphabets of the full machine#✓fully proved

For natural numbers \(g, r\), the alphabet of a stack of the full machine is the host's alphabet with \(g\) input codes on each host stack, \(\{0, 1, \dots, r - 1\}\) on the raw input stack, and the one-point type on each private counter.

abbrev FΓ (g r : ℕ) : FK → Type
  | .h k => HΓ g k
  | .raw => Fin r
  | .pc _ => Unit

Uses 4 · Used by 16

Statement usesStacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Stacks of the full machine · Scratch counters of the counter program

Used byStep bound for draining bounded stacks · The reduction machine halts with the emitted formula · Running a program, then the drain · The reduction machine · The composed program · Embedding of the counter program's stacks · Embedding of the host's stacks · The full program · Stacks during the read loop · The full program on the real generators · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The full machine as a finite multi-stack Turing machine · The precomputation · The read loop · The read loop's run

InductiveLabels of the full machine#✓fully proved

For \(D \in \mathbb{N}\) and a type \(\Lambda\) of host labels, the labels of the full machine are the read-loop label, one label for each label of the counter program with \(D\) Horner rounds, and one label for each element of \(\Lambda\).

inductive FL (D : ℕ) (Λ : Type)
  | rd
  | pre (l : PL D)
  | h (l : Λ)
  deriving DecidableEq, Fintype

Uses 1 · Used by 11

Statement usesLabels of the counter program

Used byThe reduction machine halts with the emitted formula · The reduction machine · The full program · The full program on the real generators · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The full machine as a finite multi-stack Turing machine · Initial configuration of the full machine · The precomputation · The read loop · The read loop's run

DefinitionHost counter of each target#✓fully proved

The map from the twelve targets to host stacks: \(uT\) and \(uH\) go to the counters \(T_n\) and \(H_s\) of the update generator's block, \(sT\) and \(sH\) to those of the situation-definition generator's block, \(hT\) and \(hH\) to those of the shift generator's block, \(aT\) and \(aH\) to those of the accept generator's block, and \(iT\), \(iX\), \(iE\), \(iF\) to the counters \(T_n\), \(X_n\), \(E_n\), \(F_n\) of the init generator's block.

def tgt : PT → HK
  | .uT => .up .Tn
  | .uH => .up .Hs
  | .sT => .sd .Tn
  | .sH => .sd .Hs
  | .hT => .sh .Tn
  | .hH => .sh .Hs
  | .aT => .ac .Tn
  | .aH => .ac .Hs
  | .iT => .ini .Tn
  | .iX => .ini .Xn
  | .iE => .ini .En
  | .iF => .ini .Fn

Uses 6 · Used by 4

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Counters of the transition-family generator · Counters of the initial-row generator · Target counters of the counter program · Counters of the cell-shift generator

Used byStack renaming of the counter program · Embedding of the counter program's stacks · The composed machine, raw input to formula · The precomputation

DefinitionStack renaming of the counter program#✓fully proved

The stack renaming of the counter program into the full machine sends the output stack to the host's output stack, each scratch counter \(x\) to the full machine's private counter for \(x\), and each target counter \(y\) to the host counter that receives \(y\).

def eC : SK CC → FK
  | .out => .h .out
  | .c (.s x) => .pc x
  | .c (.t y) => .h (tgt y)

Uses 7 · Used by 2

Statement usesStacks of the Cook–Levin host machine · Stacks of a counter machine · Counters of the counter program · Stacks of the full machine · Scratch counters of the counter program · Target counters of the counter program · Host counter of each target

Used byEmbedding of the counter program's stacks · The precomputation

DefinitionEmbedding of the counter program's stacks#✓fully proved

For natural numbers \(g, r\), the stack embedding of the counter program into the full machine with \(g\) input codes and \(r\) raw input symbols renames stacks by the stack renaming of the counter program and identifies the alphabet of each stack with that of its image by the identity (Booleans on the output stack, the one-point type on each counter).

Cslib.Complexity.CookLevin.Precompute.embC · 17 lines

def embC : SEmb (SΓ CC) (FΓ g r) where
  e := eC
  inj := by
    intro a b h
    rcases a with _ | (x | y) <;> rcases b with _ | (x' | y') <;>
      simp only [eC, FK.h.injEq, FK.pc.injEq, reduceCtorEq] at h ⊢
    all_goals first
      | exact h
      | (subst h; rfl)
      | (cases y <;> cases h)
      | (cases y' <;> cases h)
      | (cases y <;> cases y' <;> first | rfl | cases h)
  ι := fun k => match k with
    | .out => Equiv.refl _
    | .c (.s _) => Equiv.refl _
    | .c (.t y) => match y with
      | .uT | .uH | .sT | .sH | .hT | .hH | .aT | .aH | .iT | .iX | .iE | .iF => Equiv.refl _

Uses 15 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Stacks of a counter machine · Alphabets of a counter machine · Counters of the transition-family generator · Counters of the initial-row generator · Counters of the counter program · Stacks of the full machine · Alphabets of the full machine · Scratch counters of the counter program · Target counters of the counter program · Stack renaming of the counter program · Host counter of each target · Counters of the cell-shift generator · Stack embedding

Used byThe full program · The precomputation

DefinitionEmbedding of the host's stacks#✓fully proved

For natural numbers \(g, r\), the stack embedding of the host into the full machine with \(g\) input codes and \(r\) raw input symbols sends each host stack to the same host stack of the full machine and identifies their alphabets by the identity.

def embH : SEmb (HΓ g) (FΓ g r) where
  e := FK.h
  inj := fun _ _ h => by cases h; rfl
  ι := fun _ => Equiv.refl _

Uses 6 · Used by 2

Statement usesStacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Stacks of the full machine · Alphabets of the full machine · Scratch counters of the counter program · Stack embedding

Used byThe full program · The composed machine, raw input to formula

DefinitionThe read loop#✓fully proved

Given a code map \(c_f\) from the raw alphabet \(\mathrm{Fin}\,r\) to the code alphabet \(\mathrm{Fin}\,g\), a separator code \(c_s\) and a list \(L\) of raw symbols, the read-loop statement tests the symbols \(i\) of \(L\) in order against the top of the raw input stack. At the first \(i\) found on top, it pops it, pushes \(c_f(i)\) on the host input stack and one unit on the scratch counter \(N\), and goes back to the read-loop label (with the flag true). If no symbol of \(L\) is on top, in particular when the raw input is empty, it pushes \(c_s\) on the input stack, sets the flag to false and goes to the first label of the counter program.

The full program takes \(L\) to be all of \(\mathrm{Fin}\,r\), so each step reads one input symbol.

def rdT (cf : Fin r → Fin g) (cs : Fin g) : List (Fin r) → TM2.Stmt (FΓ g r) (FL D Λ) Bool
  | [] => .push (.h .inp) (fun _ => cs) (.load (fun _ => false) (.goto fun _ => .pre .p1))
  | i :: L => .peek .raw (fun _ o => decide (o = some i))
      (.branch id (.pop .raw (fun v _ => v) (.push (.h .inp) (fun _ => cf i)
        (.push (.pc .N) (fun _ => ()) (.goto fun _ => .rd)))) (rdT cf cs L))

Uses 6 · Used by 2

Statement usesStacks of the Cook–Levin host machine · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Labels of the counter program · Scratch counters of the counter program

Used byThe full program · The read loop's run

DefinitionStacks during the read loop#✓fully proved

For a list \(s\) of raw symbols in \(\mathrm{Fin}\,r\), a list \(w\) of input codes in \(\mathrm{Fin}\,g\), \(n \in \mathbb{N}\) and a list \(o\) of booleans, these are the stack contents of the full machine in which the raw-input stack holds \(s\), the host input stack holds \(w\), the host output stack holds \(o\), the scratch counter \(N\) holds \(n\) units, and every other stack is empty.

During the read loop, \(s\) is the unread rest of the input and \(w\) holds the codes read so far.

def fst (s : List (Fin r)) (ins : List (Fin g)) (n : ℕ) (o : List Bool) : ∀ k, List (FΓ g r k)
  | .raw => s
  | .h .inp => ins
  | .h .out => o
  | .pc .N => cnt () n
  | _ => []

Uses 9 · Used by 6

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Counters of the transition-family generator · Counters of the initial-row generator · Stacks of the full machine · Alphabets of the full machine · Scratch counters of the counter program · Counters of the cell-shift generator · Unary counter

Used byThe reduction machine halts with the emitted formula · The composed machine, raw input to formula · Polynomial time bound of the composed machine · Initial configuration of the full machine · The precomputation · The read loop's run

TheoremThe read loop's run#✓fully proved

Let \(M\) be a program of the full machine whose read-loop label carries the read loop over all of \(\mathrm{Fin}\,r\), with code map \(c_f\) and separator code \(c_s\), and let \(o\) be a list of booleans. For every raw input \(s = s_1 \cdots s_\ell\), list of codes \(w\), \(n \in \mathbb{N}\) and flag \(v\): started at the read-loop label with flag \(v\), raw input stack \(s\), input stack \(w\), scratch counter \(N = n\), output stack \(o\) and every other stack empty, \(M\) runs in exactly \(\ell + 1\) steps to the counter program's first label, with flag false, raw input stack empty, input stack \(c_s, c_f(s_\ell), \dots, c_f(s_1)\) followed by \(w\), scratch counter \(N = n + \ell\), output stack \(o\) and every other stack empty.

theorem read_run {M : FL D Λ → TM2.Stmt (FΓ g r) (FL D Λ) Bool} {cf : Fin r → Fin g} {cs : Fin g}
    (hM : M .rd = rdT cf cs (List.finRange r)) (o : List Bool) :
    ∀ (s : List (Fin r)) (ins : List (Fin g)) (n : ℕ) (v : Bool),
      Run M (s.length + 1) ⟨some .rd, v, fst s ins n o⟩
        ⟨some (.pre .p1), false, fst [] (cs :: ((s.map cf).reverse ++ ins)) (n + s.length) o⟩

Uses 15 · Used by 1

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Counters of the transition-family generator · Counters of the initial-row generator · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Labels of the counter program · Scratch counters of the counter program · Stacks during the read loop · The read loop · Counters of the cell-shift generator · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label · Unary counter

Used byThe precomputation

The full program and its run

DefinitionThe full program#✓fully proved

Let \(\gamma : \mathrm{Fin}\,r \to \mathrm{Fin}\,g\) code the raw symbols, let \(\sigma \in \mathrm{Fin}\,g\) be a separator code, let \(k\) be a polynomial with natural-number coefficients, let \(c, e, d \in \mathbb{N}\), and let \(h\) be a host program with labels \(\Lambda\) and start label \(\lambda_0 \in \Lambda\). The full program, whose counter-program labels have \(D\) Horner rounds for \(D\) the length of the coefficient list of \(k\), runs at the read-loop label the read loop for \(\gamma\) and \(\sigma\) over all raw symbols; at a counter-program label \(l\) other than the final one, the counter program for \(k, c, e, d\) at \(l\), embedded with its scratch counters on the full machine's private counters, its target counters on the corresponding host counters and its output on the host output; at the final counter-program label, a step that sets the state to false and jumps to the host label \(\lambda_0\); and at a host label \(l\), the statement \(h(l)\) on the host stacks.

noncomputable def fprog (cf : Fin r → Fin g) (cs : Fin g) (k : Polynomial ℕ) (c e d : ℕ) (hp : Λ → TM2.Stmt (HΓ g) Λ Bool)
    (start : Λ) : FL (coeffs k).length Λ → TM2.Stmt (FΓ g r) (FL (coeffs k).length Λ) Bool
  | .rd => rdT cf cs (List.finRange r)
  | .pre l => if l = .done then .load (fun _ => false) (.goto fun _ => .h start)
      else mapS (embC g r) FL.pre (cprog k c e d l)
  | .h l => mapS (embH g r) FL.h (hp l)

Uses 18 · Used by 3

Statement usesStacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Stages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Counters of the counter program · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Stages of a Horner round · Labels of the counter program · Stages of the power loop · Coefficient list of a polynomial · The counter program · Embedding of the counter program's stacks · Embedding of the host's stacks · The read loop · Translating a statement along a stack embedding

Used byThe full program on the real generators · The composed machine, raw input to formula · The precomputation

TheoremThe precomputation#✓fully proved

Fix the full program built from a code map \(c_f\) from the raw alphabet \(\mathrm{Fin}\,r\) to the code alphabet \(\mathrm{Fin}\,g\), a separator code \(c_s\), a polynomial \(k\) with natural coefficients, constants \(c, e, d \in \mathbb{N}\), a host program and its start label. Let \(s = s_1 \cdots s_n\) be a raw input word and \(o\) a list of booleans. Started at the read-loop label with flag false, raw input stack \(s\), output stack \(o\) and every other stack empty, the full program reaches the host's start label with flag false within \(n + 1 + B + 1\) steps, where \(B\) is the counter program's step budget for \(k, c, e, d\) at \(n\). The stacks it reaches satisfy: the output stack is still \(o\); the input stack is \(c_s, c_f(s_n), \dots, c_f(s_1)\); for every target \(y\), the host counter receiving \(y\) has length equal to the target value of \(y\) for \(k, c, e, d\) at \(n\); and every host stack other than the output stack, the input stack and the host counters receiving targets is empty.

These are the preloads that the assembled generator's run expects.

theorem pre_run (s : List (Fin r)) (o : List Bool) :
    ∃ S : ∀ k, List (FΓ g r k),
      RunLe (fprog cf cs k c e d hp start) (s.length + 1 + cB k c e d s.length + 1)
        ⟨some .rd, false, fst s [] 0 o⟩ ⟨some (.h start), false, S⟩ ∧
      S (.h .out) = o ∧ S (.h .inp) = cs :: (s.map cf).reverse ∧
      (∀ y, (S (.h (tgt y))).length = tv k c e d s.length y) ∧
      (∀ hk, (∀ y, tgt y ≠ hk) → hk ≠ .out → hk ≠ .inp → S (.h hk) = [])

Uses 41 · Used by 1

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Counters of the transition-family generator · Counters of the initial-row generator · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Scratch counters of the counter program · Target counters of the counter program · Step budget of the counter program · Coefficient list of a polynomial · The full program · Stacks during the read loop · Host counter of each target · Target counter values · Counters of the cell-shift generator · Runs within a step budget

Proof usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Counters of the counter program · Start counter values · Counter values at the end of the counter program · Stages of a Horner round · Labels of the counter program · Stages of the power loop · The counter program · The counter program's run · Stack renaming of the counter program · Embedding of the counter program's stacks · The read loop's run · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe composed machine, raw input to formula

The full machine on the real generators: raw input to emitted formula

AbbreviationThe full program on the real generators#✓fully proved

For an encoding \(E\) of a machine \(M\), a list \(Y\) of symbols of the input stack alphabet of \(M\), a symbol \(a\) of the output stack alphabet of \(M\), a map \(\iota\) from the raw symbols \(\mathrm{Fin}\,r\) to input stack symbols of \(M\), an input stack symbol \(\sigma\) of \(M\) (the separator), a polynomial \(k\) with natural-number coefficients and \(c, e \in \mathbb{N}\), this is the full program in which each raw symbol \(i\) is coded by the code of \(\iota(i)\) under \(E\), the separator code is the code of \(\sigma\) under \(E\), \(d = \operatorname{depth} M\), the host program is the host running the real generators of \(M\) for \(Y\) and \(a\), and the host starts at the start label of its initial-row generator.

noncomputable abbrev fullProg (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀)
    (sep : M.Γ M.k₀) (k : Polynomial ℕ) (c e : ℕ) :=
  fprog (fun i => InitFamily.encF E (ι i)) (InitFamily.encF E sep) k c e (depth M) (realProg E Ys acc)
    (.ini (.pre1 .eg))

Uses 17 · Used by 5

Statement usesLabels of the Cook–Levin host machine · The host on the real generators of a machine · Variable layout of the transition clauses · Number of literals of a transition clause · Labels of the initial-row generator · Labels of the first precomputation part · Codes of input symbols · Sorted certificate code list · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Coefficient list of a polynomial · The full program · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Window depth of a machine

Used byThe reduction machine halts with the emitted formula · The reduction machine · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The full machine as a finite multi-stack Turing machine

DefinitionStep bound of the full machine#✓fully proved

For an encoding \(E\) of a machine \(M\), a list \(Y\) of symbols of the input stack alphabet of \(M\), a polynomial \(k\) with natural-number coefficients and \(c, e, n \in \mathbb{N}\), write \(m = n + 1 + k(n)\) and \(T = (m + c)^e\). The bound is \(n + 1 + C + 1 + R\), where \(C\) is the step budget of the counter program for \(k\), \(c\), \(e\), \(d = \operatorname{depth} M\) and \(n\), and \(R\) is the host's step bound for \(E\) and \(Y\) at \(m\) and \(T\).

It bounds the number of steps of the full machine on a raw input of length \(n\).

noncomputable def fullB (Ys : List (M.Γ M.k₀)) (k : Polynomial ℕ) (c e n : ℕ) : ℕ :=
  n + 1 + cB k c e (depth M) n + 1 + realB E Ys (mOf k n) (TOf k c e n)

Uses 6 · Used by 6

Statement usesStep bound of the host · The precomputed time bound · Step budget of the counter program · Total length bound · Encoding data for a finite TM2 machine · Window depth of a machine

Used byStep bound of the composed machine · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · The composed machine, raw input to formula · Polynomial time bound of the composed machine

TheoremThe composed machine, raw input to formula#✓fully proved

From the raw input s (all other stacks empty, output o), the full machine halts its host part at fin within fullB steps, having prepended exactly encodeCNF (Phi …) for x = s.map ι ++ [sep], m = |s| + 1 + k(|s|), T = (m + c)^e. No hypotheses (|x| ≤ m is discharged here).

theorem full_run (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀) (sep : M.Γ M.k₀)
    (k : Polynomial ℕ) (c e : ℕ) (s : List (Fin r)) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (FΓ E.layout.g r k)),
      RunLe (fullProg E Ys acc ι sep k c e) (fullB E Ys k c e s.length)
        ⟨some .rd, false, fst s [] 0 o⟩ ⟨some (.h .fin), v, S⟩ ∧
      S (.h .out) = encodeCNF (Phi E (s.map ι ++ [sep]) Ys acc (mOf k s.length)
        (TOf k c e s.length)) ++ o

Uses 53 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · The formula emitted by the host · Counters of the transition-family generator · Variable layout of the transition clauses · Number of literals of a transition clause · Counters of the initial-row generator · Sorted certificate code list · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Scratch counters of the counter program · The precomputed time bound · Coefficient list of a polynomial · Stacks during the read loop · Step bound of the full machine · The full program on the real generators · Total length bound · Counters of the cell-shift generator · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Dense encoding of a CNF formula · Runs within a step budget

Proof usesInitial counters of the accept generator · Alphabets of the Cook–Levin host machine · Step bound of the host · The host on the real generators of a machine · The assembled generator, after the precomputation · Initial counters of the transition-clause generator · Labels of the initial-row generator · Labels of the first precomputation part · Codes of input symbols · Initial counters of the init generator · Target counters of the counter program · Step budget of the counter program · Embedding of the host's stacks · The full program · The precomputation · Host counter of each target · Target counter values · Initial counter values of the shift generator · Stack cap · Window depth of a machine · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Exact-length runs of a TM2 machine · Unary counter

Used byThe reduction machine halts with the emitted formula · Polynomial time bound of the composed machine

DefinitionThe full machine as a finite multi-stack Turing machine#✓fully proved

Given \(r \in \mathbb{N}\), an encoding \(E\) of the machine \(M\), a list \(Y_s\) of input symbols of \(M\), an output symbol \(a\) of \(M\), a map \(\iota\) from \(\{0, \dots, r - 1\}\) to input symbols of \(M\), an input symbol \(\sigma\) of \(M\) (the separator), a polynomial \(k\) with natural coefficients and \(c, e \in \mathbb{N}\): the finite multi-stack machine whose stacks are the full stacks (the host's stacks, the raw input stack and the scratch counters) with the full alphabets, whose labels are the full labels, with start label the read label, internal states the booleans with initial state false, and program the full program built from these data. Its input stack is the raw input stack and its output stack is the host's output stack.

noncomputable def fullTM (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀)
    (sep : M.Γ M.k₀) (k : Polynomial ℕ) (c e : ℕ) : FinTM2 where
  K := FK
  k₀ := .raw
  k₁ := .h .out
  Γ := FΓ E.layout.g r
  Λ := FL _ _
  main := .rd
  σ := Bool
  initialState := false
  m := fullProg E Ys acc ι sep k c e

Uses 41 · Used by 5

Statement usesClause kinds of the accept generator · Counters of the accept generator · Labels of the accept generator · Stages of the accept generator's literal routine · Precomputation stages of the accept generator · Stacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · Stages of the multiplication routine · Counters of the transition-family generator · Labels of the clause-family generator · Stages of the transition-clause generator's literal routine · Variable layout of the transition clauses · Number of literals of a transition clause · Stages of the transition-clause generator's precomputation · Counters of the initial-row generator · Clause kinds of the initial-row generator · Labels of the initial-row generator · Stages of the literal routine (initial-row generator) · Loop phases of the initial-row generator · Labels of the first precomputation part · Labels of the second precomputation part · Sorted certificate code list · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Stages of a Horner round · Labels of the counter program · Scratch counters of the counter program · Stages of the power loop · Coefficient list of a polynomial · The full program on the real generators · Loop-body stages of the cell-shift generator · Counters of the cell-shift generator · Clause kinds of the cell-shift family · Labels of the cell-shift generator · Stages of the cell-shift literal routine · Precomputation stages of the shift generator · Setup and loop stages of a cell-shift block · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding

Used byStep bound of the composed machine · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · Initial configuration of the full machine

TheoremInitial configuration of the full machine#✓fully proved

Let \(E\) be encoding data for a finite multi-stack Turing machine \(M\), and let \(r\) be a natural number. Fix a list \(Y\) of input-stack symbols of \(M\), an output-stack symbol \(a\) of \(M\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input-stack symbols of \(M\), a separator input-stack symbol \(\sigma\) of \(M\), a polynomial \(k\) with natural-number coefficients and natural numbers \(c\) and \(e\). On every raw input \(s\), a word over \(\{0, \dots, r-1\}\), the initial configuration of the full machine built from these data is at the read-loop label with internal state false, its raw-input stack holds \(s\), and all its other stacks (the code stack, the output stack, the scratch counters and the remaining host stacks) are empty.

theorem initList_full (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀)
    (sep : M.Γ M.k₀) (k : Polynomial ℕ) (c e : ℕ) (s : List (Fin r)) :
    initList (fullTM E Ys acc ι sep k c e) s = ⟨some .rd, false, fst s [] 0 []⟩

Uses 18 · Used by 1

Statement usesLabels of the Cook–Levin host machine · Variable layout of the transition clauses · Number of literals of a transition clause · Sorted certificate code list · Labels of the full machine · Coefficient list of a polynomial · Stacks during the read loop · The full machine as a finite multi-stack Turing machine · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding

Proof usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Counters of the transition-family generator · Counters of the initial-row generator · Stacks of the full machine · Scratch counters of the counter program · Counters of the cell-shift generator

Used byThe reduction machine halts with the emitted formula

The step bound is a polynomial in |s|

DefinitionPolynomial functions on the naturals#✓fully proved

A function \(f : \mathbb{N} \to \mathbb{N}\) is polynomial when there is a polynomial \(p\) with natural-number coefficients such that \(f(n) = p(n)\) for every \(n \in \mathbb{N}\).

def IsPoly (f : ℕ → ℕ) : Prop := ∃ p : Polynomial ℕ, ∀ n, f n = p.eval n

Used by 4

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · Polynomial time bound of the composed machine · The Horner step count is polynomial

TheoremThe Horner step count is polynomial#✓fully proved

Let \(cs\) be a list of natural numbers and let \(A : \mathbb{N} \to \mathbb{N}\) be a polynomial function, that is, there is a polynomial \(q\) with natural-number coefficients such that \(A(n) = q(n)\) for all \(n\). Then \(n \mapsto h(n, A(n))\) is a polynomial function in the same sense, where \(h(b, a)\) is the step count of the Horner rounds over \(cs\) with base \(b\) from accumulator \(a\).

theorem hornT (cs : List ℕ) : ∀ {A : ℕ → ℕ}, IsPoly A → IsPoly fun n => Precompute.hornT cs n (A n)

Uses 3 · Used by 3

Statement usesPolynomial functions on the naturals · Step count of the Horner rounds

Proof usesStep count of one Horner round

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · Polynomial time bound of the composed machine

TheoremPolynomial time bound of the composed machine#✓fully proved

Let \(M\) be a finite multi-stack machine with encoding data \(E\), let \(Y\) be a list of symbols of the input stack of \(M\), \(a\) a symbol of its output stack, \(\iota\) a map from the raw symbols \(\mathrm{Fin}\,r\) to symbols of the input stack, \(\sigma\) a symbol of the input stack (the separator), \(k\) a polynomial with natural-number coefficients and \(c, e \in \mathbb{N}\). Then there is a polynomial \(p\) with natural-number coefficients such that the following holds for every raw input \(s = s_1 \cdots s_n\) over \(\mathrm{Fin}\,r\) and every list \(o\) of booleans. Write \(m = n + 1 + k(n)\), \(T = (m + c)^e\) and \(x = \iota(s_1) \cdots \iota(s_n)\,\sigma\). The full program on the real generators for \(E\), \(Y\), \(a\), \(\iota\), \(\sigma\), \(k\), \(c\) and \(e\), started at its read-loop label with flag false, \(s\) on the raw input stack, \(o\) on the host output stack and every other stack empty, reaches the host's final label within \(p(n)\) steps, with some flag and some stack contents in which the host output stack holds the dense encoding of the formula \(\Phi(x, Y, a, m, T)\) emitted by the host, followed by \(o\).

theorem full_time_poly {r : ℕ} {M : FinTM2} (E : Situation.Enc M) (Ys : List (M.Γ M.k₀))
    (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀) (sep : M.Γ M.k₀) (k : Polynomial ℕ) (c e : ℕ) :
    ∃ p : Polynomial ℕ, ∀ (s : List (Fin r)) (o : List Bool), ∃ (v : Bool) (S : ∀ k,
        List (FΓ E.layout.g r k)),
      RunLe (fullProg E Ys acc ι sep k c e) (p.eval s.length)
        ⟨some .rd, false, fst s [] 0 o⟩ ⟨some (.h .fin), v, S⟩ ∧
      S (.h .out) = encodeCNF (Phi E (s.map ι ++ [sep]) Ys acc (mOf k s.length)
        (TOf k c e s.length)) ++ o

Uses 37

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · The formula emitted by the host · Counters of the transition-family generator · Variable layout of the transition clauses · Number of literals of a transition clause · Counters of the initial-row generator · Sorted certificate code list · Stacks of the full machine · Labels of the full machine · Alphabets of the full machine · Scratch counters of the counter program · The precomputed time bound · Coefficient list of a polynomial · Stacks during the read loop · The full program on the real generators · Total length bound · Counters of the cell-shift generator · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Dense encoding of a CNF formula · Runs within a step budget

Proof usesConstant of the accept generator's time bound · Step bound of the host · Constant of the generator's time bound · Constant of the init generator's time bound · Polynomial functions on the naturals · The Horner step count is polynomial · Step budget of the counter program · Step bound of the full machine · The composed machine, raw input to formula · Step count of the Horner rounds · Constant of the shift-generator time bound · Window depth of a machine · Exact-length runs of a TM2 machine

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.