Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.BatchRouting

Two-sort batched routing with repeated matching keys #

The first sort places a unique source before arbitrarily many destinations. The shared scan broadcasts values while preserving destination identifiers. The second sort returns results to fixed output positions. All operations are explicit De Morgan circuits with an additive cost bound.

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

Sorting by matching key and tag, followed by shared value broadcast.

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

    The bitonic sort followed by the value broadcast.

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

    The complete two-sort batched router.

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

      The exact gate count of routingCircuit.

      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.Broadcast.recordsCircuit_complementedHeader {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) :
      CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords ((recordsCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) record) = CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)
      source
      theorem Algebraic.MassProduction.Nonuniform.Broadcast.sortedCircuit_headersPermute {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) :
      Sorting.Semantics.SequencePermutes (fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords ((sortedCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) record)) fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)

      Matching and broadcast preserve the complete multiset of destination identifiers, including padding identifiers.

      source
      theorem Algebraic.MassProduction.Nonuniform.Broadcast.sortedCircuit_valueCorrect {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (header : Lex (Fin (metadataWidth + 1) → Bool)) (key : Fin keyWidth → Bool) (value : Fin valueWidth → Bool) (uniqueSource : Sorting.Semantics.UniqueIndexWhere (Sorting.flatRecords input) (Routing.recordHasKeyTag key false)) (sourceCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), Routing.recordKey input record = key → Routing.recordTag input record = false → RoutingMetadata.recordValue input record = value) (queryCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record) = header → Routing.recordKey input record = key ∧ Routing.recordTag input record = true) (destination : Fin (Sorting.networkRecords depth)) (destinationHeader : CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords ((sortedCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) destination) = header) :
      RoutingMetadata.recordValue ((sortedCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) destination = value

      Every destination header specifying the query key receives the value of its unique source. Destination keys may repeat.

      source
      theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingCircuit_fixedValue {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (header : Lex (Fin (metadataWidth + 1) → Bool)) (target : Fin (Sorting.networkRecords depth)) (key : Fin keyWidth → Bool) (value : Fin valueWidth → Bool) (uniqueHeader : Sorting.Semantics.UniqueIndexWhere (fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)) fun (candidate : Lex (Fin (metadataWidth + 1) → Bool)) => candidate = header) (rank : (Sorting.Semantics.matchingIndices (fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)) fun (candidate : Lex (Fin (metadataWidth + 1) → Bool)) => candidate < header).card = ↑target) (uniqueSource : Sorting.Semantics.UniqueIndexWhere (Sorting.flatRecords input) (Routing.recordHasKeyTag key false)) (sourceCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), Routing.recordKey input record = key → Routing.recordTag input record = false → RoutingMetadata.recordValue input record = value) (queryCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record) = header → Routing.recordKey input record = key ∧ Routing.recordTag input record = true) :
      RoutingMetadata.recordValue ((routingCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) target = value

      The concrete two-sort circuit returns each lookup result to the fixed output position determined by its unique destination identifier.

      source
      theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingCircuit_cost_le {depth keyWidth metadataWidth valueWidth : ℕ} :
      (routingCircuit depth keyWidth metadataWidth valueWidth).cost DeMorgan.standardCost ≤ depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth * (2 * ((keyWidth + 1) * (6 * (keyWidth + 1) + 4)) + 4)) + Sorting.networkRecords depth * (valueWidth * (6 * keyWidth + 4)) + (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) + depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth * (2 * ((metadataWidth + 1) * (6 * (metadataWidth + 1) + 4)) + 4)))

      The two sorts and shared scan have linear dependence on the record count, with polynomial factors in depth and record-field widths.