-
Notifications
You must be signed in to change notification settings - Fork 23
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into feat/public-input-verify
- Loading branch information
Showing
18 changed files
with
436 additions
and
16 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,25 @@ | ||
target | ||
.snfoundry_cache/ | ||
|
||
# Generated by Cargo | ||
# will have compiled files and executables | ||
**/debug/ | ||
**/target/ | ||
|
||
# Remove Cargo.lock from gitignore if creating an executable, leave it for libraries | ||
# More information here https://doc.rust-lang.org/cargo/guide/cargo-toml-vs-cargo-lock.html | ||
**/Cargo.lock | ||
|
||
# These are backup files generated by rustfmt | ||
**/*.rs.bk | ||
|
||
# MSVC Windows builds of rustc generate these, which store debugging information | ||
*.pdb | ||
|
||
# Scarb | ||
**/Scarb.lock | ||
|
||
# vscode | ||
**/.vscode/ | ||
|
||
# Resources | ||
runner/resources/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
scarb 2.4.0 | ||
scarb 2.4.1 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,21 +1,35 @@ | ||
# Cairo1 verifier | ||
# Cairo Verifier | ||
|
||
## Build | ||
``` sh | ||
scarb build | ||
This document provides steps to build and run the Cairo Verifier. | ||
|
||
## Building the Verifier | ||
|
||
To build the latest version of the verifier and create a Sierra file, follow these steps: | ||
|
||
1. Navigate to the project root directory: | ||
|
||
```bash | ||
cd . | ||
``` | ||
|
||
## Test | ||
``` sh | ||
scarb test | ||
2. Build the project: | ||
|
||
```bash | ||
scarb build | ||
``` | ||
|
||
## Format | ||
``` sh | ||
scarb fmt | ||
## Running the Verifier | ||
|
||
After building the verifier, you can run it with the following steps: | ||
|
||
1. Navigate to the runner directory: | ||
|
||
```bash | ||
cd runner | ||
``` | ||
|
||
## Clean | ||
``` sh | ||
scarb clean | ||
2. Run the verifier: | ||
|
||
```bash | ||
cargo run --release -- ../target/dev/cairo_verifier.sierra < resources/parserin.txt | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,3 @@ | ||
[package] | ||
name = "cairo_verifier" | ||
version = "0.1.0" | ||
version = "0.1.0" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
#!/usr/bin/env bash | ||
|
||
scarb build | ||
cd runner | ||
cargo run --release -- ../target/dev/cairo_verifier.sierra.json < resources/parserin.txt |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
[package] | ||
name = "runner" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
|
||
[dependencies] | ||
anyhow = "1.0.76" | ||
cairo-args-runner = "1.0.0" | ||
clap = { version = "4.4.11", features = ["derive"] } | ||
lalrpop-util = { version = "0.20.0", features = ["lexer", "unicode"] } | ||
serde = { version = "1.0.193", features = ["derive"] } | ||
serde_json = "1.0.108" | ||
|
||
[build-dependencies] | ||
lalrpop = "0.20.0" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,48 @@ | ||
# Cairo1 Verifier | ||
|
||
## Overview | ||
|
||
The Cairo1 Verifier is a tool designed for parsing and utilizing proofs in the Cairo language. This document provides instructions on how to get and use the parsed proof. | ||
|
||
## Getting the Parsed Proof | ||
|
||
To obtain the parsed proof, follow these steps: | ||
|
||
### 1. Download Source Code | ||
|
||
- Access the source code at [Cairo1 Parser Repository](https://github.com/neotheprogramist/cairo-lang/tree/parser). | ||
|
||
### 2. Install Dependencies | ||
|
||
- Execute the command: `pipenv install`. | ||
|
||
### 3. Activate Virtual Environment | ||
|
||
- Activate the virtual environment with: `pipenv shell`. | ||
|
||
### 4. Run the Parser | ||
|
||
- Use the parser by running: | ||
``` | ||
python src/main.py -l starknet_with_keccak < src/starkware/cairo/stark_verifier/air/example_proof.json > parseout.txt | ||
``` | ||
|
||
### 5. Access Output File | ||
|
||
- The output will be available in the `parseout.txt` file. | ||
|
||
## Using the Parsed Proof | ||
|
||
Once you have the parsed proof, you can use it as follows: | ||
|
||
### 1. Copy Proof to Input File | ||
|
||
- Copy the entire content or a consistent section of `parseout.txt` to `runner/resources/parsein.txt`. | ||
|
||
### 2. Adjust Input Structures | ||
|
||
- Modify the structures in `src/input_structs` to match the copied content. | ||
|
||
### 3. Execute the Runner Script | ||
|
||
- Run the script using: `./run.sh`. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
fn main() { | ||
lalrpop::process_root().unwrap(); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,66 @@ | ||
use std::{ | ||
fmt::Display, | ||
ops::{Deref, DerefMut}, | ||
}; | ||
|
||
#[derive(Debug, Clone)] | ||
pub enum Expr { | ||
Value(String), | ||
Array(Vec<Expr>), | ||
} | ||
|
||
impl Display for Expr { | ||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { | ||
match self { | ||
Expr::Value(v) => write!(f, "\"{v}\""), | ||
Expr::Array(v) => { | ||
write!(f, "[")?; | ||
|
||
for (i, expr) in v.iter().enumerate() { | ||
if i != 0 { | ||
write!(f, ", ")?; | ||
} | ||
write!(f, "{expr}")?; | ||
} | ||
|
||
write!(f, "]")?; | ||
|
||
Ok(()) | ||
} | ||
} | ||
} | ||
} | ||
|
||
#[derive(Debug, Clone)] | ||
pub struct Exprs(pub Vec<Expr>); | ||
|
||
impl Display for Exprs { | ||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { | ||
write!(f, "[")?; | ||
|
||
for (i, expr) in self.iter().enumerate() { | ||
if i != 0 { | ||
write!(f, ", ")?; | ||
} | ||
write!(f, "{expr}")?; | ||
} | ||
|
||
write!(f, "]")?; | ||
|
||
Ok(()) | ||
} | ||
} | ||
|
||
impl Deref for Exprs { | ||
type Target = Vec<Expr>; | ||
|
||
fn deref(&self) -> &Self::Target { | ||
&self.0 | ||
} | ||
} | ||
|
||
impl DerefMut for Exprs { | ||
fn deref_mut(&mut self) -> &mut Self::Target { | ||
&mut self.0 | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
use std::io::{stdin, Read}; | ||
|
||
use cairo_args_runner::{run, Arg, VecFelt252}; | ||
use clap::Parser; | ||
use lalrpop_util::lalrpop_mod; | ||
|
||
mod ast; | ||
|
||
lalrpop_mod!(pub parser); | ||
|
||
#[derive(Parser)] | ||
#[command(author, version, about, long_about = None)] | ||
struct Cli { | ||
/// Path to compiled sierra file | ||
target: String, | ||
} | ||
|
||
fn main() -> anyhow::Result<()> { | ||
let cli = Cli::parse(); | ||
let mut input = String::new(); | ||
stdin().read_to_string(&mut input)?; | ||
|
||
let parsed = parser::CairoParserOutputParser::new() | ||
.parse(&input) | ||
.map_err(|e| anyhow::anyhow!("{}", e))?; | ||
let result = parsed.to_string(); | ||
|
||
let target = cli.target; | ||
let function = "main"; | ||
let args: VecFelt252 = serde_json::from_str(&result).unwrap(); | ||
|
||
let result = run(&target, function, &[Arg::Array(args.to_vec())])?; | ||
|
||
println!("{result:?}"); | ||
Ok(()) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
use crate::ast::{Expr, Exprs}; | ||
|
||
grammar; | ||
|
||
pub CairoParserOutput: Exprs = { | ||
StructName "()" => Exprs(Vec::new()), | ||
StructName "(" <n:Comma<Arg>> ")" => Exprs(n.iter().flat_map(|x| x.iter().cloned()).collect()), | ||
}; | ||
|
||
CairoParserOutputInner: Exprs = { | ||
<n:Num> => Exprs(vec![Expr::Value(n)]), | ||
"[" <n:Comma<CairoParserOutputInner>> "]" => Exprs(vec![Expr::Array(n.iter().flat_map(|x| x.iter().cloned()).collect())]), | ||
StructName "()" => Exprs(Vec::new()), | ||
"FriWitness" "(" "layers=" "[" <n:Comma<FriWitnessLayers>> "]" ")" => Exprs(vec![Expr::Array(n.iter().flat_map(|x| x.iter().cloned()).collect())]), | ||
StructName "(" <n:Comma<Arg>> ")" => Exprs(n.iter().flat_map(|x| x.iter().cloned()).collect()), | ||
}; | ||
|
||
Arg: Exprs = { | ||
ArgName "=" <n:CairoParserOutputInner> => n, | ||
}; | ||
|
||
FriWitnessLayers: Exprs = { | ||
<n:Num> "," "[" <a:Comma<Num>> "]" => Exprs(vec![Expr::Value(n)].into_iter().chain(a.into_iter().map(Expr::Value)).collect()), | ||
StructName "(" ArgName "=" StructName "(" <n:FriWitnessLayersArgs> ")" ")" => n, | ||
}; | ||
|
||
FriWitnessLayersArgs: Exprs = { | ||
ArgName "=" <n:Num> "," ArgName "=" "[" <a:Comma<Num>> "]" => Exprs(vec![Expr::Value(n)].into_iter().chain(a.into_iter().map(Expr::Value)).collect()), | ||
}; | ||
|
||
Comma<T>: Vec<T> = { | ||
<mut v:(<T> ",")*> <e:T?> => match e { | ||
None => v, | ||
Some(e) => { | ||
v.push(e); | ||
v | ||
} | ||
} | ||
}; | ||
|
||
StructName: String = <s:r"[A-Z][A-Za-z]+"> => s.to_string(); | ||
ArgName: String = <s:r"[a-z_]+"> => s.to_string(); | ||
Num: String = <s:r"[0-9]+"> => s.to_string(); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
mod public_input; | ||
mod stark_config; | ||
mod stark_proof; | ||
mod stark_unsent_commitment; | ||
mod stark_witness; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
#[derive(Drop, Serde)] | ||
struct PublicInput { | ||
log_n_steps: felt252, | ||
range_check_min: felt252, | ||
range_check_max: felt252, | ||
layout: felt252, | ||
dynamic_params: Array<felt252>, | ||
n_segments: felt252, | ||
segments: Array<felt252>, | ||
padding_addr: felt252, | ||
padding_value: felt252, | ||
main_page_len: felt252, | ||
main_page: Array<felt252>, | ||
n_continuous_pages: felt252, | ||
continuous_page_headers: Array<felt252>, | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
#[derive(Drop, Serde)] | ||
struct StarkConfig { | ||
traces: TracesConfig, | ||
composition: TableCommitmentConfig, | ||
fri: FriConfig, | ||
proof_of_work: ProofOfWorkConfig, | ||
// Log2 of the trace domain size. | ||
log_trace_domain_size: felt252, | ||
// Number of queries to the last component, FRI. | ||
n_queries: felt252, | ||
// Log2 of the number of cosets composing the evaluation domain, where the coset size is the | ||
// trace length. | ||
log_n_cosets: felt252, | ||
// Number of layers that use a verifier friendly hash in each commitment. | ||
n_verifier_friendly_commitment_layers: felt252, | ||
} | ||
|
||
#[derive(Drop, Serde)] | ||
struct TracesConfig { | ||
original: TableCommitmentConfig, | ||
interaction: TableCommitmentConfig, | ||
} | ||
|
||
#[derive(Drop, Serde)] | ||
struct TableCommitmentConfig { | ||
columns: felt252, | ||
vector: VectorCommitmentConfig | ||
} | ||
|
||
#[derive(Drop, Serde)] | ||
struct VectorCommitmentConfig { | ||
height: felt252, | ||
verifier_friendly_commitment_layers: felt252, | ||
} | ||
|
||
#[derive(Drop, Serde)] | ||
struct FriConfig { | ||
// Log2 of the size of the input layer to FRI. | ||
log_input_size: felt252, | ||
// Number of layers in the FRI. Inner + last layer. | ||
n_layers: felt252, | ||
// Array of size n_layers - 1, each entry is a configuration of a table commitment for the | ||
// corresponding inner layer. | ||
inner_layers: Array<felt252>, | ||
// Array of size n_layers, each entry represents the FRI step size, | ||
// i.e. the number of FRI-foldings between layer i and i+1. | ||
fri_step_sizes: Array<felt252>, | ||
log_last_layer_degree_bound: felt252, | ||
} | ||
|
||
#[derive(Drop, Serde)] | ||
struct ProofOfWorkConfig { | ||
// Proof of work difficulty (number of bits required to be 0). | ||
n_bits: felt252, | ||
} |
Oops, something went wrong.