The described formula and the answers

The two halves of item 1 of thm:succinct-sat for the describer: a satisfying assignment of the described formula extending the two answer blocks exists iff the blocks are the two-bit tape encodings (tapeBits) of strings of length at most T that the decider accepts within T (planning/succinct-cook-levin.md, S3).

The bridge in both directions is the decoding: an assignment of the formula gives the tableau assignment w ∘ idxOf (sat_tableau_of_sat_formula3), and an assignment of the tableau gives the formula assignment decodeVar · |>.elim false (sat_formula3_of_sat_tableau). The answer blocks match because the canonical index of an answer cell is its answer index (idxOf_ans) and because a time-0 row of a free tape reads exactly the tape encoding of the string it holds (decide_val_inputCellVal).

The two-bit tape encoding on a time-0 row

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_bits (l : Cost.BitStr) : (Interp.bits l).length = List.length l

theorem MIPRE.TM.CookLevin.Desc.getElem_bits (l : Cost.BitStr) (k : ℕ) (h : k < (Interp.bits l).length) : (Interp.bits l)[k] = if l[k] = true then Interp.Sym.one else Interp.Sym.zero

def MIPRE.TM.CookLevin.Desc.boolsOf (s : List Interp.Sym) : Cost.BitStr

The bit string of a list of symbols over {0, 1}.

Equations

• MIPRE.TM.CookLevin.Desc.boolsOf s = List.map (fun (c : MIPRE.TM.Interp.Sym) => decide (c = MIPRE.TM.Interp.Sym.one)) s

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_boolsOf (s : List Interp.Sym) : List.length (boolsOf s) = s.length

theorem MIPRE.TM.CookLevin.Desc.bits_boolsOf (s : List Interp.Sym) (h : ∀ c ∈ s, c = Interp.Sym.zero ∨ c = Interp.Sym.one) : Interp.bits (boolsOf s) = s

theorem MIPRE.TM.CookLevin.Desc.decide_val_inputCellVal (e : ℕ) (ap : Cost.BitStr) (k : ℕ) {p : Pos (Sof e)} (hp : ↑p = k / 2 + 3) (hk : k < 2 * Sof e) : decide ((if k % 2 = 1 then CellVal.sym Interp.Sym.one else CellVal.blank) = inputCellVal (Interp.bits ap) p) = SAT.tapeBits ap k

The time-0 row of a free tape reads the tape encoding of the string it holds: the cell at position k / 2 + 3 holds the blank for k even and 1 for k odd exactly when the k-th bit of the encoding is set.

The two bridges

noncomputable def MIPRE.TM.CookLevin.Desc.wOf (e T : ℕ) (A : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) Gc → Bool) (i : Fin (2 ^ mOf e Gc)) : Bool

The assignment of the described formula read off a tableau assignment through the decoding.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.wOf_of_decode (e T : ℕ) {A : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) Gc → Bool} {i : Fin (2 ^ mOf e Gc)} {v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) Gc} (h : decodeVar e Gc (fieldsOf e Gc T (SAT.bitsOfNat (mOf e Gc) ↑i)) = some v) : wOf e T A i = A v

theorem MIPRE.TM.CookLevin.Desc.sat_formula3_of_sat_tableau (e T : ℕ) (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) (A : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) Gc → Bool) (hA : (tableauPlus e T (fixedOf D n T x y) chk).Sat A) : ((descCirc e T D n x y).formula3 (mOf e Gc)).Sat (wOf e T A)

From a tableau assignment to an assignment of the described formula.

theorem MIPRE.TM.CookLevin.Desc.sat_tableau_of_sat_formula3 (e T : ℕ) (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) (w : Fin (2 ^ mOf e Gc) → Bool) (hw : ((descCirc e T D n x y).formula3 (mOf e Gc)).Sat w) : (tableauPlus e T (fixedOf D n T x y) chk).Sat fun (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) chk.gates.length) => w ⟨idxOf e Gc T v, ⋯⟩

From an assignment of the described formula to a tableau assignment.

The input tapes of the machine

theorem MIPRE.TM.CookLevin.Desc.mem_bits' {s : Interp.Sym} {l : Cost.BitStr} (h : s ∈ Interp.bits l) : s = Interp.Sym.zero ∨ s = Interp.Sym.one

theorem MIPRE.TM.CookLevin.Desc.hfix_uInput (D : Cost.Prog) (n T : ℕ) (x y ap bp : Cost.BitStr) (j : Fin 7) (s : List Interp.Sym) : fixedOf D n T x y j = some s → Interp.uInput D n T x y ap bp j = s

theorem MIPRE.TM.CookLevin.Desc.hfree_uInput (D : Cost.Prog) (n T : ℕ) (x y ap bp : Cost.BitStr) (j : Fin 7) : fixedOf D n T x y j = none → ∀ s ∈ Interp.uInput D n T x y ap bp j, s = Interp.Sym.zero ∨ s = Interp.Sym.one

theorem MIPRE.TM.CookLevin.Desc.decide_inputCellVal_val (e : ℕ) (ap : Cost.BitStr) (k : ℕ) {p : Pos (Sof e)} (hp : ↑p = k / 2 + 3) (hk : k < 2 * Sof e) : decide (inputCellVal (Interp.bits ap) p = if k % 2 = 1 then CellVal.sym Interp.Sym.one else CellVal.blank) = SAT.tapeBits ap k

Item 1 of the theorem

theorem MIPRE.TM.CookLevin.Desc.extendsAnswers_of_encodesAccepted (𝒟 : Decider) (n T : ℕ) (x y : Cost.BitStr) (e : ℕ) (hT : T ≤ Sof e) (hlen : FixedLen e 𝒟.prog n T x y) (hTm : T + 3 < 2 ^ W e) (hrb : ∀ (ap bp : Cost.BitStr), List.length ap ≤ T → List.length bp ≤ T → Interp.runBound 𝒟.prog n x y ap bp T ≤ Sof e) (h4T : 4 * T ≤ 2 ^ mOf e Gc) (a b : Fin (2 * T) → Bool) (h : SAT.EncodesAccepted 𝒟 n x y T a b) : SAT.ExtendsAnswers h4T ((descCirc e T 𝒟.prog n x y).formula3 (mOf e Gc)) a b

Completeness: if the answers encode strings the decider accepts within T, the described formula has a satisfying assignment extending them.

theorem MIPRE.TM.CookLevin.Desc.length_le_of_inputCellVal_blank {S : ℕ} (s : List Interp.Sym) (p : Pos S) (hnb : ¬p.IsBdry) (h3 : 3 ≤ ↑p) (h : inputCellVal s p = CellVal.blank) : s.length ≤ ↑p - 3

A blank at an interior cell bounds the string on the tape.

theorem MIPRE.TM.CookLevin.Desc.encodesAccepted_of_extendsAnswers (𝒟 : Decider) (n T : ℕ) (x y : Cost.BitStr) (e : ℕ) (hT : T ≤ Sof e) (hlen : FixedLen e 𝒟.prog n T x y) (hTm : T + 3 < 2 ^ W e) (h4T : 4 * T ≤ 2 ^ mOf e Gc) (a b : Fin (2 * T) → Bool) (h : SAT.ExtendsAnswers h4T ((descCirc e T 𝒟.prog n x y).formula3 (mOf e Gc)) a b) : SAT.EncodesAccepted 𝒟 n x y T a b

Soundness: a satisfying assignment of the described formula extending the answers gives strings of length at most T, encoded by the answers, that the decider accepts within T.

theorem MIPRE.TM.CookLevin.Desc.extendsAnswers_iff (𝒟 : Decider) (n T : ℕ) (x y : Cost.BitStr) (e : ℕ) (hT : T ≤ Sof e) (hlen : FixedLen e 𝒟.prog n T x y) (hTm : T + 3 < 2 ^ W e) (hrb : ∀ (ap bp : Cost.BitStr), List.length ap ≤ T → List.length bp ≤ T → Interp.runBound 𝒟.prog n x y ap bp T ≤ Sof e) (h4T : 4 * T ≤ 2 ^ mOf e Gc) (a b : Fin (2 * T) → Bool) : SAT.ExtendsAnswers h4T ((descCirc e T 𝒟.prog n x y).formula3 (mOf e Gc)) a b ↔ SAT.EncodesAccepted 𝒟 n x y T a b

Item 1 of thm:succinct-sat for the describer.