Stage 6 — Booleanity, Bytecode & Virtualization

RamHammingBooleanity

Degree 3

Rounds $\log_2 T$

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

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

RHS (input claim)

$$0$$

Integrand

\widetilde{\text{eq}}(r_{\text{cycle}}^{(1)}, X_t) \cdot \left(\textcolor{BurntOrange}{\textsf{RamHammingWeight}}(X_t)^{2} - \textcolor{BurntOrange}{\textsf{RamHammingWeight}}(X_t)\right)

Openings produced

$\textcolor{BurntOrange}{\textsf{RamHammingWeight}}(r_{\text{cycle}}^{(6)})$

IncClaimReduction

Degree 2

Rounds $\log_2 T$

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

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

RHS (input claim)

\textcolor{ForestGreen}{\textsf{RamInc}}(r_{\text{cycle}}^{(2)}) + \gamma \cdot \textcolor{ForestGreen}{\textsf{RamInc}}(r_{\text{cycle}}^{(4)}) + \gamma^{2} \cdot \textcolor{ForestGreen}{\textsf{RdInc}}(r_{\text{cycle}}^{(4)}) + \gamma^{3} \cdot \textcolor{ForestGreen}{\textsf{RdInc}}(r_{\text{cycle}}^{(5)})

Integrand

\textcolor{ForestGreen}{\textsf{RamInc}}(X_t) \cdot \left(\widetilde{\text{eq}}(r_{\text{cycle}}^{(2)}, X_t) + \gamma \cdot \widetilde{\text{eq}}(r_{\text{cycle}}^{(4)}, X_t)\right) + \gamma^{2} \cdot \textcolor{ForestGreen}{\textsf{RdInc}}(X_t) \cdot \left(\widetilde{\text{eq}}(r_{\text{cycle}}^{(4)}, X_t) + \gamma \cdot \widetilde{\text{eq}}(r_{\text{cycle}}^{(5)}, X_t)\right)

Openings produced

$\textcolor{ForestGreen}{\textsf{RamInc}}(r_{\text{cycle}}^{(6)})$
$\textcolor{ForestGreen}{\textsf{RdInc}}(r_{\text{cycle}}^{(6)})$

BytecodeReadRaf

Degree d_bc + 1

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

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

Opening point $(r_{K_{\text{bc}}}^{(6)}, r_{\text{cycle}}^{(6)})$

RHS (input claim)

\textcolor{BurntOrange}{\textsf{UnexpandedPC}}(r_{\text{cycle}}^{(1)}) + \gamma_1 \cdot \textcolor{BurntOrange}{\textsf{Imm}}(r_{\text{cycle}}^{(1)}) + \sum_{i=0}^{N_cflags-1} \gamma_1^{2+i} \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{cf}_{i})}(r_{\text{cycle}}^{(1)}) + \gamma \cdot \left(\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}(r_{\text{cycle}}^{(2)}) + \gamma_2 \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{Branch})}(r_{\text{cycle}}^{(2)}) + \gamma_2^{2} \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsRdNotZero})}(r_{\text{cycle}}^{(2)}) + \gamma_2^{3} \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{WriteLookupOutputToRD})}(r_{\text{cycle}}^{(2)}) + \gamma_2^{4} \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{VirtualInstruction})}(r_{\text{cycle}}^{(2)})\right) + \gamma^{2} \cdot \left(\textcolor{BurntOrange}{\textsf{Imm}}(r_{\text{cycle}}^{(3)}) + \gamma_3 \cdot \textcolor{BurntOrange}{\textsf{UnexpandedPC}}(r_{\text{cycle}}^{(3)}) + \gamma_3^{2} \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{LeftOperandIsRs1Value})}(r_{\text{cycle}}^{(3)}) + \gamma_3^{3} \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{LeftOperandIsPC})}(r_{\text{cycle}}^{(3)}) + \gamma_3^{4} \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{RightOperandIsRs2Value})}(r_{\text{cycle}}^{(3)}) + \gamma_3^{5} \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{RightOperandIsImm})}(r_{\text{cycle}}^{(3)}) + \gamma_3^{6} \cdot \textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsNoop})}(r_{\text{cycle}}^{(3)}) + \gamma_3^{7} \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{VirtualInstruction})}(r_{\text{cycle}}^{(3)}) + \gamma_3^{8} \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsFirstInSequence})}(r_{\text{cycle}}^{(3)})\right) + \gamma^{3} \cdot \left(\textcolor{BurntOrange}{\textsf{RdWa}}(r_{K_{\text{reg}}}^{(4)}, r_{\text{cycle}}^{(4)}) + \gamma_4 \cdot \textcolor{BurntOrange}{\textsf{Rs1Ra}}(r_{K_{\text{reg}}}^{(4)}, r_{\text{cycle}}^{(4)}) + \gamma_4^{2} \cdot \textcolor{BurntOrange}{\textsf{Rs2Ra}}(r_{K_{\text{reg}}}^{(4)}, r_{\text{cycle}}^{(4)})\right) + \gamma^{4} \cdot \left(\textcolor{BurntOrange}{\textsf{RdWa}}(r_{K_{\text{reg}}}^{(4)}, r_{\text{cycle}}^{(5)}) + \gamma_5 \cdot \textcolor{BurntOrange}{\textsf{InstructionRafFlag}}(r_{\text{cycle}}^{(5)}) + \sum_{i=0}^{N_tables-1} \gamma_5^{2+i} \cdot \textcolor{BurntOrange}{\textsf{TableFlag}(j)}(r_{\text{cycle}}^{(5)})\right) + \gamma^{5} \cdot \textcolor{BurntOrange}{\textsf{PC}}(r_{\text{cycle}}^{(1)}) + \gamma^{6} \cdot \textcolor{BurntOrange}{\textsf{PC}}(r_{\text{cycle}}^{(3)})

Integrand

\prod_{i=0}^{d_bc-1} \textcolor{ForestGreen}{\textsf{BytecodeRa}(i)}(X_k, X_t) \cdot \left(\widetilde{\text{eq}}(r_{\text{cycle}}^{(1)}, X_t) \cdot W_1(X_k) + \gamma \cdot \widetilde{\text{eq}}(r_{\text{cycle}}^{(2)}, X_t) \cdot W_2(X_k) + \gamma^{2} \cdot \widetilde{\text{eq}}(r_{\text{cycle}}^{(3)}, X_t) \cdot W_3(X_k) + \gamma^{3} \cdot \widetilde{\text{eq}}(r_{\text{cycle}}^{(4)}, X_t) \cdot W_4(X_k) + \gamma^{4} \cdot \widetilde{\text{eq}}(r_{\text{cycle}}^{(5)}, X_t) \cdot W_5(X_k)\right)

Openings produced

$\textcolor{ForestGreen}{\textsf{BytecodeRa}(i)}(r_{K_{\text{bc}}^{(i)}}^{(6)}, r_{\text{cycle}}^{(6)}) \text{ for } i=0,\ldots,d_{\text{bc}}-1$

InstructionRaVirtualization

Degree M + 1

Rounds $\log_2 T$

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

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

RHS (input claim)

\sum_{i=0}^{d_v-1} \gamma^i \cdot \textcolor{BurntOrange}{\textsf{InstructionRa}(i)}(r_{K_{\text{instr}}^{(i)}}^{(5)}, r_{\text{cycle}}^{(5)})

Integrand

\widetilde{\text{eq}}(r_{\text{cycle}}^{(5)}, X_t) \cdot \sum_{i=0}^{d_v-1} \gamma^i \cdot \prod_{j=0}^{M-1} \textcolor{ForestGreen}{\textsf{InstructionRa}(\text{iM+j})}(r_{K^{(iM+j)}}^{(5)}, X_t)

Openings produced

$\textsf{InstructionRa}(j)(r_{K^{(j)}}^{(5)}, r_{\text{cycle}}^{(6)}) \text{ for } j=0,\ldots,d_{\text{instr}}-1$

RamRaVirtualization

Degree d_ram + 1

Rounds $\log_2 T$

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

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

RHS (input claim)

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

Integrand

\widetilde{\text{eq}}(r_{\text{cycle}}^{(5)}, X_t) \cdot \prod_{i=0}^{d_ram-1} \textcolor{ForestGreen}{\textsf{RamRa}(i)}(r_{K_{\text{ram}}^{(i)}}^{(2)}, X_t)

Openings produced

$\textcolor{ForestGreen}{\textsf{RamRa}(i)}(r_{K_{\text{ram}}^{(i)}}^{(2)}, r_{\text{cycle}}^{(6)}) \text{ for } i=0,\ldots,d_{\text{ram}}-1$

Booleanity

Degree 3

Rounds $\log_2 N_{\text{instr}} + \log_2 T$

$\displaystyle\sum$ over: $X_k \in \{0,1\}^{\log_2 N_{\text{instr}}}, X_t \in \{0,1\}^{\log_2 T}$

Opening point $(r_{\text{addr}}^{(6)}, r_{\text{cycle}}^{(6)})$

RHS (input claim)

$$0$$

Integrand

\widetilde{\text{eq}}(r_{\text{addr}}^{(5)}, r_{\text{cycle}}^{(5)}, X_k, X_t) \cdot \sum_{j=0}^{d-1} \gamma^{2j} \cdot \left(\textcolor{ForestGreen}{\textsf{Ra}_{j}}(X_k, X_t)^{2} - \textcolor{ForestGreen}{\textsf{Ra}_{j}}(X_k, X_t)\right)

Openings produced

$\textsf{Ra}_{j}(r_{\text{addr}}^{(6)}, r_{\text{cycle}}^{(6)}) \text{ for } j=0,\ldots,d-1 (d = d_{\text{instr}} + d_{\text{bc}} + d_{\text{ram}})$