Skip to content

Commit

Permalink
feat: generic constraint evaluation
Browse files Browse the repository at this point in the history
  • Loading branch information
@Fumuran
Fumuran committed Jan 6, 2023
1 parent 9ffc6ca commit 02dba70
Show file tree
Hide file tree
Showing 30 changed files with 1,640 additions and 48 deletions.
3 changes: 2 additions & 1 deletion Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,6 @@ members = [
"air-script",
"parser",
"ir",
"codegen/winterfell"
"codegen/winterfell",
"codegen/gce"
]
1 change: 1 addition & 0 deletions air-script/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ path = "src/main.rs"

[dependencies]
codegen-winter = { package = "air-codegen-winter", path = "../codegen/winterfell", version = "0.1.0" }
codegen-gce = { package = "air-codegen-gce", path = "../codegen/gce", version = "0.1.0" }
env_logger = "0.9"
ir = { package = "air-ir", path = "../ir", version = "0.1.0" }
log = { version = "0.4", default-features = false }
Expand Down
4 changes: 2 additions & 2 deletions air-script/src/cli/transpile.rs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use std::{fs, path::PathBuf};
use structopt::StructOpt;

use codegen_winter::CodeGenerator;
use codegen_winter::WinterfellCodeGenerator;
use ir::AirIR;
use parser::parse;

Expand Down Expand Up @@ -64,7 +64,7 @@ impl TranspileCmd {
let ir = ir.unwrap();

// generate Rust code targeting Winterfell
let codegen = CodeGenerator::new(&ir);
let codegen = WinterfellCodeGenerator::new(&ir);

// write transpiled output to the output path
let result = fs::write(output_path.clone(), codegen.generate());
Expand Down
2 changes: 1 addition & 1 deletion air-script/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,4 @@ pub use parser::parse;
pub use ir::AirIR;

/// Code generation targeting Rust for the Winterfell prover
pub use codegen_winter::CodeGenerator;
pub use codegen_winter::WinterfellCodeGenerator;
28 changes: 28 additions & 0 deletions air-script/tests/aux_trace/aux_trace.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
{
"num_polys": 7,
"num_variables": 18,
"constants": [1, 1, 1, 1, 1],
"expressions": [
{"op": "ADD", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "POL", "index": 2}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 0}, "rhs": {"type": "EXPR", "index": 0}},
{"op": "ADD", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "POL_NEXT", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 1}, "rhs": {"type": "EXPR", "index": 2}},
{"op": "ADD", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "EXPR", "index": 4}},
{"op": "ADD", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "VAR", "index": 16}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 6}, "rhs": {"type": "POL", "index": 1}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 7}, "rhs": {"type": "VAR", "index": 17}},
{"op": "MUL", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "EXPR", "index": 8}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 3}, "rhs": {"type": "EXPR", "index": 9}},
{"op": "ADD", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "VAR", "index": 16}},
{"op": "MUL", "lhs": {"type": "POL_NEXT", "index": 4}, "rhs": {"type": "EXPR", "index": 11}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 12}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "VAR", "index": 16}},
{"op": "SUB", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "CONST", "index": 0}}
],
"outputs": [1, 3, 5, 10, 13, 14, 15, 16, 17, 18, 19]
}
28 changes: 28 additions & 0 deletions air-script/tests/aux_trace/generated_aux_trace.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
{
"num_polys": 7,
"num_variables": 18,
"constants": [1, 1, 1, 1, 1],
"expressions": [
{"op": "ADD", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "POL", "index": 2}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 0}, "rhs": {"type": "EXPR", "index": 0}},
{"op": "ADD", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "POL_NEXT", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 1}, "rhs": {"type": "EXPR", "index": 2}},
{"op": "ADD", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "EXPR", "index": 4}},
{"op": "ADD", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "VAR", "index": 16}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 6}, "rhs": {"type": "POL", "index": 1}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 7}, "rhs": {"type": "VAR", "index": 17}},
{"op": "MUL", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "EXPR", "index": 8}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 3}, "rhs": {"type": "EXPR", "index": 9}},
{"op": "ADD", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "VAR", "index": 16}},
{"op": "MUL", "lhs": {"type": "POL_NEXT", "index": 4}, "rhs": {"type": "EXPR", "index": 11}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 12}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "VAR", "index": 16}},
{"op": "SUB", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "CONST", "index": 0}}
],
"outputs": [1, 3, 5, 10, 13, 14, 15, 16, 17, 18, 19]
}
15 changes: 15 additions & 0 deletions air-script/tests/binary/binary.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{
"num_polys": 2,
"num_variables": 16,
"constants": [0, 2, 0, 2],
"expressions": [
{"op": "MUL", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "POL", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 0}, "rhs": {"type": "POL", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 1}, "rhs": {"type": "CONST", "index": 0}},
{"op": "MUL", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 3}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 4}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}}
],
"outputs": [2, 5, 6]
}
15 changes: 15 additions & 0 deletions air-script/tests/binary/generated_binary.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{
"num_polys": 2,
"num_variables": 16,
"constants": [0, 2, 0, 2],
"expressions": [
{"op": "MUL", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "POL", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 0}, "rhs": {"type": "POL", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 1}, "rhs": {"type": "CONST", "index": 0}},
{"op": "MUL", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 3}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 4}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}}
],
"outputs": [2, 5, 6]
}
42 changes: 42 additions & 0 deletions air-script/tests/constants/constants.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
{
"num_polys": 10,
"num_variables": 32,
"constants": [1, 0, 1, 1, 2, 2, 0],
"expressions": [
{"op": "ADD", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 0}, "rhs": {"type": "EXPR", "index": 0}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 1}, "rhs": {"type": "EXPR", "index": 2}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 1}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 4}, "rhs": {"type": "POL", "index": 2}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 2}, "rhs": {"type": "EXPR", "index": 5}},
{"op": "ADD", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "CONST", "index": 0}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 7}, "rhs": {"type": "EXPR", "index": 8}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 4}, "rhs": {"type": "EXPR", "index": 9}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 1}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 11}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 12}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 15}},
{"op": "SUB", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "EXPR", "index": 16}},
{"op": "SUB", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 1}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 18}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "EXPR", "index": 19}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 21}, "rhs": {"type": "CONST", "index": 0}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 22}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 23}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 24}, "rhs": {"type": "CONST", "index": 4}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 25}, "rhs": {"type": "CONST", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "EXPR", "index": 26}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 28}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 29}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 31}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 32}}
],
"outputs": [1, 3, 6, 10, 13, 14, 17, 20, 27, 30, 33]
}
42 changes: 42 additions & 0 deletions air-script/tests/constants/generated_constants.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
{
"num_polys": 10,
"num_variables": 32,
"constants": [1, 0, 1, 1, 2, 2, 0],
"expressions": [
{"op": "ADD", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 0}, "rhs": {"type": "EXPR", "index": 0}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 1}, "rhs": {"type": "EXPR", "index": 2}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 1}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 4}, "rhs": {"type": "POL", "index": 2}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 2}, "rhs": {"type": "EXPR", "index": 5}},
{"op": "ADD", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "CONST", "index": 0}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 7}, "rhs": {"type": "EXPR", "index": 8}},
{"op": "SUB", "lhs": {"type": "POL_NEXT", "index": 4}, "rhs": {"type": "EXPR", "index": 9}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 1}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 11}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 12}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 15}},
{"op": "SUB", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "EXPR", "index": 16}},
{"op": "SUB", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 1}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 18}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "POL", "index": 2}, "rhs": {"type": "EXPR", "index": 19}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 21}, "rhs": {"type": "CONST", "index": 0}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 22}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 23}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "EXPR", "index": 24}, "rhs": {"type": "CONST", "index": 4}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 25}, "rhs": {"type": "CONST", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL", "index": 3}, "rhs": {"type": "EXPR", "index": 26}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 1}, "rhs": {"type": "CONST", "index": 4}},
{"op": "ADD", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 28}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 29}},
{"op": "MUL", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "CONST", "index": 0}},
{"op": "SUB", "lhs": {"type": "CONST", "index": 0}, "rhs": {"type": "EXPR", "index": 31}},
{"op": "SUB", "lhs": {"type": "POL", "index": 4}, "rhs": {"type": "EXPR", "index": 32}}
],
"outputs": [1, 3, 6, 10, 13, 14, 17, 20, 27, 30, 33]
}
14 changes: 14 additions & 0 deletions air-script/tests/exponentiation/exponentiation.air
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
def ExponentiationAir

trace_columns:
main: [a, b]

public_inputs:
stack_inputs: [16]

boundary_constraints:
enf a.first = stack_inputs[0]^3

transition_constraints:
enf a^15 - a = 0
enf b^2 - b = 0
20 changes: 20 additions & 0 deletions air-script/tests/exponentiation/generated_exponentiation.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
{
"num_polys": 2,
"num_variables": 16,
"constants": [15, 0, 2],
"expressions": [
{"op": "MUL", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "POL", "index": 0}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 0}, "rhs": {"type": "EXPR", "index": 0}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 1}, "rhs": {"type": "EXPR", "index": 1}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 2}, "rhs": {"type": "EXPR", "index": 1}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 3}, "rhs": {"type": "EXPR", "index": 0}},
{"op": "MUL", "lhs": {"type": "EXPR", "index": 4}, "rhs": {"type": "POL", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 5}, "rhs": {"type": "POL", "index": 0}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 6}, "rhs": {"type": "CONST", "index": 1}},
{"op": "MUL", "lhs": {"type": "POL", "index": 1}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 8}, "rhs": {"type": "POL", "index": 1}},
{"op": "SUB", "lhs": {"type": "EXPR", "index": 9}, "rhs": {"type": "CONST", "index": 1}},
{"op": "SUB", "lhs": {"type": "POL", "index": 0}, "rhs": {"type": "VAR", "index": 0}}
],
"outputs": [7, 10, 11]
}
38 changes: 25 additions & 13 deletions air-script/tests/helpers.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
use codegen_winter::CodeGenerator;
use codegen_gce::GCECodeGenerator;
use codegen_winter::WinterfellCodeGenerator;
use ir::AirIR;
use parser::parse;
use std::fs;
Expand All @@ -8,43 +9,54 @@ pub enum TestError {
IO(String),
Parse(String),
IR(String),
Gce(String),
}

pub struct Test {
input_path: String,
ir: AirIR,
}

impl Test {
pub fn new(input_path: String) -> Self {
Test { input_path }
}

pub fn transpile(&self) -> Result<String, TestError> {
pub fn new(input_path: String) -> Result<Self, TestError> {
// load source input from file
let source = fs::read_to_string(&self.input_path).map_err(|err| {
let source = fs::read_to_string(&input_path).map_err(|err| {
TestError::IO(format!(
"Failed to open input file `{:?}` - {}",
self.input_path, err
input_path, err
))
})?;

// parse the input file to the internal representation
let parsed = parse(source.as_str()).map_err(|_| {
TestError::Parse(format!(
"Failed to parse the input air file at {}",
&self.input_path
input_path
))
})?;

let ir = AirIR::from_source(&parsed).map_err(|_| {
TestError::IR(format!(
"Failed to convert the input air file at {} to IR representation",
&self.input_path
input_path
))
})?;

Ok(Test { ir })
}

pub fn generate_winterfell(&self) -> String {
// generate Rust code targeting Winterfell
let codegen = CodeGenerator::new(&ir);
Ok(codegen.generate())
let codegen = WinterfellCodeGenerator::new(&self.ir);
codegen.generate()
}

pub fn generate_gce(&self, extension_degree: u8, path: &str) -> Result<(), TestError> {
// generate Rust code targeting Winterfell
let codegen = GCECodeGenerator::new(&self.ir, extension_degree).map_err(|err| {
TestError::Gce(format!("Failed to create GCECodeGenerator: {:?}", err))
})?;
codegen
.generate(path)
.map_err(|err| TestError::Gce(format!("Failed to generate JSON file: {:?}", err)))
}
}
Loading

0 comments on commit 02dba70

Please sign in to comment.