Arithmetic circuits - Sum-check protocol

Introduction¶

Through our sum-check protocol and multilinear extensions notebooks, we have started to replicate Thaler’s elegant presentation 1 of the GKR interactive proof for circuit evaluation, as introduced by Goldwasser, Kalai, and Rothblum 23. We are nearly ready to present the GKR protocol in full, but before we do, there’s one final topic to address: arithmetic circuits.

Modeling computations¶

An arithmetic circuit is defined as a special kind of directed graph, which is assumed to be familiar to the reader.

Definition 1 (arithmetic circuit)

An arithmetic circuit $C$ over a field $\mathbb{F}$ in the variables $X = \{x_0, \ldots, x_{n-1}\}$ is a labeled directed acyclic multigraph (DAG). The nodes of this graph are called gates, and the edges are called wires.

Input gates are gates with fan-in (in-degree) zero, labeled by variables from $X$ or constants from $\mathbb{F}$ .
Output gates are gates with fan-out (out-degree) zero, where the output of the circuit is computed.
Non-input gates are either addition gates, labeled with the addition operation ( $+$ ), or multiplication gates, labeled with the multiplication operation ( $\times$ ). These gates compute the sum or product of the polynomials computed on the tails of the incoming wires. Subtraction can be represented by multiplication with the constant -1 (i.e., using $(x - y) = x + (-1) \cdot y$ ).

The output of $C$ is the polynomial (or set of polynomials) computed at the output gate(s).
The size $S$ of $C$ is the total number of gates in the graph, and the depth $d$ of $C$ is the length of the longest path from an input gate to an output gate.
Layer $i$ of $C$ is a set of all gates $v$ such that the shortest path from $v$ to any output gate has length $i$ . We index layers starting from the output layer (Layer 0), increasing as we move toward the inputs. This convention is convenient for top-down verification in the GKR protocol.

We say that $C$ is a constant-input circuit if:

Every input gate is labeled with a constant from $\mathbb{F}$ (as opposed to a variable from $X$ ).

We say that $C$ is a binary arithmetic circuit if:

Every non-input gate has a fan-in of 2, representing a binary operation on two inputs.

We say that $C$ is a strictly layered arithmetic circuit if:

All inputs are in Layer $d$ , and every wire is a wire from a gate in Layer $i + 1$ to a gate in Layer $i$ , for some $i \in \{0,1,\ldots,d - 1\}$ , where $d$ is the depth of the circuit.

Assumption 1

Throughout, we will assume that all of our arithmetic circuits are constant-input, binary and strictly layered.

Under the constant-input restriction, the circuit computes a constant polynomial. We adopt this model because, in the GKR protocol, verification concerns the correctness of gate evaluations rather than symbolic polynomial computation. Allowing variable-labeled inputs would require only notational changes and does not affect the protocol.

The binary fan-in assumption ensures that wiring predicates depend on exactly two child gates, which will be essential when defining the verification equations in later sections.

The strictly layered assumption is made primarily for conceptual and notational simplicity. In the GKR protocol, verification proceeds layer by layer, with each round reducing correctness of one layer to a polynomial identity checked via sum-check. Strict layering ensures that all dependencies are local to adjacent layers, yielding uniform wiring predicates and a clean inductive structure. This assumption is not restrictive. Any arithmetic circuit can be transformed into a strictly layered circuit by inserting identity gates, with at most polynomial overhead. The protocol and its soundness guarantees extend to general circuits after such a normalization.

Example 1

Consider evaluating the expressions $(2 + 2) \times (3 \times 3)$ and $3 \times 4 + (5 + 5)$ in the field $\mathbb{F} = \mathbb{Z}/11\mathbb{Z}$ . The following circuit of size $S = 10$ and depth $d = 2$ illustrates one way to perform this computation:

Layer 0 (output layer): The top layer contains the two gates labeled $\times$ and $+$ .
Layer 1 (intermediate layer): The middle layer contains four gates labeled $+$ , $\times$ , $\times$ , and $+$ .
Layer 2 (input layer): The bottom layer contains four gates labeled 2, 3, 4, and 5. (Although the number 3 appears only once as an input gate, it has fan-out three: its value is used as an input to two multiplication operations via three outgoing wires.)

In this structure:

Every input gate is labeled with a constant from $\mathbb{F}$ . This is a constant-input circuit.
Every gate in layers 0 and 1 has a fan-in of 2 (representing a binary operation, either addition or multiplication). This is a binary circuit.
All inputs are in Layer 2: no inputs are in Layer 0 or Layer 1. Also, wires only connect consecutive layers: from Layer 2 to Layer 1, and from Layer 1 to Layer 0. No wires connect gates within the same layer, non-consecutive layers, or consecutive layers in the ‘low to high’ (e.g. 1 to 2) direction. This is a strictly layered circuit.

For example:

The two wires from the gate labeled 2 enter the leftmost gate in Layer 1 labeled $+$ , representing the subexpression $2 + 2$ .
Similarly, the gates in Layer 1 compute the subexpressions $3 \times 3$ , $3 \times 4$ , and $5 + 5$ in parallel.

Next, in Layer 1, we evaluate:

$2 + 2 \equiv 4 \bmod 11$ ,
$3 \times 3 \equiv 9 \bmod 11$ ,
$3 \times 4 \equiv 1 \bmod 11$ ,
$5 + 5 \equiv 10 \bmod 11$ .

Finally, the output layer computes:

$4 \times 9 \equiv 3 \bmod 11$ ,
$1 + 10 \equiv 0 \bmod 11$ .

Thus, the circuit computes two expressions through six binary operations performed in two stages, holding four field elements in memory at each stage.

expression_01a = '(2 + 2)*(3*3)'
expression_01b = '3*4 + (5 + 5)'

ac_01 = ArithmeticCircuit(expression_01a, expression_01b, prime=11)
print(f"{expression_01a} mod {ac_01.field.mod}, {expression_01b} mod {ac_01.field.mod}")
display(ac_01.graphviz_circuit)

print(f"This circuit has size S = {ac_01.size} and depth d = {ac_01.depth}.")

(2 + 2)*(3*3) mod 11, 3*4 + (5 + 5) mod 11

This circuit has size S = 10 and depth d = 2.

Topological ordering¶

An arithmetic circuit cannot have cycles because it represents a well-defined, finite computation. They are designed to compute polynomials in a finite number of steps. If a cycle existed, it would be unclear where to start, and the computation would never terminate. For example, the cycle below results in the expression $2 + (3 \times (2 + ( 3 \times \cdots )))$ (or $3 \times (2 + (3 \times ( 2 + \cdots )))$ ), which is ambiguous and infinite, making it meaningless. Arithmetic circuits are acyclic to ensure that each operation is performed in a clear, finite sequence.

from graphviz import Digraph

# Non-DAG example
dot = Digraph()
dot.node('2', '2', shape='circle')
dot.node('+', '+', shape='circle')
dot.node('3', '3', shape='circle')
dot.node('×', '×', shape='circle') 
dot.edge('2', '+')
dot.edge('+', '3')
dot.edge('3', '×') 
dot.edge('×', '2')
dot.attr(rankdir='LR')
display(dot)

A topological ordering (or topological sort) of a directed graph is a linear ordering of its vertices such that, for every directed edge from vertex $u$ to vertex $v$ , vertex $u$ appears before vertex $v$ in the ordering. In other words, the ordering respects the direction of the edges.

More formally:

Since an arithmetic circuit is acyclic, a topological order of its nodes allows us to evaluate the circuit in a sequence where each node (operation) depends only on previously evaluated nodes. This ensures that each computation is performed in a clear, finite order, starting from the input nodes and progressing through intermediate gates to the output nodes. Without a valid topological order, cycles would create circular dependencies, preventing the circuit from being evaluated at all. Therefore, topological ordering guarantees that the computation proceeds in a finite, unambiguous manner.

Example 2

display(ac_01.layers)
print("")
display(ac_01.graphviz_circuit_bitstring)
print("")
ac_01.print_topological_order()

{0: {'0.0', '0.1'},
 1: {'1.00', '1.01', '1.10', '1.11'},
 2: {'2.00', '2.01', '2.10', '2.11'}}



TOPOLOGICAL ORDERING

2.00 -> 2.01 -> 2.10 -> 2.11 -> 1.00 -> 1.01 -> 1.10 -> 1.11 -> 0.0 -> 0.1

Gate-value functions¶

A gate-value function is a function that records the values computed by all gates in a given layer of an arithmetic circuit, where gates are indexed by their binary identifiers. We formalize this notion below.

Definition 4 (gate-value function)

Non-gate labels: If $\mathbf{b} \in \{0,1\}^{s_i}$ does not correspond to a valid gate label in Layer $i$ (i.e., if $S_i$ is not a power of 2 and $\mathbf{b}$ represents an integer exceeding $S_i - 1$ ), then:

W_i(\mathbf{b}) := 0.

Valid gate labels:
- Layer $d$ (input layer): For all $\mathbf{b} \in \{0,1\}^{s_d}$ , define:
  $W_d(\mathbf{b}) := \text{the input at gate $\mathbf{b}$ in Layer $d$}.$
- Intermediate layers, $d-1 \geq i \geq 0$ : For $\mathbf{c} \in \{0,1\}^{s_i}$ , let $\mathbf{a}, \mathbf{b} \in \{0,1\}^{s_{i+1}}$ (possibly $\mathbf{a} = \mathbf{b}$ ) be the gates in Layer $i+1$ connected by wires to gate $\mathbf{c}$ . Define:
  $W_i(\mathbf{c}) := W_{i+1}(\mathbf{a}) \odot W_{i+1}(\mathbf{b}),$
  where $\odot$ represents:
  - Addition, if gate $\mathbf{c}$ is an addition gate;
  - Multiplication, if gate $\mathbf{c}$ is a multiplication gate.
Multilinear extension: For each layer $i$ , the multilinear extension $\widetilde{W}_i : \mathbb{F}^{s_i} \to \mathbb{F}$ is defined to extend $W_i$ to inputs in $\mathbb{F}^{s_i}$ .

Example 3

display(ac_01.graphviz_circuit_bitstring)

ac_01.print_gate_values()


GATE VALUES

LAYER 2

W_2(0,0) = 2

W_2(0,1) = 3

W_2(1,0) = 4

W_2(1,1) = 5

LAYER 1

W_1(0,0) = 4

W_1(0,1) = 9

W_1(1,0) = 1

W_1(1,1) = 10

LAYER 0

W_0(0) = 3

W_0(1) = 0

ac_01.print_tilde_W()


MULTILINEAR EXTENSIONS OF GATE-VALUE FUNCTIONS

LAYER 2

W̃_2(x_0, x_1) = 2*x_0 + x_1 + 2

LAYER 1

W̃_1(x_0, x_1) = 4*x_0*x_1 + 8*x_0 + 5*x_1 + 4

LAYER 0

W̃_0(x_0) = 8*x_0 + 3

Wiring predicates¶

For the purposes of the next definition, we order bitstrings of a given length lexicographically with the most significant bit first (equivalently, by the numeric value of their binary representation). That is, if $\mathbf{a} = (a_0,\ldots,a_{m - 1}) \in \{0,1\}^m$ and $\mathbf{b} = (b_0,\ldots,b_{m - 1}) \in \{0,1\}^m$ , we write

\mathbf{a} \, \le \, \mathbf{b} \quad \Leftrightarrow \quad 2^{m - 1}a_{0} + 2^{m - 2}a_{1} + \cdots + 2^0a_{m - 1} \, \le \, 2^{m - 1}b_{0} + 2^{m - 2}b_1 + \cdots + 2^0b_{m - 1}.

This ordering is fixed once and for all and serves only as a convenient convention.

Definition 5 (wiring predicates)

Let $C$ be a binary, strictly layered arithmetic circuit of depth $d$ over a field $\mathbb{F}$ . For $0 \leq i \leq d$ , let Layer $i$ have size $S_i$ and bit length $s_i$ , and fix a bit labeling of each layer. For $0 \le i \le d - 1$ , the wiring predicates

\begin{align} \mathrm{add}_i & : \{0,1\}^{s_i} \times \{0,1\}^{s_{i + 1}} \times \{0,1\}^{s_{i + 1}} \to \mathbb{F} \\ \mathrm{mult}_i & : \{0,1\}^{s_i} \times \{0,1\}^{s_{i + 1}} \times \{0,1\}^{s_{i + 1}} \to \mathbb{F} \end{align}

with respect to this bit labeling is defined as follows. Let $\mathbf{c} \in \{0,1\}^{s_i}$ , and let $\mathbf{a}, \mathbf{b} \in \{0,1\}^{s_{i + 1}}$ be gates in layer $i + 1$ (with the possibility that $\mathbf{a} = \mathbf{b}$ ).

If gate $\mathbf{c}$ is:
- an addition gate, and
- the (multi)set of its two children is $\{\mathbf{a}, \mathbf{b}\}$ , and
- $\mathbf{a} \le \mathbf{b}$ ,

then we set $\mathrm{add}_i(\mathbf{c}, \mathbf{a}, \mathbf{b}) = 1$ ; otherwise, we set $\mathrm{add}_i(\mathbf{c}, \mathbf{a}, \mathbf{b}) = 0$ .

If gate $\mathbf{c}$ is:
- a multiplication gate, and
- the (multi)set of its two children is $\{\mathbf{a}, \mathbf{b}\}$ , and
- $\mathbf{a} \le \mathbf{b}$ ,

then we set $\mathrm{mult}_i(\mathbf{c}, \mathbf{a}, \mathbf{b}) = 1$ ; otherwise, we set $\mathrm{mult}_i(\mathbf{c}, \mathbf{a}, \mathbf{b}) = 0$ .

If $\mathbf{c}$ is the label of a nonexistent gate, i.e., $S_i$ is not a power of 2 and $\mathbf{c}$ is the binary representation of an integer exceeding $S_i - 1$ , $\mathrm{add}_i(\mathbf{c}, \mathbf{a}, \mathbf{b}) = \mathrm{mult}_i(\mathbf{c}, \mathbf{a}, \mathbf{b}) = 0$ .

We may then define the multilinear extensions

\begin{align} \widetilde{\mathrm{add}}_i & : \mathbb{F}^{s_i} \times \mathbb{F}^{s_{i + 1}} \times \mathbb{F}^{s_{i + 1}} \to \mathbb{F} \\ \widetilde{\mathrm{mult}}_i & : \mathbb{F}^{s_i} \times \mathbb{F}^{s_{i + 1}} \times \mathbb{F}^{s_{i + 1}} \to \mathbb{F} \end{align}

Remark 2

(i) The reason we define $\mathrm{add}_i(\mathbf{c}, \mathbf{a}, \mathbf{b})$ to be 0 unless $\mathbf{a} \le \mathbf{b}$ is precisely so that, if $\mathbf{a} \ne \mathbf{b}$ , then at most one of $\mathrm{add}_i(\mathbf{c}, \mathbf{a}, \mathbf{b})$ and $\mathrm{add}_i(\mathbf{c}, \mathbf{b}, \mathbf{a})$ can be 1. Similarly for $\mathrm{mult}_i$ . This avoids double counting in the layer-wise gate-value propagation equation and Thaler’s identity below.

(ii) For $A \subseteq \mathbb{F}$ , we may of course identify the domain $A^{s_i} \times A^{s_{i + 1}} \times A^{s_{i + 1}}$ with $A^{s_i + 2s_{i + 1}}$ , and write $(c_0,\ldots,c_{s_i - 1},a_0,\ldots,a_{s_{i + 1} - 1},b_0,\ldots,b_{s_{i + 1} - 1})$ instead of $((c_0,\ldots,c_{s_i - 1}),(a_0,\ldots,a_{s_{i + 1} - 1}),(b_0,\ldots,b_{s_{i + 1} - 1}))$ for the input of $\mathrm{add}_i$ and $\mathrm{mult}_i$ .

Example 4

ac_01.print_wiring_predicates()


ADDITION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

add_1((0,0),(0,0),(0,0)) = 1

add_1((1,1),(1,1),(1,1)) = 1


LAYER 0

add_0((1),(1,0),(1,1)) = 1


MULTIPLICATION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

mult_1((0,1),(0,1),(0,1)) = 1

mult_1((1,0),(0,1),(1,0)) = 1


LAYER 0

mult_0((0),(0,0),(0,1)) = 1

ac_01.print_wiring_predicate_mles()


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: ADD

LAYER 1

add̃_1(z_0,z_1,x_0,x_1,y_0,y_1) = 2*x_0*x_1*y_0*y_1*z_0*z_1 + 10*x_0*x_1*y_0*y_1*z_0 + 10*x_0*x_1*y_0*y_1*z_1 + x_0*x_1*y_0*y_1 + 10*x_0*x_1*y_0*z_0*z_1 + x_0*x_1*y_0*z_0 + x_0*x_1*y_0*z_1 + 10*x_0*x_1*y_0 + 10*x_0*x_1*y_1*z_0*z_1 + x_0*x_1*y_1*z_0 + x_0*x_1*y_1*z_1 + 10*x_0*x_1*y_1 + x_0*x_1*z_0*z_1 + 10*x_0*x_1*z_0 + 10*x_0*x_1*z_1 + x_0*x_1 + 10*x_0*y_0*y_1*z_0*z_1 + x_0*y_0*y_1*z_0 + x_0*y_0*y_1*z_1 + 10*x_0*y_0*y_1 + x_0*y_0*z_0*z_1 + 10*x_0*y_0*z_0 + 10*x_0*y_0*z_1 + x_0*y_0 + x_0*y_1*z_0*z_1 + 10*x_0*y_1*z_0 + 10*x_0*y_1*z_1 + x_0*y_1 + 10*x_0*z_0*z_1 + x_0*z_0 + x_0*z_1 + 10*x_0 + 10*x_1*y_0*y_1*z_0*z_1 + x_1*y_0*y_1*z_0 + x_1*y_0*y_1*z_1 + 10*x_1*y_0*y_1 + x_1*y_0*z_0*z_1 + 10*x_1*y_0*z_0 + 10*x_1*y_0*z_1 + x_1*y_0 + x_1*y_1*z_0*z_1 + 10*x_1*y_1*z_0 + 10*x_1*y_1*z_1 + x_1*y_1 + 10*x_1*z_0*z_1 + x_1*z_0 + x_1*z_1 + 10*x_1 + y_0*y_1*z_0*z_1 + 10*y_0*y_1*z_0 + 10*y_0*y_1*z_1 + y_0*y_1 + 10*y_0*z_0*z_1 + y_0*z_0 + y_0*z_1 + 10*y_0 + 10*y_1*z_0*z_1 + y_1*z_0 + y_1*z_1 + 10*y_1 + z_0*z_1 + 10*z_0 + 10*z_1 + 1

LAYER 0

add̃_0(z_0,x_0,x_1,y_0,y_1) = 10*x_0*x_1*y_0*y_1*z_0 + x_0*y_0*y_1*z_0


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: MULT

LAYER 1

mult̃_1(z_0,z_1,x_0,x_1,y_0,y_1) = 9*x_0*x_1*y_0*y_1*z_0*z_1 + x_0*x_1*y_0*y_1*z_0 + x_0*x_1*y_0*y_1*z_1 + x_0*x_1*y_0*z_0*z_1 + 10*x_0*x_1*y_0*z_0 + x_0*x_1*y_1*z_0*z_1 + 10*x_0*x_1*y_1*z_1 + 2*x_1*y_0*y_1*z_0*z_1 + 10*x_1*y_0*y_1*z_0 + 10*x_1*y_0*y_1*z_1 + 10*x_1*y_0*z_0*z_1 + x_1*y_0*z_0 + 10*x_1*y_1*z_0*z_1 + x_1*y_1*z_1

LAYER 0

mult̃_0(z_0,x_0,x_1,y_0,y_1) = x_0*x_1*y_0*y_1*z_0 + 10*x_0*x_1*y_0*y_1 + 10*x_0*x_1*y_1*z_0 + x_0*x_1*y_1 + 10*x_0*y_0*y_1*z_0 + x_0*y_0*y_1 + x_0*y_1*z_0 + 10*x_0*y_1 + 10*x_1*y_0*y_1*z_0 + x_1*y_0*y_1 + x_1*y_1*z_0 + 10*x_1*y_1 + y_0*y_1*z_0 + 10*y_0*y_1 + 10*y_1*z_0 + y_1

Thaler’s identity¶

The structure of an arithmetic circuit is fully described by the wiring predicates $\mathrm{add}_i$ and $\mathrm{mult}_i$ , which encode its topology but not the values assigned to the gates by the gate-value functions $W_i$ . The circuit’s computation can be expressed in terms of the gate-value functions and wiring predicates, as shown in part (a) of the following proposition. Part (b) enables us to apply the sum-check protocol to verify the output of a circuit, as we will explore in the next notebook. We refer to this as Thaler’s identity, a simplification by Thaler 1 of an identity of Cormode, Mitzenmacher, and Thaler 4.

Proposition 1

Let $C$ be a constant-input, binary, strictly layered arithmetic circuit of depth $d$ over a field $\mathbb{F}$ . For $0 \leq i \leq d$ , let Layer $i$ have size $S_i$ and bit length $s_i$ , and fix a bit labeling of each layer. For $0 \le i \le d$ , let $W_i$ be the gate-value function corresponding to this bit labeling, and for $0 \le i \le d - 1$ , let $\mathrm{add}_i$ and $\mathrm{mult}_i$ be the wiring predicates corresponding to this bit labeling.

(a) [Layer-wise gate-value propagation equation] Let $i \in \{0,\ldots,d - 1\}$ . For all $\mathbf{z} \in \{0,1\}^{s_i}$ ,

W_i(\mathbf{z}) = \sum_{\substack{\mathbf{x} \, \in \{0,1\}^{s_{i + 1}} \\ \mathbf{y} \, \in \{0,1\}^{s_{i + 1}}}} \Big\{ \mathrm{add}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ W_{i+1}(\mathbf{x}) + W_{i+1}(\mathbf{y})\big] + \mathrm{mult}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ W_{i+1}(\mathbf{x})W_{i+1}(\mathbf{y})\big]\Big\}.

(1)

(b) [Thaler’s identity] Let $i \in \{0,\ldots,d - 1\}$ . For all $\mathbf{z} \in \mathbb{F}^{s_i}$ ,

\widetilde{W}_i(\mathbf{z}) = \sum_{\substack{\mathbf{x} \, \in \{0,1\}^{s_{i + 1}} \\ \mathbf{y} \, \in \{0,1\}^{s_{i + 1}}}} \Big\{\widetilde{\mathrm{add}}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ \widetilde{W}_{i + 1}(\mathbf{x}) + \widetilde{W}_{i + 1}(\mathbf{y})\big] + \widetilde{\mathrm{mult}}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ \widetilde{W}_{i + 1}(\mathbf{x})\widetilde{W}_{i + 1}(\mathbf{y})\big]\Big\}.

(2)

Proof

(a) Let $\mathbf{z} \in \{0,1\}^{s_i}$ . When the (multi)set of $\mathbf{z}$ 's two children is $\{\mathbf{a}, \mathbf{b}\}$ with $\mathbf{a} \le \mathbf{b}$ , the only potentially nonzero summand on the right-hand side of (1) corresponds to $\mathbf{x} = \mathbf{a}$ and $\mathbf{y} = \mathbf{b}$ . Furthermore:

If $\mathbf{z}$ is an addition gate, then $\mathrm{mult}_i(\mathbf{z},\mathbf{a},\mathbf{b}) = 0$ , reducing the right-hand side to

\mathrm{add}_i(\mathbf{z},\mathbf{a},\mathbf{b})\big[ W_{i+1}(\mathbf{a}) + W_{i+1}(\mathbf{b})\big] = W_{i+1}(\mathbf{a}) + W_{i+1}(\mathbf{b}) = W_i(\mathbf{z}).

Similarly, if $\mathbf{z}$ is a multiplication gate, then $\mathrm{add}_i(\mathbf{z},\mathbf{a},\mathbf{b}) = 0$ , reducing the right-hand side to

\mathrm{mult}_i(\mathbf{z},\mathbf{a},\mathbf{b})\big[ W_{i+1}(\mathbf{a}) W_{i+1}(\mathbf{b})\big] = W_{i+1}(\mathbf{a}) W_{i+1}(\mathbf{b}) = W_i(\mathbf{z}).

(b) Still assuming $\mathbf{z} \in \{0,1\}^{s_i}$ , since $\mathbf{z}$ , $\mathbf{x}$ , and $\mathbf{y}$ lie in a Boolean hypercube, each function in the expression (1) can be replaced by its multilinear extension. Specifically, for $\mathbf{z} \in \{0,1\}^{s_i}$ ,

W_i(\mathbf{z}) = \widetilde{W}_i(\mathbf{z});

for $\mathbf{x}, \mathbf{y} \in \{0,1\}^{s_{i + 1}}$ ,

W_{i + 1}(\mathbf{x}) = \widetilde{W}_{i + 1}(\mathbf{x}) \quad \text{and} \quad W_{i + 1}(\mathbf{y}) = \widetilde{W}_{i + 1}(\mathbf{y});

and for $(\mathbf{z},\mathbf{x}, \mathbf{y}) \in \{0,1\}^{s_i} \times \{0,1\}^{s_{i + 1}} \times \{0,1\}^{s_{i + 1}}$ ,

\mathrm{add}_i(\mathbf{z},\mathbf{x},\mathbf{y}) = \widetilde{\mathrm{add}}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \quad \text{and} \quad \mathrm{mult}_i(\mathbf{z},\mathbf{x},\mathbf{y}) = \widetilde{\mathrm{mult}}_i(\mathbf{z},\mathbf{x},\mathbf{y}).

Therefore,

\begin{align} \begin{split} & \sum_{\substack{\mathbf{x} \, \in \{0,1\}^{s_{i + 1}} \\ \mathbf{y} \, \in \{0,1\}^{s_{i + 1}}}} \Big\{ \mathrm{add}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ W_{i+1}(\mathbf{x}) + W_{i+1}(\mathbf{y})\big] + \mathrm{mult}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ W_{i+1}(\mathbf{x})W_{i+1}(\mathbf{y})\big]\Big\} \\ & = \sum_{\substack{\mathbf{x} \, \in \{0,1\}^{s_{i + 1}} \\ \mathbf{y} \, \in \{0,1\}^{s_{i + 1}}}} \Big\{\widetilde{\mathrm{add}}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ \widetilde{W}_{i + 1}(\mathbf{x}) + \widetilde{W}_{i + 1}(\mathbf{y})\big] + \widetilde{\mathrm{mult}}_i(\mathbf{z},\mathbf{x},\mathbf{y}) \big[ \widetilde{W}_{i + 1}(\mathbf{x})\widetilde{W}_{i + 1}(\mathbf{y})\big]\Big\}. \end{split} \end{align}

The functions on both sides of (2) are defined for all $\mathbf{z} \in \mathbb{F}^{s_i}$ , and we’ve just shown they agree for all $\mathbf{z}$ in the Boolean hypercube $\{0,1\}^{s_i}$ . We claim that equality in fact holds for all $\mathbf{z}$ in $\mathbb{F}^{s_i}$ . Since the left-hand side is a multilinear extension of $W_i$ and the right hand side is an extension of $W_i$ , it suffices to show that the right-hand side is multilinear in $\mathbf{z}$ . By uniqueness of multilinear extensions, it then follows that both sides of (2) are the same function on $\mathbb{F}^{s_i}$ , viz. the multilinear extension of $W_i$ .

Indeed, given $\mathbf{x}, \mathbf{y} \in \{0,1\}^{s_{i + 1}}$ , $\widetilde{\mathrm{add}}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ and $\widetilde{\mathrm{mult}}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ are multilinear functions in $\mathbf{z}$ , because they are multilinear extensions of $\mathrm{add}_i$ and $\mathrm{mult}_i$ respectively. Recall the proposition of our multilinear extensions notebook, which states that the multilinear extension process is linear on function spaces, i.e. $\widetilde{cf + dg} = c\tilde{f} + d\tilde{g}$ . This implies that the summand on the right-hand side of (2) is a multilinear function in $\mathbf{z}$ , and therefore, in turn, that the entire sum is a multilinear function in $\mathbf{z}$ .

Remark 3

(i) We call a function multilinear if it is the evaluation map of some multilinear polynomial. For example, over $\mathbb{Z}/3\mathbb{Z}$ , the function $(z_0,z_1,x_0,x_1,y_0,y_1) \mapsto x_0^2y_1z_0^3 + x_1y_0^2z_1^3$ is multilinear in $(z_0,z_1)$ , because it is equivalent to the function $(z_0,z_1,x_0,x_1,y_0,y_1) \mapsto x_0^2y_1z_0 + x_1y_0^2z_1$ , which is the evaluation map of the polynomial $X_0^2Y_1Z_0 + X_1Y_0^2Z_1$ , which is multilinear in $(Z_0,Z_1)$ .

(ii) We did not use the fact that $\widetilde{\mathrm{add}}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ and $\widetilde{\mathrm{mult}}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ are multilinear functions with respect to $\mathbf{x}$ and $\mathbf{y}$ in the above proof. The hypotheses for Thaler’s identity can be relaxed: $\widetilde{\mathrm{add}}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ and $\widetilde{\mathrm{mult}}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ can be extensions of $\mathrm{add}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ and $\mathrm{mult}_i(\mathbf{z},\mathbf{x},\mathbf{y})$ that are multilinear in $\mathbf{z}$ .

ac_01.print_verification_propagation_equation()


VERIFICATION OF LAYER-WISE GATE-VALUE PROPAGATION EQUATION

LAYER 1

W_1(0,0) = 4, sum { add_1((0,0),x,y) [ W_2(x) + W_2(y) ] + mult_1((0,0),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W_1(0,1) = 9, sum { add_1((0,1),x,y) [ W_2(x) + W_2(y) ] + mult_1((0,1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W_1(1,0) = 1, sum { add_1((1,0),x,y) [ W_2(x) + W_2(y) ] + mult_1((1,0),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W_1(1,1) = 10, sum { add_1((1,1),x,y) [ W_2(x) + W_2(y) ] + mult_1((1,1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

LAYER 0

W_0(0) = 3, sum { add_0((0),x,y) [ W_1(x) + W_1(y) ] + mult_0((0),x,y) [ W_1(x) W_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W_0(1) = 0, sum { add_0((1),x,y) [ W_1(x) + W_1(y) ] + mult_0((1),x,y) [ W_1(x) W_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

ac_01.print_verification_propagation_equation(mle=True)


VERIFICATION OF THALER'S IDENTITY

LAYER 1

W̃_1(0,0) = 4, sum { add̃_1((0,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(0,1) = 9, sum { add̃_1((0,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(0,2) = 3, sum { add̃_1((0,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(0,3) = 8, sum { add̃_1((0,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(0,4) = 2, sum { add̃_1((0,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(0,5) = 7, sum { add̃_1((0,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(0,6) = 1, sum { add̃_1((0,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(0,7) = 6, sum { add̃_1((0,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(0,8) = 0, sum { add̃_1((0,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(0,9) = 5, sum { add̃_1((0,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(0,10) = 10, sum { add̃_1((0,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(1,0) = 1, sum { add̃_1((1,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(1,1) = 10, sum { add̃_1((1,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(1,2) = 8, sum { add̃_1((1,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(1,3) = 6, sum { add̃_1((1,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(1,4) = 4, sum { add̃_1((1,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(1,5) = 2, sum { add̃_1((1,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(1,6) = 0, sum { add̃_1((1,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(1,7) = 9, sum { add̃_1((1,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(1,8) = 7, sum { add̃_1((1,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(1,9) = 5, sum { add̃_1((1,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(1,10) = 3, sum { add̃_1((1,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(2,0) = 9, sum { add̃_1((2,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(2,1) = 0, sum { add̃_1((2,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(2,2) = 2, sum { add̃_1((2,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(2,3) = 4, sum { add̃_1((2,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(2,4) = 6, sum { add̃_1((2,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(2,5) = 8, sum { add̃_1((2,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(2,6) = 10, sum { add̃_1((2,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(2,7) = 1, sum { add̃_1((2,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(2,8) = 3, sum { add̃_1((2,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(2,9) = 5, sum { add̃_1((2,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(2,10) = 7, sum { add̃_1((2,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(3,0) = 6, sum { add̃_1((3,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(3,1) = 1, sum { add̃_1((3,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(3,2) = 7, sum { add̃_1((3,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(3,3) = 2, sum { add̃_1((3,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(3,4) = 8, sum { add̃_1((3,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(3,5) = 3, sum { add̃_1((3,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(3,6) = 9, sum { add̃_1((3,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(3,7) = 4, sum { add̃_1((3,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(3,8) = 10, sum { add̃_1((3,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(3,9) = 5, sum { add̃_1((3,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(3,10) = 0, sum { add̃_1((3,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(4,0) = 3, sum { add̃_1((4,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(4,1) = 2, sum { add̃_1((4,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(4,2) = 1, sum { add̃_1((4,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(4,3) = 0, sum { add̃_1((4,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(4,4) = 10, sum { add̃_1((4,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(4,5) = 9, sum { add̃_1((4,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(4,6) = 8, sum { add̃_1((4,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(4,7) = 7, sum { add̃_1((4,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(4,8) = 6, sum { add̃_1((4,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(4,9) = 5, sum { add̃_1((4,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(4,10) = 4, sum { add̃_1((4,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(5,0) = 0, sum { add̃_1((5,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(5,1) = 3, sum { add̃_1((5,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(5,2) = 6, sum { add̃_1((5,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(5,3) = 9, sum { add̃_1((5,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(5,4) = 1, sum { add̃_1((5,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(5,5) = 4, sum { add̃_1((5,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(5,6) = 7, sum { add̃_1((5,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(5,7) = 10, sum { add̃_1((5,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(5,8) = 2, sum { add̃_1((5,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(5,9) = 5, sum { add̃_1((5,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(5,10) = 8, sum { add̃_1((5,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(6,0) = 8, sum { add̃_1((6,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(6,1) = 4, sum { add̃_1((6,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(6,2) = 0, sum { add̃_1((6,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(6,3) = 7, sum { add̃_1((6,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(6,4) = 3, sum { add̃_1((6,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(6,5) = 10, sum { add̃_1((6,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(6,6) = 6, sum { add̃_1((6,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(6,7) = 2, sum { add̃_1((6,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(6,8) = 9, sum { add̃_1((6,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(6,9) = 5, sum { add̃_1((6,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(6,10) = 1, sum { add̃_1((6,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(7,0) = 5, sum { add̃_1((7,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,1) = 5, sum { add̃_1((7,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,2) = 5, sum { add̃_1((7,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,3) = 5, sum { add̃_1((7,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,4) = 5, sum { add̃_1((7,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,5) = 5, sum { add̃_1((7,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,6) = 5, sum { add̃_1((7,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,7) = 5, sum { add̃_1((7,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,8) = 5, sum { add̃_1((7,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,9) = 5, sum { add̃_1((7,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(7,10) = 5, sum { add̃_1((7,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((7,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(8,0) = 2, sum { add̃_1((8,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_1(8,1) = 6, sum { add̃_1((8,1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(8,2) = 10, sum { add̃_1((8,2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_1(8,3) = 3, sum { add̃_1((8,3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(8,4) = 7, sum { add̃_1((8,4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_1(8,5) = 0, sum { add̃_1((8,5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(8,6) = 4, sum { add̃_1((8,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(8,7) = 8, sum { add̃_1((8,7),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,7),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_1(8,8) = 1, sum { add̃_1((8,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(8,9) = 5, sum { add̃_1((8,9),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,9),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(8,10) = 9, sum { add̃_1((8,10),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((8,10),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_1(9,0) = 10, sum { add̃_1((9,0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((9,0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓


(Displayed 100 of 121 checked equations.)

LAYER 0

W̃_0(0) = 3, sum { add̃_0((0),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((0),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_0(1) = 0, sum { add̃_0((1),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((1),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_0(2) = 8, sum { add̃_0((2),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((2),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 8 ✓

W̃_0(3) = 5, sum { add̃_0((3),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((3),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_0(4) = 2, sum { add̃_0((4),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((4),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

W̃_0(5) = 10, sum { add̃_0((5),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((5),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 10 ✓

W̃_0(6) = 7, sum { add̃_0((6),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((6),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 7 ✓

W̃_0(7) = 4, sum { add̃_0((7),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((7),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_0(8) = 1, sum { add̃_0((8),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((8),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_0(9) = 9, sum { add̃_0((9),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((9),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_0(10) = 6, sum { add̃_0((10),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((10),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

Conclusion¶

Fix $\mathbf{z} \in \mathbb{F}^{s_i}$ . We may view the summand on the right-hand side of Thaler’s identity (2) as a function of $\mathbf{x}$ and $\mathbf{y}$ , rather than of $\mathbf{z}$ . Specifically, for fixed $\mathbf{z}$ it defines a polynomial function

F_{\mathbf{z}} : \mathbb{F}^{s_{i + 1}} \times \mathbb{F}^{s_{i + 1}} \to \mathbb{F},

which we may identify with a polynomial function on $\mathbb{F}^{2s_{i+1}}$ .

Moreover, this polynomial function may be represented by a polynomial that is multilinear (and hence of low total degree) in the variables $(\mathbf{x},\mathbf{y})$ . Thaler’s identity asserts that $\widetilde{W}_i(\mathbf{z})$ is equal to the sum of $F_{\mathbf{z}}$ over the Boolean hypercube $\{0,1\}^{2s_{i + 1}}$ . Consequently, for any fixed $\mathbf{z}$ , verification of (2) is amenable to the sum-check protocol.

Appendix A: further examples¶

Example 5

expression_02 = '(2 + 2)*(3*3)'
ac_02 = ArithmeticCircuit(expression_02, prime=7)

print(f"{expression_02} mod {ac_02.field.mod}")
display(ac_02.graphviz_circuit)
print(f"This circuit has size S = {ac_02.size} and depth d = {ac_02.depth}.")
ac_02.print_topological_order()
display(ac_02.graphviz_circuit_bitstring)
ac_02.print_gate_values()
ac_02.print_tilde_W()
ac_02.print_wiring_predicates()
ac_02.print_wiring_predicate_mles()
ac_02.print_verification_propagation_equation()
ac_02.print_verification_propagation_equation(mle=True)

(2 + 2)*(3*3) mod 7

This circuit has size S = 5 and depth d = 2.

TOPOLOGICAL ORDERING

2.0 -> 2.1 -> 1.0 -> 1.1 -> 0._


GATE VALUES

LAYER 2

W_2(0) = 2

W_2(1) = 3

LAYER 1

W_1(0) = 4

W_1(1) = 2

LAYER 0

W_0() = 1


MULTILINEAR EXTENSIONS OF GATE-VALUE FUNCTIONS

LAYER 2

W̃_2(x_0) = x_0 + 2

LAYER 1

W̃_1(x_0) = 5*x_0 + 4

LAYER 0

W̃_0() = 1


ADDITION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

add_1((0),(0),(0)) = 1


LAYER 0


MULTIPLICATION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

mult_1((1),(1),(1)) = 1


LAYER 0

mult_0((),(0),(1)) = 1


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: ADD

LAYER 1

add̃_1(z_0,x_0,y_0) = 6*x_0*y_0*z_0 + x_0*y_0 + x_0*z_0 + 6*x_0 + y_0*z_0 + 6*y_0 + 6*z_0 + 1

LAYER 0

add̃_0(x_0,y_0) = 0


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: MULT

LAYER 1

mult̃_1(z_0,x_0,y_0) = x_0*y_0*z_0

LAYER 0

mult̃_0(x_0,y_0) = 6*x_0*y_0 + y_0


VERIFICATION OF LAYER-WISE GATE-VALUE PROPAGATION EQUATION

LAYER 1

W_1(0) = 4, sum { add_1((0),x,y) [ W_2(x) + W_2(y) ] + mult_1((0),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 4 ✓

W_1(1) = 2, sum { add_1((1),x,y) [ W_2(x) + W_2(y) ] + mult_1((1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 2 ✓

LAYER 0

W_0() = 1, sum { add_0((),x,y) [ W_1(x) + W_1(y) ] + mult_0((),x,y) [ W_1(x) W_1(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 1 ✓


VERIFICATION OF THALER'S IDENTITY

LAYER 1

W̃_1(0) = 4, sum { add̃_1((0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 4 ✓

W̃_1(1) = 2, sum { add̃_1((1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 2 ✓

W̃_1(2) = 0, sum { add̃_1((2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 0 ✓

W̃_1(3) = 5, sum { add̃_1((3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 5 ✓

W̃_1(4) = 3, sum { add̃_1((4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 3 ✓

W̃_1(5) = 1, sum { add̃_1((5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 1 ✓

W̃_1(6) = 6, sum { add̃_1((6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 6 ✓

LAYER 0

W̃_0() = 1, sum { add̃_0((),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 1 ✓

Example 6

expression_03a = '5*4 + 3'
expression_03b = '5*4 + (3 + 0)'
ac_03a = ArithmeticCircuit(expression_03a, prime=7, strict=False)
ac_03b = ArithmeticCircuit(expression_03b, prime=7)

print(f"{expression_03a} mod {ac_03a.field.mod}")
display(ac_03a.graphviz_circuit)

print(f"- The above is not a strictly layered circuit because the input 3 is not in Layer {ac_03a.depth} (the depth of the circuit).")
print(f"- If an arithmetic circuit can't model such a simple computation, it is rather otiose.")
print(f"- There is a simple workaround: note that {expression_03a} = {expression_03b}.\n")
print(f"{expression_03b} mod {ac_03b.field.mod}")
display(ac_03b.graphviz_circuit)

ac_03b.print_topological_order()
display(ac_03b.graphviz_circuit_bitstring)
ac_03b.print_gate_values()
ac_03b.print_tilde_W()
ac_03b.print_wiring_predicates()
ac_03b.print_wiring_predicate_mles()
ac_03b.print_verification_propagation_equation()
ac_03b.print_verification_propagation_equation(mle=True)

5*4 + 3 mod 7

- The above is not a strictly layered circuit because the input 3 is not in Layer 2 (the depth of the circuit).
- If an arithmetic circuit can't model such a simple computation, it is rather otiose.
- There is a simple workaround: note that 5*4 + 3 = 5*4 + (3 + 0).

5*4 + (3 + 0) mod 7


TOPOLOGICAL ORDERING

2.00 -> 2.01 -> 2.10 -> 2.11 -> 1.0 -> 1.1 -> 0._


GATE VALUES

LAYER 2

W_2(0,0) = 5

W_2(0,1) = 4

W_2(1,0) = 3

W_2(1,1) = 0

LAYER 1

W_1(0) = 6

W_1(1) = 3

LAYER 0

W_0() = 2


MULTILINEAR EXTENSIONS OF GATE-VALUE FUNCTIONS

LAYER 2

W̃_2(x_0, x_1) = 5*x_0*x_1 + 5*x_0 + 6*x_1 + 5

LAYER 1

W̃_1(x_0) = 4*x_0 + 6

LAYER 0

W̃_0() = 2


ADDITION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

add_1((1),(1,0),(1,1)) = 1


LAYER 0

add_0((),(0),(1)) = 1


MULTIPLICATION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

mult_1((0),(0,0),(0,1)) = 1


LAYER 0


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: ADD

LAYER 1

add̃_1(z_0,x_0,x_1,y_0,y_1) = 6*x_0*x_1*y_0*y_1*z_0 + x_0*y_0*y_1*z_0

LAYER 0

add̃_0(x_0,y_0) = 6*x_0*y_0 + y_0


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: MULT

LAYER 1

mult̃_1(z_0,x_0,x_1,y_0,y_1) = x_0*x_1*y_0*y_1*z_0 + 6*x_0*x_1*y_0*y_1 + 6*x_0*x_1*y_1*z_0 + x_0*x_1*y_1 + 6*x_0*y_0*y_1*z_0 + x_0*y_0*y_1 + x_0*y_1*z_0 + 6*x_0*y_1 + 6*x_1*y_0*y_1*z_0 + x_1*y_0*y_1 + x_1*y_1*z_0 + 6*x_1*y_1 + y_0*y_1*z_0 + 6*y_0*y_1 + 6*y_1*z_0 + y_1

LAYER 0

mult̃_0(x_0,y_0) = 0


VERIFICATION OF LAYER-WISE GATE-VALUE PROPAGATION EQUATION

LAYER 1

W_1(0) = 6, sum { add_1((0),x,y) [ W_2(x) + W_2(y) ] + mult_1((0),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W_1(1) = 3, sum { add_1((1),x,y) [ W_2(x) + W_2(y) ] + mult_1((1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

LAYER 0

W_0() = 2, sum { add_0((),x,y) [ W_1(x) + W_1(y) ] + mult_0((),x,y) [ W_1(x) W_1(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 2 ✓


VERIFICATION OF THALER'S IDENTITY

LAYER 1

W̃_1(0) = 6, sum { add̃_1((0),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_1(1) = 3, sum { add̃_1((1),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((1),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 3 ✓

W̃_1(2) = 0, sum { add̃_1((2),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((2),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 0 ✓

W̃_1(3) = 4, sum { add̃_1((3),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((3),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 4 ✓

W̃_1(4) = 1, sum { add̃_1((4),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((4),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 1 ✓

W̃_1(5) = 5, sum { add̃_1((5),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((5),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 5 ✓

W̃_1(6) = 2, sum { add̃_1((6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 2 ✓

LAYER 0

W̃_0() = 2, sum { add̃_0((),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^1 × {0,1}^1 = 2 ✓

Example 7

expression_04 = '5*x + (3*4)'
ac_04 = ArithmeticCircuit(expression_04, prime=7, strict=False)

print(f"{expression_04} mod {ac_04.field.mod}")
display(ac_04.graphviz_circuit)

print(f"- The above is not a constant-input circuit because the input x a variable.")
print(f"- Nevertheless, we can still explore the arithmetic circuit.")
ac_04.print_topological_order()
display(ac_04.graphviz_circuit_bitstring)
print(ac_04.layers)

5*x + (3*4) mod 7

- The above is not a constant-input circuit because the input x a variable.
- Nevertheless, we can still explore the arithmetic circuit.

TOPOLOGICAL ORDERING

2.00 -> 2.01 -> 2.10 -> 2.11 -> 1.0 -> 1.1 -> 0._

{0: {'0._'}, 1: {'1.0', '1.1'}, 2: {'2.00', '2.01', '2.10', '2.11'}}

Example 8

expression_05a = '1*5 + 2*6'
expression_05b = '3*5 + 4*6'
ac_05 = ArithmeticCircuit(expression_05a, expression_05b, prime=43)

print(f"Here is an example of matrix multiplication: [ [1 2] [3 4] ] * [ [5] [6] ] ")

print(f"{expression_05a} mod {ac_05.field.mod}, {expression_05b} mod {ac_05.field.mod}")
display(ac_05.graphviz_circuit)
display(ac_05.graphviz_circuit_bitstring)
ac_05.print_topological_order()
display(ac_05.graphviz_circuit_bitstring)
ac_05.print_gate_values()
ac_05.print_tilde_W()
ac_05.print_wiring_predicates()
ac_05.print_wiring_predicate_mles()
# With prime field of size p = 43, there will be a large number of equations to print, so we just verify for a random selection
ac_05.print_verification_propagation_equation(random_selection=10)
ac_05.print_verification_propagation_equation(mle=True, random_selection=10)

Here is an example of matrix multiplication: [ [1 2] [3 4] ] * [ [5] [6] ] 
1*5 + 2*6 mod 43, 3*5 + 4*6 mod 43


TOPOLOGICAL ORDERING

2.001 -> 2.010 -> 2.011 -> 2.100 -> 2.101 -> 2.000 -> 1.00 -> 1.10 -> 1.11 -> 1.01 -> 0.0 -> 0.1


GATE VALUES

LAYER 2

W_2(0,0,0) = 4

W_2(0,0,1) = 1

W_2(0,1,0) = 5

W_2(0,1,1) = 2

W_2(1,0,0) = 6

W_2(1,0,1) = 3

W_2(1,1,0) = 0

W_2(1,1,1) = 0

LAYER 1

W_1(0,0) = 5

W_1(0,1) = 24

W_1(1,0) = 12

W_1(1,1) = 15

LAYER 0

W_0(0) = 17

W_0(1) = 39


MULTILINEAR EXTENSIONS OF GATE-VALUE FUNCTIONS

LAYER 2

W̃_2(x_0, x_1, x_2) = 3*x_0*x_1*x_2 + 36*x_0*x_1 + 2*x_0 + x_1 + 40*x_2 + 4

LAYER 1

W̃_1(x_0, x_1) = 27*x_0*x_1 + 7*x_0 + 19*x_1 + 5

LAYER 0

W̃_0(x_0) = 22*x_0 + 17


ADDITION WIRING PREDICATES (NONZERO VALUES)


LAYER 1


LAYER 0

add_0((0),(0,0),(1,0)) = 1

add_0((1),(0,1),(1,1)) = 1


MULTIPLICATION WIRING PREDICATES (NONZERO VALUES)


LAYER 1

mult_1((0,0),(0,0,1),(0,1,0)) = 1

mult_1((0,1),(0,0,0),(1,0,0)) = 1

mult_1((1,0),(0,1,1),(1,0,0)) = 1

mult_1((1,1),(0,1,0),(1,0,1)) = 1


LAYER 0


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: ADD

LAYER 1

add̃_1(z_0,z_1,x_0,x_1,x_2,y_0,y_1,y_2) = 0

LAYER 0

add̃_0(z_0,x_0,x_1,y_0,y_1) = 42*x_0*x_1*y_0*y_1 + 42*x_0*x_1*y_0*z_0 + x_0*x_1*y_0 + 42*x_0*y_0*y_1*z_0 + x_0*y_0*y_1 + x_0*y_0*z_0 + 42*x_0*y_0 + x_1*y_0*y_1 + x_1*y_0*z_0 + 42*x_1*y_0 + y_0*y_1*z_0 + 42*y_0*y_1 + 42*y_0*z_0 + y_0


MULTILINEAR EXTENSIONS OF WIRING PREDICATES: MULT

LAYER 1

mult̃_1(z_0,z_1,x_0,x_1,x_2,y_0,y_1,y_2) = 2*x_0*x_1*x_2*y_0*y_1*y_2*z_0*z_1 + 41*x_0*x_1*x_2*y_0*y_1*y_2*z_0 + 41*x_0*x_1*x_2*y_0*y_1*y_2*z_1 + x_0*x_1*x_2*y_0*y_1*y_2 + 40*x_0*x_1*x_2*y_0*y_1*z_0*z_1 + 2*x_0*x_1*x_2*y_0*y_1*z_0 + 2*x_0*x_1*x_2*y_0*y_1*z_1 + 42*x_0*x_1*x_2*y_0*y_1 + 42*x_0*x_1*x_2*y_0*y_2*z_0*z_1 + x_0*x_1*x_2*y_0*y_2*z_0 + x_0*x_1*x_2*y_0*y_2*z_1 + 2*x_0*x_1*x_2*y_0*z_0*z_1 + 42*x_0*x_1*x_2*y_0*z_0 + 42*x_0*x_1*x_2*y_0*z_1 + 42*x_0*x_1*x_2*y_1*y_2*z_0*z_1 + x_0*x_1*x_2*y_1*y_2*z_0 + x_0*x_1*x_2*y_1*y_2*z_1 + 42*x_0*x_1*x_2*y_1*y_2 + x_0*x_1*x_2*y_1*z_0*z_1 + 42*x_0*x_1*x_2*y_1*z_0 + 42*x_0*x_1*x_2*y_1*z_1 + x_0*x_1*x_2*y_1 + x_0*x_1*y_0*y_1*y_2*z_1 + x_0*x_1*y_0*y_1*z_0*z_1 + 42*x_0*x_1*y_0*y_1*z_1 + 42*x_0*x_1*y_0*y_2*z_1 + 42*x_0*x_1*y_0*z_0*z_1 + x_0*x_1*y_0*z_1 + 41*x_0*x_2*y_0*y_1*y_2*z_0*z_1 + x_0*x_2*y_0*y_1*y_2*z_0 + 2*x_0*x_2*y_0*y_1*y_2*z_1 + 42*x_0*x_2*y_0*y_1*y_2 + 2*x_0*x_2*y_0*y_1*z_0*z_1 + 42*x_0*x_2*y_0*y_1*z_0 + 41*x_0*x_2*y_0*y_1*z_1 + x_0*x_2*y_0*y_1 + x_0*x_2*y_0*y_2*z_0*z_1 + 42*x_0*x_2*y_0*y_2*z_1 + 42*x_0*x_2*y_0*z_0*z_1 + x_0*x_2*y_0*z_1 + x_0*x_2*y_1*y_2*z_0*z_1 + 42*x_0*x_2*y_1*y_2*z_0 + 42*x_0*x_2*y_1*y_2*z_1 + x_0*x_2*y_1*y_2 + 42*x_0*x_2*y_1*z_0*z_1 + x_0*x_2*y_1*z_0 + x_0*x_2*y_1*z_1 + 42*x_0*x_2*y_1 + x_0*y_0*y_1*y_2*z_0*z_1 + 42*x_0*y_0*y_1*y_2*z_1 + 42*x_0*y_0*y_1*z_0*z_1 + x_0*y_0*y_1*z_1 + 42*x_0*y_0*y_2*z_0*z_1 + x_0*y_0*y_2*z_1 + x_0*y_0*z_0*z_1 + 42*x_0*y_0*z_1 + 41*x_1*x_2*y_0*y_1*y_2*z_0*z_1 + 2*x_1*x_2*y_0*y_1*y_2*z_0 + 2*x_1*x_2*y_0*y_1*y_2*z_1 + 42*x_1*x_2*y_0*y_1*y_2 + 3*x_1*x_2*y_0*y_1*z_0*z_1 + 41*x_1*x_2*y_0*y_1*z_0 + 41*x_1*x_2*y_0*y_1*z_1 + x_1*x_2*y_0*y_1 + x_1*x_2*y_0*y_2*z_0*z_1 + 42*x_1*x_2*y_0*y_2*z_0 + 42*x_1*x_2*y_0*y_2*z_1 + 41*x_1*x_2*y_0*z_0*z_1 + x_1*x_2*y_0*z_0 + x_1*x_2*y_0*z_1 + x_1*x_2*y_1*y_2*z_0*z_1 + 42*x_1*x_2*y_1*y_2*z_0 + 42*x_1*x_2*y_1*y_2*z_1 + x_1*x_2*y_1*y_2 + 42*x_1*x_2*y_1*z_0*z_1 + x_1*x_2*y_1*z_0 + x_1*x_2*y_1*z_1 + 42*x_1*x_2*y_1 + 42*x_1*y_0*y_1*y_2*z_1 + 42*x_1*y_0*y_1*z_0*z_1 + x_1*y_0*y_1*z_1 + x_1*y_0*y_2*z_1 + x_1*y_0*z_0*z_1 + 42*x_1*y_0*z_1 + 2*x_2*y_0*y_1*y_2*z_0*z_1 + 42*x_2*y_0*y_1*y_2*z_0 + 41*x_2*y_0*y_1*y_2*z_1 + x_2*y_0*y_1*y_2 + 41*x_2*y_0*y_1*z_0*z_1 + x_2*y_0*y_1*z_0 + 2*x_2*y_0*y_1*z_1 + 42*x_2*y_0*y_1 + 42*x_2*y_0*y_2*z_0*z_1 + x_2*y_0*y_2*z_1 + x_2*y_0*z_0*z_1 + 42*x_2*y_0*z_1 + 42*x_2*y_1*y_2*z_0*z_1 + x_2*y_1*y_2*z_0 + x_2*y_1*y_2*z_1 + 42*x_2*y_1*y_2 + x_2*y_1*z_0*z_1 + 42*x_2*y_1*z_0 + 42*x_2*y_1*z_1 + x_2*y_1 + 42*y_0*y_1*y_2*z_0*z_1 + y_0*y_1*y_2*z_1 + y_0*y_1*z_0*z_1 + 42*y_0*y_1*z_1 + y_0*y_2*z_0*z_1 + 42*y_0*y_2*z_1 + 42*y_0*z_0*z_1 + y_0*z_1

LAYER 0

mult̃_0(z_0,x_0,x_1,y_0,y_1) = 0


VERIFICATION OF LAYER-WISE GATE-VALUE PROPAGATION EQUATION

LAYER 1

(Random selection of 4 z-values.)

W_1(1,1) = 15, sum { add_1((1,1),x,y) [ W_2(x) + W_2(y) ] + mult_1((1,1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 15 ✓

W_1(1,1) = 15, sum { add_1((1,1),x,y) [ W_2(x) + W_2(y) ] + mult_1((1,1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 15 ✓

W_1(1,1) = 15, sum { add_1((1,1),x,y) [ W_2(x) + W_2(y) ] + mult_1((1,1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 15 ✓

W_1(0,1) = 24, sum { add_1((0,1),x,y) [ W_2(x) + W_2(y) ] + mult_1((0,1),x,y) [ W_2(x) W_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 24 ✓

LAYER 0

(Random selection of 2 z-values.)

W_0(1) = 39, sum { add_0((1),x,y) [ W_1(x) + W_1(y) ] + mult_0((1),x,y) [ W_1(x) W_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 39 ✓

W_0(0) = 17, sum { add_0((0),x,y) [ W_1(x) + W_1(y) ] + mult_0((0),x,y) [ W_1(x) W_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 17 ✓


VERIFICATION OF THALER'S IDENTITY

LAYER 1

(Random selection of 10 z-values.)

W̃_1(19,8) = 8, sum { add̃_1((19,8),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((19,8),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 8 ✓

W̃_1(15,35) = 29, sum { add̃_1((15,35),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((15,35),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 29 ✓

W̃_1(18,33) = 26, sum { add̃_1((18,33),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((18,33),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 26 ✓

W̃_1(30,16) = 20, sum { add̃_1((30,16),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((30,16),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 20 ✓

W̃_1(34,19) = 29, sum { add̃_1((34,19),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((34,19),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 29 ✓

W̃_1(24,25) = 35, sum { add̃_1((24,25),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((24,25),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 35 ✓

W̃_1(19,34) = 37, sum { add̃_1((19,34),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((19,34),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 37 ✓

W̃_1(20,32) = 16, sum { add̃_1((20,32),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((20,32),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 16 ✓

W̃_1(31,6) = 26, sum { add̃_1((31,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((31,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 26 ✓

W̃_1(0,6) = 33, sum { add̃_1((0,6),x,y) [ W̃_2(x) + W̃_2(y) ] + mult̃_1((0,6),x,y) [ W̃_2(x) W̃_2(y)] } over (x,y) in {0,1}^3 × {0,1}^3 = 33 ✓

LAYER 0

(Random selection of 10 z-values.)

W̃_0(0) = 17, sum { add̃_0((0),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((0),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 17 ✓

W̃_0(27) = 9, sum { add̃_0((27),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((27),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 9 ✓

W̃_0(4) = 19, sum { add̃_0((4),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((4),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 19 ✓

W̃_0(18) = 26, sum { add̃_0((18),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((18),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 26 ✓

W̃_0(18) = 26, sum { add̃_0((18),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((18),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 26 ✓

W̃_0(3) = 40, sum { add̃_0((3),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((3),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 40 ✓

W̃_0(22) = 28, sum { add̃_0((22),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((22),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 28 ✓

W̃_0(21) = 6, sum { add̃_0((21),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((21),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 6 ✓

W̃_0(24) = 29, sum { add̃_0((24),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((24),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 29 ✓

W̃_0(40) = 37, sum { add̃_0((40),x,y) [ W̃_1(x) + W̃_1(y) ] + mult̃_0((40),x,y) [ W̃_1(x) W̃_1(y)] } over (x,y) in {0,1}^2 × {0,1}^2 = 37 ✓

References¶

Thaler, J. (2015). A note on the GKR protocol. https://api.semanticscholar.org/CorpusID:16402332
Goldwasser, S., Kalai, Y. T., & Rothblum, G. N. (2008). Delegating computation: Interactive proofs for muggles. Proceedings of the 40th Annual ACM Symposium on Theory of Computing (STOC), 113–122. 10.1145/1374376.1374396
Goldwasser, S., Kalai, Y. T., & Rothblum, G. N. (2015). Delegating computation: Interactive proofs for muggles. Journal of the ACM, 62(4), 1–64. 10.1145/2699436
Cormode, G., Mitzenmacher, M., & Thaler, J. (2012). Practical verified computation with streaming interactive proofs. Proceedings of the 3rd Innovations in Theoretical Computer Science Conference (ITCS), 90–112. 10.1145/2090236.2090245