Notes

Aritmetization

The goal of the STARK protocol is verifying computations succinctly and transparently. In order to achieve that, the first step is a process called arithmetization, a reduction of the problem of verifying computation to the problem of checking that a certain polynomial, which can be evaluated efficiently on the verifier’s side (succinct), is of low degree.

• enables tools from ECC (Error Correction Codes) that efficiently test low degree-ness
• only translates Computational Integrity statements into a polynomial
• need an interactive protocol that involves a prover to convince a verifier that the polynomial is indeed of low degree
• low degree if and only if the original computation is correct (except for an infinitesimally small probability)
• last step involves transforming the interactive protocol into a single non-interactive proof that can be publicy verified

Composition steps

1. generating an execution trace and polynomial constraints
2. transforming these two objects into a single low-degree polynomial
   • prover and verifier agree on what the polynomial constraints are
   • prover generates an execution trace and tries to convince the verifier that the polynomial constraints are satisfied over this execution trace, unseen by the verifier

Supermarket Receipt Analogy

Computational Integrity (CI) statement - a claim that the output of a certain computation is correct. Let’s look into an example: total sum of a supermarket receipt

Items are listed with prices and total sum is indicated at the bottom. Suppose our CI is “the summation is correct”, to see if the statement holds, one can just compute the total sum and check if the total is the same as the number at indicated at the bottom.

Arithmetization:

1. Take some CI statement and translate it into formal algebraic language
   • define the claim succinctly in an unambiguous way
   • embeds the claim in an algebraic domain
2. Reduce the CI statement to a claim about the degree of a specific polynomial

Algebraic Representation

1. Execution Trace
   • a table that represents the steps of the underlying computation (each row is a single step)
2. Set of polynomial constraints
   • constructed such that all of them are satisfied if and only if the trace represents a valid computation

Execution Trace

• must have the special trait of being succinctly testable - each row can be verified relying only on rows that are close to it in the trace
• same verification procedure is applied to each pair of rows (affects the size of the proof)

Looking back to the example, let’s add another column for running total

Taking these two rows for example

We can be convinced that the running total 7 is correct since 7 = 3 + 4. This is what we mean by succinct constraints.

Polynomial Constraints

Cairo Whitepaper

Here’s the link to the Cairo Whitepaper.

Introduction

Existing proof systems

• require that statement will be represented in terms of polynomial equations over a finite field.https://github.com/ftupas
• process of representing a statehttps://github.com/ftupasment to prove/verify complicatedhttps://github.com/ftupashttps://github.com/ftupashttps://github.com/ftupashttps://github.com/ftupas
• requires new set of equations for each statement

CAIRO (CPU AIR)

• Turing-complete STARK-friendly CPU architecture
• describes a single set of polynomial equations for the statement that the execution of a program on this architecture is valid
• Give a statement to prove -> Cairo allows writing a program that describes a statement instead of writing a set of polynomial equations
• an AIR implementing the concept of a CPU

Background

Prover convinces the verifier that a statement is correct.

General form:

“I know an input of a certain computation that results in a certain output”

• both the computation and the output are known to both the prover and verifier
• naive approach involves information leak and repetition of computation

Cryptographic proof systems for computational integrity have the following propperties

• introducing zero-knowledge for privacy
• enabling succint verification, exponentially effecient than re-execution

Cairo is designed to

• describe the computation in the form of a computer program
• generating a proof of integrity for that computation
• ease of writing and reading programs for provable statements
• efficient proving based on STARK proof system

Design principles

Cairo enables one to prove the integrity of an arbitrary computation

• convince the verifier that a certain program ran successfully with some given output
• provide intuitive programming framework for efficient proving of valid program executions using STARK protocol
• provide a layer of abstraction around STARKs that simplifies the way the computation is described
• computation -> framed as an AIR (Algebraic Intermediate Representation)

Programming

Hello World

%lang starknet
%builtins range_check

# Alphabet substituation cipher for each letter.
# a = 01, b = 02, etc.
const hello = 10000805121215  # 08, 05, 12, 12, 15.
const world = 10002315181204  # 23, 15, 18, 12, 04.

@view
func greeting() -> (number_1 : felt, number_2 : felt):
    return (hello, world)
end

The first line, %lang starknet%, instructs the Cairo compiler to interpret this file as a StarkNet contract as opposed to a regular Cairo program.

In the next line, %builtins range_check instructs the compiler that this contract will use the range_check built-in, it ensures that the numbers stay within the acceptable range.

hello and world are constants represented by alphabet substition.

A felt is a field element which is how numbers are represented in Cairo. They behave like integers bounded by a prime number. In this function, it doesn’t take any input but returns two outputs of type felt. The view decorator indicates that the function only reads state variables and doesn’t modify them (like in Solidity).

In Cairo, functions must have return and end.`

Sources

https://medium.com/starkware/tagged/stark-math