Documentation

Complexitylib.Algebraic.MassProduction.LupanovPatternBank

Lupanov pattern banks #

This module constructs the address-side and data-side pattern-recognition banks used by finite Lupanov synthesis. It proves their exact output semantics and cost ledgers before any final recombination is performed.

The two pattern banks #

source
noncomputable def Algebraic.MassProduction.LupanovSynthesis.leftTerm (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) (offset : Fin blockSize) :
DeMorgan.Expression (2 ^ addressWidth)

One possible row of a block pattern, gated by its address minterm.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.MassProduction.LupanovSynthesis.leftTerm_standardCost (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) (offset : Fin blockSize) :
    (leftTerm addressWidth blockSize block pattern offset).standardCost = 0
    source
    @[simp]
    theorem Algebraic.MassProduction.LupanovSynthesis.leftTerm_eval (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) (offset : Fin blockSize) (flags : Fin (2 ^ addressWidth) → Bool) :
    DeMorgan.Expression.eval flags (leftTerm addressWidth blockSize block pattern offset) = if rowValid : ↑block * blockSize + ↑offset < 2 ^ addressWidth then flags ⟨↑block * blockSize + ↑offset, rowValid⟩ && ShannonSynthesis.assignmentBits blockSize pattern offset else false
    source
    noncomputable def Algebraic.MassProduction.LupanovSynthesis.leftExpression (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) :
    DeMorgan.Expression (2 ^ addressWidth)

    Address-side recognizer of one pattern in one block.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.MassProduction.LupanovSynthesis.leftExpression_standardCost (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) :
      (leftExpression addressWidth blockSize block pattern).standardCost = blockSize
      source
      @[reducible]
      noncomputable def Algebraic.MassProduction.LupanovSynthesis.leftBlockGateCount (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
      ℕ

      Program-gate count of all left recognizers for one block.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algebraic.MassProduction.LupanovSynthesis.leftBlockCircuit (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
        Circuit DeMorgan.signature (2 ^ addressWidth) (patternCount blockSize)

        All address-side pattern recognizers for one block.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Algebraic.MassProduction.LupanovSynthesis.leftBlockCircuit_size (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
          (leftBlockCircuit addressWidth blockSize block).size = leftBlockGateCount addressWidth blockSize block
          source
          @[simp]
          theorem Algebraic.MassProduction.LupanovSynthesis.leftBlockCircuit_eval (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (flags : Fin (2 ^ addressWidth) → Bool) (pattern : Fin (patternCount blockSize)) :
          (leftBlockCircuit addressWidth blockSize block).eval DeMorgan.interpretation flags pattern = DeMorgan.Expression.eval flags (leftExpression addressWidth blockSize block pattern)
          source
          theorem Algebraic.MassProduction.LupanovSynthesis.leftBlockCircuit_cost (addressWidth blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
          (leftBlockCircuit addressWidth blockSize block).cost DeMorgan.standardCost = patternCount blockSize * blockSize
          source
          @[reducible]
          noncomputable def Algebraic.MassProduction.LupanovSynthesis.rightBlockGateCount {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
          ℕ

          Program-gate count of all sparse right recognizers for one block.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Algebraic.MassProduction.LupanovSynthesis.rightBlockCircuit {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
            Circuit DeMorgan.signature (2 ^ dataWidth) (patternCount blockSize)

            All sparse data-side pattern recognizers for one block.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Algebraic.MassProduction.LupanovSynthesis.rightBlockCircuit_size {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
              (rightBlockCircuit function blockSize block).size = rightBlockGateCount function blockSize block
              source
              @[simp]
              theorem Algebraic.MassProduction.LupanovSynthesis.rightBlockCircuit_eval {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) (flags : Fin (2 ^ dataWidth) → Bool) (pattern : Fin (patternCount blockSize)) :
              (rightBlockCircuit function blockSize block).eval DeMorgan.interpretation flags pattern = DeMorgan.Expression.eval flags (rightExpression function block pattern)
              source
              theorem Algebraic.MassProduction.LupanovSynthesis.rightBlockCircuit_cost {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (block : Fin (blockCount addressWidth blockSize)) :
              (rightBlockCircuit function blockSize block).cost DeMorgan.standardCost = 2 ^ dataWidth
              source
              @[reducible]
              noncomputable def Algebraic.MassProduction.LupanovSynthesis.leftBankGateCount (addressWidth blockSize : ℕ) :
              ℕ

              Program-gate count of the complete address-side pattern bank.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def Algebraic.MassProduction.LupanovSynthesis.leftBankCircuit (addressWidth dataWidth blockSize : ℕ) :
                Circuit DeMorgan.signature (2 ^ addressWidth + 2 ^ dataWidth) (blockCount addressWidth blockSize * patternCount blockSize)

                The address-side pattern banks, flattened in (block, pattern) order.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem Algebraic.MassProduction.LupanovSynthesis.leftBankCircuit_size (addressWidth dataWidth blockSize : ℕ) :
                  (leftBankCircuit addressWidth dataWidth blockSize).size = leftBankGateCount addressWidth blockSize
                  source
                  @[simp]
                  theorem Algebraic.MassProduction.LupanovSynthesis.leftBankCircuit_eval (addressWidth dataWidth blockSize : ℕ) (state : Fin (2 ^ addressWidth + 2 ^ dataWidth) → Bool) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) :
                  (leftBankCircuit addressWidth dataWidth blockSize).eval DeMorgan.interpretation state (finProdFinEquiv (block, pattern)) = DeMorgan.Expression.eval (fun (address : Fin (2 ^ addressWidth)) => state (Fin.castAdd (2 ^ dataWidth) address)) (leftExpression addressWidth blockSize block pattern)
                  source
                  theorem Algebraic.MassProduction.LupanovSynthesis.leftBankCircuit_cost (addressWidth dataWidth blockSize : ℕ) :
                  (leftBankCircuit addressWidth dataWidth blockSize).cost DeMorgan.standardCost = blockCount addressWidth blockSize * (patternCount blockSize * blockSize)
                  source
                  @[reducible]
                  noncomputable def Algebraic.MassProduction.LupanovSynthesis.rightBankGateCount {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) :
                  ℕ

                  Program-gate count of the complete data-side pattern bank.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def Algebraic.MassProduction.LupanovSynthesis.rightBankCircuit {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) :
                    Circuit DeMorgan.signature (2 ^ addressWidth + 2 ^ dataWidth) (blockCount addressWidth blockSize * patternCount blockSize)

                    The data-side sparse pattern banks, flattened in (block, pattern) order.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem Algebraic.MassProduction.LupanovSynthesis.rightBankCircuit_size {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) :
                      (rightBankCircuit function blockSize).size = rightBankGateCount function blockSize
                      source
                      @[simp]
                      theorem Algebraic.MassProduction.LupanovSynthesis.rightBankCircuit_eval {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) (state : Fin (2 ^ addressWidth + 2 ^ dataWidth) → Bool) (block : Fin (blockCount addressWidth blockSize)) (pattern : Fin (patternCount blockSize)) :
                      (rightBankCircuit function blockSize).eval DeMorgan.interpretation state (finProdFinEquiv (block, pattern)) = DeMorgan.Expression.eval (fun (data : Fin (2 ^ dataWidth)) => state (Fin.natAdd (2 ^ addressWidth) data)) (rightExpression function block pattern)
                      source
                      theorem Algebraic.MassProduction.LupanovSynthesis.rightBankCircuit_cost {addressWidth dataWidth : ℕ} (function : ScalarFunction Bool (addressWidth + dataWidth)) (blockSize : ℕ) :
                      (rightBankCircuit function blockSize).cost DeMorgan.standardCost = blockCount addressWidth blockSize * 2 ^ dataWidth