Fair semi-circuits over the full binary basis

Following Mishra and Santhanam, Section 2.3, a fair semi-circuit is an affine system of equations over 𝔽₂ followed by an acyclic circuit over the full binary basis B₂. Its internal values are parameters, auxiliary variables and gates, all named by natural numbers. The affine system consists of equations ∑ terms = rhs in the parameters and auxiliary variables, each with at most three terms; it is fair when every assignment to the parameters extends to exactly one assignment of the auxiliary variables satisfying all equations (SemiCircuit.WellFormed.solvable, SemiCircuit.WellFormed.unique), which is equivalent to the invertibility of the auxiliary matrix of the source. Each gate applies an arbitrary operation Bool → Bool → Bool to two arguments, each a constant or an internal value with a smaller name, so the order of names is a topological order. The output is a literal.

Equations are named separately from internal values. A child of an internal value t is a gate reading t or an equation containing t (SemiCircuit.children); a gate reading t twice is a single child. The degree of t is its number of children (SemiCircuit.deg).

Rerouting replaces every occurrence of an internal value v by a literal (SemiCircuit.subst), absorbing negations into the operations of gates and the right-hand sides of equations. It preserves the value of every gate and the truth of every equation on assignments giving v the value of the literal (Gate.eval_subst, Equation.holds_subst), and it changes no child of any value other than v and the target of the literal (SemiCircuit.children_subst).

A gate with a constant argument or two equal arguments is degenerate and computes a constant or a literal of an argument (Gate.eval_lit). Of the sixteen operations of B₂, the affine ones (IsAffineOp) have no product term; every other operation has the form (a + α)(b + β) + γ (exists_and_form). An affine gate whose arguments are parameters or auxiliary variables can be moved into the affine system as an equation (affEqn_holds).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit: semi-circuits, with SemiCircuit.Consistent assignments, SemiCircuit.WellFormed, SemiCircuit.children, SemiCircuit.deg and SemiCircuit.size (building on SemiCircuit.Lit, SemiCircuit.Gate and SemiCircuit.IsAffineOp in Complexity/Computability/Circuit/Boolean/SemiCircuit/Gate.lean, and SemiCircuit.Equation in Complexity/Computability/Circuit/Boolean/SemiCircuit/Equation.lean).
• Cslib.Circuits.Boolean.SemiCircuit.subst: rerouting an internal value to a literal.
• Cslib.Circuits.Boolean.SemiCircuit.AffineIn, Cslib.Circuits.Boolean.SemiCircuit.LiftsTo: affine dependence on the parameters and lifting consistent assignments.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.consistent_subst, Cslib.Circuits.Boolean.SemiCircuit.consistent_of_subst: rerouting preserves consistency.
• Cslib.Circuits.Boolean.SemiCircuit.children_subst: rerouting changes no other children.
• Cslib.Circuits.Boolean.SemiCircuit.WellFormed.exists_affineIn: on the solutions of the affine system, every auxiliary variable is an affine function of the parameters.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits
• M. G. Find, A. Golovnev, E. A. Hirsch and A. S. Kulikov, A better-than-3n lower bound for the circuit complexity of an explicit function

Semi-circuits

structure Cslib.Circuits.Boolean.SemiCircuit : Type

A semi-circuit: parameters, auxiliary variables and gates named by natural numbers, the gates and the equations of the affine system, and an output literal. Only the gates in gates and the equations in eqns belong to the semi-circuit; gate and eqn are arbitrary elsewhere.

• params : Finset ℕ

  The parameters.

• aux : Finset ℕ

  The auxiliary variables of the affine system.

• gates : Finset ℕ

  The gates of the acyclic part.

• gate : ℕ → Gate

  The gate with each name.

• eqns : Finset ℕ

  The names of the equations of the affine system.

• eqn : ℕ → Equation

  The equation with each name.

• out : Lit

  The output.

def Cslib.Circuits.Boolean.SemiCircuit.live (C : SemiCircuit) : Finset ℕ

The internal values: parameters, auxiliary variables and gates.

def Cslib.Circuits.Boolean.SemiCircuit.EqnsHold (C : SemiCircuit) (val : ℕ → Bool) : Prop

All equations of the affine system hold.

def Cslib.Circuits.Boolean.SemiCircuit.GatesHold (C : SemiCircuit) (val : ℕ → Bool) : Prop

Every gate has the value of its operation on its arguments.

def Cslib.Circuits.Boolean.SemiCircuit.Consistent (C : SemiCircuit) (val : ℕ → Bool) : Prop

A consistent assignment of the internal values satisfies every equation and every gate.

def Cslib.Circuits.Boolean.SemiCircuit.size (C : SemiCircuit) : ℕ

The size: the number of gates plus the number of equations.

def Cslib.Circuits.Boolean.SemiCircuit.gateChildren (C : SemiCircuit) (t : ℕ) : Finset ℕ

The gates reading t.

def Cslib.Circuits.Boolean.SemiCircuit.eqnChildren (C : SemiCircuit) (t : ℕ) : Finset ℕ

The equations containing t.

def Cslib.Circuits.Boolean.SemiCircuit.children (C : SemiCircuit) (t : ℕ) : Finset (ℕ ⊕ ℕ)

The children of t: the gates reading it (on the left) and the equations containing it (on the right).

def Cslib.Circuits.Boolean.SemiCircuit.deg (C : SemiCircuit) (t : ℕ) : ℕ

The degree of t: its number of children.

theorem Cslib.Circuits.Boolean.SemiCircuit.deg_eq (C : SemiCircuit) (t : ℕ) : C.deg t = (C.gateChildren t).card + (C.eqnChildren t).card

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.inl_mem_children (C : SemiCircuit) {t J : ℕ} : Sum.inl J ∈ C.children t ↔ J ∈ C.gates ∧ (C.gate J).Reads t

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.inr_mem_children (C : SemiCircuit) {t e : ℕ} : Sum.inr e ∈ C.children t ↔ e ∈ C.eqns ∧ t ∈ (C.eqn e).terms

structure Cslib.Circuits.Boolean.SemiCircuit.WellFormed (C : SemiCircuit) : Prop

A semi-circuit is well formed when its roles are disjoint, gates read constants or internal values (gates only with smaller names), equations have at most three terms among the parameters and auxiliary variables, the output reads a constant or an internal value, and the affine system is fair: every assignment of the parameters extends to a solution, whose auxiliary values are unique.

• disjoint_params_aux : Disjoint C.params C.aux

  Parameters and auxiliary variables are distinct.

• disjoint_params_gates : Disjoint C.params C.gates

  Parameters and gates are distinct.

• disjoint_aux_gates : Disjoint C.aux C.gates

  Auxiliary variables and gates are distinct.

• reads_lt (J : ℕ) : J ∈ C.gates → ∀ i ∈ C.gates, (C.gate J).Reads i → i < J

  A gate reads only gates with smaller names.

• reads_live (J : ℕ) : J ∈ C.gates → ∀ (i : ℕ), (C.gate J).Reads i → i ∈ C.live

  A gate reads only constants and internal values.

• terms_subset (e : ℕ) : e ∈ C.eqns → (C.eqn e).terms ⊆ C.params ∪ C.aux

  Equations contain only parameters and auxiliary variables.

• card_terms_le (e : ℕ) : e ∈ C.eqns → (C.eqn e).terms.card ≤ 3

  Every equation has at most three terms.

• out_live (i : ℕ) : C.out.arg = Arg.node i → i ∈ C.live

  The output reads a constant or an internal value.

• solvable (u : ℕ → Bool) : ∃ (val : ℕ → Bool), (∀ j ∈ C.params, val j = u j) ∧ C.EqnsHold val

  Every assignment of the parameters extends to a solution of the affine system.

• unique (val val' : ℕ → Bool) : (∀ j ∈ C.params, val j = val' j) → C.EqnsHold val → C.EqnsHold val' → ∀ v ∈ C.aux, val v = val' v

  The solution determines the auxiliary variables (fairness).

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_gates_of_mem_params {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.params) : i ∉ C.gates

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_aux_of_mem_params {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.params) : i ∉ C.aux

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_params_of_mem_gates {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.gates) : i ∉ C.params

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_aux_of_mem_gates {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.gates) : i ∉ C.aux

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_params_of_mem_aux {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.aux) : i ∉ C.params

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_gates_of_mem_aux {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.aux) : i ∉ C.gates

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.notMem_terms_of_mem_gates {C : SemiCircuit} (hC : C.WellFormed) {i e : ℕ} (hi : i ∈ C.gates) (he : e ∈ C.eqns) : i ∉ (C.eqn e).terms

Gates do not occur in equations.

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.not_reads_self {C : SemiCircuit} (hC : C.WellFormed) {i : ℕ} (hi : i ∈ C.gates) : ¬(C.gate i).Reads i

A gate does not read itself.

Rerouting

def Cslib.Circuits.Boolean.SemiCircuit.subst (C : SemiCircuit) (v : ℕ) (ℓ : Lit) : SemiCircuit

Reroute the internal value v to the literal ℓ in every gate, equation and the output.

theorem Cslib.Circuits.Boolean.SemiCircuit.eqnsHold_subst {C : SemiCircuit} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (C.subst v ℓ).EqnsHold val ↔ C.EqnsHold val

theorem Cslib.Circuits.Boolean.SemiCircuit.gatesHold_subst {C : SemiCircuit} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (C.subst v ℓ).GatesHold val ↔ C.GatesHold val

theorem Cslib.Circuits.Boolean.SemiCircuit.consistent_subst {C : SemiCircuit} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (C.subst v ℓ).Consistent val ↔ C.Consistent val

theorem Cslib.Circuits.Boolean.SemiCircuit.children_subst {C : SemiCircuit} {v : ℕ} {ℓ : Lit} {z : ℕ} (hzv : z ≠ v) (hzℓ : ℓ.arg ≠ Arg.node z) : (C.subst v ℓ).children z = C.children z

Rerouting v changes no child of any internal value other than v and the target of the literal.

theorem Cslib.Circuits.Boolean.SemiCircuit.children_subst_subset {C : SemiCircuit} (v : ℕ) (ℓ : Lit) (z : ℕ) : (C.subst v ℓ).children z ⊆ C.children z ∪ C.children v

After rerouting v to t, the children of t are among the former children of t and v.

theorem Cslib.Circuits.Boolean.SemiCircuit.size_subst {C : SemiCircuit} (v : ℕ) (ℓ : Lit) : (C.subst v ℓ).size = C.size

Solutions of the affine system

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.holds_add_add {E : Equation} {val val' val'' : ℕ → Bool} (h : E.Holds val) (h' : E.Holds val') (h'' : E.Holds val'') : E.Holds (val + val' + val'')

theorem Cslib.Circuits.Boolean.SemiCircuit.eqnsHold_add_add {C : SemiCircuit} {val val' val'' : ℕ → Bool} (h : C.EqnsHold val) (h' : C.EqnsHold val') (h'' : C.EqnsHold val'') : C.EqnsHold (val + val' + val'')

theorem Cslib.Circuits.Boolean.SemiCircuit.eqnsHold_congr {C : SemiCircuit} {val val' : ℕ → Bool} (hC : C.WellFormed) (h : ∀ i ∈ C.params ∪ C.aux, val i = val' i) : C.EqnsHold val ↔ C.EqnsHold val'

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.exists_consistent {C : SemiCircuit} (hC : C.WellFormed) (u : ℕ → Bool) : ∃ (val : ℕ → Bool), (∀ j ∈ C.params, val j = u j) ∧ C.Consistent val

Every assignment of the parameters of a well-formed semi-circuit extends to a consistent assignment of all internal values: solve the affine system, then evaluate the gates in the order of their names.

def Cslib.Circuits.Boolean.SemiCircuit.AffineIn {C : SemiCircuit} (t : ℕ) (c : Bool) (T : Finset ℕ) : Prop

On the solutions of the affine system, the internal value t is the affine function c + ∑ j ∈ T, u j of the parameters u.

theorem Cslib.Circuits.Boolean.SemiCircuit.affineIn_param {C : SemiCircuit} {x : ℕ} (hx : x ∈ C.params) : AffineIn x false {x}

Every parameter is an affine function of the parameters.

theorem Cslib.Circuits.Boolean.SemiCircuit.AffineIn.unique {C : SemiCircuit} (hC : C.WellFormed) {t : ℕ} {c c' : Bool} {T T' : Finset ℕ} (h : AffineIn t c T) (h' : AffineIn t c' T') : c = c' ∧ T = T'

The affine expression of an internal value in the parameters is unique.

Affine functions of finitely many bits

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_affine_of_add_add {M : Finset ℕ} {g : (ℕ → Bool) → Bool} (hcongr : ∀ (u u' : ℕ → Bool), (∀ j ∈ M, u j = u' j) → g u = g u') (hadd : ∀ (u u' u'' : ℕ → Bool), g (u + u' + u'') = g u + g u' + g u'') : ∃ T ⊆ M, ∀ (u : ℕ → Bool), g u = g 0 + ∑ j ∈ T, u j

A function of bits that depends only on the coordinates in M and preserves sums of three points is affine: a constant plus the sum of the coordinates in some T ⊆ M.

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.exists_affineIn {C : SemiCircuit} (hC : C.WellFormed) {v : ℕ} (hv : v ∈ C.aux) : ∃ (c : Bool) (T : Finset ℕ), AffineIn v c T

Every auxiliary variable of a well-formed semi-circuit is an affine function of the parameters on the solutions of the affine system.

theorem Cslib.Circuits.Boolean.SemiCircuit.AffineIn.mem_terms {C : SemiCircuit} {t : ℕ} {c : Bool} {T : Finset ℕ} (hC : C.WellFormed) (h : AffineIn t c T) (ht : t ∉ C.params) {x : ℕ} (hx : x ∈ T) : ∃ e ∈ C.eqns, x ∈ (C.eqn e).terms

An auxiliary variable can depend only on parameters occurring in the affine system.

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_affineIn_of_mem_terms {C : SemiCircuit} (hC : C.WellFormed) {x e : ℕ} (hx : x ∈ C.params) (he : e ∈ C.eqns) (hxe : x ∈ (C.eqn e).terms) : ∃ Q ∈ C.aux, ∃ (c : Bool) (T : Finset ℕ), AffineIn Q c T ∧ x ∈ T

A parameter occurring in the affine system is a summand of some auxiliary variable.

Changing unread values

theorem Cslib.Circuits.Boolean.SemiCircuit.consistent_update_iff {C : SemiCircuit} {x : ℕ} (hxg : x ∉ C.gates) (hgate : ∀ J ∈ C.gates, ¬(C.gate J).Reads x) (heqn : ∀ e ∈ C.eqns, x ∉ (C.eqn e).terms) (val : ℕ → Bool) (b : Bool) : C.Consistent (Function.update val x b) ↔ C.Consistent val

Changing the value of a name that no gate or equation reads and that is not a gate keeps consistency.

theorem Cslib.Circuits.Boolean.SemiCircuit.consistent_of_subst {C : SemiCircuit} {x : ℕ} {ℓ : Lit} (hxg : x ∉ C.gates) (hℓ : ℓ.arg ≠ Arg.node x) {val : ℕ → Bool} (h : (C.subst x ℓ).Consistent val) : C.Consistent (Function.update val x (ℓ.eval val))

After rerouting x, which is not a gate, to a literal not reading it, a consistent assignment gives a consistent assignment of the original semi-circuit once x takes the value of the literal.

Lifting consistent assignments

def Cslib.Circuits.Boolean.SemiCircuit.LiftsTo (C' C : SemiCircuit) : Prop

Every consistent assignment of C' agrees on the parameters of C with a consistent assignment of C having the same output.