Selecting a successful candidate and its clean prefix

Each candidate consists of flagged request records. First sort the request records of every candidate by their flags. A candidate succeeds precisely when its last required prefix position is flagged. Then sort whole candidate blocks by this success bit and select the first block by free wiring.

The carried candidate blocks may be large, but the outer comparison key is only one bit. The total cost remains linear in the candidate-request product apart from record widths and squared sorting depths.

@[reducible, inline]

abbrev Algebraic.MassProduction.Nonuniform.CandidateSelection.rowBits (requestDepth payloadWidth : ℕ) : ℕ

Bit length of one candidate's request array.

Equations

• Algebraic.MassProduction.Nonuniform.CandidateSelection.rowBits requestDepth payloadWidth = Algebraic.MassProduction.Sorting.networkBits requestDepth (1 + payloadWidth)

def Algebraic.MassProduction.Nonuniform.CandidateSelection.row {menuDepth requestDepth payloadWidth : ℕ} (input : Fin (Sorting.networkRecords menuDepth * rowBits requestDepth payloadWidth) → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) : Fin (rowBits requestDepth payloadWidth) → Bool

One candidate's row in the flat input array.

Equations

• Algebraic.MassProduction.Nonuniform.CandidateSelection.row input candidate bit = input (finProdFinEquiv (candidate, bit))

def Algebraic.MassProduction.Nonuniform.CandidateSelection.rowsCircuit (menuDepth requestDepth payloadWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkRecords menuDepth * Sorting.networkBits requestDepth (1 + payloadWidth)) (Sorting.networkRecords menuDepth * rowBits requestDepth payloadWidth)

Sort each candidate's requests with clean records first.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.CandidateSelection.rowsCircuit_size (menuDepth requestDepth payloadWidth : ℕ) : (rowsCircuit menuDepth requestDepth payloadWidth).size = Sorting.networkRecords menuDepth * (FlagSelection.circuit requestDepth payloadWidth).size

One flag sort per candidate row.

theorem Algebraic.MassProduction.Nonuniform.CandidateSelection.rowsCircuit_eval {menuDepth requestDepth payloadWidth : ℕ} (input : Fin (Sorting.networkRecords menuDepth * rowBits requestDepth payloadWidth) → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) : row ((rowsCircuit menuDepth requestDepth payloadWidth).eval DeMorgan.interpretation input) candidate = (FlagSelection.circuit requestDepth payloadWidth).eval DeMorgan.interpretation (row input candidate)

Each output row is exactly its independent flag sort.

def Algebraic.MassProduction.Nonuniform.CandidateSelection.thresholdIndex (requestDepth payloadWidth needed : ℕ) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : Fin (rowBits requestDepth payloadWidth)

The final position in the required clean prefix.

Equations

• Algebraic.MassProduction.Nonuniform.CandidateSelection.thresholdIndex requestDepth payloadWidth needed positive fits = finProdFinEquiv (⟨needed - 1, ⋯⟩, ⟨0, ⋯⟩)

def Algebraic.MassProduction.Nonuniform.CandidateSelection.packWiring (menuDepth requestDepth payloadWidth needed : ℕ) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) (output : Fin (Sorting.networkBits menuDepth (1 + rowBits requestDepth payloadWidth))) : DeMorgan.Wiring (Sorting.networkRecords menuDepth * rowBits requestDepth payloadWidth)

Add each candidate's success bit before its complete sorted row.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.CandidateSelection.packWiring_eval {needed requestDepth menuDepth payloadWidth : ℕ} (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) (input : Fin (Sorting.networkRecords menuDepth * rowBits requestDepth payloadWidth) → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (bit : Fin (1 + rowBits requestDepth payloadWidth)) : DeMorgan.Wiring.eval input (packWiring menuDepth requestDepth payloadWidth needed positive fits (finProdFinEquiv (candidate, bit))) = Fin.append (fun (x : Fin 1) => FlagSelection.flag (row input candidate) ⟨needed - 1, ⋯⟩) (row input candidate) bit

Packing preserves the row and prefixes its selected threshold flag.

def Algebraic.MassProduction.Nonuniform.CandidateSelection.circuit (menuDepth requestDepth payloadWidth needed : ℕ) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : Circuit DeMorgan.signature (Sorting.networkRecords menuDepth * Sorting.networkBits requestDepth (1 + payloadWidth)) (rowBits requestDepth payloadWidth)

The complete selection circuit returns the first sorted candidate block.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.CandidateSelection.circuit_size (menuDepth requestDepth payloadWidth needed : ℕ) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : (circuit menuDepth requestDepth payloadWidth needed positive fits).size = (rowsCircuit menuDepth requestDepth payloadWidth).size + ((DeMorgan.Wiring.circuit (packWiring menuDepth requestDepth payloadWidth needed positive fits)).size + (FlagSelection.circuit menuDepth (rowBits requestDepth payloadWidth)).size)

Candidate selection has exactly the gates of its row sorts, its packing layer, and its final flag sort.

theorem Algebraic.MassProduction.Nonuniform.CandidateSelection.circuit_selects {needed requestDepth menuDepth payloadWidth : ℕ} (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) (input : Fin (Sorting.networkRecords menuDepth * rowBits requestDepth payloadWidth) → Bool) (available : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), needed ≤ Nat.card { request : Fin (Sorting.networkRecords requestDepth) // FlagSelection.flag (row input candidate) request = true }) : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), (circuit menuDepth requestDepth payloadWidth needed positive fits).eval DeMorgan.interpretation input = (FlagSelection.circuit requestDepth payloadWidth).eval DeMorgan.interpretation (row input candidate) ∧ ∀ (request : Fin (Sorting.networkRecords requestDepth)), ↑request < needed → FlagSelection.flag ((circuit menuDepth requestDepth payloadWidth needed positive fits).eval DeMorgan.interpretation input) request = true

If any candidate has enough clean requests, the selected complete row comes from one candidate and all required prefix positions are clean.

theorem Algebraic.MassProduction.Nonuniform.CandidateSelection.circuit_cost_le {needed requestDepth menuDepth payloadWidth : ℕ} (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : (circuit menuDepth requestDepth payloadWidth needed positive fits).cost DeMorgan.standardCost ≤ Sorting.networkRecords menuDepth * (48 * requestDepth * requestDepth * Sorting.networkRecords requestDepth * (1 + payloadWidth)) + 48 * menuDepth * menuDepth * Sorting.networkRecords menuDepth * (1 + rowBits requestDepth payloadWidth)

Explicit cost for inner request sorts and the outer candidate-block sort.