diff --git a/src/error.rs b/src/error.rs index 5a3184e..cc91b8f 100644 --- a/src/error.rs +++ b/src/error.rs @@ -80,6 +80,12 @@ pub enum Error { // general error from backend BackendError { e: String }, + // The user did not provide an assignment for a variable during proving + MissingVariableAssignment { var_name: String }, + + // A variable assignment has an invalid value + InvalidVariableAssignmentValue { var_name: String }, + // proof fails to verify ProofVerificationFailure, @@ -193,7 +199,17 @@ impl std::fmt::Display for Error { // invalid field at repl Self::InvalidField => write!(f, "Invalid field value"), - Error::ParseError { e } => write!(f, "Error while parsing file: {e}"), + + Self::ParseError { e } => write!(f, "Error while parsing file: {e}"), + + Self::MissingVariableAssignment { var_name } => { + write!(f, "Missing assignment for variable: {var_name}") + } + + Self::InvalidVariableAssignmentValue { var_name } => write!( + f, + "The assignment for variable: {var_name} has an invalid value" + ), } } } diff --git a/src/halo2/api.rs b/src/halo2/api.rs index d3bbd95..b37e935 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -1,18 +1,28 @@ -use crate::ast::Module; +use crate::ast::{Module, VariableId}; use crate::error::Error; -use crate::error::Error::ParseError; -use crate::halo2::synth::{Halo2Module, PrimeFieldOps}; +use crate::error::Error::{ + BackendError, MissingVariableAssignment, ParseError, ProofVerificationFailure, +}; +use crate::halo2::synth::{keygen, prover, Halo2Module, PrimeFieldOps}; +use crate::halo2::synth::{make_constant, verifier}; use crate::qprintln; -use crate::util::Config; +use crate::util::{get_circuit_assignments, Config}; +use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; +use ark_serialize::{Read, SerializationError}; use bincode::error::{DecodeError, EncodeError}; +use ff::PrimeField; use halo2_proofs::pasta::{EqAffine, Fp}; +use halo2_proofs::plonk::{keygen_vk, VerifyingKey}; use halo2_proofs::poly::commitment::Params; +use num_bigint::BigInt; +use std::collections::HashMap; +use std::io::Write; use std::rc::Rc; pub fn compile(source: impl AsRef, config: &Config) -> Result { qprintln!(config, "* Compiling constraints..."); let module = Module::parse(source.as_ref()).map_err(|err| ParseError { e: err.to_string() })?; - let module_3ac = crate::transform::compile(module, &PrimeFieldOps::::default(), &config); + let module_3ac = crate::transform::compile(module, &PrimeFieldOps::::default(), config); qprintln!(config, "* Synthesizing arithmetic circuit..."); let module_rc = Rc::new(module_3ac); let circuit = Halo2Module::::new(module_rc); @@ -20,12 +30,158 @@ pub fn compile(source: impl AsRef, config: &Config) -> Result, Fp>, + config: &Config, +) -> Result { + let module = circuit_data.circuit.module.as_ref(); + let named_string_assignments: HashMap = named_assignments + .iter() + .map(|(key, value)| (key.as_ref().to_string(), *value)) + .collect(); + let assignments = get_circuit_assignments(module, &named_string_assignments)?; + let proof_data_cli = prove_from_variable_assignments(circuit_data, &assignments, config)?; + let public_fields: Vec = module + .pubs + .clone() + .into_iter() + .filter_map(|v| v.name) + .collect(); + let verifying_key = keygen_vk(&circuit_data.params, &circuit_data.circuit)?; + Ok(ProofDataHalo2 { + proof: proof_data_cli.proof, + verifying_key, + public_fields, + params: circuit_data.params.clone(), + }) +} + +pub fn verify( + proof_data: &ProofDataHalo2, + named_public_assignments: &HashMap, Fp>, + _config: &Config, +) -> Result<(), Error> { + let params = &proof_data.params; + let named_public_string_assignments: HashMap = named_public_assignments + .iter() + .map(|(key, value)| (key.as_ref().to_string(), *value)) + .collect(); + let public_input = public_inputs_from_assignments( + &proof_data.public_fields, + &named_public_string_assignments, + )?; + verifier( + params, + &proof_data.verifying_key, + &proof_data.proof, + public_input.as_slice(), + ) + .map_err(|_| ProofVerificationFailure) +} + +fn public_inputs_from_variable_assignments( + module: &Module, + public_assignments: &HashMap, +) -> Vec { + module + .pubs + .iter() + .map(|inst| public_assignments[&inst.id]) + .collect::>() +} + +fn public_inputs_from_assignments( + public_fields: &[String], + assignments: &HashMap, +) -> Result, Error> { + public_fields + .iter() + .map(|s| { + assignments + .get(s) + .cloned() + .ok_or_else(|| MissingVariableAssignment { + var_name: s.to_string(), + }) + }) + .collect() +} + +pub(crate) fn prove_from_int_variable_assignments( + circuit_data: &HaloCircuitData, + int_assignments: &HashMap, + config: &Config, +) -> Result { + let assignments: HashMap = int_assignments + .iter() + .map(|(id, f)| (*id, make_constant::(f.clone()))) + .collect(); + prove_from_variable_assignments(circuit_data, &assignments, config) +} + +pub(crate) fn prove_from_variable_assignments( + circuit_data: &HaloCircuitData, + assignments: &HashMap, + config: &Config, +) -> Result { + let params = &circuit_data.params; + let module = circuit_data.circuit.module.as_ref(); + + // Populate variable definitions + let mut circuit = circuit_data.circuit.clone(); + circuit.populate_variables(assignments.clone()); + + // Get public inputs Fp + let binding = public_inputs_from_variable_assignments(module, assignments); + let instances = binding.as_slice(); + + let public_inputs: Vec = instances + .iter() + .flat_map(|fp| { + let repr = fp.to_repr(); + repr.as_ref().to_vec() + }) + .collect(); + + // Generating proving key + qprintln!(config, "* Generating proving key..."); + let (pk, _vk) = keygen(&circuit, params)?; + + // Start proving witnesses + qprintln!(config, "* Proving knowledge of witnesses..."); + let proof = prover(circuit.clone(), params, &pk, instances) + .map_err(|e| BackendError { e: e.to_string() })?; + Ok(ProofDataCliHalo2 { + proof, + public_inputs, + }) +} + /* Captures all the data required to use a Halo2 circuit. */ pub struct HaloCircuitData { pub params: Params, pub circuit: Halo2Module, } +pub struct VerifyingKeyDataHalo2 { + pub verifying_key: VerifyingKey, + pub params: Params, +} + +pub struct ProofDataHalo2 { + pub proof: Vec, + pub verifying_key: VerifyingKey, + pub public_fields: Vec, + pub params: Params, +} + +#[derive(CanonicalSerialize, CanonicalDeserialize)] +pub(crate) struct ProofDataCliHalo2 { + pub(crate) proof: Vec, + pub(crate) public_inputs: Vec, +} + impl HaloCircuitData { pub fn read(mut reader: R) -> Result where @@ -71,6 +227,90 @@ mod tests { #[ignore] // This test panics in type checking fn test_compile_type_error() { let config = Config { quiet: true }; - assert!(compile("1/0 = 1;", &config).is_err()); + assert!(compile("(1, 2) = 1;", &config).is_err()); + } + + #[test] + fn test_prove_valid() { + let config = Config { quiet: true }; + let circuit = compile("x = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::one())]); + assert!(prove(&circuit, &assignments, &config).is_ok()); + } + + #[test] + fn test_prove_missing_assignment() { + let config = Config { quiet: true }; + let circuit = compile("x = 1;", &config).unwrap(); + let assignments: HashMap = HashMap::new(); + assert!(prove(&circuit, &assignments, &config).is_err()); + } + + #[test] + fn test_prove_invalid_assignment() { + let config = Config { quiet: true }; + let circuit = compile("x = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::zero())]); + assert!(prove(&circuit, &assignments, &config).is_ok()); + } + + #[test] + fn test_verify_valid_no_public() { + let config = Config { quiet: true }; + let circuit = compile("x = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::one())]); + let proof_data = prove(&circuit, &assignments, &config).unwrap(); + assert!(verify(&proof_data, &assignments, &config).is_ok()); + } + + #[test] + fn test_verify_valid_with_public() { + let config = Config { quiet: true }; + let circuit = compile("pub x; pub y; x + y + z = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::one()), ("y", Fp::zero()), ("z", Fp::zero())]); + let public_assignments = HashMap::from([("x", Fp::one()), ("y", Fp::zero())]); + let proof_data = prove(&circuit, &assignments, &config).unwrap(); + assert!(verify(&proof_data, &public_assignments, &config).is_ok()); + } + + #[test] + fn test_verify_invalid_input_no_public() { + let config = Config { quiet: true }; + let circuit = compile("x = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::zero())]); + let public_assignments: HashMap = HashMap::new(); + let proof_data = prove(&circuit, &assignments, &config).unwrap(); + assert!(verify(&proof_data, &public_assignments, &config).is_err()); + } + + #[test] + fn test_verify_valid_input_invalid_public_input() { + let config = Config { quiet: true }; + let circuit = compile("pub x; x = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::one())]); + let public_assignments = HashMap::from([("x", Fp::zero())]); + let proof_data = prove(&circuit, &assignments, &config).unwrap(); + assert!(verify(&proof_data, &public_assignments, &config).is_err()); + } + + #[test] + fn test_verify_valid_input_missing_public_input() { + let config = Config { quiet: true }; + let circuit = compile("pub x; x = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::one())]); + let public_assignments: HashMap = HashMap::new(); + let proof_data = prove(&circuit, &assignments, &config).unwrap(); + assert!(verify(&proof_data, &public_assignments, &config).is_err()); + } + + #[test] + fn test_verify_valid_with_public_and_corrupt_proof_data() { + let config = Config { quiet: true }; + let circuit = compile("pub x; pub y; x + y + z = 1;", &config).unwrap(); + let assignments = HashMap::from([("x", Fp::one()), ("y", Fp::zero()), ("z", Fp::zero())]); + let public_assignments = HashMap::from([("x", Fp::one()), ("y", Fp::zero())]); + let mut proof_data = prove(&circuit, &assignments, &config).unwrap(); + proof_data.public_fields = vec![]; + assert!(verify(&proof_data, &public_assignments, &config).is_err()); } } diff --git a/src/halo2/cli.rs b/src/halo2/cli.rs index 67168ab..9f4eb62 100644 --- a/src/halo2/cli.rs +++ b/src/halo2/cli.rs @@ -1,22 +1,24 @@ use crate::error::Error; -use crate::halo2::synth::{keygen, make_constant, prover, verifier}; +use crate::halo2::api::{prove_from_int_variable_assignments, ProofDataCliHalo2}; +use crate::halo2::synth::verifier; + use crate::qprintln; -use crate::util::{prompt_inputs, read_inputs_from_file, Config}; +use crate::util::{get_circuit_assignments, prompt_inputs, read_inputs_from_file, Config}; use halo2_proofs::plonk::keygen_vk; use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; -use ark_serialize::{Read, SerializationError}; -use std::io::Write; use clap::{Args, Subcommand}; use crate::halo2::api::HaloCircuitData; use ff::PrimeField; use halo2_proofs::pasta::Fp; +use num_bigint::BigInt; use std::collections::HashMap; use std::fs; use std::fs::File; +use std::ops::Deref; use std::path::PathBuf; #[derive(Subcommand)] @@ -69,7 +71,7 @@ fn compile_halo2_cmd( config: &Config, ) -> Result<(), Error> { let source = fs::read_to_string(source).expect("cannot read file"); - let halo_circuit_data = crate::halo2::api::compile(source, &config)?; + let halo_circuit_data = crate::halo2::api::compile(source, config)?; let mut circuit_file = File::create(output).expect("unable to create circuit file"); halo_circuit_data.write(&mut circuit_file).unwrap(); @@ -78,6 +80,22 @@ fn compile_halo2_cmd( Ok(()) } +fn prove_from_file( + path_to_inputs: &PathBuf, + circuit_data: &HaloCircuitData, + config: &Config, +) -> Result { + qprintln!( + config, + "* Reading inputs from file {}...", + path_to_inputs.to_string_lossy() + ); + let raw_inputs: HashMap = read_inputs_from_file(path_to_inputs).unwrap(); + let inputs = + get_circuit_assignments::(circuit_data.circuit.module.deref(), &raw_inputs)?; + prove_from_int_variable_assignments(circuit_data, &inputs, config) +} + /* Implements the subcommand that creates a proof from interactively entered * inputs. */ fn prove_halo2_cmd( @@ -94,79 +112,28 @@ fn prove_halo2_cmd( let mut expected_path_to_inputs = circuit.clone(); expected_path_to_inputs.set_extension("inputs"); - let HaloCircuitData { - params, - mut circuit, - } = HaloCircuitData::read(&mut circuit_file).unwrap(); - - // Prompt for program inputs - let var_assignments_ints = match inputs { - Some(path_to_inputs) => { - qprintln!( - config, - "* Reading inputs from file {}...", - path_to_inputs.to_string_lossy() - ); - read_inputs_from_file(&circuit.module, path_to_inputs) - } + let circuit_data = HaloCircuitData::read(&mut circuit_file).unwrap(); + + // Start proving witnesses + qprintln!(config, "* Proving knowledge of witnesses..."); + let proof_data = match inputs { + Some(path_to_inputs) => prove_from_file(path_to_inputs, &circuit_data, config), None => { if expected_path_to_inputs.exists() { - qprintln!( - config, - "* Reading inputs from file {}...", - expected_path_to_inputs.to_string_lossy() - ); - read_inputs_from_file(&circuit.module, &expected_path_to_inputs) + prove_from_file(&expected_path_to_inputs, &circuit_data, config) } else { qprintln!(config, "* Soliciting circuit witnesses..."); - prompt_inputs(&circuit.module) + let inputs = prompt_inputs(&circuit_data.circuit.module); + prove_from_int_variable_assignments(&circuit_data, &inputs, config) } } - }; - - let mut var_assignments = HashMap::new(); - for (k, v) in var_assignments_ints { - var_assignments.insert(k, make_constant(v)); - } - - // Populate variable definitions - circuit.populate_variables(var_assignments.clone()); - - // Get public inputs Fp - let binding = circuit - .module - .pubs - .iter() - .map(|inst| var_assignments[&inst.id]) - .collect::>(); - let instances = binding.as_slice(); - - // Generating proving key - qprintln!(config, "* Generating proving key..."); - let (pk, _vk) = keygen(&circuit, ¶ms)?; - - // Start proving witnesses - qprintln!(config, "* Proving knowledge of witnesses..."); - let proof = prover(circuit, ¶ms, &pk, instances)?; - - // Serilize Public Inputs - // Convert Vec to Vec - let public_inputs: Vec = instances - .iter() - .flat_map(|fp| { - let repr = fp.to_repr(); - repr.as_ref().to_vec() - }) - .collect(); + }?; qprintln!(config, "* Serializing proof to storage..."); let mut proof_file = File::create(output).expect("unable to create proof file"); - ProofDataHalo2 { - proof, - public_inputs, - } - .serialize(&mut proof_file) - .expect("Proof serialization failed"); + proof_data + .serialize(&mut proof_file) + .expect("Proof serialization failed"); qprintln!(config, "* Proof generation success!"); Ok(()) @@ -186,10 +153,10 @@ fn verify_halo2_cmd( qprintln!(config, "* Reading zero-knowledge proof..."); let mut proof_file = File::open(proof).expect("unable to load proof file"); - let ProofDataHalo2 { + let ProofDataCliHalo2 { proof, public_inputs, - } = ProofDataHalo2::deserialize(&mut proof_file).unwrap(); + } = ProofDataCliHalo2::deserialize(&mut proof_file).unwrap(); let instances_vec: Vec = public_inputs .chunks(32) @@ -215,12 +182,6 @@ fn verify_halo2_cmd( } } -#[derive(CanonicalSerialize, CanonicalDeserialize)] -struct ProofDataHalo2 { - proof: Vec, - public_inputs: Vec, -} - pub fn halo2(halo2_commands: &Halo2Commands, config: &Config) -> Result<(), Error> { match halo2_commands { Halo2Commands::Compile(args) => compile_halo2_cmd(args, config), diff --git a/src/plonk/cli.rs b/src/plonk/cli.rs index b7ed9f8..0de3533 100644 --- a/src/plonk/cli.rs +++ b/src/plonk/cli.rs @@ -1,9 +1,9 @@ -use crate::ast::Module; +use crate::ast::{Module, VariableId}; use crate::error::Error; use crate::plonk::synth::{make_constant, PlonkModule, PrimeFieldOps}; use crate::qprintln; use crate::transform::compile; -use crate::util::{prompt_inputs, read_inputs_from_file, Config}; +use crate::util::{get_circuit_assignments, prompt_inputs, read_inputs_from_file, Config}; use ark_bls12_381::{Bls12_381, Fr as BlsScalar}; use ark_ec::PairingEngine; @@ -23,10 +23,12 @@ use std::collections::HashMap; use std::fs; use std::fs::File; use std::io::Write; + use std::path::PathBuf; use std::rc::Rc; use clap::{Args, Subcommand}; +use num_bigint::BigInt; type PC = SonicKZG10>; type UniversalParams = Result, Error> { + qprintln!( + config, + "* Reading inputs from file {}...", + path_to_inputs.to_string_lossy() + ); + let raw_inputs: HashMap = read_inputs_from_file(path_to_inputs).unwrap(); + get_circuit_assignments::(circuit_module, &raw_inputs) +} + /* Implements the subcommand that creates a proof from interactively entered * inputs. */ fn prove_plonk_cmd( @@ -258,28 +274,16 @@ fn prove_plonk_cmd( // Prompt for program inputs let var_assignments_ints = match inputs { - Some(path_to_inputs) => { - qprintln!( - config, - "* Reading inputs from file {}...", - path_to_inputs.to_string_lossy() - ); - read_inputs_from_file(&circuit.module, path_to_inputs) - } + Some(path_to_inputs) => inputs_from_file(path_to_inputs, &circuit.module, config), None => { if expected_path_to_inputs.exists() { - qprintln!( - config, - "* Reading inputs from file {}...", - expected_path_to_inputs.to_string_lossy() - ); - read_inputs_from_file(&circuit.module, &expected_path_to_inputs) + inputs_from_file(&expected_path_to_inputs, &circuit.module, config) } else { qprintln!(config, "* Soliciting circuit witnesses..."); - prompt_inputs(&circuit.module) + Ok(prompt_inputs(&circuit.module)) } } - }; + }?; let mut var_assignments = HashMap::new(); for (k, v) in var_assignments_ints { diff --git a/src/transform.rs b/src/transform.rs index 49bd54e..2ba871f 100644 --- a/src/transform.rs +++ b/src/transform.rs @@ -903,10 +903,15 @@ fn collect_def_variables(def: &Definition, map: &mut HashMap) { +/* Collect all the public variables occurring in the given module. */ +pub fn collect_public_module_variables(module: &Module, map: &mut HashMap) { map.reserve(module.pubs.len()); map.extend(module.pubs.iter().map(|var| (var.id, var.clone()))); +} + +/* Collect all the variables occurring in the given module. */ +pub fn collect_module_variables(module: &Module, map: &mut HashMap) { + collect_public_module_variables(module, map); for def in &module.defs { collect_def_variables(def, map); diff --git a/src/util.rs b/src/util.rs index 1094bdf..92c341e 100644 --- a/src/util.rs +++ b/src/util.rs @@ -6,51 +6,74 @@ use std::{ }; use ark_serialize::Write; + use num_traits::Num; +use crate::ast::Variable; +use crate::error::Error; +use crate::error::Error::{InvalidVariableAssignmentValue, MissingVariableAssignment}; use crate::{ ast::{Module, Pat, VariableId}, transform::collect_module_variables, }; -/* Read satisfying inputs to the given program from a file. */ -pub fn read_inputs_from_file( - annotated: &Module, - path_to_inputs: &PathBuf, -) -> HashMap +/// Convert named circuit assignments to assignments of vamp-ir variableIds. +/// Useful for calling vamp-ir Halo2Module::populate_variable_assignments. +pub(crate) fn get_circuit_assignments( + module: &Module, + named_assignments: &HashMap, +) -> Result, Error> where - F: Num + Neg, - ::FromStrRadixErr: std::fmt::Debug, + T: Clone, { - let contents = fs::read_to_string(path_to_inputs).expect("Could not read inputs file"); - - // Read the user-supplied inputs from the file - let named_assignments: HashMap = - json5::from_str(&contents).expect("Could not parse JSON5"); - - // Get the expected inputs from the circuit module let mut input_variables = HashMap::new(); - collect_module_variables(annotated, &mut input_variables); - + collect_module_variables(module, &mut input_variables); // Defined variables should not be requested from user - for def in &annotated.defs { + for def in &module.defs { if let Pat::Variable(var) = &def.0 .0.v { input_variables.remove(&var.id); } } - let mut variable_assignments = HashMap::new(); + input_variables + .iter() + .filter_map(|(id, expected_var)| { + expected_var.name.as_deref().map(|var_name| { + named_assignments + .get(var_name) + .cloned() + .ok_or_else(|| MissingVariableAssignment { + var_name: var_name.to_string(), + }) + .map(|assignment| (*id, assignment)) + }) + }) + .collect() +} - // Check that the user supplied the expected inputs - for (id, expected_var) in input_variables { - variable_assignments.insert( - id, - parse_prefixed_num(&named_assignments[&expected_var.name.unwrap()].clone()) - .expect("input not an integer"), - ); - } +/* Read satisfying inputs to the given program from a file. */ +pub fn read_inputs_from_file(path_to_inputs: &PathBuf) -> Result, Error> +where + F: Clone + Num + Neg, + ::FromStrRadixErr: std::fmt::Debug, +{ + let contents = fs::read_to_string(path_to_inputs).expect("Could not read inputs file"); + + // Read the user-supplied inputs from the file + let named_assignments: HashMap = + json5::from_str(&contents).expect("Could not parse JSON5"); - variable_assignments + named_assignments + .into_iter() + .map(|(var_name, str_value)| { + let n = parse_prefixed_num::(&str_value).map_err(|_| { + InvalidVariableAssignmentValue { + var_name: var_name.clone(), + } + })?; + Ok((var_name, n)) + }) + .collect::, Error>>() } /* Prompt for satisfying inputs to the given program. */ @@ -73,10 +96,15 @@ where public_variables.insert(var.id); } - let mut var_assignments = HashMap::new(); + let named_input_variables: Vec<(VariableId, Variable)> = input_variables + .into_iter() + .filter(|(_id, var)| var.name.is_some()) + .collect(); + + let mut var_assignments: HashMap = HashMap::new(); // Solicit input variables from user and solve for choice point values - for (id, var) in input_variables { + for (id, var) in named_input_variables { let visibility = if public_variables.contains(&id) { "(public)" } else {