The window family, on decoded fields

The window clauses of the tableau are the Tseitin clauses of the check circuit chk at every step t and window js (windowClauses). Every such clause has a gate literal (aux t js g) in its third position: the templates of a gate (gateTemplates) list its clauses as triples of literal specs — a gate index (.aux u) or a window input (.win n) — with their signs, and the clause is recovered from the templates by instantiating the specs at (t, js) (gateClauses_eq_templates). A candidate matches a template when its third record is a gate variable of the template's gate and the other two records denote the spec's variable relative to it (SpecMatch: the time and centers are read off the third record). windowPred_iff: the candidate decodes to a window clause iff it matches a template of a gate, or is the output unit clause (planning/succinct-cook-levin.md, S3).

Templates

inductive MIPRE.TM.CookLevin.Desc.LitSpec : Type

A literal of a Tseitin clause, before instantiation: a gate variable or a window input.

• aux (u : ℕ) : LitSpec
• win (n : ℕ) : LitSpec

@[instance_reducible]

instance MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec : DecidableEq LitSpec

Equations

• MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec = MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec.decEq

def MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec.decEq (x✝ x✝¹ : LitSpec) : Decidable (x✝ = x✝¹)

Equations

• MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec.decEq (MIPRE.TM.CookLevin.Desc.LitSpec.aux a) (MIPRE.TM.CookLevin.Desc.LitSpec.aux b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec.decEq (MIPRE.TM.CookLevin.Desc.LitSpec.aux u) (MIPRE.TM.CookLevin.Desc.LitSpec.win n) = isFalse ⋯
• MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec.decEq (MIPRE.TM.CookLevin.Desc.LitSpec.win n) (MIPRE.TM.CookLevin.Desc.LitSpec.aux u) = isFalse ⋯
• MIPRE.TM.CookLevin.Desc.instDecidableEqLitSpec.decEq (MIPRE.TM.CookLevin.Desc.LitSpec.win a) (MIPRE.TM.CookLevin.Desc.LitSpec.win b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev MIPRE.TM.CookLevin.Desc.Tpl : Type

A clause template: three specs with their signs.

Equations

• MIPRE.TM.CookLevin.Desc.Tpl = ((MIPRE.TM.CookLevin.Desc.LitSpec × Bool) × (MIPRE.TM.CookLevin.Desc.LitSpec × Bool) × MIPRE.TM.CookLevin.Desc.LitSpec × Bool)

def MIPRE.TM.CookLevin.Desc.gateTemplates (g : ℕ) : SAT.Gate → List Tpl

The Tseitin clauses of gate g, as templates (gateClauses, Tseitin.lean).

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.specVar {S G : ℕ} (t : Fin S) (js : Tape 7 6 → Center S) : LitSpec → TabVar 7 6 Interp.Sym Interp.Ctl S G

The tableau variable of a spec at step t and window js.

Equations

• MIPRE.TM.CookLevin.Desc.specVar t js (MIPRE.TM.CookLevin.Desc.LitSpec.aux u) = MIPRE.TM.CookLevin.auxOf t js u
• MIPRE.TM.CookLevin.Desc.specVar t js (MIPRE.TM.CookLevin.Desc.LitSpec.win n) = MIPRE.TM.CookLevin.inpOf t js n

noncomputable def MIPRE.TM.CookLevin.Desc.Tpl.clause {S G : ℕ} (t : Fin S) (js : Tape 7 6 → Center S) (tp : Tpl) : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl S G)

The clause of a template at step t and window js.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.gateClauses_eq_templates {S G : ℕ} (t : Fin S) (js : Tape 7 6 → Center S) (g : ℕ) (gate : SAT.Gate) : SAT.gateClauses (inpOf t js) (auxOf t js) (auxOf t js g) gate = List.map (Tpl.clause t js) (gateTemplates g gate)

theorem MIPRE.TM.CookLevin.Desc.third_of_templates (g : ℕ) (gate : SAT.Gate) (tp : Tpl) (h : tp ∈ gateTemplates g gate) : tp.2.2.1 = LitSpec.aux g

The third spec of every template of gate g is the gate itself.

theorem MIPRE.TM.CookLevin.Desc.spec_of_templates (g : ℕ) (gate : SAT.Gate) (tp : Tpl) (h : tp ∈ gateTemplates g gate) (sp : LitSpec) (hsp : sp = tp.1.1 ∨ sp = tp.2.1.1 ∨ sp = tp.2.2.1) : (∃ (u : ℕ), sp = LitSpec.aux u ∧ (u = g ∨ u ∈ gate.refs)) ∨ ∃ (i : ℕ), sp = LitSpec.win i ∧ gate = SAT.Gate.input i

A spec of a template of gate g is the gate, a gate it reads, or the input it reads.

Matching a spec against the gate literal

def MIPRE.TM.CookLevin.Desc.WinMatch (e : ℕ) (Fa : Fields) : WinVar 7 6 Interp.Sym Interp.Ctl → Fields → Prop

The record F denotes the window variable wv of the window of the record Fa (a gate variable: its time and centers are Fa.t, Fa.js).

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.WinMatch e Fa (MIPRE.TM.CookLevin.WinVar.statePre q) x✝ = (MIPRE.TM.CookLevin.Desc.IsState e x✝ ∧ x✝.t = Fa.t ∧ x✝.q = MIPRE.TM.CookLevin.Desc.qCode q)
• MIPRE.TM.CookLevin.Desc.WinMatch e Fa (MIPRE.TM.CookLevin.WinVar.statePost q) x✝ = (MIPRE.TM.CookLevin.Desc.IsState e x✝ ∧ x✝.t = Fa.t + 1 ∧ x✝.q = MIPRE.TM.CookLevin.Desc.qCode q)
• MIPRE.TM.CookLevin.Desc.WinMatch e Fa MIPRE.TM.CookLevin.WinVar.emitOne x✝ = (MIPRE.TM.CookLevin.Desc.IsEmitOne e x✝ ∧ x✝.t = Fa.t)
• MIPRE.TM.CookLevin.Desc.WinMatch e Fa MIPRE.TM.CookLevin.WinVar.emitBad x✝ = (MIPRE.TM.CookLevin.Desc.IsEmitBad e x✝ ∧ x✝.t = Fa.t)

def MIPRE.TM.CookLevin.Desc.SpecMatch (e G : ℕ) (Fa : Fields) : LitSpec → Fields → Prop

The record F denotes the variable of the spec, relative to the gate record Fa.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.SpecMatch e G Fa (MIPRE.TM.CookLevin.Desc.LitSpec.aux u) x✝ = (MIPRE.TM.CookLevin.Desc.IsAux e G x✝ ∧ x✝.t = Fa.t ∧ (∀ (k : Fin 13), x✝.js k = Fa.js k) ∧ x✝.g = u)

theorem MIPRE.TM.CookLevin.Desc.winMatch_iff (e G : ℕ) {Fa : Fields} {t : Fin (Sof e)} {js : Tape 7 6 → Center (Sof e)} (ht : Fa.t = ↑t) (hjs : ∀ (d : Tape 7 6), Fa.js ⟨tapeCode d, ⋯⟩ = ↑(js d)) (wv : WinVar 7 6 Interp.Sym Interp.Ctl) (F : Fields) : WinMatch e Fa wv F ↔ decodeVar e G F = some (winVarOf t js wv)

theorem MIPRE.TM.CookLevin.Desc.specMatch_aux_iff (e G : ℕ) {Fa : Fields} {t : Fin (Sof e)} {js : Tape 7 6 → Center (Sof e)} (ht : Fa.t = ↑t) (hjs : ∀ (d : Tape 7 6), Fa.js ⟨tapeCode d, ⋯⟩ = ↑(js d)) (u : ℕ) (hu : u < G) (F : Fields) : SpecMatch e G Fa (LitSpec.aux u) F ↔ decodeVar e G F = some (specVar t js (LitSpec.aux u))

theorem MIPRE.TM.CookLevin.Desc.specMatch_win_iff (e G : ℕ) {Fa : Fields} {t : Fin (Sof e)} {js : Tape 7 6 → Center (Sof e)} (ht : Fa.t = ↑t) (hjs : ∀ (d : Tape 7 6), Fa.js ⟨tapeCode d, ⋯⟩ = ↑(js d)) (n : ℕ) (hn : n < winCard 7 6 Interp.Sym Interp.Ctl) (F : Fields) : SpecMatch e G Fa (LitSpec.win n) F ↔ decodeVar e G F = some (specVar t js (LitSpec.win n))

The window predicate

def MIPRE.TM.CookLevin.Desc.TplMatch (e G : ℕ) (tp : Tpl) (c : Cand) : Prop

The candidate matches the template, its third record being the gate literal.

Equations

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

def MIPRE.TM.CookLevin.Desc.WindowGates (e G : ℕ) (chk : SAT.Circuit) (c : Cand) : Prop

The candidate matches a template of some gate of chk.

Equations

• MIPRE.TM.CookLevin.Desc.WindowGates e G chk c = ∃ (g : Fin chk.gates.length), ∃ tp ∈ MIPRE.TM.CookLevin.Desc.gateTemplates (↑g) chk.gates[g], MIPRE.TM.CookLevin.Desc.TplMatch e G tp c

def MIPRE.TM.CookLevin.Desc.WindowOut (e G : ℕ) (c : Cand) : Prop

The candidate is the output unit clause of a window.

Equations

• MIPRE.TM.CookLevin.Desc.WindowOut e G c = (MIPRE.TM.CookLevin.Desc.UnitAux e G c ∧ MIPRE.TM.CookLevin.Desc.SameSigns c ∧ c.F₁.g = G - 1 ∧ c.s₁ = true)

def MIPRE.TM.CookLevin.Desc.WindowPred (e G : ℕ) (chk : SAT.Circuit) (c : Cand) : Prop

The window family.

Equations

• MIPRE.TM.CookLevin.Desc.WindowPred e G chk c = (MIPRE.TM.CookLevin.Desc.WindowGates e G chk c ∨ MIPRE.TM.CookLevin.Desc.WindowOut e G c)

theorem MIPRE.TM.CookLevin.Desc.spec_lt (chk : SAT.Circuit) (hC : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) (g : Fin chk.gates.length) (tp : Tpl) (h : tp ∈ gateTemplates (↑g) chk.gates[g]) (sp : LitSpec) (hsp : sp = tp.1.1 ∨ sp = tp.2.1.1 ∨ sp = tp.2.2.1) : (∃ (u : ℕ), sp = LitSpec.aux u ∧ u < chk.gates.length) ∨ ∃ (i : ℕ), sp = LitSpec.win i ∧ i < winCard 7 6 Interp.Sym Interp.Ctl

The specs of a template of a gate of chk are in range.

theorem MIPRE.TM.CookLevin.Desc.specMatch_iff (e : ℕ) (chk : SAT.Circuit) (hC : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) {Fa : Fields} {t : Fin (Sof e)} {js : Tape 7 6 → Center (Sof e)} (ht : Fa.t = ↑t) (hjs : ∀ (d : Tape 7 6), Fa.js ⟨tapeCode d, ⋯⟩ = ↑(js d)) (g : Fin chk.gates.length) (tp : Tpl) (h : tp ∈ gateTemplates (↑g) chk.gates[g]) (sp : LitSpec) (hsp : sp = tp.1.1 ∨ sp = tp.2.1.1 ∨ sp = tp.2.2.1) (F : Fields) : SpecMatch e chk.gates.length Fa sp F ↔ decodeVar e chk.gates.length F = some (specVar t js sp)

theorem MIPRE.TM.CookLevin.Desc.windowPred_iff (e : ℕ) (chk : SAT.Circuit) (hC : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) (hne : chk.gates ≠ []) (c : Cand) : WindowPred e chk.gates.length chk c ↔ ∃ cl ∈ windowClauses (Sof e) chk, Cand.Dec e chk.gates.length c cl

The window family is exact: a candidate satisfies WindowPred iff it decodes to a window clause of the tableau.

The whole tableau

theorem MIPRE.TM.CookLevin.Desc.tableau_dec_iff (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (chk : SAT.Circuit) (hC : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) (hne : chk.gates ≠ []) (c : Cand) : MainPred e fixed c ∨ WindowPred e chk.gates.length chk c ↔ ∃ cl ∈ tableau Interp.U Interp.Sym.zero Interp.Sym.one (Sof e) fixed chk, Cand.Dec e chk.gates.length c cl

The candidate decodes to a clause of the tableau iff it satisfies one of the family predicates.