1. RamAddrEqRs1PlusImmIfLoadStore

if { Load + Store }
=> ( RamAddress ) == ( Rs1Value + Imm )

### 2. RamAddrEqZeroIfNotLoadStore

This is saying that if the instruction is not a laod or a store, we should not read from RAM.

if { 1 - Load - Store }
=> ( RamAddress ) == ( 0 )

3. RamReadEqRamWriteIfLoad

Macro Definition:

if { Load }
=> ( RamReadValue ) == ( RamWriteValue )

If we encounter a load instruction then the value we read from RAM should be the value we write into the destination register.

5. Rs2EqRamWriteIfStore

This is quite self explanatory.

Macro Definition:

if { Store }
=> ( Rs2Value ) == ( RamWriteValue )

6. LeftLookupZeroUnlessAddSubMul

Macro Definition:

if { AddOperands + SubtractOperands + MultiplyOperands }
=> ( LeftLookupOperand ) == ( 0 )

Mathematical Constraint:

(AddOperands + SubtractOperands + MultiplyOperands) * LeftLookupOperand = 0

For these instructions we do not use the look up table, and the answer is stored directly in the right operand.

7. LeftLookupEqLeftInputOtherwise

Macro Definition:

if { 1 - AddOperands - SubtractOperands - MultiplyOperands }
=> ( LeftLookupOperand ) == ( LeftInstructionInput )

Mathematical Constraint:

(1 - AddOperands - SubtractOperands - MultiplyOperands) * (LeftLookupOperand - LeftInstructionInput) = 0

These are for the lookup tables.

8. RightLookupAdd

Macro Definition:

if { AddOperands }
=> ( RightLookupOperand ) == ( LeftInstructionInput + RightInstructionInput )

Mathematical Constraint:

AddOperands * (RightLookupOperand - (LeftInstructionInput + RightInstructionInput)) = 0

Semantics:

• When enforced: Add operation
• What it checks: Right lookup operand equals the sum of inputs
• Purpose: For addition, lookup the sum (to verify it’s computed correctly)

9. RightLookupSub

Macro Definition:

if { SubtractOperands }
=> ( RightLookupOperand ) == ( LeftInstructionInput - RightInstructionInput + 0x10000000000000000 )

Mathematical Constraint:

SubtractOperands * (RightLookupOperand - (LeftInstructionInput - RightInstructionInput + 0x10000000000000000)) = 0

Semantics:

• When enforced: Subtract operation
• What it checks: Right lookup operand equals difference + offset
• Purpose: Converts signed subtraction to unsigned for lookup (two’s complement)
• Note: 0x10000000000000000 = 2^64 for 64-bit wraparound

10. RightLookupEqProductIfMul

Macro Definition:

if { MultiplyOperands }
=> ( RightLookupOperand ) == ( Product )

Mathematical Constraint:

MultiplyOperands * (RightLookupOperand - Product) = 0

This because multiplication is handled slightly differently in Jolt. We do not store the right and left inputs, but rather do the multiplication in the field and store the answer instead.

11. RightLookupEqRightInputOtherwise

These are instrictions we do direct look up table work at

Macro Definition:

if { 1 - AddOperands - SubtractOperands - MultiplyOperands - Advice }
=> ( RightLookupOperand ) == ( RightInstructionInput )

Mathematical Constraint:

(1 - AddOperands - SubtractOperands - MultiplyOperands - Advice) * (RightLookupOperand - RightInstructionInput) = 0

Semantics:

• When enforced: NOT arithmetic operation, NOT advice
• What it checks: Right lookup operand equals right instruction input

12. AssertLookupOne

Just check if lookup output flag is set.

Macro Definition:

if { Assert }
=> ( LookupOutput ) == ( 1 )

Mathematical Constraint:

Assert * (LookupOutput - 1) = 0

13. RdWriteEqLookupIfWriteLookupToRd

Wrote to register correctly

Macro Definition:

if { WriteLookupOutputToRD }
=> ( RdWriteValue ) == ( LookupOutput )

14. RdWriteEqPCPlusConstIfWritePCtoRD

Macro Definition:

if { WritePCtoRD }
=> ( RdWriteValue ) == ( UnexpandedPC + 4 - 2*IsCompressed )

• When enforced: Instruction writes PC to register (e.g., JAL, JALR)
• What it checks: Destination register gets return address
• Purpose: Implements return address saving for function calls
• Details:
  • Standard instruction: PC + 4
  • Compressed instruction: PC + 2

15. NextUnexpPCEqLookupIfShouldJump

Macro Definition:

if { ShouldJump }
=> ( NextUnexpandedPC ) == ( LookupOutput )

The jump address is the output of a lookup table.

16. NextUnexpPCEqPCPlusImmIfShouldBranch

Macro Definition:

if { ShouldBranch }
=> ( NextUnexpandedPC ) == ( UnexpandedPC + Imm )

17. NextUnexpPCUpdateOtherwise

• NOT branching, NOT jumping (sequential execution)
• Implements sequential instruction flow
• Details:
  • Standard: PC + 4
  • Compressed: PC + 2
  • Multi-cycle virtual: PC unchanged (DoNotUpdateUnexpandedPC = 1)

Macro Definition:

if { 1 - ShouldBranch - Jump }
=> ( NextUnexpandedPC ) == ( UnexpandedPC + 4 - 4*DoNotUpdateUnexpandedPC - 2*IsCompressed )

18. NextPCEqPCPlusOneIfInline

Pretty self explanatory.

Macro Definition:

if { VirtualInstruction }
=> ( NextPC ) == ( PC + 1 )

19. MustStartSequenceFromBeginning

Macro Definition:

if { NextIsVirtual - NextIsFirstInSequence }
=> ( DoNotUpdateUnexpandedPC ) == ( 1 )

Next is virtual instruction but NOT the first in sequence

Complement Patterns

Several constraints come in complementary pairs:

Example: Constraints 1 & 2 (RAM address handling)

Constraint 1: (Load + Store) * (RamAddress - (Rs1 + Imm)) = 0.
Constraint 2: (1 - Load - Store) * RamAddress = 0

Together they enforce:

• If Load OR Store: RamAddress = Rs1 + Imm
• Else: RamAddress = 0

This exhausts all possibilities since (Load + Store) + (1 - Load - Store) = 1 always.

Multi-way Conditions

Some constraints handle multiple cases:

Example: Constraints 6 & 7 (Lookup operand routing)

If AddOperands OR SubtractOperands OR MultiplyOperands:
    LeftLookupOperand = 0
Else:
    LeftLookupOperand = LeftInstructionInput