The fields of a literal, as formulas

For a literal whose m index bits are the input bits b .. b + m, the formulas computing its fields (litFields): the flag, the structured fields as slices of the input, and the answer decoding (j < 2T, r = j or j - 2T, p = r / 2 + 3, v from the parity of r), multiplexed by the flag. evalFields_litFields says that they compute exactly fieldsOf on the index (planning/succinct-cook-levin.md, S3).

Input slices

def MIPRE.TM.CookLevin.Desc.ibOf (b m : ℕ) (x : ℕ → Bool) : Cost.BitStr

The input bits b .. b + m as a bit string.

Equations

• MIPRE.TM.CookLevin.Desc.ibOf b m x = List.map x (List.range' b m)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_ibOf (b m : ℕ) (x : ℕ → Bool) : List.length (ibOf b m x) = m

theorem MIPRE.TM.CookLevin.Desc.range'_drop_take (s n off w : ℕ) (h : off + w ≤ n) : List.take w (List.drop off (List.range' s n)) = List.range' (s + off) w

theorem MIPRE.TM.CookLevin.Desc.bitsOf_field_ibOf (b m off w : ℕ) (h : off + w ≤ m) (x : ℕ → Bool) : SAT.Fml.bitsOf (SAT.Fml.field (b + off) w) x = List.take w (List.drop off (ibOf b m x))

theorem MIPRE.TM.CookLevin.Desc.val_field_ibOf (b m off w : ℕ) (h : off + w ≤ m) (x : ℕ → Bool) : SAT.Fml.val (SAT.Fml.field (b + off) w) x = bitField (ibOf b m x) off w

theorem MIPRE.TM.CookLevin.Desc.getD_ibOf (b m i : ℕ) (h : i < m) (x : ℕ → Bool) : List.getD (ibOf b m x) i false = x (b + i)

Multiplexed fields and constants

def MIPRE.TM.CookLevin.Desc.muxList (s : SAT.Fml) (as bs : List SAT.Fml) : List SAT.Fml

if s then as else bs, bitwise.

Equations

• MIPRE.TM.CookLevin.Desc.muxList s as bs = List.zipWith s.mux as bs

theorem MIPRE.TM.CookLevin.Desc.length_muxList (s : SAT.Fml) (as bs : List SAT.Fml) (h : as.length = bs.length) : (muxList s as bs).length = as.length

theorem MIPRE.TM.CookLevin.Desc.bitsOf_muxList (s : SAT.Fml) (as bs : List SAT.Fml) (h : as.length = bs.length) (x : ℕ → Bool) : SAT.Fml.bitsOf (muxList s as bs) x = if SAT.Fml.eval x s = true then SAT.Fml.bitsOf as x else SAT.Fml.bitsOf bs x

theorem MIPRE.TM.CookLevin.Desc.val_muxList (s : SAT.Fml) (as bs : List SAT.Fml) (h : as.length = bs.length) (x : ℕ → Bool) : SAT.Fml.val (muxList s as bs) x = if SAT.Fml.eval x s = true then SAT.Fml.val as x else SAT.Fml.val bs x

def MIPRE.TM.CookLevin.Desc.cst (w c : ℕ) : List SAT.Fml

The constant c on w bits.

Equations

• MIPRE.TM.CookLevin.Desc.cst w c = MIPRE.SAT.Fml.constBits (MIPRE.TM.CookLevin.Desc.nbits w c)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_cst (w c : ℕ) : (cst w c).length = w

theorem MIPRE.TM.CookLevin.Desc.val_cst (w c : ℕ) (x : ℕ → Bool) : SAT.Fml.val (cst w c) x = c % 2 ^ w

theorem MIPRE.TM.CookLevin.Desc.val_take (fs : List SAT.Fml) (w : ℕ) (x : ℕ → Bool) : SAT.Fml.val (List.take w fs) x = SAT.Fml.val fs x % 2 ^ w

theorem MIPRE.TM.CookLevin.Desc.val_tail (fs : List SAT.Fml) (x : ℕ → Bool) : SAT.Fml.val fs.tail x = SAT.Fml.val fs x / 2

theorem MIPRE.TM.CookLevin.Desc.headD_eval_toNat (fs : List SAT.Fml) (x : ℕ → Bool) (hne : fs ≠ []) : (SAT.Fml.eval x (fs.headD (SAT.Fml.const false))).toNat = SAT.Fml.val fs x % 2

The fields of a literal

structure MIPRE.TM.CookLevin.Desc.FieldsF : Type

The fields of a literal as formulas.

• flag : SAT.Fml
• tag : List SAT.Fml
• t : List SAT.Fml
• d : List SAT.Fml
• p : List SAT.Fml
• v : List SAT.Fml
• q : List SAT.Fml
• js : Fin 13 → List SAT.Fml
• g : List SAT.Fml
• ansOk : SAT.Fml

def MIPRE.TM.CookLevin.Desc.evalFields (F : FieldsF) (x : ℕ → Bool) : Fields

The values of the field formulas.

Equations

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

def MIPRE.TM.CookLevin.Desc.flagF (e G b : ℕ) : SAT.Fml

The flag bit.

Equations

• MIPRE.TM.CookLevin.Desc.flagF e G b = MIPRE.SAT.Fml.inp (b + MIPRE.TM.CookLevin.Desc.flagOff e G)

def MIPRE.TM.CookLevin.Desc.jF (e G b : ℕ) : List SAT.Fml

The low m - 1 bits, the value j of an answer index.

Equations

• MIPRE.TM.CookLevin.Desc.jF e G b = MIPRE.SAT.Fml.field b (MIPRE.TM.CookLevin.Desc.flagOff e G)

def MIPRE.TM.CookLevin.Desc.twoTb (e G T : ℕ) : Cost.BitStr

2T on m - 1 bits.

Equations

• MIPRE.TM.CookLevin.Desc.twoTb e G T = MIPRE.TM.CookLevin.Desc.nbits (MIPRE.TM.CookLevin.Desc.flagOff e G) (2 * T)

def MIPRE.TM.CookLevin.Desc.lt2TF (e G T b : ℕ) : SAT.Fml

j < 2T.

Equations

• MIPRE.TM.CookLevin.Desc.lt2TF e G T b = MIPRE.SAT.Fml.ltConst (MIPRE.TM.CookLevin.Desc.jF e G b) (MIPRE.TM.CookLevin.Desc.twoTb e G T)

def MIPRE.TM.CookLevin.Desc.rF (e G T b : ℕ) : List SAT.Fml

r = j or j - 2T.

Equations

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

def MIPRE.TM.CookLevin.Desc.pAnsF (e G T b : ℕ) : List SAT.Fml

p = r / 2 + 3, on W bits.

Equations

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

def MIPRE.TM.CookLevin.Desc.litFields (e G T b : ℕ) : FieldsF

The field formulas of the literal with base b.

Equations

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

Lengths

theorem MIPRE.TM.CookLevin.Desc.W_le_flagOff (e G : ℕ) : W e + 1 ≤ flagOff e G

theorem MIPRE.TM.CookLevin.Desc.length_jF (e G b : ℕ) : (jF e G b).length = flagOff e G

theorem MIPRE.TM.CookLevin.Desc.length_rF (e G T b : ℕ) : (rF e G T b).length = flagOff e G

theorem MIPRE.TM.CookLevin.Desc.length_pAnsF (e G T b : ℕ) : (pAnsF e G T b).length = W e

Values

theorem MIPRE.TM.CookLevin.Desc.eval_flagF (e G b : ℕ) (x : ℕ → Bool) : SAT.Fml.eval x (flagF e G b) = List.getD (ibOf b (mOf e G) x) (flagOff e G) false

theorem MIPRE.TM.CookLevin.Desc.val_jF (e G b : ℕ) (x : ℕ → Bool) : SAT.Fml.val (jF e G b) x = bitField (ibOf b (mOf e G) x) 0 (flagOff e G)

theorem MIPRE.TM.CookLevin.Desc.fourT_lt (e G T : ℕ) (hT : T ≤ Sof e) : 4 * T < 2 ^ flagOff e G

The answer bound: 4T < 2^{m-1}, from T ≤ S.

theorem MIPRE.TM.CookLevin.Desc.eval_lt2TF (e G T b : ℕ) (x : ℕ → Bool) (hT : T ≤ Sof e) : SAT.Fml.eval x (lt2TF e G T b) = true ↔ bitField (ibOf b (mOf e G) x) 0 (flagOff e G) < 2 * T

theorem MIPRE.TM.CookLevin.Desc.val_rF (e G T b : ℕ) (x : ℕ → Bool) (hT : T ≤ Sof e) : SAT.Fml.val (rF e G T b) x = if bitField (ibOf b (mOf e G) x) 0 (flagOff e G) < 2 * T then bitField (ibOf b (mOf e G) x) 0 (flagOff e G) else bitField (ibOf b (mOf e G) x) 0 (flagOff e G) - 2 * T

theorem MIPRE.TM.CookLevin.Desc.val_pAnsF (e G T b : ℕ) (x : ℕ → Bool) (hT : T ≤ Sof e) : SAT.Fml.val (pAnsF e G T b) x = ((if bitField (ibOf b (mOf e G) x) 0 (flagOff e G) < 2 * T then bitField (ibOf b (mOf e G) x) 0 (flagOff e G) else bitField (ibOf b (mOf e G) x) 0 (flagOff e G) - 2 * T) / 2 + 3) % 2 ^ W e

theorem MIPRE.TM.CookLevin.Desc.eval_ansOkF (e G T b : ℕ) (x : ℕ → Bool) (hT : T ≤ Sof e) : SAT.Fml.eval x ((flagF e G b).not.and (SAT.Fml.ltConst (jF e G b) (nbits (flagOff e G) (4 * T)))) = (!SAT.Fml.eval x (flagF e G b) && decide (bitField (ibOf b (mOf e G) x) 0 (flagOff e G) < 4 * T))

theorem MIPRE.TM.CookLevin.Desc.length_dAns (e G T b : ℕ) : (muxList (lt2TF e G T b) (cst 4 5) (cst 4 6)).length = 4

theorem MIPRE.TM.CookLevin.Desc.length_vAns (e G T b : ℕ) : (muxList ((rF e G T b).headD (SAT.Fml.const false)) (cst 3 1) (cst 3 5)).length = 3

theorem MIPRE.TM.CookLevin.Desc.evalFields_litFields (e G T b : ℕ) (x : ℕ → Bool) (hT : T ≤ Sof e) : evalFields (litFields e G T b) x = fieldsOf e G T (ibOf b (mOf e G) x)

The field formulas compute the fields of the index.