Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.FlaggedRows

Carrying request payloads beside computed clean flags #

The complete clean-flag circuit runs once. A free wiring layer adds each request's original payload and presents the resulting records in the nested candidate/request layout expected by the candidate-selection circuit.

source
theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.recordIndex_assoc {candidates requests width : ℕ} (candidate : Fin candidates) (request : Fin requests) (bit : Fin width) :
Fin.cast ⋯ (finProdFinEquiv (candidate, finProdFinEquiv (request, bit))) = finProdFinEquiv (finProdFinEquiv (candidate, request), bit)

Nested and flattened row-major record indices agree.

source
def Algebraic.MassProduction.Nonuniform.FlaggedRows.flagsArrayCircuit {inputs menuDepth requestDepth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) :
Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth * 1)

Regard the computed flags as an array of width-one records.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.flagsArrayCircuit_size {inputs menuDepth requestDepth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) :
    (flagsArrayCircuit flags).size = flags.size

    The exact gate count of flagsArrayCircuit.

    source
    def Algebraic.MassProduction.Nonuniform.FlaggedRows.payloadCircuit {menuDepth requestDepth payloadWidth inputs : ℕ} (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) :
    Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth * payloadWidth)

    The request payloads are selected by free wiring.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.payloadCircuit_size {menuDepth requestDepth payloadWidth inputs : ℕ} (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) :
      (payloadCircuit payloads).size = ∑ record : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth), ∑ bit : Fin payloadWidth, (payloads record bit).expression.gateCount

      The exact gate count of payloadCircuit: one gate for every payload bit wired to a constant, and none for bits wired to inputs.

      source
      def Algebraic.MassProduction.Nonuniform.FlaggedRows.circuit {inputs menuDepth requestDepth payloadWidth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) :
      Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * (Sorting.networkRecords requestDepth * (1 + payloadWidth)))

      Assemble the complete flagged rows without copying the flag computation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.circuit_size {inputs menuDepth requestDepth payloadWidth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) :
        (circuit flags payloads).size = (RecordArray.combine (flagsArrayCircuit flags) (payloadCircuit payloads)).size

        circuit has exactly the gates of RecordArray.combine; the surrounding wiring adds none.

        source
        theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.circuit_eval_record {inputs menuDepth requestDepth payloadWidth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) :
        Sorting.flatRecords (CandidateSelection.row ((circuit flags payloads).eval DeMorgan.interpretation input) candidate) request = Fin.append (fun (x : Fin 1) => flags.eval DeMorgan.interpretation input (finProdFinEquiv (candidate, request))) fun (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (payloads (finProdFinEquiv (candidate, request)) bit)

        Each candidate/request record has its computed flag and original payload.

        source
        theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.circuit_eval_flag {inputs menuDepth requestDepth payloadWidth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) :
        FlagSelection.flag (CandidateSelection.row ((circuit flags payloads).eval DeMorgan.interpretation input) candidate) request = flags.eval DeMorgan.interpretation input (finProdFinEquiv (candidate, request))

        The selection flag is exactly the computed clean flag.

        source
        theorem Algebraic.MassProduction.Nonuniform.FlaggedRows.circuit_cost {inputs menuDepth requestDepth payloadWidth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) :
        (circuit flags payloads).cost DeMorgan.standardCost = flags.cost DeMorgan.standardCost

        Adding the payloads and regrouping the rows adds no charged gates.