Selecting flagged records by sorting

Sorting a one-bit flag in decreasing order moves all flagged records to the front while preserving complete records. A requested number of flagged records can therefore be selected by fixed output wires, with no prefix counter. This is the selection primitive for a halving scheduler phase.

def Algebraic.MassProduction.Nonuniform.FlagSelection.flag {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Bool

First bit of a record; remaining bits are carried as payload.

Equations

• Algebraic.MassProduction.Nonuniform.FlagSelection.flag input record = input (finProdFinEquiv (record, ⟨0, ⋯⟩))

def Algebraic.MassProduction.Nonuniform.FlagSelection.circuit (depth payloadWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (1 + payloadWidth)) (Sorting.networkBits depth (1 + payloadWidth))

Sort by the first bit with flagged records first.

Equations

• Algebraic.MassProduction.Nonuniform.FlagSelection.circuit depth payloadWidth = Algebraic.MassProduction.Sorting.bitonicSortCircuit ⋯ depth false

@[simp]

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_size (depth payloadWidth : ℕ) : (circuit depth payloadWidth).size = Sorting.bitonicSortGateCount ⋯ depth

Flag selection is exactly one bitonic sort.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.key_le_iff {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) (left right : Fin (Sorting.networkRecords depth)) : Sorting.flatRecordKey ⋯ (Sorting.flatRecords input left) ≤ Sorting.flatRecordKey ⋯ (Sorting.flatRecords input right) ↔ flag input left ≤ flag input right

The one-bit key order is the ordinary order on Boolean flags.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_flagsAntitone {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) : Antitone (flag ((circuit depth payloadWidth).eval DeMorgan.interpretation input))

The concrete sort puts true flags before false flags.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_flagCount {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) : Nat.card { record : Fin (Sorting.networkRecords depth) // flag ((circuit depth payloadWidth).eval DeMorgan.interpretation input) record = true } = Nat.card { record : Fin (Sorting.networkRecords depth) // flag input record = true }

Sorting preserves the number of flagged records exactly.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.flag_true_of_lt_count {count : ℕ} (flags : Fin count → Bool) (ordered : Antitone flags) (index : Fin count) (enough : ↑index < Nat.card { position : Fin count // flags position = true }) : flags index = true

In a decreasing Boolean sequence, every position below the count of true entries is true.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_selects {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) (needed : ℕ) (enough : needed ≤ Nat.card { record : Fin (Sorting.networkRecords depth) // flag input record = true }) (index : Fin (Sorting.networkRecords depth)) (selected : ↑index < needed) : flag ((circuit depth payloadWidth).eval DeMorgan.interpretation input) index = true

Fixed prefix positions select any requested number of available flagged records. The actual complete records are preserved by the sorting network.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_recordsPermute {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) : Sorting.FlatRecordsPermute ((circuit depth payloadWidth).eval DeMorgan.interpretation input) input

Complete records, including request identifiers, survive selection sorting.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_firstFlagged {depth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (1 + payloadWidth)) → Bool) (available : ∃ (record : Fin (Sorting.networkRecords depth)), flag input record = true) : ∃ (source : Fin (Sorting.networkRecords depth)), flag input source = true ∧ Sorting.flatRecords ((circuit depth payloadWidth).eval DeMorgan.interpretation input) ⟨0, ⋯⟩ = Sorting.flatRecords input source

If some record is flagged, the first output is a complete flagged input record. Thus a flag sort also selects one successful candidate block.

theorem Algebraic.MassProduction.Nonuniform.FlagSelection.circuit_cost_le {depth payloadWidth : ℕ} : (circuit depth payloadWidth).cost DeMorgan.standardCost ≤ 48 * depth * depth * Sorting.networkRecords depth * (1 + payloadWidth)

Flag sorting costs at most forty-eight gates per record bit per squared network depth. Its key width is one even for a large carried payload.