Linear-size segmented propagation

Given source bits and links between consecutive records, this circuit computes value[i] = source[i] OR (link[i] AND value[i-1]), with a false initial value. Earlier values are shared circuit wires. Exactly two charged gates are used per record, independent of the lengths of equal-key runs.

def Algebraic.MassProduction.Nonuniform.Propagation.value (source link : ℕ → Bool) : ℕ → Bool

The propagated value after processing a prefix of the records.

Equations

• Algebraic.MassProduction.Nonuniform.Propagation.value source link 0 = false
• Algebraic.MassProduction.Nonuniform.Propagation.value source link count.succ = (source count || link count && Algebraic.MassProduction.Nonuniform.Propagation.value source link count)

def Algebraic.MassProduction.Nonuniform.Propagation.sourceInput {count : ℕ} (input : Fin (count + count) → Bool) (index : ℕ) : Bool

Source bits occupy the first input block.

Equations

• Algebraic.MassProduction.Nonuniform.Propagation.sourceInput input index = if bound : index < count then input (Fin.castAdd count ⟨index, bound⟩) else false

def Algebraic.MassProduction.Nonuniform.Propagation.linkInput {count : ℕ} (input : Fin (count + count) → Bool) (index : ℕ) : Bool

Link bits occupy the second input block.

Equations

• Algebraic.MassProduction.Nonuniform.Propagation.linkInput input index = if bound : index < count then input (Fin.natAdd count ⟨index, bound⟩) else false

def Algebraic.MassProduction.Nonuniform.Propagation.program (count processed : ℕ) : processed ≤ count → Program DeMorgan.signature (count + count) (1 + 2 * processed)

Two shared gates per processed record, preceded by one free false constant. The program always reads the original fixed-size input array.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Nonuniform.Propagation.program count 0 x_2 = Cslib.Circuits.Program.empty.gate { op := Algebraic.DeMorgan.Op.false, wires := Fin.elim0 }

theorem Algebraic.MassProduction.Nonuniform.Propagation.program_eval {count : ℕ} (input : Fin (count + count) → Bool) (processed : ℕ) (fits : processed ≤ count) (prefixCount : ℕ) (prefixLe : prefixCount ≤ processed) : (program count processed fits).eval DeMorgan.interpretation input ⟨2 * prefixCount, ⋯⟩ = value (sourceInput input) (linkInput input) prefixCount

The program's even-numbered gate after each prefix is its propagated value; in particular the zero-prefix gate is false.

theorem Algebraic.MassProduction.Nonuniform.Propagation.program_cost (count processed : ℕ) (fits : processed ≤ count) : Program.cost DeMorgan.standardCost (program count processed fits) = 2 * processed

Every processed record contributes one AND and one OR gate.

def Algebraic.MassProduction.Nonuniform.Propagation.circuit (count : ℕ) : Circuit DeMorgan.signature (count + count) count

All propagated values, in the same order as the input records.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.Propagation.circuit_size (count : ℕ) : (circuit count).size = 1 + 2 * count

The circuit has one free constant plus two gates per record.

theorem Algebraic.MassProduction.Nonuniform.Propagation.circuit_eval {count : ℕ} (input : Fin (count + count) → Bool) (index : Fin count) : (circuit count).eval DeMorgan.interpretation input index = value (sourceInput input) (linkInput input) (↑index + 1)

The concrete circuit implements the segmented recurrence.

theorem Algebraic.MassProduction.Nonuniform.Propagation.circuit_cost (count : ℕ) : (circuit count).cost DeMorgan.standardCost = 2 * count

The exact charged size is linear in the number of records.

theorem Algebraic.MassProduction.Nonuniform.Propagation.value_eq_true_iff (source link : ℕ → Bool) (count : ℕ) : value source link count = true ↔ ∃ start < count, source start = true ∧ ∀ (index : ℕ), start < index → index < count → link index = true

A propagated true bit has a source connected to the current position by an uninterrupted interval of true links.