Gates over the full binary basis

The gates of fair semi-circuits (Cslib.Circuits.Boolean.SemiCircuit). An argument is a constant or an internal value named by a natural number, a literal is an argument, possibly negated, and a gate applies an operation Bool → Bool → Bool of the full binary basis B₂ to two arguments. Rerouting the internal value v to a literal (Gate.subst) absorbs the negation into the operation and preserves the value of the gate on assignments giving v the value of the literal (Gate.eval_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, an AND-type one, has the form (a + α)(b + β) + γ (exists_and_form), takes both values (exists_eq_of_not_isAffineOp'), and is constant on a line of 𝔽₂² on which any other operation is constant (exists_line_const). An affine operation that is neither constant nor a projection is XOR-type (exists_xor_form).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit.Arg, Cslib.Circuits.Boolean.SemiCircuit.Lit, Cslib.Circuits.Boolean.SemiCircuit.Gate: arguments, literals and gates.
• Cslib.Circuits.Boolean.SemiCircuit.Gate.subst: rerouting an internal value to a literal.
• Cslib.Circuits.Boolean.SemiCircuit.Gate.Degenerate, Cslib.Circuits.Boolean.SemiCircuit.Gate.lit: degenerate gates and the literal they compute.
• Cslib.Circuits.Boolean.SemiCircuit.IsAffineOp, Cslib.Circuits.Boolean.SemiCircuit.IsUnaryOp: affine operations and projections.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_subst: rerouting preserves evaluation.
• Cslib.Circuits.Boolean.SemiCircuit.exists_and_form, Cslib.Circuits.Boolean.SemiCircuit.exists_xor_form, Cslib.Circuits.Boolean.SemiCircuit.exists_line_const: the operations of B₂.

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

Arguments, literals and gates

inductive Cslib.Circuits.Boolean.SemiCircuit.Arg : Type

An argument of a gate: a constant or the internal value with the given name.

• const (b : Bool) : Arg

  A constant.

• node (i : ℕ) : Arg

  An internal value.

@[instance_reducible]

instance Cslib.Circuits.Boolean.SemiCircuit.instDecidableEqArg : DecidableEq Arg

def Cslib.Circuits.Boolean.SemiCircuit.instDecidableEqArg.decEq (x✝ x✝¹ : Arg) : Decidable (x✝ = x✝¹)

def Cslib.Circuits.Boolean.SemiCircuit.Arg.eval (val : ℕ → Bool) : Arg → Bool

The value of an argument under an assignment of the internal values.

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.Arg.eval_const (val : ℕ → Bool) (b : Bool) : eval val (const b) = b

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.Arg.eval_node (val : ℕ → Bool) (i : ℕ) : eval val (node i) = val i

def Cslib.Circuits.Boolean.SemiCircuit.Arg.substArg (a : Arg) (v : ℕ) (target : Arg) : Arg

The argument node v replaced by the argument of the literal ℓ.

theorem Cslib.Circuits.Boolean.SemiCircuit.Arg.eval_congr {a : Arg} {val val' : ℕ → Bool} (h : ∀ (i : ℕ), a = node i → val i = val' i) : eval val a = eval val' a

Changing the assignment away from the internal values an argument reads keeps its value.

structure Cslib.Circuits.Boolean.SemiCircuit.Lit : Type

A literal: an argument, negated when neg holds. Outputs and reroutings are literals.

• arg : Arg

  The argument.

• neg : Bool

  Whether the argument is negated.

@[instance_reducible]

instance Cslib.Circuits.Boolean.SemiCircuit.instDecidableEqLit : DecidableEq Lit

def Cslib.Circuits.Boolean.SemiCircuit.instDecidableEqLit.decEq (x✝ x✝¹ : Lit) : Decidable (x✝ = x✝¹)

def Cslib.Circuits.Boolean.SemiCircuit.Lit.eval (ℓ : Lit) (val : ℕ → Bool) : Bool

The value of a literal.

def Cslib.Circuits.Boolean.SemiCircuit.Lit.const (b : Bool) : Lit

The constant literal b.

def Cslib.Circuits.Boolean.SemiCircuit.Lit.node (t : ℕ) (c : Bool) : Lit

The literal t ⊕ c of the internal value t.

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.eval_const (b : Bool) (val : ℕ → Bool) : (const b).eval val = b

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.eval_node (t : ℕ) (c : Bool) (val : ℕ → Bool) : (node t c).eval val = (val t ^^ c)

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

Reroute the internal value v in a literal to the literal ℓ.

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.eval_subst {o : Lit} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (o.subst v ℓ).eval val = o.eval val

def Cslib.Circuits.Boolean.SemiCircuit.Lit.Reads (o : Lit) (t : ℕ) : Prop

The literal reads the internal value t.

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.eval_congr {o : Lit} {val val' : ℕ → Bool} (h : ∀ (i : ℕ), o.Reads i → val i = val' i) : o.eval val = o.eval val'

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.not_reads_subst {o : Lit} {v : ℕ} {ℓ : Lit} (hℓ : ¬ℓ.Reads v) : ¬(o.subst v ℓ).Reads v

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.reads_of_reads_subst {o : Lit} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : (o.subst v ℓ).Reads z) : o.Reads z ∨ o.Reads v ∧ ℓ.Reads z

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.subst_of_not_reads {o : Lit} {v : ℕ} {ℓ : Lit} (h : ¬o.Reads v) : o.subst v ℓ = o

theorem Cslib.Circuits.Boolean.SemiCircuit.Lit.eval_subst_update {o : Lit} {v : ℕ} {ℓ : Lit} (hℓ : ¬ℓ.Reads v) (val : ℕ → Bool) : (o.subst v ℓ).eval val = o.eval (Function.update val v (ℓ.eval val))

A literal with v rerouted to a literal not reading v evaluates as the literal on the assignment giving v the value of the rerouting literal.

structure Cslib.Circuits.Boolean.SemiCircuit.Gate : Type

A gate of the acyclic part: an operation of the full binary basis B₂ applied to two arguments.

• op : Bool → Bool → Bool

  The operation of the gate.

• left : Arg

  The first argument.

• right : Arg

  The second argument.

def Cslib.Circuits.Boolean.SemiCircuit.Gate.eval (g : Gate) (val : ℕ → Bool) : Bool

The value of a gate, given the values of its arguments.

def Cslib.Circuits.Boolean.SemiCircuit.Gate.Reads (g : Gate) (t : ℕ) : Prop

The gate reads the internal value t.

@[instance_reducible]

instance Cslib.Circuits.Boolean.SemiCircuit.Gate.instDecidablePredNatReads (g : Gate) : DecidablePred g.Reads

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_congr {g : Gate} {val val' : ℕ → Bool} (h : ∀ (i : ℕ), g.Reads i → val i = val' i) : g.eval val = g.eval val'

A gate's value depends only on the internal values it reads.

def Cslib.Circuits.Boolean.SemiCircuit.Gate.substNeg (a : Arg) (v : ℕ) (ℓ : Lit) : Bool

The negation absorbed into the operation when the argument a is rerouted.

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

Reroute the internal value v to the literal ℓ: arguments node v read the argument of ℓ, and the negation of ℓ is absorbed into the operation.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_substArg {a : Arg} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (Arg.eval val (a.substArg v ℓ.arg) ^^ substNeg a v ℓ) = Arg.eval val a

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_subst {g : Gate} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (g.subst v ℓ).eval val = g.eval val

Rerouting v to a literal with the value of v preserves the value of every gate.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.substArg_eq_node_of_ne {a : Arg} {v z : ℕ} {target : Arg} (hzv : z ≠ v) (hzt : target ≠ Arg.node z) : a.substArg v target = Arg.node z ↔ a = Arg.node z

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eq_node_of_substArg_eq_node {a : Arg} {v z : ℕ} {target : Arg} (h : a.substArg v target = Arg.node z) : a = Arg.node z ∨ a = Arg.node v ∧ target = Arg.node z

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.reads_subst_of_ne {g : Gate} {v : ℕ} {ℓ : Lit} {z : ℕ} (hzv : z ≠ v) (hzℓ : ℓ.arg ≠ Arg.node z) : (g.subst v ℓ).Reads z ↔ g.Reads z

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.reads_of_reads_subst {g : Gate} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : (g.subst v ℓ).Reads z) : g.Reads z ∨ g.Reads v ∧ ℓ.arg = Arg.node z

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.not_reads_subst {g : Gate} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ Arg.node v) : ¬(g.subst v ℓ).Reads v

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_subst_of_not_reads {g : Gate} {v : ℕ} {ℓ : Lit} (h : ¬g.Reads v) (val : ℕ → Bool) : (g.subst v ℓ).eval val = g.eval val

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_subst_update {g : Gate} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ Arg.node v) (val : ℕ → Bool) : (g.subst v ℓ).eval val = g.eval (Function.update val v (ℓ.eval val))

A gate with v rerouted to a literal not reading v evaluates as the gate on the assignment giving v the value of the literal.

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_subst_const (g : Gate) (v : ℕ) (b : Bool) (val : ℕ → Bool) : (g.subst v (Lit.const b)).eval val = g.eval (Function.update val v b)

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.args_of_reads {g : Gate} {z z' : ℕ} (hzz : z ≠ z') (hz : g.Reads z) (hz' : g.Reads z') : g.left = Arg.node z ∧ g.right = Arg.node z' ∨ g.left = Arg.node z' ∧ g.right = Arg.node z

A gate reading two distinct internal values reads exactly them.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.reads_of_args {g : Gate} {x y : ℕ} (h : g.left = Arg.node x ∧ g.right = Arg.node y ∨ g.left = Arg.node y ∧ g.right = Arg.node x) : g.Reads x ∧ g.Reads y

A gate whose arguments are x and y, in either order, reads both.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eq_or_eq_of_reads {g : Gate} {a b i : ℕ} (hab : a ≠ b) (ha : g.Reads a) (hb : g.Reads b) (hi : g.Reads i) : i = a ∨ i = b

A gate reading two distinct internal values reads nothing else.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.card_filter_reads_le (g : Gate) (s : Finset ℕ) : (Finset.filter g.Reads s).card ≤ 2

A gate reads at most two internal values.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_of_args {g : Gate} {a b : ℕ} (ha : g.left = Arg.node a) (hb : g.right = Arg.node b) (val : ℕ → Bool) : g.eval val = g.op (val a) (val b)

The value of a gate reading the internal values a and b.

Degenerate gates

def Cslib.Circuits.Boolean.SemiCircuit.Gate.lit (g : Gate) : Lit

The literal computed by a gate with a constant argument or two equal arguments.

def Cslib.Circuits.Boolean.SemiCircuit.Gate.Degenerate (g : Gate) : Prop

The gate has a constant argument or two equal arguments.

theorem Cslib.Circuits.Boolean.SemiCircuit.unary_cases (h : Bool → Bool) (x : Bool) : h x = if h false = h true then h false else x ^^ h false

A Boolean function of one bit is a constant or a literal.

def Cslib.Circuits.Boolean.SemiCircuit.unaryLit (h : Bool → Bool) (a : Arg) : Lit

The literal computing the Boolean function h of one bit applied to the argument a.

theorem Cslib.Circuits.Boolean.SemiCircuit.eval_unaryLit (h : Bool → Bool) (a : Arg) (val : ℕ → Bool) : h (Arg.eval val a) = (unaryLit h a).eval val

theorem Cslib.Circuits.Boolean.SemiCircuit.reads_of_unaryLit_reads {h : Bool → Bool} {a : Arg} {t : ℕ} (hr : (unaryLit h a).Reads t) : a = Arg.node t

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.eval_lit {g : Gate} (hg : g.Degenerate) (val : ℕ → Bool) : g.eval val = g.lit.eval val

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.reads_of_lit_reads {g : Gate} {t : ℕ} (h : g.lit.Reads t) : g.Reads t

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.degenerate_subst {g : Gate} (hg : g.Degenerate) (v : ℕ) (ℓ : Lit) : (g.subst v ℓ).Degenerate

Operations of the full binary basis

def Cslib.Circuits.Boolean.SemiCircuit.IsAffineOp (op : Bool → Bool → Bool) : Prop

An operation of B₂ is affine when its multilinear expression has no product term.

@[instance_reducible]

instance Cslib.Circuits.Boolean.SemiCircuit.instDecidableIsAffineOp (op : Bool → Bool → Bool) : Decidable (IsAffineOp op)

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_eq_of_not_isAffineOp {op : Bool → Bool → Bool} (h : ¬IsAffineOp op) : (∃ (b : Bool), op b false = op b true) ∧ ∃ (b : Bool), op false b = op true b

An AND-type operation becomes constant when either argument takes a suitable value.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.exists_const_of_not_isAffineOp {g : Gate} (hg : ¬IsAffineOp g.op) {a w : ℕ} (hargs : g.left = Arg.node a ∧ g.right = Arg.node w ∨ g.left = Arg.node w ∧ g.right = Arg.node a) : ∃ (b : Bool) (c : Bool), ∀ (val : ℕ → Bool), val w = b → g.eval val = c

An AND-type gate reading two internal values becomes constant once the value w is fixed suitably.

def Cslib.Circuits.Boolean.SemiCircuit.IsUnaryOp (op : Bool → Bool → Bool) : Prop

The operation is a projection or a negated projection: x ↦ c + x or y ↦ c + y.

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_diag_const (op : Bool → Bool → Bool) : ((∃ (c : Bool), op c false = op (!c) true) ∧ ∃ (c : Bool), op false c = op true !c) ∨ IsUnaryOp op

An operation that is not a projection or a negated projection is constant on a diagonal {(c + a, a)} for a suitable c, and likewise on {(a, c + a)}.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.exists_const_of_diag {g : Gate} (hg : ¬IsUnaryOp g.op) {p r : ℕ} (hargs : g.left = Arg.node p ∧ g.right = Arg.node r ∨ g.left = Arg.node r ∧ g.right = Arg.node p) : ∃ (c : Bool) (d : Bool), ∀ (val : ℕ → Bool), val p = (val r ^^ c) → g.eval val = d

An operation that is not a projection or a negated projection is constant on a diagonal: a gate with such an operation reading p and r is constant once p = r + c for a suitable c.

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_and_form {op : Bool → Bool → Bool} (h : ¬IsAffineOp op) : ∃ (α : Bool) (β : Bool) (γ : Bool), ∀ (a b : Bool), op a b = ((a ^^ α) && (b ^^ β) ^^ γ)

Every AND-type operation has the form (a + α)(b + β) + γ.

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_eq_of_not_isAffineOp' {op : Bool → Bool → Bool} (h : ¬IsAffineOp op) (δ : Bool) : ∃ (a : Bool) (b : Bool), op a b = δ

An AND-type operation takes both values.

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_xor_form {op : Bool → Bool → Bool} (h : IsAffineOp op) (hu : ¬IsUnaryOp op) (hc : ∃ (a : Bool) (b : Bool), op a b ≠ op false false) : ∃ (c : Bool), ∀ (a b : Bool), op a b = (a ^^ b ^^ c)

An affine operation that is neither constant nor a projection or a negated projection is XOR-type: a + b + c.

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_line_const {g h : Bool → Bool → Bool} (hg : ¬IsAffineOp g) : (∃ (c : Bool), (∀ (b : Bool), g c b = g c false) ∧ ∀ (b : Bool), h c b = h c false) ∨ (∃ (c : Bool), (∀ (a : Bool), g a c = g false c) ∧ ∀ (a : Bool), h a c = h false c) ∨ ∃ (c : Bool), (∀ (b : Bool), g (b ^^ c) b = g c false) ∧ ∀ (b : Bool), h (b ^^ c) b = h c false

Of two operations of two bits, one AND-type, both are constant on a common line of 𝔽₂²: a = c, b = c or a = b + c for a suitable constant c.

theorem Cslib.Circuits.Boolean.SemiCircuit.Gate.exists_op_of_args {g : Gate} {x y : ℕ} (h : g.left = Arg.node x ∧ g.right = Arg.node y ∨ g.left = Arg.node y ∧ g.right = Arg.node x) : ∃ (φ : Bool → Bool → Bool), (IsAffineOp φ ↔ IsAffineOp g.op) ∧ ∀ (val : ℕ → Bool), g.eval val = φ (val x) (val y)

A gate reading the internal values x and y computes an operation of their values, which is affine exactly when the operation of the gate is.