diff --git a/taiga_halo2/Cargo.toml b/taiga_halo2/Cargo.toml index 40d38386..5fd22962 100644 --- a/taiga_halo2/Cargo.toml +++ b/taiga_halo2/Cargo.toml @@ -16,6 +16,8 @@ bitvec = "1" subtle = { version = "2.3", default-features = false } dyn-clone = "1.0" reddsa = "0.5" +vamp-ir = { git = "https://github.com/anoma/vamp-ir.git", rev = "e11fbcd6d5a358e33456ae7cd7abe5fea9dfcc3e"} +bincode = "2.0.0-rc.1" [dev-dependencies] criterion = "0.3" diff --git a/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.halo2 b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.halo2 new file mode 100644 index 00000000..4fff00b6 Binary files /dev/null and b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.halo2 differ diff --git a/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.inputs b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.inputs new file mode 100644 index 00000000..69a4685b --- /dev/null +++ b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.inputs @@ -0,0 +1,5 @@ +{ + "x": "15", + "y": "20", + "R": "25" +} \ No newline at end of file diff --git a/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.pir b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.pir new file mode 100644 index 00000000..05f3028d --- /dev/null +++ b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.pir @@ -0,0 +1,10 @@ +// declare R to be public +pub R; + +// define the Pythagorean relation we are checking +def pyth a b c = { + a^2 + b^2 = c^2 +}; + +// appends constraint x^2 + y^2 = R^2 to the circuit +pyth x y R; \ No newline at end of file diff --git a/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.proof b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.proof new file mode 100644 index 00000000..e07d46d4 Binary files /dev/null and b/taiga_halo2/src/circuit/vamp_ir_circuits/pyth.proof differ diff --git a/taiga_halo2/src/circuit/vp_circuit.rs b/taiga_halo2/src/circuit/vp_circuit.rs index e620d68c..ee6f8847 100644 --- a/taiga_halo2/src/circuit/vp_circuit.rs +++ b/taiga_halo2/src/circuit/vp_circuit.rs @@ -15,13 +15,21 @@ use crate::{ proof::Proof, vp_vk::ValidityPredicateVerifyingKey, }; +use bincode::error::DecodeError; use dyn_clone::{clone_trait_object, DynClone}; use halo2_gadgets::{ecc::chip::EccChip, sinsemilla::chip::SinsemillaChip}; use halo2_proofs::{ circuit::{AssignedCell, Layouter, Value}, - plonk::{Circuit, ConstraintSystem, Error, VerifyingKey}, + plonk::{keygen_pk, keygen_vk, Circuit, ConstraintSystem, Error, VerifyingKey}, + poly::commitment::Params, }; use pasta_curves::{pallas, vesta}; +use rand::rngs::OsRng; +use std::collections::HashMap; +use std::fs::File; +use std::path::PathBuf; +use vamp_ir::halo2::synth::{make_constant, Halo2Module}; +use vamp_ir::util::read_inputs_from_file; #[derive(Debug, Clone)] pub struct VPVerifyingInfo { @@ -472,3 +480,102 @@ macro_rules! vp_circuit_impl { } }; } + +#[derive(Clone)] +pub struct VampIRValidityPredicateCircuit { + // TODO: vamp_ir doesn't support to set the params size manually, add the params here temporarily. + // remove the params once we can set it as VP_CIRCUIT_PARAMS_SIZE in vamp_ir. + pub params: Params, + pub circuit: Halo2Module, + pub instances: Vec, +} + +impl VampIRValidityPredicateCircuit { + pub fn from_vamp_ir_circuit(vamp_ir_circuit_file: &PathBuf, inputs_file: &PathBuf) -> Self { + let mut circuit_file = + File::open(vamp_ir_circuit_file).expect("unable to load circuit file"); + // let mut circuit: Halo2Module = + // bincode::decode_from_std_read(&mut circuit_file, bincode::config::standard()) + // .expect("unable to load circuit file"); + let HaloCircuitData { + params, + mut circuit, + } = HaloCircuitData::read(&mut circuit_file).unwrap(); + let var_assignments_ints = read_inputs_from_file(&circuit.module, inputs_file); + 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); + + // TODO: export and handle the instances + Self { + params, + circuit, + instances: vec![], + } + } +} + +impl ValidityPredicateVerifyingInfo for VampIRValidityPredicateCircuit { + fn get_verifying_info(&self) -> VPVerifyingInfo { + let mut rng = OsRng; + // let params = SETUP_PARAMS_MAP.get(&VP_CIRCUIT_PARAMS_SIZE).unwrap(); + let vk = keygen_vk(&self.params, &self.circuit).expect("keygen_vk should not fail"); + let pk = + keygen_pk(&self.params, vk.clone(), &self.circuit).expect("keygen_pk should not fail"); + // TODO: export and handle the instances + let proof = Proof::create(&pk, &self.params, self.circuit.clone(), &[], &mut rng).unwrap(); + VPVerifyingInfo { + vk, + proof, + instance: self.instances.clone(), + } + } + + fn get_vp_vk(&self) -> ValidityPredicateVerifyingKey { + // let params = SETUP_PARAMS_MAP.get(&VP_CIRCUIT_PARAMS_SIZE).unwrap(); + let vk = keygen_vk(&self.params, &self.circuit).expect("keygen_vk should not fail"); + ValidityPredicateVerifyingKey::from_vk(vk) + } +} + +// TODO: We won't need the HaloCircuitData when we can import the circuit from vamp_ir. +struct HaloCircuitData { + params: Params, + circuit: Halo2Module, +} + +impl HaloCircuitData { + fn read(mut reader: R) -> Result + where + R: std::io::Read, + { + let params = Params::::read(&mut reader) + .map_err(|x| DecodeError::OtherString(x.to_string()))?; + let circuit: Halo2Module = + bincode::decode_from_std_read(&mut reader, bincode::config::standard())?; + Ok(Self { params, circuit }) + } +} + +#[test] +fn test_create_vp_from_vamp_ir_circuit() { + let vamp_ir_circuit_file = PathBuf::from("./src/circuit/vamp_ir_circuits/pyth.halo2"); + let inputs_file = PathBuf::from("./src/circuit/vamp_ir_circuits/pyth.inputs"); + let vp_circuit = + VampIRValidityPredicateCircuit::from_vamp_ir_circuit(&vamp_ir_circuit_file, &inputs_file); + + // generate proof and instance + let vp_info = vp_circuit.get_verifying_info(); + + // verify the proof + // TODO: use the vp_info.verify() instead. vp_info.verify() doesn't work now because it uses the fixed VP_CIRCUIT_PARAMS_SIZE params. + // TODO: export and handle the instances + vp_info + .proof + .verify(&vp_info.vk, &vp_circuit.params, &[]) + .unwrap(); +}