thread 'main' panicked at 'mismatch at xxx

[nschoe]

(Sorry for the empty first post, keyboard shortcut messed up).

So I wrote a simple Cairo program which uses keccak_felts() to compute the keccak hashes of several field elements, like so :

%builtins range_check bitwise

from starkware.cairo.common.alloc import alloc
from starkware.cairo.common.cairo_keccak.keccak import keccak_felts, finalize_keccak
from starkware.cairo.common.cairo_builtins import BitwiseBuiltin
from starkware.cairo.common.uint256 import Uint256

func main{range_check_ptr, bitwise_ptr: BitwiseBuiltin*}() {
    alloc_locals;

    let (local keccak_ptr: felt*) = alloc();
    local keccak_ptr_start: felt* = keccak_ptr;

    let (local elements: felt*) = alloc();
    const n_elems = 20;
    populate_elements(elements, n_elems);

    let (local k_hash: Uint256) = keccak_felts{keccak_ptr=keccak_ptr}(n_elems, elements);

    finalize_keccak(keccak_ptr_start=keccak_ptr_start, keccak_ptr_end=keccak_ptr);

    %{ print(f'Keccak hash of {ids.n_elems} elements: {(ids.k_hash.high << 128) + ids.k_hash.low}') %}

    return ();
}

func populate_elements(elements: felt*, n_elems) {
    if (n_elems == 0) {
        return ();
    } else {
        assert elements[0] = n_elems;
        populate_elements(elements = elements + 1, n_elems = n_elems - 1);
        return();
    }
}

I then compile it with: cairo-compile test_keccak.cairo --output test_keccak_compiled.json --proof_mode and then I run it with cairo-run --program test_keccak_compiled.json --trace_file trace.bin --memory_file memory.bin --min_steps 2097152 --layout all --proof_mode --print_info.

So far it seems to work, I have some Cairo output (which I can include if needed).

But then when I try to generate a proof with sandstorm like this: RUST_BACKTRACE=full cargo +nightly run -r -F gpu,parallel,asm prove --program ../cairo/keccak/test_keccak_compiled.json --trace ../cairo/keccak/trace.bin --memory ../cairo/keccak/memory.bin --output ../cairo/keccak/test_keccak.proof it fails with a thread 'main' panicked, here is the full error:

Finished release [optimized] target(s) in 2.93s
     Running `target/release/sandstorm prove --program ../cairo/keccak/test_keccak_compiled.json --trace ../cairo/keccak/trace.bin --memory ../cairo/keccak/memory.bin --output ../cairo/keccak/test_keccak.proof`
thread 'main' panicked at 'mismatch at 16765402: a=12876, v=1085295, a_next=799309, v_next=2', src/trace.rs:575:13
stack backtrace:
   0:        0x104b71c50 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h1dd21340baccd671
   1:        0x104b1b230 - core::fmt::write::hdc5ef827149a5964
   2:        0x104b56964 - std::io::Write::write_fmt::h19ff2c3a0eb6ef79
   3:        0x104b75228 - std::sys_common::backtrace::print::he20d0412b5e489f4
   4:        0x104b74e68 - std::panicking::default_hook::{{closure}}::h34b82746f4ef2655
   5:        0x104b75d04 - std::panicking::rust_panic_with_hook::hfc548818867f7dbe
   6:        0x104b75860 - std::panicking::begin_panic_handler::{{closure}}::hbb06ce42fd65d290
   7:        0x104b757d0 - std::sys_common::backtrace::__rust_end_short_backtrace::h197c1b62d876b3ea
   8:        0x104b757ac - _rust_begin_unwind
   9:        0x104bc29dc - core::panicking::panic_fmt::h28f7baa535dc0172
  10:        0x104ae8ac0 - sandstorm::prove::h463d8e2e14dc8278
  11:        0x104ae0d88 - sandstorm::main::h79d562ee702a6443
  12:        0x104a9bfcc - std::sys_common::backtrace::__rust_begin_short_backtrace::hcc0d69e2d4780d3f
  13:        0x104ae96b4 - _main

I have successfully generated (and verified) proofs of simple Cairo programs with sandstorm and it worked well.

Am I doing something wrong? What's a 'thread main panicked'?

Thanks

[andrewmilson]

Thanks @nschoe. I'm not so familiar with Cairo code but does the program make use of any builtins during execution? If so I suspect this is the issue as Sandstorm doesn't support builtins yet. The good news is that support for the range check builtin will come in the next couple of months I hope. If it's not to do with builtins I'll investigate when I'm back from holiday (in a couple of weeks).

"thread main panicked" is just a generic program termination message in Rust. In this instance it comes from an assertion that fails. Sandstorm's error messages could be a lot more informative.

[nschoe]

Thanks for your answer @andrewmilson . Yes the program uses some Cairo's builtins indeed. I did read on the readme that builtins weren't supported, but I did try a simple program computing a "hash chain" (that is hash( ... hash(hash(x0, x1), x2) ... , xn)).

The program is shown here:

%builtins pedersen

from starkware.cairo.common.cairo_builtins import HashBuiltin
from starkware.cairo.common.hash import hash2
from starkware.cairo.common.alloc import alloc

func main{pedersen_ptr: HashBuiltin*}() {
    alloc_locals;

    const n_hashes = 100;
    local initial_x = 33;
    local initial_y = 42;
    let (local initial_hash) = hash2{hash_ptr=pedersen_ptr}(initial_x, initial_y);

    let final_hash = recurse_hash{hash_ptr=pedersen_ptr}(initial_hash, n_hashes);

    %{ print(f'Final hash (after {ids.n_hashes} hashes): {ids.final_hash}') %}

    return ();
}

func recurse_hash{hash_ptr: HashBuiltin*}(last_hash, n) -> felt {
    if (n == 0) {
        return last_hash;
    } else {
        let (new_hash) = hash2(last_hash, n);
        let next = recurse_hash(last_hash = new_hash, n = n-1);
        return next;
    }
}

And using the same exact steps as mentioned in my post (namely, the cairo-compile with --prood_mode, cairo-run with -proof_mode, and then sandstorm prove) I could generate a proof (and got a .proof file).

I then used sandstorm verify to verify it and it worked.

And this program uses the pedersen hash builtin, yet sandstorm is able to generate a proof; how come?

This preliminary success is what caused my ignoring the mention of sandstorm not supporting builtins.

Thanks for your time.

[andrewmilson]

Hey @nschoe. Thanks for your patience, I have a better grasp of the builtins now.

And this program uses the pedersen hash builtin, yet sandstorm is able to generate a proof; how come?

I'm not exactly sure but I suspect because in the Pedersen program every Pedersen ouput is referenced so the memory constraints are able to be satisfied. Perhaps in the erroring example some of the bitwise outputs don't get referenced, therefore there are holes in the memory and then the memory constraints are not able to be satisfied so it fails.

Errors aside, for security reasons the Cairo program has to be proved with a layout that supports the builtins that you're using. Even if it technically works It's not safe to prove a program that uses Pedersen builtin with a layout that doesn't support Pedersen builtin. This is because the verifier doesn't check any conditions on the Pedersen outputs to make sure they're correct. The prover could set the Pedersen outputs to whatever they wanted and the verifier would be completely fine with it. Sandstorm now support Pedersen builtin but Keccak builtin isn't supported yet. The currently supported layouts are:

• recursive which supports pedersen, range_check, bitwise and output builtins
• starknet which supports pedersen, ec_op, ecdsa, range_check, bitwise, output and poseidon builtins