Padding a circuit to an exact gate count

A circuit with at most s gates is padded to exactly s gates by copying gates (Circuit.padGates); a larger one is replaced by a trivial circuit of s gates with the same inputs, so that the gate count is s on every input (Circuit.padTo). On the circuits that fit, padding preserves well-formedness, the function computed, the formula the circuit describes, and the succinct description of a decider through three windows (describesWindows_padTo); the padding is computed in polynomial time from the circuit and s in unary (padToProg). The answer reduction's circuit function pads the window describer's circuits to its gate bound (slice P4i).

def MIPRE.SAT.Circuit.trivial (i : ℕ) : Circuit

The trivial circuit on i inputs: one constant gate.

Equations

• MIPRE.SAT.Circuit.trivial i = { inputs := i, gates := [MIPRE.SAT.Gate.const false] }

theorem MIPRE.SAT.Circuit.wellFormed_trivial (i : ℕ) : (trivial i).WellFormed

def MIPRE.SAT.Circuit.padTo (C : Circuit) (s : ℕ) : Circuit

A circuit padded to exactly s gates: copying gates when it has at most s, else the trivial circuit padded.

Equations

• C.padTo s = if C.size ≤ s then C.padGates (s - C.size) else (MIPRE.SAT.Circuit.trivial C.inputs).padGates (s - 1)

@[simp]

theorem MIPRE.SAT.Circuit.padTo_inputs (C : Circuit) (s : ℕ) : (C.padTo s).inputs = C.inputs

theorem MIPRE.SAT.Circuit.padTo_size (C : Circuit) {s : ℕ} (hs : 1 ≤ s) : (C.padTo s).size = s

theorem MIPRE.SAT.Circuit.wellFormed_padTo {C : Circuit} (hC : C.WellFormed) (s : ℕ) : (C.padTo s).WellFormed

theorem MIPRE.SAT.Circuit.padTo_of_le (C : Circuit) {s : ℕ} (h : C.size ≤ s) : C.padTo s = C.padGates (s - C.size)

theorem MIPRE.SAT.Circuit.evalBits_padTo {C : Circuit} (hC : C.WellFormed) {s : ℕ} (h : C.size ≤ s) (l : List Bool) : (C.padTo s).evalBits l = C.evalBits l

theorem MIPRE.SAT.Circuit.formula6_padTo {C : Circuit} (hC : C.WellFormed) {s : ℕ} (h : C.size ≤ s) (ℓa ℓb ℓc r : ℕ) : (C.padTo s).formula6 ℓa ℓb ℓc r = C.formula6 ℓa ℓb ℓc r

theorem MIPRE.SAT.Circuit.describesWindows_padTo {C : Circuit} (hC : C.WellFormed) {s : ℕ} (h : C.size ≤ s) {ℓa ℓb ℓc r : ℕ} {D : Decider} {n : ℕ} {x y : Cost.BitStr} {T : ℕ} (hD : C.DescribesWindows ℓa ℓb ℓc r D n x y T) : (C.padTo s).DescribesWindows ℓa ℓb ℓc r D n x y T

Padding preserves a description through three windows.

noncomputable def MIPRE.SAT.Circuit.trivialProg : Cost.PolyTimeFun ℕ Circuit

The trivial circuit, from the input count.

Equations

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

@[simp]

theorem MIPRE.SAT.Circuit.trivialProg_apply (i : ℕ) : trivialProg.toFun i = trivial i

noncomputable def MIPRE.SAT.Circuit.padToProg : Cost.PolyTimeFun (Circuit × Cost.Unary) Circuit

Exact padding in polynomial time, from the circuit and s in unary.

Equations

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

@[simp]

theorem MIPRE.SAT.Circuit.padToProg_apply (C : Circuit) (u : Cost.Unary) : padToProg.toFun (C, u) = C.padTo (List.length u)