Cook-Levin: generator machine for the initial-row family

74 fully proved

An input stack beside a counter machine

InductiveStacks of a counter machine with an input stack#✓fully proved

For a counter type \(C\), the stacks are those of the counter machine with counters \(C\) (its output stack and one counter stack for each element of \(C\)), plus one additional input stack.

inductive IK (C : Type)
  | b (k : SK C)
  | inp
  deriving DecidableEq, Fintype

Uses 1 · Used by 20

Statement usesStacks of a counter machine

Used byStacks of a counter machine with an extra input stack · Alphabets of a counter machine with an input stack · The I3 loop on the whole input · The I3 loop · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The initial-row generator · The counter stacks inside the generator's stacks · Read test for one code · The read chain · Run lifting · Host stack renaming for the init generator · Embedding of the init generator into the host · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing

AbbreviationAlphabets of a counter machine with an input stack#✓fully proved

For a counter type \(C\) and an input alphabet \(G\), each stack of the counter machine with counters \(C\) keeps its alphabet there (Booleans on the output stack, a single symbol on each counter stack), and the input stack has alphabet \(G\).

abbrev IΓ (C G : Type) : IK C → Type
  | .b k => SΓ C k
  | .inp => G

Uses 3 · Used by 18

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks of a counter machine with an input stack

Used byStacks of a counter machine with an extra input stack · The I3 loop on the whole input · The I3 loop · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The initial-row generator · The counter stacks inside the generator's stacks · Read test for one code · The read chain · Run lifting · Embedding of the init generator into the host · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing

DefinitionStacks of a counter machine with an extra input stack#✓fully proved

Given stack contents \(S\) of a counter machine with counters indexed by \(C\) (a list over the alphabet of each of its stacks) and a list \(x\) of symbols from \(G\), the combined stack contents give each stack \(k\) of the counter machine the list \(S(k)\) and give the extra input stack the list \(x\).

def emb (S : ∀ k, List (SΓ C k)) (xs : List G) : ∀ k, List (IΓ C G k)
  | .b k => S k
  | .inp => xs

Uses 4 · Used by 9

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack

Used byThe I3 loop on the whole input · The I3 loop · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The read chain · Run lifting · Sequencing

DefinitionThe counter stacks inside the generator's stacks#✓fully proved

For a counter index type \(C\) and an input alphabet \(G\), the stack embedding of a counter machine over \(C\) into the same machine with one extra input stack over \(G\): each stack (the output stack or a counter) goes to its copy among the extended machine's stacks, with the identity map on its alphabet.

def liftE : SEmb (SΓ C) (IΓ C G) where
  e := IK.b
  inj := fun _ _ h => by cases h; rfl
  ι := fun _ => Equiv.refl _

Uses 5 · Used by 4

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · Stack embedding

Used byThe I3 loop · Correctness of the init generator, with its explicit time bound · The initial-row generator · Run lifting

TheoremRun lifting#✓fully proved

Let \(M\) be a counter machine (unit counters indexed by \(C\) and a Boolean output stack) and \(M'\) a machine on the same stacks plus an input stack over \(G\), such that \(M'\) embeds \(M\) along the inclusion of the counter stacks with the same labels (at every label whose statement is not the halt statement, \(M'\) runs \(M\)'s statement). If \(M\) runs in \(n\) steps from optional label \(l\), flag \(v\) and stacks \(S\) to a label \(l'\), flag \(v'\) and stacks \(S'\), then for every input list \(xs\) over \(G\), \(M'\) runs in \(n\) steps from label \(l\), flag \(v\), stacks \(S\) and input stack \(xs\) to label \(l'\), flag \(v'\), stacks \(S'\) and input stack \(xs\).

This is an instance of run embedding.

theorem run_lift {M : Λ → TM2.Stmt (SΓ C) Λ Bool} {M' : Λ → TM2.Stmt (IΓ C G) Λ Bool}
    (hM : Embeds liftE id M M') (xs : List G) (n : ℕ) (l : Option Λ) (v : Bool)
    (S : ∀ k, List (SΓ C k)) (l' : Λ) (v' : Bool) (S' : ∀ k, List (SΓ C k))
    (h : Run M n ⟨l, v, S⟩ ⟨some l', v', S'⟩) :
    Run M' n ⟨l, v, emb S xs⟩ ⟨some l', v', emb S' xs⟩

Uses 12 · Used by 2

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · Stacks of a counter machine with an extra input stack · The counter stacks inside the generator's stacks · Embedding of a machine in a host · Exact-length runs of a TM2 machine

Proof usesAgreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Run embedding

Used byThe I3 loop · Correctness of the init generator, with its explicit time bound

Reading one input symbol into the label

DefinitionRead test for one code#✓fully proved

Given labels \(\mathrm{hit}(i)\) and \(\mathrm{miss}(i)\) for the codes \(i < g\), the read test for code \(i\) is the statement, on a counter machine's stacks plus an input stack of codes, that peeks at the top of the input stack and sets the flag to whether it equals \(i\). If it does, the test pops it and goes to \(\mathrm{hit}(i)\); otherwise (including when the input stack is empty) it goes to \(\mathrm{miss}(i)\).

def rdS (hit miss : Fin g → Λ) (i : Fin g) : TM2.Stmt (IΓ C (Fin g)) Λ Bool :=
  .peek .inp (fun _ o => decide (o = some i))
    (.branch id (.pop .inp (fun v _ => v) (.goto fun _ => hit i)) (.goto fun _ => miss i))

Uses 2 · Used by 2

Statement usesStacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack

Used byThe initial-row generator · The read chain

TheoremThe read chain#✓fully proved

Let \(M'\) be a machine on a counter machine's stacks plus an input stack of codes \(< g\), with labels \(\mathrm{rd}(i)\), \(\mathrm{hit}(i)\) and \(\mathrm{miss}(i)\) for \(i < g\), such that at \(\mathrm{rd}(i)\) it runs the read test for code \(i\) with these hit and miss labels, and \(\mathrm{miss}(i) = \mathrm{rd}(i + 1)\) whenever \(i + 1 < g\). Then for all counter stacks \(S\), codes \(c\), input lists \(xs\), all \(k\) and codes \(i\) with \(i + k = c\), and every flag \(v\), the machine \(M'\) goes in exactly \(k + 1\) steps from label \(\mathrm{rd}(i)\), flag \(v\), stacks \(S\) and input \(c\) followed by \(xs\) to label \(\mathrm{hit}(c)\), flag true, stacks \(S\) and input \(xs\).

theorem read_run {M' : Λ → TM2.Stmt (IΓ C (Fin g)) Λ Bool} {rd hit miss : Fin g → Λ}
    (hrd : ∀ i, M' (rd i) = rdS hit miss i)
    (hmiss : ∀ i : Fin g, ∀ h : i.val + 1 < g, miss i = rd ⟨i.val + 1, h⟩)
    (S : ∀ k, List (SΓ C k)) (c : Fin g) (xs : List (Fin g)) :
    ∀ k (i : Fin g), i.val + k = c.val → ∀ v : Bool,
      Run M' (k + 1) ⟨some (rd i), v, emb S (c :: xs)⟩ ⟨some (hit c), true, emb S xs⟩

Uses 8 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks of a counter machine with an input stack · Alphabets of a counter machine with an input stack · Stacks of a counter machine with an extra input stack · Read test for one code · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label

Used byThe I3 loop

The family (pure specification)

DefinitionEmpty-cell variable of the initial row#✓fully proved

For a variable layout \(L\), a stack number \(k_0\), a number \(H\) of tracked depths per stack and a depth \(j\), this is the index of the cell variable of \(L\) at time \(0\) for stack \(k_0\), depth \(j\) and symbol code \(0\) (the empty cell \(\bot\)), namely \(A + (k_0 H + j)\,g\), where \(A\) is the size of the label/state block of \(L\) and \(g\) is its number of symbol codes.

def zB (H j : ℕ) : ℕ := L.cIdx H 0 k0 j 0

Uses 2 · Used by 5

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

Used byCertificate clauses of the initial row (I4) · Row-0 prefix clauses · Row-0 tail clauses · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionStart-code clause of the initial row (I1)#✓fully proved

For a layout \(L\), a label/state code \(i_c\) and natural numbers \(T\) and \(H\), the start-code formula consists of a single clause: the dense clause over the variables of \(L\) for \(T\) time steps and depth \(H\) whose only literal is the positive literal on the time-\(0\) label/state variable with code \(i_c\).

def iCode (T H : ℕ) : CNF := [denseClause (L.numVars T H) [(L.xIdx H 0 ic, true)]]

Uses 6 · Used by 3

Statement usesVariable layout of the transition clauses · Number of variables of the transition-clause formula · Index of a label/state variable · Dense clause from a list of literals · Dense CNF formula · Dense clause

Used byThe init family · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionRow-0 clauses for the other stacks#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(k_0\) be a stack, and let \(T, H\) be natural numbers. This is the CNF over \(V = (T + 1)(A + KHg)\) variables that has, for every stack \(k < K\) with \(k \ne k_0\) and every depth \(j < H\) (stacks in increasing order, then depths in increasing order), the dense clause over \(V\) variables whose only literal is the positive literal of variable \(A + (kH + j)g\), the row-\(0\) variable saying that stack \(k\) holds code \(0\) (the empty cell) at depth \(j\).

def iOther (T H : ℕ) : CNF :=
  ((List.range L.KK).filter (· ≠ k0)).flatMap fun k =>
    (List.range H).map fun j => denseClause (L.numVars T H) [(L.cIdx H 0 k j 0, true)]

Uses 6 · Used by 3

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Dense CNF formula · Dense clause

Used byThe init family · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionInput clauses of the initial row (I3)#✓fully proved

For a layout \(L\) with \(g\) symbol codes, a stack number \(k_0\), a list \(x = (x_0, \dots, x_{\ell - 1})\) of codes below \(g\) and natural numbers \(T\) and \(H\), the input formula has, for each \(j = 0, 1, \dots, \ell - 1\) in order, one dense clause over the variables of \(L\) for \(T\) time steps and depth \(H\), whose only literal is the positive literal on the time-\(0\) cell variable of stack \(k_0\) at depth \(j\) with code \(x_j\).

def iIn (xs : List (Fin L.g)) (T H : ℕ) : CNF :=
  (List.range xs.length).map fun j => denseClause (L.numVars T H)
    [(L.cIdx H 0 k0 j ((xs[j]?).elim 0 Fin.val), true)]

Uses 6 · Used by 3

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Dense CNF formula · Dense clause

Used byThe init family · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionCertificate clauses of the initial row (I4)#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(k_0\) be a stack, let \(y = (y_1, \dots, y_r)\) be a list of natural numbers and let \(n, m, T, H\) be natural numbers. For a depth \(j\) and a code \(x\) write \(C_{j,x} = A + (k_0 H + j)g + x\) for the row-\(0\) variable saying that stack \(k_0\) holds code \(x\) at depth \(j\). This is the CNF over \(V = (T + 1)(A + KHg)\) variables that has, for \(i = 0, 1, \dots, m - n - 1\) in order (no clauses if \(m \le n\)), the dense clause over \(V\) variables whose literals are the positive literals of the variables \(C_{n+i,0}\), \(C_{n+i,y_1}\), \(\dots\), \(C_{n+i,y_r}\): the cell at depth \(n + i\) is empty or holds one of the codes in \(y\).

In use, \(y\) lists the certificate codes, sorted and distinct.

def iCert (n m T H : ℕ) : CNF :=
  (List.range (m - n)).map fun i => denseClause (L.numVars T H)
    ((zB L k0 H (n + i), true) :: ycs.map fun c => (L.cIdx H 0 k0 (n + i) c, true))

Uses 7 · Used by 3

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Empty-cell variable of the initial row · Dense CNF formula · Dense clause

Used byThe init family · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionRow-0 prefix clauses#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(k_0\) be a stack, let \(n, m, T, H\) be natural numbers, and write \(z_j = A + (k_0 H + j)g\) for the row-\(0\) variable saying that stack \(k_0\) holds code \(0\) (the empty cell) at depth \(j\). This is the CNF over \(V = (T + 1)(A + KHg)\) variables that has, for \(i = 0, 1, \dots, m - n - 1\) in order (no clauses if \(m \le n\)), the dense clause over \(V\) variables whose literals are the negative literal of variable \(z_{n+i}\) and the positive literal of variable \(z_{n+i+1}\): an empty cell at depth \(n + i\) forces an empty cell at depth \(n + i + 1\).

def iPre (n m T H : ℕ) : CNF :=
  (List.range (m - n)).map fun i => denseClause (L.numVars T H)
    [(zB L k0 H (n + i), false), (zB L k0 H (n + i + 1), true)]

Uses 6 · Used by 3

Statement usesVariable layout of the transition clauses · Number of variables of the transition-clause formula · Dense clause from a list of literals · Empty-cell variable of the initial row · Dense CNF formula · Dense clause

Used byThe init family · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionRow-0 tail clauses#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(k_0\) be a stack, let \(m, T, H\) be natural numbers, and write \(z_j = A + (k_0 H + j)g\) for the row-\(0\) variable saying that stack \(k_0\) holds code \(0\) (the empty cell) at depth \(j\). This is the CNF over \(V = (T + 1)(A + KHg)\) variables that has, for \(i = 0, 1, \dots, H - m - 1\) in order (no clauses if \(H \le m\)), the dense clause over \(V\) variables whose only literal is the positive literal of variable \(z_{m+i}\).

def iTail (m T H : ℕ) : CNF :=
  (List.range (H - m)).map fun i => denseClause (L.numVars T H) [(zB L k0 H (m + i), true)]

Uses 6 · Used by 3

Statement usesVariable layout of the transition clauses · Number of variables of the transition-clause formula · Dense clause from a list of literals · Empty-cell variable of the initial row · Dense CNF formula · Dense clause

Used byThe init family · The init family of an encoding is a layout-level init family · Correctness of the init generator, with its explicit time bound

DefinitionThe init family#✓fully proved

Let \(L\) be a layout, let \(i_c\) be a label/state code, let \(k_0\) be a stack, let \(y\) be a list of natural numbers, let \(x\) be a list of symbol codes of \(L\) of length \(\ell\), and let \(m, T, H\) be natural numbers. The init family is the CNF formula obtained by concatenating, in this order: the start-code clause of the initial row for \(i_c\), \(T\), \(H\) (I1); the row-\(0\) clauses for the stacks other than \(k_0\) for \(T\), \(H\) (I2); the input clauses of the initial row for \(k_0\), \(x\), \(T\), \(H\) (I3); the certificate clauses of the initial row for \(k_0\), \(y\), \(n = \ell\), \(m\), \(T\), \(H\) (I4); the row-\(0\) prefix clauses for \(k_0\), \(n = \ell\), \(m\), \(T\), \(H\) (I5); and the row-\(0\) tail clauses for \(k_0\), \(m\), \(T\), \(H\) (I6).

def initFam (xs : List (Fin L.g)) (m T H : ℕ) : CNF :=
  iCode L ic T H ++ iOther L k0 T H ++ iIn L k0 xs T H ++ iCert L k0 ycs xs.length m T H ++
    iPre L k0 xs.length m T H ++ iTail L k0 m T H

Uses 9 · Used by 4

Statement usesVariable layout of the transition clauses · Certificate clauses of the initial row (I4) · Start-code clause of the initial row (I1) · Input clauses of the initial row (I3) · Row-0 clauses for the other stacks · Row-0 prefix clauses · Row-0 tail clauses · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator

The generator machine

InductiveCounters of the initial-row generator#✓fully proved

The unit-counter stacks of the generator are indexed by a finite type with 27 distinct elements: Tn, Xn, En, Fn, Gc, Mm, Hs, HG, Wc, Vc, KA, ZA, Z45, Z6, Z1, Z2, N1, N2, CB, Zr, P, Q, tmp, md, c1, c2 and Id. Equality on it is decidable.

inductive CK
  | Tn | Xn | En | Fn | Gc | Mm | Hs | HG | Wc | Vc | KA | ZA | Z45 | Z6 | Z1 | Z2 | N1 | N2
  | CB | Zr | P | Q | tmp | md | c1 | c2 | Id
  deriving DecidableEq

Used by 49

Used byBase counter of a clause kind (initial-row generator) · One phase-loop iteration of the initial-row generator · Loop-count counter of a phase (initial-row generator) · Base counter of a phase (initial-row generator) · Run of one clause (initial-row generator) · The I3 loop on the whole input · The I3 loop · Counter part of one I3 iteration · Initial counters of the init generator · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The initial-row generator · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · One phase loop · Counters after the precomputation · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Empty scratch counters · 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 init 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

InductiveLoop phases of the initial-row generator#✓fully proved

The five phase loops of the generator for the initial-row clauses, in the order the generator runs them (its input loop runs between the certificate phase and the two stack phases): the tail phase (the row-\(0\) cells of the stack \(k_0\) holding the input, past the certificate block, are empty), the prefix phase (an empty cell in the certificate block is followed by an empty cell), the certificate phase (each certificate cell is empty or holds a certificate code), and two stack phases making every stack other than \(k_0\) empty, first the stacks \(k > k_0\), then the stacks \(k < k_0\).

inductive PH
  | tail | pre | cert | o2 | o1
  deriving DecidableEq

Used by 29

Used byBase counter of a clause kind (initial-row generator) · One phase-loop iteration of the initial-row generator · Loop-count counter of a phase (initial-row generator) · Base counter of a phase (initial-row generator) · Clause kinds of the initial-row generator · Run of one clause (initial-row generator) · Labels of the initial-row generator · The I3 loop on the whole input · The I3 loop · Counter part of one I3 iteration · Correctness of the init generator, with its explicit time bound · The init generator as a finite multi-stack machine · The initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · Label after a phase loop · Label after a clause · Number of literals of a clause kind · Literal offsets · One phase loop · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Literal signs of an init-family clause kind · 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

DefinitionLoop-count counter of a phase (initial-row generator)#✓fully proved

Let \(k_0\) be the index of the input stack in the tableau layout. For a loop phase \(p\), the generator counter whose units count the remaining iterations of the loop of \(p\): Fn for the I6 phase, En for both the I5 and the I4 phase, N2 for the I2 phase over the stacks \(k > k_0\), and N1 for the I2 phase over the stacks \(k < k_0\).

def cN : PH → CK
  | tail => .Fn
  | pre => .En
  | cert => .En
  | o2 => .N2
  | o1 => .N1

Uses 2 · Used by 4

Statement usesCounters of the initial-row generator · Loop phases of the initial-row generator

Used byOne phase-loop iteration of the initial-row generator · Correctness of the init generator, with its explicit time bound · One phase loop · The counter part of the initial-row generator

DefinitionBase counter of a phase (initial-row generator)#✓fully proved

Let \(k_0\) be the index of the input stack in the tableau layout. For a loop phase \(p\), the generator counter holding the base of the loop of \(p\), the cell base of its iteration \(0\): Z6 for the I6 phase, Z45 for both the I5 and the I4 phase, Z2 for the I2 phase over the stacks \(k > k_0\), and Z1 for the I2 phase over the stacks \(k < k_0\).

def cZ : PH → CK
  | tail => .Z6
  | pre => .Z45
  | cert => .Z45
  | o2 => .Z2
  | o1 => .Z1

Uses 2 · Used by 4

Statement usesCounters of the initial-row generator · Loop phases of the initial-row generator

Used byOne phase-loop iteration of the initial-row generator · Correctness of the init generator, with its explicit time bound · One phase loop · The counter part of the initial-row generator

InductiveClause kinds of the initial-row generator#✓fully proved

For \(g, n \in \mathbb{N}\), a clause kind is either the start-code clause (I1), an input clause (I3) with a symbol code \(c < g\), or the clause of one of the five loop phases \(p\). The parameter \(n\) only indexes the type. There are finitely many clause kinds and their equality is decidable.

inductive CL (g n : ℕ)
  | code
  | inp (c : Fin g)
  | ph (p : PH)
  deriving DecidableEq, Fintype

Uses 1 · Used by 30

Statement usesLoop phases of the initial-row generator

Used byLabel after a literal routine (initial-row generator) · Base counter of a clause kind (initial-row generator) · Boundary before a literal (initial-row generator) · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · Literals of a clause kind · Labels of the initial-row generator · The I3 loop · Literals of a clause kind in range · Correctness of the init generator, with its explicit time bound · The init generator as a finite multi-stack machine · The initial-row generator · Entry label of a literal routine (initial-row generator) · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · Label after a phase loop · Label after a clause · Number of literals of a clause kind · Literal offsets · One phase loop · The counter part of the initial-row generator · Literal signs of an init-family clause kind · Well-formed init-family clause kinds · 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

DefinitionNumber of literals of a clause kind#✓fully proved

For clause kinds over \(g\) codes and \(n\) certificate codes, a clause of the certificate phase has \(n + 1\) literals, a clause of the prefix phase has \(2\), and every other clause kind has \(1\).

def nl : CL g n → ℕ
  | ph .cert => n + 1
  | ph .pre => 2
  | _ => 1

Uses 2 · Used by 9

Statement usesClause kinds of the initial-row generator · Loop phases of the initial-row generator

Used byBoundary before a literal (initial-row generator) · Run of one clause (initial-row generator) · Literals of a clause kind · The I3 loop · Literals of a clause kind in range · Correctness of the init generator, with its explicit time bound · Run of the literal routines of a clause (initial-row generator) · The counter part of the initial-row generator · Well-formed init-family clause kinds

DefinitionLiteral offsets#✓fully proved

Fix numbers \(i_c\) and \(g'\) and a list \(y = (y_1, \dots, y_r)\) of numbers. The offset from the clause base of literal \(l\) in a clause of kind \(c\) is \(i_c\) for the start-code clause; \(x\) for the input clause with code \(x\); for the certificate phase, \(y_l\) if \(1 \le l \le r\) and \(0\) otherwise; for the prefix phase, \(0\) if \(l = 0\) and \(g'\) otherwise; and \(0\) for the other three phases.

def off (ic g' : ℕ) (ycs : List ℕ) : CL g n → ℕ → ℕ
  | code, _ => ic
  | inp c, _ => c
  | ph .cert, l => (0 :: ycs).getD l 0
  | ph .pre, l => if l = 0 then 0 else g'
  | ph _, _ => 0

Uses 2 · Used by 10

Statement usesClause kinds of the initial-row generator · Loop phases of the initial-row generator

Used byBoundary before a literal (initial-row generator) · Run of one clause (initial-row generator) · Literals of a clause kind · The I3 loop · Literals of a clause kind in range · Correctness of the init generator, with its explicit time bound · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · Well-formed init-family clause kinds

DefinitionLiteral signs of an init-family clause kind#✓fully proved

For a clause kind \(c\) of the init-family generator and a literal index \(l \in \mathbb{N}\), the sign of literal \(l\) of \(c\) is positive in every case except one: for the prefix-form phase (clause group I5), literal \(0\) is negative and every literal \(l \ne 0\) is positive.

def sg : CL g n → ℕ → Bool
  | ph .pre, l => decide (l ≠ 0)
  | _, _ => true

Uses 2 · Used by 6

Statement usesClause kinds of the initial-row generator · Loop phases of the initial-row generator

Used byRun of one clause (initial-row generator) · Literals of a clause kind · Correctness of the init generator, with its explicit time bound · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator)

DefinitionBase counter of a clause kind (initial-row generator)#✓fully proved

For a clause kind \(c\), the generator counter whose value is added to the literal offsets of \(c\) to give the literal positions: the counter Zr for the start-code clause (I1), and the counter CB for every other clause kind.

def bc : CL g n → CK
  | code => .Zr
  | _ => .CB

Uses 3 · Used by 7

Statement usesCounters of the initial-row generator · Clause kinds of the initial-row generator · Loop phases of the initial-row generator

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Correctness of the init generator, with its explicit time bound · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator)

InductiveLabels of the first precomputation part#✓fully proved

The finite type of labels with which the generator sets the counters \(G_c = g\), \(M_m = m\), \(H_s = H\), \(HG = H \cdot g\), \(W_c = W\) and \(V_c = V\), where \(g\) is the number of symbol codes, \(m\) the end of the certificate block, \(H\) the stack height, \(W\) the row width and \(V\) the number of variables. It consists of thirteen single labels and three multiplication loops, each with one label per multiplication stage.

inductive PS1
  | eg | cpM1 | cpM2 | cpE1 | cpE2 | cpH1 | cpH2 | cpF1 | cpF2 | hg (s : MS)
  | wA | wK | w (s : MS) | wD | inc | v (s : MS)
  deriving DecidableEq, Fintype

Uses 1 · Used by 19

Statement usesStages of the multiplication routine

Used byLabels of the initial-row generator · The I3 loop · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The initial-row generator · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · The reduction machine halts with the emitted formula · The reduction machine · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing · The full program on the real generators · The composed machine, raw input to formula · The full machine as a finite multi-stack Turing machine

InductiveLabels of the second precomputation part#✓fully proved

The finite type of labels with which the generator computes the row-0 cell bases \(Z_A, Z_{45}, Z_6, Z_1, Z_2\) and the loop counts \(N_1, N_2\). It consists of sixteen single labels and five multiplication loops, each with one label per multiplication stage.

inductive PS2
  | zA | zK | z (s : MS) | zD | f1 | f2 | f (s : MS) | s1 | s2 | s (s : MS) | z1
  | t1 | t2 | t3 | t4 | nK | n (s : MS) | nD | qK | q (s : MS) | qD
  deriving DecidableEq, Fintype

Uses 1 · Used by 13

Statement usesStages of the multiplication routine

Used byLabels of the initial-row generator · The I3 loop · Correctness of the init generator, with its explicit time bound · The init generator as a finite multi-stack machine · The initial-row generator · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · 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 literal routine (initial-row generator)#✓fully proved

The stages of the generator's routine that emits one literal of a clause: two stages copying the clause base into a target counter, a stage adding the literal's offset to the target, a stage decrementing the position counter, a stage comparing the position with the target, two restore stages for each comparison outcome (less, equal or greater), a stage emitting one empty slot, a halting error stage, a stage emitting the literal's slot, and a stage draining the target counter.

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

Used by 16

Used byLabels of the initial-row generator · The I3 loop · Correctness of the init generator, with its explicit time bound · The init generator as a finite multi-stack machine · The initial-row generator · Entry label of a literal routine (initial-row generator) · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · The counter part of the initial-row generator · 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 initial-row generator#✓fully proved

For natural numbers \(g\) and \(n\), the labels are: a label for each stage of the first precomputation part and one for each stage of the second; for each loop phase \(p\), a loop-head label, a counter-reset label, two base-copy labels, a multiplication label for each multiplication stage and a base-drain label; for the input loop, a head label, two base-copy labels, a multiplication label for each multiplication stage, a read test for each code \(i < g\) and a base-drain label; an error label; for each clause kind \(c\) for \(g\) and \(n\), a clause-start label, two labels copying the variable count, a literal label for each literal index \(l < n + 2\) and each literal stage, and a label emitting the leading gap; and a final label. The label type has decidable equality and is finite.

inductive GL (g n : ℕ)
  | pre1 (s : PS1) | pre2 (s : PS2)
  | hd (p : PH) | rs (p : PH) | b1 (p : PH) | b2 (p : PH) | bM (p : PH) (s : MS) | dr (p : PH)
  | i3h | i3b1 | i3b2 | i3M (s : MS) | rd (i : Fin g) | i3d | bad
  | e00 (c : CL g n) | cv1 (c : CL g n) | cv2 (c : CL g n)
  | lit (c : CL g n) (l : Fin (n + 2)) (s : LS) | fin (c : CL g n)
  | done
  deriving DecidableEq, Fintype

Uses 6 · Used by 34

Statement usesStages of the multiplication 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 first precomputation part · Labels of the second precomputation part

Used byLabel after a literal routine (initial-row generator) · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop on the whole input · The I3 loop · Counter part of one I3 iteration · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The initial-row generator · Labels of the initial-row generator for a layout · Entry label of a literal routine (initial-row generator) · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · Label after a failed read test · Label after a phase loop · Label after a clause · One phase loop · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · The first read test · 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 program on the real generators · The composed machine, raw input to formula · The full machine as a finite multi-stack Turing machine

DefinitionEntry label of a literal routine (initial-row generator)#✓fully proved

For a clause kind \(c\) and \(l \in \mathbb{N}\), among the generator labels with parameters \(g\) and \(n\): the first stage of the routine for literal \(l\) of \(c\) if \(l < n + 2\), and the label \(\mathrm{done}\) otherwise (that case is never used).

def litL (c : CL g n) (l : ℕ) : GL g n := if h : l < n + 2 then .lit c ⟨l, h⟩ .cp1 else .done

Uses 3 · Used by 2

Statement usesClause kinds of the initial-row generator · Labels of the initial-row generator · Stages of the literal routine (initial-row generator)

Used byLabel after a literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator)

DefinitionLabel after a literal routine (initial-row generator)#✓fully proved

Let \(g, n \in \mathbb{N}\), let \(c\) be a clause kind of the generator with parameters \(g\) and \(n\), and let \(l \in \mathbb{N}\). If \(l = 0\), the label is the final routine of \(c\), which emits the leading gap. If \(l \ge 1\), it is the start of the routine for literal \(l - 1\) of \(c\) when \(l - 1 < n + 2\), and the halting label otherwise. The generator goes here after the routine for literal \(l\), and with \(l\) the number of literals of \(c\) before its first literal routine, so literals are emitted from the last to the first.

def after (c : CL g n) (l : ℕ) : GL g n := if l = 0 then .fin c else litL c (l - 1)

Uses 3 · Used by 5

Statement usesClause kinds of the initial-row generator · Labels of the initial-row generator · Entry label of a literal routine (initial-row generator)

Used byRun of one clause (initial-row generator) · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · The counter part of the initial-row generator

DefinitionLabel after a phase loop#✓fully proved

Write \(k_0\) for the stack holding the input. The label the generator moves to when the loop of phase \(p\) finishes: the loop head of the prefix phase after the tail phase, the loop head of the certificate phase after the prefix phase, the head of the input loop after the certificate phase, the loop head of the phase for the stacks \(k < k_0\) after the phase for the stacks \(k > k_0\), and the first step of the start-code clause after the phase for the stacks \(k < k_0\).

def next : PH → GL g n
  | .tail => .hd .pre
  | .pre => .hd .cert
  | .cert => .i3h
  | .o2 => .hd .o1
  | .o1 => .e00 .code

Uses 3 · Used by 3

Statement usesClause kinds of the initial-row generator · Labels of the initial-row generator · Loop phases of the initial-row generator

Used byCorrectness of the init generator, with its explicit time bound · One phase loop · The counter part of the initial-row generator

DefinitionLabel after a clause#✓fully proved

The label the generator moves to after emitting a clause of kind \(c\): the halting label after the start-code clause, the end of the input-loop iteration (which drains the clause base) after an input clause, and the end of the loop iteration of phase \(p\) (which drains the clause base) after a clause of phase \(p\).

def nextC : CL g n → GL g n
  | .code => .done
  | .inp _ => .i3d
  | .ph p => .dr p

Uses 3 · Used by 5

Statement usesClause kinds of the initial-row generator · Labels of the initial-row generator · Loop phases of the initial-row generator

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Correctness of the init generator, with its explicit time bound · The counter part of the initial-row generator

DefinitionThe first read test#✓fully proved

For \(g, n \in \mathbb{N}\), the generator label that tests for input code \(0\) when \(g > 0\), and the error label when \(g = 0\).

def rd0 : GL g n := if h : 0 < g then .rd ⟨0, h⟩ else .bad

Uses 1 · Used by 3

Statement usesLabels of the initial-row generator

Used byThe I3 loop · Counter part of one I3 iteration · The counter part of the initial-row generator

DefinitionLabel after a failed read test#✓fully proved

For a code \(i < g\), the label reached when the read test for \(i\) fails is the read test for \(i + 1\) if \(i + 1 < g\), and the halting error label otherwise.

def miss (i : Fin g) : GL g n := if h : i.val + 1 < g then .rd ⟨i.val + 1, h⟩ else .bad

Uses 1 · Used by 2

Statement usesLabels of the initial-row generator

Used byThe I3 loop · The initial-row generator

AbbreviationLabels of the initial-row generator for a layout#✓fully proved

For a layout \(L\) and a list \(y\) of certificate codes, the label type of the generator is the type of labels of the initial-row generator with parameters \(g\), the number of symbol codes of \(L\), and \(n\), the length of \(y\).

abbrev Lb := GL L.g ycs.length

Uses 2 · Used by 17

Statement usesVariable layout of the transition clauses · Labels of the initial-row generator

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop on the whole input · The I3 loop · Counter part of one I3 iteration · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The initial-row generator · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · One phase loop · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator

DefinitionThe literal routine of the initial-row generator#✓fully proved

For a clause kind \(c\) and a literal index \(l < n + 2\), where \(n\) is the number of certificate codes, the counter program at the stages of the routine for literal \(l\) of \(c\). It copies the base counter of \(c\) into the counter \(Q\) (restoring the base counter through a scratch counter) and adds the offset of literal \(l\) to \(Q\). It then repeats: pop a unit from the counter \(P\) (halting if \(P\) is empty) and compare \(P\) with \(Q\), restoring both. If they are equal, it prepends the slot code of the sign of literal \(l\) to the output, empties \(Q\) and goes to the label before literal \(l\): the routine for literal \(l - 1\), or the leading gap of the clause if \(l = 0\). Otherwise it prepends the gap code \(01\) to the output and repeats.

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

Uses 18 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Variable layout of the transition clauses · Counters of the initial-row generator · Clause kinds of the initial-row generator · Base counter of a clause kind (initial-row generator) · Literal offsets · Literal signs of an init-family clause kind · Labels of the initial-row generator · Label after a literal routine (initial-row generator) · Stages of the literal routine (initial-row generator) · Labels of the initial-row generator for a layout · 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 byThe counter part of the initial-row generator

DefinitionThe counter part of the initial-row generator#✓fully proved

Let \(L\) be a layout with label block size \(A\), \(K\) stacks and \(g\) symbol codes, let \(i_c\) and \(k_0\) be natural numbers and let \(y\) be a list of \(n\) certificate codes. The counter part assigns to each label of the initial-row generator for \(g\) and \(n\) a statement of the counter machine with the generator's counters and a Boolean flag, as follows. Every pop sets the flag to whether a unit was popped, and pushes leave it unchanged. Below, to copy \(a\) into \(b\) is to use two labels, the first moving \(a\) unit by unit into both \(b\) and the scratch counter tmp and the second moving tmp back into \(a\); to multiply \(a \cdot b\) into \(c\) is to run the multiplication routine adding \(a \cdot b\) to \(c\) with loop index md and scratch tmp; to add \(j\) to \(a\) is to prepend \(j\) units to \(a\) in one step; and to drain \(a\) is to empty it one unit per step.

The first precomputation part adds \(g\) to Gc; copies Xn into Mm, En into Mm, Mm into Hs and Fn into Hs; multiplies Hs \(\cdot\) Gc into HG; adds \(A\) to Wc and \(K\) to KA; multiplies KA \(\cdot\) HG into Wc and drains KA; increments Tn; and multiplies Tn \(\cdot\) Wc into Vc. The second part adds \(A\) to ZA and \(k_0\) to KA, multiplies KA \(\cdot\) HG into ZA and drains KA; copies ZA into Z45 and multiplies Xn \(\cdot\) Gc into Z45; copies ZA into Z6 and multiplies Mm \(\cdot\) Gc into Z6; adds \(A\) to Z1; copies ZA into Z2 and HG into Z2; adds \(k_0\) to KA, multiplies KA \(\cdot\) Hs into N1 and drains KA; adds \(K - k_0 - 1\) (truncated subtraction) to KA, multiplies KA \(\cdot\) Hs into N2, drains KA and goes to the loop head of the tail phase.

For a loop phase \(p\) with loop-count counter \(N_p\) and base counter \(Z_p\), the loop head pops \(N_p\); if a unit was popped it pushes a unit onto Id and goes to the body, otherwise it goes to the counter-reset label, which moves Id back into \(N_p\) and goes to the label after the loop of \(p\). The body, made of the base-copy and multiplication labels of \(p\), copies \(Z_p\) into CB, multiplies \(N_p \cdot\) Gc into CB and goes to the clause-start label of the clause of phase \(p\); the base-drain label of \(p\) drains CB and goes to the loop head of \(p\). The head of the input loop pops Xn and goes to the loop head of the phase for the stacks \(k > k_0\) if Xn was empty; otherwise its base-copy and multiplication labels copy ZA into CB, multiply Xn \(\cdot\) Gc into CB and go to the first read test, or to the error label if \(g = 0\). The base-drain label of the input loop drains CB and goes to the head of the input loop. The read tests, the error label and the final label halt.

For a clause kind \(c\), the clause-start label prepends \(00\) to the output; the two labels copying the variable count then copy Vc into \(P\) and go to the label after the literal routine for \(c\) and \(\mathrm{nl}(c)\), the number of literals of \(c\); the labels of literal \(l\) of \(c\) run the literal routine of \(c\) for \(l\); and the leading-gap label of \(c\) drains \(P\), prepending \(01\) to the output for each unit, and then goes to the label after \(c\).

The read tests \(\mathrm{rd}(i)\) halt here; the generator replaces them by tests on its input stack.

Cslib.Complexity.CookLevin.InitFamily.prog · 57 lines

def prog : Lb L ycs → TM2.Stmt (SΓ CK) (Lb L ycs) Bool
  | .pre1 .eg => emitR (.c .Gc) (List.replicate L.g ()) (.pre1 .cpM1)
  | .pre1 .cpM1 => xfer (.c .Xn) [⟨.c .Mm, ()⟩, ⟨.c .tmp, ()⟩] (.pre1 .cpM1) (.pre1 .cpM2)
  | .pre1 .cpM2 => xfer (.c .tmp) [⟨.c .Xn, ()⟩] (.pre1 .cpM2) (.pre1 .cpE1)
  | .pre1 .cpE1 => xfer (.c .En) [⟨.c .Mm, ()⟩, ⟨.c .tmp, ()⟩] (.pre1 .cpE1) (.pre1 .cpE2)
  | .pre1 .cpE2 => xfer (.c .tmp) [⟨.c .En, ()⟩] (.pre1 .cpE2) (.pre1 .cpH1)
  | .pre1 .cpH1 => xfer (.c .Mm) [⟨.c .Hs, ()⟩, ⟨.c .tmp, ()⟩] (.pre1 .cpH1) (.pre1 .cpH2)
  | .pre1 .cpH2 => xfer (.c .tmp) [⟨.c .Mm, ()⟩] (.pre1 .cpH2) (.pre1 .cpF1)
  | .pre1 .cpF1 => xfer (.c .Fn) [⟨.c .Hs, ()⟩, ⟨.c .tmp, ()⟩] (.pre1 .cpF1) (.pre1 .cpF2)
  | .pre1 .cpF2 => xfer (.c .tmp) [⟨.c .Fn, ()⟩] (.pre1 .cpF2) (.pre1 (.hg .head))
  | .pre1 (.hg s) => mulS .Hs .md .Gc .HG .tmp (fun s => .pre1 (.hg s)) (.pre1 .wA) s
  | .pre1 .wA => emitR (.c .Wc) (List.replicate L.A ()) (.pre1 .wK)
  | .pre1 .wK => emitR (.c .KA) (List.replicate L.KK ()) (.pre1 (.w .head))
  | .pre1 (.w s) => mulS .KA .md .HG .Wc .tmp (fun s => .pre1 (.w s)) (.pre1 .wD) s
  | .pre1 .wD => xfer (.c .KA) [] (.pre1 .wD) (.pre1 .inc)
  | .pre1 .inc => incr (.c .Tn) () (.pre1 (.v .head))
  | .pre1 (.v s) => mulS .Tn .md .Wc .Vc .tmp (fun s => .pre1 (.v s)) (.pre2 .zA) s
  | .pre2 .zA => emitR (.c .ZA) (List.replicate L.A ()) (.pre2 .zK)
  | .pre2 .zK => emitR (.c .KA) (List.replicate k0 ()) (.pre2 (.z .head))
  | .pre2 (.z s) => mulS .KA .md .HG .ZA .tmp (fun s => .pre2 (.z s)) (.pre2 .zD) s
  | .pre2 .zD => xfer (.c .KA) [] (.pre2 .zD) (.pre2 .f1)
  | .pre2 .f1 => xfer (.c .ZA) [⟨.c .Z45, ()⟩, ⟨.c .tmp, ()⟩] (.pre2 .f1) (.pre2 .f2)
  | .pre2 .f2 => xfer (.c .tmp) [⟨.c .ZA, ()⟩] (.pre2 .f2) (.pre2 (.f .head))
  | .pre2 (.f s) => mulS .Xn .md .Gc .Z45 .tmp (fun s => .pre2 (.f s)) (.pre2 .s1) s
  | .pre2 .s1 => xfer (.c .ZA) [⟨.c .Z6, ()⟩, ⟨.c .tmp, ()⟩] (.pre2 .s1) (.pre2 .s2)
  | .pre2 .s2 => xfer (.c .tmp) [⟨.c .ZA, ()⟩] (.pre2 .s2) (.pre2 (.s .head))
  | .pre2 (.s s) => mulS .Mm .md .Gc .Z6 .tmp (fun s => .pre2 (.s s)) (.pre2 .z1) s
  | .pre2 .z1 => emitR (.c .Z1) (List.replicate L.A ()) (.pre2 .t1)
  | .pre2 .t1 => xfer (.c .ZA) [⟨.c .Z2, ()⟩, ⟨.c .tmp, ()⟩] (.pre2 .t1) (.pre2 .t2)
  | .pre2 .t2 => xfer (.c .tmp) [⟨.c .ZA, ()⟩] (.pre2 .t2) (.pre2 .t3)
  | .pre2 .t3 => xfer (.c .HG) [⟨.c .Z2, ()⟩, ⟨.c .tmp, ()⟩] (.pre2 .t3) (.pre2 .t4)
  | .pre2 .t4 => xfer (.c .tmp) [⟨.c .HG, ()⟩] (.pre2 .t4) (.pre2 .nK)
  | .pre2 .nK => emitR (.c .KA) (List.replicate k0 ()) (.pre2 (.n .head))
  | .pre2 (.n s) => mulS .KA .md .Hs .N1 .tmp (fun s => .pre2 (.n s)) (.pre2 .nD) s
  | .pre2 .nD => xfer (.c .KA) [] (.pre2 .nD) (.pre2 .qK)
  | .pre2 .qK => emitR (.c .KA) (List.replicate (L.KK - k0 - 1) ()) (.pre2 (.q .head))
  | .pre2 (.q s) => mulS .KA .md .Hs .N2 .tmp (fun s => .pre2 (.q s)) (.pre2 .qD) s
  | .pre2 .qD => xfer (.c .KA) [] (.pre2 .qD) (.hd .tail)
  | .hd p => forHead (.c p.cN) (.c .Id) () (.b1 p) (.rs p)
  | .rs p => xfer (.c .Id) [⟨.c p.cN, ()⟩] (.rs p) (GL.next p)
  | .b1 p => xfer (.c p.cZ) [⟨.c .CB, ()⟩, ⟨.c .tmp, ()⟩] (.b1 p) (.b2 p)
  | .b2 p => xfer (.c .tmp) [⟨.c p.cZ, ()⟩] (.b2 p) (.bM p .head)
  | .bM p s => mulS p.cN .md .Gc .CB .tmp (.bM p) (.e00 (.ph p)) s
  | .dr p => xfer (.c .CB) [] (.dr p) (.hd p)
  | .i3h => decr (.c .Xn) (.hd .o2) .i3b1
  | .i3b1 => xfer (.c .ZA) [⟨.c .CB, ()⟩, ⟨.c .tmp, ()⟩] .i3b1 .i3b2
  | .i3b2 => xfer (.c .tmp) [⟨.c .ZA, ()⟩] .i3b2 (.i3M .head)
  | .i3M s => mulS .Xn .md .Gc .CB .tmp .i3M GL.rd0 s
  | .rd _ => .halt
  | .i3d => xfer (.c .CB) [] .i3d .i3h
  | .bad => .halt
  | .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) (GL.after c c.nl)
  | .lit c l s => litP L ic ycs c l s
  | .fin c => xferE (.c .P) .out [false, true] (.fin c) (GL.nextC c)
  | .done => .halt

Uses 28 · Used by 10

Statement usesStages 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 · Counters of the initial-row generator · Clause kinds of the initial-row generator · Number of literals of a clause kind · Labels of the initial-row generator · Label after a literal routine (initial-row generator) · Label after a phase loop · Label after a clause · The first read test · Stages of the literal routine (initial-row generator) · Labels of the initial-row generator for a layout · Loop phases of the initial-row generator · Loop-count counter of a phase (initial-row generator) · Base counter of a phase (initial-row generator) · Labels of the first precomputation part · Labels of the second precomputation part · The literal routine of the initial-row generator · Flag bit of a machine state · Decrement · Prepending a constant list · Loop head of a for loop over a counter · Counter increment · Counter transfer loop · Draining a counter while prepending a block

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · Correctness of the init generator, with its explicit time bound · The initial-row generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · One phase loop · Run of the precomputation (initial-row generator)

DefinitionThe initial-row generator#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, let \(i_c\) and \(k_0\) be natural numbers and let \(y\) be a list of certificate codes. The generator assigns to each label of the initial-row generator for \(L\) and \(y\) a machine statement with a Boolean flag on the stacks of the counter machine with the generator's counters plus an input stack of codes below \(g\), as follows. At the read test label \(\mathrm{rd}(i)\) for a code \(i < g\), it is the read test for code \(i\) that goes on success to the clause-start label of the input clause with code \(i\) and on failure to the label after a failed read test for \(i\). At every other label, it is the statement of the counter part of the generator for \(L\), \(i_c\), \(k_0\), \(y\) at that label, translated along the embedding of the counter stacks into the generator's stacks, with labels unchanged.

def iprog : Lb L ycs → TM2.Stmt (IΓ CK (Fin L.g)) (Lb L ycs) Bool
  | .rd i => rdS (fun c => .e00 (.inp c)) GL.miss i
  | l => mapS liftE id (prog L ic k0 ycs l)

Uses 19 · Used by 9

Statement usesStages of the multiplication routine · Stacks of a counter machine · Alphabets of a counter machine · Variable layout of the transition clauses · Counters of the initial-row generator · Clause kinds of the initial-row generator · Labels of the initial-row generator · Label after a failed read test · 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) · Labels of the initial-row generator for a layout · Loop phases of the initial-row generator · Labels of the first precomputation part · Labels of the second precomputation part · The counter stacks inside the generator's stacks · The counter part of the initial-row generator · Read test for one code · Translating a statement along a stack embedding

Used byThe I3 loop on the whole input · The I3 loop · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · The init generator as a finite multi-stack machine · The host on the real generators of a machine · The assembled generator, after the precomputation

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

For a layout \(L\) with \(g\) symbol codes, a start code \(i_c\), a stack \(k_0\) and a code list \(Y\), this is the finite multi-stack Turing machine whose stacks are the generator's counters, its Boolean output stack and an extra input stack, with the extra stack as input stack and the Boolean stack as output stack; whose stack alphabets are unit symbols on the counters, bits on the output stack and codes below \(g\) on the input stack; whose labels are the generator's labels, starting at the first precomputation label; whose internal state is a Boolean starting at false; and whose transition function is the generator for \(L, i_c, k_0, Y\).

It records only that the generator is a finite machine.

def initTM : FinTM2 where
  K := IK CK
  k₀ := .inp
  k₁ := .b .out
  Γ := IΓ CK (Fin L.g)
  Λ := Lb L ycs
  main := .pre1 .eg
  σ := Bool
  initialState := false
  m := iprog L ic k0 ycs

Uses 14

Statement usesStages of the multiplication routine · Stacks of a counter machine · Variable layout of the transition clauses · 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) · Labels of the initial-row generator for a layout · Loop phases of the initial-row generator · Labels of the first precomputation part · Labels of the second precomputation part · The initial-row generator

Clause kinds: literal positions

DefinitionLiterals of a clause kind#✓fully proved

Given natural numbers \(i_c\) and \(g'\), a list \(y\) of natural numbers, a base position \(B\) and a clause kind \(c\), the literal list of \(c\) at base \(B\) is the list of the pairs \((B + \mathrm{off}(c, l), \mathrm{sg}(c, l))\) for \(l = 0, 1, \dots, \mathrm{nl}(c) - 1\) in order, where \(\mathrm{nl}(c)\) is the number of literals of \(c\), \(\mathrm{off}(c, l)\) is the offset of literal \(l\) (computed from \(i_c\), \(g'\) and \(y\)) and \(\mathrm{sg}(c, l)\) is its sign.

def clits (B : ℕ) (c : CL g n) : List (ℕ × Bool) :=
  (List.range c.nl).map fun l => (B + c.off ic g' ycs l, c.sg l)

Uses 4 · Used by 6

Statement usesClause kinds of the initial-row generator · Number of literals of a clause kind · Literal offsets · Literal signs of an init-family clause kind

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Correctness of the init generator, with its explicit time bound · Run of the literal routines of a clause (initial-row generator) · One phase loop

DefinitionWell-formed init-family clause kinds#✓fully proved

Fix natural numbers \(i_c\) and \(g'\) and a list \(Y\) of natural numbers, which determine the offsets of the literals of each clause kind from the base. A clause kind \(c\) is well formed when these offsets are strictly increasing: for every \(l \in \mathbb{N}\) with \(l + 1\) less than the number of literals of \(c\), the offset of literal \(l\) of \(c\) is less than the offset of literal \(l + 1\) of \(c\).

def WF (c : CL g n) : Prop := ∀ l, l + 1 < c.nl → c.off ic g' ycs l < c.off ic g' ycs (l + 1)

Uses 3 · Used by 5

Statement usesClause kinds of the initial-row generator · Number of literals of a clause kind · Literal offsets

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · Correctness of the init generator, with its explicit time bound · Run of the literal routines of a clause (initial-row generator) · One phase loop

DefinitionBoundary before a literal (initial-row generator)#✓fully proved

For a bound \(V\), a base \(B\), a clause kind \(c\) and \(l \in \mathbb{N}\), the boundary before literal \(l\) is \(B + \mathrm{off}_c(l)\), the position of literal \(l\), when \(l\) is less than the number of literals of \(c\), and \(V\) otherwise. Here \(\mathrm{off}_c(l)\) is the offset of literal \(l\) of \(c\) determined by the start code \(ic\), the symbol count \(g'\) and the certificate codes \(ycs\).

def bnd (V B : ℕ) (c : CL g n) (l : ℕ) : ℕ := if l < c.nl then B + c.off ic g' ycs l else V

Uses 3 · Used by 2

Statement usesClause kinds of the initial-row generator · Number of literals of a clause kind · Literal offsets

Used byRun of one clause (initial-row generator) · Run of the literal routines of a clause (initial-row generator)

DefinitionLiterals of a clause kind in range#✓fully proved

Given the start code \(i_c\), a code count \(g'\), the certificate codes \(y\), a bound \(V\), a base \(B\) and a clause kind \(c\) of the init generator, all literals of \(c\) are in range when \(B + \mathrm{off}_c(l) < V\) for every literal index \(l\) less than the number of literals of \(c\), where \(\mathrm{off}_c(l)\) is the offset of literal \(l\) of \(c\) determined by \(i_c\), \(g'\) and \(y\).

def InR (V B : ℕ) (c : CL g n) : Prop := ∀ l, l < c.nl → B + c.off ic g' ycs l < V

Uses 3 · Used by 5

Statement usesClause kinds of the initial-row generator · Number of literals of a clause kind · Literal offsets

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · Correctness of the init generator, with its explicit time bound · Run of the literal routines of a clause (initial-row generator) · One phase loop

Correctness: one literal, one clause (in the counter part)

StructureEmpty scratch counters#✓fully proved

An assignment \(F\) of natural numbers to the generator's counters has empty scratch counters when \(F(Q) = F(\mathrm{tmp}) = F(\mathrm{md}) = F(c_1) = F(c_2) = 0\).

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 9

Statement usesCounters of the initial-row generator

Used byOne phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop on the whole input · The I3 loop · Counter part of one I3 iteration · Correctness of the init generator, with its explicit time bound · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · One phase loop

TheoremRun of one literal routine (initial-row generator)#✓fully proved

For a layout and a list of \(n\) certificate codes, let \(c\) be a clause kind with base counter \(b\), let \(l < n + 2\) be a literal index with offset \(\mathrm{off}(l)\), and let \(F\) be counter values whose scratch counters \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\) are \(0\). Let \(\gamma \in \mathbb{N}\), let \(q = F(b) + \mathrm{off}(l)\) and suppose \(F(P) = q + \gamma + 1\). Then for every output \(o\) and flag \(v\), the counter program runs in at most \(\gamma(3q + 6) + 2F(b) + 4q + 9\) steps from the first stage of the routine for literal \(l\) of \(c\), with flag \(v\), counters \(F\) and output \(o\), to the label before literal \(l\) (the routine for literal \(l - 1\), or the leading gap if \(l = 0\)), with flag false, counters \(F\) except \(P = q\), and output \(s \cdot (01)^{\gamma} \cdot o\), where \(s\) is the slot code of the sign of literal \(l\).

theorem lit_run (c : CL L.g ycs.length) (l : Fin (ycs.length + 2)) (F : CK → ℕ) (hF : Rest F)
    (q gap : ℕ) (hq : q = F c.bc + c.off ic L.g ycs l) (hp : F .P = q + gap + 1) (o : List Bool)
    (v : Bool) :
    RunLe (prog L ic k0 ycs) (gap * (3 * q + 6) + 2 * F c.bc + 4 * q + 9)
      ⟨some (.lit c l .cp1), v, st F o⟩
      ⟨some (GL.after c l), false,
        st (update F .P q) (encodeSlot (some (c.sg l)) ++ rep [false, true] gap ++ o)⟩

Uses 32 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Counters of the initial-row generator · Clause kinds of the initial-row generator · Base counter of a clause kind (initial-row generator) · Literal offsets · Literal signs of an init-family clause kind · Labels of the initial-row generator · Label after a literal routine (initial-row generator) · Stages of the literal routine (initial-row generator) · Labels of the initial-row generator for a layout · Empty scratch counters · The counter part of the initial-row generator · Two-bit code of a slot · Runs within a step budget · Repeated block

Proof usesGap emission in the counter view · Loop phases of the initial-row generator · 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 byRun of the literal routines of a clause (initial-row generator)

DefinitionPer-literal step cost of the initial-row generator#✓fully proved

For \(V \in \mathbb{N}\), the per-literal cost is \(6V + 9\).

It bounds the steps the generator spends on one literal apart from the gap loop.

def litE (V : ℕ) : ℕ := 6 * V + 9

Used by 5

Used byStep bound for one clause (initial-row generator) · Run of one clause (initial-row generator) · Time bound of the init generator at uniform parameters · Polynomial time bound for the init generator · Run of the literal routines of a clause (initial-row generator)

DefinitionStep bound for one clause (initial-row generator)#✓fully proved

For natural numbers \(m\) and \(V\),

\[\mathrm{clauseB}(m, V) = V(3V + 6) + m \cdot \mathrm{litE}(V) + 3V + 4,\]

where \(\mathrm{litE}(V) = 6V + 9\) is the per-literal cost apart from the gap loop.

It bounds the steps the generator takes to emit one clause with at most \(m\) literals over \(V\) variables.

def clauseB (nm V : ℕ) : ℕ := V * (3 * V + 6) + nm * litE V + 3 * V + 4

Uses 1 · Used by 8

Statement usesPer-literal step cost of the initial-row generator

Used byStep bound for one loop iteration (initial-row generator) · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Time bound of the init generator · Time bound of the init generator at uniform parameters · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator

TheoremRun of the literal routines of a clause (initial-row generator)#✓fully proved

Let \(c\) be a clause kind with \(k\) literals at base \(B\), the \(j\)-th at position \(B + \mathrm{off}(j)\), such that the offsets are strictly increasing and every position is below \(V\). For \(l \le k\) let \(b_l\) be \(B + \mathrm{off}(l)\) if \(l < k\) and \(V\) otherwise, let \(\lambda_l\) be the list of literals of \(c\) (position and sign) from index \(l\) on, and let the label before literal \(l\) be the first stage of the routine for literal \(l - 1\), or the leading-gap stage of \(c\) if \(l = 0\). Write \(E(a, \lambda)\) for the gap encoding of the slots \(a, \dots, V - 1\) with literals \(\lambda\). Let \(F\) be counter values whose scratch counters \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\) are \(0\) and whose base counter for \(c\) equals \(B\), and let \(o\) be an output. Then for every \(l \le k\) and flag \(v\) there is a flag \(v'\) such that the counter program runs in at most \(b_l(3V + 6) + l(6V + 9)\) steps from the label before literal \(l\), with flag \(v\), counters \(F\) except \(P = b_l\) and output \(E(b_l, \lambda_l) \cdot 00 \cdot o\), to the leading-gap stage of \(c\), with flag \(v'\), counters \(F\) except \(P = b_0\) and output \(E(b_0, \lambda_0) \cdot 00 \cdot o\).

theorem lits_run {V B : ℕ} {c : CL L.g ycs.length} (hc : WF ic L.g ycs c)
    (hBV : InR ic L.g ycs V B c) (F : CK → ℕ) (hF : Rest F) (hB : F c.bc = B) (o : List Bool) :
    ∀ l, l ≤ c.nl → ∀ v : Bool, ∃ v' : Bool,
      RunLe (prog L ic k0 ycs) (bnd (ic := ic) (g' := L.g) (ycs := ycs) V B c l * (3 * V + 6) +
          l * litE V)
        ⟨some (GL.after c l), v,
          st (update F .P (bnd (ic := ic) (g' := L.g) (ycs := ycs) V B c l))
            (gapEnc (bnd (ic := ic) (g' := L.g) (ycs := ycs) V B c l)
              ((clits ic L.g ycs B c).drop l) V ++ [false, false] ++ o)⟩
        ⟨some (.fin c), v',
          st (update F .P (bnd (ic := ic) (g' := L.g) (ycs := ycs) V B c 0))
            (gapEnc (bnd (ic := ic) (g' := L.g) (ycs := ycs) V B c 0) (clits ic L.g ycs B c) V ++
              [false, false] ++ o)⟩

Uses 33 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Gap encoding of a dense clause · Counters of the initial-row generator · Clause kinds of the initial-row generator · Base counter of a clause kind (initial-row generator) · Number of literals of a clause kind · Labels of the initial-row generator · Label after a literal routine (initial-row generator) · Literals of a clause kind in range · Labels of the initial-row generator for a layout · Empty scratch counters · Well-formed init-family clause kinds · Boundary before a literal (initial-row generator) · Literals of a clause kind · Per-literal step cost of the initial-row generator · The counter part of the initial-row generator · Runs within a step budget

Proof usesIncreasing literal positions · Shifting the start of a gap encoding · Increasing literal sequences · Literal offsets · Literal signs of an init-family clause kind · Entry label of a literal routine (initial-row generator) · Stages of the literal routine (initial-row generator) · Loop phases of the initial-row generator · Run of one literal routine (initial-row generator) · Two-bit code of a slot · Budgeted run · Exact-length runs of a TM2 machine · Repeated block

Used byRun of one clause (initial-row generator)

TheoremRun of one clause (initial-row generator)#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, let \(i_c\) and \(k_0\) be natural numbers and let \(y\) be a list of \(n\) certificate codes. Let \(c\) be a clause kind for \(g\) and \(n\) that is well formed for \(i_c\), \(g\) and \(y\), and let \(V, B\) be natural numbers such that all literals of \(c\) at base \(B\) (for \(i_c\), \(g\) and \(y\)) are in range below \(V\). Let \(F\) be counter values of the generator with empty scratch counters such that \(F(b) = B\) for the base counter \(b\) of \(c\), \(F(\mathrm{Vc}) = V\) and \(F(P) = 0\). Then for every output \(o\) and flag \(v\), the counter part of the generator for \(L\), \(i_c\), \(k_0\), \(y\) runs within the step bound \(\mathrm{clauseB}(n + 2, V)\) for one clause from the clause-start label of \(c\), with flag \(v\), counters \(F\) and output \(o\), to the label after \(c\), with flag false, counters \(F\) and output \(w \cdot o\), where \(w\) is the dense encoding of the dense clause over \(V\) variables built from the literal list of \(c\) at base \(B\) (for \(i_c\), \(g\) and \(y\)).

theorem clause_run {V B : ℕ} {c : CL L.g ycs.length} (hc : WF ic L.g ycs c)
    (hBV : InR ic L.g ycs V B c) (F : CK → ℕ) (hF : Rest F) (hB : F c.bc = B) (hV : F .Vc = V)
    (hP : F .P = 0) (o : List Bool) (v : Bool) :
    RunLe (prog L ic k0 ycs) (clauseB (ycs.length + 2) V) ⟨some (.e00 c), v, st F o⟩
      ⟨some (GL.nextC c), false,
          st F (encodeClause (denseClause V (clits ic L.g ycs B c)) ++ o)⟩

Uses 45 · Used by 3

Statement usesStacks 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 · Counters of the initial-row generator · Clause kinds of the initial-row generator · Base counter of a clause kind (initial-row generator) · Labels of the initial-row generator · Label after a clause · Literals of a clause kind in range · Labels of the initial-row generator for a layout · Empty scratch counters · Well-formed init-family clause kinds · Step bound for one clause (initial-row generator) · Literals of a clause kind · The counter part of the initial-row generator · Dense encoding of a clause · Runs within a step budget

Proof usesIncreasing literal positions · Lowering the lower bound keeps a literal list increasing · Encoding a dense clause block by block · Gap encoding of a dense clause · Shifting the start of a gap encoding · Increasing literal sequences · Number of literals of a clause kind · Literal offsets · Literal signs of an init-family clause kind · Label after a literal routine (initial-row generator) · Loop phases of the initial-row generator · Boundary before a literal (initial-row generator) · Per-literal step cost of the initial-row generator · Run of the literal routines of a clause (initial-row generator) · 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 byOne phase-loop iteration of the initial-row generator · The I3 loop · Correctness of the init generator, with its explicit time bound

Correctness: the five phase loops (counter part)

DefinitionStep bound for one loop iteration (initial-row generator)#✓fully proved

For natural numbers \(m, g, N, V\),

\[\mathrm{bodyB}(m,g,N,V) = 2V + 2 + (N(2g+3) + N + 2) + g + 1 + \mathrm{clauseB}(m,V) + V + 1,\]

where \(\mathrm{clauseB}(m, V)\) is the step bound for one clause with at most \(m\) literals.

It bounds one iteration of any phase loop, and one I3 iteration including its read.

def bodyB (nm g N V : ℕ) : ℕ :=
  2 * V + 2 + (N * (2 * g + 3) + N + 2) + g + 1 + clauseB nm V + V + 1

Uses 1 · Used by 8

Statement usesStep bound for one clause (initial-row generator)

Used byOne phase-loop iteration of the initial-row generator · The I3 loop on the whole input · The I3 loop · Time bound of the init generator at uniform parameters · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · Step bound of one phase loop (initial-row generator) · One phase loop

TheoremOne phase-loop iteration of the initial-row generator#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, let \(ic, k_0 \in \mathbb{N}\), let \(ycs\) be a list of \(n\) certificate codes, and let \(p\) be a loop phase with base counter \(c_Z(p)\) and loop-count counter \(c_N(p)\). Let \(F\) give the value of each generator counter, with the scratch counters empty (\(\mathrm{Rest}(F)\)), \(F(\mathrm{CB}) = F(\mathrm{P}) = 0\), \(F(\mathrm{Vc}) = V\), \(F(\mathrm{Gc}) = g\), \(F(c_Z(p)) = Z\) and \(F(c_N(p)) = t\). Suppose \(t < N\) and \(tg + Z \le V\), the clause kind of \(p\) has strictly increasing literal offsets, and all its literals at base \(tg + Z\) lie below \(V\). Then for every output \(o\) and flag \(v\), the counter program of the generator runs in at most \(\mathrm{bodyB}(n + 2, g, N, V)\) steps from label \(b_1(p)\) with flag \(v\), counters \(F\) and output \(o\) to the loop head of \(p\) with flag false, counters \(F\) and output \(\mathrm{encodeClause}(\mathrm{denseClause}(V, \mathrm{clits}(tg + Z, p)))\) followed by \(o\). Here \(\mathrm{clits}(tg + Z, p)\) are the literals of the clause kind of \(p\) at base \(tg + Z\).

theorem body_run {p : PH} {V Z N t : ℕ} (F : CK → ℕ) (hF : Rest F) (hCB : F .CB = 0)
    (hP : F .P = 0) (hV : F .Vc = V) (hG : F .Gc = L.g) (hZ : F p.cZ = Z) (ht : F p.cN = t)
    (htN : t < N) (hBV : t * L.g + Z ≤ V) (hW : WF ic L.g ycs (CL.ph p : CL L.g ycs.length))
    (hR : InR ic L.g ycs V (t * L.g + Z) (CL.ph p : CL L.g ycs.length)) (o : List Bool)
    (v : Bool) :
    RunLe (prog L ic k0 ycs) (bodyB (ycs.length + 2) L.g N V) ⟨some (.b1 p), v, st F o⟩
      ⟨some (.hd p), false,
        st F (encodeClause (denseClause V (clits ic L.g ycs (t * L.g + Z)
          (CL.ph p : CL L.g ycs.length))) ++ o)⟩

Uses 36 · Used by 1

Statement usesStacks 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 · Counters of the initial-row generator · Clause kinds of the initial-row generator · Labels of the initial-row generator · Literals of a clause kind in range · Labels of the initial-row generator for a layout · Loop phases of the initial-row generator · Loop-count counter of a phase (initial-row generator) · Base counter of a phase (initial-row generator) · Empty scratch counters · Well-formed init-family clause kinds · Step bound for one loop iteration (initial-row generator) · Literals of a clause kind · The counter part of the initial-row generator · Dense encoding of a clause · 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 · Base counter of a clause kind (initial-row generator) · Label after a clause · Step bound for one clause (initial-row generator) · Run of one clause (initial-row generator) · Budgeted run · Flag bit of a machine state · Exact-length runs of a TM2 machine · Adding units to target stacks · Unary counter · Copying a counter through a scratch stack · Multiplying unary counters · Counter transfer loop · Running a counter transfer

Used byOne phase loop

TheoremOne phase loop#✓fully proved

Fix a layout \(L\) with \(g\) symbol codes, a start code \(i_c\), a stack index \(k_0\) and a list \(y\) of \(n\) certificate codes, and let \(M\) be the counter part of the initial-row generator for these parameters. Let \(p\) be a loop phase with loop counter \(N_p\) and base counter \(Z_p\), and let \(F\) be counter values with the scratch counters \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\) empty, \(F(\mathrm{CB}) = F(P) = F(\mathrm{Id}) = 0\), \(F(\mathrm{Vc}) = V\), \(F(\mathrm{Gc}) = g\), \(F(Z_p) = Z\) and \(F(N_p) = N\), where \(N \le N_b\). Suppose the literal offsets of phase \(p\) (for \(i_c\), \(g\) and \(y\)) are strictly increasing and, for every \(t < N\), \(tg + Z \le V\) and every literal of the phase-\(p\) clause at base \(tg + Z\) has position below \(V\). Then for every output \(o\) and flag \(v\), \(M\) goes in at most \(N_b(b + 1) + N_b + 2\) steps from the loop head of phase \(p\) with flag \(v\), counters \(F\) and output \(o\) to the label after the loop of phase \(p\) with flag false, counters \(F\) and output \(B_0 B_1 \cdots B_{N-1}\, o\). Here \(B_t\) is the encoding of the dense clause over \(V\) variables with the literals of the phase-\(p\) clause at base \(tg + Z\), and \(b\) is the loop-iteration cost bound for \(n + 2\) literals, \(g\) codes, loop count \(N_b\) and \(V\) variables.

theorem phase_run {p : PH} {V Z N Nb : ℕ} (F : CK → ℕ) (hF : Rest F) (hCB : F .CB = 0)
    (hP : F .P = 0) (hV : F .Vc = V) (hG : F .Gc = L.g) (hZ : F p.cZ = Z) (hN : F p.cN = N)
    (hId : F .Id = 0) (hNb : N ≤ Nb) (hW : WF ic L.g ycs (CL.ph p : CL L.g ycs.length))
    (hBV : ∀ t < N, t * L.g + Z ≤ V)
    (hR : ∀ t < N, InR ic L.g ycs V (t * L.g + Z) (CL.ph p : CL L.g ycs.length)) (o : List Bool)
    (v : Bool) :
    RunLe (prog L ic k0 ycs) (Nb * (bodyB (ycs.length + 2) L.g Nb V + 1) + Nb + 2)
      ⟨some (.hd p), v, st F o⟩
      ⟨some (GL.next p), false, st F ((List.range N).flatMap
        (fun t => encodeClause (denseClause V (clits ic L.g ycs (t * L.g + Z)
          (CL.ph p : CL L.g ycs.length)))) ++ o)⟩

Uses 24 · Used by 1

Statement usesStacks 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 · Counters of the initial-row generator · Clause kinds of the initial-row generator · Labels of the initial-row generator · Label after a phase loop · Literals of a clause kind in range · Labels of the initial-row generator for a layout · Loop phases of the initial-row generator · Loop-count counter of a phase (initial-row generator) · Base counter of a phase (initial-row generator) · Empty scratch counters · Well-formed init-family clause kinds · Step bound for one loop iteration (initial-row generator) · Literals of a clause kind · The counter part of the initial-row generator · Dense encoding of a clause · Runs within a step budget

Proof usesA runtime for loop in the counter view · One phase-loop iteration of the initial-row generator · Exact-length runs of a TM2 machine

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

TheoremCounter part of one I3 iteration#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes. Suppose the counters \(F\) of the init generator's counter part have \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\) and \(\mathrm{CB}\) equal to \(0\), \(\mathrm{Gc} = g\), \(\mathrm{ZA} = Z\) and \(\mathrm{Xn} = r + 1\). Then for every output \(o\) and flag \(v\), the counter part, started at the head of the I3 loop with flag \(v\), counters \(F\) and output \(o\), reaches the first read test (the halting label if \(g = 0\)) in at most \(1 + (2Z + 2) + (r(2g + 3) + r + 2)\) steps, with flag false, output \(o\), and the counters of \(F\) except that \(\mathrm{Xn} = r\) and \(\mathrm{CB} = rg + Z\).

theorem i3pre_run {r ZA : ℕ} (F : CK → ℕ) (hF : Rest F) (hCB : F .CB = 0) (hG : F .Gc = L.g)
    (hZA : F .ZA = ZA) (hX : F .Xn = r + 1) (o : List Bool) (v : Bool) :
    RunLe (prog L ic k0 ycs) (1 + (2 * ZA + 2) + (r * (2 * L.g + 3) + r + 2))
      ⟨some .i3h, v, st F o⟩
      ⟨some GL.rd0, false, st (update (update F .Xn r) .CB (r * L.g + ZA)) o⟩

Uses 23 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Counters of the initial-row generator · Labels of the initial-row generator · The first read test · Labels of the initial-row generator for a layout · Empty scratch counters · The counter part of the initial-row generator · Runs within a step budget

Proof usesStages of the multiplication routine · The multiplication routine of a counter machine · Loop phases of the initial-row generator · 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 · Decrement · Multiplying unary counters · Counter transfer loop

Used byThe I3 loop

Correctness: the I3 loop (reads the input; in the extended machine)

TheoremThe I3 loop#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, consider the init generator for a start code, a stack \(k_0\) and a list of \(\ell\) certificate codes, and let \(x = (x_0, \dots, x_{s-1})\) be a list of codes \(x_j < g\). Suppose its counters \(F\) have \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\), \(\mathrm{CB}\) and \(P\) equal to \(0\), \(\mathrm{Vc} = V\), \(\mathrm{Gc} = g\) and \(\mathrm{ZA} = Z\), that \(jg + Z + g \le V\) for every \(j < s\), and that \(s \le N_b\). Then for every \(r \le s\), every output \(o\) and every flag \(v\), the generator, started at the head of the I3 loop with flag \(v\), the counters of \(F\) except \(\mathrm{Xn} = r\), output \(o\), and \(x_{r-1}, \dots, x_1, x_0\) on its input stack (top first), reaches in at most \(r\beta + 1\) steps the head of the I2 loop over the stacks above \(k_0\), with flag false, the counters of \(F\) except \(\mathrm{Xn} = 0\), an empty input stack, and output \(e_0 e_1 \cdots e_{r-1}\) followed by \(o\). Here \(e_j\) is the encoding of the dense clause over \(V\) variables whose only literal is the positive literal of variable \(jg + Z + x_j\), and \(\beta = 3V^2 + 12V + (\ell + 2)(6V + 9) + (2g + 4)N_b + g + 10\).

theorem i3_run {V ZA Nb : ℕ} (xs : List (Fin L.g)) (F : CK → ℕ) (hF : Rest F) (hCB : F .CB = 0)
    (hP : F .P = 0) (hV : F .Vc = V) (hG : F .Gc = L.g) (hZA : F .ZA = ZA)
    (hR : ∀ j < xs.length, j * L.g + ZA + L.g ≤ V) (hNb : xs.length ≤ Nb) :
    ∀ r, r ≤ xs.length → ∀ (o : List Bool) (v : Bool),
      RunLe (iprog L ic k0 ycs) (r * bodyB (ycs.length + 2) L.g Nb V + 1)
        ⟨some .i3h, v, emb (st (update F .Xn r) o) (xs.take r).reverse⟩
        ⟨some (.hd .o2), false, emb (st (update F .Xn 0) ((List.range r).flatMap
          (fun j => encodeClause (denseClause V
            [(j * L.g + ZA + (xs[j]?).elim 0 Fin.val, true)])) ++ o)) []⟩

Uses 48 · Used by 1

Statement usesStacks of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense clause from a list of literals · 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 initial-row generator for a layout · Loop phases of the initial-row generator · Empty scratch counters · Step bound for one loop iteration (initial-row generator) · Stacks of a counter machine with an extra input stack · The initial-row generator · Dense encoding of a clause · Runs within a step budget

Proof usesStages of the multiplication routine · Alphabets of a counter machine · Clause kinds of the initial-row generator · Base counter of a clause kind (initial-row generator) · Number of literals of a clause kind · Literal offsets · Label after a failed read test · Label after a clause · The first read test · Stages of the literal routine (initial-row generator) · Labels of the first precomputation part · Labels of the second precomputation part · Step bound for one clause (initial-row generator) · Run of one clause (initial-row generator) · Literals of a clause kind · Counter part of one I3 iteration · The counter stacks inside the generator's stacks · The counter part of the initial-row generator · The read chain · Run lifting · Dense clause · Embedding of a machine in a host · Translating a statement along a stack embedding · 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 · Decrement · Counter transfer loop · Running a counter transfer

Used byThe I3 loop on the whole input

Positions, and the machine's blocks are the family's clauses

TheoremRow-0 cells fit in the variable range#✓fully proved

For a layout \(L\) with \(A\) label/state variables, \(KK\) stacks and \(g\) symbol codes, and all \(T, H, q \in \mathbb{N}\) with \(q < KK \cdot H\), we have \(A + q g + g \le V\), where \(V\) is the number of variables of \(L\) for time bound \(T\) and stack height \(H\).

theorem qpos {T H q : ℕ} (hq : q < L.KK * H) : L.A + q * L.g + L.g ≤ L.numVars T H

Uses 3 · Used by 1

Statement usesVariable layout of the transition clauses · Number of variables of the transition-clause formula

Proof usesVariables per time step

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

TheoremConcatenating consecutive blocks of indices#✓fully proved

Let \(\varphi\) be a function from the natural numbers to a type \(\alpha\) and let \(H\), \(s\), \(r\) be natural numbers. Concatenating, for \(k = s, s + 1, \dots, s + r - 1\) in order, the lists \([\varphi(kH), \varphi(kH + 1), \dots, \varphi(kH + H - 1)]\) gives the list \([\varphi(sH), \varphi(sH + 1), \dots, \varphi(sH + rH - 1)]\).

theorem flat_blocks {α : Type} (H : ℕ) (φ : ℕ → α) (s : ℕ) : ∀ r : ℕ,
    ((List.range r).map (s + ·)).flatMap (fun k => (List.range H).map fun j => φ (k * H + j)) =
      (List.range (r * H)).map fun q => φ (s * H + q)

Used by 1

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

Precomputation and the whole generator

DefinitionInitial counters of the init generator#✓fully proved

For natural numbers \(T, n, e, f\), the counters \(\mathrm{Tn}\), \(\mathrm{Xn}\), \(\mathrm{En}\) and \(\mathrm{Fn}\) of the generator hold \(T\), \(n\), \(e\) and \(f\) respectively, and every other counter holds \(0\).

In use, \(n\) is the length of the input code list, \(e = m - n\) and \(f = H - m\), where \(m\) is the depth at which the certificate block ends and \(H\) is the stack height.

def initF (T n e f : ℕ) : CK → ℕ
  | .Tn => T
  | .Xn => n
  | .En => e
  | .Fn => f
  | _ => 0

Uses 1 · Used by 7

Statement usesCounters of the initial-row generator

Used byThe init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · Run of the precomputation (initial-row generator) · The assembled generator, after the precomputation · The composed machine, raw input to formula

DefinitionCounters after the precomputation#✓fully proved

For a layout \(L\) with \(A\) label/state variables, \(K\) stacks and \(g\) symbol codes, a stack index \(k_0\) and numbers \(T, n, e, f\), write \(H = n + e + f\). The counter values after the precomputation are \(\mathrm{Tn} = T + 1\), \(\mathrm{Xn} = n\), \(\mathrm{En} = e\), \(\mathrm{Fn} = f\), \(\mathrm{Gc} = g\), \(\mathrm{Mm} = n + e\), \(\mathrm{Hs} = H\), \(\mathrm{HG} = Hg\), \(\mathrm{Wc} = A + KHg\) (the row width), \(\mathrm{Vc} = (T + 1)(A + KHg)\) (the number of variables), \(\mathrm{ZA} = A + k_0Hg\), \(\mathrm{Z45} = A + (k_0H + n)g\), \(\mathrm{Z6} = A + (k_0H + n + e)g\), \(\mathrm{Z1} = A\), \(\mathrm{Z2} = A + (k_0 + 1)Hg\), \(\mathrm{N1} = k_0H\) and \(\mathrm{N2} = (K - k_0 - 1)H\) (truncated subtraction), and \(0\) for every other counter.

Cslib.Complexity.CookLevin.InitFamily.preF · 19 lines

def preF (L : Layout) (k0 T n e f : ℕ) : CK → ℕ
  | .Tn => T + 1
  | .Xn => n
  | .En => e
  | .Fn => f
  | .Gc => L.g
  | .Mm => n + e
  | .Hs => n + e + f
  | .HG => (n + e + f) * L.g
  | .Wc => L.rowW (n + e + f)
  | .Vc => L.numVars T (n + e + f)
  | .ZA => L.cIdx (n + e + f) 0 k0 0 0
  | .Z45 => L.cIdx (n + e + f) 0 k0 n 0
  | .Z6 => L.cIdx (n + e + f) 0 k0 (n + e) 0
  | .Z1 => L.A
  | .Z2 => L.cIdx (n + e + f) 0 (k0 + 1) 0 0
  | .N1 => k0 * (n + e + f)
  | .N2 => (L.KK - k0 - 1) * (n + e + f)
  | _ => 0

Uses 5 · Used by 2

Statement usesVariable 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 · Counters of the initial-row generator

Used byCorrectness of the init generator, with its explicit time bound · Run of the precomputation (initial-row generator)

DefinitionStep bound for the precomputation#✓fully proved

For a layout \(L\) with \(A\) label/state variables, \(K\) stacks and \(g\) symbol codes, and numbers \(k_0, q, T, n, e, f\), write \(h = n + e + f\). The bound is

\[ 1 + (2n + 2) + (2e + 2) + (2(n + e) + 2) + (2f + 2) + (h(2g + 3) + h + 2) + 1 + 1 + (K(2hg + 3) + K + 2) + (K + 1) + 1 + ((T + 1)(2(Khg + A) + 3) + (T + 1) + 2) + 1 + 1 + (k_0(2hg + 3) + k_0 + 2) + (k_0 + 1) + (2(k_0 hg + A) + 2) + (n(2g + 3) + n + 2) + (2(k_0 hg + A) + 2) + ((n + e)(2g + 3) + (n + e) + 2) + 1 + (2(k_0 hg + A) + 2) + (2hg + 2) + 1 + (k_0(2h + 3) + k_0 + 2) + (k_0 + 1) + 1 + (q(2h + 3) + q + 2) + (q + 1). \]

The precomputation uses it with \(q = K - k_0 - 1\).

def preB (L : Layout) (k0 q T n e f : ℕ) : ℕ :=
  1 + (2 * n + 2) + (2 * e + 2) + (2 * (n + e) + 2) + (2 * f + 2) +
    ((n + e + f) * (2 * L.g + 3) + (n + e + f) + 2) + 1 + 1 +
    (L.KK * (2 * ((n + e + f) * L.g) + 3) + L.KK + 2) + (L.KK + 1) + 1 +
    ((T + 1) * (2 * (L.KK * ((n + e + f) * L.g) + L.A) + 3) + (T + 1) + 2) + 1 + 1 +
    (k0 * (2 * ((n + e + f) * L.g) + 3) + k0 + 2) + (k0 + 1) +
    (2 * (k0 * ((n + e + f) * L.g) + L.A) + 2) + (n * (2 * L.g + 3) + n + 2) +
    (2 * (k0 * ((n + e + f) * L.g) + L.A) + 2) + ((n + e) * (2 * L.g + 3) + (n + e) + 2) + 1 +
    (2 * (k0 * ((n + e + f) * L.g) + L.A) + 2) + (2 * ((n + e + f) * L.g) + 2) + 1 +
    (k0 * (2 * (n + e + f) + 3) + k0 + 2) + (k0 + 1) + 1 +
    (q * (2 * (n + e + f) + 3) + q + 2) + (q + 1)

Uses 1 · Used by 5

Statement usesVariable layout of the transition clauses

Used byTime bound of the init generator · Time bound of the init generator at uniform parameters · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · Run of the precomputation (initial-row generator)

TheoremRun of the precomputation (initial-row generator)#✓fully proved

Let \(L\) be a layout with \(K\) stacks, let \(i_c\) and \(k_0\) be natural numbers and let \(y\) be a list of certificate codes. For all natural numbers \(T, n, e, f\) and every output \(o\), the counter part of the generator for \(L\), \(i_c\), \(k_0\), \(y\) runs within \(\mathrm{preB}(L, k_0, K - k_0 - 1, T, n, e, f)\) steps, the step bound for the precomputation (with truncated subtraction), from the label \(\mathrm{eg}\) of the first precomputation part (its first stage), with flag false, the initial counters for \(T, n, e, f\) and output \(o\), to the loop head of the tail phase, with flag false, the counters after the precomputation for \(L, k_0, T, n, e, f\) and output \(o\).

theorem pre_run (T n e f : ℕ) (o : List Bool) :
    RunLe (prog L ic k0 ycs) (preB L k0 (L.KK - k0 - 1) T n e f)
      ⟨some (.pre1 .eg), false, st (initF T n e f) o⟩
      ⟨some (.hd .tail), false, st (preF L k0 T n e f) o⟩

Uses 33 · Used by 1

Statement usesStacks of a counter machine · Alphabets of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Counters of the initial-row generator · Labels of the initial-row generator · Labels of the initial-row generator for a layout · Loop phases of the initial-row generator · Labels of the first precomputation part · Initial counters of the init generator · Step bound for the precomputation · Counters after the precomputation · The counter part of the initial-row generator · 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 · Labels of the second precomputation part · 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 · Counter increment · Multiplying unary counters · Pushing a list of symbols onto one stack · Counter transfer loop · Running a counter transfer

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

TheoremThe I3 loop on the whole input#✓fully proved

Let \(L\) be a layout with \(g\) symbol codes, consider the init generator for a start code, a stack \(k_0\) and a list of \(\ell\) certificate codes, and let \(x = (x_0, \dots, x_{s-1})\) be a list of codes \(x_j < g\). Suppose its counters \(F\) have \(Q\), \(\mathrm{tmp}\), \(\mathrm{md}\), \(c_1\), \(c_2\), \(\mathrm{CB}\) and \(P\) equal to \(0\), \(\mathrm{Vc} = V\), \(\mathrm{Gc} = g\), \(\mathrm{ZA} = Z\) and \(\mathrm{Xn} = s\), that \(jg + Z + g \le V\) for every \(j < s\), and that \(s \le N_b\). Then for every output \(o\) and every flag \(v\), the generator, started at the head of the I3 loop with flag \(v\), counters \(F\), output \(o\), and \(x_{s-1}, \dots, x_1, x_0\) on its input stack (top first), reaches in at most \(s\beta + 1\) steps the head of the I2 loop over the stacks above \(k_0\), with flag false, the counters of \(F\) except \(\mathrm{Xn} = 0\), an empty input stack, and output \(e_0 e_1 \cdots e_{s-1}\) followed by \(o\). Here \(e_j\) is the encoding of the dense clause over \(V\) variables whose only literal is the positive literal of variable \(jg + Z + x_j\), and \(\beta = 3V^2 + 12V + (\ell + 2)(6V + 9) + (2g + 4)N_b + g + 10\).

theorem i3_full {L : Layout} {ic k0 : ℕ} {ycs : List ℕ} {V ZA Nb : ℕ} (xs : List (Fin L.g))
    (F : CK → ℕ) (hF : Rest F) (hCB : F .CB = 0) (hP : F .P = 0) (hV : F .Vc = V)
    (hG : F .Gc = L.g) (hZA : F .ZA = ZA) (hX : F .Xn = xs.length)
    (hR : ∀ j < xs.length, j * L.g + ZA + L.g ≤ V) (hNb : xs.length ≤ Nb) (o : List Bool)
    (v : Bool) :
    RunLe (iprog L ic k0 ycs) (xs.length * bodyB (ycs.length + 2) L.g Nb V + 1)
      ⟨some .i3h, v, emb (st F o) xs.reverse⟩
      ⟨some (.hd .o2), false, emb (st (update F .Xn 0) ((List.range xs.length).flatMap
        (fun j => encodeClause (denseClause V
          [(j * L.g + ZA + (xs[j]?).elim 0 Fin.val, true)])) ++ o)) []⟩

Uses 17 · Used by 1

Statement usesStacks of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · Dense clause from a list of literals · 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 initial-row generator for a layout · Loop phases of the initial-row generator · Empty scratch counters · Step bound for one loop iteration (initial-row generator) · Stacks of a counter machine with an extra input stack · The initial-row generator · Dense encoding of a clause · Runs within a step budget

Proof usesThe I3 loop

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

The whole generator

DefinitionStep bound of one phase loop (initial-row generator)#✓fully proved

For \(m, g, N, V \in \mathbb{N}\), the cost of one phase loop with count bound \(N\) is \(N(\beta + 1) + N + 2\), where \(\beta\) is the cost of one loop iteration with clauses of at most \(m\) literals, \(g\) symbol codes, count bound \(N\) and \(V\) variables.

def loopB (nm g NB V : ℕ) : ℕ := NB * (bodyB nm g NB V + 1) + NB + 2

Uses 1 · Used by 4

Statement usesStep bound for one loop iteration (initial-row generator)

Used byTime bound of the init generator · Time bound of the init generator at uniform parameters · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator

DefinitionTime bound of the init generator#✓fully proved

Let \(L\) be a layout with \(A\) label/state variables, \(K\) stacks and \(g\) symbol codes, and let \(n_Y, k_0, q, T, n, e, f\) be natural numbers. Put \(H = n + e + f\) and let \(V = (T + 1)(A + K H g)\) be the number of variables. The bound is the precomputation cost \(\mathrm{preB}(L, k_0, q, T, n, e, f)\), plus \(6\) times the phase-loop cost \(\mathrm{loopB}(n_Y + 2, g, K H + H, V)\), plus the clause cost \(\mathrm{clauseB}(n_Y + 2, V)\).

The generator uses it with \(q = K - k_0 - 1\).

def initBound (L : Layout) (nY k0 q T n e f : ℕ) : ℕ :=
  preB L k0 q T n e f +
    6 * loopB (nY + 2) L.g (L.KK * (n + e + f) + (n + e + f)) (L.numVars T (n + e + f)) +
    clauseB (nY + 2) (L.numVars T (n + e + f))

Uses 5 · Used by 3

Statement usesVariable layout of the transition clauses · Number of variables of the transition-clause formula · Step bound for one clause (initial-row generator) · Step bound of one phase loop (initial-row generator) · Step bound for the precomputation

Used byTime bound of the init generator at uniform parameters · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator

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

Let \(L\) be a layout with \(A\) label/state variables, \(K\) stacks and \(g > 0\) symbol codes, let \(i_c < A\) and \(k_0 < K\), and let \(Y\) be a strictly increasing list of codes with \(0 < y < g\) for every \(y \in Y\). Let \(xs\) be a list of codes below \(g\) with \(n = |xs|\), let \(T, e, f\) be natural numbers with \(f > 0\), and let \(o\) be a bit string. Start the generator for \(L, i_c, k_0, Y\) at its start label with state false, with the counters \(\mathrm{Tn}, \mathrm{Xn}, \mathrm{En}, \mathrm{Fn}\) holding \(T, n, e, f\) in unary and all other counters empty, \(o\) on the output stack, and \(xs\) reversed on the input stack. Then within \(\mathrm{initBound}(L, |Y|, k_0, K - k_0 - 1, T, n, e, f)\) steps it reaches the final label \(\mathrm{done}\), and its output stack there is the bit encoding of the layout-level init family for \(L, i_c, k_0, Y, xs\), \(m = n + e\), \(T\) and \(H = n + e + f\), followed by \(o\).

theorem init_run (hk0 : k0 < L.KK) (hic : ic < L.A) (hg : 0 < L.g)
    (hy : (0 :: ycs).Pairwise (· < ·)) (hyg : ∀ c ∈ ycs, c < L.g) (xs : List (Fin L.g))
    (T e f : ℕ) (hf : 0 < f) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (IΓ CK (Fin L.g) k)),
      RunLe (iprog L ic k0 ycs) (initBound L ycs.length k0 (L.KK - k0 - 1) T xs.length e f)
        ⟨some (.pre1 .eg), false, emb (st (initF T xs.length e f) o) xs.reverse⟩
        ⟨some .done, v, S⟩ ∧
      S (.b .out) = encodeCNF (initFam L ic k0 ycs xs (xs.length + e) T (xs.length + e + f)) ++ o

Uses 67 · Used by 1

Statement usesStacks of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · 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 initial-row generator for a layout · Labels of the first precomputation part · Stacks of a counter machine with an extra input stack · Time bound of the init generator · Initial counters of the init generator · The init family · The initial-row generator · Dense encoding of a CNF formula · Runs within a step budget

Proof usesStages of the multiplication routine · Alphabets of a counter machine · 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 · Clause kinds of the initial-row generator · Base counter of a clause kind (initial-row generator) · Number of literals of a clause kind · Literal offsets · Literal signs of an init-family clause kind · Label after a phase loop · Label after a clause · Literals of a clause kind in range · Stages of the literal routine (initial-row generator) · Loop phases of the initial-row generator · Loop-count counter of a phase (initial-row generator) · Base counter of a phase (initial-row generator) · Labels of the second precomputation part · Empty scratch counters · Well-formed init-family clause kinds · Step bound for one loop iteration (initial-row generator) · Step bound for one clause (initial-row generator) · Run of one clause (initial-row generator) · Literals of a clause kind · Concatenating consecutive blocks of indices · The I3 loop on the whole input · Certificate clauses of the initial row (I4) · Start-code clause of the initial row (I1) · Input clauses of the initial row (I3) · Row-0 clauses for the other stacks · Row-0 prefix clauses · Row-0 tail clauses · The counter stacks inside the generator's stacks · Step bound of one phase loop (initial-row generator) · One phase loop · Step bound for the precomputation · Counters after the precomputation · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Row-0 cells fit in the variable range · Run lifting · Empty-cell variable of the initial row · Dense CNF formula · Dense clause · Dense encoding of a clause · Embedding of a machine in a host · Translating a statement along a stack embedding · Budgeted run · Exact-length runs of a TM2 machine

Used byPolynomial time bound for the init generator

The time bound is polynomial

TheoremTime bound of the init generator at uniform parameters#✓fully proved

For all natural numbers \(k \ge 1\) and \(y \ge 1\), let \(L\) be the uniform layout with all four parameters equal to \(k\). Then the time bound of the init generator for \(L\) with \(n_Y = k_0 = q = k\) and \(T = n = e = f = y\) is at most \(18928\,k^5 y^5\).

Every monomial of the bound is then at most \(k^5 y^5\), and \(18928\) is the value of the bound at \(k = y = 1\).

theorem initBound_uni (k y : ℕ) (hk : 1 ≤ k) (hy : 1 ≤ y) :
    initBound (Cslib.Complexity.CookLevin.Family.Layout.uni k) k k k y y y y ≤ 18928 * k ^ 5 * y ^ 5

Uses 10 · Used by 1

Statement usesUniform layout · Time bound of the init generator

Proof usesVariable layout of the transition clauses · Number of variables of the transition-clause formula · Variables per time step · Step bound for one loop iteration (initial-row generator) · Step bound for one clause (initial-row generator) · Per-literal step cost of the initial-row generator · Step bound of one phase loop (initial-row generator) · Step bound for the precomputation

Used byPolynomial time bound for the init generator

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

For a layout \(L\) with \(A\) label/state variables, \(K\) stacks and \(g\) symbol codes, and natural numbers \(n_Y\) and \(k_0\), the constant is \(18928\,(A + K + g + n_Y + k_0 + 1)^5\).

It depends only on \(A\), \(K\), \(g\), the number \(n_Y\) of certificate codes and the input stack \(k_0\).

def initC (L : Layout) (nY k0 : ℕ) : ℕ := 18928 * (L.A + L.KK + L.g + nY + k0 + 1) ^ 5

Uses 1 · Used by 8

Statement usesVariable layout of the transition clauses

Used byThe init generator at the stack cap · Time and output of the init generator for an encoding · Polynomial time bound for the init 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 for the init generator#✓fully proved

Let \(L\) be a layout with \(A\) label/state variables, \(K\) stacks and \(g > 0\) symbol codes, let \(i_c < A\) and \(k_0 < K\), and let \(Y\) be a strictly increasing list of codes with \(0 < y < g\) for every \(y \in Y\). Let \(xs\) be a list of codes below \(g\) with \(n = |xs|\), let \(T, e, f\) be natural numbers with \(f > 0\), and let \(o\) be a bit string. Start the generator for \(L, i_c, k_0, Y\) at its start label with state false, with the counters \(\mathrm{Tn}, \mathrm{Xn}, \mathrm{En}, \mathrm{Fn}\) holding \(T, n, e, f\) in unary and all other counters empty, \(o\) on the output stack, and \(xs\) reversed on the input stack. Then within \(C\,(T + n + e + f + 1)^5\) steps, where \(C = 18928\,(A + K + g + |Y| + k_0 + 1)^5\), it reaches the final label \(\mathrm{done}\), and its output stack there is the bit encoding of the layout-level init family for \(L, i_c, k_0, Y, xs\), \(m = n + e\), \(T\) and \(H = n + e + f\), followed by \(o\).

theorem init_time {L : Layout} {ic k0 : ℕ} {ycs : List ℕ} (hk0 : k0 < L.KK) (hic : ic < L.A)
    (hg : 0 < L.g) (hy : (0 :: ycs).Pairwise (· < ·)) (hyg : ∀ c ∈ ycs, c < L.g)
    (xs : List (Fin L.g)) (T e f : ℕ) (hf : 0 < f) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (IΓ CK (Fin L.g) k)),
      RunLe (iprog L ic k0 ycs)
        (initC L ycs.length k0 * (T + (xs.length + e + f) + 1) ^ 5)
        ⟨some (.pre1 .eg), false, emb (st (initF T xs.length e f) o) xs.reverse⟩
        ⟨some .done, v, S⟩ ∧
      S (.b .out) = encodeCNF (initFam L ic k0 ycs xs (xs.length + e) T (xs.length + e + f)) ++ o

Uses 28 · Used by 1

Statement usesStacks of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · 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 initial-row generator for a layout · Labels of the first precomputation part · Stacks of a counter machine with an extra input stack · Constant of the init generator's time bound · Initial counters of the init generator · The init family · The initial-row generator · Dense encoding of a CNF formula · Runs within a step budget

Proof usesNumber of variables of the transition-clause formula · Variables per time step · Uniform layout · Step bound for one loop iteration (initial-row generator) · Step bound for one clause (initial-row generator) · Time bound of the init generator · Time bound of the init generator at uniform parameters · Correctness of the init generator, with its explicit time bound · Per-literal step cost of the initial-row generator · Step bound of one phase loop (initial-row generator) · Step bound for the precomputation · Exact-length runs of a TM2 machine

Used byTime and output of the init generator for an encoding

Link to the semantic initial-row family (I4 sorted and deduplicated)

TheoremLookup in an all-positive literal list#✓fully proved

Let \(\lambda\) be a list of pairs of a natural number and a boolean in which every boolean is true. For every \(v \in \mathbb{N}\), looking up \(v\) in \(\lambda\) (the boolean of the first pair with first entry \(v\), if any) gives true if \(v\) is the first entry of some pair in \(\lambda\), and no value otherwise.

theorem lookup_pos (v : ℕ) : ∀ ls : List (ℕ × Bool), (∀ p ∈ ls, p.2 = true) →
    ls.lookup v = if v ∈ ls.map Prod.fst then some true else none

Used by 1

Used byDense clauses of positive literals depend only on their positions

TheoremDense clauses of positive literals depend only on their positions#✓fully proved

Let \(\ell\) and \(\ell'\) be lists of literals (pairs of a position and a sign) in which every sign is positive. If every natural number \(v\) is a position of \(\ell\) exactly when it is a position of \(\ell'\), then for every \(V\) the dense clause over \(V\) variables with literals \(\ell\) equals the dense clause over \(V\) variables with literals \(\ell'\): order and repetitions in the lists are irrelevant.

theorem denseClause_congr {V : ℕ} {ls ls' : List (ℕ × Bool)} (h : ∀ p ∈ ls, p.2 = true)
    (h' : ∀ p ∈ ls', p.2 = true) (hm : ∀ v, v ∈ ls.map Prod.fst ↔ v ∈ ls'.map Prod.fst) :
    denseClause V ls = denseClause V ls'

Uses 3 · Used by 1

Statement usesDense clause from a list of literals · Dense clause

Proof usesLookup in an all-positive literal list

Used byThe init family of an encoding is a layout-level init family

DefinitionSorted certificate code list#✓fully proved

Given an encoding \(E\) of a machine \(M\) and a list \(Y\) of symbols of the input stack of \(M\), this is the list of the distinct codes that \(E\) assigns to the symbols of \(Y\) on the input stack, sorted in strictly increasing order.

Besides the empty cell, these are the codes allowed in the certificate cells of the initial row (clause group I4).

noncomputable def ycs (Ys : List (M.Γ M.k₀)) : List ℕ :=
  ((Ys.map (E.enc M.k₀)).toFinset).sort (· ≤ ·)

Uses 1 · Used by 15

Statement usesEncoding data for a finite TM2 machine

Used byThe init family of an encoding is a layout-level init family · The init generator at the stack cap · Time and output of the init generator for an encoding · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · The reduction machine · Step bound of the host · The host on the real generators of a machine · The assembled generator, after the precomputation · 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

DefinitionCodes of input symbols#✓fully proved

Let \(E\) be an encoding of a finite multi-stack Turing machine \(M\), and let \(g\) be the number of symbol codes of the layout of \(E\). A symbol \(z\) of the input stack of \(M\) is sent to its symbol code under \(E\), viewed as an element of \(\{0, \dots, g - 1\}\); the code is below \(g\) because every input symbol is an effective symbol of the input stack.

def encF (z : M.Γ M.k₀) : Fin E.layout.g := ⟨E.enc M.k₀ z, E.enc_lt _ z (E.input_mem z)⟩

Uses 4 · Used by 6

Statement usesVariable layout of the transition clauses · Encoding data for a finite TM2 machine · Symbol-code bound · Clause layout of a machine encoding

Used byThe init family of an encoding is a layout-level init family · The init generator at the stack cap · Time and output of the init generator for an encoding · The assembled generator, after the precomputation · The full program on the real generators · The composed machine, raw input to formula

TheoremThe init family of an encoding is a layout-level init family#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T, H\) be natural numbers. The init family of \(E\) for \(x, Y, m, T, H\) equals the layout-level init family over the layout of \(E\) with start code the code of the pair of the main label and the initial state of \(M\), stack \(k_0\) the number of the input stack, code list the codes of the symbols of \(Y\) in increasing order without repetitions, input codes the codes of the symbols of \(x\), and the same \(m, T, H\).

The family of \(E\) lists the certificate symbols \(Y\) in their given order, possibly with repeated codes; the equality holds because order and repetitions do not change these clauses.

theorem initFamily_eq (x Ys : List (M.Γ M.k₀)) (m T H : ℕ) :
    E.initFamily x Ys m T H =
      initFam E.layout (E.lc (some M.main, M.initialState)) (E.kc M.k₀) (ycs E Ys)
        (x.map (encF E)) m T H

Uses 27 · Used by 1

Statement usesVariable layout of the transition clauses · Codes of input symbols · The init family · Sorted certificate code list · Encoding data for a finite TM2 machine · The row-0 init family of an encoding · Clause layout of a machine encoding · Dense CNF formula

Proof usesIndex of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Dense clauses of positive literals depend only on their positions · Certificate clauses of the initial row (I4) · Start-code clause of the initial row (I1) · Input clauses of the initial row (I3) · Row-0 clauses for the other stacks · Row-0 prefix clauses · Row-0 tail clauses · Empty-cell variable of the initial row · Certificate clauses of the init family · Start-code clause of the init family · Input clauses of the init family · Empty-stack clauses of the init family · Prefix clauses of the init family · Length-bound clauses of the init family · Index of the empty-cell variable of the input stack · Dense clause

Used byTime and output of the init generator for an encoding

TheoremTime and output of the init generator for an encoding#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), let \(m, T, H\) be natural numbers with \(|x| \le m < H\), and let \(o\) be a bit string. Let \(C\) be the time constant for the layout of \(E\), the number of distinct codes of \(Y\) and the number \(k_0\) of the input stack. Start the generator for \(E\) (start code: the code of the pair of the main label and the initial state; stack \(k_0\); code list: the distinct codes of \(Y\) in increasing order) at its start label with state false, with the counters \(\mathrm{Tn}, \mathrm{Xn}, \mathrm{En}, \mathrm{Fn}\) holding \(T\), \(|x|\), \(m - |x|\), \(H - m\) in unary and all other counters empty, \(o\) on the output stack, and the list of codes of \(x\), reversed, on the input stack. Then within \(C\,(T + H + 1)^5\) steps it reaches the final label \(\mathrm{done}\), and its output stack there is the bit encoding of the init family of \(E\) for \(x, Y, m, T, H\) followed by \(o\).

theorem init_gen_time (x Ys : List (M.Γ M.k₀)) (m T H : ℕ) (hx : x.length ≤ m) (hmH : m < H)
    (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (IΓ CK (Fin E.layout.g) k)),
      RunLe (iprog E.layout (E.lc (some M.main, M.initialState)) (E.kc M.k₀) (ycs E Ys))
        (initC E.layout (ycs E Ys).length (E.kc M.k₀) * (T + H + 1) ^ 5)
        ⟨some (.pre1 .eg), false,
          emb (st (initF T x.length (m - x.length) (H - m)) o) (x.map (encF E)).reverse⟩
        ⟨some .done, v, S⟩ ∧
      S (.b .out) = encodeCNF (E.initFamily x Ys m T H) ++ o

Uses 26 · Used by 1

Statement usesStacks of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · 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 initial-row generator for a layout · Labels of the first precomputation part · Stacks of a counter machine with an extra input stack · Codes of input symbols · Constant of the init generator's time bound · Initial counters of the init generator · The initial-row generator · Sorted certificate code list · Encoding data for a finite TM2 machine · The row-0 init family of an encoding · Clause layout of a machine encoding · Dense encoding of a CNF formula · Runs within a step budget

Proof usesThe init family · The init family of an encoding is a layout-level init family · Polynomial time bound for the init generator · Number of situations · Symbol-code bound · Dense CNF formula

Used byThe init generator at the stack cap

TheoremThe init generator at the stack cap#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), let \(m, T\) be natural numbers with \(|x| \le m\), let \(H = m + (T + 1)d + 1\) be the stack cap, and let \(o\) be a bit string. Let \(C\) be the time constant for the layout of \(E\), the number of distinct codes of \(Y\) and the number \(k_0\) of the input stack. Start the generator for \(E\) (start code: the code of the pair of the main label and the initial state; stack \(k_0\); code list: the distinct codes of \(Y\) in increasing order) at its start label with state false, with the counters \(\mathrm{Tn}, \mathrm{Xn}, \mathrm{En}, \mathrm{Fn}\) holding \(T\), \(|x|\), \(m - |x|\), \(H - m\) in unary and all other counters empty, \(o\) on the output stack, and the list of codes of \(x\), reversed, on the input stack. Then within \(C\,(T + H + 1)^5\) steps it reaches the final label \(\mathrm{done}\), and its output stack there is the bit encoding of the init family of \(E\) for \(x, Y, m, T, H\) followed by \(o\).

theorem init_gen_capH (x Ys : List (M.Γ M.k₀)) (m T : ℕ) (hx : x.length ≤ m) (o : List Bool) :
    ∃ (v : Bool) (S : ∀ k, List (IΓ CK (Fin E.layout.g) k)),
      RunLe (iprog E.layout (E.lc (some M.main, M.initialState)) (E.kc M.k₀) (ycs E Ys))
        (initC E.layout (ycs E Ys).length (E.kc M.k₀) *
          (T + Cslib.Complexity.CookLevin.Situation.capH m T (Cslib.Complexity.CookLevin.Situation.depth M) + 1) ^ 5)
        ⟨some (.pre1 .eg), false, emb (st (initF T x.length (m - x.length)
          (Cslib.Complexity.CookLevin.Situation.capH m T (Cslib.Complexity.CookLevin.Situation.depth M) - m)) o) (x.map (encF E)).reverse⟩
        ⟨some .done, v, S⟩ ∧
      S (.b .out) = encodeCNF (E.initFamily x Ys m T (Cslib.Complexity.CookLevin.Situation.capH m T (Cslib.Complexity.CookLevin.Situation.depth M))) ++ o

Uses 23 · Used by 1

Statement usesStacks of a counter machine · Stacks holding given counter values · Variable layout of the transition clauses · 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 initial-row generator for a layout · Labels of the first precomputation part · Stacks of a counter machine with an extra input stack · Codes of input symbols · Constant of the init generator's time bound · Initial counters of the init generator · The initial-row generator · Sorted certificate code list · Encoding data for a finite TM2 machine · The row-0 init family of an encoding · Clause layout of a machine encoding · Stack cap · Window depth of a machine · Dense encoding of a CNF formula · Runs within a step budget

Proof usesTime and output of the init generator for an encoding

Used byThe assembled generator, after the precomputation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.