Correctness of sorted predecessor routing

The local routing scan is useful only after proving that its intended source really is the destination's immediate predecessor. This module isolates that order-theoretic argument. A strictly covered pair of unique keys must occupy adjacent positions in an increasing finite sequence; applying that fact to the verified Batcher output makes the guarded predecessor copy exact.

Transporting unique records through a sorting permutation

@[reducible, inline]

abbrev Algebraic.MassProduction.Routing.UniqueIndexWhere {n : ℕ} {α : Sort u_1} (sequence : Fin n → α) (predicate : α → Prop) : Prop

Routing-namespace compatibility alias for the generic finite-sequence uniqueness predicate.

Equations

• Algebraic.MassProduction.Routing.UniqueIndexWhere sequence predicate = Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere sequence predicate

@[reducible, inline]

noncomputable abbrev Algebraic.MassProduction.Routing.matchingIndices {n : ℕ} {α : Sort u_1} (sequence : Fin n → α) (predicate : α → Prop) : Finset (Fin n)

Routing-namespace compatibility alias for generic matching positions.

Equations

• Algebraic.MassProduction.Routing.matchingIndices sequence predicate = Algebraic.MassProduction.Sorting.Semantics.matchingIndices sequence predicate

@[reducible, inline]

noncomputable abbrev Algebraic.MassProduction.Routing.predicateBit {α : Sort u_1} (predicate : α → Prop) (value : α) : Bool

Routing-namespace compatibility alias for generic predicate reflection.

Equations

• Algebraic.MassProduction.Routing.predicateBit predicate value = Algebraic.MassProduction.Sorting.Semantics.predicateBit predicate value

theorem Algebraic.MassProduction.Routing.uniqueIndexWhere_iff_filter_card_eq_one {n : ℕ} {α : Sort u_1} (sequence : Fin n → α) (predicate : α → Prop) : UniqueIndexWhere sequence predicate ↔ (matchingIndices sequence predicate).card = 1

Routing-namespace compatibility theorem for unique matching positions.

theorem Algebraic.MassProduction.Routing.countP_ofFn_eq_filter_card {n : ℕ} {α : Type u_1} (sequence : Fin n → α) (predicate : α → Prop) : List.countP (predicateBit predicate) (List.ofFn sequence) = (matchingIndices sequence predicate).card

Routing-namespace compatibility theorem for predicate counting.

theorem Algebraic.MassProduction.Routing.UniqueIndexWhere.of_sequencePermutes {n : ℕ} {α : Type u_1} {output input : Fin n → α} {predicate : α → Prop} (permuted : Sorting.Semantics.SequencePermutes output input) (uniqueInput : UniqueIndexWhere input predicate) : UniqueIndexWhere output predicate

Routing-namespace compatibility theorem for transporting a unique match through a finite-sequence permutation.

theorem Algebraic.MassProduction.Routing.UniqueIndexWhere.of_flatRecordsPermute {depth packedWidth : ℕ} {output input : Fin (Sorting.networkBits depth packedWidth) → Bool} {predicate : (Fin packedWidth → Bool) → Prop} (permuted : Sorting.FlatRecordsPermute output input) (uniqueInput : UniqueIndexWhere (Sorting.flatRecords input) predicate) : UniqueIndexWhere (Sorting.flatRecords output) predicate

Routing-namespace compatibility theorem for transporting a unique record predicate through packed sorting.

theorem Algebraic.MassProduction.Routing.SequencePermutes.rangeContained {n : ℕ} {α : Type u_1} {output input : Fin n → α} (permuted : Sorting.Semantics.SequencePermutes output input) : Sorting.Semantics.SequenceRangeContained output input

Routing-namespace compatibility theorem for the generic sequence result.

theorem Algebraic.MassProduction.Routing.FlatRecordsPermute.rangeContained {depth packedWidth : ℕ} {output input : Fin (Sorting.networkBits depth packedWidth) → Bool} (permuted : Sorting.FlatRecordsPermute output input) : Sorting.Semantics.SequenceRangeContained (Sorting.flatRecords output) (Sorting.flatRecords input)

theorem Algebraic.MassProduction.Routing.adjacent_indices_of_increasing_covBy {κ : Type u_1} {n : ℕ} [LinearOrder κ] (sequence : Fin n → κ) (increasing : Sorting.Semantics.SequenceIncreasing sequence) (source destination : Fin n) (covered : sequence source ⋖ sequence destination) (sourceUnique : ∀ (index : Fin n), sequence index = sequence source → index = source) (destinationUnique : ∀ (index : Fin n), sequence index = sequence destination → index = destination) : ↑destination = ↑source + 1

In an increasing finite sequence, two uniquely occurring keys related by CovBy occupy adjacent indices.

def Algebraic.MassProduction.Routing.keyWithTag {keyWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) : Fin (keyWidth + 1) → Bool

Append the source/destination tag after all routing-key bits.

Equations

• Algebraic.MassProduction.Routing.keyWithTag key tag = Fin.snoc key tag

theorem Algebraic.MassProduction.Routing.keyWithTag_false_covBy_true {keyWidth : ℕ} (key : Fin keyWidth → Bool) : toLex (keyWithTag key false) ⋖ toLex (keyWithTag key true)

There is no lexicographic Boolean key strictly between a fixed key tagged as a source and the same key tagged as a destination.

def Algebraic.MassProduction.Routing.recordKeyAndTag {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Lex (Fin (keyWidth + 1) → Bool)

The key used by a scatter/gather matching pass: physical key bits followed by the source/destination tag.

Equations

• Algebraic.MassProduction.Routing.recordKeyAndTag input record = Algebraic.MassProduction.Sorting.flatRecordKey ⋯ (Algebraic.MassProduction.Sorting.flatRecords input record)

theorem Algebraic.MassProduction.Routing.recordKeyAndTag_eq_keyWithTag {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordKeyAndTag input record = toLex (keyWithTag (recordKey input record) (recordTag input record))

The prefix consumed by the sorter is exactly the routing key with its tag appended in the final key position.

theorem Algebraic.MassProduction.Routing.recordKeyAndTag_eq_iff {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (left right : Fin (Sorting.networkRecords depth)) : recordKeyAndTag input left = recordKeyAndTag input right ↔ recordKey input left = recordKey input right ∧ recordTag input left = recordTag input right

Equality of the sorter's combined key is exactly equality of the physical key and tag fields.

def Algebraic.MassProduction.Routing.recordHasKeyTag {keyWidth payloadWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (record : Fin (recordWidth keyWidth payloadWidth) → Bool) : Prop

Standalone-record predicate used to identify one source or destination record before and after complete-record sorting.

Equations

• Algebraic.MassProduction.Routing.recordHasKeyTag key tag record = (Algebraic.MassProduction.Routing.packedRecordKey record = key ∧ Algebraic.MassProduction.Routing.packedRecordTag record = tag)

theorem Algebraic.MassProduction.Routing.recordHasKeyTag_flatRecords_iff {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) (key : Fin keyWidth → Bool) (tag : Bool) : recordHasKeyTag key tag (Sorting.flatRecords input record) ↔ recordKey input record = key ∧ recordTag input record = tag

theorem Algebraic.MassProduction.Routing.recordKeyAndTag_covBy_of_sameKey {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (source destination : Fin (Sorting.networkRecords depth)) (sameKey : recordKey input source = recordKey input destination) (sourceTag : recordTag input source = false) (destinationTag : recordTag input destination = true) : recordKeyAndTag input source ⋖ recordKeyAndTag input destination

Same routing keys tagged false and true form a covering pair in the sorter's lexicographic key order.

theorem Algebraic.MassProduction.Routing.predecessor_eq_of_sorted_covBy {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (source destination : Fin (Sorting.networkRecords depth)) (covered : recordKeyAndTag input source ⋖ recordKeyAndTag input destination) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), recordKeyAndTag input index = recordKeyAndTag input source → index = source) (destinationUnique : ∀ (index : Fin (Sorting.networkRecords depth)), recordKeyAndTag input index = recordKeyAndTag input destination → index = destination) : ∃ (positive : 0 < ↑destination), predecessor destination positive = source

A sorted array places a uniquely occurring covered source key immediately before its uniquely occurring destination key.

theorem Algebraic.MassProduction.Routing.predecessorCopyBits_recordPayload_of_sorted_covBy {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (source destination : Fin (Sorting.networkRecords depth)) (covered : recordKeyAndTag input source ⋖ recordKeyAndTag input destination) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), recordKeyAndTag input index = recordKeyAndTag input source → index = source) (destinationUnique : ∀ (index : Fin (Sorting.networkRecords depth)), recordKeyAndTag input index = recordKeyAndTag input destination → index = destination) (sameKey : recordKey input source = recordKey input destination) (sourceHasTag : recordTag input source = sourceTag) (destinationHasTag : recordTag input destination = destinationTag) : recordPayload (predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) destination = recordPayload input source

Once the source/destination keys are known to be adjacent, the explicit guarded scan copies the complete payload of the intended source record.

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

Sorting by (key, tag) and scanning predecessors routes a unique source payload to the unique same-key destination. The source tag is false and the destination tag is true, matching the order used by the manuscript.

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuit_routes_unique {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (source destination : Fin (Sorting.networkRecords depth)) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), recordKeyAndTag (Sorting.bitonicSortBits ⋯ depth true input) index = recordKeyAndTag (Sorting.bitonicSortBits ⋯ depth true input) source → index = source) (destinationUnique : ∀ (index : Fin (Sorting.networkRecords depth)), recordKeyAndTag (Sorting.bitonicSortBits ⋯ depth true input) index = recordKeyAndTag (Sorting.bitonicSortBits ⋯ depth true input) destination → index = destination) (sameKey : recordKey (Sorting.bitonicSortBits ⋯ depth true input) source = recordKey (Sorting.bitonicSortBits ⋯ depth true input) destination) (sourceTag : recordTag (Sorting.bitonicSortBits ⋯ depth true input) source = false) (destinationTag : recordTag (Sorting.bitonicSortBits ⋯ depth true input) destination = true) : recordPayload ((sortedPredecessorCopyCircuit depth keyWidth payloadWidth false true).eval DeMorgan.interpretation input) destination = recordPayload (Sorting.bitonicSortBits ⋯ depth true input) source

End-to-end correctness of the explicit sort-and-match circuit under the unique source/destination record invariant.

theorem Algebraic.MassProduction.Routing.sortedPredecessorCopyCircuit_routes_unique_key {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool) (key : Fin keyWidth → Bool) (uniqueSource : UniqueIndexWhere (Sorting.flatRecords input) (recordHasKeyTag key false)) (uniqueDestination : UniqueIndexWhere (Sorting.flatRecords input) (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)), recordHasKeyTag key false (Sorting.flatRecords input sourceInput) ∧ recordHasKeyTag key false (Sorting.flatRecords sorted sourceSorted) ∧ recordHasKeyTag key true (Sorting.flatRecords sorted destinationSorted) ∧ recordPayload ((sortedPredecessorCopyCircuit depth keyWidth payloadWidth false true).eval DeMorgan.interpretation input) destinationSorted = packedRecordPayload (Sorting.flatRecords input sourceInput)

Turn the router's position-level theorem into a packing-friendly API. If the unsorted input contains exactly one source and one destination with a given key, the explicit sort-and-copy circuit has a destination carrying the original source payload.