An Intro into SNARKs and Trusted Computing

Overview:

 Imagine that you are a weak client that needs to run a heavy piece of code. The best option that you have is to outsource that computation to another party (like Amazon Web Services). Now obviously you should be able to trust this party, but is there a way to ensure that the party is returning both a good result and that they actually ran the program that you sent? This is what a SNARK sets out to accomplish.

 Informally, a SNARK (succinct non-interactive argument of knowledge) is a witness that allows a verifier (the client) to verify that their code was run and has a correct output by the prover (the server) sublinear with respect to the program work. Thus, when given a output and SNARK from a third party, the verifier can accept or reject the output based on the SNARK.

 A trivial solution to verification would just be to run the code on your own and verify that they gave the correct solution, but this isn't interesting in our use case, thus we constrain SNARKs to be sublinear with respect to the work of the computation.

Thus SNARKs are:

• Succinct: Allow for fast verification (sublinear w.r.t. program runtime/work)
• Non-interactive: Only one message to transfer between prover and verifier
• Give an Argument of Knowledge: Ensures that the prover has executed this program (with non-negl prob)

Formal Definition:

 Given a fast but potentially malicious prover $\mathcal{P}$, a slow but trusted verifier $\mathcal{V}$, a program $\Psi$, and input to the program $x$, $\mathcal{V}$ gives the computation $\Psi(x)$ to $\mathcal{P}$ to compute and receives output $y$ along with a proof $\pi$ that convinces $\mathcal{V}$ that $y = \Psi(x)$ (with non-negligibleA function $f(n)$ is non-negligible if $\exists c > 0$ s.t. $f(n) \geq \frac{1}{n^c}$ for all $n$. probability).

Specifically, a SNARK satisfies the following:
1.) Completeness: $y = \Psi(x) \implies$ a honest $\mathcal{P}$ can convince $\mathcal{V}$.
2.) Soundness: $y' \neq \Psi(x') \implies$ a dishonest $\mathcal{P}$ cannot convince $\mathcal{V}$ with non-neglA function $f(n)$ is non-negligible if $\exists c > 0$ s.t. $f(n) \geq \frac{1}{n^c}$ for all $n$. probability.
3.) Succinctness: $\mathcal{V}$'s cost to verify $\pi$ is sublinear to the work required to compute $\Psi(x)$

 This is a nice idea and all, but how do SNARKs really work? They seem useful for verifiers, but if they take too long to construct by the prover or have huge proof sizes, then they may not be practical. It turns out that there is a large amount of research into making SNARKs quick for the prover to construct, verifier to verify, and small enough to be useful. Thus lots of tools have been released to work with SNARKs by researchers.

For now we will just go over the GKR protocol (which is only one approach of many to construct SNARKs). The protocol can be divided into 3 main steps:

1.) Arithmetization into Layered Circuits
2.) Sumcheck Protocol
3.) Polynomial Commitment

Circuit Arithmetization:

 The first step of the GKR protocol is to arithmetize the program into a layered circuit. Essentially, it turns out that most programs can be represented by simple arithmetic constraints. To formalize this, let a constraint set be a set of rules applied to values of a set of variables. Also, arithmetic constraints only addition, multiplication, and equality are supported over a finite field modulo $p$.

 So when given a program $\Psi(\vec{X}) = Y$, the compiler produces constraints $\mathcal{C}(\vec{X}, Y, \vec{Z})$ such that $Y \text{ is correct} \Longleftrightarrow \exists \vec{Z} \text{ that satisfies } \mathcal{C}$. We call these $\vec{Z}$ values, witnesses.

 For instance, we may represent a program like Y = (X_0 + X_1) * (X_0 * X_1) as:

$$\text{Constraints: } X_0, X_1, Y, Z_0, Z_1\\ \begin{align*}Z_0 &= X_0 + X_1\\ Z_1 &= X_0 * X_1\\ Y &= Z_0 * Z_1\\ \end{align*}\\ \text{With a satisfying assignment being: }\\ X_0 = 1, X_1 = 2, Y = 6, Z_0 = 3, Z_1 = 2$$

 Note that loops, conditional branching, and assertions can also be represented this way! For example an if statement that may look something like:

if (a == b):
  c = 1;
else:
  c = 2;

This turns into the following arithmatic constraints:

$$\begin{align*} 0 &= Z * (a - b)\\ 0 &= Z * (c - 1)\\\\ \end{align*} \text{ (For the \emph{if} branch)}\\ \begin{align*} 0 &= (1 - Z) * W * (a - b) \tag{constraint for $a \neq b$ with $W = (a-b)^{-1}$}\\ 0 &= (1 - Z) * (c - 2) \end{align*}$$

Where $Z$ is set by the prover to 1 or 0 depending on which branch is taken. Assertions and looping can be derived in a similar manner and are left as an exercise to the reader.

 Memory accesses are somewhat tougher to handle, but treating them as a type of consistency check it is easier to represent. In general, we just extract all memory operations and check that for every LOAD from an address, that the value from the last address that was accessed is the same. Encoding a memory instruction as 4 elements of an Address, Value, Load/Store bit, and Timestamp gives us all the information in order to perform a consistency check in linear time using some permutation checking algorithm.In particular, let $P_A(x) = \Pi_{i=1}^n(x - a_i)$ and note that for arrays $A$ and $B$ of length $n$ that $A$ is a valid permutation of $B$ iff $P_A(x) \equiv P_B(x)$. So for a randomly generated $\gamma$ and two arrays $A$ and $B$, it can be shown that they are permutations with high probability iff $P_A(\gamma) \equiv P_B(\gamma)$. This can be accomplished with $n-1 \in O(n)$ multiplications.

 Now that we have a correct and sound way to arithmetize our program we need to make it cleaner in order to progress on the succinct requirement. This is accomplished with a layered circuit. There exists ways to make a "good" circuit that minimizes the depth $d$ by expanding the width with more gates.

 For instance $Y = ((X_0 + X_1) * X_2 + X_3) * X_5$ has a depth of 5, but can be lessened to 4 by using an extra constraint that the prover must add (which can continue to happen up to get logarithmic depth):

$$\begin{align*} Z = (X_0 + X_1) * X_2\\ Y = (Z + X_3) * X_4 \end{align*}$$

Now that we have minimal depth circuits, we use the sumcheck protocol to allow for quick verification of the layered circuit.

Sumcheck Protocol:

In order to check that the circuit is correct $\mathcal{V}$ checks inputs, outputs (that should match the claim provided by the prover), and the transitions between each layer. The sumcheck protocol is utilized to speed up the transition check of each layer of the circuit.

To check that an arbitrary transition $i+1 \to i$ with width $S$, input nodes $V_{p_1}, V_{p_2}$, and output nodes $W_q$ holds we have:

$$\begin{align*} \forall q &\in 0,1,\cdots,S\\ 0 &= \sum_{p_1, p_2}f(p_1, p_2, q) \text{ where,}\\ f(p_1, p_2, q) &= \text{add}_{p_1, p_2, q} \cdot (V_{p_1} + V_{p_2} - W_q) + \text{mult}_{p_1, p_2, q} \cdot (V_{p_1} * V_{p_2} - W_q) \end{align*}$$

 In order to check that $0 = \sum_{p_1, p_2}f(p_1, p_2, q)$, we can use sumcheckGoal: Verify $C = \sum_x g(x), x \in 0..N$. express $g(x)$ as polynomial $g`(b_1, \cdots, b_n)$ on bits of $x$ and instead now verify $C_0 = \sum_{b_1, \cdots, b_n \in \{0,1\}} g`(b_1, \cdots, b_n)$. This takes $n$ rounds to verify by having the prover provide claims $h_i(x) = \sum_{b_i,\cdots,b_n}g`(r_{i-1}, x, b_i, \cdots, b_n)$ for rounds $i \in 1..n$. For each claim, the verifier checks $h_i(0) + h_i(1) = C_{i-1}$, samples random $r_i$, and computes $C_i = h_i(r_i)$ quickly. Then at $i=n$, $\mathcal{V}$ finally checks $h_n(r_n) = g`(r_1, \cdots, r_n)$ to go through this in $O(n = \log (N))$ verifier time.

 Ok great! This looks like a fast and efficient way to verify that an arithmatic layered circuit is correct if we use this approach $d$ times on each layer. However, this is still not succinct as the verifier (while only having to do $d$ layers, each verified in $O(\log S)$ time) still has to evaluate each layer's input + witness where the size of the witness $\approx$ size of execution. Thus we need polynomial commitment to finally reach succinctness.

Polynomial Commitment:

 Currently, we have an approach that turns correct arithmatic layered circuits into succinct checks and polynomial evaluation. However, opening a single point on layer $d$ is just as expensive as executing the program. Thus our final step is using a polynomial commitment scheme.

 In short, our goal is to verify that $y = f(r)$ for some (prover given) polynomial $f$ s.t. for $|f| = N$, the time it takes to verify $y = f(r)$ is sublinear to $N$. So the process is have the prover commit to $f$ and send a short commitment $C$ to the verifier that is then used to compute $r$ by running GKR with prover and send it back to the prover. After this the prover computes $y = f(r)$ and produces a short proof corresponding to $f, C, r, \text{and }y$. Then the verifier can verify this with the commitment quickly and accept $y$ if it passes.

 One great PCS-adjacent method that accomplishes the same goals is a Merkle Tree. Specifically, this is called a vector commitment scheme but is very similar to a PCS. A Merkle Tree is defined as follows:

 Let $\text{hash: } \{0,1\}^{2k} \to \{0,1\}^k$ be a collision-resistant hash function for some $k$. Then our goal is that given an array $A = [a_0, ..., a_{N-1}]$ and arbitrary index $r \in 0..N-1$, retrieve $A[r] \text{ in } O(\log N)$ time. We then define for each pair of adjacent array entries as an $H$ gate s.t. $H(L, R) = \text{hash}(L||R)$. Then each hash produced by each gate is paired with the adjacent hash on its layer until there is only one hash $T$ at the top (resulting in a logarithmic depth hash tree). In order to commit, the prover sends $T$ to the verifier and the verifier gives back an arbitrary $r \in 0..N-1$ to find $a_r$.

 As for the prover, they need to help the verifier produce the path up the tree to re-derive $T$ starting from $a_r$. Thus the prover provides $O(\log N)$ entries to have the verifier hash back up the tree and derive $T$.

 Thus, while the prover has to deal with $O(N)$ hashes (the commitment cost) and $O(\log N)$ values to provide entries to the verifier given an arbitrary $r$, the verifier only has a commitment size of $O(1)$, proof size of $O(\log N)$ entries, and a final verification size of $O(\log N)$ hashes. Thus we have achieved true succinctness for our SNARK generation/verification protocol!

Summary:

 In short, the GKR protocol takes in a program $\Psi$ and produces an arithmatic layered circuit with minimal depth, verifies the circuit using the sumcheck protocol to produce a fast polynomial evaluation of the circuit, and then finally uses a polynomial (or vector) commitment scheme to avoid the verifier having to open the entire program circuit by itself, producing a small proof (the SNARK) to go along with the output of the program.

Looking to the Future:

 SNARKs are just a small tip of what cryptographic proof systems have to offer. There is lots of research to extend of concepts like SNARKs and the field is still seeing lots of work done (with cryptocurrencies, trusted computing, and other topics).

Here are some papers and projects that I have found fairly interesting regarding SNARK research:
 zk-SNARKs are a form of SNARK that also ensure a property of zero-knowledge. So a $\mathcal{P}$ can convince $\mathcal{V}$ that it has successfully executed $\Psi(x)$ without giving away any knowledge of secret inputs to the computation.
 zk-STARKs perform a similar task of a zk-SNARK but are also safe against post-quantum adversaries.
 Understanding zk-SNARKs - A paper summarizing/reviewing how SNARKs have been integrated into real world systems.
 Jolt - A cool SNARK generation framework (zkVM) that is easy to set up and start generating proofs using constraints based around assembly instructions.
 CoBBl Dynamic Constraint Generation - I worked on this project during Summer 2026 developing a Rust frontend for CoBBl! CoBBl breaks a program into basic blocks and performs optimizations on them in order to generate constraints between blocks and states of the program (which turns out to be very fast and decreases prover times across an array of benchmarks).

Acknowledgements:

 A great deal of the explanations and understanding that I have with this topic comes from a lecture from Benny for the class Introduction to Computer Security (15/18-330). Much of the examples in this post come from his slides :)