# Defeating malicious provers in Cairo : How to have a Zero-Knowledge Proof mentality in practice

How to use the power of Cairo hints by being two developers at the same time. ;)

Hints in Cairo can be very powerful when utilized properly, and very dangerous if malicious actions are not prevented. In this post, we'll review through two examples how to defeat malicious provers by forcing them to comply to provide you what you want.

## 1. An important recap about Cairo, provers, verifiers and hints.

Cairo is a Turing-complete programming language that you first prove then verify. It is not like your traditional programming language when you run the code on your machine or a cloud server and that's it. Here, there is two people and two steps involved:

- **The prover** who runs the full .cairo code and outputs a proof a computation.

- **The verifier** who validates the proof related to the .cairo file, without running the .cairo file.

All instructions written in a Cairo program are proven with a proof of computation.

-> So what are the benefits of functioning that way ?

**The scaling properties of STARK proofs are such that the bigger the original computation gets, the bigger the computation compression ratio between the cost of the original computation and the cost of verifying the proof becomes.**

However, there's more.
Not only Cairo offers a proven Turing-complete language, but it also offers you to **play with the prover directly inside the .cairo code** if you want to prove more, manually.

**This is where the beauty of this language comes from: interacting with the prover enables you to "*zero-knowledge prove*" any kind of computation as the tool that we have with Cairo is already a proven Turing-complete language.**

The way to interact with the prover in Cairo is through **hints**. Hints are only **suggested instructions** given to the prover. In the previous .cairo 0 files, they are represented by the syntax `%{ [...] %}` where `[...]` is a set of instructions.

There is absolutely zero guarantee that the prover will follow the hints you suggested. Hints are not part of the STARK proof. However you may suggest him instructions and write the appropriate Cairo code so that if the prover is not following your hints, the Cairo program will inevitably fail.

**This means you can theoretically write every [weak client/strong server] delegation algorithm directly by replacing the weak client by the proven .cairo code and the strong server by the "hints".**

<figure>
<img
src="https://i.imgur.com/rjCeTS7.jpg"
alt="The beautiful MDN logo.">
<figcaption> The prover from the verifier's point of view: a monstrous powerful robot.</figcaption>
</figure>

We will show three progressive levels of interaction so you can understand gradually what this is all about.

### i. first level of interaction : no interaction.

This is equivalent to what we could name "writing pure Cairo code". You can use all the tools from Cairo, including all allowed operations, builtins, memory, locals, etc. All these tools combined are already proven and no additional interaction with the prover is needed.
You are able to write any piece of program you want in Cairo without any additional interaction with the prover if you want to.

func main{}() {
    let x = 10;
    let y = x + x;
    let z = y * y + x;
    return ();
}

Note that even if this may appear as a regular programming language, what is done internally is still a proof of computation.

### ii. second level of interaction : "read-only" interaction.

In this second level, only one side of the communication channel between the prover and the verifier is opened. This is particularly useful when writing what we could name "debugging hints". In this example, `ids` is an object that contains referenced variables in the memory of the Cairo program.

func read_only{}(a) {
    %{
        # Note that ids is an object containing the referenced variables in the
        # memory of the Cairo program.  

        print(f"The value of a is {ids.a}") 
    %}
    return ();
}

### iii. third level of interaction : "read and write".

Here we open a write access to the prover. This is useful for delegating computation or achieving privacy.
You must note that without any Cairo assertion on undefined_value, the prover is free to fill any value between 0 and P-1 where P is STARK prime.

// Read the a value and write a+1 to the memory. 
// This program will fail if the prover did not follow the hint.
func read_and_write{}(a) {
    alloc_locals;
    local undefined_value;
    %{
        # Read the a value:
        a=ids.a
        # Write a+1 to the undefined_value cairo variable:
        ids.undefined_value = a + 1 
    %}

    assert undefined_value = a + 1; 

    return ();
}

## 2. A common example: finding modular inverses over finite prime fields.

For simplicity of this example and only showcase the general idea, let `p` be a prime number satisfying `p < 2^124`.

The way to find the modular inverse of a number `x` modulo `p` is to find the number `y` such that `x * y = 1 (mod p)`.
This is a very important problem in cryptography and is used in many applications.
The usual way to find a modular inverse is to use the Extended Euclidean Algorithm.
However, this requires many successive euclidean divisions which are not efficient in practice.
One can use the prover to delegate this computation and find the modular inverse of a number `x` modulo `p` with only a few steps.

from starkware.cairo.common.math import unsigned_div_rem

// Finds the modular inverse of x modulo p. 
// p must be a prime number satisfying p < 2^124.
// x must be a integer satisfying 0 <= x < p.
// It that is case, this program will always fail if the prover did not follow the hint.
func inverse_mod_p{range_check_ptr}(x, p) -> (inv:felt) {
    alloc_locals;
    local asked_modular_inverse;
    %{
        x, p = ids.x, ids.p
        ids.asked_modular_inverse = pow(x,-1,p)
    %}

    // This ensures 0 <= asked_modular_inverse < 2**128:
    assert [range_check_ptr] = asked_modular_inverse;
    // This then ensures 0 <= asked_modular_inverse < p:
    assert [range_check_ptr+1] = asked_modular_inverse + 2**128 - p;

    // This computes the x*asked_modular_inverse mod p and ensures it is equal to 1: 

    let xy_unreduced = x * asked_modular_inverse;
    let (xy_div_p, xy_mod_p) = unsigned_div_rem(xy_unreduced, p);
    assert xy_mod_p = 1; 

    // Therefore, by unicity of the modular inverse if p is prime,
    // asked_modular_inverse is the modular inverse of x modulo p.

    let range_check_ptr = range_check_ptr + 2;
    return (inv=asked_modular_inverse);
}

The idea of this technique can be used on emulated prime fields of any size.
For example, this allows faster computation of elliptic curves (EC) point additions using affine coordinates. Usually, EC additions in affine coordinates are slower to perform because of divisions, but inside a zero-knowledge system such as Cairo, it turns out to be cheaper.

<figure>
<img
src="https://i.imgur.com/NtDa77j.jpg"
alt="The beautiful MDN logo.">
<figcaption> The verifier from the prover's point of view: a brave young woman wearing her Cairo Turing-complete armor. </figcaption>
</figure>

## 3. Retrieving the number of bits needed to store a field element.

In Cairo, every cell in the memory is a field element. Precisely, they're an integer between 0 and P-1., where P is the STARK prime. We can store any 251-bits number in a field element, and a subset of all the 252-bits numbers.
This is because `2^251 < P < 2^252.`

To retrieve the number of bits in Cairo, a naïve approach would be to use a recursive function that would divide the number by 2 until it reaches 0, and count the number of iterations. However, for a 250-bits number, this would require 250 iterations modular divisions, which is not efficient at all.

Another approach would be to ask the prover directly the number of bits of the field element and verify this claim with some assertions. This is what we will do in this example.

from starkware.cairo.common.cairo_builtins import BitwiseBuiltin
from src.utils import pow2

// x must contains at most 251 bits to fit into the bitwise_ptr.
func get_felt_bitlength{bitwise_ptr: BitwiseBuiltin*}(x: felt) -> felt {
    alloc_locals;
    local bit_length;
    // Asks the prover the number of bits in x : 
    %{
        x = ids.x
        ids.bit_length = x.bit_length()
    %}

    // Computes N=2^bit_length and n=2^(bit_length-1)
    // x is supposed to verify n <= x < N
    let N = pow2(bit_length);
    let n = pow2(bit_length - 1);

    // Computes bitwise x AND (N-1)
    // (N-1) in binary representation is 111...1111 with bit_length 1's.
    assert bitwise_ptr[0].x = x;
    assert bitwise_ptr[0].y = N - 1;
    tempvar word = bitwise_ptr[0].x_and_y;

    // This ensures x < N:
    assert word = x;

    // Computes bitwise x AND (n-1)
    // (n-1) in binary representation is 111...111 with (bit_length-1) 1's.
    assert bitwise_ptr[1].x = x;
    assert bitwise_ptr[1].y = n - 1;
    tempvar word = bitwise_ptr[1].x_and_y;

    // This ensures x >= n:
    assert word = x - n;

    // We have proven that 2^(bit_length-1) <= x < 2^bit_length
    // Therefore, x has bit_length bits.

    let bitwise_ptr = bitwise_ptr + 2 * BitwiseBuiltin.SIZE;
    return bit_length;
}

## 4. Conclusion : when and how to use the power of hints in Cairo

Hints are very useful when the verification cost of computing some value is cheaper than finding the value.
Some other examples can include finding solutions to some equations.

The questions you need to ask yourself are :
-What will be the properties of the inputs you're going to provide ?
-What inequality defines them ?
-What tools & builtins do you already have in Cairo ?
-What would happen if the input is 0 ? 1 ? Exceed the inequalities ? Can you find an incorrect value that would still make the verification pass ?

Note that the new hyped Cairo 1.0 language abstract these hints into core libraries functions to ease the development of efficient smart contracts.
Because hints can be dangerous, they are not enabled by default on Starknet.
However, when doing local proving, they can be very useful for debugging, be creative, and find new optimisations.

If you want to look at deeper examples, you can check out the whole [cairo-lang common repo](https://github.com/starkware-libs/cairo-lang/tree/master/src/starkware/cairo/common) and the Cairo 0 [docs](https://www.cairo-lang.org/docs/how_cairo_works/hints.html).
You can also have a look at Garaga and its [emulated field arithmetic](https://github.com/keep-starknet-strange/garaga/blob/main/src/bn254/fq.cairo#L197) for the bn254 prime field.

[Garaga](https://github.com/keep-starknet-strange/garaga/) is an open-source, very efficient, and working cryptographic pairing library written in Cairo.
It will be available on mainnet very soon to enable SNARKS circuits to be verified on Starknet!