Skip to content

Commit

Permalink
refactor: Refactor codebase to remove proving Alpha MultiFrame functi…
Browse files Browse the repository at this point in the history 
…onality

- Removed the use of `witness_cs::WitnessCS`, `boolean::Boolean`, and `Provable` trait from various modules in `bellpepper_core`,
- Dropped multithreading support on `prove_recursively` function in `nova.rs`,
- Deleted `StepCircuit` and `SuperStepCircuit<F>` implementation for `MultiFrame`, including its functions `synthesize` and `compute_witness`,
- Refactored several functions in `nova::prove_recursively`,
- Removed unused imports and implementations across multiple files.
  • Loading branch information
@huitseeker
huitseeker committed Nov 9, 2023
1 parent 848bb93 commit 9e6a2fd
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 382 deletions.
126 changes: 2 additions & 124 deletions src/circuit/circuit_frame.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,7 @@ use std::fmt::Debug;
use std::marker::PhantomData;

use bellpepper::util_cs::{witness_cs::WitnessCS, Comparable};
use bellpepper_core::{
boolean::Boolean, num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError,
};
use bellpepper_core::{boolean::Boolean, num::AllocatedNum, ConstraintSystem, SynthesisError};
use rayon::prelude::*;
use tracing::{debug, info};

Expand Down Expand Up @@ -33,13 +31,12 @@ use crate::circuit::circuit_frame::constraints::{
allocate_is_negative, boolean_to_num, enforce_pack, enforce_product_and_sum, mul,
};
use crate::circuit::gadgets::hashes::{AllocatedConsWitness, AllocatedContWitness};
use crate::circuit::ToInputs;
use crate::coprocessor::Coprocessor;
use crate::eval::{Frame, Meta, Witness, IO};
use crate::expr::Thunk;
use crate::hash_witness::HashWitness;
use crate::lurk_sym_ptr;
use crate::proof::{supernova::FoldingConfig, Provable};
use crate::proof::supernova::FoldingConfig;
use crate::ptr::Ptr;
use crate::store::Store;
use crate::tag::{ContTag, ExprTag, Op1, Op2};
Expand Down Expand Up @@ -480,38 +477,6 @@ impl<F: LurkField, C: Coprocessor<F>> MultiFrame<'_, F, C> {
}
}

impl<
F: LurkField, // W: Copy + Sync,
C: Coprocessor<F>,
> Provable<F> for MultiFrame<'_, F, C>
{
fn public_inputs(&self) -> Vec<F> {
let mut inputs: Vec<_> = Vec::with_capacity(self.public_input_size());

if let Some(input) = &self.input {
inputs.extend(input.to_inputs(self.get_store()));
} else {
panic!("public inputs for blank circuit");
}
if let Some(output) = &self.output {
inputs.extend(output.to_inputs(self.get_store()));
} else {
panic!("public outputs for blank circuit");
}

inputs
}

fn public_input_size(&self) -> usize {
let input_output_size = IO::<F>::input_size();
input_output_size * 2
}

fn reduction_count(&self) -> usize {
self.count
}
}

type AllocatedIO<F> = (AllocatedPtr<F>, AllocatedPtr<F>, AllocatedContPtr<F>);

impl<F: LurkField, C: Coprocessor<F>> CircuitFrame<'_, F, C> {
Expand Down Expand Up @@ -584,93 +549,6 @@ impl<F: LurkField, C: Coprocessor<F>> CircuitFrame<'_, F, C> {
}
}

impl<F: LurkField, C: Coprocessor<F>> Circuit<F> for MultiFrame<'_, F, C> {
#[tracing::instrument(skip_all, name = "<MultiFrame as Circuit>::synthesize")]
fn synthesize<CS: ConstraintSystem<F>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
////////////////////////////////////////////////////////////////////////////////
// Bind public inputs.
//
// Initial input:
let mut synth = |store,
frames: &[CircuitFrame<'_, F, C>],
input: Option<IO<F>>,
output: Option<IO<F>>| {
let input_expr = AllocatedPtr::bind_input(
&mut cs.namespace(|| "outer input expression"),
input.as_ref().map(|input| &input.expr),
store,
)?;

let input_env = AllocatedPtr::bind_input(
&mut cs.namespace(|| "outer input env"),
input.as_ref().map(|input| &input.env),
store,
)?;

let input_cont = AllocatedContPtr::bind_input(
&mut cs.namespace(|| "outer input cont"),
input.as_ref().map(|input| &input.cont),
store,
)?;

// Final output:
let output_expr = AllocatedPtr::bind_input(
&mut cs.namespace(|| "outer output expression"),
output.as_ref().map(|output| &output.expr),
store,
)?;

let output_env = AllocatedPtr::bind_input(
&mut cs.namespace(|| "outer output env"),
output.as_ref().map(|output| &output.env),
store,
)?;

let output_cont = AllocatedContPtr::bind_input(
&mut cs.namespace(|| "outer output cont"),
output.as_ref().map(|output| &output.cont),
store,
)?;

//
// End public inputs.
////////////////////////////////////////////////////////////////////////////////
let g = GlobalAllocations::new(&mut cs.namespace(|| "global_allocations"), store)?;

let (new_expr, new_env, new_cont) =
self.synthesize_frames(cs, store, input_expr, input_env, input_cont, frames, &g);

output_expr.enforce_equal(
&mut cs.namespace(|| "outer output expr is correct"),
&new_expr,
);
output_env.enforce_equal(
&mut cs.namespace(|| "outer output env is correct"),
&new_env,
);
output_cont.enforce_equal(
&mut cs.namespace(|| "outer output cont is correct"),
&new_cont,
);

Ok(())
};

match self.store {
Some(s) => {
let frames = self.frames.as_ref().unwrap();
synth(s, frames, self.input, self.output)
}
None => {
let store = Default::default();
assert!(self.frames.is_none());
let frames = vec![CircuitFrame::blank(); self.count];
synth(&store, &frames, self.input, self.output)
}
}
}
}

#[derive(Default)]
struct Results<'a, F: LurkField> {
expr_tag_clauses: Vec<CaseClause<'a, F>>,
Expand Down
165 changes: 1 addition & 164 deletions src/proof/nova.rs
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
#![allow(non_snake_case)]

use abomonation::Abomonation;
use bellpepper::util_cs::witness_cs::WitnessCS;
use bellpepper_core::{boolean::Boolean, num::AllocatedNum, ConstraintSystem, SynthesisError};
use bellpepper_core::{num::AllocatedNum, ConstraintSystem};
use ff::Field;
use nova::{
errors::NovaError,
Expand All @@ -24,20 +23,12 @@ use std::{
};

use crate::{
circuit::{
gadgets::{
data::GlobalAllocations,
pointer::{AllocatedContPtr, AllocatedPtr},
},
CircuitFrame, MultiFrame,
},
config::lurk_config,
coprocessor::Coprocessor,
error::ProofError,
eval::{lang::Lang, Meta},
field::LurkField,
proof::{supernova::FoldingConfig, EvaluationStore, FrameLike, MultiFrameTrait, Prover},
store::Store,
};

/// This trait defines most of the requirements for programming generically over the supported Nova curve cycles
Expand Down Expand Up @@ -498,157 +489,3 @@ where
vec![<G2<F> as Group>::Scalar::ZERO]
}
}

impl<'a, F: LurkField, C: Coprocessor<F>> StepCircuit<F> for MultiFrame<'a, F, C> {
fn arity(&self) -> usize {
6
}

#[tracing::instrument(skip_all, name = "<MultiFrame as StepCircuit>::synthesize")]
fn synthesize<CS>(
&self,
cs: &mut CS,
z: &[AllocatedNum<F>],
) -> Result<Vec<AllocatedNum<F>>, SynthesisError>
where
CS: ConstraintSystem<F>,
{
assert_eq!(self.arity(), z.len());

if cs.is_witness_generator() {
if let Some(w) = &self.cached_witness {
let aux = w.aux_slice();
let end = aux.len() - 6;
let inputs = &w.inputs_slice()[1..];

cs.extend_aux(aux);
cs.extend_inputs(inputs);

let scalars = &aux[end..];

let allocated = {
let mut bogus_cs = WitnessCS::new();

scalars
.iter()
.map(|scalar| AllocatedNum::alloc_infallible(&mut bogus_cs, || *scalar))
.collect::<Vec<_>>()
};

return Ok(allocated);
}
};
let input_expr = AllocatedPtr::by_index(0, z);
let input_env = AllocatedPtr::by_index(1, z);
let input_cont = AllocatedContPtr::by_index(2, z);

let count = self.count;

let (new_expr, new_env, new_cont) = match self.meta {
Meta::Lurk => match self.frames.as_ref() {
Some(frames) => {
let s = self.store.expect("store missing");
let g = GlobalAllocations::new(&mut cs.namespace(|| "global_allocations"), s)?;

self.synthesize_frames(cs, s, input_expr, input_env, input_cont, frames, &g)
}
None => {
assert!(self.store.is_none());
let s = Store::default();
let blank_frame = CircuitFrame::blank();
let frames = vec![blank_frame; count];

let g = GlobalAllocations::new(&mut cs.namespace(|| "global_allocations"), &s)?;

self.synthesize_frames(cs, &s, input_expr, input_env, input_cont, &frames, &g)
}
},
Meta::Coprocessor(z_ptr) => {
let c = self
.folding_config
.lang()
.get_coprocessor_from_zptr(&z_ptr)
.expect("coprocessor not found for a frame that requires one");
match self.frames.as_ref() {
Some(frames) => {
assert_eq!(1, frames.len());
let s = self.store.expect("store missing");
let g =
GlobalAllocations::new(&mut cs.namespace(|| "global_allocations"), s)?;

c.synthesize_step_circuit(
cs,
s,
&g,
&z_ptr,
&input_expr,
&input_env,
&input_cont,
&Boolean::Constant(false),
)?
}
None => {
assert!(self.store.is_none());
let s = Store::default();

let g =
GlobalAllocations::new(&mut cs.namespace(|| "global_allocations"), &s)?;

c.synthesize_step_circuit(
cs,
&s,
&g,
&z_ptr,
&input_expr,
&input_env,
&input_cont,
&Boolean::Constant(false),
)?
}
}
}
};

Ok(vec![
new_expr.tag().clone(),
new_expr.hash().clone(),
new_env.tag().clone(),
new_env.hash().clone(),
new_cont.tag().clone(),
new_cont.hash().clone(),
])
}
}

impl<'a, F: LurkField, C: Coprocessor<F>> MultiFrame<'a, F, C> {
#[allow(dead_code)] // TODO(huitseeker): is this used?
fn compute_witness(&self, s: &Store<F>) -> WitnessCS<F> {
let mut wcs = WitnessCS::new();

let input = self.input.unwrap();

use crate::tag::Tag;
let expr = s.hash_expr(&input.expr).unwrap();
let env = s.hash_expr(&input.env).unwrap();
let cont = s.hash_cont(&input.cont).unwrap();

let z_scalar = [
expr.tag().to_field(),
*expr.value(),
env.tag().to_field(),
*env.value(),
cont.tag().to_field(),
*cont.value(),
];

let mut bogus_cs = WitnessCS::<F>::new();
let z: Vec<AllocatedNum<F>> = z_scalar
.iter()
.map(|x| AllocatedNum::alloc(&mut bogus_cs, || Ok(*x)).unwrap())
.collect::<Vec<_>>();

let _ = self.clone().synthesize(&mut wcs, z.as_slice());

wcs
}
}
Loading

0 comments on commit 9e6a2fd

Please sign in to comment.