Cook-Levin: halting cleanup and packaging of the reduction machine

21 fully proved

A generic drain phase

TheoremDraining a stack with the transfer loop#✓fully proved

Let \(M\) be a TM2 machine whose state type carries a flag bit, and suppose that the statement of \(M\) at label \(\ell\) is the transfer loop that pops stack \(k\) with no target stacks, returning to \(\ell\) while the pop succeeds and going to label \(\ell'\) once stack \(k\) is empty. Then for every state \(v\) and every stack assignment \(S\), writing \(S_k\) for the contents of stack \(k\) under \(S\) and \(|S_k|\) for its length, in exactly \(|S_k| + 1\) steps the machine goes from label \(\ell\) with state \(v\) and stacks \(S\) to label \(\ell'\) with the state that stores the flag bit false and the stacks of \(S\) with stack \(k\) replaced by the empty list, all other stacks unchanged.

theorem xfer_drain {self next : Λ} {k : K} (hp : M self = xfer k [] self next) :
    ∀ (l : List (Γ k)) (v : σ) (S : ∀ k, List (Γ k)), S k = l →
      Run M (l.length + 1) ⟨some self, v, S⟩ ⟨some next, Flag.tag false, update S k []⟩

Uses 5 · Used by 1

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Counter transfer loop

Proof usesA single step executes the statement at the current label · Pushing symbols onto several stacks

Used byThe drain

DefinitionThe drain program#✓fully proved

Given a list \(k_0, \dots, k_{m-1}\) of stacks, a type \(\Lambda\) of labels and labels \(\lambda : \mathbb{N} \to \Lambda\), stage \(i\) of the drain program is as follows. For \(i < m\) it pops stack \(k_i\), recording in the state whether a symbol was popped, and jumps to \(\lambda(i)\) if one was and to \(\lambda(i + 1)\) if the stack was empty; repeated, this empties \(k_i\). For \(i \ge m\) it sets the state to store the flag bit false and halts.

def drainS (ks : List K) (lab : ℕ → Λ) (i : ℕ) : TM2.Stmt Γ Λ σ :=
  match ks[i]? with
  | some k => xfer k [] (lab i) (lab (i + 1))
  | none => .load (fun _ => Flag.tag false) .halt

Uses 2 · Used by 3

Statement usesFlag bit of a machine state · Counter transfer loop

Used byThe drain · Running a program, then the drain · The composed program

DefinitionDrain step count#✓fully proved

For a list \(k_1, \dots, k_m\) of stacks and contents \(S\) assigning a list \(S_k\) to each stack \(k\), the drain step count is \(1 + \sum_{i=1}^{m} (|S_{k_i}| + 1)\).

def drainB (ks : List K) (S : ∀ k, List (Γ k)) : ℕ :=
  (ks.map fun k => (S k).length + 1).sum + 1

Used by 4

Used byStep bound for draining bounded stacks · The drain · The reduction machine halts with the emitted formula · Running a program, then the drain

TheoremThe drain#✓fully proved

Let \(M\) be a multi-stack machine program with labels in a type \(\Lambda\), let \(k_0, \dots, k_{m-1}\) be a list of distinct stacks, and let \(\lambda : \mathbb{N} \to \Lambda\) be labels such that for every \(i \le m\) the instruction of \(M\) at \(\lambda(i)\) is stage \(i\) of the drain program for this list and these labels. Then for every state \(v\) and stack contents \(S\), the machine runs in exactly \(1 + \sum_{i < m} (|S_{k_i}| + 1)\) steps from label \(\lambda(0)\), state \(v\) and contents \(S\) to the halted configuration whose state stores the flag bit false and whose contents are empty on each \(k_i\) and equal to \(S\) on every other stack.

theorem drain_run :
    ∀ (ks : List K) (lab : ℕ → Λ), ks.Nodup → (∀ i ≤ ks.length, M (lab i) = drainS ks lab i) →
      ∀ (v : σ) (S : ∀ k, List (Γ k)),
        Run M (drainB ks S) ⟨some (lab 0), v, S⟩
          ⟨none, Flag.tag false, fun k => if k ∈ ks then [] else S k⟩

Uses 7 · Used by 1

Statement usesDrain step count · The drain program · Flag bit of a machine state · Exact-length runs of a TM2 machine

Proof usesDraining a stack with the transfer loop · A single step executes the statement at the current label · Counter transfer loop

Used byRunning a program, then the drain

The composed machine: full machine, then the drain

InductiveLabels of the composed machine#✓fully proved

For a type \(\Lambda\) of labels and \(n \in \mathbb{N}\), a label of the composed machine is either a label \(l \in \Lambda\) of the original machine or a drain stage \(i \in \{0, \dots, n\}\).

inductive DL (Λ : Type) (n : ℕ)
  | f (l : Λ)
  | dr (i : Fin (n + 1))
  deriving DecidableEq, Fintype

Used by 5

Used byDrain-stage label · The reduction machine halts with the emitted formula · Running a program, then the drain · The reduction machine · The composed program

DefinitionDrain-stage label#✓fully proved

For \(n, j \in \mathbb{N}\), the label of the composed machine with drain stages \(0, \dots, n\) that names drain stage \(\min(j, n)\).

def dlab {Λ : Type} (n j : ℕ) : DL Λ n := .dr ⟨min j n, by omega⟩

Uses 1 · Used by 2

Statement usesLabels of the composed machine

Used byRunning a program, then the drain · The composed program

DefinitionThe identity stack embedding#✓fully proved

For a family of stack alphabets \(\Gamma\) indexed by \(K\), the identity stack embedding of \(\Gamma\) into itself sends every stack to itself and identifies every alphabet with itself by the identity bijection: a pure relabelling.

def idE {K : Type} (Γ : K → Type) : SEmb Γ Γ := ⟨id, injective_id, fun _ => Equiv.refl _⟩

Uses 1 · Used by 2

Statement usesStack embedding

Used byRunning a program, then the drain · The composed program

DefinitionStacks to drain#✓fully proved

The list of all stacks of the full machine other than its output stack, each appearing exactly once, in an unspecified order. These are the stacks that the drain empties before the composed machine halts.

noncomputable def dks : List FK := (Finset.univ.erase (FK.h .out)).toList

Uses 7 · Used by 9

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 · Scratch counters of the counter program · Counters of the cell-shift generator

Used byStep 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

TheoremOnly the output stack survives the drain#✓fully proved

For any alphabets and any assignment \(T\) of contents to the stacks of the full machine, the contents that are empty on every stack to drain and agree with \(T\) elsewhere are the contents that agree with \(T\) on the output stack and are empty on every other stack.

theorem drained {Γ : FK → Type} (T : ∀ k, List (Γ k)) :
    (fun q => if q ∈ dks then [] else T q) = fun q => if q = FK.h .out then T q else []

Uses 8 · 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 to drain · 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

DefinitionThe composed program#✓fully proved

Let \(g, r \in \mathbb{N}\), let \(P\) be a program with labels \(\Lambda\) and Boolean state over the stacks of the full machine with alphabets \(F\Gamma_{g,r}\), and let \(\mathit{fin} \in \Lambda\). The composed program has as labels the labels of \(P\) and the drain stages \(0, \dots, n\), where \(n\) is the number of stacks other than the output stack. At a label \(\ell \ne \mathit{fin}\) it runs \(P(\ell)\) with every jump target relabelled; at \(\mathit{fin}\) it jumps to drain stage \(0\); at drain stage \(i < n\) it empties the \(i\)-th stack other than the output stack (in a fixed order) and moves to stage \(i + 1\), and at stage \(n\) it sets the state to false and halts.

noncomputable def gprog (P : Λ → TM2.Stmt (FΓ g r) Λ Bool) (fin : Λ) :
    DL Λ dks.length → TM2.Stmt (FΓ g r) (DL Λ dks.length) Bool
  | .f l => if l = fin then .goto (fun _ => dlab _ 0) else mapS (idE _) DL.f (P l)
  | .dr i => drainS dks (dlab _) i.val

Uses 9 · Used by 3

Statement usesLabels of the composed machine · Stacks to drain · Drain-stage label · The drain program · The identity stack embedding · Stacks of the full machine · Alphabets of the full machine · Translating a statement along a stack embedding · Flag bit of a machine state

Used byThe reduction machine halts with the emitted formula · Running a program, then the drain · The reduction machine

TheoremRunning a program, then the drain#✓fully proved

Let \(g, r \in \mathbb{N}\), let \(P\) be a program with labels \(\Lambda\) and Boolean state over the stacks of the full machine with alphabets \(F\Gamma_{g,r}\), and let \(\mathit{fin}\) be a label with \(P(\mathit{fin}) = \mathrm{halt}\). Suppose \(P\) goes in at most \(B\) steps from the configuration with label \(\ell\), state \(v\) and stacks \(S\) to the configuration with label \(\mathit{fin}\), state \(v'\) and stacks \(T\). Then the composed program of \(P\) and \(\mathit{fin}\) goes in at most \(B + 1 + d(T)\) steps from label \(\ell\) (as a label of the composed program), state \(v\) and stacks \(S\) to the halted configuration with state false in which every stack other than the output stack is empty and the output stack is that of \(T\). Here \(d(T)\), the step count of the drain, is \(1\) plus the sum of \(|T_q| + 1\) over the stacks \(q\) other than the output stack.

theorem g_run_gen {P : Λ → TM2.Stmt (FΓ g r) Λ Bool} {fin : Λ} (hfin : P fin = .halt)
    {B : ℕ} {l : Λ} {v v' : Bool} {S T : ∀ k, List (FΓ g r k)}
    (h : RunLe P B ⟨some l, v, S⟩ ⟨some fin, v', T⟩) :
    RunLe (gprog P fin) (B + 1 + drainB dks T) ⟨some (.f l), v, S⟩
      ⟨none, false, fun k => if k ∈ dks then [] else T k⟩

Uses 26 · 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 · Labels of the composed machine · Stacks to drain · Drain step count · The composed program · Stacks of the full machine · Alphabets of the full machine · Scratch counters of the counter program · Counters of the cell-shift generator · Runs within a step budget

Proof usesDrain-stage label · The drain program · The drain · The identity stack embedding · 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 · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe reduction machine halts with the emitted formula

TheoremStep bound for draining bounded stacks#✓fully proved

Let \(g, r, h \in \mathbb{N}\) and let \(T\) assign to every stack \(k\) of the full machine (with alphabets \(\Gamma_{g,r}\)) a list \(T_k\) of length at most \(h\). Let \(L\) be the number of stacks other than the output stack. Then the drain step count \(1 + \sum_k (|T_k| + 1)\), summed over the stacks \(k\) other than the output stack, is at most \(L(h + 1) + 1\).

theorem drainB_le {T : ∀ k, List (FΓ g r k)} {h : ℕ} (hT : ∀ k, (T k).length ≤ h) :
    drainB dks T ≤ dks.length * (h + 1) + 1

Uses 4 · Used by 1

Statement usesStacks to drain · Drain step count · Stacks of the full machine · Alphabets of the full machine

Used byThe reduction machine halts with the emitted formula

The composed machine on the real generators

DefinitionThe reduction machine#✓fully proved

Fix \(r \in \mathbb{N}\), a finite TM2 machine \(M\) with an encoding \(E\), a list \(Y\) of input symbols of \(M\), an output symbol \(a\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input symbols, an input symbol \(\mathit{sep}\), a polynomial \(k\) with coefficients in \(\mathbb{N}\) and \(c, e \in \mathbb{N}\). The reduction machine is the finite TM2 machine with the stacks and alphabets of the full machine, input on the raw-input stack and output on the output stack; its labels are those of the full machine together with the drain stages \(0, \dots, n\), where \(n\) is the number of stacks other than the output stack; it starts at the read-loop label with state false; and its program is the composed program of the full machine's program and its final label: the full machine, followed by the drain.

noncomputable def gTM (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
  Λ := DL (FL _ _) dks.length
  main := .f .rd
  σ := Bool
  initialState := false
  m := gprog (fullProg E Ys acc ι sep k c e) (.h .fin)

Uses 44 · Used by 3

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 · Labels of the composed machine · Stacks to drain · The composed 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 · 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 byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula

DefinitionThe formula emitted on a raw input#✓fully proved

Fix \(r \in \mathbb{N}\), a finite TM2 machine \(M\) with an encoding \(E\), a list \(Y\) of input symbols of \(M\), an output symbol \(a\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input symbols, an input symbol \(\mathit{sep}\), a polynomial \(k\) with coefficients in \(\mathbb{N}\) and \(c, e \in \mathbb{N}\). For a raw input \(s\), a list over \(\{0, \dots, r-1\}\), let \(x\) be \(s\) with each symbol mapped by \(\iota\), followed by \(\mathit{sep}\), let \(m = |s| + 1 + k(|s|)\) and \(T = (m + c)^e\). The emitted formula for \(s\) is the bit-string encoding of the assembled Cook–Levin formula \(\Phi_E(x, Y, a, m, T)\).

noncomputable def phiOf (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)) : List Bool :=
  encodeCNF (Phi E (s.map ι ++ [sep]) Ys acc (mOf k s.length) (TOf k c e s.length))

Uses 5 · Used by 4

Statement usesThe formula emitted by the host · The precomputed time bound · Total length bound · Encoding data for a finite TM2 machine · Dense encoding of a CNF formula

Used byThe Cook–Levin reduction function · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula

DefinitionStep bound of the composed machine#✓fully proved

Fix the verifier data (an encoding \(E\) of a stack machine \(M\), a list \(Y\) of input symbols, an output symbol \(\mathrm{acc}\), a map \(\iota\) into the input alphabet, a separator \(\mathrm{sep}\), a polynomial \(k\) and \(c, e \in \mathbb{N}\)) and an input length \(n\). Let \(B(n)\) be the step bound of the full machine on inputs of length \(n\), let \(D\) be the depth of the full machine (the most push, peek and pop operations on any path of one of its instructions), and let \(L\) be the number of stacks other than the output stack. The step bound of the composed machine is \(B(n) + 1 + (L(n + B(n) D + 1) + 1)\).

noncomputable def gB (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀)
    (sep : M.Γ M.k₀) (k : Polynomial ℕ) (c e n : ℕ) : ℕ :=
  fullB E Ys k c e n + 1 +
    (dks.length * (n + fullB E Ys k c e n * depth (fullTM E Ys acc ι sep k c e) + 1) + 1)

Uses 6 · Used by 3

Statement usesStacks to drain · Stacks of the full machine · Step bound of the full machine · The full machine as a finite multi-stack Turing machine · Encoding data for a finite TM2 machine · Window depth of a machine

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula

TheoremThe reduction machine halts with the emitted formula#✓fully proved

Fix \(r \in \mathbb{N}\), a finite TM2 machine \(M\) with an encoding \(E\), a list \(Y\) of input symbols of \(M\), an output symbol \(a\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input symbols, an input symbol \(\mathit{sep}\), a polynomial \(k\) with coefficients in \(\mathbb{N}\) and \(c, e \in \mathbb{N}\). For every raw input \(s\), a list over \(\{0, \dots, r-1\}\), the program of the reduction machine goes in at most \(g_B(|s|)\) steps from the initial configuration on input \(s\) to the halting configuration with output the emitted formula for \(s\) (no label, the initial state, that formula on the output stack and every other stack empty), where \(g_B\) is the step bound of the composed machine.

No assumption on the verifier data is needed.

theorem g_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)) :
    RunLe (gTM E Ys acc ι sep k c e).m (gB E Ys acc ι sep k c e s.length)
      (initList (gTM E Ys acc ι sep k c e) s)
      (haltList (gTM E Ys acc ι sep k c e) (phiOf E Ys acc ι sep k c e s))

Uses 66 · Used by 2

Statement usesStep bound of the composed machine · The reduction machine · The formula emitted on a raw input · Encoding data for a finite TM2 machine · Runs within a step budget

Proof 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 · The formula emitted by the host · 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 · Labels of the composed machine · Stacks to drain · Drain step count · Step bound for draining bounded stacks · Only the output stack survives the drain · Running a program, then the drain · The composed 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 · Scratch counters of the counter program · Stages of the power loop · 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 · The full machine as a finite multi-stack Turing machine · The composed machine, raw input to formula · Initial configuration of the full machine · Total length bound · 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 · Number of situations · Clause layout of a machine encoding · Window depth of a machine · Idle-extended run · Stack heights along a run · The idle-extended run follows the real run · Dense encoding of a CNF formula · Exact-length runs of a TM2 machine

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine

Output in time and polynomial-time computability

DefinitionA bounded halting run certifies the output#✓fully proved

Let \(M\) be a finite TM2 machine, \(l\) a list over its input alphabet, \(l'\) a list over its output alphabet and \(B \in \mathbb{N}\). If the program of \(M\) goes in at most \(B\) steps from the initial configuration on input \(l\) (its start label, its initial state, \(l\) on the input stack and every other stack empty) to the halting configuration with output \(l'\) (no label, the initial state, \(l'\) on the output stack and every other stack empty), then \(M\) outputs \(l'\) on input \(l\) within \(B\) steps.

noncomputable def outputsOfRunLe {tm : FinTM2} {l : List (tm.Γ tm.k₀)} {l' : List (tm.Γ tm.k₁)}
    {B : ℕ} (h : RunLe tm.m B (initList tm l) (haltList tm l')) :
    TM2OutputsInTime tm l (some l') B where
  steps := Classical.choose h
  evals_in_steps := (Classical.choose_spec h).2
  steps_le_m := (Classical.choose_spec h).1

Uses 2 · Used by 2

Statement usesExact-length runs of a TM2 machine · Runs within a step budget

Used byOne polynomial bounds the reduction machine · A bounded halting run certifies the output, up to an equal output

DefinitionA bounded halting run certifies the output, up to an equal output#✓fully proved

Let \(M\) be a finite TM2 machine, \(l\) a list over its input alphabet, \(l'\) and \(l''\) lists over its output alphabet and \(B \in \mathbb{N}\). If the program of \(M\) goes in at most \(B\) steps from the initial configuration on input \(l\) to the halting configuration with output \(l''\), and \(l'' = l'\), then \(M\) outputs \(l'\) on input \(l\) within \(B\) steps.

noncomputable def outputsOfRunLe' {tm : FinTM2} {l : List (tm.Γ tm.k₀)}
    {l' l'' : List (tm.Γ tm.k₁)} {B : ℕ} (h : RunLe tm.m B (initList tm l) (haltList tm l''))
    (he : l'' = l') : TM2OutputsInTime tm l (some l') B :=
  outputsOfRunLe (he ▸ h)

Uses 2 · Used by 1

Statement usesA bounded halting run certifies the output · Runs within a step budget

Used byThe reduction machine as a polynomial-time computation

TheoremOne polynomial bounds the reduction machine#✓fully proved

Fix \(r \in \mathbb{N}\), a finite TM2 machine \(M\) with an encoding \(E\), a list \(Y\) of input symbols of \(M\), an output symbol \(a\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input symbols, an input symbol \(\mathit{sep}\), a polynomial \(k\) with coefficients in \(\mathbb{N}\) and \(c, e \in \mathbb{N}\). There is a polynomial \(p\) with coefficients in \(\mathbb{N}\) such that for every raw input \(s\), a list over \(\{0, \dots, r-1\}\), the reduction machine on input \(s\) outputs the emitted formula for \(s\) within \(p(|s|)\) steps.

theorem g_outputs (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),
      Nonempty (TM2OutputsInTime (gTM E Ys acc ι sep k c e) s
        (some (phiOf E Ys acc ι sep k c e s)) (p.eval s.length))

Uses 28

Statement usesThe reduction machine · The formula emitted on a raw input · Encoding data for a finite TM2 machine

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 · Sorted certificate code list · Stacks to drain · Step bound of the composed machine · The reduction machine halts with the emitted formula · A bounded halting run certifies the output · Stacks of the full machine · Polynomial functions on the naturals · The Horner step count is polynomial · The precomputed time bound · Step budget of the counter program · Coefficient list of a polynomial · Step bound of the full machine · The full machine as a finite multi-stack Turing machine · Step count of the Horner rounds · Total length bound · Constant of the shift-generator time bound · Number of situations · Clause layout of a machine encoding · Window depth of a machine · Exact-length runs of a TM2 machine · Runs within a step budget

DefinitionThe Cook–Levin reduction function#✓fully proved

Fix \(r \in \mathbb{N}\), a finite TM2 machine \(M\) with an encoding \(E\), a list \(Y\) of input symbols of \(M\), an output symbol \(\mathrm{acc}\) of \(M\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input symbols of \(M\), an input symbol \(\mathit{sep}\) of \(M\), a polynomial \(k\) with coefficients in \(\mathbb{N}\) and \(c, e \in \mathbb{N}\). Let \(\mathit{ea}\) encode the elements of a type \(\alpha\) as lists over an alphabet \(\Sigma\), and let \(\mathit{eqv}\) be a bijection from \(\{0, \dots, r-1\}\) to \(\Sigma\). The reduction function sends \(u \in \alpha\) to the emitted formula for the raw input \(s\) obtained by applying \(\mathit{eqv}^{-1}\) to each symbol of \(\mathit{ea}(u)\): the dense encoding of the assembled Cook–Levin formula \(\Phi_E(x, Y, \mathrm{acc}, m, T)\), where \(x\) is \(s\) with each symbol mapped by \(\iota\), followed by \(\mathit{sep}\), \(m = |s| + 1 + k(|s|)\) and \(T = (m + c)^e\).

noncomputable def fR {α αΓ : Type} (ea : α → List αΓ) (eqv : Fin r ≃ αΓ)
    (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀) (sep : M.Γ M.k₀)
    (k : Polynomial ℕ) (c e : ℕ) (a : α) : List Bool :=
  phiOf E Ys acc ι sep k c e ((ea a).map eqv.invFun)

Uses 2 · Used by 4

Statement usesThe formula emitted on a raw input · Encoding data for a finite TM2 machine

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · The reduction machine as a polynomial-time computation · Every NP problem reduces to binary-index CNF-SAT

DefinitionThe reduction machine as a polynomial-time computation#✓fully proved

Fix \(r \in \mathbb{N}\), a finite TM2 machine \(M\) with an encoding \(E\), a list \(Y\) of input symbols of \(M\), an output symbol \(a\), a map \(\iota\) from \(\{0, \dots, r-1\}\) to input symbols, an input symbol \(\mathit{sep}\), a polynomial \(k\) with coefficients in \(\mathbb{N}\) and \(c, e \in \mathbb{N}\). Let \(\mathit{ea}\) encode the elements of a type \(\alpha\) as lists over an alphabet \(\Sigma\), and let \(\mathit{eqv}\) be a bijection from \(\{0, \dots, r-1\}\) to \(\Sigma\). This is a polynomial-time TM2 computation of the reduction function \(f_R\), which sends \(u \in \alpha\) to the emitted formula for the raw input obtained by applying \(\mathit{eqv}^{-1}\) to each symbol of \(\mathit{ea}(u)\), from the encoding \(\mathit{ea}\) to the identity encoding of bit strings: the machine is the reduction machine, its input alphabet is identified with \(\Sigma\) by \(\mathit{eqv}\), its output alphabet with the Booleans by the identity, and its time bound is a polynomial \(p\) with \(p(n) = g_B(n)\) for all \(n\), where \(g_B\) is the step bound of the composed machine.

noncomputable def gComp {α αΓ : Type} (ea : α → List αΓ) (eqv : Fin r ≃ αΓ)
    (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (ι : Fin r → M.Γ M.k₀) (sep : M.Γ M.k₀)
    (k : Polynomial ℕ) (c e : ℕ) :
    TM2ComputableInPolyTime ea (fun l : List Bool => l)
      (fR E ea eqv Ys acc ι sep k c e) where
  tm := gTM E Ys acc ι sep k c e
  inputAlphabet := eqv
  outputAlphabet := Equiv.refl Bool
  time := Classical.choose (gB_poly E Ys acc ι sep k c e)
  outputsFun a := outputsOfRunLe' (by
    have h := g_run E Ys acc ι sep k c e ((ea a).map eqv.invFun)
    rw [List.length_map, Classical.choose_spec (gB_poly E Ys acc ι sep k c e)] at h
    exact h) (List.map_id _).symm

Uses 28 · Used by 1

Statement 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 · Sorted certificate code list · Stacks to drain · The Cook–Levin reduction function · Step bound of the composed machine · The reduction machine · The reduction machine halts with the emitted formula · A bounded halting run certifies the output, up to an equal output · The formula emitted on a raw input · Stacks of the full machine · Polynomial functions on the naturals · The Horner step count is polynomial · The precomputed time bound · Step budget of the counter program · Coefficient list of a polynomial · Step bound of the full machine · The full machine as a finite multi-stack Turing machine · Step count of the Horner rounds · Total length bound · Constant of the shift-generator time bound · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Window depth of a machine · Runs within a step budget

Used byThe Cook–Levin reduction is polynomial-time

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.