Zero-cost routing-record wiring

This module lifts Boolean routing-record layouts to explicit zero-cost De Morgan wiring specifications. It is independent of the scheduler and resource pipeline assembled by RoutingAssembly.

def Algebraic.MassProduction.RoutingAssembly.wiringPackRecord {keyWidth inputs payloadWidth : ℕ} (key : Fin keyWidth → DeMorgan.Wiring inputs) (tag : DeMorgan.Wiring inputs) (payload : Fin payloadWidth → DeMorgan.Wiring inputs) : Fin (Routing.recordWidth keyWidth payloadWidth) → DeMorgan.Wiring inputs

Record packing lifted from Booleans to wiring-bit descriptions.

Equations

• Algebraic.MassProduction.RoutingAssembly.wiringPackRecord key tag payload = Fin.append (Fin.append key fun (x : Fin 1) => tag) payload

theorem Algebraic.MassProduction.RoutingAssembly.wiringPackRecord_eval {keyWidth inputs payloadWidth : ℕ} (key : Fin keyWidth → DeMorgan.Wiring inputs) (tag : DeMorgan.Wiring inputs) (payload : Fin payloadWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) : (fun (bit : Fin (Routing.recordWidth keyWidth payloadWidth)) => DeMorgan.Wiring.eval input (wiringPackRecord key tag payload bit)) = Routing.packRecord (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (key bit)) (DeMorgan.Wiring.eval input tag) fun (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (payload bit)

theorem Algebraic.MassProduction.RoutingAssembly.wiringPackRecord_eval_apply {keyWidth inputs payloadWidth : ℕ} (key : Fin keyWidth → DeMorgan.Wiring inputs) (tag : DeMorgan.Wiring inputs) (payload : Fin payloadWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (bit : Fin (Routing.recordWidth keyWidth payloadWidth)) : DeMorgan.Wiring.eval input (wiringPackRecord key tag payload bit) = Routing.packRecord (fun (keyBit : Fin keyWidth) => DeMorgan.Wiring.eval input (key keyBit)) (DeMorgan.Wiring.eval input tag) (fun (payloadBit : Fin payloadWidth) => DeMorgan.Wiring.eval input (payload payloadBit)) bit

def Algebraic.MassProduction.RoutingAssembly.wiringRoutingRecordSequence {sourceCount keyWidth inputs payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → DeMorgan.Wiring inputs) (sourcePayloads : Fin sourceCount → Fin payloadWidth → DeMorgan.Wiring inputs) (destinationKeys : Fin destinationCount → Fin keyWidth → DeMorgan.Wiring inputs) (destinationPayloads : Fin destinationCount → Fin payloadWidth → DeMorgan.Wiring inputs) (paddingKeys : Fin paddingCount → Fin keyWidth → DeMorgan.Wiring inputs) (paddingPayloads : Fin paddingCount → Fin payloadWidth → DeMorgan.Wiring inputs) : Fin (sourceCount + destinationCount + paddingCount) → Fin (Routing.recordWidth keyWidth payloadWidth) → DeMorgan.Wiring inputs

Routing records whose fields are all wiring-bit descriptions.

Equations

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

theorem Algebraic.MassProduction.RoutingAssembly.wiringRoutingRecordSequence_eval {sourceCount keyWidth inputs payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → DeMorgan.Wiring inputs) (sourcePayloads : Fin sourceCount → Fin payloadWidth → DeMorgan.Wiring inputs) (destinationKeys : Fin destinationCount → Fin keyWidth → DeMorgan.Wiring inputs) (destinationPayloads : Fin destinationCount → Fin payloadWidth → DeMorgan.Wiring inputs) (paddingKeys : Fin paddingCount → Fin keyWidth → DeMorgan.Wiring inputs) (paddingPayloads : Fin paddingCount → Fin payloadWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) : (fun (record : Fin (sourceCount + destinationCount + paddingCount)) (bit : Fin (Routing.recordWidth keyWidth payloadWidth)) => DeMorgan.Wiring.eval input (wiringRoutingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads record bit)) = Routing.routingRecordSequence (fun (source : Fin sourceCount) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) (fun (source : Fin sourceCount) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (sourcePayloads source bit)) (fun (destination : Fin destinationCount) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (destinationKeys destination bit)) (fun (destination : Fin destinationCount) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (destinationPayloads destination bit)) (fun (padding : Fin paddingCount) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (paddingKeys padding bit)) fun (padding : Fin paddingCount) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (paddingPayloads padding bit)

def Algebraic.MassProduction.RoutingAssembly.wiringRoutingInputBits {sourceCount keyWidth inputs payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → DeMorgan.Wiring inputs) (sourcePayloads : Fin sourceCount → Fin payloadWidth → DeMorgan.Wiring inputs) (destinationKeys : Fin destinationCount → Fin keyWidth → DeMorgan.Wiring inputs) (destinationPayloads : Fin destinationCount → Fin payloadWidth → DeMorgan.Wiring inputs) (paddingKeys : Fin paddingCount → Fin keyWidth → DeMorgan.Wiring inputs) (paddingPayloads : Fin paddingCount → Fin payloadWidth → DeMorgan.Wiring inputs) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → DeMorgan.Wiring inputs

Exact-capacity routing records whose fields are all wiring-bit descriptions, flattened in the sorter's row-major format.

Equations

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

theorem Algebraic.MassProduction.RoutingAssembly.wiringRoutingInputBits_eval {sourceCount keyWidth inputs payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → DeMorgan.Wiring inputs) (sourcePayloads : Fin sourceCount → Fin payloadWidth → DeMorgan.Wiring inputs) (destinationKeys : Fin destinationCount → Fin keyWidth → DeMorgan.Wiring inputs) (destinationPayloads : Fin destinationCount → Fin payloadWidth → DeMorgan.Wiring inputs) (paddingKeys : Fin paddingCount → Fin keyWidth → DeMorgan.Wiring inputs) (paddingPayloads : Fin paddingCount → Fin payloadWidth → DeMorgan.Wiring inputs) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (input : Fin inputs → Bool) : (fun (bit : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))) => DeMorgan.Wiring.eval input (wiringRoutingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount bit)) = Routing.routingInputBits (fun (source : Fin sourceCount) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) (fun (source : Fin sourceCount) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (sourcePayloads source bit)) (fun (destination : Fin destinationCount) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (destinationKeys destination bit)) (fun (destination : Fin destinationCount) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (destinationPayloads destination bit)) (fun (padding : Fin paddingCount) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (paddingKeys padding bit)) (fun (padding : Fin paddingCount) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (paddingPayloads padding bit)) recordCount

Evaluating a wiring-level routing layout gives the corresponding Boolean routing layout exactly.