Finite Lupanov circuit

This module recombines the two pattern banks into the finite Lupanov block-table circuit. It gives an explicit cost ledger and proves exact evaluation and ComputesWith theorems for every positive block size.

Recombination and the complete finite circuit

@[reducible]

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

Number of flattened (block, pattern) flags in either bank.

Equations

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

@[reducible]

noncomputable def Algebraic.MassProduction.LupanovSynthesis.patternBankGateCount {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) : ℕ

Program-gate count of both flattened pattern banks.

Equations

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

noncomputable def Algebraic.MassProduction.LupanovSynthesis.patternBankCircuit {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) : Circuit DeMorgan.signature (2 ^ addressWidth + 2 ^ dataWidth) (bankWidth addressWidth blockSize + bankWidth addressWidth blockSize)

Compute the left and right pattern banks side by side.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LupanovSynthesis.patternBankCircuit_size {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) : (patternBankCircuit function blockSize).size = patternBankGateCount function blockSize

def Algebraic.MassProduction.LupanovSynthesis.leftPatternInput {addressWidth blockSize : ℕ} (index : Fin (bankWidth addressWidth blockSize)) : Fin (bankWidth addressWidth blockSize + bankWidth addressWidth blockSize)

Coordinate of a left-bank flag in the combined pattern state.

Equations

• Algebraic.MassProduction.LupanovSynthesis.leftPatternInput index = Fin.castAdd (Algebraic.MassProduction.LupanovSynthesis.bankWidth addressWidth blockSize) index

def Algebraic.MassProduction.LupanovSynthesis.rightPatternInput {addressWidth blockSize : ℕ} (index : Fin (bankWidth addressWidth blockSize)) : Fin (bankWidth addressWidth blockSize + bankWidth addressWidth blockSize)

Coordinate of the corresponding right-bank flag.

Equations

• Algebraic.MassProduction.LupanovSynthesis.rightPatternInput index = Fin.natAdd (Algebraic.MassProduction.LupanovSynthesis.bankWidth addressWidth blockSize) index

@[simp]

theorem Algebraic.MassProduction.LupanovSynthesis.patternBankCircuit_eval_left {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (state : Fin (2 ^ addressWidth + 2 ^ dataWidth) → Bool) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) : (patternBankCircuit function blockSize).eval DeMorgan.interpretation state (leftPatternInput (finProdFinEquiv (block, pattern))) = DeMorgan.Expression.eval (fun (address : Fin (2 ^ addressWidth)) => state (Fin.castAdd (2 ^ dataWidth) address)) (leftExpression addressWidth blockSize block pattern)

@[simp]

theorem Algebraic.MassProduction.LupanovSynthesis.patternBankCircuit_eval_right {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (state : Fin (2 ^ addressWidth + 2 ^ dataWidth) → Bool) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) : (patternBankCircuit function blockSize).eval DeMorgan.interpretation state (rightPatternInput (finProdFinEquiv (block, pattern))) = DeMorgan.Expression.eval (fun (data : Fin (2 ^ dataWidth)) => state (Fin.natAdd (2 ^ addressWidth) data)) (rightExpression function block pattern)

theorem Algebraic.MassProduction.LupanovSynthesis.patternBankCircuit_cost {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) : (patternBankCircuit function blockSize).cost DeMorgan.standardCost = blockCount addressWidth blockSize * (patternCount blockSize * blockSize) + blockCount addressWidth blockSize * 2 ^ dataWidth

def Algebraic.MassProduction.LupanovSynthesis.matchingPatternTerm (addressWidth blockSize : ℕ) (index : Fin (bankWidth addressWidth blockSize)) : DeMorgan.Expression (bankWidth addressWidth blockSize + bankWidth addressWidth blockSize)

Conjoin corresponding flags in the two pattern banks.

Equations

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

def Algebraic.MassProduction.LupanovSynthesis.synthesisExpression (addressWidth blockSize : ℕ) : DeMorgan.Expression (bankWidth addressWidth blockSize + bankWidth addressWidth blockSize)

OR all matching block-pattern conjunctions.

Equations

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

theorem Algebraic.MassProduction.LupanovSynthesis.synthesisExpression_standardCost (addressWidth blockSize : ℕ) : (synthesisExpression addressWidth blockSize).standardCost = 2 * bankWidth addressWidth blockSize

@[reducible]

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

Program-gate count of all three stages of finite Lupanov synthesis.

Equations

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

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

The finite Lupanov block-table circuit.

Equations

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

@[simp]

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

def Algebraic.MassProduction.LupanovSynthesis.costBound (addressWidth dataWidth blockSize : ℕ) : ℕ

Explicit finite cost ledger.

Equations

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

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

Exact semantics

theorem Algebraic.MassProduction.LupanovSynthesis.leftExpression_eval_minterms_true_iff (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) (addressInput : Fin addressWidth → Bool) : DeMorgan.Expression.eval ((ShannonSynthesis.mintermCircuit addressWidth).eval DeMorgan.interpretation addressInput) (leftExpression addressWidth blockSize block pattern) = true ↔ ∃ (offset : Fin blockSize) (rowValid : ↑block * blockSize + ↑offset < 2 ^ addressWidth), ⟨↑block * blockSize + ↑offset, rowValid⟩ = (ShannonSynthesis.bitVectorEquiv addressWidth) addressInput ∧ ShannonSynthesis.assignmentBits blockSize pattern offset = true

The address-side block expression, fed by the shared minterm table, is true exactly when one of its literal rows is the selected address and the corresponding pattern bit is true.

theorem Algebraic.MassProduction.LupanovSynthesis.rightExpression_eval_minterms {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) (dataInput : Fin dataWidth → Bool) : DeMorgan.Expression.eval ((ShannonSynthesis.mintermCircuit dataWidth).eval DeMorgan.interpretation dataInput) (rightExpression function block pattern) = decide (blockPattern function block ((ShannonSynthesis.bitVectorEquiv dataWidth) dataInput) = pattern)

The data-side sparse expression, fed by the shared minterm table, is the indicator of the selected data column having the requested block pattern.

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

The finite block-table circuit computes the supplied Boolean function exactly.

theorem Algebraic.MassProduction.LupanovSynthesis.circuit_computes {blockSize addressWidth dataWidth : ℕ} (blockSizePositive : 0 < blockSize) (function : ScalarFunction Bool (addressWidth + dataWidth)) : (circuit function blockSize).ComputesWith DeMorgan.interpretation (scalarTarget function)