Correctness of the Cook–Levin tableau

The tableau formula of S steps of a machine M (tableau) is satisfiable, with the fixed input tapes holding their strings, iff M accepts some completion of the free input tapes within S steps (planning/succinct-cook-levin.md, S1; answer_reduction.tex lem:correct-tableau). Acceptance is AcceptsIn: halted at time S with output string exactly [acc].

• Completeness (tableau_sat_of_acceptsIn): the assignment of an accepting run (runAssign) satisfies every clause; the window clauses because the windows of a run are locally consistent (locallyConsistent_localCfgOf) and the check circuit computes local consistency, its specification being the hypothesis hchk.
• Soundness (acceptsIn_of_tableau_sat): a satisfying assignment determines the free input strings from its time-0 rows, and its rows encode the configurations of the run on those inputs, by induction on time: at each step the window clauses force, through the check circuit, local consistency of every window, and a locally consistent window whose time-t part is that of a configuration has the time-t + 1 part of its successor (post_of_pre). The acceptance row and the emission bookkeeping then give acceptance.

Both directions use the head bounds headsIn_cfgAt: along a run, a head moves at most one cell per step, so at every time t ≤ S every head is on an interior cell of the tableau.

def MIPRE.TM.CookLevin.AcceptsIn {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) (input : Fin i → List Symbol) (S : ℕ) : Prop

Acceptance within S steps: halted at time S, having output exactly [acc].

Equations

• MIPRE.TM.CookLevin.AcceptsIn M acc input S = ((Turing.MultiInputTM.configs (Turing.MultiInputTM.initCfg input) S).state = none ∧ M.outputString (Turing.MultiInputTM.initCfg input) S = [acc])

Head bounds along a run

theorem MIPRE.TM.CookLevin.cfgAt_zero {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} : cfgAt M 0 = Turing.MultiInputTM.initCfg input

theorem MIPRE.TM.CookLevin.cfgAt_zero' {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} : cfgAt M ↑0 = Turing.MultiInputTM.initCfg input

theorem MIPRE.TM.CookLevin.SignType.cast_bounds (m : SignType) : -1 ≤ ↑m ∧ ↑m ≤ 1

theorem MIPRE.TM.CookLevin.inputPos_cfgAt_le {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (t : ℕ) (j : Fin i) : ↑((cfgAt M t).inputPos j) ≤ t + 1

An input head is at position at most t + 1 at time t.

theorem MIPRE.TM.CookLevin.workTapePos_cfgAt_bounds {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (t : ℕ) (j : Fin w) : -↑t ≤ (cfgAt M t).workTapePos j ∧ (cfgAt M t).workTapePos j ≤ ↑t

A work head is at a position of absolute value at most t at time t.

theorem MIPRE.TM.CookLevin.headsIn_cfgAt {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (t : ℕ) (ht : t ≤ S) : HeadsIn (cfgAt M t) S

At every time t ≤ S, every head of the run is on an interior cell.

The output string of an accepting run

theorem MIPRE.TM.CookLevin.outputString_zero {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) : M.outputString c 0 = []

theorem MIPRE.TM.CookLevin.outputString_succ' {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (t : ℕ) : M.outputString (Turing.MultiInputTM.initCfg input) (t + 1) = M.outputString (Turing.MultiInputTM.initCfg input) t ++ (Turing.MultiInputTM.outputSymbol (cfgAt M t)).toList

theorem MIPRE.TM.CookLevin.outputString_split {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (t : ℕ) (ht : t < S) : M.outputString (Turing.MultiInputTM.initCfg input) S = M.outputString (Turing.MultiInputTM.initCfg input) t ++ (Turing.MultiInputTM.outputSymbol (cfgAt M t)).toList ++ M.outputString (cfgAt M (t + 1)) (S - (t + 1))

The output of S steps, split at step t.

theorem MIPRE.TM.CookLevin.singleton_eq_append₃ {α : Type u_3} {x : α} {A B C : List α} (h : [x] = A ++ B ++ C) : (B ≠ [] → A = [] ∧ B = [x] ∧ C = []) ∧ (A ≠ [] → B = [])

theorem MIPRE.TM.CookLevin.outputSymbol_of_accepting {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (hacc : M.outputString (Turing.MultiInputTM.initCfg input) S = [acc]) (t : ℕ) (ht : t < S) (hne : Turing.MultiInputTM.outputSymbol (cfgAt M t) ≠ none) : Turing.MultiInputTM.outputSymbol (cfgAt M t) = some acc ∧ M.outputString (Turing.MultiInputTM.initCfg input) t = []

In a run whose output over S steps is [acc], a step that emits emits acc, and nothing was emitted before it.

The assignment of a run, by variable

@[simp]

theorem MIPRE.TM.CookLevin.runAssign_cell {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin (S + 1)) (d : Tape i w) (p : Pos S) (v : CellVal Symbol) : runAssign M acc chk (TabVar.cell t d p v) = baseAssign M acc chk.gates.length (TabVar.cell t d p v)

@[simp]

theorem MIPRE.TM.CookLevin.runAssign_head {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin (S + 1)) (d : Tape i w) (p : Pos S) : runAssign M acc chk (TabVar.head t d p) = baseAssign M acc chk.gates.length (TabVar.head t d p)

@[simp]

theorem MIPRE.TM.CookLevin.runAssign_state {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin (S + 1)) (q : Option State) : runAssign M acc chk (TabVar.state t q) = baseAssign M acc chk.gates.length (TabVar.state t q)

@[simp]

theorem MIPRE.TM.CookLevin.runAssign_emitOne {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin S) : runAssign M acc chk (TabVar.emitOne t) = baseAssign M acc chk.gates.length (TabVar.emitOne t)

@[simp]

theorem MIPRE.TM.CookLevin.runAssign_emitBad {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin S) : runAssign M acc chk (TabVar.emitBad t) = baseAssign M acc chk.gates.length (TabVar.emitBad t)

@[simp]

theorem MIPRE.TM.CookLevin.runAssign_emitted {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin (S + 1)) : runAssign M acc chk (TabVar.emitted t) = baseAssign M acc chk.gates.length (TabVar.emitted t)

theorem MIPRE.TM.CookLevin.runAssign_aux {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin S) (js : Tape i w → Center S) (g : Fin chk.gates.length) : runAssign M acc chk (TabVar.aux t js g) = chk.valueAt (fun (n : ℕ) => baseAssign M acc chk.gates.length (inpOf t js n)) ↑g

theorem MIPRE.TM.CookLevin.runAssign_winVarOf {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin S) (js : Tape i w → Center S) (v : WinVar i w Symbol State) : runAssign M acc chk (winVarOf t js v) = baseAssign M acc chk.gates.length (winVarOf t js v)

theorem MIPRE.TM.CookLevin.runAssign_inpOf {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (t : Fin S) (js : Tape i w → Center S) (n : ℕ) : runAssign M acc chk (inpOf t js n) = baseAssign M acc chk.gates.length (inpOf t js n)

Clause evaluation

theorem MIPRE.TM.CookLevin.unit_eval {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (v : TabVar i w Symbol State S G) (b : Bool) : SAT.Clause3.eval f (unit v b) = true ↔ f v = b

theorem MIPRE.TM.CookLevin.imp2_eval {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (a b : TabVar i w Symbol State S G) : SAT.Clause3.eval f (imp2 a b) = true ↔ f a = true → f b = true

theorem MIPRE.TM.CookLevin.nand2_eval {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (a b : TabVar i w Symbol State S G) : SAT.Clause3.eval f (nand2 a b) = true ↔ ¬(f a = true ∧ f b = true)

theorem MIPRE.TM.CookLevin.cl_eval {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (l₁ l₂ l₃ : SAT.Lit (TabVar i w Symbol State S G)) : SAT.Clause3.eval f (SAT.cl l₁ l₂ l₃) = true ↔ SAT.Lit.eval f l₁ = true ∨ SAT.Lit.eval f l₂ = true ∨ SAT.Lit.eval f l₃ = true

@[simp]

theorem MIPRE.TM.CookLevin.lit_eval_true {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (v : TabVar i w Symbol State S G) : SAT.Lit.eval f { var := v, pos := true } = f v

@[simp]

theorem MIPRE.TM.CookLevin.lit_eval_false {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (v : TabVar i w Symbol State S G) : SAT.Lit.eval f { var := v, pos := false } = !f v

Cells

theorem MIPRE.TM.CookLevin.cellValAt_inl {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (j : Fin i) (p : Pos S) : cellValAt c (Sum.inl j) p = inputCellVal (input j) p

theorem MIPRE.TM.CookLevin.cellValAt_bdry {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (d : Tape i w) (p : Pos S) (hb : p.IsBdry) : cellValAt c d p = CellVal.bdry

theorem MIPRE.TM.CookLevin.inputCellVal_mem {Symbol : Type u_1} {S : ℕ} (x : List Symbol) (p : Pos S) (hnb : ¬p.IsBdry) : inputCellVal x p = CellVal.blank ∨ ∃ (k : ℕ) (hk : k < x.length), ↑p = k + 3 ∧ inputCellVal x p = CellVal.sym x[k]

An interior input cell holds a blank or a symbol of the string.

theorem MIPRE.TM.CookLevin.inputCellVal_two {Symbol : Type u_1} {S : ℕ} (x : List Symbol) : inputCellVal x ⟨2, ⋯⟩ = CellVal.blank

Cell 2 of an input tape is blank.

theorem MIPRE.TM.CookLevin.inputCellVal_blank_mono {Symbol : Type u_1} {S : ℕ} (x : List Symbol) (p p' : Pos S) (h2 : 2 < ↑p) (hnb' : ¬p'.IsBdry) (hpp' : p < p') (h : inputCellVal x p = CellVal.blank) : inputCellVal x p' = CellVal.blank

Blanks propagate to the right on an input tape.

Completeness: the window clauses

theorem MIPRE.TM.CookLevin.baseAssign_emitted_zero {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} {G : ℕ} : baseAssign M acc G (TabVar.emitted 0) = false

theorem MIPRE.TM.CookLevin.getD_winBits {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S G : ℕ} (f : TabVar i w Symbol State S G → Bool) (h0 : f (TabVar.emitted 0) = false) (t : Fin S) (js : Tape i w → Center S) (n : ℕ) : (winBits fun (v : WinVar i w Symbol State) => f (winVarOf t js v)).getD n false = f (inpOf t js n)

The bits of the window read from f are the values of f on the circuit's inputs.

theorem MIPRE.TM.CookLevin.chk_eval_run {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (hchk : IsCheckCircuit M acc chk) (t : Fin S) (js : Tape i w → Center S) : (chk.eval fun (n : ℕ) => baseAssign M acc chk.gates.length (inpOf t js n)) = true

The check circuit accepts every window of the run.

theorem MIPRE.TM.CookLevin.windowClauses_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (hchk : IsCheckCircuit M acc chk) (hC : chk.RefsLt) : (windowClauses S chk).Sat (runAssign M acc chk)

Completeness: the other clauses

theorem MIPRE.TM.CookLevin.startClauses_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (fixed : Fin i → Option (List Symbol)) (hfix : ∀ (j : Fin i) (x : List Symbol), fixed j = some x → input j = x) : (startClauses S chk.gates.length M fixed).Sat (runAssign M acc chk)

theorem MIPRE.TM.CookLevin.freeClauses_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (hfree : ∀ (j : Fin i), fixed j = none → ∀ s ∈ input j, s = s₀ ∨ s = s₁) : (freeClauses S chk.gates.length s₀ s₁ fixed).Sat (runAssign M acc chk)

theorem MIPRE.TM.CookLevin.bdryClauses_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) : (bdryClauses S chk.gates.length).Sat (runAssign M acc chk)

theorem MIPRE.TM.CookLevin.emitClauses_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (hacc : M.outputString (Turing.MultiInputTM.initCfg input) S = [acc]) : (emitClauses S chk.gates.length).Sat (runAssign M acc chk)

theorem MIPRE.TM.CookLevin.finalClauses_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (hacc : AcceptsIn M acc input S) : (finalClauses S chk.gates.length).Sat (runAssign M acc chk)

theorem MIPRE.TM.CookLevin.tableau_sat_of_acceptsIn {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (hchk : IsCheckCircuit M acc chk) (hC : chk.RefsLt) (hfix : ∀ (j : Fin i) (x : List Symbol), fixed j = some x → input j = x) (hfree : ∀ (j : Fin i), fixed j = none → ∀ s ∈ input j, s = s₀ ∨ s = s₁) (hacc : AcceptsIn M acc input S) : (tableau M s₀ s₁ S fixed chk).Sat (runAssign M acc chk)

Completeness of the tableau. The assignment of an accepting run satisfies the tableau formula.