Module turshi 

This implements the constraints of the Cairo gates

Cairo programs can have the following assembly-like instructions:

• Memory access: [x]
• Assert equal: <left_hand_op> = <right_hand_op> · val · [reg1 + off_op1] · [reg0 + off_op0] +|* [reg1 + off_op1] · [reg0 + off_op0] +|* val · [[reg0 + off_op0] + off_op1]
• Jumps · jmp abs <address> // unconditional absolute jump · jmp rel <offset> // unconditional relative jump · jmp rel <offset> if <op> != 0 // conditional jump
• Functions · call abs <address> // calls a function (absolute location) · call rel <offset> // calls a function (relative location) · ret // returns to execution after the call
• Increments · ap += <op> · ap++

A Cairo program runs across a number of state transitions. Each state transition has the following structure:

• Has access to a read-only memory
• Input: 3 types of registers

• pc (= program counter): address of current instruction
• ap (= allocation pointer): first free memory address
• fp (= frame pointer): beginning of stack (for function arguments)

• Output:

• next_pc: address of next instruction
• next_ap: address of next free memory slot
• next_fp: pointer to stack (can remain the same as fp)

Cairo words are field elements of characteristic > 2^64 Cairo instructions are stored as words (63 or 64 bits - actual instruction or immediate value) Instructions with immediate values are stored in 2 words

• The first word stores instruction
• The second word stores the value

Words of instructions consist of

• 3 signed offsets of 16 bits each, in the range [-2^15,2^15) biased representation

• off_dst (= offset from destination address): used to compute address of assignment
• off_op0 (= offset from first operand): used to compute address of first operand in instruction
• off_op1 (= offset from second operand): used to compute address of second operand in instruction

• 15 bits of flags divided into 7 groups When multiple bits, at most one can be 1 and the rest must be 0
  • dst_reg [0] = fDST_REG : indicates what pointer off_dst refers to ( 0 => ap , 1 => fp )
  • op0_reg [1] = fOP0_REG : indicates what pointer off_op0 refers to ( 0 => ap , 1 => fp )
  • op1_src [2..4] : encodes the type of second operand · 0: indicates off_op1 is b in the double indexing [[ point + a ] + b ] · 1: indicates off_op1 is an immediate value = fOP1_VAL = 1 · 2: indicates offset off_op1 relative to fp = fOP1_FP = 1 · 4: indicates offset off_op1 relative to ap = fOP1_AP = 1
  • res_logic [5..6]: defines (if any) arithmetic operation in right part · 0: right part is single operand · 1: right part is addition = fRES_ADD = 1 · 2: right part is multiplication = fRES_MUL = 1
  • pc_update [7..9]: defines the type of update for the pc · 0 = regular increase by size of current instruction · 1 = absolute jump to res address = fPC_ABS_JMP = 1 · 2 = relative jump of step res = fPC_REL_JMP = 1 · 4 = conditional jump (jnz) with step in op1 = fPC_JNZ = 1
  • ap_update [10..11]: defines the type of update for the ap · 0: means the new ap is the same, same free position · 1: means there is an ap+=<op> instruction = fAP_INC = 1 · 2: means there is an ap++ instruction = fAP_ADD1 = 1
  • opcode [12..14]: encodes type of assembly instruction · 0: jumps or increments instruction · 1: call instruction = fOPC_CALL = 1 · 2: return instruction = fOPC_RET = 1 · 4: assert equal instruction (assignment to value or check equality) = fOPC_ASSEQ = 1
• in little-endian form = leftmost least significant bit

The transition function uses 4 auxiliary values:

• dst: left part of instruction, destination
• op0: content of first operand of right part
• op1: content of second operand of right part
• res: result of the operation in the right part

Modules

testing

witness

Structs

Claim

Flags

Instruction

Transition

Constants

CIRCUIT_GATE_COUNT

Functions

circuit_gate_combined_constraints

Combines the constraints for the Cairo gates depending on its type