Introduction

• this is a book on STARKs
• it is a work in progress

Finite Fields

Functions and low-degree extension

Extension Fields

Code Theory

• I think “succinct proofs and linear algebra” provides a good intro and notation

Hamming weight

hamming weight of a string is the number of non-zero entries.

The Hamming weight of a string is the number of symbols that are different from the zero-symbol of the alphabet used

For $s=(1,0,0,1,1)$ we have:

\text{hamming_weight}(s) = 3

in other words for $\vec{x}\in F^n$ we have:

\text{hamming_weight}(\vec{x}) = |{ i | x[i] \neq 0 }|

Hamming Distance

In information theory, the Hamming distance between two strings of equal length is the number of positions at which the corresponding symbols are different.

\text{hamming_distance}(\vec{x}, \vec{y}) = |{ i | x[i] \neq y[i] }|

Repeated code

$$G=[I_n,\cdots ,I_n{]}^t$$

($I_n$ is the identity, repeated $k$ times in the matrix)

$$G\vec{x}=[x[0],\cdots ,x[n-1],x[0],\cdots ,x[n-1],\cdots ]$$

($\vec{x}$ repeated $k$ times)

Reed–Solomon error correcting code

$$RS[F,D,\rho ]:=\{f:D\to F:deg(f)<\rho \cdot |D|\}$$

“the RS code of rate $\rho$ evaluated over $D$”.

Johnson bound

What is Johnson bound?

TODO: We should explain it here, and also make sure we have defined everything we need to understand it.

Let $V\in F^D$ be a code with minimum relative distance $1-\rho$, for $\rho \in (0,1)$. Then $V$ is $(1-\sqrt{\rho }-ϵ,1/(2ϵ\sqrt{\rho }))$-list-decodable for every $ϵ\in (0,1-\sqrt{\rho })$.

TODO: is this the conjecture, or is conjecture 2.3 from the DEEP paper the conjecture based on the Jonhson bound?

AIR

• check https://cronokirby.com/posts/2022/09/notes-on-stark-arithmetization/

Overview

Here’s some notes on how STARK works, following my read of the ethSTARK Documentation (thanks Bobbin for the pointer!).

Warning: the following explanation should look surprisingly close to PlonK or SNARKs in general, to anyone familiar with these other schemes. If you know PlonK, maybe you can think of STARKs as turboplonk without preprocessing and without copy constraints/permutation. Just turboplonk with a single custom gate that updates the next row, also the commitment scheme makes everything complicated.

The execution trace table

Imagine a table with $W$ columns representing registers, which can be used as temporary values in our program/circuit. The table has $N$ rows, which represent the temporary values of each of these registers in each “step” of the program/circuit.

For example, a table of 4 registers and 3 steps:

The constraints

There are two types of constraints which we want to enforce on this execution trace table to simulate our program:

• boundary constraints: if I understand correctly this is for initializing the inputs of your program in the first rows of the table (e.g. the second register must be set to 1 initially) as well as the outputs (e.g. the registers in the last two rows must contain $3$, $4$, and $5$).
• state transitions: these are constraints that apply to ALL contiguous pairs of rows (e.g. the first two registers added together in a row equal the value of the third register in the next row). The particularity of STARKs (and what makes them “scallable” and fast in practice) is that the same constraint is applied repeatidly. This is also why people like to use STARKs to implement zkVMs, as VMs do the same thing over and over.

This way of encoding a circuit as constraints is called AIR (for Algebraic Intermediate Representation).

Straw man 1: Doing things in the clear coz YOLO

Let’s see an example of how a STARK could work as a naive interactive protocol between a prover and verifier:

1. the prover constructs the execution trace table and sends it to the verifier
2. the verifier checks the constraints on the execution trace table by themselves

This protocol works if we don’t care about zero-knowledge, but it is obviously not very efficient: the prover sends a huge table to the verifier, and the verifier has to check that the table makes sense (vis a vis of the constraints) by checking every rows involved in the boundary constraints, and checking every contiguous pair of rows involved in the state transition constraints.

Straw man 2: Encoding things as polynomials for future profit

Let’s try to improve on the previous protocol by using polynomials. This step will not immediately improve anything, but will set the stage for the step afterwards. Before we talk about the change to the protocol let’s see two different observations:

First, let’s note that one can encode a list of values as a polynomial by applying a low-degree extension (LDE). That is, if your list of values look like this: $(y_0,y_1,y_2,\cdots )$, then interpolate these values into a polynomial $f$ such that $f(0)=y_0,f(1)=y_1,f(2)=y_2,\cdots$

Usually, as we’re acting in a field, a subgroup of large-enough size is chosen in place of $0,1,2$ as domain. You can read why’s that here. (This domain is called the “trace evaluation domain” by ethSTARK.)

Second, let’s see how to represent a constraint like “the first two registers added together in a row equal the value of the third register in the next row” as a polynomial. If the three registers in our examples are encoded as the polynomials $f_1,f_2,f_3$ then we need a way to encode “the next row”. If our domain is simply $(0,1,2,\cdots )$ then the next row for a polynomial $f_1(x)$ is simply $f_1(x+1)$. Similarly, if we’re using a subgroup generated by $g$ as domain, we can write the next row as $f_1(x\cdot g)$. So the previous example constraint can be written as the constraint polynomial $c_0(x)=f_1(x)+f_2(x)-f_3(x\cdot g)$.

If a constraint polynomial $c_0(x)$ is correctly satisfied by a given execution trace, then it should be zero on the entire domain (for state transition constraints) or on some values of the domain (for boundary constraints). This means we can write it as $c_0(x)=t(x)\cdot {\prod }_i(x-g^i)$ for some “quotient” polynomial $t$ and the evaluation points $g^i$ (that encode the rows) where the constraint should apply. (In other words, you can factor $c_0$ using its roots $g^i$.)

Note: for STARKs to be efficient, you shouldn’t have too many roots. Hence why boundary constraints should be limited to a few rows. But how does it work for state transition constraints that need to be applied to all the rows? The answer is that since we are in a subgroup there’s a very efficient way to compute ${\prod }_i(x-g^i)$. You can read more about that in Efficient computation of the vanishing polynomial of the Mina book.

At this point, you should understand that a prover that wants to convince you that a constraint $c_1$ applies to an execution trace table can do so by showing you that $t$ exists. The prover can do so by sending the verifier the $t$ polynomial and the verifier computes $c_1$ from the register polynomials and verifies that it is indeed equal to $t$ multiplied by the ${\prod }_i(x-g^i)$. This is what is done both in Plonk and in STARK.

Note: if a constraint doesn’t satisfy the execution trace, then you won’t be able to factor it with ${\prod }_i(x-g^i)$ as not all of the $g^i$ will be roots. For this reason you’ll get something like $c_1(x)=t(x)\cdot {\prod }_i(x-g^i)+r(x)$ for $r$ some “rest” polynomial. TODO: at this point can we still get a $t$ but it will have a high degree? If not then why do we have to do a low-degree test later?

Now let’s see our modification to the previous protocol:

1. Instead of sending the execution trace table, the prover encodes each column of the execution trace table (of height $N$) as polynomials, and sends the polynomials to the verifier.
2. The prover then creates the constraint polynomials $c_0,c_1,\cdots$ (as described above) for each constraint involved in the AIR.
3. The prover then computes the associated quotient polynomials $t_0,t_1,\cdots$ (as described above) and sends them to the verifier. Note that the ethSTARK paper call these quotient polynomials the constraint polynomials (sorry for the confusion).
4. The verifier now has to check two things:
   • low-degree check: that these quotient polynomials are indeed low-degree. This is easy as we’re doing everything in the clear for now (TODO: why do we need to check that though?)
   • correctness check: that these quotient polynomials were correctly constructed. For example, the verifier can check that for $t_0$ by computing $c_0$ themselves using the execution trace polynomials and then checking that it equals $t_0\cdot (x-1)$. That is, assuming that the first constraint $c_0$ only apply to the first row $g^0=1$.

Straw man 3: Let’s make use of the polynomials with the Schwartz-Zippel optimization!

The verifier doesn’t actually have to compute and compare large polynomials in the correctness check. Using the Schwartz-Zippel lemma one can check that two polynomials are equal by evaluating both of them at a random value and checking that the evaluations match. This is because Schwartz-Zippel tells us that two polynomials that are equal will be equal on all their evaluations, but if they differ they will differ on most of their evaluations.

So the previous protocol can be modified to:

1. The prover sends the columns of the execution trace as polynomials $f_0,f_1,\cdots$ to the verifier.
2. The prover produces the quotient polynomials $t_0,t_1,\cdots$ and sends them to the verifier.
3. The verifier produces a random evaluation point $z$.
4. The verifier checks that each quotient polynomial has been computed correctly. For example, for the first constraint, they evaluate $c_0$ at $z$, then evaluate $t_0(z)\cdot (z-1)$, then check that both evaluations match.

Straw man 4: Using commitments to hide stuff and reduce proof size!

As the title indicates, we eventually want to use commitments in our scheme so that we can add zero-knowledge (by hiding the polynomials we’re sending) and reduce the proof size (our commitments will be much smaller than what they commit).

The commitments used in STARKs are merkle trees, where the leaves contain evaluations of a polynomial. Unlike the commitments used in SNARKs (like IPA and KZG), merkle trees don’t have an algebraic structure and thus are quite limited in what they allow us to do. Most of the complexity in STARKs come from the commitments. In this section we will not open that pandora box, and assume that the commitments we’re using are normal polynomial commitment schemes which allow us to not only commit to polynomials, but also evaluate them and provide proofs that the evaluations are correct.

Now our protocol looks like this:

1. The prover commits to the execution trace columns polynomials, then sends the commitments to the verifier.
2. The prover commits to the quotient polynomials, the sends them to the verifier.
3. The verifier sends a random value $z$.
4. The prover evaluates the execution trace column polynomials at $z$ and $z\cdot g$ (remember the verifier might want to evaluate a constraint that looks like this $c_0(x)=f1(x)+f2(x)-f3(x\cdot g)$ as it also uses the next row) and sends the evaluations to the verifier.
5. The prover evaluates the quotient polynomials at $z$ and sends the evaluations to the verifier (these evaluations are called “masks” in the paper).
6. For each evaluation, the prover also sends evaluation proofs.
7. The verifier verifies all evaluation proofs.
8. The verifier then checks that each constraint is satisfied, by checking the $t=c\cdot {\prod }_i(x-g^i)$ equation in the clear (using the evaluations provided by the prover).

Straw man 5: a random linear combination to reduce all the checks to a single check

If you’ve been reading STARK papers you’re probably wondering where the heck is the composition polynomial. That final polynomial is simply a way to aggregate a number of checks in order to optimize the protocol.

The idea is that instead of checking a property on a list of polynomial, you can check that property on a random linear combination. For example, instead of checking that $f_1(z)=3$ and $f_2(z)=4$, and $f_3(z)=8$, you can check that for random values $r_1,r_2,r_3$ you have:

$$r_1\cdot f_1(z)+r_2\cdot f_2(z)+r_3\cdot f_3(z)=3r_1+4r_2+8r_3$$

Often we avoid generating multiple random values and instead use powers of a single random value, which is a tiny bit less secure but much more practical for a number of reasons I won’t touch here. So things often look like this instead, with a random value $r$:

$$f_1(z)+r\cdot f_2(z)+r^2\cdot f_3(z)=3+4r+8r^2$$

Now our protocol should look like this:

1. The prover commits to the execution trace columns polynomials, then sends the commitments to the verifier.
2. The verifier sends a random value $r$.
3. The prover produces a random linear combination of the constraint polynomials.
4. The prover produces the quotient polynomial for that random linear combination, which ethSTARK calls the composition polynomial.
5. The prover commits to the composition polynomial, then sends them to the verifier.
6. The protocol continues pretty much like the previous one

Note: in the ethSTARK paper they note that the composition polynomial is likely of higher degree than the polynomials encoding the execution trace columns. (The degree of the composition polynomial is equal to the degree of the highest-degree constraint.) For this reason, there’s some further optimization that split the composition polynomial into several polynomials, but we will avoid talking about it here.

We now have a protocol that looks somewhat clean, which seems contradictory with the level of complexity introduced by the various papers. Let’s fix that in the next blogpost on FRI…

FRI

Cairo

Check cairo book: https://book.cairo-lang.org/

There’s different ways to write for the Cairo VM:

• using Cairo instructions directly, documented in the Cairo paper (good luck)
• using Cairo 0, a low-level language documented here https://docs.cairo-lang.org/how_cairo_works/builtins.html
• using Cairo 1, a rust-like high-level language documented here https://book.cairo-lang.org/

Public Memory

Here are some notes on how the Cairo zkVM encodes its (public) memory in the AIR (arithmetization) of the STARK.

If you’d rather watch a 25min video of the article, here it is:

The AIR arithmetization is limited on how it can handle public inputs and outputs, as it only offer boundary constraints. These boundary constraints can only be used on a few rows, otherwise they’re expensive to compute for the verifier. (A verifier would have to compute ${\prod }_{i\in S}(x-g^i)$ for some given $x$, so we want to keep $|S|$ small.)

For this reason Cairo introduce another way to get the program and its public inputs/outputs in: public memory. This public memory is strongly related to the memory vector of cairo which a program can read and write to.

In this article we’ll talk about both. This is to accompany this video and section 9.7 of the Cairo paper.

Cairo’s memory

Cairo’s memory layout is a single vector that is indexed (each rows/entries is assigned to an address starting from 1) and is segmented. For example, the first $l$ rows are reserved for the program itself, some other rows are reserved for the program to write and read cells, etc.

Cairo uses a very natural “constraint-led” approach to memory, by making it write-once instead of read-write. That is, all accesses to the same address should yield the same value. Thus, we will check at some point that for an address $a$ and a value $v$, there’ll be some constraint that for any two $(a_1,v_1)$ and $(a_2,v_2)$ such that $a_1=a_2$, then $v_1=v_2$.

Accesses are part of the execution trace

At the beginning of our STARK, we saw in How STARKs work if you don’t care about FRI that the prover encodes, commits, and sends the columns of the execution trace to the verifier.

The memory, or memory accesses rather (as we will see), are columns of the execution trace as well.

The first two columns introduced in the paper are called $L_1.a$ and $L_1.v$. For each rows in these columns, they represent the access made to the address $a$ in memory, with value $v$. As said previously, we don’t care if that access is a write or a read as the difference between them are blurred (any read for a specific address could be the write).

These columns can be used as part of the Cairo CPU, but they don’t really prevent the prover from lying about the memory accesses:

1. First, we haven’t proven that all accesses to the same addresses $a_i$ always return the same value $v_i$.
2. Second, we haven’t proven that the memory contains fixed values in specific addresses. For example, it should contain the program itself in the first $l$ cells.

Let’s tackle the first question first, and we will address the second one later.

Another list to help

In order to prove that the two columns in the $L_1$ part of the execution trace, Cairo adds two columns to the execution trace: $L_2.a^{\prime }$ and $L_2.v^{\prime }$. These two columns contain essentially the same things as the $L_1$ columns, except that these times the accesses are sorted by address.

One might wonder at this point, why can’t L1 memory accesses be sorted? Because these accesses represents the actual memory accesses of the program during runtime, and this row by row (or step by step). The program might read the next instruction in some address, then jump and read the next instruction at some other address, etc. We can’t force the accesses to be sorted at this point.

We will have to prove (later) that $L_1$ and $L_2$ represent the same accesses (up to some permutation we don’t care about).

So let’s assume for now that $L_2$ correctly contains the same accesses as $L_1$ but sorted, what can we check on $L_2$?

The first thing we want to check is that it is indeed sorted. Or in other words:

• each access is on the same address as previous: $a_{i+1}^{\prime }=a_i^{\prime }$
• or on the next address: $a_{i+1}^{\prime }=a_i^{\prime }+1$

For this, Cairo adds a continuity constraint to its AIR:

The second thing we want to check is that accesses to the same addresses yield the same values. Now that things are sorted its easy to check this! We just need to check that:

• either the values are the same: $v_{i+1}^{\prime }=v_i^{\prime }$
• or the address being accessed was bumped so it’s fine to have different values: $a_{i+1}^{\prime }=a_i^{\prime }+1$

For this, Cairo adds a single-valued constraint to its AIR:

And that’s it! We now have proven that the $L_2$ columns represent correct memory accesses through the whole memory (although we didn’t check that the first access was at address $1$, not sure if Cairo checks that somewhere), and that the accesses are correct.

That is, as long as $L_2$ contains the same list of accesses as $L_1$.

A multiset check between $L_1$ and $L_2$

To ensure that two list of elements match, up to some permutation (meaning we don’t care how they were reordered), we can use the same permutation that Plonk uses (except that plonk fixes the permutation).

The check we want to perform is the following:

$$\{(a_i,v_i){\}}_i=\{(a_i^{\prime },v_i^{\prime }){\}}_i$$

But we can’t check tuples like that, so let’s get a random value $\alpha$ from the verifier and encode tuples as linear combinations:

$$\{a_i+\alpha \cdot v_i{\}}_i=\{a_i^{\prime }+\alpha \cdot v_i^{\prime }{\}}_i$$

Now, let’s observe that instead of checking that these two sets match, we can just check that two polynomials have the same roots (where the roots have been encoded to be the elements in our lists):

$$\prod _i[X-(a_i+\alpha \cdot v_i)]=\prod _i[X-(a_i^{\prime }+\alpha \cdot v_i^{\prime })]$$

Which is the same as checking that

$$\frac{{\prod }_i[X-(a_i+\alpha \cdot v_i)]}{{\prod }_i[X-(a_i^{\prime }+\alpha \cdot v_i^{\prime })]}=1$$

Finally, we observe that we can use Schwartz-Zippel to reduce this claim to evaluating the LHS at a random verifier point $z$. If the following is true at the random point $z$ then with high probability it is true in general:

$$\frac{{\prod }_i[z-(a_i+\alpha \cdot v_i)]}{{\prod }_i[z-(a_i^{\prime }+\alpha \cdot v_i^{\prime })]}=1$$

The next question to answer is, how do we check this thing in our STARK?

Creating a circuit for the multiset check

Recall that our AIR allows us to write a circuit using successive pairs of rows in the columns of our execution trace.

That is, while we can’t access all the $a_i$ and $a_i^{\prime }$ and $v_i$ and $v_i^{\prime }$ in one shot, we can access them row by row.

So the idea is to write a circuit that produces the previous section’s ratio row by row. To do that, we introduce a new column $p$ in our execution trace which will help us keep track of the ratio as we produce it.

$$p_i=p_{i-1}\cdot \frac{z-(a_i+\alpha \cdot v_i)}{z-(a_i^{\prime }+\alpha \cdot v_i^{\prime })}$$

This is how you compute that $p$ column of the execution trace as the prover.

Note that on the verifier side, as we can’t divide, we will have to create the circuit constraint by moving the denominator to the right-hand side:

$$p(g\cdot x)\cdot [z-(a^{\prime }(x)+\alpha \cdot v^{\prime }(x))]=p(x)\cdot [z-(a(x)+\alpha \cdot v(x))]$$

There are two additional (boundary) constraints that the verifier needs to impose to ensure that the multiset check is coherent:

• the initial value $p_0$ should be computed correctly ($p_0=\frac{z-(a_0+\alpha \cdot v_0)}{z-(a_0^{\prime }+\alpha \cdot v_0^{\prime })}$)
• the final value $p_{-1}$ should contain $1$

Importantly, let me note that this new column $p$ of the execution trace cannot be created, encoded to a polynomial, committed, and sent to the verifier in the same round as other columns of the execution trace. This is because it makes uses of two verifier challenges $z$ and $\alpha$ which have to be revealed after the other columns of the execution trace have been sent to the verifier.

Note: a way to understand this article is that the prover is now building the execution trace interactively with the help of the verifier, and parts of the circuits (here a permutation circuit) will need to use these columns of the execution trace that are built at different stages of the proof.

Inserting the public memory in the memory

Now is time to address the second half of the problem we stated earlier:

Second, we haven’t proven that the memory contains fixed values in specific addresses. For example, it should contain the program itself in the first $l$ cells.

To do this, the first $l$ accesses are replaced with accesses to $(0,0)$ in $L_1$. $L_2$ on the other hand uses acceses to the first parts of the memory and retrieves values from the public memory $m^{\ast }$ (e.g. $(1,m^{\ast }[0]),(2,m^{\ast }[1]),\cdots$).

This means two things:

1. the nominator of $p$ will contain $z-(0+\alpha \cdot 0)=z$ in the first $l$ iterations (so $z^l$). Furthermore, these will not be cancelled by any values in the denominator (as $L_2$ is supposedly using actual accesses to the public memory)
2. the denominator of $p$ will contain ${\prod }_{i\in [[0,l]]}[z-(a_i^{\prime }+\alpha \cdot m^{\ast }[i])]$, and these values won’t be canceled by values in the nominator either

As such, the final value of the accumulator should look like this if the prover followed our directions:

$$\frac{z^l}{{\prod }_{i\in [[0,l]]}[z-(a_i^{\prime }+\alpha \cdot m^{\ast }[i])]}$$

which we can enforce (as the verifier) with a boundary constraint.

Section 9.8 of the Cairo paper writes exactly that:

Bootloader

Builtins and Layouts

Builtins

Layouts

Different layouts are deployed on SHARP:

https://github.com/starkware-libs/starkex-contracts/tree/aecf37f2278b2df233edd13b686d0aa9462ada02/evm-verifier/solidity/contracts/cpu

Starkex

The starkex contracts are:

• deployed at 0x6cB3EE90C50a38A0e4662bB7e7E6e40B91361BF6
• and sit behind the upgradable smart contract at 0x47312450b3ac8b5b8e247a6bb6d523e7605bdb60.

By looking at the Constructor Arguments section of the implementation contract (which might be outdated at the moment of this writing, as the implementation contract is upgradable) one can see where the subcontracts are deployed:

• bootloaderProgramContract: 0x5d07afFAfc8721Ef3dEe4D11A2D1484CBf6A9dDf
• memoryPageFactRegistry_: 0xFD14567eaf9ba941cB8c8a94eEC14831ca7fD1b4
• cairoVerifierContracts]: 0x217750c27bE9147f9e358D9FF26a8224F8aCC214,0x630A97901Ac29590DF83f4A64B8D490D54caf239,0x8488e8f4e26eBa40faE229AB653d98E341cbE57B,0x9E614a417f8309575fC11b175A51599661f2Bd21,0xC879aF7D5eD80e4676C203FD300E640C297F31e3,0x78Af2BFB12Db15d35f7dE8DD77f29C299C78c590,0xe9664D230490d5A515ef7Ef30033d8075a8D0E24,0x03Fa911dfCa026D9C8Edb508851b390accF912e8
• hashedSupportedCairoVerifiers: 3178097804922730583543126053422762895998573737925004508949311089390705597156
• simpleBootloaderProgramHash: 2962621603719000361370283216422448934312521782617806945663080079725495842070

Note: The different verifier contracts correspond to the different layouts that are supported for Cairo (see the Builtins and Layouts of Cairo section of the book).

Somewhat outdated implementations live on Github at starkware-libs/starkex-contracts.

They implement the SHARP (SHARed Prover) verifier, which allows us to verify SHARP proofs on Ethereum.

Note: A number of contracts refer to “GPS” which is the old name for SHARP (general-proving service).

Any application on Ethereum that wants to use Cairo can make use of this service to verify proofs. The flow is split in two parts:

1. The proof is sent to the SHARP service, which verifies it and returns a fact.
2. The application can check that the fact has been verified.

We explain what “facts” are in facts section.

Fact Registry

The Starkex contracts implement the verifier side of the SHARP service. In other words, when people create proofs using the SHARP service, they can get them verified on Ethereum using the Starkex contracts.

First, let’s introduce what a fact is: a fact can be any computation that was computed by some logic in the smart contract. For example, a fact can be: “we successfully verified a proof for this Cairo program and these public inputs”. This example is actually the main fact that Starkex will register for the different applications making use of it. But internally, other facts are used whenever a computation (like verifying a proof) is split in different transactions that need to produce a snapshot of what has been done so far and resume from other snapshots. This is explained in more details in the Verifying Cairo proofs section.

A fact is represented (or authenticated) by a hash of its variables. As such, it is important that different applications or different contexts use “different” hash functions not to have collisions. This can be done by adding some domain separation string to the hash function, or as it is done by starkex by using different fact registries for different usecases.

The Fact Registry

Let’s introduce the smart contract in charge of these facts, FactRegistry.sol:

contract FactRegistry is IQueryableFactRegistry {
    // Mapping: fact hash -> true.
    mapping(bytes32 => bool) private verifiedFact

As you can see, facts are just tracked via a hashmap. Registering a fact is such straightfoward:

    function registerFact(bytes32 factHash) internal {
        // This function stores the fact hash in the mapping.
        verifiedFact[factHash] = true;

As well as checking if a fact has been registered:

    function isValid(bytes32 fact) external view override returns (bool) {
        return _factCheck(fact);
    }

Example of facts from external applications

An example of registering a fact can be seen, for example at the end of a proof verification. In GpsStatementVerifier.sol:verifyProofAndRegister():

    function verifyProofAndRegister(
        uint256[] calldata proofParams,
        uint256[] calldata proof,
        uint256[] calldata taskMetadata,
        uint256[] calldata cairoAuxInput,
        uint256 cairoVerifierId
    ) external {
        // TRUNCATED...

        registerGpsFacts(taskMetadata, publicMemoryPages, cairoAuxInput[OFFSET_OUTPUT_BEGIN_ADDR]);
    }

where registerGpsFacts is defined as:

    function registerGpsFacts(
        uint256[] calldata taskMetadata,
        uint256[] memory publicMemoryPages,
        uint256 outputStartAddress
    ) internal {
        // TRUNCATED...

        // Register the fact for each task.
        for (task = 0; task < nTasks; task++) {
            // TRUNCATED...

            bytes32 fact = keccak256(abi.encode(programHash, programOutputFact));

            // TRUNCATED...
            registerFact(fact);

            // TRUNCATED...
        }

        // TRUNCATED...
    }

Starknet is the main application making use of SHARP, and as such their smart contract uses the fact registry directly.

The main function of Starknet is updateState(), which updates the state based on proofs that have been verified:

    function updateState(
        int256 sequenceNumber,
        uint256[] calldata programOutput,
        uint256 onchainDataHash,
        uint256 onchainDataSize
    ) external onlyOperator {
        // TRUNCATED...

        bytes32 sharpFact = keccak256(
            abi.encode(programHash(), stateTransitionFact)
        );
        require(
            IFactRegistry(verifier()).isValid(sharpFact),
            "NO_STATE_TRANSITION_PROOF"
        );

        // TRUNCATED...

Example of checking if a fact internally

Another example we can look at is within a proof verification. As explained in Verifying a Cairo proof, a proof verification is split in multiple transactions.

For example, Merkle membership proofs are verified in segregated transactions, and then the fact that they were verified is used within another execution. The fact is first verified and then registered in MerkleStatementContract:verifyMerkle():

    function verifyMerkle(
        uint256[] memory merkleView,
        uint256[] memory initialMerkleQueue,
        uint256 height,
        uint256 expectedRoot
    ) public {
        // TRUNCATED...

        bytes32 resRoot = verifyMerkle(channelPtr, merkleQueuePtr, bytes32(expectedRoot), nQueries);
        bytes32 factHash;
        assembly {
            // Append the resulted root (should be the return value of verify) to dataToHashPtr.
            mstore(dataToHashPtr, resRoot)
            // Reset dataToHashPtr.
            dataToHashPtr := add(channelPtr, 0x20)
            factHash := keccak256(dataToHashPtr, add(mul(nQueries, 0x40), 0x20))
        }

        registerFact(factHash);
    }

and in MerkleStatementVerifier:verifyMerkle():

    function verifyMerkle(
        uint256, /*channelPtr*/
        uint256 queuePtr,
        bytes32 root,
        uint256 n
    ) internal view virtual override returns (bytes32) {
        // TRUNCATED...

        require(merkleStatementContract.isValid(statement), "INVALIDATED_MERKLE_STATEMENT");
        return root;
    }

where both use their own fact registry not to collide with other usecase (as pointed out at the beginning of this section).

Verifying Cairo proofs

Verifying a SHARP Cairo proof on the Starkex contracts is done in a number of transactions:

• 3 Verify Merkle transactions to verify Merkle paths (example)
• 8 Verify FRI transactions to verify the FRI proofs (example)
• A bunch of Register Continuous Memory Page transactions (example)
• A single Verify Proof and Register (example)

The reason the verification of a proof is split in multiple transactions is because proofs are too large, and the verification cost too much gas, to fit in a single transaction.

Note: Proofs can be split using stark-evm-adapter

Layouts

Different layouts are deployed on SHARP:

https://github.com/starkware-libs/starkex-contracts/tree/aecf37f2278b2df233edd13b686d0aa9462ada02/evm-verifier/solidity/contracts/cpu

Proof Splitter

Due to the gas limitations when verifying an original STARK proof, the proof generated by the Stone Prover should be split into three types: the main proof, Trace Merkle proof, and FRI proof. Typically, this includes one Main Proof accompanied by several Trace Merkle Proofs and FRI Proofs.

This process relies on the fact registry, which functions as verification snapshots. These snapshots can be viewed as pre-verified subproofs. This allows the Main Proof to be verified based on earlier snapshots obtained from the Merkle Proofs and FRI Proofs, thereby circumventing the bottleneck caused by gas limitations in a single EVM transaction.

This section aims to clarify the roles of the various proof types, showing how the split proof works with references to the source code in Cairo verifier contracts, Stone Prover and Stark EVM Adapter.

Main proof

The Main proof is the primary proof that corresponds to the original proof generated by the Stone Prover. It encompasses essential proof data, including commitments for traces and FRI layers, along with trace values necessary for deriving the deep composition polynomial $p_0$, among other elements.

At a high level, it performs the following two key functions:

1. Deriving a deep composition polynomial $p_0$
2. Checking FRI layers for $p_0$

This explanation reuses the notations from the ethSTARK paper.

The Main Proof contains the commitments for the traces and FRI, as well as the trace values for deriving the polynomial $p_0$.

These trace values, also referred to as mask values, can be categorized into two types:

1. Trace values involved in expressing $C_j(x)$ in the following composition polynomial:

$$h(x)=\sum _{j=1}^k{C}_j(x)({\alpha }_j{x}^{D-D_j^{-1}}+{\beta }_j)$$

2. Evaluations of the polynomials $h_i(x)$ decomposed from the $h(x)$:

$$h(x)=\sum _{i=0}^{M_2-1}{x}^i{h}_i(x^{M_2})$$

By invoking the CpuConstraintPoly contract to evaluate the $h(x)$ with the trace mask values, it checks the out-of-domain-sampling (oods) consistency among these provided trace values and the evaluations of decomposed composition polynomial.

In other word, to do the check at a random point $z$, they check:

$$\sum _{j=1}^k{C}_j(z)({\alpha }_j{z}^{D-D_j^{-1}}+{\beta }_j)==\sum _{i=0}^{M_2-1}{z}^i{h}_i(z^{M_2})$$

After passed the OODS consistency check, it proceeds to prepare and verifie the FRI layers for $p_0$.

By aggregating the trace values $y_{\ell }$ and evaluations ${\hat{y}}_i$ obtained from the OODS, it derives the deep composition polynomial $p_0$ (or quotient polynomial) through the CpuOods contract.

$$p_0(x)=\sum _{\ell =0}^{M_1-1}\frac{{\gamma }_{\ell }\cdot (f_{\ell }(x)-y_{\ell })}{x-z{g}^{s\ell }}+\sum _{i=0}^{M_2-1}\frac{{\gamma }_{M_1+i}\cdot (h_i(x)-{\hat{y}}_i)}{x-z^{M_2}}$$

FRI plays the role as a PCS. Doing this means that the prover has to prove that quotient polynomial $p_0$ exists for OODS evaluations and is of degree $d(h)-1$. During FRI the verifier will obtain different evaluations of $p_0$. For example if they want an evaluation of $p_0(3)$ the prover would have to produce merkle proofs for $f_{\ell }(3)$ for all $\ell$ and $h_i(3)$ for all $i$.

In the first FRI layer computation stage, the contract reads these induced values based on FRI queries and decommits them from the main proof. Three traces are required for the Cairo verifier: execution trace, interaction trace and composition trace. Each decommitment checks against a trace commitment, which should have been verified and registered as a fact in the Merkle fact registry.

These facts serve as verification snapshots, which are crucial when it is needed to split a verification into multiple stages. This approach is necessary due to various reasons, such as circumventing gas cost limitations or conserving gas costs for transaction retries based on a verified snapshot.

Similarly, the process of checking the FRI layers depends on the FRI Merkle verification snapshots obtained earlier. It involves verifying whether the fact is registered with the FRI layer’s commitment.

Other split proofs

In order to provide the verfication snapshots for the Main Proof, it is essential to first complete both the Trace Merkle Proofs and the FRI Merkle Proofs. These preliminary steps are necessary to generate the verification snapshots required for the Main Proof.

The MerkleStatementContract and FriStatementContract are specifically designed for verifying the Trace Merkle Proofs and FRI Merkle Proofs, respectively. Upon successful verification, these facts will be registered as verification snapshots.

Proof annotations

With the original proof file obtained from the Stone Prover, it is necessary to run its CPU verifier to generate the annotations. This process is akin to operating an offline simulator, which verifies the proof and simulates the required proof data as annotations. These annotations are then utilized by verifiers in other locations, such as the EVM Cairo verifier.

The primary reason for generating these annotations, rather than extracting directly from the original proof, would be to facilitate the restructuring of the data in the original proof into a clearer format. This restructuring is particularly beneficial for other verification procedures, such as those employed by EVM Cairo verifiers.

Here is an example of an annotated proof. This example showcases how annotations are combined with the original proof into a single JSON file for further processing. The annotations themselves represent various data points, here are some of the examples:

// execution trace commitment
"P->V[0:32]: /cpu air/STARK/Original/Commit on Trace: Commitment: Hash(0x3c8537043a0e5298ac50fd0c85a697b4f64ad84d000000000000000000000000)"

// interaction trace commitment
"P->V[32:64]: /cpu air/STARK/Interaction/Commit on Trace: Commitment: Hash(0xf5a5807d04f92b370a2ca27ccafaf40f196a27ab000000000000000000000000)"

// composition trace commitment
"P->V[64:96]: /cpu air/STARK/Out Of Domain Sampling/Commit on Trace: Commitment: Hash(0x2a0d752d3cf399e94ebc1cc8a425ce89d848b7d7000000000000000000000000)"

// verifier challenges for interaction trace 
"V->P: /cpu air/STARK/Interaction: Interaction element #0: Field Element(0x29767aebd00e6750d36470c07b003624f52e08794f24c23c17fdbcf66e1593f)",
"V->P: /cpu air/STARK/Interaction: Interaction element #1: Field Element(0x5e8b64f90ebe7e15559196630cd2bb6bb95b0d9121ff82adf708a2e6637b142)..."

// oods evaluation point
"V->P: /cpu air/STARK/Out Of Domain Sampling/OODS values: Evaluation point: Field Element(0x4f03c43ef1a1476cea9b31c4880f1808ed0dada6e2d650af829115186740856)"

// commitments for FRI layers
"P->V[8768:8800]: /cpu air/STARK/FRI/Commitment/Layer 1: Commitment: Hash(0x994586a93d3f0397b588be7eb5ea55ecaec10145000000000000000000000000)",
"V->P: /cpu air/STARK/FRI/Commitment/Layer 2: Evaluation point: Field Element(0x69d6218dda1b690e11974c0d7bce4b5fb6584f5b188d2d8988436c9d7423fac)",
"P->V[8800:8832]: /cpu air/STARK/FRI/Commitment/Layer 2: Commitment: Hash(0x533a5b9d2896a3a50338eba17f3c660f6fc89995000000000000000000000000..."

Open source library

The Stark EVM Adapter provides an API to facilitate the splitting of original proofs from the Stone Prover into these segmented proofs. This library is particularly useful for developers working with STARK proofs in EVM environments. Included in the repository is a demo script that illustrates the complete process of splitting a Stone proof. This script demonstrates not only how to split the proof but also how to submit the resultant proofs to the Cairo verifier contracts.

Bootloader

Starknet

See more: https://book.starknet.io/