From 5e36d4ba03ca26b85aba9ece2884267605f2d17b Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 19 Jan 2023 00:13:09 -0800 Subject: [PATCH] features: add bellman, spartan, aby (#139) Also, add ./driver --check-all, which checks every single-feature build. --- Cargo.toml | 15 +- driver.py | 15 ++ examples/circ.rs | 38 +++-- examples/zk.rs | 22 ++- src/ir/term/dist.rs | 30 ++++ src/ir/term/test.rs | 256 +++++++++++++++++-------------- src/target/aby/assignment/ilp.rs | 3 +- src/target/ilp/mod.rs | 4 +- src/target/ilp/trans.rs | 18 +-- src/target/mod.rs | 2 + src/target/r1cs/mod.rs | 4 +- src/target/r1cs/trans.rs | 132 ++++++---------- util.py | 4 +- 13 files changed, 308 insertions(+), 235 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 32404bcd..9e8f5c0f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,7 +11,7 @@ circ_fields = { path = "circ_fields" } circ_opt = { path = "circ_opt" } circ_hc = { path = "circ_hc", default-features = false, features = ["rc", "lru"]} rug = { version = "1.11", features = ["serde"] } -gmp-mpfr-sys = "1.4" +gmp-mpfr-sys = { version = "1.4", optional = true } lazy_static = { version = "1.4", optional = true } rand = "0.8" rsmt2 = { version = "0.14", optional = true } @@ -57,12 +57,17 @@ approx = "0.5.0" [features] default = [] +# frontends c = ["lang-c"] -lp = ["good_lp", "lp-solvers"] -r1cs = ["bellman", "spartan", "merlin", "curve25519-dalek", "ff", "group", "pairing", "serde_bytes", "bincode"] -smt = ["rsmt2", "ieee754"] zok = ["zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"] datalog = ["pest", "pest-ast", "pest_derive", "from-pest", "lazy_static"] +# backends +smt = ["rsmt2", "ieee754"] +lp = ["good_lp", "lp-solvers"] +aby = ["lp"] +r1cs = [] +spartan = ["r1cs", "dep:spartan", "merlin", "curve25519-dalek", "bincode", "gmp-mpfr-sys"] +bellman = ["r1cs", "dep:bellman", "ff", "group", "pairing", "serde_bytes", "bincode", "gmp-mpfr-sys"] [[example]] name = "circ" @@ -81,7 +86,7 @@ required-features = ["smt", "zok"] [[example]] name = "opa_bench" -required-features = ["lp"] +required-features = ["lp", "aby"] [profile.release] debug = true diff --git a/driver.py b/driver.py index 1d0d3718..1168ebbc 100755 --- a/driver.py +++ b/driver.py @@ -61,6 +61,15 @@ def check(features): log_run_check(cmd) +def check_all(): + """ + Run cargo check with every individual feature + """ + for feature in cargo_features: + log_run_check(["cargo", "check", "--tests", "--examples", "--benches", "--bins", "--features", feature]) + + + def build(features): """ Run cargo build and any test cases in the feature list @@ -271,6 +280,9 @@ if __name__ == "__main__": parser.add_argument( "-c", "--check", action="store_true", help="run `cargo check`" ) + parser.add_argument( + "--check-all", action="store_true", help="Check all single-feature builds" + ) parser.add_argument( "-b", "--build", @@ -355,6 +367,9 @@ if __name__ == "__main__": if args.check: check(features) + if args.check_all: + check_all() + if args.build: build(features) diff --git a/examples/circ.rs b/examples/circ.rs index b4d12a2f..417a52a6 100644 --- a/examples/circ.rs +++ b/examples/circ.rs @@ -1,13 +1,14 @@ #![allow(unused_imports)] -#[cfg(feature = "r1cs")] -use bellman::gadgets::test::TestConstraintSystem; -#[cfg(feature = "r1cs")] -use bellman::groth16::{ - create_random_proof, generate_parameters, generate_random_parameters, prepare_verifying_key, - verify_proof, Parameters, Proof, VerifyingKey, +#[cfg(feature = "bellman")] +use bellman::{ + gadgets::test::TestConstraintSystem, + groth16::{ + create_random_proof, generate_parameters, generate_random_parameters, + prepare_verifying_key, verify_proof, Parameters, Proof, VerifyingKey, + }, + Circuit, }; -#[cfg(feature = "r1cs")] -use bellman::Circuit; +#[cfg(feature = "bellman")] use bls12_381::{Bls12, Scalar}; use circ::cfg::{ cfg, @@ -29,15 +30,16 @@ use circ::ir::{ text::{parse_value_map, serialize_value_map}, }, }; +#[cfg(feature = "aby")] use circ::target::aby::trans::to_aby; #[cfg(feature = "lp")] use circ::target::ilp::{assignment_to_values, trans::to_ilp}; -#[cfg(feature = "r1cs")] +#[cfg(feature = "bellman")] use circ::target::r1cs::bellman::gen_params; -use circ::target::r1cs::opt::reduce_linearities; -#[cfg(feature = "r1cs")] +#[cfg(feature = "spartan")] use circ::target::r1cs::spartan::write_data; -use circ::target::r1cs::trans::to_r1cs; +#[cfg(feature = "r1cs")] +use circ::target::r1cs::{opt::reduce_linearities, trans::to_r1cs}; #[cfg(feature = "smt")] use circ::target::smt::find_model; use circ_fields::FieldT; @@ -154,6 +156,7 @@ fn determine_language(l: &Language, input_path: &Path) -> DeterminedLanguage { } } +#[allow(unused_variables, unreachable_code)] fn main() { env_logger::Builder::from_default_env() .format_level(false) @@ -281,6 +284,7 @@ fn main() { println!("Final R1cs size: {}", prover_data.r1cs.constraints().len()); match action { ProofAction::Count => (), + #[cfg(feature = "bellman")] ProofAction::Setup => { println!("Generating Parameters"); gen_params::( @@ -291,16 +295,22 @@ fn main() { ) .unwrap(); } + #[cfg(not(feature = "bellman"))] + ProofAction::Setup => panic!("Missing feature: bellman"), + #[cfg(feature = "spartan")] ProofAction::SpartanSetup => { write_data::<_, _>(prover_key, verifier_key, &prover_data, &verifier_data) .unwrap(); } + #[cfg(not(feature = "spartan"))] + ProofAction::SpartanSetup => panic!("Missing feature: spartan"), } } #[cfg(not(feature = "r1cs"))] Backend::R1cs { .. } => { panic!("Missing feature: r1cs"); } + #[cfg(feature = "aby")] Backend::Mpc { cost_model, selection_scheme, @@ -315,6 +325,10 @@ fn main() { println!("Selection scheme: {}", selection_scheme); to_aby(cs, &path_buf, &lang_str, &cost_model, &selection_scheme); } + #[cfg(not(feature = "aby"))] + Backend::Mpc { .. } => { + panic!("Missing feature: aby"); + } #[cfg(feature = "lp")] Backend::Ilp { .. } => { println!("Converting to ilp"); diff --git a/examples/zk.rs b/examples/zk.rs index 5f6ccef5..95423cd0 100644 --- a/examples/zk.rs +++ b/examples/zk.rs @@ -1,10 +1,17 @@ -use bls12_381::Bls12; use circ::cfg::clap::{self, Parser, ValueEnum}; -use circ::ir::term::text::parse_value_map; -use circ::target::r1cs::bellman; -use circ::target::r1cs::spartan; use std::path::PathBuf; +#[cfg(feature = "bellman")] +use bls12_381::Bls12; +#[cfg(feature = "bellman")] +use circ::target::r1cs::bellman; + +#[cfg(feature = "spartan")] +use circ::target::r1cs::spartan; + +#[cfg(any(feature = "bellman", feature = "spartan"))] +use circ::ir::term::text::parse_value_map; + #[derive(Debug, Parser)] #[command(name = "zk", about = "The CirC ZKP runner")] struct Options { @@ -40,16 +47,19 @@ fn main() { .init(); let opts = Options::parse(); match opts.action { + #[cfg(feature = "bellman")] ProofAction::Prove => { let input_map = parse_value_map(&std::fs::read(opts.inputs).unwrap()); println!("Proving"); bellman::prove::(opts.prover_key, opts.proof, &input_map).unwrap(); } + #[cfg(feature = "bellman")] ProofAction::Verify => { let input_map = parse_value_map(&std::fs::read(opts.inputs).unwrap()); println!("Verifying"); bellman::verify::(opts.verifier_key, opts.proof, &input_map).unwrap(); } + #[cfg(feature = "spartan")] ProofAction::Spartan => { let prover_input_map = parse_value_map(&std::fs::read(opts.pin).unwrap()); println!("Spartan Proving"); @@ -59,5 +69,9 @@ fn main() { println!("Spartan Verifying"); spartan::verify(opts.verifier_key, &verifier_input_map, &gens, &inst, proof).unwrap(); } + #[cfg(not(feature = "bellman"))] + ProofAction::Prove | ProofAction::Verify => panic!("Missing feature: bellman"), + #[cfg(not(feature = "spartan"))] + ProofAction::Spartan => panic!("Missing feature: spartan"), } } diff --git a/src/ir/term/dist.rs b/src/ir/term/dist.rs index 038442fe..04e62dfe 100644 --- a/src/ir/term/dist.rs +++ b/src/ir/term/dist.rs @@ -321,6 +321,36 @@ pub mod test { use rand::distributions::Distribution; use rand::SeedableRng; + #[derive(Clone, Debug)] + pub struct PureBool(pub Term, pub FxHashMap); + + impl Arbitrary for PureBool { + fn arbitrary(g: &mut Gen) -> Self { + let mut rng = rand::rngs::StdRng::seed_from_u64(u64::arbitrary(g)); + let t = PureBoolDist(g.size()).sample(&mut rng); + let values: FxHashMap = PostOrderIter::new(t.clone()) + .filter_map(|c| { + if let Op::Var(n, _) = &c.op() { + Some((n.clone(), Value::Bool(bool::arbitrary(g)))) + } else { + None + } + }) + .collect(); + PureBool(t, values) + } + + fn shrink(&self) -> Box> { + let vs = self.1.clone(); + let ts = PostOrderIter::new(self.0.clone()) + .collect::>() + .into_iter() + .rev(); + + Box::new(ts.skip(1).map(move |t| PureBool(t, vs.clone()))) + } + } + #[derive(Clone)] pub struct ArbitraryTerm(pub Term); diff --git a/src/ir/term/test.rs b/src/ir/term/test.rs index c7963e29..f8e3ce65 100644 --- a/src/ir/term/test.rs +++ b/src/ir/term/test.rs @@ -2,7 +2,6 @@ #![allow(missing_docs)] use super::*; -use crate::target::r1cs::trans::test::bv; use fxhash::FxHashMap; #[test] @@ -71,12 +70,22 @@ fn map_test_bv_key() { let a1 = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0001, 4), bv(0b0010, 4), bv(0b0011, 4), bv(0b0100, 4)], + vec![ + bv_lit(0b0001, 4), + bv_lit(0b0010, 4), + bv_lit(0b0011, 4), + bv_lit(0b0100, 4), + ], ); let a2 = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0001, 4), bv(0b0100, 4), bv(0b1001, 4), bv(0b0000, 4)], + vec![ + bv_lit(0b0001, 4), + bv_lit(0b0100, 4), + bv_lit(0b1001, 4), + bv_lit(0b0000, 4), + ], ); let actual_eq = term![Op::Map(Box::new(Op::Eq)); a1.clone(), a2.clone()]; let actual_add = term![Op::Map(Box::new(BV_ADD)); a1, a2]; @@ -88,7 +97,12 @@ fn map_test_bv_key() { let expected_add = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0010, 4), bv(0b0110, 4), bv(0b1100, 4), bv(0b0100, 4)], + vec![ + bv_lit(0b0010, 4), + bv_lit(0b0110, 4), + bv_lit(0b1100, 4), + bv_lit(0b0100, 4), + ], ); assert_eq!( @@ -106,22 +120,42 @@ fn test_rot() { let a = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0001, 4), bv(0b0010, 4), bv(0b0011, 4), bv(0b0100, 4)], + vec![ + bv_lit(0b0001, 4), + bv_lit(0b0010, 4), + bv_lit(0b0011, 4), + bv_lit(0b0100, 4), + ], ); let expected_rot_0 = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0001, 4), bv(0b0010, 4), bv(0b0011, 4), bv(0b0100, 4)], + vec![ + bv_lit(0b0001, 4), + bv_lit(0b0010, 4), + bv_lit(0b0011, 4), + bv_lit(0b0100, 4), + ], ); let expected_rot_1 = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0100, 4), bv(0b0001, 4), bv(0b0010, 4), bv(0b0011, 4)], + vec![ + bv_lit(0b0100, 4), + bv_lit(0b0001, 4), + bv_lit(0b0010, 4), + bv_lit(0b0011, 4), + ], ); let expected_rot_2 = make_array( Sort::BitVector(32), Sort::BitVector(4), - vec![bv(0b0011, 4), bv(0b0100, 4), bv(0b0001, 4), bv(0b0010, 4)], + vec![ + bv_lit(0b0011, 4), + bv_lit(0b0100, 4), + bv_lit(0b0001, 4), + bv_lit(0b0010, 4), + ], ); let rot_0 = term![Op::Rot(0); a.clone()]; @@ -201,20 +235,20 @@ pub fn bv_eq_tests() -> Vec { vec![ term![ Op::Eq; - bv(0b1111, 4), - bv(0b1111, 4) + bv_lit(0b1111, 4), + bv_lit(0b1111, 4) ], term![ Op::Eq; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], term![ Op::Eq; term![ Op::Eq; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], bool(true) ], @@ -222,8 +256,8 @@ pub fn bv_eq_tests() -> Vec { Op::Eq; term![ Op::Eq; - bv(0b0101, 4), - bv(0b1101, 4) + bv_lit(0b0101, 4), + bv_lit(0b1101, 4) ], bool(false) ], @@ -234,20 +268,20 @@ pub fn bv_le_tests() -> Vec { vec![ term![ BV_ULE; - bv(0b1111, 4), - bv(0b1111, 4) + bv_lit(0b1111, 4), + bv_lit(0b1111, 4) ], term![ BV_ULE; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], term![ Op::Eq; term![ BV_ULE; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], bool(true) ], @@ -255,8 +289,8 @@ pub fn bv_le_tests() -> Vec { Op::Eq; term![ BV_ULE; - bv(0b1101, 4), - bv(0b0101, 4) + bv_lit(0b1101, 4), + bv_lit(0b0101, 4) ], bool(false) ], @@ -267,30 +301,30 @@ pub fn bv_sle_tests() -> Vec { vec![ term![ BV_SLE; - bv(0b1111, 4), - bv(0b1111, 4) + bv_lit(0b1111, 4), + bv_lit(0b1111, 4) ], term![ BV_SLE; - bv(0b1000, 4), - bv(0b0111, 4) + bv_lit(0b1000, 4), + bv_lit(0b0111, 4) ], term![ BV_SLE; - bv(0b1000, 4), - bv(0b0000, 4) + bv_lit(0b1000, 4), + bv_lit(0b0000, 4) ], term![ BV_SLE; - bv(0b1111, 4), - bv(0b0000, 4) + bv_lit(0b1111, 4), + bv_lit(0b0000, 4) ], term![ Op::Eq; term![ BV_SLE; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], bool(true) ], @@ -298,8 +332,8 @@ pub fn bv_sle_tests() -> Vec { Op::Eq; term![ BV_SLE; - bv(0b0101, 4), - bv(0b1101, 4) + bv_lit(0b0101, 4), + bv_lit(0b1101, 4) ], bool(false) ], @@ -310,25 +344,25 @@ pub fn bv_slt_tests() -> Vec { vec![ term![ BV_SLT; - bv(0b0000, 4), - bv(0b0001, 4) + bv_lit(0b0000, 4), + bv_lit(0b0001, 4) ], term![ BV_SLT; - bv(0b1111, 4), - bv(0b0000, 4) + bv_lit(0b1111, 4), + bv_lit(0b0000, 4) ], term![ BV_SLT; - bv(0b0101, 4), - bv(0b0110, 4) + bv_lit(0b0101, 4), + bv_lit(0b0110, 4) ], term![ Op::Eq; term![ BV_SLT; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], bool(false) ], @@ -336,8 +370,8 @@ pub fn bv_slt_tests() -> Vec { Op::Eq; term![ BV_SLT; - bv(0b0101, 4), - bv(0b1101, 4) + bv_lit(0b0101, 4), + bv_lit(0b1101, 4) ], bool(false) ], @@ -349,10 +383,10 @@ pub fn bv_concat_tests() -> Vec { Op::Eq; term![ BV_CONCAT; - bv(0b0101, 4), - bv(0b0100, 4) + bv_lit(0b0101, 4), + bv_lit(0b0100, 4) ], - bv(0b01010100, 8) + bv_lit(0b01010100, 8) ]] } @@ -361,9 +395,9 @@ pub fn bv_not_tests() -> Vec { Op::Eq; term![ BV_NOT; - bv(0b0100, 4) + bv_lit(0b0100, 4) ], - bv(0b1011, 4) + bv_lit(0b1011, 4) ]] } @@ -373,25 +407,25 @@ pub fn bv_neg_tests() -> Vec { Op::Eq; term![ BV_NEG; - bv(0b0100, 4) + bv_lit(0b0100, 4) ], - bv(0b1100, 4) + bv_lit(0b1100, 4) ], term![ Op::Eq; term![ BV_NEG; - bv(0b0000, 4) + bv_lit(0b0000, 4) ], - bv(0b0000, 4) + bv_lit(0b0000, 4) ], term![ Op::Eq; term![ BV_NEG; - bv(0b1111, 4) + bv_lit(0b1111, 4) ], - bv(0b0001, 4) + bv_lit(0b0001, 4) ], ] } @@ -400,20 +434,20 @@ pub fn bv_lt_tests() -> Vec { vec![ term![ BV_ULT; - bv(0b0111, 4), - bv(0b1111, 4) + bv_lit(0b0111, 4), + bv_lit(0b1111, 4) ], term![ BV_ULT; - bv(0b0101, 4), - bv(0b1101, 4) + bv_lit(0b0101, 4), + bv_lit(0b1101, 4) ], term![ Op::Eq; term![ BV_ULT; - bv(0b0101, 4), - bv(0b0101, 4) + bv_lit(0b0101, 4), + bv_lit(0b0101, 4) ], bool(false) ], @@ -421,8 +455,8 @@ pub fn bv_lt_tests() -> Vec { Op::Eq; term![ BV_ULT; - bv(0b0101, 4), - bv(0b1101, 4) + bv_lit(0b0101, 4), + bv_lit(0b1101, 4) ], bool(false) ], @@ -433,13 +467,13 @@ pub fn bv_and_tests() -> Vec { vec![ term![ Op::Eq; - term![BV_AND; bv(0b1111,4), bv(0b1111,4)], - bv(0b1111, 4) + term![BV_AND; bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b1111, 4) ], term![ Op::Eq; - term![BV_AND; bv(0b0111,4), bv(0b1101,4)], - bv(0b0101, 4) + term![BV_AND; bv_lit(0b0111,4), bv_lit(0b1101,4)], + bv_lit(0b0101, 4) ], ] } @@ -447,13 +481,13 @@ pub fn bv_or_tests() -> Vec { vec![ term![ Op::Eq; - term![BV_OR; bv(0b1111,4), bv(0b1111,4)], - bv(0b1111, 4) + term![BV_OR; bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b1111, 4) ], term![ Op::Eq; - term![BV_OR; bv(0b0111,4), bv(0b0101,4)], - bv(0b0111, 4) + term![BV_OR; bv_lit(0b0111,4), bv_lit(0b0101,4)], + bv_lit(0b0111, 4) ], ] } @@ -461,28 +495,28 @@ pub fn bv_add_tests() -> Vec { vec![ term![ Op::Eq; - term![BV_ADD; bv(0b1111,4), bv(0b1111,4)], - bv(0b1110, 4) + term![BV_ADD; bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b1110, 4) ], term![ Op::Eq; - term![BV_ADD; bv(0b1111,4), bv(0b0101,4)], - bv(0b0100, 4) + term![BV_ADD; bv_lit(0b1111,4), bv_lit(0b0101,4)], + bv_lit(0b0100, 4) ], term![ Op::Eq; - term![BV_ADD; bv(0b1111,4), bv(0b1111,4), bv(0b1111,4), bv(0b1111,4)], - bv(0b1100, 4) + term![BV_ADD; bv_lit(0b1111,4), bv_lit(0b1111,4), bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b1100, 4) ], term![ Op::Eq; - term![BV_ADD; bv(0b1111,4), bv(0b1111,4), bv(0b1111,4)], - bv(0b1101, 4) + term![BV_ADD; bv_lit(0b1111,4), bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b1101, 4) ], term![ Op::Eq; - term![BV_ADD; bv(0b0000,4), bv(0b1110,4), bv(0b0000,4), bv(0b0000,4)], - bv(0b1110, 4) + term![BV_ADD; bv_lit(0b0000,4), bv_lit(0b1110,4), bv_lit(0b0000,4), bv_lit(0b0000,4)], + bv_lit(0b1110, 4) ], ] } @@ -490,23 +524,23 @@ pub fn bv_mul_tests() -> Vec { vec![ term![ Op::Eq; - term![BV_MUL; bv(0b0001,4)], - bv(0b0001, 4) + term![BV_MUL; bv_lit(0b0001,4)], + bv_lit(0b0001, 4) ], term![ Op::Eq; - term![BV_MUL; bv(0b0000,4), bv(0b1111,4)], - bv(0b0000, 4) + term![BV_MUL; bv_lit(0b0000,4), bv_lit(0b1111,4)], + bv_lit(0b0000, 4) ], term![ Op::Eq; - term![BV_MUL; bv(0b0010,4), bv(0b1111,4)], - bv(0b1110, 4) + term![BV_MUL; bv_lit(0b0010,4), bv_lit(0b1111,4)], + bv_lit(0b1110, 4) ], term![ Op::Eq; - term![BV_MUL; bv(0b1001,4), bv(0b0101,4)], - bv(0b1101, 4) + term![BV_MUL; bv_lit(0b1001,4), bv_lit(0b0101,4)], + bv_lit(0b1101, 4) ], ] } @@ -517,25 +551,25 @@ pub fn bv_sext_tests() -> Vec { Op::Eq; term![ Op::BvSext(2); - bv(0b10, 2) + bv_lit(0b10, 2) ], - bv(0b1110, 4) + bv_lit(0b1110, 4) ], term![ Op::Eq; term![ Op::BvSext(2); - bv(0b01, 2) + bv_lit(0b01, 2) ], - bv(0b0001, 4) + bv_lit(0b0001, 4) ], term![ Op::Eq; term![ Op::BvSext(2); - term![BV_ADD; bv(0b01, 2), bv(0b01, 2)] + term![BV_ADD; bv_lit(0b01, 2), bv_lit(0b01, 2)] ], - bv(0b1110, 4) + bv_lit(0b1110, 4) ], ] } @@ -546,25 +580,25 @@ pub fn bv_uext_tests() -> Vec { Op::Eq; term![ Op::BvUext(2); - bv(0b10, 2) + bv_lit(0b10, 2) ], - bv(0b0010, 4) + bv_lit(0b0010, 4) ], term![ Op::Eq; term![ Op::BvUext(2); - term![BV_ADD; bv(0b01, 2), bv(0b01, 2)] + term![BV_ADD; bv_lit(0b01, 2), bv_lit(0b01, 2)] ], - bv(0b0010, 4) + bv_lit(0b0010, 4) ], term![ Op::Eq; term![ Op::BvUext(2); - bv(0b01, 2) + bv_lit(0b01, 2) ], - bv(0b0001, 4) + bv_lit(0b0001, 4) ], ] } @@ -572,23 +606,23 @@ pub fn bv_sub_tests() -> Vec { vec![ term![ Op::Eq; - term![BV_SUB; bv(0b1111,4), bv(0b1111,4)], - bv(0b0000, 4) + term![BV_SUB; bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b0000, 4) ], term![ Op::Eq; - term![BV_SUB; bv(0b1111,4), bv(0b0000,4)], - bv(0b1111, 4) + term![BV_SUB; bv_lit(0b1111,4), bv_lit(0b0000,4)], + bv_lit(0b1111, 4) ], term![ Op::Eq; - term![BV_SUB; bv(0b1111,4), bv(0b1110,4)], - bv(0b0001, 4) + term![BV_SUB; bv_lit(0b1111,4), bv_lit(0b1110,4)], + bv_lit(0b0001, 4) ], term![ Op::Eq; - term![BV_SUB; bv(0b0000,4), bv(0b1111,4)], - bv(0b0001, 4) + term![BV_SUB; bv_lit(0b0000,4), bv_lit(0b1111,4)], + bv_lit(0b0001, 4) ], ] } diff --git a/src/target/aby/assignment/ilp.rs b/src/target/aby/assignment/ilp.rs index bddd8853..3a338884 100644 --- a/src/target/aby/assignment/ilp.rs +++ b/src/target/aby/assignment/ilp.rs @@ -35,7 +35,8 @@ use super::{ShareType, SharingMap, SHARE_TYPES}; use crate::ir::term::*; use crate::target::aby::assignment::CostModel; -use crate::target::ilp::{variable, Expression, Ilp, Variable}; +use crate::target::ilp::{Expression, Ilp, Variable}; +use good_lp::variable; use std::env::var; diff --git a/src/target/ilp/mod.rs b/src/target/ilp/mod.rs index 7bf8635c..953d703b 100644 --- a/src/target/ilp/mod.rs +++ b/src/target/ilp/mod.rs @@ -5,8 +5,8 @@ pub mod trans; use crate::ir::term::*; use fxhash::FxHashMap as HashMap; pub(crate) use good_lp::{ - variable, Constraint, Expression, ProblemVariables, ResolutionError, Solution, Solver, - SolverModel, Variable, VariableDefinition, + Constraint, Expression, ProblemVariables, ResolutionError, Solution, Solver, SolverModel, + Variable, VariableDefinition, }; use log::debug; use std::fmt::{self, Debug, Formatter}; diff --git a/src/target/ilp/trans.rs b/src/target/ilp/trans.rs index d752d24e..55a90ee7 100644 --- a/src/target/ilp/trans.rs +++ b/src/target/ilp/trans.rs @@ -66,7 +66,7 @@ impl ToMilp { fn fresh_bv(&mut self, ctx: &D, bits: usize) -> Expression { let n = format!("{}_v{}", ctx, self.next_idx); self.next_idx += 1; - self.bv(n, bits) + self.bv_lit(n, bits) } /// Get a new variable, with name dependent on `d`. @@ -83,7 +83,7 @@ impl ToMilp { } /// Get a new BV variable, named `name`. - fn bv(&mut self, name: String, bits: usize) -> Expression { + fn bv_lit(&mut self, name: String, bits: usize) -> Expression { self.ilp .new_variable( variable() @@ -258,7 +258,7 @@ impl ToMilp { if !self.cache.contains_key(&bv) { match &bv.op() { Op::Var(name, Sort::BitVector(n_bits)) => { - let var = self.bv(name.clone(), *n_bits); + let var = self.bv_lit(name.clone(), *n_bits); self.set_bv_uint(bv.clone(), var, n); } Op::Const(Value::BitVector(b)) => { @@ -684,8 +684,8 @@ pub fn to_ilp(cs: Computation) -> Ilp { mod test { use super::*; use crate::ir::proof::Constraints; + use crate::ir::term::dist::test::PureBool; use crate::ir::term::test as test_vecs; - use crate::target::r1cs::trans::test::{bv, PureBool}; use approx::assert_abs_diff_eq; use good_lp::default_solver; use quickcheck_macros::quickcheck; @@ -864,7 +864,7 @@ mod test { let cs = Computation { outputs: vec![term![BV_MUL; leaf_term(Op::Var("a".to_owned(), Sort::BitVector(4))), - bv(1,4) + bv_lit(1,4) ]], metadata: ComputationMetadata::default(), precomputes: Default::default(), @@ -880,7 +880,7 @@ mod test { precomputes: Default::default(), outputs: vec![term![BV_MUL; leaf_term(Op::Var("a".to_owned(), Sort::BitVector(4))), - bv(2,4) + bv_lit(2,4) ]], metadata: ComputationMetadata::default(), }; @@ -895,7 +895,7 @@ mod test { outputs: vec![term![BV_ADD; term![BV_MUL; leaf_term(Op::Var("a".to_owned(), Sort::BitVector(4))), - bv(2,4) + bv_lit(2,4) ], leaf_term(Op::Var("a".to_owned(), Sort::BitVector(4))) @@ -914,8 +914,8 @@ mod test { let cs = Computation { precomputes: Default::default(), outputs: vec![term![BV_ADD; - term![ITE; c, bv(2,4), bv(1,4)], - term![BV_MUL; a, bv(2,4)] + term![ITE; c, bv_lit(2,4), bv_lit(1,4)], + term![BV_MUL; a, bv_lit(2,4)] ]], metadata: ComputationMetadata::default(), }; diff --git a/src/target/mod.rs b/src/target/mod.rs index 8fcb9319..f0a70785 100644 --- a/src/target/mod.rs +++ b/src/target/mod.rs @@ -1,8 +1,10 @@ //! Target circuit representations (and lowering passes) +#[cfg(feature = "aby")] pub mod aby; #[cfg(feature = "lp")] pub mod ilp; +#[cfg(feature = "r1cs")] pub mod r1cs; #[cfg(feature = "smt")] pub mod smt; diff --git a/src/target/r1cs/mod.rs b/src/target/r1cs/mod.rs index 25e201dd..4fd13c29 100644 --- a/src/target/r1cs/mod.rs +++ b/src/target/r1cs/mod.rs @@ -12,10 +12,10 @@ use std::hash::Hash; use crate::ir::term::*; -#[cfg(feature = "r1cs")] +#[cfg(feature = "bellman")] pub mod bellman; pub mod opt; -#[cfg(feature = "r1cs")] +#[cfg(feature = "spartan")] pub mod spartan; pub mod trans; diff --git a/src/target/r1cs/trans.rs b/src/target/r1cs/trans.rs index b832226d..782d0a60 100644 --- a/src/target/r1cs/trans.rs +++ b/src/target/r1cs/trans.rs @@ -273,7 +273,7 @@ impl<'cfg> ToR1cs<'cfg> { self.embed_bool(c); } Sort::BitVector(_) => { - self.embed_bv(c); + self.embed_bv_lit(c); } Sort::Field(_) => { self.embed_pf(c); @@ -501,21 +501,21 @@ impl<'cfg> ToR1cs<'cfg> { } /// Shift `x` left by `2^y`, if bit-valued `c` is true. - fn const_pow_shift_bv(&mut self, x: &TermLc, y: usize, c: TermLc) -> TermLc { + fn const_pow_shift_bv_lit(&mut self, x: &TermLc, y: usize, c: TermLc) -> TermLc { self.ite(c, x.clone() * (1 << (1 << y)), x) } /// Shift `x` left by `y`, filling the blank spots with bit-valued `ext_bit`. /// Returns an *oversized* number - fn shift_bv(&mut self, x: TermLc, y: Vec, ext_bit: Option) -> TermLc { + fn shift_bv_lit(&mut self, x: TermLc, y: Vec, ext_bit: Option) -> TermLc { if let Some(b) = ext_bit { - let left = self.shift_bv(x, y.clone(), None); - let right = self.shift_bv(b.clone(), y, None) - 1; + let left = self.shift_bv_lit(x, y.clone(), None); + let right = self.shift_bv_lit(b.clone(), y, None) - 1; left + &self.mul(b, right) } else { y.into_iter() .enumerate() - .fold(x, |x, (i, yi)| self.const_pow_shift_bv(&x, i, yi)) + .fold(x, |x, (i, yi)| self.const_pow_shift_bv_lit(&x, i, yi)) } } @@ -536,7 +536,7 @@ impl<'cfg> ToR1cs<'cfg> { Some(e) => e.clone() * &self.r1cs.modulus.new_v((1 << x_w) - 1), None => self.zero.clone(), }; - let s = self.shift_bv(x, y, ext_bit); + let s = self.shift_bv_lit(x, y, ext_bit); let masked_s = self.ite(c, mask, &s); let mut bits = self.bitify("shift", &masked_s, (1 << y_w) + x_w - 1, false); bits.truncate(x_w); @@ -557,7 +557,7 @@ impl<'cfg> ToR1cs<'cfg> { (some_high_bit, shift_amt) } - fn embed_bv(&mut self, bv: Term) { + fn embed_bv_lit(&mut self, bv: Term) { //println!("Embed: {}", bv); //let bv2= bv.clone(); if let Sort::BitVector(n) = check(&bv) { @@ -822,7 +822,7 @@ impl<'cfg> ToR1cs<'cfg> { ); } - fn get_bv(&self, t: &Term) -> Rc> { + fn get_bv_lit(&self, t: &Term) -> Rc> { match self .cache .get(t) @@ -834,11 +834,11 @@ impl<'cfg> ToR1cs<'cfg> { } fn bv_has_bits(&self, t: &Term) -> bool { - !(*self.get_bv(t)).borrow().bits.is_empty() + !(*self.get_bv_lit(t)).borrow().bits.is_empty() } fn get_bv_uint(&mut self, t: &Term) -> TermLc { - let entry_rc = self.get_bv(t); + let entry_rc = self.get_bv_lit(t); let mut entry = entry_rc.borrow_mut(); if let Some(uint) = entry.uint.as_ref() { uint.clone() @@ -855,7 +855,7 @@ impl<'cfg> ToR1cs<'cfg> { } fn get_bv_bits(&mut self, t: &Term) -> Vec { - let entry_rc = self.get_bv(t); + let entry_rc = self.get_bv_lit(t); let mut entry = entry_rc.borrow_mut(); if entry.bits.is_empty() { entry.bits = self.bitify("getbits", entry.uint.as_ref().unwrap(), entry.width, false); @@ -1010,14 +1010,10 @@ pub mod test { use crate::ir::proof::Constraints; use crate::ir::term::dist::test::*; - use crate::ir::term::dist::*; use crate::target::r1cs::opt::reduce_linearities; use fxhash::FxHashMap; - use quickcheck::{Arbitrary, Gen}; use quickcheck_macros::quickcheck; - use rand::distributions::Distribution; - use rand::SeedableRng; fn to_r1cs_dflt(cs: Computation) -> (ProverData, VerifierData) { to_r1cs(cs, &CircCfg::default()) @@ -1058,36 +1054,6 @@ pub mod test { pd.r1cs.check_all(&extended_values); } - #[derive(Clone, Debug)] - pub struct PureBool(pub Term, pub FxHashMap); - - impl Arbitrary for PureBool { - fn arbitrary(g: &mut Gen) -> Self { - let mut rng = rand::rngs::StdRng::seed_from_u64(u64::arbitrary(g)); - let t = PureBoolDist(g.size()).sample(&mut rng); - let values: FxHashMap = PostOrderIter::new(t.clone()) - .filter_map(|c| { - if let Op::Var(n, _) = &c.op() { - Some((n.clone(), Value::Bool(bool::arbitrary(g)))) - } else { - None - } - }) - .collect(); - PureBool(t, values) - } - - fn shrink(&self) -> Box> { - let vs = self.1.clone(); - let ts = PostOrderIter::new(self.0.clone()) - .collect::>() - .into_iter() - .rev(); - - Box::new(ts.skip(1).map(move |t| PureBool(t, vs.clone()))) - } - } - #[quickcheck] fn random_pure_bool(PureBool(t, values): PureBool) { let t = if eval(&t, &values).as_bool() { @@ -1156,7 +1122,7 @@ pub mod test { .collect(); let cs = Computation::from_constraint_system_parts( - vec![term![Op::Not; term![Op::Eq; bv(0b10110, 8), + vec![term![Op::Not; term![Op::Eq; bv_lit(0b10110, 8), term![Op::BvUnOp(BvUnOp::Neg); leaf_term(Op::Var("b".to_owned(), Sort::BitVector(8)))]]]], vec![leaf_term(Op::Var("b".to_owned(), Sort::BitVector(8)))], ); @@ -1185,14 +1151,6 @@ pub mod test { r1cs2.check_all(&extended_values); } - /// A bit-vector literal with value `u` and size `w` - pub fn bv(u: usize, w: usize) -> Term { - leaf_term(Op::Const(Value::BitVector(BitVector::new( - Integer::from(u), - w, - )))) - } - fn pf_dflt(i: isize) -> Term { leaf_term(Op::Const(Value::Field(CircCfg::default().field().new_v(i)))) } @@ -1211,43 +1169,43 @@ pub mod test { init(); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Udiv); bv(0b1111,4), bv(0b1111,4)], - bv(0b0001, 4) + term![Op::BvBinOp(BvBinOp::Udiv); bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b0001, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Udiv); bv(0b1111,4), bv(0b0001,4)], - bv(0b1111, 4) + term![Op::BvBinOp(BvBinOp::Udiv); bv_lit(0b1111,4), bv_lit(0b0001,4)], + bv_lit(0b1111, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Udiv); bv(0b0111,4), bv(0b0000,4)], - bv(0b1111, 4) + term![Op::BvBinOp(BvBinOp::Udiv); bv_lit(0b0111,4), bv_lit(0b0000,4)], + bv_lit(0b1111, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Udiv); bv(0b1111,4), bv(0b0010,4)], - bv(0b0111, 4) + term![Op::BvBinOp(BvBinOp::Udiv); bv_lit(0b1111,4), bv_lit(0b0010,4)], + bv_lit(0b0111, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Urem); bv(0b1111,4), bv(0b1111,4)], - bv(0b0000, 4) + term![Op::BvBinOp(BvBinOp::Urem); bv_lit(0b1111,4), bv_lit(0b1111,4)], + bv_lit(0b0000, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Urem); bv(0b1111,4), bv(0b0001,4)], - bv(0b0000, 4) + term![Op::BvBinOp(BvBinOp::Urem); bv_lit(0b1111,4), bv_lit(0b0001,4)], + bv_lit(0b0000, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Urem); bv(0b0111,4), bv(0b0000,4)], - bv(0b0111, 4) + term![Op::BvBinOp(BvBinOp::Urem); bv_lit(0b0111,4), bv_lit(0b0000,4)], + bv_lit(0b0111, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Urem); bv(0b1111,4), bv(0b0010,4)], - bv(0b0001, 4) + term![Op::BvBinOp(BvBinOp::Urem); bv_lit(0b1111,4), bv_lit(0b0010,4)], + bv_lit(0b0001, 4) ]); } @@ -1256,52 +1214,52 @@ pub mod test { init(); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Shl); bv(0b1111,4), bv(0b0011,4)], - bv(0b1000, 4) + term![Op::BvBinOp(BvBinOp::Shl); bv_lit(0b1111,4), bv_lit(0b0011,4)], + bv_lit(0b1000, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Shl); bv(0b1101,4), bv(0b0010,4)], - bv(0b0100, 4) + term![Op::BvBinOp(BvBinOp::Shl); bv_lit(0b1101,4), bv_lit(0b0010,4)], + bv_lit(0b0100, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Ashr); bv(0b1111,4), bv(0b0011,4)], - bv(0b1111, 4) + term![Op::BvBinOp(BvBinOp::Ashr); bv_lit(0b1111,4), bv_lit(0b0011,4)], + bv_lit(0b1111, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Ashr); bv(0b0111,4), bv(0b0010,4)], - bv(0b0001, 4) + term![Op::BvBinOp(BvBinOp::Ashr); bv_lit(0b0111,4), bv_lit(0b0010,4)], + bv_lit(0b0001, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Lshr); bv(0b0111,4), bv(0b0010,4)], - bv(0b0001, 4) + term![Op::BvBinOp(BvBinOp::Lshr); bv_lit(0b0111,4), bv_lit(0b0010,4)], + bv_lit(0b0001, 4) ]); const_test(term![ Op::Eq; - term![Op::BvBinOp(BvBinOp::Lshr); bv(0b1111,4), bv(0b0011,4)], - bv(0b0001, 4) + term![Op::BvBinOp(BvBinOp::Lshr); bv_lit(0b1111,4), bv_lit(0b0011,4)], + bv_lit(0b0001, 4) ]); } #[test] - fn pf2bv() { + fn pf2bv_lit() { const_test(term![ Op::Eq; term![Op::PfToBv(4); pf_dflt(8)], - bv(0b1000, 4) + bv_lit(0b1000, 4) ]); const_test(term![ Op::Eq; term![Op::PfToBv(4); pf_dflt(15)], - bv(0b1111, 4) + bv_lit(0b1111, 4) ]); const_test(term![ Op::Eq; term![Op::PfToBv(8); pf_dflt(15)], - bv(0b1111, 8) + bv_lit(0b1111, 8) ]); } diff --git a/util.py b/util.py index 42cf3851..bbd70851 100644 --- a/util.py +++ b/util.py @@ -4,8 +4,8 @@ from os import path # Gloable variables feature_path = ".features.txt" mode_path = ".mode.txt" -valid_features = {"aby", "c", "lp", "r1cs", "smt", "zok", "datalog"} -cargo_features = {"c", "lp", "r1cs", "smt", "zok", "ristretto255", "datalog"} +valid_features = {"aby", "c", "lp", "r1cs", "smt", "zok", "datalog", "bellman", "spartan"} +cargo_features = {"aby", "c", "lp", "r1cs", "smt", "zok", "datalog", "bellman", "spartan"} # Environment variables ABY_SOURCE="./../ABY"