Complete finite Uhlig layer

This module composes the routing and shared decoder circuits into one complete finite mass-production layer. It proves exact correctness and exact cost identities at finite widths and for an arbitrary number of request pairs.

Complete finite Uhlig layer

noncomputable def Algebraic.MassProduction.UhligCircuit.layerStateCircuit {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : Circuit DeMorgan.signature (layerInputCount prefixWidth suffixWidth pairs) (layerStateCount prefixWidth suffixWidth pairs)

Preserve the original inputs and append every routed resource value.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.layerStateCircuit_size {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (layerStateCircuit pairs resourceCircuits).size = ∑ resource : Fin (prefixLast prefixWidth + 2), routedResourceGateCount prefixWidth suffixWidth pairs (fun (resource : Fin (prefixLast prefixWidth + 2)) => (resourceCircuits resource).size) resource

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.layerStateCircuit_eval_original {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (input : Fin (layerInputCount prefixWidth suffixWidth pairs) → Bool) : originalInputFromState ((layerStateCircuit pairs resourceCircuits).eval DeMorgan.interpretation input) = input

theorem Algebraic.MassProduction.UhligCircuit.layerStateCircuit_eval_resource {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (computes : ∀ (resource : Fin (prefixLast prefixWidth + 2)), (resourceCircuits resource).ComputesWith DeMorgan.interpretation (directProduct (resourceFunction function resource) pairs)) (input : Fin (layerInputCount prefixWidth suffixWidth pairs) → Bool) (resource : Fin (prefixLast prefixWidth + 2)) (pair : Fin pairs) : (layerStateCircuit pairs resourceCircuits).eval DeMorgan.interpretation input (resourceStateIndex resource pair) = resourceValue function input pair resource

theorem Algebraic.MassProduction.UhligCircuit.decodedStateValue_layerStateCircuit_eval {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (computes : ∀ (resource : Fin (prefixLast prefixWidth + 2)), (resourceCircuits resource).ComputesWith DeMorgan.interpretation (directProduct (resourceFunction function resource) pairs)) (input : Fin (layerInputCount prefixWidth suffixWidth pairs) → Bool) (pair : Fin pairs) (side : Fin 2) : decodedStateValue ((layerStateCircuit pairs resourceCircuits).eval DeMorgan.interpretation input) pair side = decodedValue function input pair side

Decoding the completed layer state agrees with the semantic Uhlig decoder.

noncomputable def Algebraic.MassProduction.UhligCircuit.sharedUhligLayerCircuit {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : Circuit DeMorgan.signature (layerInputCount prefixWidth suffixWidth pairs) (2 * pairs)

Quantitatively useful finite Uhlig layer, using circuit sharing inside each XOR decoder.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedUhligLayerCircuit_size {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (sharedUhligLayerCircuit pairs resourceCircuits).size = ∑ resource : Fin (prefixLast prefixWidth + 2), routedResourceGateCount prefixWidth suffixWidth pairs (fun (resource : Fin (prefixLast prefixWidth + 2)) => (resourceCircuits resource).size) resource + ∑ output : Fin (2 * pairs), sharedDecoderOutputGateCount prefixWidth suffixWidth pairs output

theorem Algebraic.MassProduction.UhligCircuit.sharedUhligLayerCircuit_computes {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (computes : ∀ (resource : Fin (prefixLast prefixWidth + 2)), (resourceCircuits resource).ComputesWith DeMorgan.interpretation (directProduct (resourceFunction function resource) pairs)) : (sharedUhligLayerCircuit pairs resourceCircuits).ComputesWith DeMorgan.interpretation (directProduct function (2 * pairs))

Exact correctness of the shared finite layer.

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedUhligLayerCircuit_cost {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (sharedUhligLayerCircuit pairs resourceCircuits).cost DeMorgan.standardCost = ∑ resource : Fin (prefixLast prefixWidth + 2), (∑ _pair : Fin pairs, (resourceRouterCircuit resource).cost DeMorgan.standardCost + (resourceCircuits resource).cost DeMorgan.standardCost) + ∑ output : Fin (2 * pairs), have pairSide := decoderPairSide output; (sharedDecodedCircuit pairSide.1 pairSide.2).cost DeMorgan.standardCost

Exact cost ledger for the shared finite layer.

noncomputable def Algebraic.MassProduction.UhligCircuit.uhligLayerCircuit {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : Circuit DeMorgan.signature (layerInputCount prefixWidth suffixWidth pairs) (2 * pairs)

Compose routing, supplied resource evaluation, and exact decoding.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.uhligLayerCircuit_size {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (uhligLayerCircuit pairs resourceCircuits).size = ∑ resource : Fin (prefixLast prefixWidth + 2), routedResourceGateCount prefixWidth suffixWidth pairs (fun (resource : Fin (prefixLast prefixWidth + 2)) => (resourceCircuits resource).size) resource + ∑ output : Fin (2 * pairs), decoderGateCount prefixWidth suffixWidth pairs output

theorem Algebraic.MassProduction.UhligCircuit.uhligLayerCircuit_computes {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (computes : ∀ (resource : Fin (prefixLast prefixWidth + 2)), (resourceCircuits resource).ComputesWith DeMorgan.interpretation (directProduct (resourceFunction function resource) pairs)) : (uhligLayerCircuit pairs resourceCircuits).ComputesWith DeMorgan.interpretation (directProduct function (2 * pairs))

Exact finite Uhlig circuit theorem. If each resource function is available on pairs independent suffixes, one explicit De Morgan circuit computes 2 * pairs independent copies of the original function.

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.layerStateCircuit_cost {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (layerStateCircuit pairs resourceCircuits).cost DeMorgan.standardCost = ∑ resource : Fin (prefixLast prefixWidth + 2), (∑ _pair : Fin pairs, (resourceRouterCircuit resource).cost DeMorgan.standardCost + (resourceCircuits resource).cost DeMorgan.standardCost)

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.uhligLayerCircuit_cost {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (uhligLayerCircuit pairs resourceCircuits).cost DeMorgan.standardCost = ∑ resource : Fin (prefixLast prefixWidth + 2), (∑ _pair : Fin pairs, (resourceRouterCircuit resource).cost DeMorgan.standardCost + (resourceCircuits resource).cost DeMorgan.standardCost) + ∑ output : Fin (2 * pairs), (decoderOutputExpression output).standardCost

Exact cost ledger for the complete finite layer.