Stage 1 — Spartan

Integrand structure

\widetilde{\text{eq}}((\tau_t, \tau_b), (X_t, X_b)) \cdot L_{\tau_c}(X_c) \cdot A_z(X_t, X_b, X_c) \cdot B_z(X_t, X_b, X_c)

RHS

$$0$$

Group 0 ($X_b = 0$)

c	Label	$A_z$ (guard)	$B_z$ (value)
-5	RamAddrZeroIfNotLoadStore	$1 - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Load})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Store})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RamAddress}}(X_t)$
-4	RamReadEqRamWriteIfLoad	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Load})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RamReadValue}}(X_t) - \textcolor{BurntOrange}{\textsf{RamWriteValue}}(X_t)$
-3	RamReadEqRdWriteIfLoad	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Load})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RamReadValue}}(X_t) - \textcolor{BurntOrange}{\textsf{RdWriteValue}}(X_t)$
-2	Rs2EqRamWriteIfStore	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Store})}(X_t)$	$\textcolor{BurntOrange}{\textsf{Rs2Value}}(X_t) - \textcolor{BurntOrange}{\textsf{RamWriteValue}}(X_t)$
-1	LeftLookupZeroUnlessAddSubMul	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Add})}(X_t) + \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Sub})}(X_t) + \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Mul})}(X_t)$	$\textcolor{BurntOrange}{\textsf{LeftLookupOperand}}(X_t)$
0	LeftLookupEqLeftInputOtherwise	$1 - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Add})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Sub})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Mul})}(X_t)$	$\textcolor{BurntOrange}{\textsf{LeftLookupOperand}}(X_t) - \textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(X_t)$
1	AssertLookupOne	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Assert})}(X_t)$	$\textcolor{BurntOrange}{\textsf{LookupOutput}}(X_t) - 1$
2	NextUnexpPCEqLookupIfJump	$\textcolor{BurntOrange}{\textsf{ShouldJump}}(X_t)$	$\textcolor{BurntOrange}{\textsf{NextUnexpandedPC}}(X_t) - \textcolor{BurntOrange}{\textsf{LookupOutput}}(X_t)$
3	NextPCEqPCPlusOneIfInline	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{VirtualInstruction})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{LastInSeq})}(X_t)$	$\textcolor{BurntOrange}{\textsf{NextPC}}(X_t) - \textcolor{BurntOrange}{\textsf{PC}}(X_t) - 1$
4	MustStartSequenceFromBeginning	$\textcolor{BurntOrange}{\textsf{NextIsVirtual}}(X_t) - \textcolor{BurntOrange}{\textsf{NextIsFirstInSequence}}(X_t)$	$1 - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{DoNotUpdateUnexpandedPC})}(X_t)$

Group 1 ($X_b = 1$)

c	Label	$A_z$ (guard)	$B_z$ (value)
-5	RamAddrEqRs1PlusImmIfLoadStore	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Load})}(X_t) + \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Store})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RamAddress}}(X_t) - \textcolor{BurntOrange}{\textsf{Rs1Value}}(X_t) - \textcolor{BurntOrange}{\textsf{Imm}}(X_t)$
-4	RightLookupAdd	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Add})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}(X_t) - \textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(X_t) - \textcolor{BurntOrange}{\textsf{RightInstructionInput}}(X_t)$
-3	RightLookupSub	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Sub})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}(X_t) - \textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(X_t) + \textcolor{BurntOrange}{\textsf{RightInstructionInput}}(X_t) - 2^{64}$
-2	RightLookupEqProductIfMul	$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Mul})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}(X_t) - \textcolor{BurntOrange}{\textsf{Product}}(X_t)$
-1	RightLookupEqRightInputOtherwise	$1 - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Add})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Sub})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Mul})}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Advice})}(X_t)$	$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}(X_t) - \textcolor{BurntOrange}{\textsf{RightInstructionInput}}(X_t)$
0	RdWriteEqLookupIfWriteLookupToRd	$\textcolor{BurntOrange}{\textsf{WriteLookupOutputToRD}}(X_t)$	$\textcolor{BurntOrange}{\textsf{RdWriteValue}}(X_t) - \textcolor{BurntOrange}{\textsf{LookupOutput}}(X_t)$
1	RdWriteEqPCPlusConstIfWritePCtoRD	$\textcolor{BurntOrange}{\textsf{WritePCtoRD}}(X_t)$	$\textcolor{BurntOrange}{\textsf{RdWriteValue}}(X_t) - \textcolor{BurntOrange}{\textsf{UnexpandedPC}}(X_t) - 4 + 2 \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsCompressed})}(X_t)$
2	NextUnexpPCEqPCPlusImmIfBranch	$\textcolor{BurntOrange}{\textsf{ShouldBranch}}(X_t)$	$\textcolor{BurntOrange}{\textsf{NextUnexpandedPC}}(X_t) - \textcolor{BurntOrange}{\textsf{UnexpandedPC}}(X_t) - \textcolor{BurntOrange}{\textsf{Imm}}(X_t)$
3	NextUnexpPCUpdateOtherwise	$1 - \textcolor{BurntOrange}{\textsf{ShouldBranch}}(X_t) - \textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}(X_t)$	$\textcolor{BurntOrange}{\textsf{NextUnexpandedPC}}(X_t) - \textcolor{BurntOrange}{\textsf{UnexpandedPC}}(X_t) - 4 + 4 \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{DoNotUpdateUnexpandedPC})}(X_t) + 2 \cdot \textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsCompressed})}(X_t)$
4	(zero-padded)	$0$	$0$

Openings produced

$\textcolor{BurntOrange}{\textsf{LeftInstructionInput}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{RightInstructionInput}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{Product}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{WriteLookupOutputToRD}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{WritePCtoRD}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{ShouldBranch}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{PC}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{UnexpandedPC}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{Imm}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{RamAddress}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{Rs1Value}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{Rs2Value}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{RdWriteValue}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{RamReadValue}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{RamWriteValue}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{LeftLookupOperand}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{NextUnexpandedPC}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{NextPC}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{NextIsVirtual}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{NextIsFirstInSequence}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{LookupOutput}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{ShouldJump}}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{AddOperands})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{SubtractOperands})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{MultiplyOperands})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Load})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Store})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{WriteLookupOutputToRD})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{VirtualInstruction})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Assert})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{DoNotUpdateUnexpandedPC})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Advice})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsCompressed})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsFirstInSequence})}(r_{\text{cycle}}^{(1)})$
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsLastInSequence})}(r_{\text{cycle}}^{(1)})$

Stage 1 — Spartan

SpartanOuter (Stage 1)

Integrand structure

RHS

Group 0 ($X_b = 0$)

Group 1 ($X_b = 1$)

Openings produced