Provide hints for implementing a backend for a minimized version of Solidity

[sshine]

I'm trying to understand what it means to compile a smart contract language to/through Cairo and still have it execute.

To get the ball rolling, here is a minimized variant of Solidity:

contract Puzzle {
    function puzzle(int a, int b, ERC20 coin) public {
        if (a^2 + b^2 == 458) {
            coin.transfer(caller, 1);
        }
    }
}

If I were to just compile this into EVM, I'd eventually have a CALL opcode that is triggered by some logic.

Questions:

1. What could this example be extended with to provide a useful off-chain proving-of-something?
2. If we don't target EVM, how do we eventually achieve something comparable to an on-chain CALL?

Is it only a portion of the code that gets compiled to Cairo? Or is EVM eventually produced by Cairo?

[sshine]

I'll extend the example to coincide with the example given on Discord of a trustless on-chain lookup into an off-chain database, since that appears to be one minimal example (in the sense of understanding, rather than implementation). Perhaps then another minimal example (in the sense of implementation) could also be made.

@MichaelRiabzev-StarkWare wrote on Discord:

For example, assume you want to connect your dApp to a big key-value database (billions of records), and allow the contract to "query" the database trustelssly. The simplest solution would be to store the entire database in you dApps contract storage. But this would be very expensive.

An alternative is to store on your dApp contract only the hash of your database, and keep the database offchain. Whenever there is a need to pass (trustlesly) a record from the offchain database to the smart-contract you prove to it instead that you used a Cairo program which queried a database having the same hash kept onchain, and the value of the required key there is value.

You can think about the on-chain verifier (in this case) as something containing a function verify(proof, db_hash, key, value), and if the proof does not satisfy the statement "I know a db which has hash digest db_hash, and it has value at key", it reverts.

Actually, because the verifier is universal, looks something as follows: verify(proof, cairo_program_hash, outpub_blob) and it reverts if the proof does not prove the statement "I know a cairo program with hash digest cairo_program_hash and some private input to this program making it output output_blob".

For the case above you can think output_blob encodes (db_hash, key, value). This encoding is defined by the cairo_program.

There are two definitions for verify() here. I don't know which is preferred in terms of modelling, but I suppose that the second is a generalisation of the first, so that the particular parameters of the first coincide with being arbitrary program inputs/outputs.

I assume that proof is a piece of EVM bytecode? Otherwise, I'm not sure how to encode "I know a Cairo program ...". The following is pseudo-Solidity; proof could have been executed on-chain in advance of making the contract call, rather than get passed as an argument... either way, those exact semantics don't seem important.

contract Contract {
    function verify(bytecode proof, uint256 db_hash, uint256 key, uint256 value) public {
        if (proof(db_hash, key, value)) {
            ...;
        } else {
            REVERT;
        }
    }
}

Given my interpretation, it seems to me that a "Solidity -> Cairo" back-end would actually need to generate EVM code at some point for this on-chain verifier. Isn't there a "... -> Solidity/EVM" component here at which the "I know a Cairo program ..." proof must compile with in order to make the verify(...) call?

I think a high-level description of the pipeline would help me here.

[MichaelRiabzev-StarkWare]

The proof is not an EVM bytecode at all, it is a STARK proof (academic paper:https://eprint.iacr.org/2018/046.pdf , lighter medium posts describing it: https://medium.com/starkware/tagged/stark-math).

At a high level, a STARK proof attests to the knowledge of a valid execution trace, given some boundary constraints. For the case of Cairo we prove there is knowledge of a valid Cairo (architecture) trace, and the boundary constraints are:

• The program counter register (pc) points to an address in the memory, where is written a known (public) program. The program can take as many memory entries as it needs, it is all part of the boundary constraints.
• The values returned by the program are written to a predefined memory area, and their values should be equal to some expected values.

Now, we will see how does the proof looks like (simplified).
Imagine you want to check if an x86 trace (a table showing the changes of the CPU registers at each cycle) is valid or not. Notice verification of a trace can be thought of as (almost) a local problem. I can choose a random row in the trace, read it and the instruction executed on it (e.g. move eax, ebx). This provides some restrictions on the next line (e.g. ecx should stay the same, and now eax should equal ebx). Randomly checking the consistency of pairs of such trace line pairs is not sound enough. Even if we add to it checking explicitly the boundary constraints. But his is good enough intuition to how the proof looks likes - some random sampling of trace line pairs. The verification, at a high level, would be to verify the consistency of such trace lines (and the boundary constraints). This is merely for intuition, to actually understand how a STARK proof really looks like I encourage you to go over the links above.

This explanation mostly focus on what a STARK proof is, and not as much on the higher flow, but I hope it does shed some light, does it help?

[sshine]

I think a high-level description of the pipeline would help me here.

I hope it does shed some light, does it help?

Not really. What does a someCoin.transfer(caller, 1) become in Cairo?

[MichaelRiabzev-StarkWare]

The shortest answer: we just published a related blog post: https://www.cairo-lang.org/cairo-for-blockchain-developers

The short answer:
It does not change. It does not move to Cairo, it stays in solidity.

The long answer:
Let's generalize this code, to something like this:

contract Puzzle {
    function puzzle(solution, ERC20 coin) public {
        if (is_valid_solution(solution)) {
            coin.transfer(caller, 1);
        }
    }
}

When the verification of a solution is a short computation, as described before (a^2 + b^2 == 458), there is actually no need to use Cairo at all.
Now let's assume the verification of a solution is actually a very long computation. For example, the solution is a 64 bit integer n. It is valid if it is a prime. The naive way to verify the number is a prime is to make sure it does not divide any number in the range 2 - sqrt(n). While the is_valid_solution(n) function can be easily implemented with a simple loop, it would probably require too much gas, and we practically won't be able to execute it.

On the other hand, we can implement the same logic in Cairo as well. We can use it to generate a proof, and verify the proof instead (simplified for the sake of clarity, more details in the blogpost). This would make us to change the contract to be something like this:

contract Puzzle {
    function puzzle(solution, proof, ERC20 coin) public {
        if (is_valid_solution(solution, proof)) {
            coin.transfer(caller, 1);
        }
    }
}

Where is_valid_solution(solution, proof) verifies the STARK proof instead of naively executing the long computation over solution. The gas consumptions of the proof verification scale poly-logarithmically with the original execution time, and actually consumes constant gas for any practical use case.

This, of course, does not allow one to send funds directly on Ethereum, so how does StarkWare scalable exchange (L2) solution look like? It is very similar to common banks - the Cairo never changes actual asset ownership, only balance records (just like bank transfers don't make the bank employees move around cases full of dollars from one account to another).
In StarkEx all the funds are kept on the StarkEx smart contract (think of it as the federal reserve), and the balance state is represented on-chain solely by its hash (merkle root).
When there are operations only between StarkEx accounts, we only update the hash of the balances:

contract MyExchange {
    function update_state(new_state_hash, proof) public {
        if (is_valid_state_update(current_state_hash, new_state_hash, proof)) {
            current_state_hash = new_state_hash;
        }
    }
}

The Cairo program enforces the exchange rules (no creation of money out of thin air, no taking of money belonging to others with no permission, etc), and the proof attests that the new state_root is a valid new state - reached by applying only allowed operation on the previous state.

Does this help?