This is a study note of Hello, Cairo tutorial.

1 Basics

Cairo has four types: felt, struct, tuple and pointer T* where T is a type.

Cairo has nine types of expressions:

  • An integer literal of type felt.
  • An identifier of a constant or a reference. my_identifier, struct_name.member_name, or reference_name.member_name.
  • An address register: ap (allocation pointer) or fp (frame pointer). Both have type felt.
  • x + y, x - y, x * y, x / y, -x where x and y are expressions.
  • (x)
  • [x]: the value at the address x.
  • &x: the address of the expression x
  • cast(x, T) where x is an expression and T is a type. It cast the value x to type T.

A tuple is an ordered, finite list that can contain any combination of valid types. Each element can be accessed with a zero-based index like loc_tuple[2].

A reference can be defined as let ref_name : ref_type = ref_expr. A reference can be rebound and revoked. A reference can be thought as an alias to an expression.

A function call is a statement. You must use return at the end of the funciton even if there are no return values. You cannot call functions as part of other expressions, for example foo(bar()) is invalid.

The assert <expr0> = <expr1> does one of two things: if expr0 is memory cell that was not set before, it assigns a value to the memory cell and continue. Otherwise, it verifies that the two valules are the same and continue. If the two values are not the same, abort execution.

The main() function is the starting point of the Cairo program.

%builtins directive followed by the name of builtins are declared at the top of a Cairo code file. A builtin is utilized by writing the inputs to a dedicated memory segment accessed via the builtin pointer. The builtin directive adds those pointers as parameters to main, which can then be passed to any function using them. Pointer names follow the convention <builtin name>_ptr and pointer types can be found in the cairo_builtins module of the common library. The common builtins are: output, pedersen, range_check, ecdsa, bitwise.

The syntax {output_ptr : felt*} declares an implicit argument that adds both a corresponding argument and return value.

felt is the primitive type of field element. It is also the default type of a variable/argument. It is an integer in the range of -P/2 < x x P/2 where P is a very large prime number. The result of add, subtract, multiple, division is computed with modulo P.

tempvar is a syntactic sugar that allocates one memory cell and defines a temporary varible: tempvar var_name = <expr> is equivalent to two statements [ap] = <expr>; ap++ and let var_name = [ap - 1]. The scope of a temporary variable is restricted. it may be revoked due to jumps (e.g., if statement) or function calls.

A local variable is less restricted than tempvar. Local variables are placed at the beginning of the function stack, so they require prior allocation using the instruction alloc_locals (usually the first tatement in a function), but they can be accessed throughout the entire execution of the function.

The scope of the result of a function call is similar to that of a temporary variable. If you need to access the returned value later, you should copy the result to a local variable.

For technical reasons, when Cairo needs to retrieve the address of a local variable (&loc_variable), it needs to be told the value of the frame pointer register fp. The statement let (__fp__, _) = get_fp_and_pc() fulfills this requirement. __fp__ is the name Cairo looks for when it has to know fp.

2 Hints

The Cairo proof system is used for zero-knowledge proof (ZKP). There are two parties involved: a prover tries to prove that a certain computation we performed, and a verifier wants to verify the correctness of the proof. The prover doesn’t share the input (solution) with the verifier.

A hint is a piece of Python code that only the prover sees and executes. Hints are used to provide program inputs. The ids variable is the way hints communicate with Cairo objects. It can be used to read and write local variables. To get the address of a varible of type T*, use addr = ids.var_name.address_. Then Python uses memory[addr] to read/write the varible value.

The verifier takes unitialized (or guess, nondeterministic) variables and check constraints of results. The correctness of code from the point of view of the verifier is called “soundness”, and if it holds the code is said to be sound. When you analyze the soundness of the code you must ignore all the hints. The other direction – that indeed the hint will find the right index is called “completeness” (and of course when checking for “completeness” you do take into account the hints).

Hint can also be used to print debugging data.