From 4570dd22a32ba52954ae2da48cee23689592f44c Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 13 Jul 2023 12:31:32 +0100 Subject: [PATCH 1/9] Add get_circuit_assignments This function converts named circuit assignments to assignments of vamp-ir variableIds. This will be used in the library proving API when the user supplies the variable assignemnts associated with a circuit. This new function returns an Error if a variable assignment is missing for the circuit or the value of an assignment is invalid. Previously the code would panic in these circumstances. --- src/error.rs | 13 +++++++- src/halo2/cli.rs | 4 +-- src/plonk/cli.rs | 4 +-- src/util.rs | 78 ++++++++++++++++++++++++++++++++---------------- 4 files changed, 69 insertions(+), 30 deletions(-) diff --git a/src/error.rs b/src/error.rs index 5a3184e..08ae3f8 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,12 @@ 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/cli.rs b/src/halo2/cli.rs index 67168ab..8ab62f0 100644 --- a/src/halo2/cli.rs +++ b/src/halo2/cli.rs @@ -107,7 +107,7 @@ fn prove_halo2_cmd( "* Reading inputs from file {}...", path_to_inputs.to_string_lossy() ); - read_inputs_from_file(&circuit.module, path_to_inputs) + read_inputs_from_file(&circuit.module, path_to_inputs).unwrap() } None => { if expected_path_to_inputs.exists() { @@ -116,7 +116,7 @@ fn prove_halo2_cmd( "* Reading inputs from file {}...", expected_path_to_inputs.to_string_lossy() ); - read_inputs_from_file(&circuit.module, &expected_path_to_inputs) + read_inputs_from_file(&circuit.module, &expected_path_to_inputs).unwrap() } else { qprintln!(config, "* Soliciting circuit witnesses..."); prompt_inputs(&circuit.module) diff --git a/src/plonk/cli.rs b/src/plonk/cli.rs index b7ed9f8..26628c9 100644 --- a/src/plonk/cli.rs +++ b/src/plonk/cli.rs @@ -264,7 +264,7 @@ fn prove_plonk_cmd( "* Reading inputs from file {}...", path_to_inputs.to_string_lossy() ); - read_inputs_from_file(&circuit.module, path_to_inputs) + read_inputs_from_file(&circuit.module, path_to_inputs).unwrap() } None => { if expected_path_to_inputs.exists() { @@ -273,7 +273,7 @@ fn prove_plonk_cmd( "* Reading inputs from file {}...", expected_path_to_inputs.to_string_lossy() ); - read_inputs_from_file(&circuit.module, &expected_path_to_inputs) + read_inputs_from_file(&circuit.module, &expected_path_to_inputs).unwrap() } else { qprintln!(config, "* Soliciting circuit witnesses..."); prompt_inputs(&circuit.module) diff --git a/src/util.rs b/src/util.rs index 1094bdf..32e0889 100644 --- a/src/util.rs +++ b/src/util.rs @@ -8,18 +8,55 @@ use std::{ use ark_serialize::Write; use num_traits::Num; +use crate::error::Error; +use crate::error::Error::{InvalidVariableAssignmentValue, MissingVariableAssignment}; use crate::{ ast::{Module, Pat, VariableId}, transform::collect_module_variables, }; +/// 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: Clone + Num + Neg, + ::FromStrRadixErr: std::fmt::Debug, +{ + let mut input_variables = HashMap::new(); + collect_module_variables(module, &mut input_variables); + // Defined variables should not be requested from user + for def in &module.defs { + if let Pat::Variable(var) = &def.0 .0.v { + input_variables.remove(&var.id); + } + } + + 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() +} + /* Read satisfying inputs to the given program from a file. */ pub fn read_inputs_from_file( annotated: &Module, path_to_inputs: &PathBuf, -) -> HashMap +) -> Result, Error> where - F: Num + Neg, + F: Clone + Num + Neg, ::FromStrRadixErr: std::fmt::Debug, { let contents = fs::read_to_string(path_to_inputs).expect("Could not read inputs file"); @@ -28,29 +65,20 @@ where 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); - - // Defined variables should not be requested from user - for def in &annotated.defs { - if let Pat::Variable(var) = &def.0 .0.v { - input_variables.remove(&var.id); - } - } - - let mut variable_assignments = HashMap::new(); - - // 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"), - ); - } - - variable_assignments + let fp_named_assignments: HashMap = 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.clone(), n)) + }, + ) + .collect::, Error>>()?; + get_circuit_assignments(annotated, &fp_named_assignments) } /* Prompt for satisfying inputs to the given program. */ From 14f8e8dbd6383112a2b7b1c1f7826c77ec7a133d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 13 Jul 2023 12:44:16 +0100 Subject: [PATCH 2/9] Fix formatting --- src/error.rs | 9 +++++++-- src/util.rs | 18 ++++++++---------- 2 files changed, 15 insertions(+), 12 deletions(-) diff --git a/src/error.rs b/src/error.rs index 08ae3f8..cc91b8f 100644 --- a/src/error.rs +++ b/src/error.rs @@ -202,9 +202,14 @@ impl std::fmt::Display for Error { Self::ParseError { e } => write!(f, "Error while parsing file: {e}"), - Self::MissingVariableAssignment { var_name } => write!(f, "Missing assignment for variable: {var_name}"), + 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") + Self::InvalidVariableAssignmentValue { var_name } => write!( + f, + "The assignment for variable: {var_name} has an invalid value" + ), } } } diff --git a/src/util.rs b/src/util.rs index 32e0889..38b1dfe 100644 --- a/src/util.rs +++ b/src/util.rs @@ -67,16 +67,14 @@ where let fp_named_assignments: HashMap = 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.clone(), n)) - }, - ) + .map(|(var_name, str_value)| { + let n = parse_prefixed_num::(&str_value).map_err(|_| { + InvalidVariableAssignmentValue { + var_name: var_name.clone(), + } + })?; + Ok((var_name.clone(), n)) + }) .collect::, Error>>()?; get_circuit_assignments(annotated, &fp_named_assignments) } From a5d9381c561eb67d71c43f0e641a98b14d565001 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 17 Jul 2023 12:22:45 +0100 Subject: [PATCH 3/9] Add prove API This commit adds prove_from_int_variable_assignments, prove_from_variable_assignments crate only private API to facilitate CLI. --- src/halo2/api.rs | 85 ++++++++++++++++++++++++++++++++++-- src/halo2/cli.rs | 109 +++++++++++++++-------------------------------- src/util.rs | 44 ++++++++++++++++--- 3 files changed, 153 insertions(+), 85 deletions(-) diff --git a/src/halo2/api.rs b/src/halo2/api.rs index d3bbd95..10d60ad 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -1,12 +1,19 @@ -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, ParseError}; +use crate::halo2::synth::make_constant; +use crate::halo2::synth::{keygen, prover, Halo2Module, PrimeFieldOps}; 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::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 { @@ -20,12 +27,82 @@ pub fn compile(source: impl AsRef, config: &Config) -> Result, + config: &Config, +) -> Result { + let module = circuit_data.circuit.module.as_ref(); + let assignments = get_circuit_assignments(module, named_assignments)?; + prove_from_variable_assignments(circuit_data, &assignments, config) +} + +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 = module + .pubs + .iter() + .map(|inst| assignments[&inst.id]) + .collect::>(); + 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, ¶ms)?; + + // Start proving witnesses + qprintln!(config, "* Proving knowledge of witnesses..."); + let proof = prover(circuit.clone(), ¶ms, &pk, instances) + .map_err(|e| BackendError { e: e.to_string() })?; + Ok(ProofDataHalo2 { + proof, + public_inputs, + }) +} + /* Captures all the data required to use a Halo2 circuit. */ pub struct HaloCircuitData { pub params: Params, pub circuit: Halo2Module, } +#[derive(CanonicalSerialize, CanonicalDeserialize)] +pub struct ProofDataHalo2 { + pub proof: Vec, + pub public_inputs: Vec, +} + impl HaloCircuitData { pub fn read(mut reader: R) -> Result where diff --git a/src/halo2/cli.rs b/src/halo2/cli.rs index 8ab62f0..b2d980e 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, ProofDataHalo2}; +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_file2, 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)] @@ -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_file2(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).unwrap() - } + 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).unwrap() + 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(()) @@ -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/util.rs b/src/util.rs index 38b1dfe..9d6089e 100644 --- a/src/util.rs +++ b/src/util.rs @@ -8,6 +8,7 @@ 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::{ @@ -17,13 +18,12 @@ use crate::{ /// 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( +pub(crate) fn get_circuit_assignments( module: &Module, - named_assignments: &HashMap, -) -> Result, Error> + named_assignments: &HashMap, +) -> Result, Error> where - F: Clone + Num + Neg, - ::FromStrRadixErr: std::fmt::Debug, + T: Clone, { let mut input_variables = HashMap::new(); collect_module_variables(module, &mut input_variables); @@ -50,6 +50,31 @@ where .collect() } +/* Read satisfying inputs to the given program from a file. */ +pub fn read_inputs_from_file2(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"); + + 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.clone(), n)) + }) + .collect::, Error>>() +} + /* Read satisfying inputs to the given program from a file. */ pub fn read_inputs_from_file( annotated: &Module, @@ -99,10 +124,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 { From 72e510bdd21da6619436447ddb994ea24bd2600e Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 18 Jul 2023 17:15:20 +0100 Subject: [PATCH 4/9] Refactor to a single read_inputs_from_file function --- src/halo2/cli.rs | 4 ++-- src/plonk/cli.rs | 40 ++++++++++++++++++++++------------------ src/util.rs | 32 ++------------------------------ 3 files changed, 26 insertions(+), 50 deletions(-) diff --git a/src/halo2/cli.rs b/src/halo2/cli.rs index b2d980e..687ebc6 100644 --- a/src/halo2/cli.rs +++ b/src/halo2/cli.rs @@ -3,7 +3,7 @@ use crate::halo2::api::{prove_from_int_variable_assignments, ProofDataHalo2}; use crate::halo2::synth::verifier; use crate::qprintln; -use crate::util::{get_circuit_assignments, prompt_inputs, read_inputs_from_file2, Config}; +use crate::util::{get_circuit_assignments, prompt_inputs, read_inputs_from_file, Config}; use halo2_proofs::plonk::keygen_vk; @@ -90,7 +90,7 @@ fn prove_from_file( "* Reading inputs from file {}...", path_to_inputs.to_string_lossy() ); - let raw_inputs: HashMap = read_inputs_from_file2(path_to_inputs).unwrap(); + 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) diff --git a/src/plonk/cli.rs b/src/plonk/cli.rs index 26628c9..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).unwrap() - } + 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).unwrap() + 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/util.rs b/src/util.rs index 9d6089e..c43fa08 100644 --- a/src/util.rs +++ b/src/util.rs @@ -6,6 +6,7 @@ use std::{ }; use ark_serialize::Write; + use num_traits::Num; use crate::ast::Variable; @@ -51,7 +52,7 @@ where } /* Read satisfying inputs to the given program from a file. */ -pub fn read_inputs_from_file2(path_to_inputs: &PathBuf) -> Result, Error> +pub fn read_inputs_from_file(path_to_inputs: &PathBuf) -> Result, Error> where F: Clone + Num + Neg, ::FromStrRadixErr: std::fmt::Debug, @@ -75,35 +76,6 @@ where .collect::, Error>>() } -/* Read satisfying inputs to the given program from a file. */ -pub fn read_inputs_from_file( - annotated: &Module, - 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"); - - let fp_named_assignments: HashMap = 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.clone(), n)) - }) - .collect::, Error>>()?; - get_circuit_assignments(annotated, &fp_named_assignments) -} - /* Prompt for satisfying inputs to the given program. */ pub fn prompt_inputs(annotated: &Module) -> HashMap where From 4cd8546bddd3035b11c939caa65bd14ca8d2a911 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 18 Jul 2023 18:03:33 +0100 Subject: [PATCH 5/9] Add tests for prove --- src/halo2/api.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/halo2/api.rs b/src/halo2/api.rs index 10d60ad..3014aa8 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -150,4 +150,28 @@ mod tests { let config = Config { quiet: true }; assert!(compile("1/0 = 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()); + } } From 9b0a4d70b1fc69b358a0c51a23fdf8ac47752144 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 18 Jul 2023 18:03:49 +0100 Subject: [PATCH 6/9] Prove API does not contain the serialized public input --- src/halo2/api.rs | 33 +++++++++++++++++++++++++-------- src/halo2/cli.rs | 8 ++++---- 2 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/halo2/api.rs b/src/halo2/api.rs index 3014aa8..b5252f0 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -29,19 +29,24 @@ pub fn compile(source: impl AsRef, config: &Config) -> Result, + named_assignments: &HashMap, Fp>, config: &Config, ) -> Result { let module = circuit_data.circuit.module.as_ref(); - let assignments = get_circuit_assignments(module, named_assignments)?; - prove_from_variable_assignments(circuit_data, &assignments, config) + let named_string_assignments: HashMap = named_assignments + .into_iter() + .map(|(key, value)| (key.as_ref().to_string(), *value)) + .collect(); + let assignments = get_circuit_assignments(module, &named_string_assignments)?; + let proof_data = prove_from_variable_assignments(circuit_data, &assignments, config)?; + Ok(ProofDataHalo2::from_proof_data_cli_halo2(proof_data)) } pub(crate) fn prove_from_int_variable_assignments( circuit_data: &HaloCircuitData, int_assignments: &HashMap, config: &Config, -) -> Result { +) -> Result { let assignments: HashMap = int_assignments .iter() .map(|(id, f)| (*id, make_constant::(f.clone()))) @@ -53,7 +58,7 @@ pub(crate) fn prove_from_variable_assignments( circuit_data: &HaloCircuitData, assignments: &HashMap, config: &Config, -) -> Result { +) -> Result { let params = &circuit_data.params; let module = circuit_data.circuit.module.as_ref(); @@ -85,7 +90,7 @@ pub(crate) fn prove_from_variable_assignments( qprintln!(config, "* Proving knowledge of witnesses..."); let proof = prover(circuit.clone(), ¶ms, &pk, instances) .map_err(|e| BackendError { e: e.to_string() })?; - Ok(ProofDataHalo2 { + Ok(ProofDataCliHalo2 { proof, public_inputs, }) @@ -97,10 +102,22 @@ pub struct HaloCircuitData { pub circuit: Halo2Module, } -#[derive(CanonicalSerialize, CanonicalDeserialize)] pub struct ProofDataHalo2 { pub proof: Vec, - pub public_inputs: Vec, +} + +impl ProofDataHalo2 { + fn from_proof_data_cli_halo2(proof_data: ProofDataCliHalo2) -> ProofDataHalo2 { + ProofDataHalo2 { + proof: proof_data.proof, + } + } +} + +#[derive(CanonicalSerialize, CanonicalDeserialize)] +pub(crate) struct ProofDataCliHalo2 { + pub(crate) proof: Vec, + pub(crate) public_inputs: Vec, } impl HaloCircuitData { diff --git a/src/halo2/cli.rs b/src/halo2/cli.rs index 687ebc6..2ee2832 100644 --- a/src/halo2/cli.rs +++ b/src/halo2/cli.rs @@ -1,5 +1,5 @@ use crate::error::Error; -use crate::halo2::api::{prove_from_int_variable_assignments, ProofDataHalo2}; +use crate::halo2::api::{prove_from_int_variable_assignments, ProofDataCliHalo2}; use crate::halo2::synth::verifier; use crate::qprintln; @@ -84,7 +84,7 @@ fn prove_from_file( path_to_inputs: &PathBuf, circuit_data: &HaloCircuitData, config: &Config, -) -> Result { +) -> Result { qprintln!( config, "* Reading inputs from file {}...", @@ -153,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) From 4e3184e33c946c4852fb1fae10f68479a3b76263 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 18 Jul 2023 19:23:26 +0100 Subject: [PATCH 7/9] Add verify API pub fn verify( circuit_data: &HaloCircuitData, proof_data: &ProofDataHalo2, named_public_assignments: &HashMap, Fp>, _config: &Config, ) NB: The proof data returned by the prove API does not contain the public inputs. They must be passed into the verify API separately. --- src/halo2/api.rs | 111 ++++++++++++++++++++++++++++++++++++++++++----- src/halo2/cli.rs | 2 +- src/transform.rs | 9 +++- src/util.rs | 54 ++++++++++++++++------- 4 files changed, 146 insertions(+), 30 deletions(-) diff --git a/src/halo2/api.rs b/src/halo2/api.rs index b5252f0..450e1d2 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -1,15 +1,16 @@ use crate::ast::{Module, VariableId}; use crate::error::Error; -use crate::error::Error::{BackendError, ParseError}; -use crate::halo2::synth::make_constant; +use crate::error::Error::{BackendError, ParseError, ProofVerificationFailure}; use crate::halo2::synth::{keygen, prover, Halo2Module, PrimeFieldOps}; +use crate::halo2::synth::{make_constant, verifier}; use crate::qprintln; -use crate::util::{get_circuit_assignments, Config}; +use crate::util::{get_circuit_assignments, get_public_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; use halo2_proofs::poly::commitment::Params; use num_bigint::BigInt; use std::collections::HashMap; @@ -19,7 +20,7 @@ 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); @@ -34,7 +35,7 @@ pub fn prove( ) -> Result { let module = circuit_data.circuit.module.as_ref(); let named_string_assignments: HashMap = named_assignments - .into_iter() + .iter() .map(|(key, value)| (key.as_ref().to_string(), *value)) .collect(); let assignments = get_circuit_assignments(module, &named_string_assignments)?; @@ -42,6 +43,47 @@ pub fn prove( Ok(ProofDataHalo2::from_proof_data_cli_halo2(proof_data)) } +pub fn verify( + circuit_data: &HaloCircuitData, + proof_data: &ProofDataHalo2, + named_public_assignments: &HashMap, Fp>, + _config: &Config, +) -> Result<(), Error> { + let circuit = &circuit_data.circuit; + let params = &circuit_data.params; + let module = circuit.module.as_ref(); + 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(module, &named_public_string_assignments)?; + let vk = keygen_vk(params, circuit)?; + verifier(params, &vk, &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( + module: &Module, + assignments: &HashMap, +) -> Result, Error> { + let var_assignments = get_public_circuit_assignments(module, assignments)?; + Ok(public_inputs_from_variable_assignments( + module, + &var_assignments, + )) +} + pub(crate) fn prove_from_int_variable_assignments( circuit_data: &HaloCircuitData, int_assignments: &HashMap, @@ -67,11 +109,7 @@ pub(crate) fn prove_from_variable_assignments( circuit.populate_variables(assignments.clone()); // Get public inputs Fp - let binding = module - .pubs - .iter() - .map(|inst| assignments[&inst.id]) - .collect::>(); + let binding = public_inputs_from_variable_assignments(module, assignments); let instances = binding.as_slice(); let public_inputs: Vec = instances @@ -84,11 +122,11 @@ pub(crate) fn prove_from_variable_assignments( // Generating proving key qprintln!(config, "* Generating proving key..."); - let (pk, _vk) = keygen(&circuit, ¶ms)?; + let (pk, _vk) = keygen(&circuit, params)?; // Start proving witnesses qprintln!(config, "* Proving knowledge of witnesses..."); - let proof = prover(circuit.clone(), ¶ms, &pk, instances) + let proof = prover(circuit.clone(), params, &pk, instances) .map_err(|e| BackendError { e: e.to_string() })?; Ok(ProofDataCliHalo2 { proof, @@ -191,4 +229,53 @@ mod tests { 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(&circuit, &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(&circuit, &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(&circuit, &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(&circuit, &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(&circuit, &proof_data, &public_assignments, &config).is_err()); + } } diff --git a/src/halo2/cli.rs b/src/halo2/cli.rs index 2ee2832..9f4eb62 100644 --- a/src/halo2/cli.rs +++ b/src/halo2/cli.rs @@ -71,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(); 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 c43fa08..144af33 100644 --- a/src/util.rs +++ b/src/util.rs @@ -12,30 +12,21 @@ use num_traits::Num; use crate::ast::Variable; use crate::error::Error; use crate::error::Error::{InvalidVariableAssignmentValue, MissingVariableAssignment}; +use crate::transform::collect_public_module_variables; use crate::{ ast::{Module, Pat, VariableId}, transform::collect_module_variables, }; -/// 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, +/// Find a value for each expected variable from among the named assignments. +fn translate_named_assignments( + expected_variables: &HashMap, named_assignments: &HashMap, ) -> Result, Error> where T: Clone, { - let mut input_variables = HashMap::new(); - collect_module_variables(module, &mut input_variables); - // Defined variables should not be requested from user - for def in &module.defs { - if let Pat::Variable(var) = &def.0 .0.v { - input_variables.remove(&var.id); - } - } - - input_variables + expected_variables .iter() .filter_map(|(id, expected_var)| { expected_var.name.as_deref().map(|var_name| { @@ -51,6 +42,39 @@ where .collect() } +/// Convert named circuit assignments for public variables to assignments of vamp-ir variableIds. +pub(crate) fn get_public_circuit_assignments( + module: &Module, + named_assignments: &HashMap, +) -> Result, Error> +where + T: Clone, +{ + let mut input_variables = HashMap::new(); + collect_public_module_variables(module, &mut input_variables); + translate_named_assignments(&input_variables, named_assignments) +} + +/// 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 + T: Clone, +{ + let mut input_variables = HashMap::new(); + collect_module_variables(module, &mut input_variables); + // Defined variables should not be requested from user + for def in &module.defs { + if let Pat::Variable(var) = &def.0 .0.v { + input_variables.remove(&var.id); + } + } + translate_named_assignments(&input_variables, named_assignments) +} + /* Read satisfying inputs to the given program from a file. */ pub fn read_inputs_from_file(path_to_inputs: &PathBuf) -> Result, Error> where @@ -71,7 +95,7 @@ where var_name: var_name.clone(), } })?; - Ok((var_name.clone(), n)) + Ok((var_name, n)) }) .collect::, Error>>() } From ed24c6981a8124a1628ef716d73063f2d87db56d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 19 Jul 2023 13:46:01 +0100 Subject: [PATCH 8/9] Fix typechecking error test case --- src/halo2/api.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/halo2/api.rs b/src/halo2/api.rs index 450e1d2..682d1b2 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -203,7 +203,7 @@ 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] From 41141d5e96fd9b7f1cecf540a697ff791c7d6b58 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 20 Jul 2023 14:58:26 +0100 Subject: [PATCH 9/9] verify does not require the circuit The proof API now returns: ``` pub struct ProofDataHalo2 { pub proof: Vec, pub verifying_key: VerifyingKey, pub public_fields: Vec, pub params: Params, } ``` The proof, verifying_key and params are used in the Halo2 verification API. The public fields are a vector of vamp-ir public variable names that need to be provided for verification. The order of these Strings is used to construct the correct ordered vector of field elements to pass to the verifier. The verify API is now: ``` pub fn verify( proof_data: &ProofDataHalo2, named_public_assignments: &HashMap, Fp>, _config: &Config, ) -> Result<(), Error> ``` The circuit is not required for verification. --- src/halo2/api.rs | 99 ++++++++++++++++++++++++++++++++---------------- src/util.rs | 52 +++++++------------------ 2 files changed, 81 insertions(+), 70 deletions(-) diff --git a/src/halo2/api.rs b/src/halo2/api.rs index 682d1b2..b37e935 100644 --- a/src/halo2/api.rs +++ b/src/halo2/api.rs @@ -1,16 +1,18 @@ use crate::ast::{Module, VariableId}; use crate::error::Error; -use crate::error::Error::{BackendError, ParseError, ProofVerificationFailure}; +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::{get_circuit_assignments, get_public_circuit_assignments, 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; +use halo2_proofs::plonk::{keygen_vk, VerifyingKey}; use halo2_proofs::poly::commitment::Params; use num_bigint::BigInt; use std::collections::HashMap; @@ -39,27 +41,43 @@ pub fn prove( .map(|(key, value)| (key.as_ref().to_string(), *value)) .collect(); let assignments = get_circuit_assignments(module, &named_string_assignments)?; - let proof_data = prove_from_variable_assignments(circuit_data, &assignments, config)?; - Ok(ProofDataHalo2::from_proof_data_cli_halo2(proof_data)) + 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( - circuit_data: &HaloCircuitData, proof_data: &ProofDataHalo2, named_public_assignments: &HashMap, Fp>, _config: &Config, ) -> Result<(), Error> { - let circuit = &circuit_data.circuit; - let params = &circuit_data.params; - let module = circuit.module.as_ref(); + 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(module, &named_public_string_assignments)?; - let vk = keygen_vk(params, circuit)?; - verifier(params, &vk, &proof_data.proof, public_input.as_slice()) - .map_err(|_| ProofVerificationFailure) + 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( @@ -74,14 +92,20 @@ fn public_inputs_from_variable_assignments( } fn public_inputs_from_assignments( - module: &Module, + public_fields: &[String], assignments: &HashMap, ) -> Result, Error> { - let var_assignments = get_public_circuit_assignments(module, assignments)?; - Ok(public_inputs_from_variable_assignments( - module, - &var_assignments, - )) + 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( @@ -140,16 +164,16 @@ pub struct HaloCircuitData { pub circuit: Halo2Module, } -pub struct ProofDataHalo2 { - pub proof: Vec, +pub struct VerifyingKeyDataHalo2 { + pub verifying_key: VerifyingKey, + pub params: Params, } -impl ProofDataHalo2 { - fn from_proof_data_cli_halo2(proof_data: ProofDataCliHalo2) -> ProofDataHalo2 { - ProofDataHalo2 { - proof: proof_data.proof, - } - } +pub struct ProofDataHalo2 { + pub proof: Vec, + pub verifying_key: VerifyingKey, + pub public_fields: Vec, + pub params: Params, } #[derive(CanonicalSerialize, CanonicalDeserialize)] @@ -236,7 +260,7 @@ mod tests { let circuit = compile("x = 1;", &config).unwrap(); let assignments = HashMap::from([("x", Fp::one())]); let proof_data = prove(&circuit, &assignments, &config).unwrap(); - assert!(verify(&circuit, &proof_data, &assignments, &config).is_ok()); + assert!(verify(&proof_data, &assignments, &config).is_ok()); } #[test] @@ -246,7 +270,7 @@ mod tests { 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(&circuit, &proof_data, &public_assignments, &config).is_ok()); + assert!(verify(&proof_data, &public_assignments, &config).is_ok()); } #[test] @@ -256,7 +280,7 @@ mod tests { let assignments = HashMap::from([("x", Fp::zero())]); let public_assignments: HashMap = HashMap::new(); let proof_data = prove(&circuit, &assignments, &config).unwrap(); - assert!(verify(&circuit, &proof_data, &public_assignments, &config).is_err()); + assert!(verify(&proof_data, &public_assignments, &config).is_err()); } #[test] @@ -266,7 +290,7 @@ mod tests { 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(&circuit, &proof_data, &public_assignments, &config).is_err()); + assert!(verify(&proof_data, &public_assignments, &config).is_err()); } #[test] @@ -276,6 +300,17 @@ mod tests { let assignments = HashMap::from([("x", Fp::one())]); let public_assignments: HashMap = HashMap::new(); let proof_data = prove(&circuit, &assignments, &config).unwrap(); - assert!(verify(&circuit, &proof_data, &public_assignments, &config).is_err()); + 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/util.rs b/src/util.rs index 144af33..92c341e 100644 --- a/src/util.rs +++ b/src/util.rs @@ -12,21 +12,30 @@ use num_traits::Num; use crate::ast::Variable; use crate::error::Error; use crate::error::Error::{InvalidVariableAssignmentValue, MissingVariableAssignment}; -use crate::transform::collect_public_module_variables; use crate::{ ast::{Module, Pat, VariableId}, transform::collect_module_variables, }; -/// Find a value for each expected variable from among the named assignments. -fn translate_named_assignments( - expected_variables: &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 T: Clone, { - expected_variables + let mut input_variables = HashMap::new(); + collect_module_variables(module, &mut input_variables); + // Defined variables should not be requested from user + for def in &module.defs { + if let Pat::Variable(var) = &def.0 .0.v { + input_variables.remove(&var.id); + } + } + + input_variables .iter() .filter_map(|(id, expected_var)| { expected_var.name.as_deref().map(|var_name| { @@ -42,39 +51,6 @@ where .collect() } -/// Convert named circuit assignments for public variables to assignments of vamp-ir variableIds. -pub(crate) fn get_public_circuit_assignments( - module: &Module, - named_assignments: &HashMap, -) -> Result, Error> -where - T: Clone, -{ - let mut input_variables = HashMap::new(); - collect_public_module_variables(module, &mut input_variables); - translate_named_assignments(&input_variables, named_assignments) -} - -/// 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 - T: Clone, -{ - let mut input_variables = HashMap::new(); - collect_module_variables(module, &mut input_variables); - // Defined variables should not be requested from user - for def in &module.defs { - if let Pat::Variable(var) = &def.0 .0.v { - input_variables.remove(&var.id); - } - } - translate_named_assignments(&input_variables, named_assignments) -} - /* Read satisfying inputs to the given program from a file. */ pub fn read_inputs_from_file(path_to_inputs: &PathBuf) -> Result, Error> where