From eaf996c69d0c47c6f316b9359ff144ddcaf17f47 Mon Sep 17 00:00:00 2001 From: wwared Date: Fri, 1 Mar 2024 14:24:32 -0300 Subject: [PATCH] Fix coprocessors returning lists in SuperNova (#1186) * Fix coprocessors returning lists in SuperNova In NIVC, the Lurk circuit calls out to the coprocessor circuit, and then on the next fold step calls back into the main Lurk circuit with the result of the coprocessor. If the coprocessor returns a single value, there is no issue, but if the coprocessor returns a list, then the lurk circuit attempts to evaluate that expression instead of simply returning it. To fix it, we wrap the coprocessor return expr with a thunk. * test correctness of a simple coprocessor that returns a list in the NIVC context --------- Co-authored-by: Arthur Paulino --- src/cli/repl/mod.rs | 15 +++----- src/coprocessor/mod.rs | 55 ++++++++++++++++++++++++++ src/lem/eval.rs | 6 ++- src/proof/nova.rs | 3 +- src/proof/supernova.rs | 3 +- src/proof/tests/mod.rs | 2 + src/proof/tests/supernova_tests.rs | 62 ++++++++++++++++++++++++++++++ src/public_parameters/instance.rs | 29 +++++++++++++- 8 files changed, 160 insertions(+), 15 deletions(-) create mode 100644 src/proof/tests/supernova_tests.rs diff --git a/src/cli/repl/mod.rs b/src/cli/repl/mod.rs index 1f5169a81a..ac4b5890b0 100644 --- a/src/cli/repl/mod.rs +++ b/src/cli/repl/mod.rs @@ -43,10 +43,7 @@ use crate::{ supernova::SuperNovaProver, RecursiveSNARKTrait, }, - public_parameters::{ - instance::{Instance, Kind}, - public_params, supernova_public_params, - }, + public_parameters::{instance::Instance, public_params, supernova_public_params}, state::State, tag::{ContTag, ExprTag}, Symbol, @@ -338,12 +335,11 @@ where info!("Proof not cached"); let (proof, public_inputs, public_outputs) = match self.backend { Backend::Nova => { + let prover = NovaProver::<_, C>::new(self.rc, self.lang.clone()); info!("Loading Nova public parameters"); - let instance = - Instance::new(self.rc, self.lang.clone(), true, Kind::NovaPublicParams); + let instance = Instance::new_nova(&prover, true); let pp = public_params(&instance)?; - let prover = NovaProver::<_, C>::new(self.rc, self.lang.clone()); info!("Proving with NovaProver"); let (proof, public_inputs, public_outputs, num_steps) = prover.prove_from_frames(&pp, frames, &self.store)?; @@ -354,12 +350,11 @@ where (LurkProofWrapper::Nova(proof), public_inputs, public_outputs) } Backend::SuperNova => { + let prover = SuperNovaProver::<_, C>::new(self.rc, self.lang.clone()); info!("Loading SuperNova public parameters"); - let instance = - Instance::new(self.rc, self.lang.clone(), true, Kind::SuperNovaAuxParams); + let instance = Instance::new_supernova(&prover, true); let pp = supernova_public_params(&instance)?; - let prover = SuperNovaProver::<_, C>::new(self.rc, self.lang.clone()); info!("Proving with SuperNovaProver"); let (proof, public_inputs, public_outputs, _num_steps) = prover.prove_from_frames(&pp, frames, &self.store)?; diff --git a/src/coprocessor/mod.rs b/src/coprocessor/mod.rs index 504ee8d85f..5a769c9214 100644 --- a/src/coprocessor/mod.rs +++ b/src/coprocessor/mod.rs @@ -116,6 +116,8 @@ pub(crate) mod test { use bellpepper_core::num::AllocatedNum; use serde::{Deserialize, Serialize}; + use self::gadgets::construct_cons; + use super::*; use crate::circuit::gadgets::constraints::{alloc_equal, mul}; use crate::lem::{pointers::RawPtr, tag::Tag as LEMTag}; @@ -348,4 +350,57 @@ pub(crate) mod test { Self::intern_hello_world(s) } } + + /// A coprocessor that simply returns the pair (nil . nil) + #[derive(Clone, Debug, Serialize, Deserialize)] + pub(crate) struct NilNil { + _p: PhantomData, + } + + impl NilNil { + pub(crate) fn new() -> Self { + Self { + _p: Default::default(), + } + } + } + + impl CoCircuit for NilNil { + fn arity(&self) -> usize { + 0 + } + + fn synthesize_simple>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + s: &Store, + _not_dummy: &Boolean, + _args: &[AllocatedPtr], + ) -> Result, SynthesisError> { + let nil = g.alloc_ptr(cs, &s.intern_nil(), s); + construct_cons(cs, g, s, &nil, &nil) + } + + fn alloc_globals>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + s: &Store, + ) { + g.alloc_ptr(cs, &s.intern_nil(), s); + g.alloc_tag(cs, &ExprTag::Cons); + } + } + + impl Coprocessor for NilNil { + fn has_circuit(&self) -> bool { + true + } + + fn evaluate_simple(&self, s: &Store, _args: &[Ptr]) -> Ptr { + let nil = s.intern_nil(); + s.cons(nil, nil) + } + } } diff --git a/src/lem/eval.rs b/src/lem/eval.rs index e856f6617e..51e6a75258 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -353,6 +353,7 @@ fn car_cdr() -> Func { /// // there must be no remaining arguments /// if is_nil { /// Op::Cproc([expr, env, cont], x, [x0, x1, ..., x{n-1}, env, cont]); +/// let expr: Expr::Thunk = cons2(expr, cont); /// return (expr, env, cont); /// } /// return (evaluated_args_cp, env, err); @@ -390,7 +391,10 @@ fn run_cproc(cproc_sym: Symbol, arity: usize) -> Func { cproc_inp.push(env.clone()); cproc_inp.push(cont.clone()); let mut block = Block { - ops: vec![Op::Cproc(cproc_out, cproc_sym.clone(), cproc_inp.clone())], + ops: vec![ + Op::Cproc(cproc_out, cproc_sym.clone(), cproc_inp.clone()), + op!(let expr: Expr::Thunk = cons2(expr, cont)), + ], ctrl: Ctrl::Return(func_out), }; for (i, cproc_arg) in cproc_inp[0..arity].iter().enumerate() { diff --git a/src/proof/nova.rs b/src/proof/nova.rs index 0b194b870a..e822af7712 100644 --- a/src/proof/nova.rs +++ b/src/proof/nova.rs @@ -399,7 +399,8 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor + 'a> NovaProver<'a, F, C> { } #[inline] - fn lang(&self) -> &Arc> { + /// Returns the `Lang` wrapped with `Arc` for cheap cloning + pub fn lang(&self) -> &Arc> { &self.lang } } diff --git a/src/proof/supernova.rs b/src/proof/supernova.rs index 21a846b479..47f1cd1b6d 100644 --- a/src/proof/supernova.rs +++ b/src/proof/supernova.rs @@ -183,7 +183,8 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor + 'a> SuperNovaProver<'a, F, C } #[inline] - fn lang(&self) -> &Arc> { + /// Returns the `Lang` wrapped with `Arc` for cheap cloning + pub fn lang(&self) -> &Arc> { &self.lang } } diff --git a/src/proof/tests/mod.rs b/src/proof/tests/mod.rs index 8dd9882c07..60f4967573 100644 --- a/src/proof/tests/mod.rs +++ b/src/proof/tests/mod.rs @@ -1,4 +1,6 @@ mod nova_tests; +mod supernova_tests; + use bellpepper::util_cs::{metric_cs::MetricCS, witness_cs::WitnessCS, Comparable}; use bellpepper_core::{test_cs::TestConstraintSystem, Circuit, ConstraintSystem, Delta}; use expect_test::Expect; diff --git a/src/proof/tests/supernova_tests.rs b/src/proof/tests/supernova_tests.rs new file mode 100644 index 0000000000..725a127c5b --- /dev/null +++ b/src/proof/tests/supernova_tests.rs @@ -0,0 +1,62 @@ +use halo2curves::bn256::Fr; +use std::sync::Arc; + +use crate::{ + eval::lang::Lang, + lem::{ + eval::{evaluate, make_cprocs_funcs_from_lang, make_eval_step_from_config, EvalConfig}, + store::Store, + }, + proof::{supernova::SuperNovaProver, RecursiveSNARKTrait}, + public_parameters::{instance::Instance, supernova_public_params}, + state::user_sym, +}; + +#[test] +fn test_nil_nil_lang() { + use crate::coprocessor::test::NilNil; + let mut lang = Lang::>::new(); + lang.add_coprocessor(user_sym("nil-nil"), NilNil::new()); + + let eval_config = EvalConfig::new_nivc(&lang); + let lurk_step = make_eval_step_from_config(&eval_config); + let cprocs = make_cprocs_funcs_from_lang(&lang); + + let store = Store::default(); + let expr = store.read_with_default_state("(nil-nil)").unwrap(); + let frames = evaluate(Some((&lurk_step, &cprocs, &lang)), expr, &store, 50).unwrap(); + + // iteration 1: main circuit sets up a call to the coprocessor + // iteration 2: coprocessor does its job + // iteration 3: main circuit sets termination to terminal + assert_eq!(frames.len(), 3); + + let first_frame = frames.first().unwrap(); + let last_frame = frames.last().unwrap(); + let output = &last_frame.output; + + // the result is the (nil . nil) pair + let nil = store.intern_nil(); + assert!(store.ptr_eq(&output[0], &store.cons(nil, nil))); + + // computation must end with the terminal continuation + assert!(store.ptr_eq(&output[2], &store.cont_terminal())); + + let supernova_prover = SuperNovaProver::new(5, Arc::new(lang)); + let instance = Instance::new_supernova(&supernova_prover, true); + let pp = supernova_public_params(&instance).unwrap(); + + let (proof, ..) = supernova_prover + .prove_from_frames(&pp, &frames, &store) + .unwrap(); + + let input_scalar = store.to_scalar_vector(&first_frame.input); + let output_scalar = store.to_scalar_vector(output); + + // uncompressed proof verifies + assert!(proof.verify(&pp, &input_scalar, &output_scalar).unwrap()); + + // compressed proof verifies + let proof = proof.compress(&pp).unwrap(); + assert!(proof.verify(&pp, &input_scalar, &output_scalar).unwrap()); +} diff --git a/src/public_parameters/instance.rs b/src/public_parameters/instance.rs index 6a4e1629ef..ada36de366 100644 --- a/src/public_parameters/instance.rs +++ b/src/public_parameters/instance.rs @@ -50,8 +50,9 @@ use crate::{ coprocessor::Coprocessor, eval::lang::Lang, proof::{ - nova::{self, CurveCycleEquipped}, - supernova::{self}, + nova::{self, CurveCycleEquipped, NovaProver}, + supernova::{self, SuperNovaProver}, + Prover, }, }; @@ -134,6 +135,30 @@ impl> Instance { } } + /// Returns an `Instance` for Nova public parameters with the prover's + /// reduction count and lang + #[inline] + pub fn new_nova(prover: &NovaProver<'_, F, C>, abomonated: bool) -> Self { + Self::new( + prover.reduction_count(), + prover.lang().clone(), + abomonated, + Kind::NovaPublicParams, + ) + } + + /// Returns an `Instance` for SuperNova public parameters with the prover's + /// reduction count and lang + #[inline] + pub fn new_supernova(prover: &SuperNovaProver<'_, F, C>, abomonated: bool) -> Self { + Self::new( + prover.reduction_count(), + prover.lang().clone(), + abomonated, + Kind::SuperNovaAuxParams, + ) + } + /// If this [Instance] is of [Kind::SuperNovaAuxParams], then generate the `num_circuits + 1` /// circuit param instances that are determined by the internal [Lang]. pub fn circuit_param_instances(&self) -> Vec {