Documentation

Complexitylib.Algebraic.MassProduction.ScheduledRoutingWiring

Scheduled-incidence routing wiring #

This module identifies each affine-point bit in the grouped scheduler output with the corresponding incidence-key wire. It is the narrow bridge from the semantic schedule to the zero-cost routing-record wiring layer; assembly of the scatter and gather records is kept in the focused ScatterAssembly and GatherAssembly modules.

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

Number of Boolean wires in one grouped scheduler output.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.MassProduction.RoutingAssembly.scheduledIncidencePointBitIndex {totalRequests groups requestsPerGroup width dimension : ℕ} (capacity : totalRequests ≤ groups * requestsPerGroup) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (pointBit : Fin (dimension * width)) :
    Fin (scheduleBitCount groups requestsPerGroup dimension width)

    Scheduler-output wire containing one affine-point bit of a flattened scheduled incidence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.MassProduction.RoutingAssembly.scheduledIncidencePointBit {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) (pointBit : Fin (dimension * width)) :
      binaryExtensionVectorBits widthPositive (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).2 pointBit = scheduleOutput (scheduledIncidencePointBitIndex capacity incidence pointBit)

      Decoding and re-encoding a scheduled point is exactly the corresponding scheduler-output block.

      source
      theorem Algebraic.MassProduction.RoutingAssembly.scheduledIncidenceKeyBits_eq_wiring {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (scheduleBitCount groups requestsPerGroup dimension width) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) :
      IncidenceRouting.scheduledIncidenceKeyBits widthPositive groupBitWidth capacity scheduleOutput incidence = activeRoutingKey (Fin.append (finiteIndexBits groupBitWidth (IncidenceRouting.scheduledIncidenceSlotAt widthPositive capacity scheduleOutput incidence).1) fun (pointBit : Fin (dimension * width)) => scheduleOutput (scheduledIncidencePointBitIndex capacity incidence pointBit))

      Scheduled matching keys are a constant active marker and group prefix followed by scheduler-output point wires.