Output guesses and erasure for aggregate circuits

Only special occurrences receive guessed bits. Erasure preserves every gate index and every ordinary incoming wire, replacing each special gate by a nullary constant. Thus a special output may feed another special gate, an ordinary gate, or the output.

@[reducible, inline]

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

The special gate occurrences in an actual straight-line program.

Equations

• Algebraic.Aggregate.SpecialGate p = { gate : Fin g // Algebraic.Aggregate.Op.isSpecial (p.lines gate).op = true }

def Algebraic.Aggregate.specialCount {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : ℕ

The number of special occurrences, not the number of possible operation symbols.

Equations

• Algebraic.Aggregate.specialCount p = Fintype.card (Algebraic.Aggregate.SpecialGate p)

@[reducible, inline]

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

One output bit for each special occurrence.

Equations

• Algebraic.Aggregate.Guess p = (Algebraic.Aggregate.SpecialGate p → Bool)

@[reducible, inline]

abbrev Algebraic.Aggregate.Register {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (gate : SpecialGate p) : Type

The aggregate register belonging to a particular special occurrence.

Equations

• Algebraic.Aggregate.Register p gate = Algebraic.Aggregate.Op.Register (p.lines ↑gate).op

@[reducible, inline]

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

Simultaneous registers for all special occurrences.

Equations

• Algebraic.Aggregate.Registers p = ((gate : Algebraic.Aggregate.SpecialGate p) → Algebraic.Aggregate.Register p gate)

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

Output-guess bits plus the binary logarithmic budgets of the actual registers.

Equations

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

def Algebraic.Aggregate.guessValues {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) (gate : Fin g) : Bool

Extend special-only guesses by a dummy bit on ordinary gates. The dummy is ignored.

Equations

• Algebraic.Aggregate.guessValues p a gate = if h : Algebraic.Aggregate.Op.isSpecial (p.lines gate).op = true then a ⟨gate, h⟩ else false

def Algebraic.Aggregate.eraseLine {J : Type} {State : J → Type} {n g : ℕ} (line : Line (signature State) n g) (value : Bool) : Line ordinarySignature n g

Erase one line while retaining the wire namespace.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Aggregate.eraseLine { op := Algebraic.Aggregate.Op.binary f, wires := wires } value = { op := Algebraic.Aggregate.OrdinaryOp.binary f, wires := wires }

def Algebraic.Aggregate.eraseWith {J : Type} {State : J → Type} {n g : ℕ} : Program (signature State) n g → (Fin g → Bool) → Program ordinarySignature n g

The structural erasure uses a total lookup; only special entries are inspected.

Equations

• Algebraic.Aggregate.eraseWith Cslib.Circuits.Program.empty x_3 = Cslib.Circuits.Program.empty
• Algebraic.Aggregate.eraseWith (p.gate line) values = (Algebraic.Aggregate.eraseWith p (values ∘ Fin.castSucc)).gate (Algebraic.Aggregate.eraseLine line (values (Fin.last g)))

def Algebraic.Aggregate.erase {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) : Program ordinarySignature n g

Replace each special gate by its guessed nullary output, preserving all gate indices.

Equations

• Algebraic.Aggregate.erase p a = Algebraic.Aggregate.eraseWith p (Algebraic.Aggregate.guessValues p a)

def Algebraic.Aggregate.eraseCircuit {J : Type} {State : J → Type} {n m : ℕ} (c : Circuit (signature State) n m) (a : Guess c.program) : Circuit ordinarySignature n m

The designated outputs use precisely the same wires after erasure.

Equations

• Algebraic.Aggregate.eraseCircuit c a = { size := c.size, program := Algebraic.Aggregate.erase c.program a, outputs := c.outputs }

def Algebraic.Aggregate.Consistent {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (input : Fin n → Bool) : Prop

Every special gate agrees with evaluation of its original slots on a candidate trace.

Equations

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

def Algebraic.Aggregate.actualGuess {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (input : Fin n → Bool) : Guess p

The true special-output vector.

Equations

• Algebraic.Aggregate.actualGuess p input gate = p.eval Algebraic.Aggregate.interpretation input ↑gate