Boolean gate cost with free constants

nonconstantCost charges NOT, AND and OR gates, while constants are free. This is the cost convention used by the mass-production source; ordinary Circuit.size also charges constants. The source's free identity gates are represented by native wiring.

Main definitions

• Cslib.Circuits.Boolean.nonconstantCost: one for NOT, AND and OR, zero for constants.

Main results

• Cslib.Circuits.Program.cost_nonconstantCost_le: this cost is at most the gate count.

References

• Adapted from Basis/DeMorgan.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.nonconstantCost : Op → ℕ

Charge NOT, AND and OR once, and constants zero times. Designated outputs and wiring are already free in the underlying circuit model.

@[simp]

theorem Cslib.Circuits.Boolean.nonconstantCost_const (b : Bool) : nonconstantCost (Op.const b) = 0

Constant gates have nonconstantCost equal to 0.

@[simp]

theorem Cslib.Circuits.Boolean.nonconstantCost_not : nonconstantCost Op.not = 1

Negation gates have nonconstantCost equal to 1.

@[simp]

theorem Cslib.Circuits.Boolean.nonconstantCost_and : nonconstantCost Op.and = 1

Conjunction gates have nonconstantCost equal to 1.

@[simp]

theorem Cslib.Circuits.Boolean.nonconstantCost_or : nonconstantCost Op.or = 1

Disjunction gates have nonconstantCost equal to 1.

theorem Cslib.Circuits.Boolean.nonconstantCost_le_one (op : Op) : nonconstantCost op ≤ 1

Every De Morgan operation has nonconstantCost at most 1.

theorem Cslib.Circuits.Program.cost_nonconstantCost_le {n g : ℕ} (p : Program Boolean.signature n g) : p.cost Boolean.nonconstantCost ≤ g

Ignoring constant gates cannot increase the gate count.