github/circ
1
1
Fork 0
mirror of https://github.com/circify/circ.git synced 2026-01-10 06:08:02 -05:00
Code Issues Packages Projects Releases Wiki Activity

Configuration system. Kill DFL_T (#127)

Browse Source 
* Configuration system. Kill DFL_T

* add circ::cfg::CircCfg that holds cfg info
   * it's constructible from circ_opt::CircOpt
      * implements clap::Args, so you can set it from your compiler's
        CLI/envvars
      * defined in external crate to keep clap out of our main build
      * organized by circ module, but not feature gated
         *  no point: the build wouldn't meaningfully change
      * includes a way to set the default field
* added circ::cfg::set and circ::cfg::cfg
   * also circ::cfg::set_default and circ::cfg::set_cfg
   * access a sync::once_cell, static configuration
* killed DFL_T

* workflows
   * unit-tested component probably need to not read circ::cfg::cfg.
   * compilers need to call circ::cfg::set or circ::cfg::set_default.

* rm dead features
This commit is contained in:
Alex Ozdemir
2022-12-25 20:53:27 -08:00
committed by GitHub
parent 05b793d565
commit be8741c615
29 changed files with 2060 additions and 505 deletions
Download Patch File Download Diff File Expand all files Collapse all files

102
examples/circ.rs
View File

@@ -9,6 +9,11 @@ use bellman::groth16::{
#[cfg(feature = "r1cs")]
use bellman::Circuit;
use bls12_381::{Bls12, Scalar};
use circ::cfg::{
cfg,
clap::{self, Args, Parser, Subcommand, ValueEnum},
CircOpt,
};
#[cfg(feature = "c")]
use circ::front::c::{self, C};
use circ::front::datalog::{self, Datalog};
@@ -35,7 +40,6 @@ use circ::target::r1cs::spartan::write_data;
use circ::target::r1cs::trans::to_r1cs;
#[cfg(feature = "smt")]
use circ::target::smt::find_model;
use circ::util::field::DFL_T;
use circ_fields::FieldT;
use fxhash::FxHashMap as HashMap;
#[cfg(feature = "lp")]
@@ -44,87 +48,69 @@ use std::fs::File;
use std::io::Read;
use std::io::Write;
use std::path::{Path, PathBuf};
use structopt::clap::arg_enum;
use structopt::StructOpt;
#[derive(Debug, StructOpt)]
#[structopt(name = "circ", about = "CirC: the circuit compiler")]
#[derive(Debug, Parser)]
#[command(name = "circ", about = "CirC: the circuit compiler")]
struct Options {
/// Input file
#[structopt(parse(from_os_str), name = "PATH")]
#[arg(name = "PATH")]
path: PathBuf,
#[structopt(flatten)]
#[command(flatten)]
frontend: FrontendOptions,
#[command(flatten)]
circ: CircOpt,
/// Number of parties for an MPC.
#[structopt(long, default_value = "2", name = "PARTIES")]
#[arg(long, default_value = "2", name = "PARTIES")]
parties: u8,
#[structopt(subcommand)]
backend: Backend,
}
#[derive(Debug, StructOpt)]
#[derive(Debug, Args)]
struct FrontendOptions {
/// Input language
#[structopt(long, default_value = "auto", name = "LANG")]
#[arg(long, default_value = "auto", name = "LANG")]
language: Language,
/// Value threshold
#[structopt(long)]
#[arg(long)]
value_threshold: Option<u64>,
/// How many recursions to allow (datalog)
#[structopt(short, long, name = "N", default_value = "5")]
rec_limit: usize,
/// Lint recursions that are allegedly primitive recursive (datalog)
#[structopt(long)]
lint_prim_rec: bool,
#[cfg(feature = "zok")]
/// In Z#, "isolate" assertions. That is, assertions in if/then/else expressions only take
/// effect if that branch is active.
///
/// See `--branch-isolation` in
/// [ZoKrates](https://zokrates.github.io/language/control_flow.html).
#[structopt(long)]
z_isolate_asserts: bool,
}
#[derive(Debug, StructOpt)]
#[derive(Debug, Subcommand)]
enum Backend {
#[allow(dead_code)]
R1cs {
#[structopt(long, default_value = "P", parse(from_os_str))]
#[arg(long, default_value = "P")]
prover_key: PathBuf,
#[structopt(long, default_value = "V", parse(from_os_str))]
#[arg(long, default_value = "V")]
verifier_key: PathBuf,
#[structopt(long, default_value = "50")]
#[arg(long, default_value = "50")]
/// linear combination constraints up to this size will be eliminated
lc_elimination_thresh: usize,
#[structopt(long, default_value = "count")]
#[arg(long, default_value = "count")]
action: ProofAction,
},
Smt {},
Ilp {},
Mpc {
#[structopt(long, default_value = "hycc", name = "cost_model")]
#[arg(long, default_value = "hycc", name = "cost_model")]
cost_model: String,
#[structopt(long, default_value = "lp", name = "selection_scheme")]
#[arg(long, default_value = "lp", name = "selection_scheme")]
selection_scheme: String,
},
}
arg_enum! {
#[derive(PartialEq, Eq, Debug)]
enum Language {
Zsharp,
Datalog,
C,
Auto,
}
#[derive(PartialEq, Eq, Debug, Clone, ValueEnum)]
enum Language {
Zsharp,
Datalog,
C,
Auto,
}
#[derive(PartialEq, Eq, Debug)]
@@ -140,13 +126,11 @@ pub enum CostModelType {
Hycc,
}
arg_enum! {
#[derive(PartialEq, Eq, Debug)]
enum ProofAction {
Count,
Setup,
SpartanSetup,
}
#[derive(PartialEq, Eq, Debug, Clone, ValueEnum)]
enum ProofAction {
Count,
Setup,
SpartanSetup,
}
fn determine_language(l: &Language, input_path: &Path) -> DeterminedLanguage {
@@ -175,7 +159,8 @@ fn main() {
.format_level(false)
.format_timestamp(None)
.init();
let options = Options::from_args();
let options = Options::parse();
circ::cfg::set(&options.circ);
let path_buf = options.path.clone();
println!("{:?}", options);
let mode = match options.backend {
@@ -194,7 +179,6 @@ fn main() {
let inputs = zsharp::Inputs {
file: options.path,
mode,
isolate_asserts: options.frontend.z_isolate_asserts,
};
ZSharpFE::gen(inputs)
}
@@ -203,11 +187,7 @@ fn main() {
panic!("Missing feature: smt,zok");
}
DeterminedLanguage::Datalog => {
let inputs = datalog::Inputs {
file: options.path,
rec_limit: options.frontend.rec_limit,
lint_prim_rec: options.frontend.lint_prim_rec,
};
let inputs = datalog::Inputs { file: options.path };
Datalog::gen(inputs)
}
#[cfg(feature = "c")]
@@ -285,15 +265,13 @@ fn main() {
action,
prover_key,
verifier_key,
lc_elimination_thresh,
..
} => {
println!("Converting to r1cs");
let (r1cs, mut prover_data, verifier_data) =
to_r1cs(cs.get("main").clone(), FieldT::from(DFL_T.modulus()));
let (r1cs, mut prover_data, verifier_data) = to_r1cs(cs.get("main").clone(), cfg());
println!("Pre-opt R1cs size: {}", r1cs.constraints().len());
let r1cs = reduce_linearities(r1cs, Some(lc_elimination_thresh));
let r1cs = reduce_linearities(r1cs, cfg());
println!("Final R1cs size: {}", r1cs.constraints().len());
// save the optimized r1cs: the prover needs it to synthesize.
@@ -363,7 +341,7 @@ fn main() {
}
#[cfg(feature = "smt")]
Backend::Smt { .. } => {
if options.frontend.lint_prim_rec {
if options.circ.datalog.lint_prim_rec {
let main_comp = cs.get("main").clone();
assert_eq!(main_comp.outputs.len(), 1);
match find_model(&main_comp.outputs[0]) {

10
examples/opa_bench.rs
View File

@@ -1,16 +1,16 @@
use circ::cfg::clap::{self, Parser};
use circ::ir::term::*;
use circ::target::aby::assignment::ilp;
use circ::term;
use structopt::StructOpt;
#[derive(Debug, StructOpt)]
#[structopt(
#[derive(Debug, Parser)]
#[command(
name = "opa_bench",
about = "Optimal Protocol Assignment via ILP benchmarker"
)]
struct Options {
/// Number of parties for an MPC. If missing, generates a proof circuit.
#[structopt(name = "MULTS")]
#[arg(name = "MULTS")]
n_mults: u32,
}
@@ -19,7 +19,7 @@ fn main() {
.format_level(false)
.format_timestamp(None)
.init();
let options = Options::from_args();
let options = Options::parse();
let v = leaf_term(Op::Var("a".to_owned(), Sort::BitVector(32)));
let mut t = v.clone();
for _i in 0..options.n_mults {

39
examples/zk.rs
View File

@@ -1,39 +1,36 @@
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;
use structopt::clap::arg_enum;
use structopt::StructOpt;
#[derive(Debug, StructOpt)]
#[structopt(name = "circ", about = "CirC: the circuit compiler")]
#[derive(Debug, Parser)]
#[command(name = "zk", about = "The CirC ZKP runner")]
struct Options {
#[structopt(long, default_value = "P", parse(from_os_str))]
#[arg(long, default_value = "P")]
prover_key: PathBuf,
#[structopt(long, default_value = "V", parse(from_os_str))]
#[arg(long, default_value = "V")]
verifier_key: PathBuf,
#[structopt(long, default_value = "pi", parse(from_os_str))]
#[arg(long, default_value = "pi")]
proof: PathBuf,
#[structopt(long, default_value = "in", parse(from_os_str))]
#[arg(long, default_value = "in")]
inputs: PathBuf,
#[structopt(long, default_value = "pin", parse(from_os_str))]
#[arg(long, default_value = "pin")]
pin: PathBuf,
#[structopt(long, default_value = "vin", parse(from_os_str))]
#[arg(long, default_value = "vin")]
vin: PathBuf,
#[structopt(long)]
#[arg(long)]
action: ProofAction,
}
arg_enum! {
#[derive(PartialEq, Debug)]
/// `Prove`/`Verify` execute proving/verifying in bellman separately
/// `Spartan` executes both proving/verifying in spartan
enum ProofAction {
Prove,
Verify,
Spartan,
}
#[derive(PartialEq, Debug, Clone, ValueEnum)]
/// `Prove`/`Verify` execute proving/verifying in bellman separately
/// `Spartan` executes both proving/verifying in spartan
enum ProofAction {
Prove,
Verify,
Spartan,
}
fn main() {
@@ -41,7 +38,7 @@ fn main() {
.format_level(false)
.format_timestamp(None)
.init();
let opts = Options::from_args();
let opts = Options::parse();
match opts.action {
ProofAction::Prove => {
let input_map = parse_value_map(&std::fs::read(opts.inputs).unwrap());

67
examples/zxc.rs
View File

@@ -10,74 +10,71 @@ use bls12_381::{Bls12, Scalar};
use circ::front::zsharp::{self, ZSharpFE};
use circ::front::{FrontEnd, Mode};
use circ::ir::opt::{opt, Opt};
use circ_fields::FieldT;
/*
use circ::target::r1cs::bellman::parse_instance;
*/
use circ::target::r1cs::opt::reduce_linearities;
use circ::target::r1cs::trans::to_r1cs;
use circ::util::field::DFL_T;
/*
use std::fs::File;
use std::io::Read;
use std::io::Write;
*/
use circ::cfg::{
cfg,
clap::{self, Parser, ValueEnum},
CircOpt,
};
use std::path::PathBuf;
use structopt::clap::arg_enum;
use structopt::StructOpt;
#[derive(Debug, StructOpt)]
#[structopt(name = "zxc", about = "CirC: the circuit compiler")]
#[derive(Debug, Parser)]
#[command(name = "zxc", about = "CirC: the circuit compiler")]
struct Options {
/// Input file
#[structopt(parse(from_os_str), name = "PATH")]
#[arg(name = "PATH")]
path: PathBuf,
/*
#[structopt(long, default_value = "P", parse(from_os_str))]
#[arg(long, default_value = "P", parse(from_os_str))]
prover_key: PathBuf,
#[structopt(long, default_value = "V", parse(from_os_str))]
#[arg(long, default_value = "V", parse(from_os_str))]
verifier_key: PathBuf,
#[structopt(long, default_value = "pi", parse(from_os_str))]
#[arg(long, default_value = "pi", parse(from_os_str))]
proof: PathBuf,
#[structopt(long, default_value = "x", parse(from_os_str))]
#[arg(long, default_value = "x", parse(from_os_str))]
instance: PathBuf,
*/
#[structopt(short = "L")]
#[arg(short = 'L')]
/// skip linearity reduction entirely
skip_linred: bool,
#[structopt(long, default_value = "50")]
/// linear combination constraints up to this size will be eliminated (if the pass is enabled)
lc_elimination_thresh: usize,
#[command(flatten)]
/// CirC options
circ: CircOpt,
#[structopt(long, default_value = "count")]
#[arg(long, default_value = "count")]
action: ProofAction,
#[structopt(short = "q")]
#[arg(short = 'q')]
/// quiet mode: don't print R1CS at the end
quiet: bool,
}
arg_enum! {
#[derive(PartialEq, Debug)]
enum ProofAction {
Count,
Prove,
Setup,
Verify,
}
#[derive(PartialEq, Eq, Debug, Clone, ValueEnum)]
enum ProofAction {
Count,
Setup,
Prove,
Verify,
}
arg_enum! {
#[derive(PartialEq, Debug)]
enum ProofOption {
Count,
Prove,
}
#[derive(PartialEq, Debug, Clone, ValueEnum)]
enum ProofOption {
Count,
Prove,
}
fn main() {
@@ -85,14 +82,14 @@ fn main() {
.format_level(false)
.format_timestamp(None)
.init();
let options = Options::from_args();
let options = Options::parse();
circ::cfg::set(&options.circ);
println!("{:?}", options);
let cs = {
let inputs = zsharp::Inputs {
file: options.path,
mode: Mode::Proof,
isolate_asserts: false,
};
ZSharpFE::gen(inputs)
};
@@ -132,7 +129,7 @@ fn main() {
*/
println!("Converting to r1cs");
let (r1cs, _, _) = to_r1cs(cs.get("main").clone(), FieldT::from(DFL_T.modulus()));
let (r1cs, _, _) = to_r1cs(cs.get("main").clone(), cfg());
let r1cs = if options.skip_linred {
println!("Skipping linearity reduction, as requested.");
r1cs
@@ -141,7 +138,7 @@ fn main() {
"R1cs size before linearity reduction: {}",
r1cs.constraints().len()
);
reduce_linearities(r1cs, Some(options.lc_elimination_thresh))
reduce_linearities(r1cs, cfg())
};
println!("Final R1cs size: {}", r1cs.constraints().len());
match action {

36
examples/zxi.rs
View File

@@ -1,23 +1,22 @@
use circ::front::zsharp::{Inputs, ZSharpFE};
use circ::cfg::{
clap::{self, Parser},
CircOpt,
};
use circ::front::Mode;
use std::path::PathBuf;
use structopt::StructOpt;
#[derive(Debug, StructOpt)]
#[structopt(name = "circ", about = "CirC: the circuit compiler")]
#[derive(Debug, Parser)]
#[command(name = "zxi", about = "The Z# interpreter")]
struct Options {
/// Input file
#[structopt(parse(from_os_str))]
#[arg()]
zsharp_path: PathBuf,
/// Number of parties for an MPC. If missing, generates a proof circuit.
#[structopt(short, long, name = "PARTIES")]
parties: Option<u8>,
/// Whether to maximize the output
#[structopt(short, long)]
maximize: bool,
#[command(flatten)]
/// CirC options
circ: CircOpt,
}
fn main() {
@@ -25,20 +24,11 @@ fn main() {
.format_level(false)
.format_timestamp(None)
.init();
let options = Options::from_args();
//println!("{:?}", options);
let mode = if options.maximize {
Mode::Opt
} else {
match options.parties {
Some(p) => Mode::Mpc(p),
None => Mode::Proof,
}
};
let options = Options::parse();
circ::cfg::set(&options.circ);
let inputs = Inputs {
file: options.zsharp_path,
mode,
isolate_asserts: false,
mode: Mode::Proof,
};
let cs = ZSharpFE::interpret(inputs);
cs.pretty(&mut std::io::stdout().lock())