Routing records with preserved ordering metadata

Gather records are matched by (group, point) but finally ordered by (request, line position). These are different keys. This module extends the basic record layout to

(matching key, tag, preserved metadata, copied value).

The predecessor pass updates only the value field of a matched destination; its ordering metadata stays with the destination record. This is the exact layout needed for the manuscript's two gather sorts.

@[reducible, inline]

abbrev Algebraic.MassProduction.RoutingMetadata.recordWidth (keyWidth metadataWidth valueWidth : ℕ) : ℕ

Width of a routing record with an additional preserved metadata field.

Equations

• Algebraic.MassProduction.RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth = Algebraic.MassProduction.Routing.recordWidth keyWidth (metadataWidth + valueWidth)

def Algebraic.MassProduction.RoutingMetadata.metadataBit (keyWidth metadataWidth valueWidth : ℕ) (bit : Fin metadataWidth) : Fin (recordWidth keyWidth metadataWidth valueWidth)

Physical index of one metadata bit.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.valueBit (keyWidth metadataWidth valueWidth : ℕ) (bit : Fin valueWidth) : Fin (recordWidth keyWidth metadataWidth valueWidth)

Physical index of one copied-value bit.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.recordMetadata {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Fin metadataWidth → Bool

Metadata projection from one flat record array.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.recordValue {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Fin valueWidth → Bool

Copied-value projection from one flat record array.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.packRecord {keyWidth metadataWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (metadata : Fin metadataWidth → Bool) (value : Fin valueWidth → Bool) : Fin (recordWidth keyWidth metadataWidth valueWidth) → Bool

Pack one metadata-aware routing record.

Equations

• Algebraic.MassProduction.RoutingMetadata.packRecord key tag metadata value = Algebraic.MassProduction.Routing.packRecord key tag (Fin.append metadata value)

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.packedRecordKey_packRecord {keyWidth metadataWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (metadata : Fin metadataWidth → Bool) (value : Fin valueWidth → Bool) : Routing.packedRecordKey (packRecord key tag metadata value) = key

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.packedRecordTag_packRecord {keyWidth metadataWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (metadata : Fin metadataWidth → Bool) (value : Fin valueWidth → Bool) : Routing.packedRecordTag (packRecord key tag metadata value) = tag

def Algebraic.MassProduction.RoutingMetadata.packedRecordMetadata {keyWidth metadataWidth valueWidth : ℕ} (record : Fin (recordWidth keyWidth metadataWidth valueWidth) → Bool) : Fin metadataWidth → Bool

Metadata projection from one standalone record.

Equations

• Algebraic.MassProduction.RoutingMetadata.packedRecordMetadata record bit = record (Algebraic.MassProduction.RoutingMetadata.metadataBit keyWidth metadataWidth valueWidth bit)

def Algebraic.MassProduction.RoutingMetadata.packedRecordValue {keyWidth metadataWidth valueWidth : ℕ} (record : Fin (recordWidth keyWidth metadataWidth valueWidth) → Bool) : Fin valueWidth → Bool

Value projection from one standalone record.

Equations

• Algebraic.MassProduction.RoutingMetadata.packedRecordValue record bit = record (Algebraic.MassProduction.RoutingMetadata.valueBit keyWidth metadataWidth valueWidth bit)

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.packedRecordMetadata_packRecord {keyWidth metadataWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (metadata : Fin metadataWidth → Bool) (value : Fin valueWidth → Bool) : packedRecordMetadata (packRecord key tag metadata value) = metadata

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.packedRecordValue_packRecord {keyWidth metadataWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (metadata : Fin metadataWidth → Bool) (value : Fin valueWidth → Bool) : packedRecordValue (packRecord key tag metadata value) = value

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.packedRecordMetadata_flatRecords {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : packedRecordMetadata (Sorting.flatRecords input record) = recordMetadata input record

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.packedRecordValue_flatRecords {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : packedRecordValue (Sorting.flatRecords input record) = recordValue input record

Guarded value-only predecessor copy

def Algebraic.MassProduction.RoutingMetadata.predecessorCopyOutputExpression (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) (output : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth))) : DeMorgan.Expression (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth))

One output formula. Headers and metadata are preserved; only the final value field is conditionally copied.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool

Semantic value-only predecessor copy.

Equations

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

@[reducible]

def Algebraic.MassProduction.RoutingMetadata.predecessorCopyOutputGateCount (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) (output : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth))) : ℕ

Gate count of one output expression in the value-only predecessor-copy pass.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.predecessorCopyCircuit (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) : Circuit DeMorgan.signature (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth))

Explicit complete value-only copy pass.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyCircuit_size (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) : (predecessorCopyCircuit depth keyWidth metadataWidth valueWidth sourceTag destinationTag).size = ∑ output : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)), predecessorCopyOutputGateCount depth keyWidth metadataWidth valueWidth sourceTag destinationTag output

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyCircuit_eval {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) : (predecessorCopyCircuit depth keyWidth metadataWidth valueWidth sourceTag destinationTag).eval DeMorgan.interpretation input = predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits_recordKey {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Routing.recordKey (predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) record = Routing.recordKey input record

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits_recordTag {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Routing.recordTag (predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) record = Routing.recordTag input record

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits_recordMetadata {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordMetadata (predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) record = recordMetadata input record

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits_recordValue_of_positive {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) : recordValue (predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) current = if DeMorgan.Expression.eval input (Routing.predecessorMatchExpression depth keyWidth (metadataWidth + valueWidth) sourceTag destinationTag current positive) = true then recordValue input (Routing.predecessor current positive) else fun (x : Fin valueWidth) => false

A positive record copies the predecessor value exactly when the same key/tag guard succeeds.

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits_recordValue_of_match {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (current : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑current) (sameKey : Routing.recordKey input (Routing.predecessor current positive) = Routing.recordKey input current) (previousTag : Routing.recordTag input (Routing.predecessor current positive) = sourceTag) (currentTag : Routing.recordTag input current = destinationTag) : recordValue (predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) current = recordValue input (Routing.predecessor current positive)

A correctly tagged same-key predecessor is copied exactly.

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyBits_recordValue_of_sorted_unique {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (source destination : Fin (Sorting.networkRecords depth)) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), Routing.recordKeyAndTag input index = Routing.recordKeyAndTag input source → index = source) (destinationUnique : ∀ (index : Fin (Sorting.networkRecords depth)), Routing.recordKeyAndTag input index = Routing.recordKeyAndTag input destination → index = destination) (sameKey : Routing.recordKey input source = Routing.recordKey input destination) (sourceTag : Routing.recordTag input source = false) (destinationTag : Routing.recordTag input destination = true) : recordValue (predecessorCopyBits depth keyWidth metadataWidth valueWidth false true input) destination = recordValue input source

In a sorted array, a uniquely occurring same-key source/destination pair routes its value while leaving destination metadata untouched.

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyOutputExpression_standardCost_le {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (output : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth))) : (predecessorCopyOutputExpression depth keyWidth metadataWidth valueWidth sourceTag destinationTag output).standardCost ≤ 12 * keyWidth + 12

theorem Algebraic.MassProduction.RoutingMetadata.predecessorCopyCircuit_cost_le {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) : (predecessorCopyCircuit depth keyWidth metadataWidth valueWidth sourceTag destinationTag).cost DeMorgan.standardCost ≤ Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth) * (12 * keyWidth + 12)

Sort and value-copy composition

@[reducible]

def Algebraic.MassProduction.RoutingMetadata.sortedPredecessorCopyGateCount (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) : ℕ

Total gate count of sorting followed by value-only predecessor copying.

Equations

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

def Algebraic.MassProduction.RoutingMetadata.sortedPredecessorCopyCircuit (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) : Circuit DeMorgan.signature (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth))

Sort by (matching key, tag) and copy only the value field.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.sortedPredecessorCopyCircuit_size (depth keyWidth metadataWidth valueWidth : ℕ) (sourceTag destinationTag : Bool) : (sortedPredecessorCopyCircuit depth keyWidth metadataWidth valueWidth sourceTag destinationTag).size = sortedPredecessorCopyGateCount depth keyWidth metadataWidth valueWidth sourceTag destinationTag

@[simp]

theorem Algebraic.MassProduction.RoutingMetadata.sortedPredecessorCopyCircuit_eval {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) : (sortedPredecessorCopyCircuit depth keyWidth metadataWidth valueWidth sourceTag destinationTag).eval DeMorgan.interpretation input = predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag (Sorting.bitonicSortBits ⋯ depth true input)

theorem Algebraic.MassProduction.RoutingMetadata.sortedPredecessorCopyCircuit_cost_le {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) : (sortedPredecessorCopyCircuit depth keyWidth metadataWidth valueWidth sourceTag destinationTag).cost DeMorgan.standardCost ≤ depth * depth * Sorting.networkRecords depth * (2 * recordWidth keyWidth metadataWidth valueWidth * (2 * ((keyWidth + 1) * (6 * (keyWidth + 1) + 4)) + 4)) + Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth) * (12 * keyWidth + 12)

Packing-friendly correctness API

theorem Algebraic.MassProduction.RoutingMetadata.sortedPredecessorCopyCircuit_routes_unique_key {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth metadataWidth valueWidth)) → Bool) (key : Fin keyWidth → Bool) (uniqueSource : Sorting.Semantics.UniqueIndexWhere (Sorting.flatRecords input) (Routing.recordHasKeyTag key false)) (uniqueDestination : Sorting.Semantics.UniqueIndexWhere (Sorting.flatRecords input) (Routing.recordHasKeyTag key true)) : have sorted := Sorting.bitonicSortBits ⋯ depth true input; ∃ (sourceInput : Fin (Sorting.networkRecords depth)) (sourceSorted : Fin (Sorting.networkRecords depth)) (destinationSorted : Fin (Sorting.networkRecords depth)), Routing.recordHasKeyTag key false (Sorting.flatRecords input sourceInput) ∧ Routing.recordHasKeyTag key false (Sorting.flatRecords sorted sourceSorted) ∧ Routing.recordHasKeyTag key true (Sorting.flatRecords sorted destinationSorted) ∧ recordValue ((sortedPredecessorCopyCircuit depth keyWidth metadataWidth valueWidth false true).eval DeMorgan.interpretation input) destinationSorted = packedRecordValue (Sorting.flatRecords input sourceInput)

Sorting and value-only predecessor copying routes a unique source value to the unique same-key destination.