Top of a stack as read from the windows to Next label/state code of a situation

DefinitionTop of a stack as read from the windows#✓fully proved

Let \(W\) assign to each stack \(k\) a window, a list of entries that are symbols of \(k\) or the empty cell \(\bot\); let \(P\) assign to each stack \(k\) a list of symbols of \(k\); and let \(c\) assign a natural number to each stack. The top of stack \(k\) is the first element of \(P(k)\) when \(P(k)\) is nonempty. Otherwise it is the entry of \(W(k)\) at position \(c(k)\), counting from \(0\), or \(\bot\) when \(W(k)\) has fewer than \(c(k) + 1\) entries.

Here \(P(k)\) lists the symbols pushed in this step and still on top, and \(c(k)\) counts the original symbols already consumed.

def readTop (W : ∀ k, List (Option (Γ k))) (P : ∀ k, List (Γ k)) (c : K → ℕ) (k : K) :
    Option (Γ k) :=
  match P k with
  | x :: _ => some x
  | [] => (W k).getD (c k) none

Used by 5

Used bySymbolic effect of a statement tree · The symbolic effect grows by at most the number of stack operations · Pushed symbols come from the start or from push nodes · The symbolic effect of a statement agrees with the real step · Reading the top through the windows

DefinitionSymbolic effect of a statement tree#✓fully proved

Let \(W\) assign to each stack \(k\) a window \(W_k\), a list of cells each holding a symbol or \(\bot\). The window top of stack \(k\) for pushed lists \(P\) and consumption counts \(c\) is the head of \(P_k\) if \(P_k\) is nonempty, and otherwise the entry of \(W_k\) at position \(c_k\) (counting from \(0\)), or \(\bot\) if there is none. The effect of a statement tree \(q\) from a state \(v\), pushed lists \(P\) and consumption counts \(c\) is a label (or none), a state, pushed lists and consumption counts, defined by recursion on \(q\): a push onto stack \(k\) prepends the symbol computed from \(v\) to \(P_k\) and continues; a peek on stack \(k\) replaces \(v\) by the state computed from \(v\) and the window top of \(k\) and continues; a pop on stack \(k\) does the same, also removes the head of \(P_k\) (if any), and increases \(c_k\) by one if \(P_k\) was empty; a load replaces \(v\) by the state computed from \(v\) and continues; a branch continues with the subtree selected by \(v\); a goto returns the label computed from \(v\), and a halt returns no label, each together with the current \(v\), \(P\) and \(c\).

Thus \(P_k\) holds the symbols pushed in this step and still on top, and \(c_k\) counts the original symbols consumed, a push followed by a pop cancelling.

def eff (W : ∀ k, List (Option (Γ k))) :
    TM2.Stmt Γ Λ σ → σ → (∀ k, List (Γ k)) → (K → ℕ) →
      Option Λ × σ × (∀ k, List (Γ k)) × (K → ℕ)
  | .push k f q, v, P, c => eff W q v (update P k (f v :: P k)) c
  | .peek k f q, v, P, c => eff W q (f v (readTop W P c k)) P c
  | .pop k f q, v, P, c =>
      eff W q (f v (readTop W P c k)) (update P k (P k).tail)
        (if (P k).isEmpty then update c k (c k + 1) else c)
  | .load a q, v, P, c => eff W q (a v) P c
  | .branch p q₁ q₂, v, P, c => cond (p v) (eff W q₁ v P c) (eff W q₂ v P c)
  | .goto f, v, P, c => (some (f v), v, P, c)
  | .halt, v, P, c => (none, v, P, c)

def readTop (W : ∀ k, List (Option (Γ k))) (P : ∀ k, List (Γ k)) (c : K → ℕ) (k : K) :
    Option (Γ k) :=
  match P k with
  | x :: _ => some x
  | [] => (W k).getD (c k) none

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:70

Uses 1 · Used by 14

Statement usesTop of a stack as read from the windows

Used byThe symbolic effect grows by at most the number of stack operations · Pushed symbols come from the start or from push nodes · The situation step · Halted situations stay fixed · Symbols left pushed by a situation are effective · The cell-shift tables of a machine are well formed · The symbolic effect of a statement agrees with the real step · The idle-extended step preserves good configurations · The idle-extended step is the situation step applied to the stacks · The table-driven step · Stack heights grow by at most the window depth per step · Overflow cells of the next row hold the table value · Pushed-fill forcing on a real run · The run assignment satisfies the cell-shift family

DefinitionStack operations on a path of a statement tree#✓fully proved

For a statement tree \(q\) of a multi-stack Turing machine, \(\operatorname{ops}(q)\) is the largest number of push, peek and pop nodes on a path from the root of \(q\) to a leaf. Load and branch nodes do not count, and goto and halt leaves contribute \(0\).

def ops : TM2.Stmt Γ Λ σ → ℕ
  | .push _ _ q => ops q + 1
  | .peek _ _ q => ops q + 1
  | .pop _ _ q => ops q + 1
  | .load _ q => ops q
  | .branch _ q₁ q₂ => max (ops q₁) (ops q₂)
  | .goto _ => 0
  | .halt => 0

Used by 10

Used byWindow depth of a machine · The symbolic effect grows by at most the number of stack operations · The cell-shift tables of a machine are well formed · The symbolic effect of a statement agrees with the real step · The idle-extended step is the situation step applied to the stacks · The table-driven step · Stack heights grow by at most the window depth per step · Overflow cells of the next row hold the table value · Pushed-fill forcing on a real run · The run assignment satisfies the cell-shift family

DefinitionSymbols a statement tree can push#✓fully proved

Let \(q\) be a statement tree of a multi-stack Turing machine with state type \(\sigma\), let \(k\) be a stack and \(x\) a symbol of the alphabet of \(k\). Then \(x\) can be pushed onto \(k\) by \(q\) when \(q\) contains a push node onto stack \(k\) with symbol function \(f\) and some state \(v \in \sigma\) satisfies \(x = f(v)\). Every push node of \(q\) counts, whichever branches are taken.

def PushSym (k : K) : TM2.Stmt Γ Λ σ → Γ k → Prop
  | .push k' f q, x => (∃ (h : k' = k) (v : σ), x = cast (congrArg Γ h) (f v)) ∨ PushSym k q x
  | .peek _ _ q, x => PushSym k q x
  | .pop _ _ q, x => PushSym k q x
  | .load _ q, x => PushSym k q x
  | .branch _ q₁ q₂, x => PushSym k q₁ x ∨ PushSym k q₂ x
  | .goto _, _ => False
  | .halt, _ => False

Used by 6

Used byTableau encoding with a chosen accept symbol · Pushed symbols come from the start or from push nodes · Encoding data for a finite TM2 machine · The classical encoding record of a finite multi-stack machine · Symbols left pushed by a situation are effective · The idle-extended step preserves good configurations

TheoremThe symbolic effect grows by at most the number of stack operations#✓fully proved

Let \(q\) be a statement tree, let \(W\) assign to each stack a window (a list of cells, each a symbol or \(\bot\)), and let \(n(q)\) be the largest number of push, peek and pop nodes on a root-to-leaf path of \(q\). For every state \(v\), pushed lists \(P\) and consumption counts \(c\), the pushed lists \(P'\) and consumption counts \(c'\) of the symbolic effect of \(q\) on \(W\) from \(v\), \(P\), \(c\) satisfy \(|P'_k| \le |P_k| + n(q)\) and \(c'_k \le c_k + n(q)\) for every stack \(k\).

theorem eff_bound (W : ∀ k, List (Option (Γ k))) (q : TM2.Stmt Γ Λ σ) :
    ∀ (v : σ) (P : ∀ k, List (Γ k)) (c : K → ℕ) (k : K),
      ((eff W q v P c).2.2.1 k).length ≤ (P k).length + ops q ∧
        (eff W q v P c).2.2.2 k ≤ c k + ops q

def eff (W : ∀ k, List (Option (Γ k))) :
    TM2.Stmt Γ Λ σ → σ → (∀ k, List (Γ k)) → (K → ℕ) →
      Option Λ × σ × (∀ k, List (Γ k)) × (K → ℕ)
  | .push k f q, v, P, c => eff W q v (update P k (f v :: P k)) c
  | .peek k f q, v, P, c => eff W q (f v (readTop W P c k)) P c
  | .pop k f q, v, P, c =>
      eff W q (f v (readTop W P c k)) (update P k (P k).tail)
        (if (P k).isEmpty then update c k (c k + 1) else c)
  | .load a q, v, P, c => eff W q (a v) P c
  | .branch p q₁ q₂, v, P, c => cond (p v) (eff W q₁ v P c) (eff W q₂ v P c)
  | .goto f, v, P, c => (some (f v), v, P, c)
  | .halt, v, P, c => (none, v, P, c)

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:78

def ops : TM2.Stmt Γ Λ σ → ℕ
  | .push _ _ q => ops q + 1
  | .peek _ _ q => ops q + 1
  | .pop _ _ q => ops q + 1
  | .load _ q => ops q
  | .branch _ q₁ q₂ => max (ops q₁) (ops q₂)
  | .goto _ => 0
  | .halt => 0

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:92

Uses 3 · Used by 6

Statement usesSymbolic effect of a statement tree · Stack operations on a path of a statement tree

Proof usesTop of a stack as read from the windows

Used byThe cell-shift tables of a machine are well formed · The table-driven step · Stack heights grow by at most the window depth per step · Overflow cells of the next row hold the table value · Pushed-fill forcing on a real run · The run assignment satisfies the cell-shift family

TheoremPushed symbols come from the start or from push nodes#✓fully proved

Let \(q\) be a statement tree, let \(W\) assign to each stack a window, and for each stack \(k\) let \(Q_k\) be a property of symbols of stack \(k\) such that every symbol that some push node of \(q\) can push onto stack \(k\), for some state, satisfies \(Q_k\). Then for every state \(v\), pushed lists \(P\) and consumption counts \(c\) such that every symbol of \(P_k\) satisfies \(Q_k\) for every stack \(k\), every symbol of the pushed list on stack \(k\) produced by the symbolic effect of \(q\) on \(W\) from \(v\), \(P\), \(c\) satisfies \(Q_k\), for every stack \(k\).

theorem eff_pushed (W : ∀ k, List (Option (Γ k))) (Q : ∀ k, Γ k → Prop) (q : TM2.Stmt Γ Λ σ)
    (hq : ∀ k x, PushSym k q x → Q k x) :
    ∀ (v : σ) (P : ∀ k, List (Γ k)) (c : K → ℕ), (∀ k, ∀ x ∈ P k, Q k x) →
      ∀ k, ∀ x ∈ (eff W q v P c).2.2.1 k, Q k x

def PushSym (k : K) : TM2.Stmt Γ Λ σ → Γ k → Prop
  | .push k' f q, x => (∃ (h : k' = k) (v : σ), x = cast (congrArg Γ h) (f v)) ∨ PushSym k q x
  | .peek _ _ q, x => PushSym k q x
  | .pop _ _ q, x => PushSym k q x
  | .load _ q, x => PushSym k q x
  | .branch _ q₁ q₂, x => PushSym k q₁ x ∨ PushSym k q₂ x
  | .goto _, _ => False
  | .halt, _ => False

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:102

def eff (W : ∀ k, List (Option (Γ k))) :
    TM2.Stmt Γ Λ σ → σ → (∀ k, List (Γ k)) → (K → ℕ) →
      Option Λ × σ × (∀ k, List (Γ k)) × (K → ℕ)
  | .push k f q, v, P, c => eff W q v (update P k (f v :: P k)) c
  | .peek k f q, v, P, c => eff W q (f v (readTop W P c k)) P c
  | .pop k f q, v, P, c =>
      eff W q (f v (readTop W P c k)) (update P k (P k).tail)
        (if (P k).isEmpty then update c k (c k + 1) else c)
  | .load a q, v, P, c => eff W q (a v) P c
  | .branch p q₁ q₂, v, P, c => cond (p v) (eff W q₁ v P c) (eff W q₂ v P c)
  | .goto f, v, P, c => (some (f v), v, P, c)
  | .halt, v, P, c => (none, v, P, c)

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:78

Uses 3 · Used by 2

Statement usesSymbols a statement tree can push · Symbolic effect of a statement tree

Proof usesTop of a stack as read from the windows

Used bySymbols left pushed by a situation are effective · The idle-extended step preserves good configurations

StructureEncoding data for a finite TM2 machine#✓fully proved

An encoding of a finite TM2 machine \(M\) consists of a number \(K\), a map \(\kappa\) from the stacks of \(M\) to the naturals below \(K\) and a map \(\kappa'\) from naturals to stacks with \(\kappa'(\kappa(k)) = k\) for every stack \(k\) and \(\kappa(\kappa'(n)) = n\) for every \(n < K\); a number \(A_0\), a map \(\lambda\) from pairs (label or halted, state) to the naturals below \(A_0\) and a map \(\lambda'\) back with \(\lambda'(\lambda(x)) = x\) for every pair \(x\) and \(\lambda(\lambda'(a)) = a\) for every \(a < A_0\); and for each stack \(k\) a size \(s_k\), effective symbols \(d_k(i)\) for \(i < s_k\), and a symbol code map \(e_k\) on the alphabet of stack \(k\) with \(e_k(d_k(i)) = i + 1\). It is required that every symbol that a push node of the statement tree of some label can push onto stack \(k\), for some state, is an effective symbol of stack \(k\), and that every symbol of the input stack's alphabet is an effective symbol of the input stack.

Symbol code \(0\) stands for \(\bot\), the empty cell.

Cslib.Complexity.CookLevin.Situation.Enc · 28 lines

structure Enc (M : FinTM2) where
  /-- Number of stacks. -/
  KK : ℕ
  /-- Stack numbering. -/
  kc : M.K → ℕ
  /-- Inverse of the stack numbering. -/
  kd : ℕ → M.K
  kc_lt : ∀ k, kc k < KK
  kd_kc : ∀ k, kd (kc k) = k
  kc_kd : ∀ n < KK, kc (kd n) = n
  /-- Number of (label, state) codes. -/
  A0 : ℕ
  /-- (Label, state) numbering. -/
  lc : Option M.Λ × M.σ → ℕ
  /-- Inverse of the (label, state) numbering. -/
  ld : ℕ → Option M.Λ × M.σ
  lc_lt : ∀ x, lc x < A0
  ld_lc : ∀ x, ld (lc x) = x
  lc_ld : ∀ c < A0, lc (ld c) = c
  /-- Size of the effective alphabet of each stack. -/
  sz : M.K → ℕ
  /-- The effective symbols of each stack. -/
  dec : ∀ k, Fin (sz k) → M.Γ k
  /-- Symbol codes (`1 + index`; `0` is the empty cell). -/
  enc : ∀ k, M.Γ k → ℕ
  enc_dec : ∀ k i, enc k (dec k i) = i + 1
  push_mem : ∀ l k x, PushSym k (M.m l) x → ∃ i, dec k i = x
  input_mem : ∀ x : M.Γ M.k₀, ∃ i, dec M.k₀ i = x

  kc : M.K → ℕ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:205

  KK : ℕ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:203

  kd : ℕ → M.K

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:207

  lc : Option M.Λ × M.σ → ℕ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:214

  A0 : ℕ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:212

  ld : ℕ → Option M.Λ × M.σ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:216

  sz : M.K → ℕ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:221

  enc : ∀ k, M.Γ k → ℕ

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:225

  dec : ∀ k, Fin (sz k) → M.Γ k

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:223

def PushSym (k : K) : TM2.Stmt Γ Λ σ → Γ k → Prop
  | .push k' f q, x => (∃ (h : k' = k) (v : σ), x = cast (congrArg Γ h) (f v)) ∨ PushSym k q x
  | .peek _ _ q, x => PushSym k q x
  | .pop _ _ q, x => PushSym k q x
  | .load _ q, x => PushSym k q x
  | .branch _ q₁ q₂, x => PushSym k q₁ x ∨ PushSym k q₂ x
  | .goto _, _ => False
  | .halt, _ => False

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:102

Uses 1 · Used by 136

Statement usesSymbols a statement tree can push

Used byTableau encoding with a chosen accept symbol · The chosen accept symbol is encodable · Tableau encoding of the verifier · The concrete accept family is a layout-level accept family · Time bound of the accept generator for a concrete machine · Codes of input symbols · The 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 · Sorted certificate code list · The Cook–Levin reduction function · Step bound of the composed machine · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · The reduction machine · The formula emitted on a raw input · Decoding a symbol code · Symbol-code bound · Number of window combinations · Label/state code of a situation · Clause layout of a machine encoding · Number of situations · Next label/state code of a situation · Effect of a situation · Position of a situation's variable · Window symbol code of a situation · Decoded windows of a situation · Consumption table of a situation · The symbol-code bound is positive · Halted situations stay fixed · Mixed-radix index of a situation · The classical encoding record of a finite multi-stack machine · Push-count table of a situation · Pushed-symbol table of a situation · Pushed codes are valid symbol codes · Symbols left pushed by a situation are effective · Time bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · Situation surjectivity · Time bound of the transition-clause generator on the tables of a machine · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · Cell code of a configuration · Label-and-state code of a configuration · Good configurations · The idle-extended step preserves good configurations · Situation index of a configuration · The situation index matches the code and windows · The table-driven row update · Reads of the in-range shift stay in the row · The table-driven step · The table-driven step along a run · C1c (cell arrays of good configurations are well-formed rows) · Cell block of a row equal to an array · Cell literals of an array hold in a row · C1 decoder (decoding a row) · C1e (the row decoder reads only the window) · C1a (decoding recovers a good configuration) · C1d (decoded configurations are good) · C2' (decoding the table-driven row gives the next configuration) · C1b (decoding a well-formed row loses nothing) · Good configurations are determined by their row (C1f) · Well-formed rows of cells · Positive core of the shift step (L2⁺) · Exact shift step (L2) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · The code of a configuration holds in a row · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · Certificate clauses of the init family · Start-code clause of the init family · The row-0 init family of an encoding · Input clauses of the init family · Init obligation, input pinned · The init family discharges the init obligation · Empty-stack clauses of the init family · Prefix clauses of the init family · Init semantics · Length-bound clauses of the init family · One-step invariant at the stack cap · One-step invariant · Row-0 obligation · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Index of the empty-cell variable of the input stack · Accept-cell clauses · Accept-cell clauses pin the top output symbol · Accept-code clauses · Accept-code clauses pin the (label, state) code · The accept family · The all-true assignment violates the accept family · Satisfying assignments yield accepting runs · Accepting code · The init family is faithful with positive literals · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The assignment of the real run's literals · The real run's literals · Situation variables lie in the label/state block · Faithful clauses with a literal agreeing with the real run are satisfied · Unit clauses on run literals are satisfied · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · Step bound of the host · The host on the real generators of a machine · The assembled generator, after the precomputation · Step bound of the full machine · 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 · Every clause of the Cook–Levin formula has one slot per variable

DefinitionWindow depth of a machine#✓fully proved

For a finite TM2 machine \(M\), the window depth is the maximum, over all labels \(l\) of \(M\), of the largest number of push, peek and pop nodes on a root-to-leaf path of the statement tree of \(l\).

def depth (M : FinTM2) : ℕ :=
  letI := M.ΛFin
  Finset.univ.sup fun l => ops (M.m l)

def ops : TM2.Stmt Γ Λ σ → ℕ
  | .push _ _ q => ops q + 1
  | .peek _ _ q => ops q + 1
  | .pop _ _ q => ops q + 1
  | .load _ q => ops q
  | .branch _ q₁ q₂ => max (ops q₁) (ops q₂)
  | .goto _ => 0
  | .halt => 0

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:92

Uses 1 · Used by 70

Statement usesStack operations on a path of a statement tree

Used byThe init generator at the stack cap · Step bound of the composed machine · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · Number of window combinations · Clause layout of a machine encoding · Window symbol code of a situation · Decoded windows of a situation · Mixed-radix index of a situation · Time bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · Situation surjectivity · Time bound of the transition-clause generator on the tables of a machine · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · Situation index of a configuration · The situation index matches the code and windows · The idle-extended step is the situation step applied to the stacks · The table-driven step · The table-driven step along a run · Windows of a configuration · C2' (decoding the table-driven row gives the next configuration) · Positive core of the shift step (L2⁺) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Stack heights grow by at most the window depth per step · Stack heights are at most the cap minus the window depth · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · Stack heights along a run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · Init obligation, input pinned · The init family discharges the init obligation · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · Step bound of the host · The assembled generator, after the precomputation · Step bound of the full machine · The full program on the real generators · The composed machine, raw input to formula · Polynomial time bound of the composed machine · Every clause of the Cook–Levin formula has one slot per variable · Every NP problem reduces to binary-index CNF-SAT

DefinitionThe situation step#✓fully proved

Let \(M\) be a finite multi-stack Turing machine, let \(l\) be either a label of \(M\) or \(\mathrm{none}\) (the halted label), let \(v\) be a state of \(M\), and let \(W\) assign to each stack \(k\) a window, a list of entries that are symbols of \(k\) or the empty cell. If \(l = \mathrm{none}\), the step returns the label \(\mathrm{none}\), the state \(v\), no pushed symbols on any stack and no consumed symbols on any stack. If \(l\) is a label, the step is the effect, read from the windows \(W\), of the statement tree of \(l\) started in state \(v\) with nothing pushed and nothing consumed.

def sitStep (M : FinTM2) (l : Option M.Λ) (v : M.σ) (W : ∀ k, List (Option (M.Γ k))) :
    Option M.Λ × M.σ × (∀ k, List (M.Γ k)) × (M.K → ℕ) :=
  match l with
  | none => (none, v, fun _ => [], fun _ => 0)
  | some l => eff W (M.m l) v (fun _ => []) (fun _ => 0)

def eff (W : ∀ k, List (Option (Γ k))) :
    TM2.Stmt Γ Λ σ → σ → (∀ k, List (Γ k)) → (K → ℕ) →
      Option Λ × σ × (∀ k, List (Γ k)) × (K → ℕ)
  | .push k f q, v, P, c => eff W q v (update P k (f v :: P k)) c
  | .peek k f q, v, P, c => eff W q (f v (readTop W P c k)) P c
  | .pop k f q, v, P, c =>
      eff W q (f v (readTop W P c k)) (update P k (P k).tail)
        (if (P k).isEmpty then update c k (c k + 1) else c)
  | .load a q, v, P, c => eff W q (a v) P c
  | .branch p q₁ q₂, v, P, c => cond (p v) (eff W q₁ v P c) (eff W q₂ v P c)
  | .goto f, v, P, c => (some (f v), v, P, c)
  | .halt, v, P, c => (none, v, P, c)

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:78

Uses 1 · Used by 10

Statement usesSymbolic effect of a statement tree

Used byEffect of a situation · Halted situations stay fixed · The cell-shift tables of a machine are well formed · The idle-extended step preserves good configurations · The idle-extended step is the situation step applied to the stacks · The table-driven step · Stack heights grow by at most the window depth per step · Overflow cells of the next row hold the table value · Pushed-fill forcing on a real run · The run assignment satisfies the cell-shift family

DefinitionSymbol-code bound#✓fully proved

For an encoding \(E\) of a finite TM2 machine \(M\), the symbol-code bound is \(g = 1 + \max_k s_k\), where the maximum runs over all stacks \(k\) of \(M\) and \(s_k\) is the size of the effective alphabet of stack \(k\).

Effective symbols of stack \(k\) have codes \(1, \dots, s_k\), all below \(g\); code \(0\) is \(\bot\).

def g : ℕ :=
  letI := M.kFin
  1 + Finset.univ.sup E.sz

Uses 1 · Used by 27

Statement usesEncoding data for a finite TM2 machine

Used byCodes of input symbols · Time and output of the init generator for an encoding · Number of window combinations · Clause layout of a machine encoding · Window symbol code of a situation · The symbol-code bound is positive · Mixed-radix index of a situation · Situation surjectivity · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · Situation index of a configuration · The situation index matches the code and windows · Cell block of a row equal to an array · Positive core of the shift step (L2⁺) · Exact shift step (L2) · Exact shift step on a real run (L3) · Accept-cell clauses · Accept-cell clauses pin the top output symbol · Satisfying assignments yield accepting runs · The init family is faithful with positive literals · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the cell-shift family · Situation injectivity · Every clause of the Cook–Levin formula has one slot per variable

DefinitionNumber of window combinations#✓fully proved

For an encoding \(E\) of a finite TM2 machine \(M\) with \(K\) numbered stacks and symbol-code bound \(g\), the number of window combinations is \(G = g^{K d}\), where \(d\) is the window depth of \(M\).

def G : ℕ := E.g ^ (E.KK * depth M)

Uses 3 · Used by 8

Statement usesEncoding data for a finite TM2 machine · Symbol-code bound · Window depth of a machine

Used byLabel/state code of a situation · Number of situations · Halted situations stay fixed · Mixed-radix index of a situation · The situation-definition tables of a machine are well formed · The transition tables of a machine are well formed · Transition families with a run-literal head are satisfied by the run · Situation injectivity

DefinitionNumber of situations#✓fully proved

For an encoding \(E\) of a finite multi-stack Turing machine \(M\), the number of situations is \(N = A_0 \cdot G\), where \(A_0\) is the number of (label, state) codes of \(E\) and \(G\) is the number of window combinations.

def N : ℕ := E.A0 * E.G

Uses 2 · Used by 64

Statement usesEncoding data for a finite TM2 machine · Number of window combinations

Used byTime bound of the accept generator for a concrete machine · 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 · Clause layout of a machine encoding · Mixed-radix index of a situation · Time bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · Situation surjectivity · Time bound of the transition-clause generator on the tables of a machine · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · The situation index matches the code and windows · The table-driven step · The table-driven step along a run · Positive core of the shift step (L2⁺) · Exact shift step (L2) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · The all-true assignment violates the accept family · Satisfying assignments yield accepting runs · The init family is faithful with positive literals · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Situation variables lie in the label/state block · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · 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 · Every clause of the Cook–Levin formula has one slot per variable

DefinitionClause layout of a machine encoding#✓fully proved

For an encoding \(E\) of a finite TM2 machine \(M\), the layout of the transition clauses has label/state block size \(A = A_0 + N\), where \(A_0\) is the number of label/state codes and \(N = A_0 G\) is the number of situations (\(G\) the number of window combinations), together with the number \(K\) of numbered stacks, the symbol-code bound \(g\) and the window depth \(d\) of \(M\). The block is a one-hot part on \([0, A_0)\) followed by one variable per situation.

def layout : Family.Layout := ⟨E.A0 + E.N, E.KK, E.g, depth M⟩

structure Layout where
  /-- Size of the label/state block of a row. -/
  A : ℕ
  /-- Number of stacks. -/
  KK : ℕ
  /-- Number of symbol codes (code `0` is the empty cell). -/
  g : ℕ
  /-- Window depth. -/
  d : ℕ

CSLibExt/Computability/Complexity/CookLevin/Family.lean:78

def depth (M : FinTM2) : ℕ :=
  letI := M.ΛFin
  Finset.univ.sup fun l => ops (M.m l)

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231

Uses 5 · Used by 82

Statement usesVariable layout of the transition clauses · Encoding data for a finite TM2 machine · Number of situations · Symbol-code bound · Window depth of a machine

Used byThe concrete accept family is a layout-level accept family · Time bound of the accept generator for a concrete machine · Codes of input symbols · The 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 · Time bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · Time bound of the transition-clause generator on the tables of a machine · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · Cell block of a row equal to an array · Cell literals of an array hold in a row · Positive core of the shift step (L2⁺) · Exact shift step (L2) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · The code of a configuration holds in a row · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · 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 · Init semantics · Length-bound clauses of the init family · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Index of the empty-cell variable of the input stack · Accept-cell clauses · Accept-cell clauses pin the top output symbol · Accept-code clauses · Accept-code clauses pin the (label, state) code · The all-true assignment violates the accept family · Satisfying assignments yield accepting runs · The init family is faithful with positive literals · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The assignment of the real run's literals · The real run's literals · Situation variables lie in the label/state block · Faithful clauses with a literal agreeing with the real run are satisfied · Unit clauses on run literals are satisfied · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · 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 · Every clause of the Cook–Levin formula has one slot per variable · Every NP problem reduces to binary-index CNF-SAT

DefinitionLabel/state code of a situation#✓fully proved

For an encoding \(E\) of a finite TM2 machine with \(A_0\) label/state codes and \(G\) window combinations, the label/state code of a situation \(i \in \mathbb{N}\) is \(\lfloor i / G \rfloor \bmod A_0\), the top digit of \(i\) in the mixed radix whose lower digits are the window symbol codes.

def la (i : ℕ) : ℕ := i / E.G % E.A0

Uses 2 · Used by 49

Statement usesEncoding data for a finite TM2 machine · Number of window combinations

Used byEffect of a situation · Halted situations stay fixed · Mixed-radix index of a situation · Symbols left pushed by a situation are effective · Time bound of the situation-definition generator on the tables of a machine · Situation surjectivity · Time bound of the transition-clause generator on the tables of a machine · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · The situation index matches the code and windows · The table-driven step · The table-driven step along a run · Positive core of the shift step (L2⁺) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · The host on the real generators of a machine · The assembled generator, after the precomputation · Every clause of the Cook–Levin formula has one slot per variable

DefinitionWindow symbol code of a situation#✓fully proved

Let \(E\) be an encoding of a finite multi-stack Turing machine \(M\), let \(s_\kappa\) be the size of the effective alphabet of stack \(\kappa\) in \(E\), let \(g = 1 + \max_\kappa s_\kappa\) (so the empty-cell code \(0\) and every effective symbol code are below \(g\)), and let \(d\) be the window depth of \(M\). For natural numbers \(i\), \(k\) and \(j\), the window symbol code of situation \(i\) on stack number \(k\) at depth \(j\) is the base-\(g\) digit of \(i\) at position \(kd + j\), namely \(\lfloor i / g^{kd + j} \rfloor \bmod g\).

def wa (i k j : ℕ) : ℕ := i / E.g ^ (k * depth M + j) % E.g

Uses 3 · Used by 46

Statement usesEncoding data for a finite TM2 machine · Symbol-code bound · Window depth of a machine

Used byDecoded windows of a situation · Mixed-radix index of a situation · Time bound of the situation-definition generator on the tables of a machine · Situation surjectivity · Time bound of the transition-clause generator on the tables of a machine · The situation-definition tables of a machine are well formed · The transition tables of a machine are well formed · The situation index matches the code and windows · The table-driven step · The table-driven step along a run · Positive core of the shift step (L2⁺) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · The host on the real generators of a machine · The assembled generator, after the precomputation · Every clause of the Cook–Levin formula has one slot per variable

DefinitionPosition of a situation's variable#✓fully proved

For an encoding \(E\) of a finite multi-stack Turing machine \(M\) with \(A_0\) (label, state) codes and a natural number \(i\), the variable of situation \(i\) sits at position \(A_0 + i\) of the label/state block of a row.

def sa (i : ℕ) : ℕ := E.A0 + i

Uses 1 · Used by 41

Statement usesEncoding data for a finite TM2 machine

Used byTime bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · Positive core of the shift step (L2⁺) · Exact shift step (L2) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Cell literals propagate one step along the real run · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The real run's literals · Situation variables lie in the label/state block · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · The host on the real generators of a machine · The assembled generator, after the precomputation · Every clause of the Cook–Levin formula has one slot per variable

DefinitionDecoding a symbol code#✓fully proved

For an encoding \(E\) of a finite TM2 machine \(M\), a stack \(k\) and a natural number \(c\), the decoded symbol is the effective symbol of stack \(k\) with index \(c - 1\) when \(1 \le c\) and \(c - 1 < s_k\), where \(s_k\) is the size of the effective alphabet of stack \(k\); otherwise, in particular for \(c = 0\), it is \(\bot\) (no symbol).

def decO (k : M.K) (c : ℕ) : Option (M.Γ k) :=
  if h : 1 ≤ c ∧ c - 1 < E.sz k then some (E.dec k ⟨c - 1, h.2⟩) else none

Uses 1 · Used by 10

Statement usesEncoding data for a finite TM2 machine

Used byDecoded windows of a situation · Pushed codes are valid symbol codes · The cell-shift tables of a machine are well formed · The table-driven step · C1 decoder (decoding a row) · C1e (the row decoder reads only the window) · C1a (decoding recovers a good configuration) · C1d (decoded configurations are good) · C1b (decoding a well-formed row loses nothing) · The run assignment satisfies the cell-shift family

DefinitionDecoded windows of a situation#✓fully proved

Let \(E\) be an encoding of a finite multi-stack Turing machine \(M\) with window depth \(d\), and let \(i\) be a natural number. The window of situation \(i\) on stack \(k\) is the list of length \(d\) whose entry at position \(j < d\) decodes the window symbol code \(c\) of situation \(i\) on the stack number of \(k\) at depth \(j\). A code with \(1 \le c \le s_k\), where \(s_k\) is the size of the effective alphabet of \(k\), decodes to the effective symbol of \(k\) with index \(c - 1\); every other code decodes to the empty cell \(\bot\).

def win (i : ℕ) : ∀ k, List (Option (M.Γ k)) := fun k =>
  (List.range (depth M)).map fun j => E.decO k (E.wa i (E.kc k) j)

Uses 4 · Used by 8

Statement usesEncoding data for a finite TM2 machine · Decoding a symbol code · Window symbol code of a situation · Window depth of a machine

Used byEffect of a situation · Halted situations stay fixed · Symbols left pushed by a situation are effective · The cell-shift tables of a machine are well formed · The table-driven step · Overflow cells of the next row hold the table value · Pushed-fill forcing on a real run · The run assignment satisfies the cell-shift family

DefinitionEffect of a situation#✓fully proved

Let \(E\) be an encoding of a finite multi-stack Turing machine \(M\) and \(i\) a natural number. Let \((l, v)\), an optional label and a state, be the result of decoding the label/state code of situation \(i\) with the inverse (label, state) numbering of \(E\), and let \(W\) be the decoded windows of situation \(i\). The effect of situation \(i\) is the situation step of \(M\) from \(l\), \(v\) and \(W\): a new optional label, a new state, the symbols left pushed on each stack, and the number of original symbols consumed from each stack.

def res (i : ℕ) : Option M.Λ × M.σ × (∀ k, List (M.Γ k)) × (M.K → ℕ) :=
  sitStep M (E.ld (E.la i)).1 (E.ld (E.la i)).2 (E.win i)

def sitStep (M : FinTM2) (l : Option M.Λ) (v : M.σ) (W : ∀ k, List (Option (M.Γ k))) :
    Option M.Λ × M.σ × (∀ k, List (M.Γ k)) × (M.K → ℕ) :=
  match l with
  | none => (none, v, fun _ => [], fun _ => 0)
  | some l => eff W (M.m l) v (fun _ => []) (fun _ => 0)

CSLibExt/Computability/Complexity/CookLevin/Situation.lean:240

Uses 4 · Used by 13

Statement usesEncoding data for a finite TM2 machine · Label/state code of a situation · Decoded windows of a situation · The situation step

Used byNext label/state code of a situation · Consumption table of a situation · Halted situations stay fixed · Push-count table of a situation · Pushed-symbol table of a situation · Pushed codes are valid symbol codes · Symbols left pushed by a situation are effective · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · The table-driven step · Overflow cells of the next row hold the table value · Pushed-fill forcing on a real run · The run assignment satisfies the cell-shift family

DefinitionNext label/state code of a situation#✓fully proved

For an encoding \(E\) of a finite multi-stack Turing machine \(M\) and a natural number \(i\), the next label/state code of situation \(i\) is the code, in the (label, state) numbering of \(E\), of the pair formed by the label and the state that the effect of situation \(i\) produces.

def na (i : ℕ) : ℕ := E.lc ((E.res i).1, (E.res i).2.1)

Uses 2 · Used by 30

Statement usesEncoding data for a finite TM2 machine · Effect of a situation

Used byHalted situations stay fixed · Time bound of the transition-clause generator on the tables of a machine · The transition tables of a machine are well formed · The table-driven step · The table-driven step along a run · C2' (decoding the table-driven row gives the next configuration) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row on a real run · Pushed-fill forcing on a real run · Update forcing (positive) · Update forcing, real run · One-step invariant at the stack cap · One-step invariant · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the five clause families · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · The host on the real generators of a machine · The assembled generator, after the precomputation · Every clause of the Cook–Levin formula has one slot per variable

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.