Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.BroadcastRecords

Shared broadcast preserving routing metadata #

The concrete scan updates only copied values. Matching keys, tags, and destination ordering metadata remain attached to each record. Its cost is linear in the number of records, with an explicit bit-width factor.

source
def Algebraic.MassProduction.Nonuniform.Broadcast.valuesCircuit (depth keyWidth metadataWidth valueWidth : ℕ) :
Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth (metadataWidth + valueWidth))) (valueWidth * Sorting.networkRecords depth)

Compute every copied-value bit through its shared propagation circuit.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.MassProduction.Nonuniform.Broadcast.valuesCircuit_size (depth keyWidth metadataWidth valueWidth : ℕ) :
    (valuesCircuit depth keyWidth metadataWidth valueWidth).size = ∑ member : Fin valueWidth, (payloadCircuit depth keyWidth (metadataWidth + valueWidth) (Fin.natAdd metadataWidth member)).size

    The exact gate count of valuesCircuit.

    source
    def Algebraic.MassProduction.Nonuniform.Broadcast.outputWire (depth keyWidth metadataWidth valueWidth : ℕ) (output : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))) :
    Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) + valueWidth * Sorting.networkRecords depth)

    Free output wiring retains all fields preceding the copied-value block.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit (depth keyWidth metadataWidth valueWidth : ℕ) :
      Circuit DeMorgan.signature (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))

      One complete record scan with shared wires and preserved metadata.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_size (depth keyWidth metadataWidth valueWidth : ℕ) :
        (recordsCircuit depth keyWidth metadataWidth valueWidth).size = (valuesCircuit depth keyWidth metadataWidth valueWidth).size

        recordsCircuit has exactly the gates of valuesCircuit; the surrounding wiring adds none.

        source
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_eval_preserved {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) (preserved : ↑bit < keyWidth + 1 + metadataWidth) :
        (recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input (finProdFinEquiv (record, bit)) = input (finProdFinEquiv (record, bit))

        Every header and metadata bit is preserved by free output wiring.

        source
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_eval_value {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin valueWidth) :
        RoutingMetadata.recordValue ((recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) record bit = (payloadCircuit depth keyWidth (metadataWidth + valueWidth) (Fin.natAdd metadataWidth bit)).eval DeMorgan.interpretation input record

        The copied-value field consists exactly of the shared broadcast outputs.

        source
        @[simp]
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_recordKey {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) :
        Routing.recordKey ((recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) record = Routing.recordKey input record
        source
        @[simp]
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_recordTag {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) :
        Routing.recordTag ((recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) record = Routing.recordTag input record
        source
        @[simp]
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_recordMetadata {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) :
        RoutingMetadata.recordMetadata ((recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) record = RoutingMetadata.recordMetadata input record
        source
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_routesSorted {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (source destination : Fin (Sorting.networkRecords depth)) (sameKey : Routing.recordKey input source = Routing.recordKey input destination) (sourceTag : Routing.recordTag input source = false) (destinationTag : Routing.recordTag input destination = true) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), Routing.recordKey input index = Routing.recordKey input source → Routing.recordTag input index = false → index = source) :
        RoutingMetadata.recordValue ((recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) destination = RoutingMetadata.recordValue input source

        The record circuit broadcasts the complete value to each destination.

        source
        theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_cost_le {depth keyWidth metadataWidth valueWidth : ℕ} :
        (recordsCircuit depth keyWidth metadataWidth valueWidth).cost DeMorgan.standardCost ≤ Sorting.networkRecords depth * (valueWidth * (6 * keyWidth + 4))

        Exact linear record-count dependence, including all copied value bits.