Exact gate-count padding

Our circuit representation designates its last gate as the output. To add any number of gates while retaining that convention, append copying OR gates, each reading the previous output twice. Every former output has fan-out two; the new output is terminal. This realizes the exact-size padding required by prop:explicit-padded-succinct-deciders, without a separate output-wire index.

def MIPRE.SAT.Circuit.copyOutput (C : Circuit) : Circuit

Append one gate copying the previous output.

Equations

• C.copyOutput = { inputs := C.inputs, gates := C.gates ++ [MIPRE.SAT.Gate.or (C.gates.length - 1) (C.gates.length - 1)] }

theorem MIPRE.SAT.Circuit.terminal_of_refsLt (C : Circuit) (h : C.RefsLt) : C.fanout (C.gates.length - 1) = 0

theorem MIPRE.SAT.Circuit.eval_copyOutput (C : Circuit) (hne : C.gates ≠ []) (x : ℕ → Bool) : C.copyOutput.eval x = C.eval x

A copying gate preserves the circuit's value.

theorem MIPRE.SAT.Circuit.wellFormed_copyOutput {C : Circuit} (hC : C.WellFormed) : C.copyOutput.WellFormed

A copying gate preserves topological order, fan-out two, and a terminal output.

def MIPRE.SAT.Circuit.padGates (C : Circuit) (k : ℕ) : Circuit

Append exactly k copying gates.

Equations

• C.padGates k = { inputs := C.inputs, gates := C.gates ++ List.map (fun (i : ℕ) => MIPRE.SAT.Gate.or i i) (List.range' (C.gates.length - 1) k) }

@[simp]

theorem MIPRE.SAT.Circuit.padGates_inputs (C : Circuit) (k : ℕ) : (C.padGates k).inputs = C.inputs

@[simp]

theorem MIPRE.SAT.Circuit.padGates_size (C : Circuit) (k : ℕ) : (C.padGates k).size = C.size + k

@[simp]

theorem MIPRE.SAT.Circuit.padGates_zero (C : Circuit) : C.padGates 0 = C

theorem MIPRE.SAT.Circuit.padGates_succ (C : Circuit) (hne : C.gates ≠ []) (k : ℕ) : C.padGates (k + 1) = (C.padGates k).copyOutput

theorem MIPRE.SAT.Circuit.wellFormed_padGates {C : Circuit} (hC : C.WellFormed) (k : ℕ) : (C.padGates k).WellFormed

Exact gate padding preserves well-formedness.

theorem MIPRE.SAT.Circuit.eval_padGates {C : Circuit} (hC : C.WellFormed) (k : ℕ) (x : ℕ → Bool) : (C.padGates k).eval x = C.eval x

Exact gate padding preserves the function on every input.

noncomputable def MIPRE.SAT.Circuit.partsProg : Cost.PolyTimeFun Circuit (ℕ × List Gate)

The pair representation of a circuit has the same encoding.

Equations

• MIPRE.SAT.Circuit.partsProg = MIPRE.Cost.PolyTimeFun.ofEncodeEq (fun (C : MIPRE.SAT.Circuit) => (C.inputs, C.gates)) MIPRE.SAT.Circuit.partsProg._proof_1

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

Construct exact gate padding in polynomial time in the original circuit and the number of padding gates, supplied in unary.

Equations

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

@[simp]

theorem MIPRE.SAT.Circuit.padGatesProg_apply (p : Circuit × Cost.Unary) : padGatesProg.toFun p = p.1.padGates (List.length p.2)