This section covers the basic building blocks used to build the Cairo AIR.

Felt252 to M31

Cairo works over the prime field P=2251+172192+1P = 2^{251} + 17 \cdot 2^{192} + 1, while S-two works over the prime field M31=2311M31 = 2^{31} - 1. Thus, in order to represent the execution of Cairo with S-two, we need to decompose the 252-bit integers into 31-bit integers. The Cairo AIR chooses to use the 9-bit decomposition, so a single 252-bit integer will result in 28 9-bit limbs.

Range checks

Range-checks are very commonly used in the Cairo AIR. They are used to ensure that the values of the witness values are within a certain range, most commonly within a certain bit length. For example, in the Felt252 to M31 section, we saw that a 252-bit integer is decomposed into 28 9-bit limbs, so we need to verify that each limb is in the range 0limb<290 \leq \text{limb} < 2^{9}. This is done by using a preprocessed column that contains the entire range of possible values for the bit length. For example, for a 9-bit range check, the column will contain the values from 0 to 2912^9 − 1. We also have another column that contains the number of times the range-check was invoked for each valid value and we use lookups to check that each range-check is valid. For a more practical example, please refer to the Static Lookups section.