Boolean one-way messages for signed gates

Each gate sends one bit determined only by selected primary inputs. Affine gates send the partial parity and conjunctions send the conjunction of selected literals. One spare coordinate covers a directly designated primary output.

def Algebraic.Aggregate.Geometry.conjunctionSummary {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) (x : Wire n g → Bool) : Bool

Conjunction of selected primary literals.

Equations

• Algebraic.Aggregate.Geometry.conjunctionSummary polarity wires U x = decide (∀ (i : Fin r), Algebraic.Aggregate.Capacity.selected U (wires i) → x (wires i) = polarity i)

def Algebraic.Aggregate.Geometry.lineSummary {n g : ℕ} (line : Line signature n g) (U : Finset (Fin n)) (x : Wire n g → Bool) : Bool

A gate sends only its partial aggregate of selected primary inputs.

Equations

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

def Algebraic.Aggregate.Geometry.key {n g : ℕ} (p : Program signature n g) (U : Finset (Fin n)) (x : Fin n → Bool) : Fin g → Bool

The vector of Boolean messages, one for each actual gate.

Equations

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

def Algebraic.Aggregate.Geometry.outputKey {n g : ℕ} (p : Program signature n g) (U : Finset (Fin n)) (out : Wire n g) (x : Fin n → Bool) : Fin (g + 1) → Bool

The message includes at most one extra bit for a designated primary output.

Equations

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