Native Shannon synthesis

This module gives an Algebraic-native version of the finite synthesis construction used as the base case of the mass-production induction. It uses a shared circuit for all minterms, followed by a shared library of all Boolean functions on a short address block. No external circuit model and no new type-class instances are used.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.bitVectorEquiv (width : ℕ) : (Fin width → Bool) ≃ Fin (2 ^ width)

Canonical finite index of a Boolean vector.

Equations

• Algebraic.MassProduction.ShannonSynthesis.bitVectorEquiv width = (Equiv.piCongrRight fun (x : Fin width) => finTwoEquiv.symm).trans finFunctionFinEquiv

noncomputable def Algebraic.MassProduction.ShannonSynthesis.assignmentBits (width : ℕ) (assignment : Fin (2 ^ width)) : Fin width → Bool

Decode a canonical finite index back to its Boolean vector.

Equations

• Algebraic.MassProduction.ShannonSynthesis.assignmentBits width assignment = (Algebraic.MassProduction.ShannonSynthesis.bitVectorEquiv width).symm assignment

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.bitVectorEquiv_assignmentBits {width : ℕ} (assignment : Fin (2 ^ width)) : (bitVectorEquiv width) (assignmentBits width assignment) = assignment

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.assignmentBits_bitVectorEquiv {width : ℕ} (input : Fin width → Bool) : assignmentBits width ((bitVectorEquiv width) input) = input

def Algebraic.MassProduction.ShannonSynthesis.matchingLiteral {inputs : ℕ} (index : Fin inputs) (expected : Bool) : DeMorgan.Expression inputs

A positive or negative occurrence of one input, according to the expected Boolean value.

Equations

• Algebraic.MassProduction.ShannonSynthesis.matchingLiteral index expected = if expected = true then Algebraic.DeMorgan.Expression.input index else (Algebraic.DeMorgan.Expression.input index).not

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.matchingLiteral_eval {inputs : ℕ} (index : Fin inputs) (expected : Bool) (input : Fin inputs → Bool) : DeMorgan.Expression.eval input (matchingLiteral index expected) = decide (input index = expected)

theorem Algebraic.MassProduction.ShannonSynthesis.matchingLiteral_standardCost_le {inputs : ℕ} (index : Fin inputs) (expected : Bool) : (matchingLiteral index expected).standardCost ≤ 1

def Algebraic.MassProduction.ShannonSynthesis.previousMintermInput {width : ℕ} (assignment : Fin (2 ^ width)) : Fin (2 ^ width + 1)

Index in the retained-state vector of a minterm from the previous dimension.

Equations

• Algebraic.MassProduction.ShannonSynthesis.previousMintermInput assignment = Fin.castAdd 1 assignment

def Algebraic.MassProduction.ShannonSynthesis.newHeadInput (width : ℕ) : Fin (2 ^ width + 1)

Index in the retained-state vector of the newly prepended input bit.

Equations

• Algebraic.MassProduction.ShannonSynthesis.newHeadInput width = Fin.last (2 ^ width)

noncomputable def Algebraic.MassProduction.ShannonSynthesis.assignmentTailIndex (width : ℕ) (assignment : Fin (2 ^ (width + 1))) : Fin (2 ^ width)

The previous-dimension assignment required by a full assignment.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.extensionExpression (width : ℕ) (assignment : Fin (2 ^ (width + 1))) : DeMorgan.Expression (2 ^ width + 1)

One output of the layer which extends all width-bit minterms by one new head bit.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

noncomputable def Algebraic.MassProduction.ShannonSynthesis.extensionGateCount (width : ℕ) : ℕ

Program-gate count of one full minterm-extension layer.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.extensionCircuit (width : ℕ) : Circuit DeMorgan.signature (2 ^ width + 1) (2 ^ (width + 1))

Compute all extended minterms in parallel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.extensionCircuit_size (width : ℕ) : (extensionCircuit width).size = extensionGateCount width

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.extensionCircuit_eval {width : ℕ} (state : Fin (2 ^ width + 1) → Bool) (assignment : Fin (2 ^ (width + 1))) : (extensionCircuit width).eval DeMorgan.interpretation state assignment = (state (previousMintermInput (assignmentTailIndex width assignment)) && decide (state (newHeadInput width) = assignmentBits (width + 1) assignment 0))

theorem Algebraic.MassProduction.ShannonSynthesis.extensionCircuit_cost_le (width : ℕ) : (extensionCircuit width).cost DeMorgan.standardCost ≤ 2 * 2 ^ (width + 1)

@[reducible]

noncomputable def Algebraic.MassProduction.ShannonSynthesis.mintermGateCount : ℕ → ℕ

Program-gate count of the shared all-minterms circuit.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.ShannonSynthesis.mintermGateCount 0 = 1

noncomputable def Algebraic.MassProduction.ShannonSynthesis.mintermCircuit (width : ℕ) : Circuit DeMorgan.signature width (2 ^ width)

A shared circuit computing the indicator of every Boolean assignment. The recursive layer prepends the new input bit, matching Fin.cons.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.ShannonSynthesis.mintermCircuit 0 = (Algebraic.DeMorgan.Expression.constant true).circuit

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.mintermCircuit_size (width : ℕ) : (mintermCircuit width).size = mintermGateCount width

theorem Algebraic.MassProduction.ShannonSynthesis.assignment_eq_iff_head_tail {width : ℕ} (input : Fin (width + 1) → Bool) (assignment : Fin (2 ^ (width + 1))) : (bitVectorEquiv (width + 1)) input = assignment ↔ (bitVectorEquiv width) (Fin.tail input) = assignmentTailIndex width assignment ∧ input 0 = assignmentBits (width + 1) assignment 0

Equality with a decoded assignment is exactly equality of the head bit and equality of the encoded tail.

theorem Algebraic.MassProduction.ShannonSynthesis.assignmentIndicator_extension {width : ℕ} (input : Fin (width + 1) → Bool) (assignment : Fin (2 ^ (width + 1))) : (decide ((bitVectorEquiv width) (Fin.tail input) = assignmentTailIndex width assignment) && decide (input 0 = assignmentBits (width + 1) assignment 0)) = decide ((bitVectorEquiv (width + 1)) input = assignment)

The Boolean conjunction used by an extension layer is the indicator of the represented full assignment.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.mintermCircuit_eval (width : ℕ) (input : Fin width → Bool) (assignment : Fin (2 ^ width)) : (mintermCircuit width).eval DeMorgan.interpretation input assignment = decide ((bitVectorEquiv width) input = assignment)

Every output of the shared minterm circuit is the exact indicator of its canonical Boolean assignment.

theorem Algebraic.MassProduction.ShannonSynthesis.mintermCircuit_cost_le (width : ℕ) : (mintermCircuit width).cost DeMorgan.standardCost ≤ 4 * 2 ^ width

The complete shared minterm table costs at most four gates per Boolean assignment.

The shared library of short-address Boolean functions

noncomputable def Algebraic.MassProduction.ShannonSynthesis.columnTerm (addressWidth : ℕ) (pattern : Fin (2 ^ 2 ^ addressWidth)) (assignment : Fin (2 ^ addressWidth)) : DeMorgan.Expression (2 ^ addressWidth)

One hardwired term in the truth-table disjunction for a short-address function.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.columnExpression (addressWidth : ℕ) (pattern : Fin (2 ^ 2 ^ addressWidth)) : DeMorgan.Expression (2 ^ addressWidth)

The truth-table formula for one Boolean function of the address block, evaluated on a one-hot vector of address minterms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.columnTerm_standardCost (addressWidth : ℕ) (pattern : Fin (2 ^ 2 ^ addressWidth)) (assignment : Fin (2 ^ addressWidth)) : (columnTerm addressWidth pattern assignment).standardCost = 0

theorem Algebraic.MassProduction.ShannonSynthesis.columnExpression_standardCost (addressWidth : ℕ) (pattern : Fin (2 ^ 2 ^ addressWidth)) : (columnExpression addressWidth pattern).standardCost = 2 ^ addressWidth

theorem Algebraic.MassProduction.ShannonSynthesis.columnExpression_eval_oneHot (addressWidth : ℕ) (pattern : Fin (2 ^ 2 ^ addressWidth)) (flags : Fin (2 ^ addressWidth) → Bool) (selected : Fin (2 ^ addressWidth)) (selectedTrue : flags selected = true) (unique : ∀ (assignment : Fin (2 ^ addressWidth)), flags assignment = true → assignment = selected) : DeMorgan.Expression.eval flags (columnExpression addressWidth pattern) = assignmentBits (2 ^ addressWidth) pattern selected

A hardwired column formula reads the truth-table bit selected by a one-hot minterm vector.

@[reducible]

noncomputable def Algebraic.MassProduction.ShannonSynthesis.libraryGateCount (addressWidth : ℕ) : ℕ

Program-gate count of the complete short-address function library.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.libraryCircuit (addressWidth : ℕ) : Circuit DeMorgan.signature (2 ^ addressWidth) (2 ^ 2 ^ addressWidth)

All Boolean functions of addressWidth inputs, sharing the same address minterm vector.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.libraryCircuit_size (addressWidth : ℕ) : (libraryCircuit addressWidth).size = libraryGateCount addressWidth

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.libraryCircuit_eval (addressWidth : ℕ) (flags : Fin (2 ^ addressWidth) → Bool) (pattern : Fin (2 ^ 2 ^ addressWidth)) : (libraryCircuit addressWidth).eval DeMorgan.interpretation flags pattern = DeMorgan.Expression.eval flags (columnExpression addressWidth pattern)

theorem Algebraic.MassProduction.ShannonSynthesis.libraryCircuit_cost (addressWidth : ℕ) : (libraryCircuit addressWidth).cost DeMorgan.standardCost = 2 ^ 2 ^ addressWidth * 2 ^ addressWidth

theorem Algebraic.MassProduction.ShannonSynthesis.library_after_minterms_eval (addressWidth : ℕ) (input : Fin addressWidth → Bool) (pattern : Fin (2 ^ 2 ^ addressWidth)) : (libraryCircuit addressWidth).eval DeMorgan.interpretation ((mintermCircuit addressWidth).eval DeMorgan.interpretation input) pattern = assignmentBits (2 ^ addressWidth) pattern ((bitVectorEquiv addressWidth) input)

Composing the library after the shared minterm circuit evaluates the canonical truth-table bit of the input address.

Synthesis of an arbitrary split-input Boolean function

def Algebraic.MassProduction.ShannonSynthesis.addressInput {addressWidth : ℕ} (dataWidth : ℕ) (input : Fin (addressWidth + dataWidth) → Bool) : Fin addressWidth → Bool

The initial address block of a split input.

Equations

• Algebraic.MassProduction.ShannonSynthesis.addressInput dataWidth input = input ∘ Fin.castAdd dataWidth

def Algebraic.MassProduction.ShannonSynthesis.dataInput {dataWidth : ℕ} (addressWidth : ℕ) (input : Fin (addressWidth + dataWidth) → Bool) : Fin dataWidth → Bool

The final data block of a split input.

Equations

• Algebraic.MassProduction.ShannonSynthesis.dataInput addressWidth input = input ∘ Fin.natAdd addressWidth

theorem Algebraic.MassProduction.ShannonSynthesis.append_addressInput_dataInput {addressWidth dataWidth : ℕ} (input : Fin (addressWidth + dataWidth) → Bool) : Fin.append (addressInput dataWidth input) (dataInput addressWidth input) = input

@[reducible]

noncomputable def Algebraic.MassProduction.ShannonSynthesis.splitMintermGateCount (addressWidth dataWidth : ℕ) : ℕ

Gate count of the two shared minterm tables.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.splitMintermCircuit (addressWidth dataWidth : ℕ) : Circuit DeMorgan.signature (addressWidth + dataWidth) (2 ^ addressWidth + 2 ^ dataWidth)

Compute all address and all data minterms in parallel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.splitMintermCircuit_size (addressWidth dataWidth : ℕ) : (splitMintermCircuit addressWidth dataWidth).size = splitMintermGateCount addressWidth dataWidth

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.splitMintermCircuit_eval {addressWidth dataWidth : ℕ} (input : Fin (addressWidth + dataWidth) → Bool) : (splitMintermCircuit addressWidth dataWidth).eval DeMorgan.interpretation input = Fin.append ((mintermCircuit addressWidth).eval DeMorgan.interpretation (addressInput dataWidth input)) ((mintermCircuit dataWidth).eval DeMorgan.interpretation (dataInput addressWidth input))

@[reducible]

noncomputable def Algebraic.MassProduction.ShannonSynthesis.libraryAndDataGateCount (addressWidth : ℕ) : ℕ

Gate count of the library stage, whose retained data minterms are free wires.

Equations

• Algebraic.MassProduction.ShannonSynthesis.libraryAndDataGateCount addressWidth = Algebraic.MassProduction.ShannonSynthesis.libraryGateCount addressWidth

noncomputable def Algebraic.MassProduction.ShannonSynthesis.libraryAndDataCircuit (addressWidth dataWidth : ℕ) : Circuit DeMorgan.signature (2 ^ addressWidth + 2 ^ dataWidth) (2 ^ 2 ^ addressWidth + 2 ^ dataWidth)

Evaluate the complete address library while retaining every data minterm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.libraryAndDataCircuit_size (addressWidth dataWidth : ℕ) : (libraryAndDataCircuit addressWidth dataWidth).size = libraryAndDataGateCount addressWidth

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.libraryAndDataCircuit_eval {addressWidth dataWidth : ℕ} (state : Fin (2 ^ addressWidth + 2 ^ dataWidth) → Bool) : (libraryAndDataCircuit addressWidth dataWidth).eval DeMorgan.interpretation state = Fin.append ((libraryCircuit addressWidth).eval DeMorgan.interpretation fun (assignment : Fin (2 ^ addressWidth)) => state (Fin.castAdd (2 ^ dataWidth) assignment)) fun (assignment : Fin (2 ^ dataWidth)) => state (Fin.natAdd (2 ^ addressWidth) assignment)

noncomputable def Algebraic.MassProduction.ShannonSynthesis.columnPattern {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (dataAssignment : Fin (2 ^ dataWidth)) : Fin (2 ^ 2 ^ addressWidth)

The address truth-table column required when the data block has one fixed assignment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.assignmentBits_columnPattern {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (dataAssignment : Fin (2 ^ dataWidth)) (addressAssignment : Fin (2 ^ addressWidth)) : assignmentBits (2 ^ addressWidth) (columnPattern function dataAssignment) addressAssignment = function (Fin.append (assignmentBits addressWidth addressAssignment) (assignmentBits dataWidth dataAssignment))

def Algebraic.MassProduction.ShannonSynthesis.columnInput {addressWidth : ℕ} (dataWidth : ℕ) (pattern : Fin (2 ^ 2 ^ addressWidth)) : Fin (2 ^ 2 ^ addressWidth + 2 ^ dataWidth)

Input coordinate of a precomputed address-column value.

Equations

• Algebraic.MassProduction.ShannonSynthesis.columnInput dataWidth pattern = Fin.castAdd (2 ^ dataWidth) pattern

def Algebraic.MassProduction.ShannonSynthesis.dataMintermInput {dataWidth : ℕ} (addressWidth : ℕ) (assignment : Fin (2 ^ dataWidth)) : Fin (2 ^ 2 ^ addressWidth + 2 ^ dataWidth)

Input coordinate of a retained data minterm.

Equations

• Algebraic.MassProduction.ShannonSynthesis.dataMintermInput addressWidth assignment = Fin.natAdd (2 ^ 2 ^ addressWidth) assignment

noncomputable def Algebraic.MassProduction.ShannonSynthesis.rowExpression {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (dataAssignment : Fin (2 ^ dataWidth)) : DeMorgan.Expression (2 ^ 2 ^ addressWidth + 2 ^ dataWidth)

Combine one retained data minterm with the corresponding hardwired address-function column.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.synthesisExpression {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) : DeMorgan.Expression (2 ^ 2 ^ addressWidth + 2 ^ dataWidth)

OR the row terms to obtain the synthesized function.

Equations

• Algebraic.MassProduction.ShannonSynthesis.synthesisExpression function = Algebraic.DeMorgan.Expression.finOr (2 ^ dataWidth) (Algebraic.MassProduction.ShannonSynthesis.rowExpression function)

theorem Algebraic.MassProduction.ShannonSynthesis.synthesisExpression_standardCost {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) : (synthesisExpression function).standardCost = 2 * 2 ^ dataWidth

@[reducible]

noncomputable def Algebraic.MassProduction.ShannonSynthesis.synthesisGateCount {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) : ℕ

Program-gate count of the complete native Shannon circuit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.ShannonSynthesis.circuit {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) : Circuit DeMorgan.signature (addressWidth + dataWidth) 1

Algebraic-native Shannon synthesis with a caller-selected address/data split.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.circuit_size {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) : (circuit function).size = synthesisGateCount function

noncomputable def Algebraic.MassProduction.ShannonSynthesis.libraryState (addressWidth dataWidth : ℕ) (input : Fin (addressWidth + dataWidth) → Bool) : Fin (2 ^ 2 ^ addressWidth + 2 ^ dataWidth) → Bool

Intermediate values after both minterm tables and the address-function library have been evaluated.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.libraryState_column {addressWidth dataWidth : ℕ} (input : Fin (addressWidth + dataWidth) → Bool) (pattern : Fin (2 ^ 2 ^ addressWidth)) : libraryState addressWidth dataWidth input (columnInput dataWidth pattern) = assignmentBits (2 ^ addressWidth) pattern ((bitVectorEquiv addressWidth) (addressInput dataWidth input))

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.libraryState_dataMinterm {addressWidth dataWidth : ℕ} (input : Fin (addressWidth + dataWidth) → Bool) (assignment : Fin (2 ^ dataWidth)) : libraryState addressWidth dataWidth input (dataMintermInput addressWidth assignment) = decide ((bitVectorEquiv dataWidth) (dataInput addressWidth input) = assignment)

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.rowExpression_eval_libraryState {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (input : Fin (addressWidth + dataWidth) → Bool) (dataAssignment : Fin (2 ^ dataWidth)) : DeMorgan.Expression.eval (libraryState addressWidth dataWidth input) (rowExpression function dataAssignment) = (decide ((bitVectorEquiv dataWidth) (dataInput addressWidth input) = dataAssignment) && function (Fin.append (addressInput dataWidth input) (assignmentBits dataWidth dataAssignment)))

theorem Algebraic.MassProduction.ShannonSynthesis.circuit_eval {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (input : Fin (addressWidth + dataWidth) → Bool) : (circuit function).eval DeMorgan.interpretation input 0 = function input

The native Shannon circuit computes the supplied Boolean function.

@[reducible]

def Algebraic.MassProduction.ShannonSynthesis.costBound (addressWidth dataWidth : ℕ) : ℕ

Explicit cost ledger for the split synthesis construction.

Equations

• Algebraic.MassProduction.ShannonSynthesis.costBound addressWidth dataWidth = 4 * 2 ^ addressWidth + 4 * 2 ^ dataWidth + 2 ^ 2 ^ addressWidth * 2 ^ addressWidth + 2 * 2 ^ dataWidth

theorem Algebraic.MassProduction.ShannonSynthesis.circuit_cost_le {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) : (circuit function).cost DeMorgan.standardCost ≤ costBound addressWidth dataWidth