The fields of a literal, as programs

FieldsR ι is a record of readers: one program per field of FieldsF, all of them reading the same input ι. FieldsR.ev A i is the field record its programs produce on the input i, and it is a structure literal whose components are, definitionally, the values of those programs — so every formula built from a FieldsR matches the same formula built from FieldsR.ev by rfl, and the whole family of programs of FamilyProg.lean costs one rfl each.

litFieldsR is the record of programs for litFields: the one place where the constants of the layout have to be produced, and the only proof in the program layer that is not definitional (planning/succinct-cook-levin.md, S3).

Records of readers

structure MIPRE.TM.CookLevin.Desc.FieldsR (ι : Type u_2) [Cost.SizedEncoding ι] : Type u_2

A field record of programs, all reading the same input.

• flag : Cost.PolyTimeFun ι SAT.Fml
• tag : Cost.PolyTimeFun ι (List SAT.Fml)
• t : Cost.PolyTimeFun ι (List SAT.Fml)
• d : Cost.PolyTimeFun ι (List SAT.Fml)
• p : Cost.PolyTimeFun ι (List SAT.Fml)
• v : Cost.PolyTimeFun ι (List SAT.Fml)
• q : Cost.PolyTimeFun ι (List SAT.Fml)
• js : Fin 13 → Cost.PolyTimeFun ι (List SAT.Fml)
• g : Cost.PolyTimeFun ι (List SAT.Fml)
• ansOk : Cost.PolyTimeFun ι SAT.Fml

def MIPRE.TM.CookLevin.Desc.FieldsR.ev {ι : Type u_1} [Cost.SizedEncoding ι] (A : FieldsR ι) (i : ι) : FieldsF

The field record the programs produce on an input.

Equations

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

structure MIPRE.TM.CookLevin.Desc.CandR (ι : Type u_2) [Cost.SizedEncoding ι] : Type u_2

A candidate of programs.

• A₁ : FieldsR ι
• σ₁ : Cost.PolyTimeFun ι SAT.Fml
• A₂ : FieldsR ι
• σ₂ : Cost.PolyTimeFun ι SAT.Fml
• A₃ : FieldsR ι
• σ₃ : Cost.PolyTimeFun ι SAT.Fml

def MIPRE.TM.CookLevin.Desc.CandR.ev {ι : Type u_1} [Cost.SizedEncoding ι] (C : CandR ι) (i : ι) : CandF

The candidate the programs produce on an input.

Equations

• C.ev i = { A₁ := C.A₁.ev i, σ₁ := C.σ₁.toFun i, A₂ := C.A₂.ev i, σ₂ := C.σ₂.toFun i, A₃ := C.A₃.ev i, σ₃ := C.σ₃.toFun i }

The constants of the layout

theorem MIPRE.TM.CookLevin.Desc.cstR_zero {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (cstR w (bitsR 0)).toFun i = cst (List.length (w.toFun i)) 0

theorem MIPRE.TM.CookLevin.Desc.cstR_const {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (cstR w (bitsR k)).toFun i = cst (List.length (w.toFun i)) k

theorem MIPRE.TM.CookLevin.Desc.nbitsR_const {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (nbitsR w (bitsR k)).toFun i = nbits (List.length (w.toFun i)) k

noncomputable def MIPRE.TM.CookLevin.Desc.dblR {ι : Type u_1} [Cost.SizedEncoding ι] (T : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι Cost.BitStr

Twice a number, as a bit string.

Equations

• MIPRE.TM.CookLevin.Desc.dblR T = MIPRE.TM.CookLevin.Desc.dblP.ap₁ (MIPRE.Cost.PolyTimeFun.natBits.ap₁ T)

theorem MIPRE.TM.CookLevin.Desc.dblR_spec {ι : Type u_1} [Cost.SizedEncoding ι] (T : Cost.PolyTimeFun ι ℕ) (i : ι) (j : ℕ) : List.getD ((dblR T).toFun i) j false = (2 * T.toFun i).testBit j

noncomputable def MIPRE.TM.CookLevin.Desc.quadR {ι : Type u_1} [Cost.SizedEncoding ι] (T : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι Cost.BitStr

Four times a number, as a bit string.

Equations

• MIPRE.TM.CookLevin.Desc.quadR T = MIPRE.TM.CookLevin.Desc.dblP.ap₁ (MIPRE.TM.CookLevin.Desc.dblR T)

theorem MIPRE.TM.CookLevin.Desc.quadR_spec {ι : Type u_1} [Cost.SizedEncoding ι] (T : Cost.PolyTimeFun ι ℕ) (i : ι) (j : ℕ) : List.getD ((quadR T).toFun i) j false = (4 * T.toFun i).testBit j

The fields of a literal

noncomputable def MIPRE.TM.CookLevin.Desc.offR {ι : Type u_1} [Cost.SizedEncoding ι] (b o : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι ℕ

An index into a field, from an offset in unary.

Equations

• MIPRE.TM.CookLevin.Desc.offR b o = MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ (MIPRE.TM.CookLevin.Desc.addU.ap₂ b o)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.offR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (b o : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (offR b o).toFun i = List.length (b.toFun i) + List.length (o.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.flagR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι SAT.Fml

flagF.

Equations

• MIPRE.TM.CookLevin.Desc.flagR eu b = MIPRE.SAT.Fml.inpF.ap₁ (MIPRE.TM.CookLevin.Desc.offR b (MIPRE.TM.CookLevin.Desc.flagOffU eu))

theorem MIPRE.TM.CookLevin.Desc.flagR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (flagR eu b).toFun i = flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.jR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

jF.

Equations

• MIPRE.TM.CookLevin.Desc.jR eu b = MIPRE.SAT.fieldP.ap₂ (MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ b) (MIPRE.TM.CookLevin.Desc.flagOffU eu)

theorem MIPRE.TM.CookLevin.Desc.jR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (jR eu b).toFun i = jF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.twoTbR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι Cost.BitStr

twoTb.

Equations

• MIPRE.TM.CookLevin.Desc.twoTbR eu TR = MIPRE.TM.CookLevin.Desc.nbitsR (MIPRE.TM.CookLevin.Desc.flagOffU eu) (MIPRE.TM.CookLevin.Desc.dblR TR)

theorem MIPRE.TM.CookLevin.Desc.twoTbR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (i : ι) : (twoTbR eu TR).toFun i = twoTb (List.length (eu.toFun i)) Gc (TR.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.lt2TR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι SAT.Fml

lt2TF.

Equations

• MIPRE.TM.CookLevin.Desc.lt2TR eu TR b = MIPRE.SAT.ltConstP.ap₂ (MIPRE.TM.CookLevin.Desc.jR eu b) (MIPRE.TM.CookLevin.Desc.twoTbR eu TR)

theorem MIPRE.TM.CookLevin.Desc.lt2TR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (lt2TR eu TR b).toFun i = lt2TF (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.rR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

rF.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.rR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (rR eu TR b).toFun i = rF (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.pAnsR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

pAnsF.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.pAnsR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (pAnsR eu TR b).toFun i = pAnsF (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i))

The ten fields

noncomputable def MIPRE.TM.CookLevin.Desc.tagR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The tag field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.tagR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (tagR eu b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + tagOff) 3) (cst 3 0)

noncomputable def MIPRE.TM.CookLevin.Desc.tR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The t field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.tR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (tR eu b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + tOff) (W (List.length (eu.toFun i)))) (cst (W (List.length (eu.toFun i))) 0)

noncomputable def MIPRE.TM.CookLevin.Desc.dR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The d field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.dR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (dR eu TR b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + dOff (List.length (eu.toFun i))) 4) (muxList (lt2TF (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i))) (cst 4 5) (cst 4 6))

noncomputable def MIPRE.TM.CookLevin.Desc.pR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The p field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.pR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (pR eu TR b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + pOff (List.length (eu.toFun i))) (W (List.length (eu.toFun i)))) (pAnsF (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i)))

noncomputable def MIPRE.TM.CookLevin.Desc.vR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The v field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.vR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (vR eu TR b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + vOff (List.length (eu.toFun i))) 3) (muxList ((rF (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i))).headD (SAT.Fml.const false)) (cst 3 1) (cst 3 5))

noncomputable def MIPRE.TM.CookLevin.Desc.qR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The q field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.qR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (qR eu b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + qOff (List.length (eu.toFun i))) Qb) (cst Qb 0)

noncomputable def MIPRE.TM.CookLevin.Desc.jsR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) : Cost.PolyTimeFun ι (List SAT.Fml)

The js fields.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.jsR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (jsR eu b k).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + jsOff (List.length (eu.toFun i)) k) (W (List.length (eu.toFun i)))) (cst (W (List.length (eu.toFun i))) 0)

noncomputable def MIPRE.TM.CookLevin.Desc.gR {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The g field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.gR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (gR eu b).toFun i = muxList (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (SAT.Fml.field (List.length (b.toFun i) + gOff (List.length (eu.toFun i))) (Gb Gc)) (cst (Gb Gc) 0)

noncomputable def MIPRE.TM.CookLevin.Desc.ansOkR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι SAT.Fml

The ansOk field.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.ansOkR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (ansOkR eu TR b).toFun i = (flagF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))).not.and (SAT.Fml.ltConst (jF (List.length (eu.toFun i)) Gc (List.length (b.toFun i))) (nbits (flagOff (List.length (eu.toFun i)) Gc) (4 * TR.toFun i)))

noncomputable def MIPRE.TM.CookLevin.Desc.litFieldsR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) : FieldsR ι

The field programs of the literal with base b.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.litFieldsR_ev {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (litFieldsR eu TR b).ev i = litFields (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i))

The field programs are the field formulas: the record of programs for litFields produces litFields.