
## sumcheck formula
> syntax: initial claim = sumcheck formula
### phase 1 out (gate x wit_out )
$$
\sum_{i} \alpha^{i} \space \text{wit_out}_{i}[rt_i || ry_i] = \sum_{i} \alpha^{i} \sum_{g \in [0, G]} \sum_{s || x} \text{eq($rt_i$, s)} \space \text{copy_to}_{\text{g ->i}}(ry_i, x) \ \text{V}_{g}[s||x]
$$
### phase 2 (gates), support linear/non linear/custom gate
$$
\sum_{g \in [0, G]} \alpha^{g} \space \text{V}_{g}[rt_g || ry_g] = \sum_{g \in [0, G]} \alpha^{g} \space \sum_{s || x} \text{eq($rt_g$, s)} \space \text{gate}_g(ry_g, x) \space \text{Gate}_g(V_g(s || x || c0), V_g(s || x || c1), ...)
$$
> here right-hand-side $V_g$ can come from either next layer, or previous layers as subset. In subset case, $Gate_g$ function as $\text{paste_from}(ry, x)$. c0, c1, c2, c3 ... are binary constant to access fixed fanin e.g. (0, 0), (0, 1), (1, 0), (1, 1)
### phase 1 (gate x gate full shuffle), linear operation
$$
\sum_{g1 \in [0, G]} \alpha^{g1} \space \text{V}_{g1}[rt_{g1} || ry_{g1}] = \sum_{g1 \in [0, G]} \alpha^{g1} \space \sum_{g2 \in [0, G]} \sum_{s || x} \text{eq($rt_{g1}$, s)} \space \text{copy_to}_{\text{g2 ->g1}}(ry_{g1}, x) \ \text{V}_{g2}[s||x]
$$
> here left-hand-side $V_{g1}$ can be subset copied to early layers.
### phase 1 input (gate x wit_in full shuffle)
$$
\sum_{g \in [0, G]} \alpha^{g} \space \text{V}_{g}[rt_g || ry_g] = \sum_{g \in [0, G]} \alpha^{g} \sum_{i} \sum_{s || x} \text{eq($rt_g$, s)} \space \text{paste_from}_{\text{i ->g}}(ry_g, x) \ \text{wit_in}_{i}[s||x]
$$