Moving and rewiring gates

Two changes of the gates of a fair semi-circuit that keep its parameters and the function it computes, as in Mishra and Santhanam, Sections 2.3 and 4.2:

• SemiCircuit.moveAffine: an affine gate reading no gates becomes an auxiliary variable, with its equation SemiCircuit.affEqn added to the affine system; this does not increase the degree of any parameter (SemiCircuit.deg_moveAffine_le);
• SemiCircuit.rewire: a gate is replaced by a gate reading only parameters that computes the same value whenever the other gates take their values.

Both preserve well-formedness, and every consistent assignment of the result is consistent for the original semi-circuit (SemiCircuit.MoveOK.liftsTo, SemiCircuit.RewireOK.liftsTo).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit.moveAffine, Cslib.Circuits.Boolean.SemiCircuit.rewire.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.WellFormed.moveAffine, Cslib.Circuits.Boolean.SemiCircuit.WellFormed.rewire: well-formedness is preserved.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits

Moving an affine gate into the affine system

def Cslib.Circuits.Boolean.SemiCircuit.moveAffine (C : SemiCircuit) (J e : ℕ) : SemiCircuit

Move the affine gate J into the affine system as the auxiliary variable J with the new equation e.

structure Cslib.Circuits.Boolean.SemiCircuit.MoveOK (C : SemiCircuit) (J e : ℕ) : Prop

The hypotheses of moving a gate into the affine system: J is an affine gate reading no gates and e is a fresh equation name.

• mem : J ∈ C.gates
• fresh : e ∉ C.eqns
• affine : IsAffineOp (C.gate J).op
• inputs (i : ℕ) : (C.gate J).Reads i → i ∉ C.gates

theorem Cslib.Circuits.Boolean.SemiCircuit.MoveOK.eqn_of_mem {C : SemiCircuit} {J e : ℕ} (h : C.MoveOK J e) {e' : ℕ} (he' : e' ∈ C.eqns) : (C.moveAffine J e).eqn e' = C.eqn e'

theorem Cslib.Circuits.Boolean.SemiCircuit.MoveOK.eqnsHold_iff {C : SemiCircuit} {J e : ℕ} (h : C.MoveOK J e) (val : ℕ → Bool) : (C.moveAffine J e).EqnsHold val ↔ C.EqnsHold val ∧ (affEqn (C.gate J) J).Holds val

The solutions of the new affine system are those of the old one on which the moved gate takes its value.

theorem Cslib.Circuits.Boolean.SemiCircuit.MoveOK.live_eq {C : SemiCircuit} {J e : ℕ} (h : C.MoveOK J e) : (C.moveAffine J e).live = C.live

theorem Cslib.Circuits.Boolean.SemiCircuit.MoveOK.mem_params_or_aux {C : SemiCircuit} (hC : C.WellFormed) {J e : ℕ} (h : C.MoveOK J e) {i : ℕ} (hi : (C.gate J).Reads i) : i ∈ C.params ∪ C.aux

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.moveAffine {C : SemiCircuit} (hC : C.WellFormed) {J e : ℕ} (h : C.MoveOK J e) : (C.moveAffine J e).WellFormed

Moving an affine gate reading no gates into the affine system preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.MoveOK.liftsTo {C : SemiCircuit} {J e : ℕ} (h : C.MoveOK J e) : (C.moveAffine J e).LiftsTo C

A consistent assignment after moving a gate into the affine system is consistent for the original semi-circuit.

theorem Cslib.Circuits.Boolean.SemiCircuit.deg_moveAffine_le {C : SemiCircuit} {J e : ℕ} (h : C.MoveOK J e) {z : ℕ} (hzJ : z ≠ J) : (C.moveAffine J e).deg z ≤ C.deg z

Moving a gate into the affine system does not increase the degree of any value other than the gate.

Rewiring a gate

def Cslib.Circuits.Boolean.SemiCircuit.rewire (C : SemiCircuit) (J : ℕ) (g : Gate) : SemiCircuit

Replace the gate J by the gate g.

structure Cslib.Circuits.Boolean.SemiCircuit.RewireOK (C : SemiCircuit) (J : ℕ) (g : Gate) : Prop

The hypotheses of rewiring: g reads only parameters and computes the value of J whenever all other gates take their values.

• mem : J ∈ C.gates
• reads (i : ℕ) : g.Reads i → i ∈ C.params
• value (val : ℕ → Bool) : (∀ K ∈ C.gates, K ≠ J → val K = (C.gate K).eval val) → g.eval val = (C.gate J).eval val

theorem Cslib.Circuits.Boolean.SemiCircuit.rewire_gate_of_ne {C : SemiCircuit} {J K : ℕ} {g : Gate} (hKJ : K ≠ J) : (C.rewire J g).gate K = C.gate K

theorem Cslib.Circuits.Boolean.SemiCircuit.rewire_gate_self {C : SemiCircuit} {J : ℕ} {g : Gate} : (C.rewire J g).gate J = g

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.rewire {C : SemiCircuit} (hC : C.WellFormed) {J : ℕ} {g : Gate} (h : C.RewireOK J g) : (C.rewire J g).WellFormed

Rewiring a gate to read only parameters preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.RewireOK.liftsTo {C : SemiCircuit} {J : ℕ} {g : Gate} (h : C.RewireOK J g) : (C.rewire J g).LiftsTo C

A consistent assignment of a rewired semi-circuit is consistent for the original one.