Boolean scalar synthesis data

This module packages a concrete one-output De Morgan circuit for every Boolean function at a fixed input width. Synthesis data is always passed explicitly; neither the fixed-width package nor a width-indexed family is a typeclass.

structure Algebraic.MassProduction.ScalarSynthesis (width : ℕ) : Type

Explicit data for synthesizing every Boolean function at one fixed input width.

• circuit (function : ScalarFunction Bool width) : Circuit DeMorgan.signature width 1

  Concrete one-output circuit selected for each scalar target.

• computes (function : ScalarFunction Bool width) : (self.circuit function).ComputesWith DeMorgan.interpretation (scalarTarget function)

  Proof that every selected circuit computes its requested target.

@[reducible, inline]

abbrev Algebraic.MassProduction.ScalarSynthesis.gateCount {width : ℕ} (synthesis : ScalarSynthesis width) (function : ScalarFunction Bool width) : ℕ

Program-gate count selected for each scalar target.

Equations

• synthesis.gateCount function = (synthesis.circuit function).size

@[reducible, inline]

abbrev Algebraic.MassProduction.ScalarSynthesisFamily : Type

Width-indexed one-copy synthesis data.

Equations

• Algebraic.MassProduction.ScalarSynthesisFamily = ((width : ℕ) → Algebraic.MassProduction.ScalarSynthesis width)