Lupanov truth-table blocks

This module defines the padded truth-table blocks and sparse support expressions used by finite Lupanov synthesis. It contains only the table representation and its elementary cost and one-hot semantics.

def Algebraic.MassProduction.LupanovSynthesis.blockCount (addressWidth blockSize : ℕ) : ℕ

Number of consecutive address-table blocks of length blockSize.

Equations

• Algebraic.MassProduction.LupanovSynthesis.blockCount addressWidth blockSize = 2 ^ addressWidth ⌈/⌉ blockSize

def Algebraic.MassProduction.LupanovSynthesis.patternCount (blockSize : ℕ) : ℕ

Number of Boolean patterns on one address block.

Equations

• Algebraic.MassProduction.LupanovSynthesis.patternCount blockSize = 2 ^ blockSize

def Algebraic.MassProduction.LupanovSynthesis.selectedBlock {blockSize addressWidth : ℕ} (blockSizePositive : 0 < blockSize) (address : Fin (2 ^ addressWidth)) : Fin (blockCount addressWidth blockSize)

The block containing a given address assignment.

Equations

• Algebraic.MassProduction.LupanovSynthesis.selectedBlock blockSizePositive address = ⟨↑address / blockSize, ⋯⟩

def Algebraic.MassProduction.LupanovSynthesis.selectedOffset {blockSize addressWidth : ℕ} (blockSizePositive : 0 < blockSize) (address : Fin (2 ^ addressWidth)) : Fin blockSize

Offset of an address assignment inside its selected block.

Equations

• Algebraic.MassProduction.LupanovSynthesis.selectedOffset blockSizePositive address = ⟨↑address % blockSize, ⋯⟩

noncomputable def Algebraic.MassProduction.LupanovSynthesis.blockColumn {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (data : Fin (2 ^ dataWidth)) : Fin blockSize → Bool

The padded truth-table column on one consecutive address block. Rows beyond the address table in the last block are fixed to false.

Equations

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

noncomputable def Algebraic.MassProduction.LupanovSynthesis.blockPattern {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (data : Fin (2 ^ dataWidth)) : Fin (patternCount blockSize)

Canonical index of the padded pattern in one truth-table block.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LupanovSynthesis.assignmentBits_blockPattern {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (data : Fin (2 ^ dataWidth)) (offset : Fin blockSize) : ShannonSynthesis.assignmentBits blockSize (blockPattern function block data) offset = blockColumn function block data offset

noncomputable def Algebraic.MassProduction.LupanovSynthesis.rightSupport {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) : Finset (Fin (2 ^ dataWidth))

Data assignments whose padded column has one fixed block pattern.

Equations

• Algebraic.MassProduction.LupanovSynthesis.rightSupport function block pattern = {data : Fin (2 ^ dataWidth) | Algebraic.MassProduction.LupanovSynthesis.blockPattern function block data = pattern}

@[simp]

theorem Algebraic.MassProduction.LupanovSynthesis.mem_rightSupport {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) (data : Fin (2 ^ dataWidth)) : data ∈ rightSupport function block pattern ↔ blockPattern function block data = pattern

noncomputable def Algebraic.MassProduction.LupanovSynthesis.supportExpression {inputs : ℕ} (support : Finset (Fin inputs)) : DeMorgan.Expression inputs

OR exactly the input wires in a finite support. Unlike a full-width OR, its charged size is the cardinality of the support.

Equations

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

theorem Algebraic.MassProduction.LupanovSynthesis.supportExpression_standardCost {inputs : ℕ} (support : Finset (Fin inputs)) : (supportExpression support).standardCost = support.card

theorem Algebraic.MassProduction.LupanovSynthesis.supportExpression_eval_oneHot {inputs : ℕ} (support : Finset (Fin inputs)) (flags : Fin inputs → Bool) (selected : Fin inputs) (selectedTrue : flags selected = true) (unique : ∀ (index : Fin inputs), flags index = true → index = selected) : DeMorgan.Expression.eval flags (supportExpression support) = decide (selected ∈ support)

On a one-hot vector, a sparse OR is exactly support membership of the selected coordinate.

noncomputable def Algebraic.MassProduction.LupanovSynthesis.rightExpression {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) : DeMorgan.Expression (2 ^ dataWidth)

The sparse data-pattern expression for one block and pattern.

Equations

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

theorem Algebraic.MassProduction.LupanovSynthesis.rightExpression_standardCost {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) : (rightExpression function block pattern).standardCost = (rightSupport function block pattern).card

theorem Algebraic.MassProduction.LupanovSynthesis.sum_rightSupport_card {addressWidth dataWidth blockSize : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (block : Fin (blockCount addressWidth blockSize)) : ∑ pattern : Fin (patternCount blockSize), (rightSupport function block pattern).card = 2 ^ dataWidth

The right supports for a fixed block partition all data assignments.