Primary-input summaries for aggregate circuits

Each binary occurrence contributes one bit. Each special occurrence contributes one monoid element, aggregating only the selected primary-input slots. No internal wire values or output guesses enter this summary.

@[reducible, inline]

abbrev Algebraic.Aggregate.Capacity.SummaryRegister {J : Type} {State : J → Type} : Op State → Type

The per-occurrence summary type.

Equations

• Algebraic.Aggregate.Capacity.SummaryRegister (Algebraic.Aggregate.Op.binary function) = Bool
• Algebraic.Aggregate.Capacity.SummaryRegister (Algebraic.Aggregate.Op.special kind arity contribution readout) = State kind

@[instance_reducible]

instance Algebraic.Aggregate.Capacity.instFintypeSummaryRegister {J : Type} {State : J → Type} [(j : J) → Fintype (State j)] (op : Op State) : Fintype (SummaryRegister op)

Equations

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

def Algebraic.Aggregate.Capacity.selected {n g : ℕ} (U : Finset (Fin n)) : Wire n g → Prop

Only selected primary inputs belong to the sending party.

Equations

• Algebraic.Aggregate.Capacity.selected U (Cslib.Circuits.Wire.input i) = (i ∈ U)
• Algebraic.Aggregate.Capacity.selected U (Cslib.Circuits.Wire.gate gate) = False

@[instance_reducible]

instance Algebraic.Aggregate.Capacity.instDecidableSelected {n g : ℕ} (U : Finset (Fin n)) (wire : Wire n g) : Decidable (selected U wire)

Equations

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

def Algebraic.Aggregate.Capacity.lineSummary {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (U : Finset (Fin n)) (values : Wire n g → Bool) : SummaryRegister line.op

A line's summary uses only selected values. If both binary inputs are selected, only its output is needed; if exactly one is selected, only that input is needed.

Equations

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

@[reducible, inline]

abbrev Algebraic.Aggregate.Capacity.Key {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : Type

The one-way key has one register for each actual gate occurrence.

Equations

• Algebraic.Aggregate.Capacity.Key p = ((gate : Fin g) → Algebraic.Aggregate.Capacity.SummaryRegister (p.lines gate).op)

def Algebraic.Aggregate.Capacity.key {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (U : Finset (Fin n)) (input : Fin n → Bool) : Key p

The sending party summarizes its primary inputs at every gate.

Equations

• Algebraic.Aggregate.Capacity.key p U input gate = Algebraic.Aggregate.Capacity.lineSummary (p.lines gate) U (Cslib.Circuits.Wire.elim input fun (x : Fin g) => false)

def Algebraic.Aggregate.Capacity.capacity {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : ℕ

Bit capacity charges a binary gate one bit and a special gate its register size.

Equations

• Algebraic.Aggregate.Capacity.capacity p = Algebraic.Aggregate.ordinaryCount p + ∑ gate : Algebraic.Aggregate.SpecialGate p, Nat.clog 2 (Fintype.card (Algebraic.Aggregate.Register p gate))