Exact one-way protocols for signed AND/OR/XOR circuits

The public message consists of one partial aggregate per actual gate and one optional primary-output bit. It determines the output for every complementary input.

noncomputable def Algebraic.Aggregate.Geometry.circuitOneWaySummary {n : ℕ} (c : Circuit signature n 1) (U : Finset (Fin n)) : Cutwidth.Aggregate.OneWaySummary (c.outputFunction interpretation 0) U (Fin (c.size + 1) → Bool)

The actual Boolean gate summaries form a one-way protocol.

Equations

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