Introducing Hints in Cairo programming language

🔗 GitHub repository and documentation of Cairo Hints.

Before we jump into the implementation of hints in Cairo, let’s take a look at the STARK proof system used at the core of Starknet. StarkWare developed the STARK protocol to allow blockchain developers to move expensive calculations off-chain, and then cost-effectively verify the results of these computations on-chain. For a more in-depth discussion on the idea, please check out the discussion as part of our post on the formal verification of ZK circuits.

Anatomy of a STARK

Modern proof systems consist of two major components: an arithmetization and a commitment scheme. The first component enables developers to define the computation that they will later prove, while the commitment scheme ensures that they don't cheat.

Arithmetization is a method of encoding complex computations in a way that can be easily proven cryptographically. STARKs use the Algebraic Intermediate Representation (AIR) – formed of an execution trace and a set of polynomial constraints.

An execution trace (or execution table) represents how the program’s state in memory evolved over time. In this table, columns represent memory (registers), and each row is the program's state after the execution of each instruction.

These rows are then connected using two kinds of constraints; these ensure that only correct states can occur.

• Boundary Constraints: These assert that a register is set to a particular value at a specific moment in time. Boundary constraints can be used, for example, to set input values or expect a specific output.
• Transition Constraints: These are equations that evaluate to 0 if and only if a transition from one row to another was performed according to the program's rules. Transition constraints ensure that the execution trace represents the desired computation.

Transition constraints have an interesting property: they can almost glimpse the future.

In a regular programming language, you start by setting some values and then derive other values based on them. Let's consider this basic multiplication for example.

fn main() {
	let a = 4;
	let b = 6;
	let c = a * b;
	assert(c == 24);
}

In a traditional program, execution happens line by line. If we remove the let b = 6 line, the compiler will fail, indicating that it cannot proceed to calculate c because b is missing.

However, in AIR, boundary constraints enforce a = 4, c = 24. We also know that c = a * b, which implies that b must be equal 6. We can consider the entire program at once and "fill in the blanks" as long as all our variables are fully constrained: each variable can assume exactly one value.

The ability to infer variables from the surrounding context allows us to express calculations using fewer or cheaper constraints (for example, it’s cheaper to ensure that x * x = y than sqrt(y) = x). However, when we overlook some constraints (in other words, if our AIR becomes under-constrained), we expose the verifier to unexpected incorrect inputs.

This is a problem and a big source of security vulnerabilities in production use of ZK circuits. Just see this ZK Bug Tracker. One way to prevent such catastrophic issues is to formally verify that the chosen set of constraints accepts only the expected solutions.

Compiling trace tables and constraints can be a cumbersome task. Thanks to Cairo, a programming language inspired by Rust and developed by StarkWare, developers can write their programs using a familiar syntax instead. In fact, the previous multiplication example was already valid Cairo code that automatically generates the correct AIR representation.

Cairo Hints

In the previous section, we briefly mentioned that some constraints are cheaper to implement than the others. Because multiplication is a natively supported operation inside AIR, checking if a result of sqrt is correct is less computationally intensive than finding the sqrt in the first place.

With Cairo Hints, you can specify a "square root oracle" using Protocol Buffers. This will generate the code necessary to obtain square root values in Cairo without calculating them in circuit.

// Oracle definition using Protocol Buffers 3

message Request {
    uint64 n = 1;
}

message Response {
    uint64 n = 1;
}

service SqrtOracle {
    rpc Sqrt(Request) returns (Response);
}

// Using the oracle in Cairo code

let result = SqrtOracle::sqrt(Request { n: input });

// Constraining the result of SqrtOracle in Cairo

result.n * result.n == input

Another use case is binary decomposition. Finding a binary representation of a number is more difficult than checking if a given decomposition (x0, x1, …xn) is a correct binary representation of N:

The solution for an effective proof system is to perform expensive operations outside of the AIR, and only verify correctness of their outputs within the circuit. In other words, we want to move expensive operations outside of Cairo (that compiles to AIR for us), and only perform a cheap verification in our Cairo program. We will do so by a mechanism called “an oracle”, or “hints”; at various points of execution, the Cairo program can ask an external helper for a value that will be calculated outside of the proof system.

In the previous generation of Cairo, sometimes known as Cairo0 or CairoZero, developers had the ability to include inline hints in a Python language. The results of the Python program would be inserted into the Cairo program as local variables.

Reilabs' implementation of Cairo Hints builds upon this concept for the current generation of Cairo (version 2.5.3 at the time of writing). Instead of limiting developers to inline Python code, they can specify a JSON-RPC server that will provide additional inputs to their Cairo program.

To continue with the sqrt example, we can create a service that exposes an HTTP POST /sqrt endpoint, accepts JSON like {"input": 25}, and returns {"result": 5}. To accomplish this, we can utilize any programming language capable of running an HTTP server, parsing JSON objects, and returning the desired responses. The Cairo Hints repository offers example implementations in Rust and JavaScript.

⚠️ It is important to emphasize that hints cannot be used to simply replace parts of Cairo with libraries written in other languages. Developers must be extremely careful to correctly constrain any results coming from a hints server lest they have an under-constrained program.

Since these servers can execute arbitrary code, they can only be used within the context of local proving and cannot be deployed to Starknet. From the perspective of the blockchain, there are no concerns regarding centralization or availability of hints. It is a responsibility of app developers to deploy the hints server as part of their Cairo proving infrastructure.

Looking to the Future: Private Inputs

In the future, hints could be used as private inputs to Cairo programs. They would allow developers to prove that they know a value (referred to as a witness) without revealing the value itself. For example, they could prove that they know a value that hashes to a certain digest.

fn poseidon(input: Span<Felt252>) -> Felt252 {
	// poseidon hash implementation
}

fn main() {
	let digest = 3115281239805795994436322590308493735630519107973543550375762423685232930936;
	// SecretOracle will insert [10, 20, 30, 40] array as a secret input to the poseidon function
  assert(poseidon(SecretOracle::hash_preimage()) == digest);
}

In the example above, a developer implements a Poseidon hash in the same way they would in a language like Rust. Cairo ensures that the inputs and output of the Poseidon function are correctly constrained. There is no need to expose the secret value (in this example, an array of [10, 20, 30, 40]) in the source code.

⚠️ Secret inputs are a prerequisite for zero-knowledge proving systems. However, it is important to note that this alone is not sufficient to implement an actual zero-knowledge process. In zk-STARKs, the prover must also ensure that no data is leaked in the generated proof. Currently, none of the generally available provers (such as StarkWare's SHARP and Stone, or Lambdaclass' lambdaworks) guarantee that data is not leaked in their proofs.

Getting Started with Cairo Hints

For those interested in adding hints to their Cairo projects, please visit our GitHub repository to learn how to set up a project and use hints in practice. If you want to learn more about Cairo, we highly recommend The Cairo Book.

Finally, if you want to work with us, please reach out to hi@reilabs.io

Hope you have enjoyed this post. If you'd like to stay up to date and receive emails when new content is published, subscribe here!