Cook-Levin: generator machine for the accept family

36 fully proved

The family (pure specification)

DefinitionLiterals of an accept code clause#✓fully proved

For a layout \(L\), a code \(a_c\), a time \(T\), a height \(H\) and \(u \in \mathbb{N}\), the literal list of code clause \(u\) is the single literal whose variable is the label/state variable \(X[T, u]\) (entry \(u\) of the label/state block at time \(T\), for height \(H\)) and which is positive exactly when \(u = a_c\).

def codeLits (T H u : ℕ) : List (ℕ × Bool) := [(L.xIdx H T u, decide (u = ac))]

Uses 2 · Used by 1

Statement usesVariable layout of the transition clauses · Index of a label/state variable

Used byThe accept family of a layout

DefinitionLiterals of an accept cell clause#✓fully proved

For a layout \(L\), a stack \(k_1\), a symbol code \(e_a\), a time \(T\), a height \(H\) and \(x \in \mathbb{N}\), the literal list of cell clause \(x\) is the single literal whose variable is the cell variable \(C[T, k_1, 0, x]\) (time \(T\), stack \(k_1\), depth \(0\) from the top, symbol code \(x\), for height \(H\)) and which is positive exactly when \(x = e_a\).

def cellLits (T H x : ℕ) : List (ℕ × Bool) := [(L.cIdx H T k1 0 x, decide (x = ea))]

Uses 2 · Used by 1

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout

Used byThe accept family of a layout

DefinitionThe accept family of a layout#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(n_1, a, k_1, e, T, H\) be natural numbers, \(W = A + K H g\) and \(V = (T + 1) W\). The accept family is the CNF formula over \(V\) variables made of, first, for each \(u < n_1\) in increasing order, the clause whose only literal is the label variable \(X[T, u]\) (variable \(T W + u\)), positive if \(u = a\) and negative otherwise; then, for each \(x < g\) in increasing order, the clause whose only literal is the top-cell variable \(C[T, k_1, 0, x]\) of stack \(k_1\) (variable \(T W + A + k_1 H g + x\)), positive if \(x = e\) and negative otherwise. Each clause is a dense row of \(V\) slots: the slot of its variable holds the literal and every other slot is empty (all slots are empty if the variable is at least \(V\)).

def accFam (T H : ℕ) : CNF :=
  (List.range n1).map (fun u => denseClause (L.numVars T H) (codeLits L ac T H u)) ++
    (List.range L.g).map (fun x => denseClause (L.numVars T H) (cellLits L k1 ea T H x))

Uses 7 · Used by 3

Statement usesLiterals of an accept cell clause · Literals of an accept code clause · Variable layout of the transition clauses · Number of variables of the transition-clause formula · Dense clause from a list of literals · Dense CNF formula · Dense clause

Used byThe concrete accept family is a layout-level accept family · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator

The generator machine

InductiveCounters of the accept generator#✓fully proved

The accept-family generator has sixteen distinct unit counters, named \(\mathsf{Tn}\), \(\mathsf{Hs}\), \(\mathsf{Gc}\), \(\mathsf{HG}\), \(\mathsf{Wc}\), \(\mathsf{Kc}\), \(\mathsf{K1}\), \(\mathsf{Vc}\), \(\mathsf{TW}\), \(\mathsf{CB}\), \(\mathsf{P}\), \(\mathsf{Q}\), \(\mathsf{tmp}\), \(\mathsf{md}\), \(\mathsf{c1}\) and \(\mathsf{c2}\).

inductive CK
  | Tn | Hs | Gc | HG | Wc | Kc | K1 | Vc | TW | CB | P | Q | tmp | md | c1 | c2
  deriving DecidableEq

Used by 41

Used byTime bound of the accept generator for a concrete machine · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · The accept generator as a finite multi-stack machine · Base counter of an accept clause · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Initial counters of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Counters after the precomputation of the accept generator · Run of the accept generator's precomputation · Generator machine for the accept family · Empty scratch counters of the accept generator · Stacks 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 · Host stack renaming for the accept 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 · Stacks of the Cook–Levin host machine · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing · Embedding of the counter program's stacks · 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's run · Host counter of each target

InductiveClause kinds of the accept generator#✓fully proved

For natural numbers \(n_1\) and \(g\), a clause kind is either a code clause \(u\) for some \(u < n_1\) or a cell clause \(x\) for some \(x < g\).

inductive AK (n1 g : ℕ)
  | code (u : Fin n1)
  | cell (x : Fin g)
  deriving DecidableEq, Fintype

Used by 20

Used byThe accept generator as a finite multi-stack machine · Base counter of an accept clause · Entry label of an accept cell clause · Run of the accept cell chain · One clause of the accept generator · Entry label of an accept code clause · Run of the code-clause chain of the accept generator · Labels of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Next label after a clause of the accept generator · Offset of a clause's literal · Generator machine for the accept family · Polarity of an accept clause's literal · The reduction machine halts with the emitted formula · The reduction machine · The host as a finite multi-stack Turing machine · The host program · Sequencing · The full machine as a finite multi-stack Turing machine

DefinitionBase counter of an accept clause#✓fully proved

For a clause kind \(c\) of the accept generator, the base counter of its single literal is the counter \(\mathsf{TW}\) when \(c\) is a code clause and the counter \(\mathsf{CB}\) when \(c\) is a cell clause.

def bc : AK n1 g → CK
  | code _ => .TW
  | cell _ => .CB

Uses 2 · Used by 5

Statement usesClause kinds of the accept generator · Counters of the accept generator

Used byRun of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator

DefinitionOffset of a clause's literal#✓fully proved

For \(n_1, g \in \mathbb{N}\), the offset of a clause kind of the accept generator is its index: \(u\) for the code clause \(u < n_1\) and \(x\) for the cell clause \(x < g\). It is the distance of the clause's single literal from its base counter.

def off : AK n1 g → ℕ
  | code u => u
  | cell x => x

Uses 1 · Used by 5

Statement usesClause kinds of the accept generator

Used byRun of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator

DefinitionPolarity of an accept clause's literal#✓fully proved

Fix naturals \(n_1\) and \(g\), and let \(a\) and \(e\) be naturals. The polarity of the code clause of \(u < n_1\) is true exactly when \(u = a\), and the polarity of the cell clause of \(x < g\) is true exactly when \(x = e\).

def sg (ac ea : ℕ) : AK n1 g → Bool
  | code u => decide (u.val = ac)
  | cell x => decide (x.val = ea)

Uses 1 · Used by 5

Statement usesClause kinds of the accept generator

Used byRun of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator

InductivePrecomputation stages of the accept generator#✓fully proved

Write \(A\), \(K\) and \(g\) for the label/state block size, the number of stacks and the number of symbol codes of the generator's layout, and \(k_1\) for the index of the stack whose top cell it checks. A precomputation stage is one of eight plain stages or one of five multiplication stages, each of which carries a stage \(s\) of the multiplication routine. Named by the step the generator takes there, in the order it runs them, they are: push \(g\) units on \(\mathsf{Gc}\); multiply into \(\mathsf{HG}\) at \(s\); push \(A\) units on \(\mathsf{Wc}\); push \(K\) units on \(\mathsf{Kc}\); multiply into \(\mathsf{Wc}\) at \(s\); multiply into \(\mathsf{TW}\) at \(s\); increment \(\mathsf{Tn}\); multiply into \(\mathsf{Vc}\) at \(s\); drain \(\mathsf{TW}\) onto both \(\mathsf{CB}\) and \(\mathsf{tmp}\); drain \(\mathsf{tmp}\) back onto \(\mathsf{TW}\); push \(A\) units on \(\mathsf{CB}\); push \(k_1\) units on \(\mathsf{K1}\); multiply into \(\mathsf{CB}\) at \(s\).

inductive PS
  | eg | hg (s : MS) | ew | ek | w (s : MS) | tw (s : MS) | inc | v (s : MS)
  | cb1 | cb2 | cbA | k1 | cbM (s : MS)
  deriving DecidableEq, Fintype

Uses 1 · Used by 13

Statement usesStages of the multiplication routine

Used byTime bound of the accept generator for a concrete machine · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · The accept generator as a finite multi-stack machine · Labels of the accept generator · Run of the accept generator's precomputation · Generator machine for the accept family · The reduction machine halts with the emitted formula · The reduction machine · The host as a finite multi-stack Turing machine · The host program · Sequencing · The full machine as a finite multi-stack Turing machine

InductiveStages of the accept generator's literal routine#✓fully proved

The stages of the accept generator's routine emitting a clause's literal are \(\mathrm{cp1}\), \(\mathrm{cp2}\), \(\mathrm{eo}\), \(\mathrm{dec}\), \(\mathrm{cmp}\), \(r(o)\) and \(r_B(o)\) for each ordering \(o \in \{<, =, >\}\), \(\mathrm{emL}\), \(\mathrm{bad}\), \(\mathrm{slot}\) and \(\mathrm{dq}\). They form a finite type with decidable equality.

inductive LS
  | cp1 | cp2 | eo | dec | cmp | r (o : Ordering) | rB (o : Ordering) | emL | bad | slot | dq
  deriving DecidableEq, Fintype

Used by 12

Used byThe accept generator as a finite multi-stack machine · One clause of the accept generator · Labels of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Generator machine for the accept family · The reduction machine halts with the emitted formula · The reduction machine · The host as a finite multi-stack Turing machine · The host program · Sequencing · The full machine as a finite multi-stack Turing machine

InductiveLabels of the accept generator#✓fully proved

For \(n_1, g \in \mathbb{N}\), a label is one of: a precomputation stage; \(\mathrm{e00}(c)\), \(\mathrm{cv1}(c)\), \(\mathrm{cv2}(c)\) or \(\mathrm{fin}(c)\) for a clause kind \(c\) (a code clause \(u < n_1\) or a cell clause \(x < g\)); \(\mathrm{lit}(c, s)\) for a clause kind \(c\) and a stage \(s\) of the literal routine; or the halting label \(\mathrm{done}\). The labels form a finite type with decidable equality.

inductive GL (n1 g : ℕ)
  | pre (s : PS)
  | e00 (c : AK n1 g) | cv1 (c : AK n1 g) | cv2 (c : AK n1 g) | lit (c : AK n1 g) (s : LS)
  | fin (c : AK n1 g)
  | done
  deriving DecidableEq, Fintype

Uses 3 · Used by 24

Statement usesClause kinds of the accept generator · Stages of the accept generator's literal routine · Precomputation stages of the accept generator

Used byTime bound of the accept generator for a concrete machine · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · The accept generator as a finite multi-stack machine · Entry label of an accept cell clause · Run of the accept cell chain · One clause of the accept generator · Entry label of an accept code clause · Start of the accept code chain · Run of the code-clause chain of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Next label after a clause of the accept generator · Run of the accept generator's precomputation · Generator machine for the accept family · First clause label of the accept generator · The reduction machine halts with the emitted formula · The reduction machine · Labels of the Cook–Levin host machine · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing · The full machine as a finite multi-stack Turing machine

DefinitionEntry label of an accept code clause#✓fully proved

For a generator with \(n_1\) code clauses and \(g\) cell clauses and \(u \in \mathbb{N}\), the code-chain label at \(u\) is the entry label of code clause \(u\) when \(u < n_1\), and the halting label \(\mathrm{done}\) when \(u \ge n_1\).

def codeFrom (u : ℕ) : GL n1 g := if h : u < n1 then .e00 (.code ⟨u, h⟩) else .done

Uses 2 · Used by 5

Statement usesClause kinds of the accept generator · Labels of the accept generator

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept cell chain · Start of the accept code chain · Run of the code-clause chain of the accept generator · Next label after a clause of the accept generator

DefinitionStart of the accept code chain#✓fully proved

For a generator with \(n_1\) code clauses, the code chain starts at the entry label of code clause \(n_1 - 1\) (the last one, as clauses are emitted last first), or at the halting label \(\mathrm{done}\) when \(n_1 = 0\).

def codeStart : GL n1 g := if n1 = 0 then .done else codeFrom (n1 - 1)

Uses 2 · Used by 5

Statement usesLabels of the accept generator · Entry label of an accept code clause

Used byCorrectness of the accept generator, with its explicit time bound · Entry label of an accept cell clause · Run of the accept cell chain · Next label after a clause of the accept generator · First clause label of the accept generator

DefinitionEntry label of an accept cell clause#✓fully proved

For a generator with \(n_1\) code clauses and \(g\) cell clauses and \(x \in \mathbb{N}\), the cell-chain label at \(x\) is the entry label of cell clause \(x\) when \(x < g\), and the start of the code chain when \(x \ge g\).

def cellFrom (x : ℕ) : GL n1 g := if h : x < g then .e00 (.cell ⟨x, h⟩) else codeStart

Uses 3 · Used by 4

Statement usesClause kinds of the accept generator · Labels of the accept generator · Start of the accept code chain

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept cell chain · Next label after a clause of the accept generator · First clause label of the accept generator

DefinitionFirst clause label of the accept generator#✓fully proved

Fix naturals \(n_1\) and \(g\), the numbers of code clauses and of cell clauses. Clauses are emitted last first, so the label at which clause emission starts is the start label of the cell clause of \(g - 1\) when \(g > 0\). When \(g = 0\) it is the start label of the code clause of \(n_1 - 1\) if \(n_1 > 0\), and the final label if \(n_1 = 0\).

def start : GL n1 g := if g = 0 then codeStart else cellFrom (g - 1)

Uses 3 · Used by 3

Statement usesLabels of the accept generator · Entry label of an accept cell clause · Start of the accept code chain

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept generator's precomputation · Generator machine for the accept family

DefinitionNext label after a clause of the accept generator#✓fully proved

Let \(n_1, g \in \mathbb{N}\); clauses are emitted last first. After the code clause \(u < n_1\) the generator goes to the halting label \(\mathrm{done}\) if \(u = 0\), and otherwise to the first label \(\mathrm{e00}\) of code clause \(u - 1\). After the cell clause \(x < g\) it goes, if \(x = 0\), to the start of the code chain (the first label of code clause \(n_1 - 1\), or \(\mathrm{done}\) if \(n_1 = 0\)), and otherwise to the first label of cell clause \(x - 1\).

def nextC : AK n1 g → GL n1 g
  | .code u => if u.val = 0 then .done else codeFrom (u.val - 1)
  | .cell x => if x.val = 0 then codeStart else cellFrom (x.val - 1)

Uses 5 · Used by 4

Statement usesClause kinds of the accept generator · Labels of the accept generator · Entry label of an accept cell clause · Entry label of an accept code clause · Start of the accept code chain

Used byRun of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Generator machine for the accept family

DefinitionLiteral routine of the accept generator#✓fully proved

Fix a layout \(L\) with \(g\) symbol codes and parameters \(n_1\), \(\mathrm{ac}\), \(\mathrm{ea}\), and a clause kind \(c\) with base counter \(b(c)\), offset \(\mathrm{off}(c)\) and polarity \(\sigma(c)\). The literal routine of \(c\) gives the generator's statement at each label \(\mathrm{lit}(c, s)\); below, a stage \(s\) stands for the label \(\mathrm{lit}(c, s)\), and moving a counter onto targets means popping it until it is empty and pushing one unit onto every target for each unit popped. At \(\mathrm{cp1}\) it moves \(b(c)\) onto \(Q\) and \(\mathrm{tmp}\), then goes to \(\mathrm{cp2}\). At \(\mathrm{cp2}\) it moves \(\mathrm{tmp}\) onto \(b(c)\), then goes to \(\mathrm{eo}\). At \(\mathrm{eo}\) it pushes \(\mathrm{off}(c)\) units onto \(Q\) and goes to \(\mathrm{dec}\). At \(\mathrm{dec}\) it pops \(P\) and goes to \(\mathrm{bad}\) if \(P\) was empty, else to \(\mathrm{cmp}\). At \(\mathrm{cmp}\) it pops one unit from each nonempty one of \(P\) and \(Q\), pushing a unit onto \(c_1\) for \(P\) and onto \(c_2\) for \(Q\); it repeats \(\mathrm{cmp}\) if both were nonempty, and otherwise goes to \(r(o)\), where the ordering \(o\) is \(<\) if only \(Q\) was nonempty, \(=\) if both were empty, and \(>\) if only \(P\) was nonempty. At \(r(o)\) it moves \(c_1\) onto \(P\), then goes to \(r_B(o)\). At \(r_B(o)\) it moves \(c_2\) onto \(Q\), then goes to \(\mathrm{slot}\) if \(o\) is \(=\) and to \(\mathrm{emL}\) otherwise. At \(\mathrm{emL}\) it prepends the bits false, true to the output and goes to \(\mathrm{dec}\). At \(\mathrm{bad}\) it halts. At \(\mathrm{slot}\) it prepends the bits true, \(\lnot\sigma(c)\) to the output and goes to \(\mathrm{dq}\). At \(\mathrm{dq}\) it empties \(Q\), then goes to \(\mathrm{fin}(c)\).

def litP (c : AK n1 L.g) : LS → TM2.Stmt (SΓ CK) (GL n1 L.g) Bool
  | .cp1 => xfer (.c c.bc) [⟨.c .Q, ()⟩, ⟨.c .tmp, ()⟩] (.lit c .cp1) (.lit c .cp2)
  | .cp2 => xfer (.c .tmp) [⟨.c c.bc, ()⟩] (.lit c .cp2) (.lit c .eo)
  | .eo => emitR (.c .Q) (List.replicate c.off ()) (.lit c .dec)
  | .dec => decr (.c .P) (.lit c .bad) (.lit c .cmp)
  | .cmp => cmpStep (.c .P) (.c .Q) (.c .c1) (.c .c2) () () (.lit c .cmp)
      (.lit c (.r .lt)) (.lit c (.r .eq)) (.lit c (.r .gt))
  | .r o => xfer (.c .c1) [⟨.c .P, ()⟩] (.lit c (.r o)) (.lit c (.rB o))
  | .rB o => xfer (.c .c2) [⟨.c .Q, ()⟩] (.lit c (.rB o))
      (if o = .eq then .lit c .slot else .lit c .emL)
  | .emL => emitR .out [false, true] (.lit c .dec)
  | .bad => .halt
  | .slot => emitR .out (encodeSlot (some (c.sg ac ea))) (.lit c .dq)
  | .dq => xfer (.c .Q) [] (.lit c .dq) (.fin c)

Uses 16 · Used by 1

Statement usesClause kinds of the accept generator · Base counter of an accept clause · Offset of a clause's literal · Polarity of an accept clause's literal · Counters of the accept generator · Labels of the accept generator · Stages of the accept generator's literal routine · Stacks of a counter machine · Alphabets of a counter machine · Variable layout of the transition clauses · Two-bit code of a slot · Flag bit of a machine state · One round of counter comparison · Decrement · Prepending a constant list · Counter transfer loop

Used byGenerator machine for the accept family

DefinitionGenerator machine for the accept family#✓fully proved

Fix a layout \(L\) with label/state block size \(A\), \(K\) stacks and \(g\) symbol codes, and naturals \(n_1\), \(a\), \(k_1\), \(e\). The generator is a multi-stack machine with a Boolean output stack, the unit counters of the generator, and a Boolean internal state. Its precomputation pushes \(g\) units on \(\mathsf{Gc}\), adds \(\mathsf{Hs} \cdot \mathsf{Gc}\) to \(\mathsf{HG}\), pushes \(A\) units on \(\mathsf{Wc}\), pushes \(K\) units on \(\mathsf{Kc}\), adds \(\mathsf{Kc} \cdot \mathsf{HG}\) to \(\mathsf{Wc}\), adds \(\mathsf{Tn} \cdot \mathsf{Wc}\) to \(\mathsf{TW}\), pushes one unit on \(\mathsf{Tn}\), adds \(\mathsf{Tn} \cdot \mathsf{Wc}\) to \(\mathsf{Vc}\), drains \(\mathsf{TW}\) onto both \(\mathsf{CB}\) and \(\mathsf{tmp}\) and then \(\mathsf{tmp}\) back onto \(\mathsf{TW}\), pushes \(A\) units on \(\mathsf{CB}\), pushes \(k_1\) units on \(\mathsf{K1}\), adds \(\mathsf{K1} \cdot \mathsf{HG}\) to \(\mathsf{CB}\), and goes to the first clause label; each multiplication uses \(\mathsf{md}\) as its index counter and \(\mathsf{tmp}\) as scratch. For each clause \(c\) (a code clause of \(u < n_1\) or a cell clause of \(x < g\)) it prepends \([\mathrm{false}, \mathrm{false}]\) to the output, drains \(\mathsf{Vc}\) onto both \(\mathsf{P}\) and \(\mathsf{tmp}\) and then \(\mathsf{tmp}\) back onto \(\mathsf{Vc}\), runs the literal routine of \(c\) with polarity parameters \(a\) and \(e\), drains \(\mathsf{P}\) while prepending \([\mathrm{false}, \mathrm{true}]\) to the output once per unit, and goes to the label after \(c\). At its final label it halts.

It is meant to be started with \(T\) on \(\mathsf{Tn}\), \(H\) on \(\mathsf{Hs}\) and every other counter empty.

Cslib.Complexity.CookLevin.Accept.prog · 20 lines

def prog : GL n1 L.g → TM2.Stmt (SΓ CK) (GL n1 L.g) Bool
  | .pre .eg => emitR (.c .Gc) (List.replicate L.g ()) (.pre (.hg .head))
  | .pre (.hg s) => mulS .Hs .md .Gc .HG .tmp (fun s => .pre (.hg s)) (.pre .ew) s
  | .pre .ew => emitR (.c .Wc) (List.replicate L.A ()) (.pre .ek)
  | .pre .ek => emitR (.c .Kc) (List.replicate L.KK ()) (.pre (.w .head))
  | .pre (.w s) => mulS .Kc .md .HG .Wc .tmp (fun s => .pre (.w s)) (.pre (.tw .head)) s
  | .pre (.tw s) => mulS .Tn .md .Wc .TW .tmp (fun s => .pre (.tw s)) (.pre .inc) s
  | .pre .inc => incr (.c .Tn) () (.pre (.v .head))
  | .pre (.v s) => mulS .Tn .md .Wc .Vc .tmp (fun s => .pre (.v s)) (.pre .cb1) s
  | .pre .cb1 => xfer (.c .TW) [⟨.c .CB, ()⟩, ⟨.c .tmp, ()⟩] (.pre .cb1) (.pre .cb2)
  | .pre .cb2 => xfer (.c .tmp) [⟨.c .TW, ()⟩] (.pre .cb2) (.pre .cbA)
  | .pre .cbA => emitR (.c .CB) (List.replicate L.A ()) (.pre .k1)
  | .pre .k1 => emitR (.c .K1) (List.replicate k1 ()) (.pre (.cbM .head))
  | .pre (.cbM s) => mulS .K1 .md .HG .CB .tmp (fun s => .pre (.cbM s)) GL.start s
  | .e00 c => emitR .out [false, false] (.cv1 c)
  | .cv1 c => xfer (.c .Vc) [⟨.c .P, ()⟩, ⟨.c .tmp, ()⟩] (.cv1 c) (.cv2 c)
  | .cv2 c => xfer (.c .tmp) [⟨.c .Vc, ()⟩] (.cv2 c) (.lit c .cp1)
  | .lit c s => litP L n1 ac ea c s
  | .fin c => xferE (.c .P) .out [false, true] (.fin c) (GL.nextC c)
  | .done => .halt

Uses 18 · Used by 11

Statement usesClause kinds of the accept generator · Counters of the accept generator · Labels of the accept generator · Next label after a clause of the accept generator · First clause label of the accept generator · Stages of the accept generator's literal routine · Precomputation stages of the accept generator · Literal routine of the accept generator · Stages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · The multiplication routine of a counter machine · Variable layout of the transition clauses · Flag bit of a machine state · Prepending a constant list · Counter increment · Counter transfer loop · Draining a counter while prepending a block

Used byTime bound of the accept generator for a concrete machine · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · The accept generator as a finite multi-stack machine · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · The host on the real generators of a machine · The assembled generator, after the precomputation

DefinitionThe accept generator as a finite multi-stack machine#✓fully proved

For a layout \(L\) with \(g\) symbol codes and natural numbers \(n_1, a, k_1, e\), this is the finite multi-stack Turing machine whose stacks are an output stack of bits and one unary counter for each of the generator's sixteen counter names, whose input stack is the counter \(T_n\) and output stack the bit stack, whose labels are the generator's labels for \(n_1\) code clauses and \(g\) cell clauses with start label the first precomputation stage, whose internal states are booleans with initial state false, and whose transition function is the accept generator for \(L\), \(n_1\), \(a\), \(k_1\), \(e\).

It serves only to check that the generator meets the finiteness conditions of a finite machine.

def accTM : FinTM2 where
  K := SK CK
  k₀ := .c .Tn
  k₁ := .out
  Γ := SΓ CK
  Λ := GL n1 L.g
  main := .pre .eg
  σ := Bool
  initialState := false
  m := prog L n1 ac k1 ea

Uses 10

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 · Generator machine for the accept family · Stages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Variable layout of the transition clauses

Correctness: one clause

StructureEmpty scratch counters of the accept generator#✓fully proved

An assignment \(F\) of a natural number to each counter of the generator satisfies this predicate when \(F\) is zero on the scratch counters \(\mathsf{Q}\), \(\mathsf{tmp}\), \(\mathsf{md}\), \(\mathsf{c1}\) and \(\mathsf{c2}\).

The generator keeps these counters empty whenever a clause starts.

structure Rest (F : CK → ℕ) : Prop where
  Q : F .Q = 0
  tmp : F .tmp = 0
  md : F .md = 0
  c1 : F .c1 = 0
  c2 : F .c2 = 0

Uses 1 · Used by 5

Statement usesCounters of the accept generator

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Run of the literal routine of the accept generator

TheoremRun of the literal routine of the accept generator#✓fully proved

Let \(c\) be a clause kind with base counter \(b(c)\), offset \(\mathrm{off}(c)\) and polarity \(\sigma(c)\), and let \(F\) assign values to the counters of the accept generator (for layout \(L\) and parameters \(n_1\), \(\mathrm{ac}\), \(k_1\), \(\mathrm{ea}\)) such that the scratch counters \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\) are \(0\). Let \(q, m \in \mathbb{N}\) with \(q = F(b(c)) + \mathrm{off}(c)\) and \(F(P) = q + m + 1\). Then for every output word \(o\) and every Boolean state \(v\), the generator runs in at most \(m(3q + 6) + 2F(b(c)) + 4q + 9\) steps from the label \(\mathrm{lit}(c, \mathrm{cp1})\), with state \(v\), counters \(F\) and output \(o\), to the label \(\mathrm{fin}(c)\), with state false, the counters \(F\) except that \(P\) holds \(q\), and output \(s\,z\,o\). Here \(s\) is the two bits true, \(\lnot\sigma(c)\) (the encoding of a slot holding a literal of polarity \(\sigma(c)\)), and \(z\) is \(m\) copies of the two bits false, true (the encoding of \(m\) empty slots).

theorem lit_run (c : AK n1 L.g) (F : CK → ℕ) (hF : Rest F) (q gap : ℕ)
    (hq : q = F c.bc + c.off) (hp : F .P = q + gap + 1) (o : List Bool) (v : Bool) :
    RunLe (prog L n1 ac k1 ea) (gap * (3 * q + 6) + 2 * F c.bc + 4 * q + 9)
      ⟨some (.lit c .cp1), v, st F o⟩
      ⟨some (.fin c), false,
        st (update F .P q) (encodeSlot (some (c.sg ac ea)) ++ rep [false, true] gap ++ o)⟩

Uses 29 · Used by 1

Statement usesClause kinds of the accept generator · Base counter of an accept clause · Offset of a clause's literal · Polarity of an accept clause's literal · Counters of the accept generator · Labels of the accept generator · Stages of the accept generator's literal routine · Empty scratch counters of the accept generator · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Two-bit code of a slot · Runs within a step budget · Repeated block

Proof usesGap emission in the counter view · 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 · Adding units to target stacks · Unary counter · Copying a counter through a scratch stack · Pushing a constant list · Prepending a constant list · Pushing a list of symbols onto one stack · Counter transfer loop · Running a counter transfer

Used byOne clause of the accept generator

DefinitionStep bound for one accept clause#✓fully proved

For \(V \in \mathbb{N}\), the step budget for one clause of the accept generator is \(B(V) = V(3V + 6) + 10V + 13\).

def clauseB (V : ℕ) : ℕ := V * (3 * V + 6) + 10 * V + 13

Used by 7

Used byExplicit time bound of the accept generator · The accept generator's time bound on the uniform layout · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator

TheoremOne clause of the accept generator#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, let \(n_1, a, k_1, e, V \in \mathbb{N}\), and let \(c\) be a clause kind of the accept generator (a code clause \(u < n_1\) or a cell clause \(x < g\)) with base counter \(b(c)\), offset \(\mathrm{off}(c)\) and polarity \(\sigma(c)\) for \(a\) and \(e\). Let \(F\) be counter values of the generator whose scratch counters \(\mathsf{Q}\), \(\mathsf{tmp}\), \(\mathsf{md}\), \(\mathsf{c1}\), \(\mathsf{c2}\) are \(0\), with \(F(\mathsf{Vc}) = V\), \(F(\mathsf{P}) = 0\) and \(p = F(b(c)) + \mathrm{off}(c) < V\). Then for every output word \(o\) and every Boolean state \(v\), the accept generator for \(L\), \(n_1\), \(a\), \(k_1\), \(e\) runs in at most \(V(3V + 6) + 10V + 13\) steps from the label \(\mathrm{e00}(c)\), with state \(v\), counters \(F\) and output \(o\), to the label after clause \(c\), with state false, the same counters \(F\), and output the encoding of the dense clause over \(V\) variables whose only literal is the variable \(p\) with polarity \(\sigma(c)\), followed by \(o\).

theorem clause_run {V : ℕ} (c : AK n1 L.g) (F : CK → ℕ) (hF : Rest F) (hV : F .Vc = V)
    (hP : F .P = 0) (hlt : F c.bc + c.off < V) (o : List Bool) (v : Bool) :
    RunLe (prog L n1 ac k1 ea) (clauseB V) ⟨some (.e00 c), v, st F o⟩
      ⟨some (GL.nextC c), false,
        st F (encodeClause (denseClause V [(F c.bc + c.off, c.sg ac ea)]) ++ o)⟩

Uses 35 · Used by 2

Statement usesClause kinds of the accept generator · Base counter of an accept clause · Offset of a clause's literal · Polarity of an accept clause's literal · Counters of the accept generator · Labels of the accept generator · Next label after a clause of the accept generator · Empty scratch counters of the accept generator · Step bound for one accept clause · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense clause from a list of literals · Dense encoding of a clause · Runs within a step budget

Proof usesStages of the accept generator's literal routine · Run of the literal routine of the accept generator · Increasing literal positions · Encoding a dense clause block by block · Gap encoding of a dense clause · Two-bit code of a slot · 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 · Pushing a list of symbols onto one stack · Repeated block · Counter transfer loop · Draining a counter while prepending a block

Used byRun of the accept cell chain · Run of the code-clause chain of the accept generator

Correctness: the two label chains and the whole generator

TheoremRun of the code-clause chain of the accept generator#✓fully proved

Let \(F\) assign values to the counters of the accept generator (for layout \(L\) and parameters \(n_1\), \(\mathrm{ac}\), \(k_1\), \(\mathrm{ea}\)) such that the scratch counters \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\) are \(0\), \(F(\mathrm{Vc}) = V\), \(F(P) = 0\) and \(F(\mathrm{TW}) + n_1 \le V\). Then for every \(u < n_1\), every output word \(o\) and every Boolean state \(v\), the generator runs in at most \((u + 1)(V(3V + 6) + 10V + 13)\) steps from the first label of code clause \(u\), with state \(v\), counters \(F\) and output \(o\), to the halting label \(\mathrm{done}\), with state false, counters \(F\) and output \(w_0 w_1 \cdots w_u\, o\). Here \(w_i\) is the encoding of the dense clause over \(V\) variables whose only literal is variable \(F(\mathrm{TW}) + i\), positive if and only if \(i = \mathrm{ac}\).

theorem codes_run {V : ℕ} (F : CK → ℕ) (hF : Rest F) (hV : F .Vc = V) (hP : F .P = 0)
    (hlt : F .TW + n1 ≤ V) :
    ∀ u, u < n1 → ∀ (o : List Bool) (v : Bool),
      RunLe (prog L n1 ac k1 ea) ((u + 1) * clauseB V) ⟨some (GL.codeFrom u), v, st F o⟩
        ⟨some .done, false, st F ((List.range (u + 1)).flatMap
          (fun u => encodeClause (denseClause V [(F .TW + u, decide (u = ac))])) ++ o)⟩

Uses 22 · Used by 2

Statement usesCounters of the accept generator · Labels of the accept generator · Entry label of an accept code clause · Empty scratch counters of the accept generator · Step bound for one accept clause · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense clause from a list of literals · Dense encoding of a clause · Runs within a step budget

Proof usesClause kinds of the accept generator · Base counter of an accept clause · Offset of a clause's literal · Polarity of an accept clause's literal · Next label after a clause of the accept generator · One clause of the accept generator · Dense clause · Budgeted run · Exact-length runs of a TM2 machine

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept cell chain

TheoremRun of the accept cell chain#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, let \(n_1, a_c, k_1, e_a \in \mathbb{N}\) be the parameters of the generator, and let \(F\) give a value to every counter of the generator such that the scratch counters \(\mathsf{Q}\), \(\mathsf{tmp}\), \(\mathsf{md}\), \(\mathsf{c1}\), \(\mathsf{c2}\) are \(0\), \(F(\mathsf{Vc}) = V\), \(F(\mathsf{P}) = 0\), \(F(\mathsf{TW}) + n_1 \le V\) and \(F(\mathsf{CB}) + g \le V\). Write \(B(V) = V(3V + 6) + 10V + 13\) for the one-clause step bound. Then for every \(x < g\), every output stack \(o\) and every state bit \(v\), the generator started at the entry label of cell clause \(x\) with state \(v\), counters \(F\) and output \(o\) reaches the halting label \(\mathrm{done}\) within \((x + 1)B(V) + n_1 B(V)\) steps, with state false, counters \(F\), and output consisting of the encodings of the dense clauses over \(V\) variables whose single literal is at \(F(\mathsf{TW}) + u\), positive exactly when \(u = a_c\), for \(u = 0, \dots, n_1 - 1\), then of those whose single literal is at \(F(\mathsf{CB}) + y\), positive exactly when \(y = e_a\), for \(y = 0, \dots, x\), then \(o\).

theorem cells_run {V : ℕ} (F : CK → ℕ) (hF : Rest F) (hV : F .Vc = V) (hP : F .P = 0)
    (hlt : F .TW + n1 ≤ V) (hlc : F .CB + L.g ≤ V) :
    ∀ x, x < L.g → ∀ (o : List Bool) (v : Bool),
      RunLe (prog L n1 ac k1 ea) ((x + 1) * clauseB V + n1 * clauseB V)
        ⟨some (GL.cellFrom x), v, st F o⟩
        ⟨some .done, false, st F ((List.range n1).flatMap
          (fun u => encodeClause (denseClause V [(F .TW + u, decide (u = ac))])) ++
          (List.range (x + 1)).flatMap
          (fun x => encodeClause (denseClause V [(F .CB + x, decide (x = ea))])) ++ o)⟩

Uses 24 · Used by 1

Statement usesCounters of the accept generator · Labels of the accept generator · Entry label of an accept cell clause · Empty scratch counters of the accept generator · Step bound for one accept clause · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense clause from a list of literals · Dense encoding of a clause · Runs within a step budget

Proof usesClause kinds of the accept generator · Base counter of an accept clause · Offset of a clause's literal · Polarity of an accept clause's literal · Entry label of an accept code clause · Start of the accept code chain · Next label after a clause of the accept generator · One clause of the accept generator · Run of the code-clause chain of the accept generator · Budgeted run · Exact-length runs of a TM2 machine

Used byCorrectness of the accept generator, with its explicit time bound

DefinitionInitial counters of the accept generator#✓fully proved

For \(T, H \in \mathbb{N}\), the initial counter values are \(T\) on the counter \(\mathrm{Tn}\), \(H\) on the counter \(\mathrm{Hs}\), and \(0\) on every other counter.

def initF (T H : ℕ) : CK → ℕ
  | .Tn => T
  | .Hs => H
  | _ => 0

Uses 1 · Used by 6

Statement usesCounters of the accept generator

Used byTime bound of the accept generator for a concrete machine · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · Run of the accept generator's precomputation · The assembled generator, after the precomputation · The composed machine, raw input to formula

DefinitionCounters after the precomputation of the accept generator#✓fully proved

For a layout \(L\) with \(A\) label/state variables per row, \(K\) stacks and \(g\) symbol codes, and for \(k_1, T, H \in \mathbb{N}\), let \(W = A + KHg\) be the row width. The counter values after the precomputation are \(T + 1\) on \(\mathrm{Tn}\), \(H\) on \(\mathrm{Hs}\), \(g\) on \(\mathrm{Gc}\), \(Hg\) on \(\mathrm{HG}\), \(W\) on \(\mathrm{Wc}\), \(K\) on \(\mathrm{Kc}\), \(k_1\) on \(\mathrm{K1}\), \((T + 1)W\) on \(\mathrm{Vc}\), \(TW\) on \(\mathrm{TW}\), \(TW + A + k_1Hg\) on \(\mathrm{CB}\) (the index of the cell variable of stack \(k_1\), depth \(0\) and symbol code \(0\) at time \(T\)), and \(0\) on every other counter.

def preF (L : Layout) (k1 T H : ℕ) : CK → ℕ
  | .Tn => T + 1
  | .Hs => H
  | .Gc => L.g
  | .HG => H * L.g
  | .Wc => L.rowW H
  | .Kc => L.KK
  | .K1 => k1
  | .Vc => L.numVars T H
  | .TW => T * L.rowW H
  | .CB => L.cIdx H T k1 0 0
  | _ => 0

Uses 5 · Used by 2

Statement usesCounters of the accept generator · Variable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Variables per time step

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept generator's precomputation

DefinitionCost of the precomputation of the accept generator#✓fully proved

For a layout \(L\) with \(A\) label/state variables per row, \(K\) stacks and \(g\) symbol codes, and for \(k_1, T, H \in \mathbb{N}\), let \(W = A + KHg\) be the row width. The step budget of the precomputation is \(3 + (H(2g + 3) + H + 2) + (K(2Hg + 3) + K + 2) + (T(2W + 3) + T + 2) + 1 + ((T + 1)(2W + 3) + (T + 1) + 2) + (2TW + 2) + 2 + (k_1(2Hg + 3) + k_1 + 2)\).

def preB (L : Layout) (k1 T H : ℕ) : ℕ :=
  3 + (H * (2 * L.g + 3) + H + 2) + (L.KK * (2 * (H * L.g) + 3) + L.KK + 2) +
    (T * (2 * L.rowW H + 3) + T + 2) + 1 + ((T + 1) * (2 * L.rowW H + 3) + (T + 1) + 2) +
    (2 * (T * L.rowW H) + 2) + 2 + (k1 * (2 * (H * L.g) + 3) + k1 + 2)

Uses 2 · Used by 5

Statement usesVariable layout of the transition clauses · Variables per time step

Used byExplicit time bound of the accept generator · The accept generator's time bound on the uniform layout · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · Run of the accept generator's precomputation

DefinitionExplicit time bound of the accept generator#✓fully proved

For a layout \(L\) with label block size \(A\), \(K\) stacks and \(g\) symbol codes, and natural numbers \(n_1\), \(k_1\), \(T\), \(H\), let \(W = A + K H g\) and \(V = (T + 1) W\) (the number of variables). The bound is \(P + (g + n_1)\,C\), where \(C = V(3V + 6) + 10V + 13\) is the cost of one clause and the precomputation cost is \(P = 3 + (H(2g + 3) + H + 2) + (K(2Hg + 3) + K + 2) + (T(2W + 3) + T + 2) + 1 + ((T + 1)(2W + 3) + (T + 1) + 2) + (2TW + 2) + 2 + (k_1(2Hg + 3) + k_1 + 2)\).

It is at most \(314\,(A + K + g + n_1 + k_1 + 1)^5\,(T + H + 1)^4\).

def accBound (L : Layout) (n1 k1 T H : ℕ) : ℕ :=
  preB L k1 T H + (L.g + n1) * clauseB (L.numVars T H)

Uses 4 · Used by 3

Statement usesStep bound for one accept clause · Cost of the precomputation of the accept generator · Variable layout of the transition clauses · Number of variables of the transition-clause formula

Used byThe accept generator's time bound on the uniform layout · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator

TheoremRun of the accept generator's precomputation#✓fully proved

Fix a layout \(L\) with label/state block size \(A\), \(K\) stacks and \(g\) symbol codes, and naturals \(n_1\), \(a\), \(k_1\), \(e\). For all \(T, H \in \mathbb{N}\) and every list \(o\) of Booleans, write \(W = A + K H g\) for the row width. The accept generator, started at its first precomputation label with internal state false, output \(o\), \(T\) units on counter \(\mathsf{Tn}\), \(H\) units on \(\mathsf{Hs}\) and every other counter empty, reaches in at most \(\mathrm{preB}(L, k_1, T, H)\) steps the first clause label with internal state false, output still \(o\), and counters \(\mathsf{Tn} = T + 1\), \(\mathsf{Hs} = H\), \(\mathsf{Gc} = g\), \(\mathsf{HG} = H g\), \(\mathsf{Wc} = W\), \(\mathsf{Kc} = K\), \(\mathsf{K1} = k_1\), \(\mathsf{Vc} = (T + 1) W\), \(\mathsf{TW} = T W\), \(\mathsf{CB} = T W + A + k_1 H g\), and every other counter empty.

theorem pre_run (T H : ℕ) (o : List Bool) :
    RunLe (prog L n1 ac k1 ea) (preB L k1 T H)
      ⟨some (.pre .eg), false, st (initF T H) o⟩ ⟨some GL.start, false, st (preF L k1 T H) o⟩

Uses 29 · Used by 1

Statement usesCounters of the accept generator · Labels of the accept generator · First clause label of the accept generator · Precomputation stages of the accept generator · Initial counters of the accept generator · Cost of the precomputation of the accept generator · Counters after the precomputation of the accept generator · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · 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 · Variables per time step · 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 · Counter increment · Multiplying unary counters · Pushing a list of symbols onto one stack · Counter transfer loop

Used byCorrectness of the accept generator, with its explicit time bound

TheoremCorrectness of the accept generator, with its explicit time bound#✓fully proved

Let \(L\) be a layout with label block size \(A\) and \(K\) stacks, and let \(n_1, a, k_1, e, T, H\) be natural numbers with \(n_1 \le A\), \(k_1 < K\) and \(H > 0\). Start the accept generator for \(L\), \(n_1\), \(a\), \(k_1\), \(e\) at its start label, with internal state false, \(T\) and \(H\) in unary on its counters \(T_n\) and \(H_s\), all other counters empty and an arbitrary bit list \(o\) on its output stack. Within a number of steps at most the explicit time bound for \(L\), \(n_1\), \(k_1\), \(T\), \(H\), it reaches the label done, with some internal state, and its output stack then holds the binary encoding of the accept family of \(L\) for \(n_1\), \(a\), \(k_1\), \(e\) at \(T\), \(H\) followed by \(o\).

The hypotheses say that the code block fits in the label block, that \(k_1\) is a stack, and that there is a top cell.

theorem acc_run (hn1 : n1 ≤ L.A) (hk1 : k1 < L.KK) (T H : ℕ) (hH : 0 < H) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (SΓ CK k)),
      RunLe (prog L n1 ac k1 ea) (accBound L n1 k1 T H)
        ⟨some (.pre .eg), false, st (initF T H) o⟩ ⟨some .done, v, S⟩ ∧
        S .out = encodeCNF (accFam L n1 ac k1 ea T H) ++ o

Uses 33 · Used by 1

Statement usesCounters of the accept generator · Labels of the accept generator · Precomputation stages of the accept generator · Explicit time bound of the accept generator · The accept family of a layout · Initial counters of the accept generator · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense encoding of a CNF formula · Runs within a step budget

Proof usesEntry label of an accept cell clause · Entry label of an accept code clause · Start of the accept code chain · First clause label of the accept generator · Empty scratch counters of the accept generator · Run of the accept cell chain · Step bound for one accept clause · Run of the code-clause chain of the accept generator · Cost of the precomputation of the accept generator · Counters after the precomputation of the accept generator · Run of the accept generator's precomputation · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Variables per time step · Index of a label/state variable · Dense clause from a list of literals · Dense clause · Dense encoding of a clause · Budgeted run · Exact-length runs of a TM2 machine

Used byPolynomial time bound of the accept generator

The time bound is polynomial

TheoremThe accept generator's time bound on the uniform layout#✓fully proved

For all natural numbers \(k \ge 1\) and \(y \ge 1\), the explicit time bound of the accept generator for the layout with all four constants equal to \(k\), with \(n_1 = k_1 = k\) and \(T = H = y\), is at most \(314\,k^5 y^4\).

Every monomial of the bound is at most \(k^5 y^4\), and the coefficients sum to \(314\), the value of the bound at \(k = y = 1\).

theorem accBound_uni (k y : ℕ) (hk : 1 ≤ k) (hy : 1 ≤ y) :
    accBound (Cslib.Complexity.CookLevin.Family.Layout.uni k) k k y y ≤ 314 * k ^ 5 * y ^ 4

Uses 7 · Used by 1

Statement usesExplicit time bound of the accept generator · Uniform layout

Proof usesStep bound for one accept clause · Cost of the precomputation of the accept generator · Variable layout of the transition clauses · Number of variables of the transition-clause formula · Variables per time step

Used byPolynomial time bound of the accept generator

DefinitionConstant of the accept generator's time bound#✓fully proved

For a layout \(L\) with label block size \(A\), \(K\) stacks and \(g\) symbol codes, and natural numbers \(n_1\), \(k_1\), the constant is \(314\,(A + K + g + n_1 + k_1 + 1)^5\).

def accC (L : Layout) (n1 k1 : ℕ) : ℕ := 314 * (L.A + L.KK + L.g + n1 + k1 + 1) ^ 5

Uses 1 · Used by 7

Statement usesVariable layout of the transition clauses

Used byTime bound of the accept generator for a concrete machine · Polynomial time bound of the accept generator · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · Step bound of the host · The assembled generator, after the precomputation · Polynomial time bound of the composed machine

TheoremPolynomial time bound of the accept generator#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(n_1, a, k_1, e, T, H\) be natural numbers with \(n_1 \le A\), \(k_1 < K\) and \(H > 0\), and let \(c = 314\,(A + K + g + n_1 + k_1 + 1)^5\). Start the accept generator for \(L\), \(n_1\), \(a\), \(k_1\), \(e\) at its start label, with internal state false, \(T\) and \(H\) in unary on its counters \(T_n\) and \(H_s\), all other counters empty and an arbitrary bit list \(o\) on its output stack. Within at most \(c\,(T + H + 1)^4\) steps it reaches the label done, with some internal state, and its output stack then holds the binary encoding of the accept family of \(L\) for \(n_1\), \(a\), \(k_1\), \(e\) at \(T\), \(H\) followed by \(o\).

theorem acc_time {L : Layout} {n1 ac k1 ea : ℕ} (hn1 : n1 ≤ L.A) (hk1 : k1 < L.KK) (T H : ℕ)
    (hH : 0 < H) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (SΓ CK k)),
      RunLe (prog L n1 ac k1 ea) (accC L n1 k1 * (T + H + 1) ^ 4)
        ⟨some (.pre .eg), false, st (initF T H) o⟩ ⟨some .done, v, S⟩ ∧
        S .out = encodeCNF (accFam L n1 ac k1 ea T H) ++ o

Uses 22 · Used by 1

Statement usesCounters of the accept generator · Labels of the accept generator · Precomputation stages of the accept generator · Constant of the accept generator's time bound · The accept family of a layout · Initial counters of the accept generator · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense encoding of a CNF formula · Runs within a step budget

Proof usesExplicit time bound of the accept generator · The accept generator's time bound on the uniform layout · Correctness of the accept generator, with its explicit time bound · Step bound for one accept clause · Cost of the precomputation of the accept generator · Number of variables of the transition-clause formula · Variables per time step · Uniform layout · Exact-length runs of a TM2 machine

Used byTime bound of the accept generator for a concrete machine

Link to the semantic accept family

TheoremThe concrete accept family is a layout-level accept family#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with encoding \(E\), let \(\mathit{acc}\) be a symbol of the output stack of \(M\), and let \(T\), \(H\) be natural numbers. The accept family of \(E\) for \(\mathit{acc}\) at \(T\), \(H\) equals, by definition, the accept family of the layout of \(E\) at \(T\), \(H\) with parameters \(n_1 = A_0\), the number of (label, state) codes of \(E\); \(a\), the (label, state) code of the halted configuration (no label, initial state); \(k_1\), the number \(E\) gives the output stack; and \(e\), the code of \(\mathit{acc}\).

theorem accFamily_eq (acc : M.Γ M.k₁) (T H : ℕ) :
    E.accFamily acc T H = accFam E.layout E.A0 E.acode (E.kc M.k₁) (E.enc M.k₁ acc) T H

Uses 6

Statement usesThe accept family of a layout · Encoding data for a finite TM2 machine · The accept family · Accepting code · Clause layout of a machine encoding · Dense CNF formula

TheoremTime bound of the accept generator for a concrete machine#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with encoding \(E\), let \(\mathit{acc}\) be a symbol of the output stack of \(M\), and let \(T\), \(H\) be natural numbers with \(H > 0\). Let \(L\) be the layout of \(E\), with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(A_0\) be the number of (label, state) codes of \(E\), let \(k_1\) be the number \(E\) gives the output stack, and let \(c = 314\,(A + K + g + A_0 + k_1 + 1)^5\). Start the accept generator for \(L\), \(A_0\), the code of the halted configuration, \(k_1\) and the code of \(\mathit{acc}\) at its start label, with internal state false, \(T\) and \(H\) in unary on its counters \(T_n\) and \(H_s\), all other counters empty and an arbitrary bit list \(o\) on its output stack. Within at most \(c\,(T + H + 1)^4\) steps it reaches the label done, with some internal state, and its output stack then holds the binary encoding of the accept family of \(E\) for \(\mathit{acc}\) at \(T\), \(H\) followed by \(o\).

theorem acc_gen_time (acc : M.Γ M.k₁) (T H : ℕ) (hH : 0 < H) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (SΓ CK k)),
      RunLe (prog E.layout E.A0 E.acode (E.kc M.k₁) (E.enc M.k₁ acc))
        (accC E.layout E.A0 (E.kc M.k₁) * (T + H + 1) ^ 4)
        ⟨some (.pre .eg), false, st (initF T H) o⟩ ⟨some .done, v, S⟩ ∧
        S .out = encodeCNF (E.accFamily acc T H) ++ o

Uses 18 · Used by 1

Statement usesCounters of the accept generator · Labels of the accept generator · Precomputation stages of the accept generator · Constant of the accept generator's time bound · Initial counters of the accept generator · Generator machine for the accept family · Stacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Encoding data for a finite TM2 machine · The accept family · Accepting code · Clause layout of a machine encoding · Dense encoding of a CNF formula · Runs within a step budget

Proof usesPolynomial time bound of the accept generator · Number of situations

Used byThe assembled generator, after the precomputation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.