leonardoalt

 ./INSTALL                                 
+ cargo run --bin creusot-install --
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.14s
     Running `target/debug/creusot-install`
Building prelude...
Installing Why3 and Why3find...
Package creusot-deps does not exist, create as a NEW package? [y/n] y
The following additional pinnings are required by creusot-deps.dev:
  - why3.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb
  - why3-ide.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb

leonardoalt

use std::machines::large_field::binary::Binary;
use std::machines::range::Bit2;
use std::machines::range::Bit6;
use std::machines::range::Bit7;
use std::machines::range::Byte;
use std::machines::range::Byte2;
use std::machines::binary::ByteBinary;
use std::machines::split::ByteCompare;
use std::machines::large_field::shift::ByteShift;
use std::machines::hash::poseidon_gl_memory::PoseidonGLMemory;

leonardoalt

#![no_main]
#![no_std]

extern crate powdr_riscv_runtime;

#[no_mangle]
fn main() {
    loop_test_matrix();
}

leonardoalt

use std::machines::binary::Binary;
use std::machines::range::Bit2;
use std::machines::range::Bit6;
use std::machines::range::Bit7;
use std::machines::range::Byte;
use std::machines::range::Byte2;
use std::machines::binary::ByteBinary;
use std::machines::split::ByteCompare;
use std::machines::shift::ByteShift;
use std::machines::shift::Shift;

leonardoalt

owner(owner).
tx(id, calldata, addr).
approved(owner, tx).
executed(tx).
quorum(quorum).

public(add_tx).
public(approve).
public(execute).

leonardoalt

namespace std::convert(1024);
    let int = [];
namespace std::prover(1024);
    enum Query {
        Input(int),
        PrintChar(int),
        Hint(fe),
        DataIdentifier(int, int),
    }
    let eval: expr -> fe = [];

leonardoalt

Checkout branch https://github.com/powdr-labs/powdr/tree/single-snark-halo2

Download setup of size 22 (faster than generating): https://drive.google.com/file/d/1xG_O_KqooiRR3QJno3tXIiNELSB2AQMH/view?usp=sharing

Generate witness and Poseidon transcript proof for this test (application)

cargo run -r pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2 --backend-options "poseidon" -f --params params22.bin

Create application verification key

leonardoalt

machine Brainfuck {
	reg pc[@pc];
	reg X[<=];
	reg Y[<=];
	reg Z[<=];

	// The pc of the given brainfuck program
	reg b_pc;
	// The current operator
	reg op;

leonardoalt

// SPDX-License-Identifier: MIT

pragma solidity ^0.8.0;

contract Halo2Verifier {
    uint256 internal constant    PROOF_LEN_CPTR = 0x44;
    uint256 internal constant        PROOF_CPTR = 0x64;
    uint256 internal constant NUM_INSTANCE_CPTR = 0x04c4;
    uint256 internal constant     INSTANCE_CPTR = 0x04e4;

leonardoalt

// SPDX-License-Identifier: MIT

pragma solidity ^0.8.0;

contract Halo2Verifier {
    uint256 internal constant    PROOF_LEN_CPTR = 0x44;
    uint256 internal constant        PROOF_CPTR = 0x64;
    uint256 internal constant NUM_INSTANCE_CPTR = 0x1304;
    uint256 internal constant     INSTANCE_CPTR = 0x1324;