Documentation

Complexitylib.Algebraic.MassProduction.HighRate.PrefixMetadata

Shared prefix lookup for high-rate request metadata #

One offline table maps each original source prefix to its code-copy, information-point, and basis-bit coordinates. The whole batch shares this table, including repeated prefixes. Suffixes are retained by free wiring.

source
@[reducible, inline]
abbrev Algebraic.MassProduction.HighRate.PrefixMetadata.metadataWidth (dimension width copyBits selectorBits : ℕ) :
ℕ

Information-point bits followed by copy and basis-bit indices.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Algebraic.MassProduction.HighRate.PrefixMetadata.payloadWidth (dimension width copyBits selectorBits suffixWidth : ℕ) :
    ℕ

    One request's metadata followed by its unchanged suffix.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algebraic.MassProduction.HighRate.PrefixMetadata.metadata {width dimension prefixWidth copies : ℕ} (positive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Fin (2 ^ prefixWidth) ↪ InformationBit code copies) (copyBits selectorBits : ℕ) (source : Fin (2 ^ prefixWidth)) :
      Fin (metadataWidth dimension width copyBits selectorBits) → Bool

      Offline metadata for one assigned source bit.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Algebraic.MassProduction.HighRate.PrefixMetadata.targetProjection (dimension width copyBits selectorBits suffixWidth : ℕ) (bit : Fin (dimension * width)) :
        Fin (payloadWidth dimension width copyBits selectorBits suffixWidth)

        Target-field projection inside a processed request.

        Equations
        Instances For
          source
          def Algebraic.MassProduction.HighRate.PrefixMetadata.copyProjection (dimension width copyBits selectorBits suffixWidth : ℕ) (bit : Fin copyBits) :
          Fin (payloadWidth dimension width copyBits selectorBits suffixWidth)

          Copy-index projection inside a processed request.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Algebraic.MassProduction.HighRate.PrefixMetadata.selectorProjection (dimension width copyBits selectorBits suffixWidth : ℕ) (bit : Fin selectorBits) :
            Fin (payloadWidth dimension width copyBits selectorBits suffixWidth)

            Basis-bit projection inside a processed request.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Algebraic.MassProduction.HighRate.PrefixMetadata.suffixProjection (dimension width copyBits selectorBits suffixWidth : ℕ) (bit : Fin suffixWidth) :
              Fin (payloadWidth dimension width copyBits selectorBits suffixWidth)

              Suffix projection inside a processed request.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Algebraic.MassProduction.HighRate.PrefixMetadata.costBound (requests prefixWidth dimension width copyBits selectorBits : ℕ) :
                ℕ

                Cost of one lookup shared by every request.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Algebraic.MassProduction.HighRate.PrefixMetadata.existsCircuit {width dimension prefixWidth copies : ℕ} (positive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Fin (2 ^ prefixWidth) ↪ InformationBit code copies) (requests suffixWidth copyBits selectorBits : ℕ) :
                  ∃ (prepared : Circuit DeMorgan.signature (requests * (prefixWidth + suffixWidth)) (requests * payloadWidth dimension width copyBits selectorBits suffixWidth)), prepared.cost DeMorgan.standardCost ≤ costBound requests prefixWidth dimension width copyBits selectorBits ∧ ∀ (input : Fin (requests * (prefixWidth + suffixWidth)) → Bool) (request : Fin requests) (bit : Fin (payloadWidth dimension width copyBits selectorBits suffixWidth)), prepared.eval DeMorgan.interpretation input (finProdFinEquiv (request, bit)) = Fin.append (metadata positive code placement copyBits selectorBits (RuntimePipeline.requestSource input request)) (RuntimePipeline.requestSuffix input request) bit

                  A concrete preprocessing circuit reads raw prefix/suffix requests and returns their exact offline metadata and retained suffixes.