How Cairo is used in StarkEx

In the overview, we treat the StarkEx service as one component of the system that includes the STARK Prover inside. Here we discuss what exactly is done by the Prover, and what is the goal of wrapping the Prover along with the StarkEx service.

The description here refers only to StarkEx. However, any application can use similar functionality on top of Cairo.

What our STARK Prover actually proves, is a correct execution of a Cairo program. Cairo is a general, Turing-complete language. You can read more about the Cairo language here. An important thing to bear in mind for this description is that Cairo operates in the following framework:

  • It is stateless. i.e. - the Cairo/Prover component of the system is not the one that holds the off-chain state.​

  • It cannot prove wrong transactions. By comparison, on L1, an invalid transaction can be executed, shown to be invalid and reverted. If the input to the Cairo program has an invalid transaction - the Cairo program would not be able to run with it (and then, we will have nothing to prove).

The Goals of StarkEx Backend

StarkEx backend service has two goals which naturally derive from the Cairo framework described above:

  1. Ensure that all transactions to be executed and proved, are valid according to the application business logic - so the Cairo program will be able to complete a run with them as an input.

  2. Prepare the input for the Cairo program and run it. This is done by first aggregating a sufficient number of valid transactions into one batch and then invoking the Cairo program with this batch of transactions as input. In this process, the STARK prover attests to the Cairo program's correct execution.

The Cairo program gets not only the transaction list, but also more information to correlate with the previous state. For example, if there is a transaction that transfers 500 USDC from Alice to Bob, the input to the Cairo program has to include the old balance of Alice's vault, alongside a Merkle path that ties it to the previous balancesTree root.

StarkEx Proves Batches

As a result of the modus operandi described above, we see that StarkEx works in units (and proves the validity) of batches. This is important since each batch contains a header, in addition to the transactions, that is used in the proof.

Here is an example of how the batch header is used. Let's look at the expiration_timestamp field, used in trades and transfers. Since the Cairo program is stateless, it is not aware of the current time and thus cannot verify the expiration of time. Thus, this must be done with blockchain time. However, comparing each and every timestamp in the batch on-chain, to the blockchain time is very expensive. To solve this problem and reduce costs, the StarkEx backend puts the minimum expiration time of all the transactions in the batch, in the batch header. The Cairo program attests that the expiration timestamp in each transaction is equal to or later than this minimum. After the proof submission, it is sufficient for the on-chain contract to only compare the minimal time with the blockchain time.