Skip to content

Commit

Permalink
Coroutines and Nova (#1115)
Browse files Browse the repository at this point in the history 
* WIP coroutine prove

* some simplifications

* public parameters

* finished proving

* updates; snark verification is failing

* circuit uniformity test

* expect values update

* small fix for non-witness CS

* Move `check_from_scope`
  • Loading branch information
@gabriel-barrett
gabriel-barrett authored Feb 16, 2024
1 parent 4906408 commit 6621d24
Show file tree
Hide file tree
Showing 4 changed files with 520 additions and 49 deletions.
2 changes: 1 addition & 1 deletion src/coprocessor/gadgets.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,7 @@ pub(crate) fn deconstruct_provenance<F: LurkField, CS: ConstraintSystem<F>>(
) -> Result<(AllocatedNum<F>, AllocatedPtr<F>, AllocatedNum<F>), SynthesisError> {
let prov_zptr = ZPtr::from_parts(
tag::Tag::Expr(ExprTag::Prov),
provenance.get_value().unwrap(),
provenance.get_value().unwrap_or(F::ZERO),
);
let prov_ptr = s.to_ptr(&prov_zptr);

Expand Down
20 changes: 10 additions & 10 deletions src/coroutine/memoset/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -319,21 +319,21 @@ mod test {
// Without internal insertions transcribed.

let (one_lookup_constraints, one_lookup_aux) =
test_lookup_circuit_aux(s, a, empty, expect!["3525"], expect!["3542"]);
test_lookup_circuit_aux(s, a, empty, expect!["3526"], expect!["3544"]);

test_lookup_circuit_aux(s, a, a_env, expect!["3525"], expect!["3542"]);
test_lookup_circuit_aux(s, a, a_env, expect!["3526"], expect!["3544"]);

let (two_lookup_constraints, two_lookup_aux) =
test_lookup_circuit_aux(s, b, a_env, expect!["6459"], expect!["6487"]);
test_lookup_circuit_aux(s, b, a_env, expect!["6461"], expect!["6491"]);

test_lookup_circuit_aux(s, b, b_env, expect!["3525"], expect!["3542"]);
test_lookup_circuit_aux(s, a, a2_env, expect!["3525"], expect!["3542"]);
test_lookup_circuit_aux(s, b, b_env, expect!["3526"], expect!["3544"]);
test_lookup_circuit_aux(s, a, a2_env, expect!["3526"], expect!["3544"]);

let (three_lookup_constraints, three_lookup_aux) =
test_lookup_circuit_aux(s, c, b_env, expect!["9393"], expect!["9432"]);
test_lookup_circuit_aux(s, c, b_env, expect!["9396"], expect!["9438"]);

test_lookup_circuit_aux(s, c, c_env, expect!["3525"], expect!["3542"]);
test_lookup_circuit_aux(s, c, a2_env, expect!["6459"], expect!["6487"]);
test_lookup_circuit_aux(s, c, c_env, expect!["3526"], expect!["3544"]);
test_lookup_circuit_aux(s, c, a2_env, expect!["6461"], expect!["6491"]);

let delta1_constraints = two_lookup_constraints - one_lookup_constraints;
let delta2_constraints = three_lookup_constraints - two_lookup_constraints;
Expand All @@ -342,7 +342,7 @@ mod test {
assert_eq!(delta1_constraints, delta2_constraints);

// This is the number of constraints per lookup.
expect_eq(delta1_constraints, expect!["2934"]);
expect_eq(delta1_constraints, expect!["2935"]);

// This is the number of constraints in the constant overhead.
expect_eq(overhead_constraints, expect!["591"]);
Expand All @@ -354,7 +354,7 @@ mod test {
assert_eq!(delta1_aux, delta2_aux);

// This is the number of aux per lookup.
expect_eq(delta1_aux, expect!["2945"]);
expect_eq(delta1_aux, expect!["2947"]);

// This is the number of aux in the constant overhead.
expect_eq(overhead_aux, expect!["597"]);
Expand Down
141 changes: 103 additions & 38 deletions src/coroutine/memoset/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,11 @@ use std::collections::{HashMap, HashSet};
use std::fmt::{Debug, Formatter};
use std::marker::PhantomData;

use bellpepper_core::{boolean::Boolean, num::AllocatedNum, ConstraintSystem, SynthesisError};
use bellpepper_core::{
boolean::{AllocatedBit, Boolean},
num::AllocatedNum,
ConstraintSystem, SynthesisError,
};
use once_cell::sync::OnceCell;

use crate::circuit::gadgets::{
Expand All @@ -58,6 +62,7 @@ pub use query::{CircuitQuery, Query};
mod demo;
mod env;
mod multiset;
mod prove;
mod query;

#[derive(Debug)]
Expand Down Expand Up @@ -379,6 +384,22 @@ impl<F: LurkField, Q: Query<F>> Scope<Q, LogMemo<F>, F> {

Ok(Provenance::new(query, result, dependencies))
}

fn init_memoset(&self, s: &Store<F>) -> Ptr {
let mut memoset = s.num(F::ZERO);
for kv in self.toplevel_insertions.iter() {
memoset = self.memoset.acc_add(&memoset, kv, s);
}
memoset
}

fn init_transcript(&self, s: &Store<F>) -> Ptr {
let mut transcript = Transcript::new(s);
for kv in self.toplevel_insertions.iter() {
transcript.add(s, *kv);
}
transcript.acc
}
}

#[derive(Debug, Clone)]
Expand All @@ -391,33 +412,58 @@ pub struct CircuitScope<F: LurkField, CM> {
acc: Option<AllocatedPtr<F>>,
}

#[derive(Clone)]
pub struct CoroutineCircuit<'a, F: LurkField, CM, Q> {
input: Option<Vec<Ptr>>,
provenances: HashMap<ZPtr<Tag, F>, ZPtr<Tag, F>>,
memoset: CM,
keys: Vec<Ptr>,
query_index: usize,
next_query_index: usize,
store: &'a Store<F>,
rc: usize,
_p: PhantomData<Q>,
}

// TODO: Make this generic rather than specialized to LogMemo.
// That will require a CircuitScopeTrait.
impl<'a, F: LurkField, Q: Query<F>> CoroutineCircuit<'a, F, LogMemoCircuit<F>, Q> {
impl<'a, F: LurkField, Q: Query<F>> CoroutineCircuit<'a, F, LogMemo<F>, Q> {
fn new(
input: Option<Vec<Ptr>>,
scope: &'a Scope<Q, LogMemo<F>, F>,
memoset: LogMemoCircuit<F>,
memoset: LogMemo<F>,
keys: Vec<Ptr>,
query_index: usize,
next_query_index: usize,
store: &'a Store<F>,
rc: usize,
) -> Self {
assert!(keys.len() <= rc);
Self {
input,
memoset,
provenances: scope.provenances(store).clone(), // FIXME
keys,
query_index,
next_query_index,
store,
rc,
_p: Default::default(),
}
}

fn blank(
query_index: usize,
store: &'a Store<F>,
rc: usize,
) -> CoroutineCircuit<'a, F, LogMemo<F>, Q> {
Self {
input: None,
memoset: Default::default(),
provenances: Default::default(),
keys: Default::default(),
query_index,
next_query_index: 0,
store,
rc,
_p: Default::default(),
Expand All @@ -426,8 +472,8 @@ impl<'a, F: LurkField, Q: Query<F>> CoroutineCircuit<'a, F, LogMemoCircuit<F>, Q

// This is a supernova::StepCircuit method.
// // TODO: we need to create a supernova::StepCircuit that will prove up to a fixed number of queries of a given type.
fn synthesize<CS: ConstraintSystem<F>>(
&mut self,
fn supernova_synthesize<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
z: &[AllocatedPtr<F>],
) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedPtr<F>>), SynthesisError> {
Expand All @@ -438,8 +484,12 @@ impl<'a, F: LurkField, Q: Query<F>> CoroutineCircuit<'a, F, LogMemoCircuit<F>, Q
unreachable!()
};

let memoset = LogMemoCircuit {
multiset: self.memoset.multiset.clone(),
r: r.hash().clone(),
};
let mut circuit_scope: CircuitScope<F, LogMemoCircuit<F>> =
CircuitScope::new(cs, g, self.store, self.memoset.clone(), &self.provenances);
CircuitScope::new(cs, g, self.store, memoset, &self.provenances);
circuit_scope.update_from_io(memoset_acc.clone(), transcript.clone(), r);

for (i, key) in self
Expand All @@ -460,12 +510,14 @@ impl<'a, F: LurkField, Q: Query<F>> CoroutineCircuit<'a, F, LogMemoCircuit<F>, Q
}

let (memoset_acc, transcript, r_num) = circuit_scope.io();
let r = AllocatedPtr::alloc_tag(ns!(cs, "r"), ExprTag::Num.to_field(), r_num)?;
let r = AllocatedPtr::alloc_tag(ns!(cs, "r"), ExprTag::Cons.to_field(), r_num)?;

let z_out = vec![c.clone(), e.clone(), k.clone(), memoset_acc, transcript, r];

let next_pc = None; // FIXME.
Ok((next_pc, z_out))
let next_pc = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "next_pc"), || {
F::from_u64(self.next_query_index as u64)
});
Ok((Some(next_pc), z_out))
}
}

Expand Down Expand Up @@ -722,7 +774,7 @@ impl<F: LurkField, Q: Query<F>> Scope<Q, LogMemo<F>, F> {

{
let (memoset_acc, transcript, r_num) = circuit_scope.io();
let r = AllocatedPtr::alloc_tag(ns!(cs, "r"), ExprTag::Num.to_field(), r_num)?;
let r = AllocatedPtr::from_parts(g.alloc_tag(cs, &ExprTag::Num).clone(), r_num);
let dummy = g.alloc_ptr(cs, &s.intern_nil(), s);
let mut z = vec![
dummy.clone(),
Expand All @@ -742,17 +794,20 @@ impl<F: LurkField, Q: Query<F>> Scope<Q, LogMemo<F>, F> {
// It shouldn't exist, when instead we have only the single NIVC circuit repeated multiple times.
let cs = ns!(cs, format!("chunk-{i}"));

let mut circuit: CoroutineCircuit<'_, F, LogMemoCircuit<F>, Q> =
CoroutineCircuit::new(
self,
memoset_circuit.clone(),
chunk.to_vec(),
*index,
s,
rc,
);

let (_next_pc, z_out) = circuit.synthesize(cs, &z)?;
// `next_query_index` is only relevant for SuperNova
let next_query_index = 0;
let circuit: CoroutineCircuit<'_, F, LogMemo<F>, Q> = CoroutineCircuit::new(
None,
self,
self.memoset.clone(),
chunk.to_vec(),
*index,
next_query_index,
s,
rc,
);

let (_next_pc, z_out) = circuit.supernova_synthesize(cs, &z)?;
{
let memoset_acc = &z_out[3];
let transcript = &z_out[4];
Expand Down Expand Up @@ -1058,15 +1113,18 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
Q::CQ::dummy_from_index(ns!(cs, "circuit_query"), s, index)
};

let not_dummy = key.is_some();
let not_dummy = Boolean::Is(AllocatedBit::alloc(
cs.namespace(|| "not_dummy"),
Some(key.is_some()),
)?);

self.synthesize_prove_query::<_, Q::CQ>(
cs,
g,
s,
&allocated_key,
&circuit_query,
not_dummy,
&not_dummy,
)?;
Ok(())
}
Expand All @@ -1078,7 +1136,7 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
s: &Store<F>,
allocated_key: &AllocatedPtr<F>,
circuit_query: &CQ,
not_dummy: bool,
not_dummy: &Boolean,
) -> Result<(), SynthesisError> {
let acc = self.acc.clone().unwrap();
let transcript = self.transcript.clone();
Expand All @@ -1101,13 +1159,13 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
// Prover can choose non-deterministically whether or not a given query is a dummy, to allow for padding.
let final_acc = AllocatedPtr::pick(
ns!(cs, "final_acc"),
&Boolean::Constant(not_dummy),
not_dummy,
&new_acc,
self.acc.as_ref().expect("acc missing"),
)?;
let final_transcript = CircuitTranscript::pick(
ns!(cs, "final_transcript"),
&Boolean::Constant(not_dummy),
not_dummy,
&new_transcript,
&self.transcript,
)?;
Expand Down Expand Up @@ -1203,6 +1261,13 @@ impl<F: LurkField> LogMemo<F> {
.clone()
.unwrap()
}

fn acc_add(&self, acc: &Ptr, kv: &Ptr, store: &Store<F>) -> Ptr {
let acc_num = store.expect_f(acc.get_atom().unwrap());
let kv_num = store.hash_raw_ptr(kv.raw()).0;
let element = self.map_to_element(kv_num).unwrap();
store.num(*acc_num + element)
}
}

impl<F: LurkField> MemoSet<F> for LogMemo<F> {
Expand Down Expand Up @@ -1310,24 +1375,24 @@ mod test {
#[test]
fn test_query() {
test_query_aux(
expect!["9451"],
expect!["9502"],
expect!["10034"],
expect!["10092"],
expect!["9456"],
expect!["9512"],
expect!["10039"],
expect!["10102"],
1,
);
test_query_aux(
expect!["11195"],
expect!["11255"],
expect!["11778"],
expect!["11845"],
expect!["11201"],
expect!["11263"],
expect!["11784"],
expect!["11853"],
3,
);
test_query_aux(
expect!["18248"],
expect!["18344"],
expect!["18831"],
expect!["18934"],
expect!["18258"],
expect!["18355"],
expect!["18841"],
expect!["18945"],
10,
)
}
Expand Down
Loading

1 comment on commit 6621d24

@github-actions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Benchmarks

Table of Contents

Overview

This benchmark report shows the Fibonacci GPU benchmark.
NVIDIA L4
Intel(R) Xeon(R) CPU @ 2.20GHz
32 vCPUs
125 GB RAM
Workflow run: https://github.com/lurk-lab/lurk-rs/actions/runs/7936555948

Benchmark Results

LEM Fibonacci Prove - rc = 100

ref=4906408d782aa7473a15024f118fbc8d898f982b ref=6621d24b3c7a9a30e4d806164aac98d7bfa97f35
num-100 1.45 s (✅ 1.00x) 1.45 s (✅ 1.00x slower)
num-200 2.77 s (✅ 1.00x) 2.78 s (✅ 1.00x slower)

LEM Fibonacci Prove - rc = 600

ref=4906408d782aa7473a15024f118fbc8d898f982b ref=6621d24b3c7a9a30e4d806164aac98d7bfa97f35
num-100 1.84 s (✅ 1.00x) 1.84 s (✅ 1.00x slower)
num-200 3.02 s (✅ 1.00x) 3.06 s (✅ 1.01x slower)

Made with criterion-table

Please sign in to comment.