Cook-Levin: the five generators as sub-machines of one host

22 fully proved

Host stacks and the five embeddings

InductiveStacks of the Cook–Levin host machine#✓fully proved

The host has a shared output stack, an input-code stack, and five private counter blocks: an update block and a situation-definition block, each with one stack per counter of the family generator, and a shift block, an accept block and an init block, with one stack per counter of the shift, accept and init generator respectively.

inductive HK
  | out
  | inp
  | up (x : Family.CK)
  | sd (x : Family.CK)
  | sh (x : Shift.CK)
  | ac (x : Accept.CK)
  | ini (x : InitFamily.CK)
  deriving DecidableEq, Fintype

Uses 4 · Used by 37

Statement usesCounters of the accept generator · Counters of the transition-family generator · Counters of the initial-row generator · Counters of the cell-shift generator

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 · Chaining step of the host program · Host stack renaming for the accept generator · Host stack renaming for the shift generator · Host stack renaming for the init generator · Host stack renaming for the situation-definition generator · Host stack renaming for the update generator · Embedding of the accept generator into the host · Embedding of the shift generator into the host · Embedding of the init generator into the host · Embedding of the situation-definition generator into the host · Embedding of the update generator's stacks into the host · Alphabets of the Cook–Levin host machine · The host as a finite multi-stack Turing machine · The host program · The host on the real generators of a machine · The assembled generator, after the precomputation · Sequencing · Stack renaming of the counter program · Embedding of the counter program's stacks · Embedding of the host's stacks · Alphabets of the full machine · Stacks of the full machine · The full program · 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 · Host counter of each target

AbbreviationAlphabets of the Cook–Levin host machine#✓fully proved

For \(g \in \mathbb{N}\), the host stacks carry the following alphabets: the shared output stack holds Booleans, the input-code stack holds codes in \(\{0, \dots, g - 1\}\), and every stack of every private counter block has a one-element alphabet.

abbrev HΓ (g : ℕ) : HK → Type
  | .out => Bool
  | .inp => Fin g
  | .up _ => Unit
  | .sd _ => Unit
  | .sh _ => Unit
  | .ac _ => Unit
  | .ini _ => Unit

Uses 5 · Used by 16

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 · Counters of the cell-shift generator

Used byChaining step of the host program · Embedding of the accept generator into the host · Embedding of the shift generator into the host · Embedding of the init generator into the host · Embedding of the situation-definition generator into the host · Embedding of the update generator's stacks into the host · The host as a finite multi-stack Turing machine · The host program · The host on the real generators of a machine · The assembled generator, after the precomputation · Sequencing · Embedding of the host's stacks · Alphabets of the full machine · The full program · The composed machine, raw input to formula · The precomputation

DefinitionHost stack renaming for the update generator#✓fully proved

The map from the stacks of the clause-family generator, used as the update generator, to the host stacks that sends the output stack to the shared output stack and the counter stack of each counter \(x\) to the counter \(x\) of the host's update block.

def eU : Family.GK → HK
  | .out => .out
  | .c x => .up x

Uses 4 · Used by 1

Statement usesStacks of the Cook–Levin host machine · Stacks of a counter machine · Counters of the transition-family generator · Stacks of the clause-family generator

Used byEmbedding of the update generator's stacks into the host

DefinitionHost stack renaming for the situation-definition generator#✓fully proved

The map from the stacks of the clause-family generator, used as the situation-definition generator, to the host stacks that sends the output stack to the shared output stack and the counter stack of each counter \(x\) to the counter \(x\) of the host's situation-definition block.

def eS : Family.GK → HK
  | .out => .out
  | .c x => .sd x

Uses 4 · Used by 1

Statement usesStacks of the Cook–Levin host machine · Stacks of a counter machine · Counters of the transition-family generator · Stacks of the clause-family generator

Used byEmbedding of the situation-definition generator into the host

DefinitionHost stack renaming for the shift generator#✓fully proved

The map from the stacks of the shift generator to the host stacks that sends the output stack to the shared output stack and the counter stack of each shift counter \(x\) to the counter \(x\) of the host's shift block.

def eH : SK Shift.CK → HK
  | .out => .out
  | .c x => .sh x

Uses 3 · Used by 1

Statement usesStacks of the Cook–Levin host machine · Stacks of a counter machine · Counters of the cell-shift generator

Used byEmbedding of the shift generator into the host

DefinitionHost stack renaming for the accept generator#✓fully proved

The map from the stacks of the accept generator to the host stacks that sends the output stack to the shared output stack and the counter stack of each accept counter \(x\) to the counter \(x\) of the host's accept block.

def eA : SK Accept.CK → HK
  | .out => .out
  | .c x => .ac x

Uses 3 · Used by 1

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Stacks of a counter machine

Used byEmbedding of the accept generator into the host

DefinitionHost stack renaming for the init generator#✓fully proved

The map from the stacks of the init generator to the host stacks that sends the output stack to the shared output stack, the input stack to the host's input-code stack, and the counter stack of each init counter \(x\) to the counter \(x\) of the host's init block.

def eI : IK InitFamily.CK → HK
  | .b .out => .out
  | .b (.c x) => .ini x
  | .inp => .inp

Uses 4 · Used by 1

Statement usesStacks of the Cook–Levin host machine · Stacks of a counter machine · Counters of the initial-row generator · Stacks of a counter machine with an input stack

Used byEmbedding of the init generator into the host

DefinitionEmbedding of the update generator's stacks into the host#✓fully proved

For \(g \in \mathbb{N}\), this is the stack embedding of the family generator's stacks (a Boolean output stack and one unit counter stack per counter) into the host stacks with \(g\) input codes, used for the update generator: the output stack goes to the host's shared output stack, and the counter stack \(x\) goes to the stack \(x\) of the host's private update block. Distinct stacks go to distinct host stacks, and each stack's alphabet is identified with its host stack's alphabet by the identity.

def embU : SEmb Family.GΓ (HΓ g) where
  e := eU
  inj := by intro a b h; cases a <;> cases b <;> simp_all [eU]
  ι := fun k => match k with
    | .out => Equiv.refl _
    | .c _ => Equiv.refl _

Uses 10 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Host stack renaming for the update generator · Stacks of a counter machine · Counters of the transition-family generator · Stack alphabets of the generator · Counters of the initial-row generator · Counters of the cell-shift generator · Stack embedding

Used byThe host program · Sequencing

DefinitionEmbedding of the situation-definition generator into the host#✓fully proved

For \(g\) input codes, the stack embedding of the clause-family generator's stacks, used as the situation-definition generator, into the host stacks that sends the output stack to the shared output stack and the counter stack of each counter \(x\) to the counter \(x\) of the host's situation-definition block, identifying each stack's alphabet with itself.

def embS : SEmb Family.GΓ (HΓ g) where
  e := eS
  inj := by intro a b h; cases a <;> cases b <;> simp_all [eS]
  ι := fun k => match k with
    | .out => Equiv.refl _
    | .c _ => Equiv.refl _

Uses 10 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Host stack renaming for the situation-definition generator · Stacks of a counter machine · Counters of the transition-family generator · Stack alphabets of the generator · Counters of the initial-row generator · Counters of the cell-shift generator · Stack embedding

Used byThe host program · Sequencing

DefinitionEmbedding of the shift generator into the host#✓fully proved

For \(g\) input codes, the stack embedding of the shift generator's stacks into the host stacks that sends the output stack to the shared output stack and the counter stack of each shift counter \(x\) to the counter \(x\) of the host's shift block, identifying each stack's alphabet with itself.

def embH : SEmb (SΓ Shift.CK) (HΓ g) where
  e := eH
  inj := by intro a b h; cases a <;> cases b <;> simp_all [eH]
  ι := fun k => match k with
    | .out => Equiv.refl _
    | .c _ => Equiv.refl _

Uses 10 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Host stack renaming for the shift generator · 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 cell-shift generator · Stack embedding

Used byThe host program · Sequencing

DefinitionEmbedding of the accept generator into the host#✓fully proved

For \(g\) input codes, the stack embedding of the accept generator's stacks into the host stacks that sends the output stack to the shared output stack and the counter stack of each accept counter \(x\) to the counter \(x\) of the host's accept block, identifying each stack's alphabet with itself.

def embA : SEmb (SΓ Accept.CK) (HΓ g) where
  e := eA
  inj := by intro a b h; cases a <;> cases b <;> simp_all [eA]
  ι := fun k => match k with
    | .out => Equiv.refl _
    | .c _ => Equiv.refl _

Uses 10 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Host stack renaming for the accept generator · 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 cell-shift generator · Stack embedding

Used byThe host program · Sequencing

DefinitionEmbedding of the init generator into the host#✓fully proved

For \(g\) input codes, the stack embedding of the init generator's stacks (with input alphabet the \(g\) codes) into the host stacks that sends the output stack to the shared output stack, the input stack to the host's input-code stack, and the counter stack of each init counter \(x\) to the counter \(x\) of the host's init block, identifying each stack's alphabet with itself.

def embI : SEmb (IΓ InitFamily.CK (Fin g)) (HΓ g) where
  e := eI
  inj := by
    intro a b h
    rcases a with (_ | a) | _ <;> rcases b with (_ | b) | _ <;> simp_all [eI]
  ι := fun k => match k with
    | .b .out => Equiv.refl _
    | .b (.c _) => Equiv.refl _
    | .inp => Equiv.refl _

Uses 11 · Used by 2

Statement usesCounters of the accept generator · Stacks of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · Host stack renaming for the init generator · Stacks of a counter machine · Counters of the transition-family generator · Counters of the initial-row generator · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · Counters of the cell-shift generator · Stack embedding

Used byThe host program · Sequencing

The host program and the sequencing theorem

InductiveLabels of the Cook–Levin host machine#✓fully proved

For parameters \(N, n_L, K, g, d, n_1, n_Y\), the host labels consist of a copy of the family generator's labels (for \(N\) situations and \(n_L\) literals) for the update phase, a second copy of them for the situation-definition phase, a copy of the shift generator's labels (for \(N\) situations, \(K\) stacks, \(g\) symbols and depth \(d\)), a copy of the accept generator's labels (for \(n_1\) code clauses and \(g\) symbols), a copy of the init generator's labels (for \(g\) symbols and \(n_Y\) certificate codes), and one final label.

inductive HL (N nL KK g d n1 ny : ℕ)
  | up (l : Family.GL N nL)
  | sd (l : Family.GL N nL)
  | sh (l : Shift.GL N KK g d)
  | ac (l : Accept.GL n1 g)
  | ini (l : InitFamily.GL g ny)
  | fin
  deriving DecidableEq, Fintype

Uses 4 · Used by 13

Statement usesLabels of the accept generator · Labels of the clause-family generator · Labels of the initial-row generator · Labels of the cell-shift generator

Used byThe reduction machine halts with the emitted formula · The reduction machine · Chaining step of the host program · The host as a finite multi-stack Turing machine · The host program · The host on the real generators of a machine · The assembled generator, after the precomputation · Sequencing · 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

DefinitionChaining step of the host program#✓fully proved

For a host label \(l\), the chaining step is the host statement that sets the Boolean internal state to false (the state in which every generator starts) and then jumps to \(l\).

def chain (l : HL N nL KK g d n1 ny) : TM2.Stmt (HΓ g) (HL N nL KK g d n1 ny) Bool :=
  .load (fun _ => false) (.goto fun _ => l)

Uses 3 · Used by 2

Statement usesStacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine

Used byThe host program · Sequencing

DefinitionThe host program#✓fully proved

Given the five generator programs (update, situation definition, shift, accept and init), the host program runs init, then update, then situation definition, then shift, then accept. At each label of a generator other than its final label, the host executes that generator's statement with the generator's stacks embedded into the host stacks (output onto the shared output stack, counters onto the generator's own private counter block, and for init the input stack onto the host's input-code stack) and its labels renamed into the host's copy of them. At a generator's final label the host performs one chaining step: it resets the Boolean state to false and jumps to the start label of the next generator, and after accept it jumps to the final host label, where it halts.

def hprog : HL N nL KK g d n1 ny → TM2.Stmt (HΓ g) (HL N nL KK g d n1 ny) Bool
  | .ini l => if l = .done then chain (.up (.pre .eg)) else mapS (embI g) HL.ini (Pi l)
  | .up l => if l = .done then chain (.sd (.pre .eg)) else mapS (embU g) HL.up (Pu l)
  | .sd l => if l = .done then chain (.sh (.pre .eg)) else mapS (embS g) HL.sd (Ps l)
  | .sh l => if l = .done then chain (.ac (.pre .eg)) else mapS (embH g) HL.sh (Ph l)
  | .ac l => if l = .done then chain .fin else mapS (embA g) HL.ac (Pa l)
  | .fin => .halt

Uses 39 · Used by 4

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 · Alphabets of the Cook–Levin host machine · Chaining step of the host program · Embedding of the accept generator into the host · Embedding of the shift generator into the host · Embedding of the init generator into the host · Embedding of the situation-definition generator into the host · Embedding of the update generator's stacks into the host · Stages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Counters of the transition-family generator · Labels of the clause-family generator · Stack alphabets of the generator · Stages of the transition-clause generator's literal routine · 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 · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · 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 · 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 · Translating a statement along a stack embedding

Used byThe host as a finite multi-stack Turing machine · The host on the real generators of a machine · The assembled generator, after the precomputation · Sequencing

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

Given the five generator programs (update and situation-definition programs over the family generator's stacks, a shift program, an accept program, and an init program whose input alphabet has \(g\) codes), the host machine is the finite multi-stack Turing machine whose stacks are the host stacks, with the input-code stack as input stack and the shared output stack as output stack, whose alphabets are the host alphabets, whose labels are the host labels, whose start label is the init generator's start label, whose internal state is a Boolean with initial value false, and whose program is the host program built from the five generator programs.

This is a finiteness check only: the input and output stacks are provisional until the precomputation is attached.

def hostTM : FinTM2 where
  K := HK
  k₀ := .inp
  k₁ := .out
  Γ := HΓ g
  Λ := HL N nL KK g d n1 ny
  main := .ini (.pre1 .eg)
  σ := Bool
  initialState := false
  m := hprog Pu Ps Ph Pa Pi

Uses 33

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 · Alphabets of the Cook–Levin host machine · The host program · Stages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Counters of the transition-family generator · Labels of the clause-family generator · Stack alphabets of the generator · Stages of the transition-clause generator's literal routine · 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 · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · 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 · 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

TheoremSequencing#✓fully proved

Let \(P_u\), \(P_s\) (update and situation definition), \(P_h\) (shift), \(P_a\) (accept) and \(P_i\) (init) be generator programs that halt at their label done, and let \(\xi\) be a list of input codes. Suppose that for each generator \(j \in \{u, s, h, a, i\}\) there are counter values \(F_j\), a word \(w_j\) and a bound \(B_j\) such that, for every output word \(o\), the run of \(P_j\) from its start label with state bit false, on stacks holding the counters \(F_j\) and the output \(o\) (for init, also \(\xi\) on its input stack), reaches done within \(B_j\) steps, with some state bit and with output \(w_j o\). Let \(o\) be a word and let \(S_0\) be host stacks whose output stack holds \(o\), whose input stack holds \(\xi\), and whose private block of each generator \(j\) holds the counters \(F_j\). Then the host program on \(P_u, P_s, P_h, P_a, P_i\), started at the init generator's start label with state bit false on \(S_0\), reaches its final label within \(B_i + B_u + B_s + B_h + B_a + 5\) steps, with some state bit and with output \(w_a w_h w_s w_u w_i o\).

Cslib.Complexity.CookLevin.Assembly.seq_run · 23 lines

theorem seq_run (hu0 : Pu .done = .halt) (hs0 : Ps .done = .halt) (hh0 : Ph .done = .halt)
    (ha0 : Pa .done = .halt) (hi0 : Pi .done = .halt)
    {Fu Fs : Family.CK → ℕ} {Fh : Shift.CK → ℕ} {Fa : Accept.CK → ℕ} {Fi : InitFamily.CK → ℕ}
    {xs : List (Fin g)} {wu ws wh wa wi : List Bool} {Bu Bs Bh Ba Bi : ℕ}
    (hu : ∀ o, ∃ (v : Bool) (S : ∀ k, List (Family.GΓ k)),
      RunLe Pu Bu ⟨some (.pre .eg), false, CounterView.st Fu o⟩ ⟨some .done, v, S⟩ ∧ S .out = wu ++ o)
    (hs : ∀ o, ∃ (v : Bool) (S : ∀ k, List (Family.GΓ k)),
      RunLe Ps Bs ⟨some (.pre .eg), false, CounterView.st Fs o⟩ ⟨some .done, v, S⟩ ∧ S .out = ws ++ o)
    (hh : ∀ o, ∃ (v : Bool) (S : ∀ k, List (SΓ Shift.CK k)),
      RunLe Ph Bh ⟨some (.pre .eg), false, CounterView.st Fh o⟩ ⟨some .done, v, S⟩ ∧ S .out = wh ++ o)
    (ha : ∀ o, ∃ (v : Bool) (S : ∀ k, List (SΓ Accept.CK k)),
      RunLe Pa Ba ⟨some (.pre .eg), false, CounterView.st Fa o⟩ ⟨some .done, v, S⟩ ∧ S .out = wa ++ o)
    (hi : ∀ o, ∃ (v : Bool) (S : ∀ k, List (IΓ InitFamily.CK (Fin g) k)),
      RunLe Pi Bi ⟨some (.pre1 .eg), false, emb (CounterView.st Fi o) xs⟩ ⟨some .done, v, S⟩ ∧
        S (.b .out) = wi ++ o)
    (S₀ : ∀ k, List (HΓ g k)) (o : List Bool) (ho : S₀ .out = o) (hin : S₀ .inp = xs)
    (cu : ∀ x, S₀ (.up x) = cnt () (Fu x)) (cs : ∀ x, S₀ (.sd x) = cnt () (Fs x))
    (ch : ∀ x, S₀ (.sh x) = cnt () (Fh x)) (ca : ∀ x, S₀ (.ac x) = cnt () (Fa x))
    (ci : ∀ x, S₀ (.ini x) = cnt () (Fi x)) :
    ∃ (v : Bool) (S : ∀ k, List (HΓ g k)),
      RunLe (hprog Pu Ps Ph Pa Pi) (Bi + Bu + Bs + Bh + Ba + 5)
        ⟨some (.ini (.pre1 .eg)), false, S₀⟩ ⟨some .fin, v, S⟩ ∧
      S .out = wa ++ (wh ++ (ws ++ (wu ++ (wi ++ o))))

Uses 51 · Used by 1

Statement usesCounters of the accept generator · Labels of the accept generator · Precomputation stages of the accept generator · Stacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · The host program · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Counters of the transition-family generator · Labels of the clause-family generator · Stack alphabets of the generator · Stages of the transition-clause generator's precomputation · Counters of the initial-row generator · Labels of the initial-row generator · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · Labels of the first precomputation part · Stacks of a counter machine with an extra input stack · Counters of the cell-shift generator · Labels of the cell-shift generator · Precomputation stages of the shift generator · Runs within a step budget · Unary counter

Proof usesClause kinds of the accept generator · Stages of the accept generator's literal routine · Chaining step of the host program · Embedding of the accept generator into the host · Embedding of the shift generator into the host · Embedding of the init generator into the host · Embedding of the situation-definition generator into the host · Embedding of the update generator's stacks into the host · Stages of the multiplication routine · Stages of the transition-clause generator's literal routine · Clause kinds of the initial-row generator · Stages of the literal routine (initial-row generator) · Loop phases of the initial-row generator · Labels of the second precomputation part · Loop-body stages of the cell-shift generator · Clause kinds of the cell-shift family · Stages of the cell-shift literal routine · Setup and loop stages of a cell-shift block · 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 assembled generator, after the precomputation

The host on the five real generators of a machine

AbbreviationThe host on the real generators of a machine#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with encoding data \(E\), let \(Y\) be a list of input symbols, and let \(\mathit{acc}\) be an output symbol. This is the host program whose five generators are the real ones for \(M\). The update generator is the family generator of \(E\) for the (label, state) codes, window codes and next (label, state) codes of the situations of \(E\). The situation-definition generator is the family generator of \(E\) for the same (label, state) codes and window codes, with the positions of the situation variables in place of the next codes. The shift generator is the one of \(E\). The accept generator is the one for the number of (label, state) codes, the code of the halted label with the initial internal state, the number of the output stack, and the code of \(\mathit{acc}\) on the output stack. The init generator is the one for the code of the start label and initial state of \(M\), the number of the input stack, and the sorted distinct codes of the symbols of \(Y\). The input itself is not a parameter: the init generator reads it from the host's input-code stack.

noncomputable abbrev realProg (Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) :=
  hprog (Family.prog E.layout E.la E.na E.wa E.N) (Family.prog E.layout E.la E.sa E.wa E.N)
    (Shift.prog E.layout E.sa E.pl E.cn E.pu E.N)
    (Accept.prog E.layout E.A0 E.acode (E.kc M.k₁) (E.enc M.k₁ acc))
    (InitFamily.iprog E.layout (E.lc (some M.main,
        M.initialState)) (E.kc M.k₀) (InitFamily.ycs E Ys))

Uses 22 · Used by 3

Statement usesGenerator machine for the accept family · Stacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · The host program · Variable layout of the transition clauses · Number of literals of a transition clause · Generator machine for the transition clause families · The initial-row generator · Sorted certificate code list · The cell-shift generator · Encoding data for a finite TM2 machine · Number of situations · Accepting code · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation

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

DefinitionThe formula emitted by the host#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with encoding data \(E\), let \(x\) and \(Y\) be lists of input symbols, let \(\mathit{acc}\) be an output symbol, and let \(m, T \in \mathbb{N}\). Let \(H = m + (T + 1) d + 1\) be the stack cap, where \(d\) is the window depth of \(M\). The CNF formula \(\Phi(x, Y, \mathit{acc}, m, T)\) is the concatenation, in this order, of the accept family for \(\mathit{acc}\), the shift family, the situation-definition family, the update family, and the init family for \(x\), \(Y\) and \(m\), all at run length \(T\) and stack cap \(H\).

noncomputable def Phi (x Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (m T : ℕ) : CNF :=
  E.accFamily acc T (capH m T (depth M)) ++
    (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M)) ++
      (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N ++
        (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N ++
          E.initFamily x Ys m T (capH m T (depth M)))))

Uses 18 · Used by 9

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Number of situations · The accept family · Consumption table of a situation · The row-0 init family of an encoding · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Stack cap · Window depth of a machine · Dense CNF formula · Dense clause

Used byCorrectness of the reduction · The reduction machine halts with the emitted formula · The formula emitted on a raw input · Correctness of the assembled formula · The assembled generator, after the precomputation · The composed machine, raw input to formula · Polynomial time bound of the composed machine · Every clause of the Cook–Levin formula has one slot per variable · Every NP problem reduces to binary-index CNF-SAT

DefinitionStep bound of the host#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with encoding data \(E\), let \(Y\) be a list of input symbols, and let \(m, T \in \mathbb{N}\). Let \(H = m + (T + 1) d + 1\), where \(d\) is the window depth of \(M\), and let \(R = T + H + 1\). Let \(L\) be the layout of \(E\) and \(N\) its number of situations. Let \(c_I\) be the init generator's constant for \(L\), the number of distinct codes of symbols of \(Y\), and the number of the input stack; let \(c_F\) be the family generator's constant for \(L\) and \(N\); let \(c_S\) be the shift generator's constant for \(L\) and \(N\); and let \(c_A\) be the accept generator's constant for \(L\), the number of (label, state) codes, and the number of the output stack. The step bound is

\[c_I R^5 + c_F R^5 + c_F R^5 + c_S R^6 + c_A R^4 + 5,\]

the bounds of the init, update, situation-definition, shift and accept generators plus five chaining steps.

noncomputable def realB (Ys : List (M.Γ M.k₀)) (m T : ℕ) : ℕ :=
  InitFamily.initC E.layout (InitFamily.ycs E Ys).length (E.kc M.k₀) * (T + capH m T (depth M) + 1) ^ 5 +
    Family.genC E.layout E.N * (T + capH m T (depth M) + 1) ^ 5 +
    Family.genC E.layout E.N * (T + capH m T (depth M) + 1) ^ 5 +
    Shift.shC E.layout E.N * (T + capH m T (depth M) + 1) ^ 6 +
    Accept.accC E.layout E.A0 (E.kc M.k₁) * (T + capH m T (depth M) + 1) ^ 4 + 5

Uses 10 · Used by 6

Statement usesConstant of the accept generator's time bound · Constant of the generator's time bound · Constant of the init generator's time bound · Sorted certificate code list · Constant of the shift-generator time bound · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Stack cap · Window depth of a machine

Used byThe reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The assembled generator, after the precomputation · Step bound of the full machine · The composed machine, raw input to formula · Polynomial time bound of the composed machine

TheoremThe assembled generator, after the precomputation#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of input symbols of \(M\), let \(a\) be a symbol of its output stack, and let \(m, T \in \mathbb{N}\) with \(|x| \le m\). Put \(H = m + (T + 1)d + 1\), where \(d\) is the window depth of \(M\). Let \(S_0\) be host stacks whose output stack holds a word \(o\), whose input stack holds the symbol codes of \(x\) in reverse order, whose update, situation-definition, shift and accept blocks each hold \(T\) on the time counter, \(H\) on the height counter and nothing on the other counters, and whose init block holds \(T\), \(|x|\), \(m - |x|\) and \(H - m\) on its four size counters and nothing on the others. Then the host program on the real generators of \(E\) for \(Y\) and \(a\), started at the init generator's start label with state bit false on \(S_0\), reaches its final label within the step bound \(\mathrm{realB}(E, Y, m, T)\) (the five generators' bounds plus five chaining steps), with some state bit and with output stack the dense encoding of the formula \(\Phi(E, x, Y, a, m, T)\) followed by \(o\).

theorem real_run (x Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (m T : ℕ) (hx : x.length ≤ m)
    (S₀ : ∀ k, List (HΓ E.layout.g k)) (o : List Bool) (ho : S₀ .out = o)
    (hin : S₀ .inp = (x.map (InitFamily.encF E)).reverse)
    (cu : ∀ z, S₀ (.up z) = cnt () (Family.initF T (capH m T (depth M)) z))
    (cs : ∀ z, S₀ (.sd z) = cnt () (Family.initF T (capH m T (depth M)) z))
    (ch : ∀ z, S₀ (.sh z) = cnt () (Shift.initF T (capH m T (depth M)) z))
    (ca : ∀ z, S₀ (.ac z) = cnt () (Accept.initF T (capH m T (depth M)) z))
    (ci : ∀ z, S₀ (.ini z) = cnt () (InitFamily.initF T x.length (m - x.length)
      (capH m T (depth M) - m) z)) :
    ∃ (v : Bool) (S : ∀ k, List (HΓ E.layout.g k)),
      RunLe (realProg E Ys acc) (realB E Ys m T)
        ⟨some (.ini (.pre1 .eg)), false, S₀⟩ ⟨some .fin, v, S⟩ ∧
      S .out = encodeCNF (Phi E x Ys acc m T) ++ o

Uses 66 · Used by 1

Statement usesCounters of the accept generator · Initial counters of the accept generator · Stacks of the Cook–Levin host machine · Labels of the Cook–Levin host machine · Alphabets of the Cook–Levin host machine · The formula emitted by the host · Step bound of the host · The host on the real generators of a machine · Counters of the transition-family generator · Variable layout of the transition clauses · Number of literals of a transition clause · Initial counters of the transition-clause generator · Counters of the initial-row generator · Labels of the initial-row generator · Labels of the first precomputation part · Codes of input symbols · Initial counters of the init generator · Sorted certificate code list · Counters of the cell-shift generator · Initial counter values of the shift generator · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Stack cap · Window depth of a machine · Dense encoding of a CNF formula · Runs within a step budget · Unary counter

Proof usesLabels of the accept generator · Constant of the accept generator's time bound · Time bound of the accept generator for a concrete machine · Generator machine for the accept family · The host program · Sequencing · Stacks of a counter machine · Alphabets of a counter machine · Labels of the clause-family generator · Stack alphabets of the generator · The transition clause family · Constant of the generator's time bound · Generator machine for the transition clause families · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · Constant of the init generator's time bound · The init generator at the stack cap · The initial-row generator · Labels of the cell-shift generator · The cell-shift generator · Constant of the shift-generator time bound · The cell-shift clause family · The accept family · Accepting code · Consumption table of a situation · The row-0 init family of an encoding · Label/state code of a situation · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Time bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · Time bound of the transition-clause generator on the tables of a machine · Dense CNF formula · Dense clause · Dense encoding of a clause

Used byThe composed machine, raw input to formula

TheoremCorrectness of the assembled formula#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with encoding data \(E\), let \(x\) and \(Y\) be lists of input symbols of \(M\), let \(\mathit{acc}\) be an output symbol of \(M\), and let \(m, T \in \mathbb{N}\). Suppose that \(|x| \le m\) and that \(\mathit{acc}\) is one of the effective symbols of the output stack under \(E\). Then the formula \(\Phi(x, Y, \mathit{acc}, m, T)\) emitted by the host is satisfiable if and only if there is a list \(y\) of input symbols, all belonging to \(Y\), such that the concatenation \(xy\) has length at most \(m\) and the idle-extended run of \(M\) from the initial configuration on input \(xy\) is, after \(T\) steps, an accepting configuration for \(\mathit{acc}\): halted, in the initial internal state, with \(\mathit{acc}\) on top of the output stack.

The proof carries the soundness and completeness of the five families through the concatenation.

theorem phi_iff {x Ys : List (M.Γ M.k₀)} {acc : M.Γ M.k₁} {m T : ℕ} (hx : x.length ≤ m)
    (hacc : ∃ i, E.dec M.k₁ i = acc) :
    (∃ a, cnfSat (Phi E x Ys acc m T) a) ↔
      ∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧
        Accepts M (runI M (initList M (x ++ y)) T) acc

Uses 24 · Used by 1

Statement usesThe formula emitted by the host · Accepting configuration · Encoding data for a finite TM2 machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesThe transition clause family · The cell-shift clause family · Number of situations · The accept family · Consumption table of a situation · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The row-0 init family of an encoding · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Stack cap · Satisfying a concatenation of CNF formulas · Window depth of a machine · Dense CNF formula · Dense clause

Used byCorrectness of the reduction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.