Documentation

MIPRE.TM.CookLevin.Link

The link clauses of the decoupled describer #

Rows 2 to 9 of the paper's circuit (prop:explicit-succinct-deciders): the clause families that tie the two answer blocks a, b of a decoupled 5SAT instance to the first 4T variables of the three auxiliary blocks, pin the padding of a and b above 2T, and force the three auxiliary blocks to agree.

Link is the disjunction of the eight conditions on a decoded clause and linkFml the formula that decides it on the 2ℓ + 3r + 5 input bits, with eval_linkFml their equivalence. Every comparison is made at width r, with the two ℓ-bit answer indices zero-padded: at width ℓ the constant 2T is not representable when T is a power of two, since then 2T = 2 ^ ℓ exactly (planning/decoupled-5sat.md, A1b).

The parities of rows 4 to 7 are a repair of the verification campaign. Blocks are 0-indexed and the blank encodes as 10, so the honest padding starts at the even index 2T and puts 1 at even indices and 0 at odd ones. The pre-repair text had it the other way round, which is violated by the honest assignment and breaks completeness. Our tapeBits past the end of a string is the blank cell, hence true at even and false at odd positions, so it agrees with the repaired parity.

The input layout #

def MIPRE.TM.CookLevin.Desc.sgOff (ℓ r : ℕ) :

The offset of the five signs.

Equations

MIPRE.TM.CookLevin.Desc.sgOff ℓ r = 2 * ℓ + 3 * r

Instances For

def MIPRE.TM.CookLevin.Desc.j₁F (ℓ r : ℕ) :

The two answer indices, zero-padded to r bits, and the three auxiliary indices.

Equations

MIPRE.TM.CookLevin.Desc.j₁F ℓ r = MIPRE.SAT.Fml.padTo r (MIPRE.SAT.Fml.field 0 ℓ)

Instances For

def MIPRE.TM.CookLevin.Desc.j₂F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.j₂F ℓ r = MIPRE.SAT.Fml.padTo r (MIPRE.SAT.Fml.field ℓ ℓ)

Instances For

def MIPRE.TM.CookLevin.Desc.j₃F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.j₃F ℓ r = MIPRE.SAT.Fml.field (2 * ℓ) r

Instances For

def MIPRE.TM.CookLevin.Desc.j₄F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.j₄F ℓ r = MIPRE.SAT.Fml.field (2 * ℓ + r) r

Instances For

def MIPRE.TM.CookLevin.Desc.j₅F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.j₅F ℓ r = MIPRE.SAT.Fml.field (2 * ℓ + 2 * r) r

Instances For

def MIPRE.TM.CookLevin.Desc.s₁F (ℓ r : ℕ) :

The five signs.

Equations

MIPRE.TM.CookLevin.Desc.s₁F ℓ r = MIPRE.SAT.Fml.inp (MIPRE.TM.CookLevin.Desc.sgOff ℓ r)

Instances For

def MIPRE.TM.CookLevin.Desc.s₂F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.s₂F ℓ r = MIPRE.SAT.Fml.inp (MIPRE.TM.CookLevin.Desc.sgOff ℓ r + 1)

Instances For

def MIPRE.TM.CookLevin.Desc.s₃F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.s₃F ℓ r = MIPRE.SAT.Fml.inp (MIPRE.TM.CookLevin.Desc.sgOff ℓ r + 2)

Instances For

def MIPRE.TM.CookLevin.Desc.s₄F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.s₄F ℓ r = MIPRE.SAT.Fml.inp (MIPRE.TM.CookLevin.Desc.sgOff ℓ r + 3)

Instances For

def MIPRE.TM.CookLevin.Desc.s₅F (ℓ r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.s₅F ℓ r = MIPRE.SAT.Fml.inp (MIPRE.TM.CookLevin.Desc.sgOff ℓ r + 4)

Instances For

theorem MIPRE.TM.CookLevin.Desc.length_j₁F (ℓ r : ℕ) (h : ℓ ≤ r) :

(j₁F ℓ r).length = r

theorem MIPRE.TM.CookLevin.Desc.length_j₂F (ℓ r : ℕ) (h : ℓ ≤ r) :

(j₂F ℓ r).length = r

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_j₃F (ℓ r : ℕ) :

(j₃F ℓ r).length = r

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_j₄F (ℓ r : ℕ) :

(j₄F ℓ r).length = r

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_j₅F (ℓ r : ℕ) :

(j₅F ℓ r).length = r

The eight conditions #

def MIPRE.TM.CookLevin.Desc.Link (ℓ r T : ℕ) (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

The link conditions on a decoupled clause: rows 2 to 9 of the paper's circuit.

Equations

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

Instances For

def MIPRE.TM.CookLevin.Desc.linkFml (ℓ r T : ℕ) :

The formula deciding Link on the 2ℓ + 3r + 5 input bits.

Equations

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

Instances For

theorem MIPRE.TM.CookLevin.Desc.InputsLt.linkFml (ℓ r T : ℕ) (h : ℓ ≤ r) :

SAT.Fml.InputsLt (2 * ℓ + 3 * r + 5) (Desc.linkFml ℓ r T)

The slices of a clause's input #

def MIPRE.TM.CookLevin.Desc.sgList {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

The five signs, as a list.

Equations

MIPRE.TM.CookLevin.Desc.sgList c = [c.l₁.pos, c.l₂.pos, c.l₃.pos, c.l₄.pos, c.l₅.pos]

Instances For

theorem MIPRE.TM.CookLevin.Desc.clauseInput5_eq {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

SAT.clauseInput5 ℓ r c = SAT.bitsOfNat ℓ ↑c.l₁.var ++ (SAT.bitsOfNat ℓ ↑c.l₂.var ++ (SAT.bitsOfNat r ↑c.l₃.var ++ (SAT.bitsOfNat r ↑c.l₄.var ++ (SAT.bitsOfNat r ↑c.l₅.var ++ sgList c))))

theorem MIPRE.TM.CookLevin.Desc.drop_two {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

List.drop (2 * ℓ) (SAT.clauseInput5 ℓ r c) = SAT.bitsOfNat r ↑c.l₃.var ++ (SAT.bitsOfNat r ↑c.l₄.var ++ (SAT.bitsOfNat r ↑c.l₅.var ++ sgList c))

theorem MIPRE.TM.CookLevin.Desc.drop_three {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

List.drop (2 * ℓ + r) (SAT.clauseInput5 ℓ r c) = SAT.bitsOfNat r ↑c.l₄.var ++ (SAT.bitsOfNat r ↑c.l₅.var ++ sgList c)

theorem MIPRE.TM.CookLevin.Desc.drop_four {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

List.drop (2 * ℓ + 2 * r) (SAT.clauseInput5 ℓ r c) = SAT.bitsOfNat r ↑c.l₅.var ++ sgList c

theorem MIPRE.TM.CookLevin.Desc.drop_signs {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

List.drop (sgOff ℓ r) (SAT.clauseInput5 ℓ r c) = sgList c

theorem MIPRE.TM.CookLevin.Desc.val_j₁F {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

(SAT.Fml.val (j₁F ℓ r) fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) = ↑c.l₁.var

theorem MIPRE.TM.CookLevin.Desc.val_j₂F {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

(SAT.Fml.val (j₂F ℓ r) fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) = ↑c.l₂.var

theorem MIPRE.TM.CookLevin.Desc.val_j₃F {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

(SAT.Fml.val (j₃F ℓ r) fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) = ↑c.l₃.var

theorem MIPRE.TM.CookLevin.Desc.val_j₄F {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

(SAT.Fml.val (j₄F ℓ r) fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) = ↑c.l₄.var

theorem MIPRE.TM.CookLevin.Desc.val_j₅F {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

(SAT.Fml.val (j₅F ℓ r) fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) = ↑c.l₅.var

theorem MIPRE.TM.CookLevin.Desc.eval_sgF {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) (k : ℕ) :

SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) (SAT.Fml.inp (sgOff ℓ r + k)) = List.getD (sgList c) k false

The formula decides the conditions #

theorem MIPRE.TM.CookLevin.Desc.eval_xor_iff (f g : SAT.Fml) (x : ℕ → Bool) :

SAT.Fml.eval x (f.xor g) = true ↔ SAT.Fml.eval x f ≠ SAT.Fml.eval x g

theorem MIPRE.TM.CookLevin.Desc.eval_headD_iff {fs : List SAT.Fml} (hne : fs ≠ []) (x : ℕ → Bool) :

SAT.Fml.eval x (fs.headD (SAT.Fml.const false)) = true ↔ ¬SAT.Fml.val fs x % 2 = 0

theorem MIPRE.TM.CookLevin.Desc.eval_linkFml {ℓ r T : ℕ} (hℓr : ℓ ≤ r) (hr : 1 ≤ r) (hT : 2 * T < 2 ^ r) (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) :

SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) (linkFml ℓ r T) = true ↔ Link ℓ r T c

The link formula decides the link conditions.