Documentation

Complexitylib.Algebraic.MassProduction.ScatterAssembly

Scatter routing assembly #

This module turns a grouped scheduler output and the corresponding request suffixes into the fixed record layout consumed by canonical scatter routing. The assembly layer consists only of constants and input wires; the subsequent two-pass routing circuit performs the actual Boolean work.

Scatter inputs #

source
@[reducible]
noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterAssemblyInputCount (groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ) :
ℕ

Scheduler output followed by one suffix for every actual request.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterScheduleInputIndex {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (index : Fin (scheduleBitCount groups requestsPerGroup dimension width)) :
    Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)

    Embed a scheduler-output wire into the scatter-assembly input.

    Equations
    Instances For
      source
      noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterSuffixInputIndex {totalRequests suffixWidth groups requestsPerGroup dimension width : ℕ} (request : Fin totalRequests) (bit : Fin suffixWidth) :
      Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)

      Embed a row-major request-suffix wire into the scatter-assembly input.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterScheduleInput {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) :
        Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool

        Scheduler-output view of the combined scatter-assembly input.

        Equations
        Instances For
          source
          noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterSuffixInput {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) :
          Fin totalRequests → Fin suffixWidth → Bool

          Request-suffix view of the combined scatter-assembly input.

          Equations
          Instances For
            source
            @[simp]
            theorem Algebraic.MassProduction.RoutingAssembly.scatterScheduleInput_append {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (schedule : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool) (suffixes : Fin (totalRequests * suffixWidth) → Bool) :
            scatterScheduleInput (Fin.append schedule suffixes) = schedule
            source
            @[simp]
            theorem Algebraic.MassProduction.RoutingAssembly.scatterSuffixInput_append {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (schedule : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool) (suffixes : Fin (totalRequests * suffixWidth) → Bool) :
            scatterSuffixInput (Fin.append schedule suffixes) = fun (request : Fin totalRequests) (bit : Fin suffixWidth) => suffixes (finProdFinEquiv (request, bit))

            Zero-cost record assembly #

            source
            noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterSourceKeyWiring {totalRequests groups requestsPerGroup width dimension suffixWidth : ℕ} (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) :
            Fin (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) → DeMorgan.Wiring (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)

            A scheduled incidence key consists only of constants and direct scheduler output wires.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Algebraic.MassProduction.RoutingAssembly.scatterSourceKeyWiring_eval {width totalRequests groups requestsPerGroup dimension suffixWidth : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) :
              (fun (bit : Fin (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width)) => DeMorgan.Wiring.eval input (scatterSourceKeyWiring groupBitWidth capacity incidence bit)) = IncidenceRouting.scheduledIncidenceKeyBits widthPositive groupBitWidth capacity (scatterScheduleInput input) incidence
              source
              noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterSourcePayloadWiring {totalRequests width suffixWidth groups requestsPerGroup dimension : ℕ} (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) :
              Fin suffixWidth → DeMorgan.Wiring (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)

              One source payload is a direct copy of its request's suffix wires.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Algebraic.MassProduction.RoutingAssembly.scatterSourcePayloadWiring_eval {groups requestsPerGroup dimension width totalRequests suffixWidth : ℕ} (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) :
                (fun (bit : Fin suffixWidth) => DeMorgan.Wiring.eval input (scatterSourcePayloadWiring incidence bit)) = IncidenceRouting.incidenceSourcePayload (scatterSuffixInput input) incidence
                source
                noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterAssemblySpecification {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth suffixWidth : ℕ} (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)) → DeMorgan.Wiring (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth)

                Zero-gate wiring description of the complete scatter sorter input. Destination and padding payloads are initialized to zero because their prior contents are semantically irrelevant.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterAssemblyCircuit {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth : ℕ} (suffixWidth groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                  Circuit DeMorgan.signature (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth))

                  Scatter record assembly itself uses no Boolean gates.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem Algebraic.MassProduction.RoutingAssembly.scatterAssemblyCircuit_size {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth : ℕ} (suffixWidth groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                    (scatterAssemblyCircuit suffixWidth groupBitWidth capacity recordCount).size = ∑ output : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth)), (scatterAssemblySpecification groupBitWidth capacity recordCount output).expression.gateCount

                    The exact gate count of scatterAssemblyCircuit.

                    source
                    @[simp]
                    theorem Algebraic.MassProduction.RoutingAssembly.scatterAssemblyCircuit_cost {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth suffixWidth : ℕ} (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                    (scatterAssemblyCircuit suffixWidth groupBitWidth capacity recordCount).cost DeMorgan.standardCost = 0
                    source
                    theorem Algebraic.MassProduction.RoutingAssembly.scatterAssemblyCircuit_eval {width totalRequests groups requestsPerGroup dimension paddingCount routingDepth suffixWidth : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) :
                    (scatterAssemblyCircuit suffixWidth groupBitWidth capacity recordCount).eval DeMorgan.interpretation input = IncidenceRouting.fullScatterRoutingInputBits widthPositive groupBitWidth capacity (scatterScheduleInput input) (scatterSuffixInput input) (fun (_destination : Fin (2 ^ (groupBitWidth + dimension * width))) (_bit : Fin suffixWidth) => false) (fun (_padding : Fin paddingCount) (_bit : Fin suffixWidth) => false) recordCount

                    Routed scatter #

                    source
                    noncomputable def Algebraic.MassProduction.RoutingAssembly.scatterRoutingCircuit {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth : ℕ} (suffixWidth groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                    Circuit DeMorgan.signature (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth))

                    Complete scatter routing, including its zero-cost record assembly.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem Algebraic.MassProduction.RoutingAssembly.scatterRoutingCircuit_size {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth : ℕ} (suffixWidth groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                      (scatterRoutingCircuit suffixWidth groupBitWidth capacity recordCount).size = (scatterAssemblyCircuit suffixWidth groupBitWidth capacity recordCount).size + (CanonicalRouting.matchedCanonicalRoutingCircuit routingDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth).size

                      The exact gate count of scatterRoutingCircuit.

                      source
                      @[simp]
                      theorem Algebraic.MassProduction.RoutingAssembly.scatterRoutingCircuit_cost {totalRequests groups requestsPerGroup width dimension paddingCount routingDepth : ℕ} (suffixWidth groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) :
                      (scatterRoutingCircuit suffixWidth groupBitWidth capacity recordCount).cost DeMorgan.standardCost = (CanonicalRouting.matchedCanonicalRoutingCircuit routingDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth).cost DeMorgan.standardCost
                      source
                      theorem Algebraic.MassProduction.RoutingAssembly.scatterRoutingCircuit_eval {width totalRequests groups requestsPerGroup dimension paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (suffixWidth groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) (input : Fin (scatterAssemblyInputCount groups requestsPerGroup dimension width totalRequests suffixWidth) → Bool) :
                      (scatterRoutingCircuit suffixWidth groupBitWidth capacity recordCount).eval DeMorgan.interpretation input = CanonicalScatter.canonicalFullScatterBits widthPositive groupBitWidth capacity (scatterScheduleInput input) (scatterSuffixInput input) (fun (_destination : Fin (2 ^ (groupBitWidth + dimension * width))) (_bit : Fin suffixWidth) => false) (fun (_padding : Fin paddingCount) (_bit : Fin suffixWidth) => false) recordCount