Record broadcast circuits

The input records have the established (key, tag, payload) layout. A false tag marks a source. For each payload bit, this circuit propagates source bits along adjacent equal-key links using the shared linear-size recurrence. It supports arbitrarily many destination records for the same source key.

Sorting and source-existence hypotheses belong to the routing application; this module proves the concrete broadcast recurrence and its exact cost bound.

def Algebraic.MassProduction.Nonuniform.Broadcast.sourceExpression (depth keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

A source record seeds its own payload bit into the current segment.

Equations

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

def Algebraic.MassProduction.Nonuniform.Broadcast.linkExpression (depth keyWidth payloadWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

Link to the predecessor exactly when the key is unchanged.

Equations

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

def Algebraic.MassProduction.Nonuniform.Broadcast.inputExpression (depth keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) : Fin (Sorting.networkRecords depth + Sorting.networkRecords depth) → DeMorgan.Expression (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

Source and link inputs for the shared propagation circuit.

Equations

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

def Algebraic.MassProduction.Nonuniform.Broadcast.inputsCircuit (depth keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) : Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) (Sorting.networkRecords depth + Sorting.networkRecords depth)

Compile all local source and link tests.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.Broadcast.inputsCircuit_size (depth keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) : (inputsCircuit depth keyWidth payloadWidth bit).size = ∑ index : Fin (Sorting.networkRecords depth + Sorting.networkRecords depth), (inputExpression depth keyWidth payloadWidth bit index).gateCount

The exact gate count of inputsCircuit.

def Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit (depth keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) : Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) (Sorting.networkRecords depth)

Broadcast one selected payload bit across all records.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_size (depth keyWidth payloadWidth : ℕ) (bit : Fin payloadWidth) : (payloadCircuit depth keyWidth payloadWidth bit).size = (inputsCircuit depth keyWidth payloadWidth bit).size + (1 + 2 * Sorting.networkRecords depth)

The exact gate count of payloadCircuit.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.inputsCircuit_eval {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : (inputsCircuit depth keyWidth payloadWidth bit).eval DeMorgan.interpretation input = fun (index : Fin (Sorting.networkRecords depth + Sorting.networkRecords depth)) => DeMorgan.Expression.eval input (inputExpression depth keyWidth payloadWidth bit index)

Local tests have exactly their expression semantics.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_eval {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : (payloadCircuit depth keyWidth payloadWidth bit).eval DeMorgan.interpretation input record = Propagation.value (Propagation.sourceInput fun (index : Fin (Sorting.networkRecords depth + Sorting.networkRecords depth)) => DeMorgan.Expression.eval input (inputExpression depth keyWidth payloadWidth bit index)) (Propagation.linkInput fun (index : Fin (Sorting.networkRecords depth + Sorting.networkRecords depth)) => DeMorgan.Expression.eval input (inputExpression depth keyWidth payloadWidth bit index)) (↑record + 1)

Concrete operational semantics: sources and adjacent-key tests feed the shared propagation recurrence.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.sourceExpression_eval {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression.eval input (sourceExpression depth keyWidth payloadWidth bit record) = (!Routing.recordTag input record && Routing.recordPayload input record bit)

Only false-tagged source records seed a payload bit.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.linkExpression_eval_eq_true_iff {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) (positive : 0 < ↑record) : DeMorgan.Expression.eval input (linkExpression depth keyWidth payloadWidth record) = true ↔ Routing.recordKey input (Routing.predecessor record positive) = Routing.recordKey input record

A noninitial record links to the preceding record precisely at equal keys.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_cost_le {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) : (payloadCircuit depth keyWidth payloadWidth bit).cost DeMorgan.standardCost ≤ Sorting.networkRecords depth * (6 * keyWidth + 4)

Broadcasting one payload bit costs at most 6 * keyWidth + 4 gates per record, independently of equal-key run lengths.