The describer circuit and the clauses it describes

descCirc e T D n x y is the circuit of the describer: the flattening of the formula tableauPlusF on the candidate that reads the three m-bit indices and the three signs off its 3m + 3 inputs (candOf). mem_formula3_iff is what it describes: a clause of Fin (2 ^ m) is accepted iff its three indices decode to the literals of a clause of tableauPlus — the tableau of U on the input tapes fixedOf together with the two answer-end clauses (planning/succinct-cook-levin.md, S3).

Reading the input bits of a clause

theorem MIPRE.TM.CookLevin.Desc.getD_drop_eq (l : Cost.BitStr) (k i : ℕ) : (List.drop k l).getD i false = List.getD l (k + i) false

theorem MIPRE.TM.CookLevin.Desc.ibOf_getD (l : Cost.BitStr) (b n : ℕ) (h : b + n ≤ List.length l) : (ibOf b n fun (i : ℕ) => List.getD l i false) = List.take n (List.drop b l)

The input tapes

def MIPRE.TM.CookLevin.Desc.fixedOf (D : Cost.Prog) (n T : ℕ) (x y : Cost.BitStr) : Fin 7 → Option (List Interp.Sym)

The input tapes of the interpreter machine: the program, the index, the time bound in unary and the two questions are fixed; the two answer tapes are free.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Desc.freeSpec (D : Cost.Prog) (n T : ℕ) (x y : Cost.BitStr) : FreeSpec (fixedOf D n T x y) [5, 6]

def MIPRE.TM.CookLevin.Desc.FixedLen (e : ℕ) (D : Cost.Prog) (n T : ℕ) (x y : Cost.BitStr) : Prop

The tapes are short enough for the tableau.

Equations

• MIPRE.TM.CookLevin.Desc.FixedLen e D n T x y = ∀ (j : Fin 7) (s : List MIPRE.TM.Interp.Sym), MIPRE.TM.CookLevin.Desc.fixedOf D n T x y j = some s → s.length ≤ MIPRE.TM.CookLevin.Desc.Sof e

noncomputable def MIPRE.TM.CookLevin.Desc.tabsOf (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (A : FieldsF) : List (ℕ × SAT.Fml)

The value formulas of the fixed tapes.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Desc.tapeSpec (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (hT : T ≤ Sof e) (hlen : FixedLen e D n T x y) : TapeSpec e A (fixedOf D n T x y) (tabsOf e T D n x y A)

theorem MIPRE.TM.CookLevin.Desc.tabsOf_inputsLt (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) {N : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt N A) (jv : ℕ × SAT.Fml) : jv ∈ tabsOf e T D n x y A → SAT.Fml.InputsLt N jv.2

The candidate of formulas

noncomputable def MIPRE.TM.CookLevin.Desc.candOf (e G T : ℕ) : CandF

The candidate the describer reads off its inputs: the three m-bit indices at bases 0, m, 2m and the three signs at 3m, 3m + 1, 3m + 2.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Desc.candOf_lengths (e G T : ℕ) : CandF.Lengths e G (candOf e G T)

theorem MIPRE.TM.CookLevin.Desc.candOf_inputsLt (e G T : ℕ) : CandF.InputsLt (3 * mOf e G + 3) (candOf e G T)

The circuit

noncomputable def MIPRE.TM.CookLevin.Desc.descFml (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Fml

The formula of the describer.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.TM.CookLevin.Desc.descCirc (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Circuit

The describer circuit: the flattening of descFml on 3 m + 3 inputs.

Equations

• MIPRE.TM.CookLevin.Desc.descCirc e T D n x y = MIPRE.SAT.Fml.toCircuit (3 * MIPRE.TM.CookLevin.Desc.mOf e MIPRE.TM.CookLevin.Desc.Gc + 3) (MIPRE.TM.CookLevin.Desc.descFml e T D n x y)

theorem MIPRE.TM.CookLevin.Desc.descCirc_inputs (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : (descCirc e T D n x y).inputs = 3 * mOf e Gc + 3

theorem MIPRE.TM.CookLevin.Desc.descFml_inputsLt (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Fml.InputsLt (3 * mOf e Gc + 3) (descFml e T D n x y)

theorem MIPRE.TM.CookLevin.Desc.descCirc_wellFormed (e T : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : (descCirc e T D n x y).WellFormed

What the circuit describes

noncomputable def MIPRE.TM.CookLevin.Desc.candOfClause (e T : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : Cand

The candidate of a clause: the fields of its three indices and its three signs.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Desc.clauseInput_eq (m : ℕ) (c' : SAT.Clause3 (Fin (2 ^ m))) : SAT.clauseInput m c' = SAT.bitsOfNat m ↑c'.l₁.var ++ (SAT.bitsOfNat m ↑c'.l₂.var ++ (SAT.bitsOfNat m ↑c'.l₃.var ++ [c'.l₁.pos, c'.l₂.pos, c'.l₃.pos]))

theorem MIPRE.TM.CookLevin.Desc.ibOf_clauseInput_zero (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : (ibOf 0 (mOf e Gc) fun (i : ℕ) => (SAT.clauseInput (mOf e Gc) c).getD i false) = SAT.bitsOfNat (mOf e Gc) ↑c.l₁.var

The bits of the three blocks of the input of a clause.

theorem MIPRE.TM.CookLevin.Desc.ibOf_clauseInput_one (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : (ibOf (mOf e Gc) (mOf e Gc) fun (i : ℕ) => (SAT.clauseInput (mOf e Gc) c).getD i false) = SAT.bitsOfNat (mOf e Gc) ↑c.l₂.var

theorem MIPRE.TM.CookLevin.Desc.ibOf_clauseInput_two (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : (ibOf (2 * mOf e Gc) (mOf e Gc) fun (i : ℕ) => (SAT.clauseInput (mOf e Gc) c).getD i false) = SAT.bitsOfNat (mOf e Gc) ↑c.l₃.var

theorem MIPRE.TM.CookLevin.Desc.drop_clauseInput (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : List.drop (3 * mOf e Gc) (SAT.clauseInput (mOf e Gc) c) = [c.l₁.pos, c.l₂.pos, c.l₃.pos]

theorem MIPRE.TM.CookLevin.Desc.getD_clauseInput_sign0 (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : (SAT.clauseInput (mOf e Gc) c).getD (3 * mOf e Gc) false = c.l₁.pos

theorem MIPRE.TM.CookLevin.Desc.getD_clauseInput_sign1 (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : (SAT.clauseInput (mOf e Gc) c).getD (3 * mOf e Gc + 1) false = c.l₂.pos

theorem MIPRE.TM.CookLevin.Desc.getD_clauseInput_sign2 (e : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) : (SAT.clauseInput (mOf e Gc) c).getD (3 * mOf e Gc + 2) false = c.l₃.pos

theorem MIPRE.TM.CookLevin.Desc.evalCand_candOf (e T : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) (hT : T ≤ Sof e) : (evalCand (candOf e Gc T) fun (i : ℕ) => (SAT.clauseInput (mOf e Gc) c).getD i false) = candOfClause e T c

The candidate of formulas, evaluated on the input bits of a clause, is the candidate of the clause.

theorem MIPRE.TM.CookLevin.Desc.mem_formula3_iff (e T : ℕ) (c : SAT.Clause3 (Fin (2 ^ mOf e Gc))) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (hT : T ≤ Sof e) (hlen : FixedLen e D n T x y) (hTm : T + 3 < 2 ^ W e) : c ∈ (descCirc e T D n x y).formula3 (mOf e Gc) ↔ ∃ cl ∈ tableauPlus e T (fixedOf D n T x y) chk, Cand.Dec e Gc (candOfClause e T c) cl

What the describer describes: a clause is accepted iff its three indices decode to the literals of a clause of tableauPlus.