Stage 2 — Virtualization & RAM

Constraints 5 product constraints

Cycle var $X_t \in \{0,1\}^{\log_2 T}$

Constraint domain [-2, -1, 0, 1, 2]

Rounds $\log_2 T + 5$

\widetilde{\text{eq}}(r_{\text{cycle}}^{(1)}, X_t) \cdot L_{\tau_c}(X_c) \cdot \text{Left}(X_t, X_c) \cdot \text{Right}(X_t, X_c)

c	Label	Output	Left	Right
-2	Product	$\textcolor{BurntOrange}{\textsf{Product}}(X_t)$	$\textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(X_t)$	$\textcolor{BurntOrange}{\textsf{RightInstructionInput}}(X_t)$
-1	WriteLookupOutputToRD	$\textcolor{BurntOrange}{\textsf{WriteLookupOutputToRD}}(X_t)$	$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsRdNotZero})}(X_t)$	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{WriteLookupOutputToRD})}(X_t)$
0	WritePCtoRD	$\textcolor{BurntOrange}{\textsf{WritePCtoRD}}(X_t)$	$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsRdNotZero})}(X_t)$	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}(X_t)$
1	ShouldBranch	$\textcolor{BurntOrange}{\textsf{ShouldBranch}}(X_t)$	$\textcolor{BurntOrange}{\textsf{LookupOutput}}(X_t)$	$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{Branch})}(X_t)$
2	ShouldJump	$\textcolor{BurntOrange}{\textsf{ShouldJump}}(X_t)$	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}(X_t)$	$1 - \textcolor{BurntOrange}{\textsf{NextIsNoop}}(X_t)$

$\textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{RightInstructionInput}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsRdNotZero})}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{WriteLookupOutputToRD})}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{LookupOutput}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{Branch})}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{NextIsNoop}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{VirtualInstruction})}(r_{\text{cycle}}^{(2)})$

Degree 3

Rounds $\log_2 K_{\text{ram}} + \log_2 T$

$\displaystyle\sum$ over: $X_k \in \{0,1\}^{\log_2 K_{\text{ram}}}, X_j \in \{0,1\}^{\log_2 T}$

Opening point $(r_{K_{\text{ram}}}^{(2)}, r_{\text{cycle}}^{(2)})$

\textcolor{BurntOrange}{\textsf{RamReadValue}}(r_{\text{cycle}}^{(1)}) + \gamma \cdot \textcolor{BurntOrange}{\textsf{RamWriteValue}}(r_{\text{cycle}}^{(1)})

\widetilde{\text{eq}}(r_{\text{cycle}}^{(1)}, X_j) \cdot \textcolor{BurntOrange}{\textsf{RamRa}}(X_k, X_j) \cdot \left(\textcolor{BurntOrange}{\textsf{RamVal}}(X_k, X_j) + \gamma \cdot \left(\textcolor{BurntOrange}{\textsf{RamVal}}(X_k, X_j) + \textcolor{ForestGreen}{\textsf{RamInc}}(X_j)\right)\right)

$\textcolor{BurntOrange}{\textsf{RamVal}}(r_{K_{\text{ram}}}^{(2)}, r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{RamRa}}(r_{K_{\text{ram}}}^{(2)}, r_{\text{cycle}}^{(2)})$
$\textcolor{ForestGreen}{\textsf{RamInc}}(r_{\text{cycle}}^{(2)})$

Degree 2

Rounds $\log_2 T$

$\displaystyle\sum$ over: $X_j \in \{0,1\}^{\log_2 T}$

Opening point $(r_{\text{cycle}}^{(2)})$

\textcolor{BurntOrange}{\textsf{LookupOutput}}(r_{\text{cycle}}^{(1)}) + \gamma \cdot \textcolor{BurntOrange}{\textsf{LeftLookupOperand}}(r_{\text{cycle}}^{(1)}) + \gamma^{2} \cdot \textcolor{BurntOrange}{\textsf{RightLookupOperand}}(r_{\text{cycle}}^{(1)})

\widetilde{\text{eq}}(r_{\text{cycle}}^{(1)}, X_j) \cdot \left(\textcolor{BurntOrange}{\textsf{LookupOutput}}(X_j) + \gamma \cdot \textcolor{BurntOrange}{\textsf{LeftLookupOperand}}(X_j) + \gamma^{2} \cdot \textcolor{BurntOrange}{\textsf{RightLookupOperand}}(X_j)\right)

$\textcolor{BurntOrange}{\textsf{LookupOutput}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{LeftLookupOperand}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(r_{\text{cycle}}^{(2)})$
$\textcolor{BurntOrange}{\textsf{RightInstructionInput}}(r_{\text{cycle}}^{(2)})$

Degree 2

Rounds $\log_2 K_{\text{ram}}$

$\displaystyle\sum$ over: $X_k \in \{0,1\}^{\log_2 K_{\text{ram}}}$

Opening point $(r_{K_{\text{ram}}}^{(2)})$

\textcolor{BurntOrange}{\textsf{RamAddress}}(r_{\text{cycle}}^{(1)})

\textcolor{BurntOrange}{\textsf{RamRa}}(X_k, r_{\text{cycle}}^{(1)}) \cdot \textsf{unmap}(X_k)

$\textcolor{BurntOrange}{\textsf{RamRa}}(r_{K_{\text{ram}}}^{(2)}, r_{\text{cycle}}^{(1)})$

Degree 2

Rounds $\log_2 K_{\text{ram}}$

$\displaystyle\sum$ over: $X_k \in \{0,1\}^{\log_2 K_{\text{ram}}}$

Opening point $(r_{K_{\text{ram}}}^{(2)})$

$$0$$

\widetilde{\text{eq}}(r_{K_{\text{ram}}}^{(2)}, X_k) \cdot \textsf{io\_mask}(X_k) \cdot \left(\textcolor{BurntOrange}{\textsf{RamValFinal}}(X_k) - \textsf{ValIO}(X_k)\right)