Playground & SHARP Alpha

You’ve written your Cairo code in the Playground, and now you want to take the next step and actually get it proved. To do that you need to send your code to the Shared Prover (SHARP). We’ve described how the SHARP works before, now let’s take a look at what actually happens when you send your code from the Playground to the SHARP.

Compile

The Playground compiles and runs your code and creates a trace. This trace is sent to the off-chain Cairo SHARP to be proved.

Proof

The Cairo SHARP collects several (possibly unrelated) programs and creates a STARK proof that they ran successfully. Such a batch of programs is called a “train“. Just like a train doesn’t leave the station on-demand, a Cairo train may take a while to be dispatched to the prover. It will wait for a large enough batch of program traces to accumulate or a certain amount of time to pass – whichever happens first.

Verification and Fact Registry

Once the STARK proof was created, the SHARP sends it to be verified on-chain (on Ropsten, for now). For each program in the train, the SHARP contract writes a fact in the Fact Registry attesting to the validity of the run with its particular output. At this point the loop is closed, and your on-chain dapp can use the output of the program. (To understand how a fact is computed, see below)

Monitoring

It will take some time (say, a few minutes) – from sending to SHARP to closing the loop. To monitor the status of your job, you can click the link in the Playground output pane – it will open a new tab that will auto-refresh, showing you where in the process your job is.

Want to try it? Take the SHARP challenge from the “Challenges” menu in the Playground!

You can also find your job’s fact in the SHARP contract using the isValid() method.

Extra Credit – How is the Fact Computed?

The fact is a 32-byte value which is a function of two components:

  1. The Cairo program – We take the compiled program and compute its (Pedersen) hash.
  2. The program output – Any Cairo program can output a list of field elements. We take the keccak hash of those elements (taking each as a 32-byte value).

To compute the final value of the fact we take keccak(program_hash, output_hash).

Here’s an example of a Python code that computes the fact of a program that outputs [1, 2, 3]:

from web3 import Web3
program_hash = \ 0x4cbc2dafc7f58fc1f8235d3edfb8eaa730a25562b475c849701dbf61949ff00
program_output = [1, 2, 3]
Web3.solidityKeccak([‘uint256‘, ‘bytes32‘], [
    program_hash,
    Web3.solidityKeccak([‘uint256[]‘], [program_output])