From 50863bf3cd56c4d8acc14287bf76c747350b125d Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Wed, 10 Jan 2024 15:45:50 -0300 Subject: [PATCH 01/10] moved demo to own file --- src/coprocessor/memoset/demo.rs | 254 +++++++++++++++++++++++++++++++ src/coprocessor/memoset/mod.rs | 4 +- src/coprocessor/memoset/query.rs | 245 +---------------------------- 3 files changed, 258 insertions(+), 245 deletions(-) create mode 100644 src/coprocessor/memoset/demo.rs diff --git a/src/coprocessor/memoset/demo.rs b/src/coprocessor/memoset/demo.rs new file mode 100644 index 0000000000..92eb0e1fcd --- /dev/null +++ b/src/coprocessor/memoset/demo.rs @@ -0,0 +1,254 @@ +use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; + +use super::{ + query::{CircuitQuery, Query}, + CircuitScope, CircuitTranscript, LogMemo, Scope, +}; +use crate::circuit::gadgets::constraints::alloc_is_zero; +use crate::coprocessor::gadgets::construct_list; +use crate::coprocessor::AllocatedPtr; +use crate::field::LurkField; +use crate::lem::circuit::GlobalAllocator; +use crate::lem::{pointers::Ptr, store::Store}; +use crate::symbol::Symbol; +use crate::tag::{ExprTag, Tag}; + +#[derive(Debug, Clone)] +pub enum DemoQuery { + Factorial(Ptr), + Phantom(F), +} + +pub enum DemoCircuitQuery { + Factorial(AllocatedPtr), +} + +impl Query for DemoQuery { + // DemoQuery and Scope depend on each other. + fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr { + match self { + Self::Factorial(n) => { + let n_zptr = s.hash_ptr(n); + let n = n_zptr.value(); + + if *n == F::ZERO { + s.num(F::ONE) + } else { + let m_ptr = self.recursive_eval(scope, s, Self::Factorial(s.num(*n - F::ONE))); + let m_zptr = s.hash_ptr(&m_ptr); + let m = m_zptr.value(); + + s.num(*n * m) + } + } + _ => unreachable!(), + } + } + + fn recursive_eval( + &self, + scope: &mut Scope>, + s: &Store, + subquery: Self, + ) -> Ptr { + scope.query_recursively(s, self, subquery) + } + + fn symbol(&self) -> Symbol { + match self { + Self::Factorial(_) => Symbol::sym(&["lurk", "user", "factorial"]), + _ => unreachable!(), + } + } + + fn from_ptr(s: &Store, ptr: &Ptr) -> Option { + let (head, body) = s.car_cdr(ptr).expect("query should be cons"); + let sym = s.fetch_sym(&head).expect("head should be sym"); + + if sym == Symbol::sym(&["lurk", "user", "factorial"]) { + let (num, _) = s.car_cdr(&body).expect("query body should be cons"); + Some(Self::Factorial(num)) + } else { + None + } + } + + fn to_ptr(&self, s: &Store) -> Ptr { + match self { + Self::Factorial(n) => { + let factorial = s.intern_symbol(&self.symbol()); + + s.list(vec![factorial, *n]) + } + _ => unreachable!(), + } + } + + fn index(&self) -> usize { + match self { + Self::Factorial(_) => 0, + _ => unreachable!(), + } + } +} + +impl CircuitQuery for DemoCircuitQuery { + type Q = DemoQuery; + + fn dummy_query_variant(&self, s: &Store) -> Self::Q { + match self { + Self::Factorial(_) => Self::Q::Factorial(s.num(F::ZERO)), + } + } + + fn synthesize_eval>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + scope: &mut CircuitScope>, + acc: &AllocatedPtr, + transcript: &CircuitTranscript, + ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + match self { + // TODO: Factor out the recursive boilerplate so individual queries can just implement their distinct logic + // using a sane framework. + Self::Factorial(n) => { + // FIXME: Check n tag or decide not to. + let base_case_f = g.alloc_const(cs, F::ONE); + let base_case = AllocatedPtr::alloc_tag( + &mut cs.namespace(|| "base_case"), + ExprTag::Num.to_field(), + base_case_f.clone(), + )?; + + let n_is_zero = alloc_is_zero(&mut cs.namespace(|| "n_is_zero"), n.hash())?; + + let (recursive_result, recursive_acc, recursive_transcript) = { + let new_n = AllocatedNum::alloc(&mut cs.namespace(|| "new_n"), || { + n.hash() + .get_value() + .map(|n| n - F::ONE) + .ok_or(SynthesisError::AssignmentMissing) + })?; + + // new_n * 1 = n - 1 + cs.enforce( + || "enforce_new_n", + |lc| lc + new_n.get_variable(), + |lc| lc + CS::one(), + |lc| lc + n.hash().get_variable() - CS::one(), + ); + + let subquery = { + let symbol = + g.alloc_ptr(cs, &store.intern_symbol(&self.symbol(store)), store); + + let new_num = AllocatedPtr::alloc_tag( + &mut cs.namespace(|| "new_num"), + ExprTag::Num.to_field(), + new_n, + )?; + construct_list( + &mut cs.namespace(|| "subquery"), + g, + store, + &[&symbol, &new_num], + None, + )? + }; + + let (sub_result, new_acc, new_transcript) = scope.synthesize_query( + &mut cs.namespace(|| "recursive query"), + g, + store, + &subquery, + acc, + transcript, + &n_is_zero.not(), + )?; + + let result_f = n.hash().mul( + &mut cs.namespace(|| "incremental multiplication"), + sub_result.hash(), + )?; + + let result = AllocatedPtr::alloc_tag( + &mut cs.namespace(|| "result"), + ExprTag::Num.to_field(), + result_f, + )?; + + (result, new_acc, new_transcript) + }; + + let value = AllocatedPtr::pick( + &mut cs.namespace(|| "pick value"), + &n_is_zero, + &base_case, + &recursive_result, + )?; + + let acc = AllocatedPtr::pick( + &mut cs.namespace(|| "pick acc"), + &n_is_zero, + acc, + &recursive_acc, + )?; + + let transcript = CircuitTranscript::pick( + &mut cs.namespace(|| "pick recursive_transcript"), + &n_is_zero, + transcript, + &recursive_transcript, + )?; + + Ok((value, acc, transcript)) + } + } + } + + fn from_ptr>( + cs: &mut CS, + s: &Store, + ptr: &Ptr, + ) -> Result, SynthesisError> { + let query = Self::Q::from_ptr(s, ptr); + Ok(if let Some(q) = query { + match q { + Self::Q::Factorial(n) => Some(Self::Factorial(AllocatedPtr::alloc(cs, || { + Ok(s.hash_ptr(&n)) + })?)), + _ => unreachable!(), + } + } else { + None + }) + } +} + +#[cfg(test)] +mod test { + use super::*; + + use ff::Field; + use pasta_curves::pallas::Scalar as F; + + #[test] + fn test_factorial() { + let s = Store::default(); + let mut scope: Scope, LogMemo> = Scope::default(); + let zero = s.num(F::ZERO); + let one = s.num(F::ONE); + let two = s.num(F::from_u64(2)); + let three = s.num(F::from_u64(3)); + let four = s.num(F::from_u64(4)); + let six = s.num(F::from_u64(6)); + let twenty_four = s.num(F::from_u64(24)); + assert_eq!(one, DemoQuery::Factorial(zero).eval(&s, &mut scope)); + assert_eq!(one, DemoQuery::Factorial(one).eval(&s, &mut scope)); + assert_eq!(two, DemoQuery::Factorial(two).eval(&s, &mut scope)); + assert_eq!(six, DemoQuery::Factorial(three).eval(&s, &mut scope)); + assert_eq!(twenty_four, DemoQuery::Factorial(four).eval(&s, &mut scope)); + } +} diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index ced6ee354f..8eb3ef2ae4 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -46,9 +46,11 @@ use crate::lem::{pointers::Ptr, store::Store}; use crate::tag::{ExprTag, Tag as XTag}; use crate::z_ptr::ZPtr; +use demo::DemoCircuitQuery; use multiset::MultiSet; -use query::{CircuitQuery, DemoCircuitQuery, Query}; +use query::{CircuitQuery, Query}; +mod demo; mod multiset; mod query; diff --git a/src/coprocessor/memoset/query.rs b/src/coprocessor/memoset/query.rs index fe85db927e..87c80c8074 100644 --- a/src/coprocessor/memoset/query.rs +++ b/src/coprocessor/memoset/query.rs @@ -1,14 +1,11 @@ -use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; +use bellpepper_core::{ConstraintSystem, SynthesisError}; use super::{CircuitScope, CircuitTranscript, LogMemo, Scope}; -use crate::circuit::gadgets::constraints::alloc_is_zero; -use crate::coprocessor::gadgets::construct_list; use crate::coprocessor::AllocatedPtr; use crate::field::LurkField; use crate::lem::circuit::GlobalAllocator; use crate::lem::{pointers::Ptr, store::Store}; use crate::symbol::Symbol; -use crate::tag::{ExprTag, Tag}; pub trait Query where @@ -64,243 +61,3 @@ where fn dummy_query_variant(&self, s: &Store) -> Self::Q; } - -#[derive(Debug, Clone)] -pub enum DemoQuery { - Factorial(Ptr), - Phantom(F), -} - -pub enum DemoCircuitQuery { - Factorial(AllocatedPtr), -} - -impl Query for DemoQuery { - // DemoQuery and Scope depend on each other. - fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr { - match self { - Self::Factorial(n) => { - let n_zptr = s.hash_ptr(n); - let n = n_zptr.value(); - - if *n == F::ZERO { - s.num(F::ONE) - } else { - let m_ptr = self.recursive_eval(scope, s, Self::Factorial(s.num(*n - F::ONE))); - let m_zptr = s.hash_ptr(&m_ptr); - let m = m_zptr.value(); - - s.num(*n * m) - } - } - _ => unreachable!(), - } - } - - fn recursive_eval( - &self, - scope: &mut Scope>, - s: &Store, - subquery: Self, - ) -> Ptr { - scope.query_recursively(s, self, subquery) - } - - fn symbol(&self) -> Symbol { - match self { - Self::Factorial(_) => Symbol::sym(&["lurk", "user", "factorial"]), - _ => unreachable!(), - } - } - - fn from_ptr(s: &Store, ptr: &Ptr) -> Option { - let (head, body) = s.car_cdr(ptr).expect("query should be cons"); - let sym = s.fetch_sym(&head).expect("head should be sym"); - - if sym == Symbol::sym(&["lurk", "user", "factorial"]) { - let (num, _) = s.car_cdr(&body).expect("query body should be cons"); - Some(Self::Factorial(num)) - } else { - None - } - } - - fn to_ptr(&self, s: &Store) -> Ptr { - match self { - Self::Factorial(n) => { - let factorial = s.intern_symbol(&self.symbol()); - - s.list(vec![factorial, *n]) - } - _ => unreachable!(), - } - } - - fn index(&self) -> usize { - match self { - Self::Factorial(_) => 0, - _ => unreachable!(), - } - } -} - -impl CircuitQuery for DemoCircuitQuery { - type Q = DemoQuery; - - fn dummy_query_variant(&self, s: &Store) -> Self::Q { - match self { - Self::Factorial(_) => Self::Q::Factorial(s.num(F::ZERO)), - } - } - - fn synthesize_eval>( - &self, - cs: &mut CS, - g: &GlobalAllocator, - store: &Store, - scope: &mut CircuitScope>, - acc: &AllocatedPtr, - transcript: &CircuitTranscript, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { - match self { - // TODO: Factor out the recursive boilerplate so individual queries can just implement their distinct logic - // using a sane framework. - Self::Factorial(n) => { - // FIXME: Check n tag or decide not to. - let base_case_f = g.alloc_const(cs, F::ONE); - let base_case = AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "base_case"), - ExprTag::Num.to_field(), - base_case_f.clone(), - )?; - - let n_is_zero = alloc_is_zero(&mut cs.namespace(|| "n_is_zero"), n.hash())?; - - let (recursive_result, recursive_acc, recursive_transcript) = { - let new_n = AllocatedNum::alloc(&mut cs.namespace(|| "new_n"), || { - n.hash() - .get_value() - .map(|n| n - F::ONE) - .ok_or(SynthesisError::AssignmentMissing) - })?; - - // new_n * 1 = n - 1 - cs.enforce( - || "enforce_new_n", - |lc| lc + new_n.get_variable(), - |lc| lc + CS::one(), - |lc| lc + n.hash().get_variable() - CS::one(), - ); - - let subquery = { - let symbol = - g.alloc_ptr(cs, &store.intern_symbol(&self.symbol(store)), store); - - let new_num = AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "new_num"), - ExprTag::Num.to_field(), - new_n, - )?; - construct_list( - &mut cs.namespace(|| "subquery"), - g, - store, - &[&symbol, &new_num], - None, - )? - }; - - let (sub_result, new_acc, new_transcript) = scope.synthesize_query( - &mut cs.namespace(|| "recursive query"), - g, - store, - &subquery, - acc, - transcript, - &n_is_zero.not(), - )?; - - let result_f = n.hash().mul( - &mut cs.namespace(|| "incremental multiplication"), - sub_result.hash(), - )?; - - let result = AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "result"), - ExprTag::Num.to_field(), - result_f, - )?; - - (result, new_acc, new_transcript) - }; - - let value = AllocatedPtr::pick( - &mut cs.namespace(|| "pick value"), - &n_is_zero, - &base_case, - &recursive_result, - )?; - - let acc = AllocatedPtr::pick( - &mut cs.namespace(|| "pick acc"), - &n_is_zero, - acc, - &recursive_acc, - )?; - - let transcript = CircuitTranscript::pick( - &mut cs.namespace(|| "pick recursive_transcript"), - &n_is_zero, - transcript, - &recursive_transcript, - )?; - - Ok((value, acc, transcript)) - } - } - } - - fn from_ptr>( - cs: &mut CS, - s: &Store, - ptr: &Ptr, - ) -> Result, SynthesisError> { - let query = Self::Q::from_ptr(s, ptr); - Ok(if let Some(q) = query { - match q { - Self::Q::Factorial(n) => Some(Self::Factorial(AllocatedPtr::alloc(cs, || { - Ok(s.hash_ptr(&n)) - })?)), - _ => unreachable!(), - } - } else { - None - }) - } -} - -#[cfg(test)] -mod test { - use super::*; - - use ff::Field; - use pasta_curves::pallas::Scalar as F; - - #[test] - fn test_factorial() { - let s = Store::default(); - let mut scope: Scope, LogMemo> = Scope::default(); - let zero = s.num(F::ZERO); - let one = s.num(F::ONE); - let two = s.num(F::from_u64(2)); - let three = s.num(F::from_u64(3)); - let four = s.num(F::from_u64(4)); - let six = s.num(F::from_u64(6)); - let twenty_four = s.num(F::from_u64(24)); - assert_eq!(one, DemoQuery::Factorial(zero).eval(&s, &mut scope)); - assert_eq!(one, DemoQuery::Factorial(one).eval(&s, &mut scope)); - assert_eq!(two, DemoQuery::Factorial(two).eval(&s, &mut scope)); - assert_eq!(six, DemoQuery::Factorial(three).eval(&s, &mut scope)); - assert_eq!(twenty_four, DemoQuery::Factorial(four).eval(&s, &mut scope)); - } -} From fb38df012e95d5017c9a28ec7be674d46ea96646 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 11 Jan 2024 15:24:15 -0300 Subject: [PATCH 02/10] make mod generic --- src/coprocessor/memoset/demo.rs | 8 +- src/coprocessor/memoset/mod.rs | 138 ++++++++++++++----------------- src/coprocessor/memoset/query.rs | 6 +- 3 files changed, 72 insertions(+), 80 deletions(-) diff --git a/src/coprocessor/memoset/demo.rs b/src/coprocessor/memoset/demo.rs index 92eb0e1fcd..5165287483 100644 --- a/src/coprocessor/memoset/demo.rs +++ b/src/coprocessor/memoset/demo.rs @@ -13,13 +13,15 @@ use crate::lem::{pointers::Ptr, store::Store}; use crate::symbol::Symbol; use crate::tag::{ExprTag, Tag}; +#[allow(dead_code)] #[derive(Debug, Clone)] -pub enum DemoQuery { +pub(crate) enum DemoQuery { Factorial(Ptr), Phantom(F), } -pub enum DemoCircuitQuery { +#[derive(Debug, Clone)] +pub(crate) enum DemoCircuitQuery { Factorial(AllocatedPtr), } @@ -106,7 +108,7 @@ impl CircuitQuery for DemoCircuitQuery { cs: &mut CS, g: &GlobalAllocator, store: &Store, - scope: &mut CircuitScope>, + scope: &mut CircuitScope>, acc: &AllocatedPtr, transcript: &CircuitTranscript, ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index 8eb3ef2ae4..fea600760f 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -46,7 +46,6 @@ use crate::lem::{pointers::Ptr, store::Store}; use crate::tag::{ExprTag, Tag as XTag}; use crate::z_ptr::ZPtr; -use demo::DemoCircuitQuery; use multiset::MultiSet; use query::{CircuitQuery, Query}; @@ -54,9 +53,6 @@ mod demo; mod multiset; mod query; -type ScopeCircuitQuery = DemoCircuitQuery; -type ScopeQuery = as CircuitQuery>::Q; - #[derive(Clone, Debug)] pub struct Transcript { acc: Ptr, @@ -201,7 +197,7 @@ pub struct Scope { _p: PhantomData<(F, Q)>, } -impl Default for Scope, LogMemo> { +impl Default for Scope> { fn default() -> Self { Self { memoset: Default::default(), @@ -215,17 +211,17 @@ impl Default for Scope, LogMemo> { } } -pub struct CircuitScope, M: MemoSet> { +pub struct CircuitScope, M: MemoSet> { memoset: M, /// k -> v queries: HashMap, ZPtr>, /// k -> allocated v transcript: CircuitTranscript, acc: Option>, - _p: PhantomData, + _p: PhantomData, } -impl Scope, LogMemo> { +impl> Scope> { pub fn query(&mut self, s: &Store, form: Ptr) -> Ptr { let (response, kv_ptr) = self.query_aux(s, form); @@ -234,12 +230,7 @@ impl Scope, LogMemo> { response } - fn query_recursively( - &mut self, - s: &Store, - parent: &ScopeQuery, - child: ScopeQuery, - ) -> Ptr { + fn query_recursively(&mut self, s: &Store, parent: &Q, child: Q) -> Ptr { let form = child.to_ptr(s); self.internal_insertions.push(form); @@ -255,7 +246,7 @@ impl Scope, LogMemo> { fn query_aux(&mut self, s: &Store, form: Ptr) -> (Ptr, Ptr) { let response = self.queries.get(&form).cloned().unwrap_or_else(|| { - let query = ScopeQuery::from_ptr(s, &form).expect("invalid query"); + let query = Q::from_ptr(s, &form).expect("invalid query"); let evaluated = query.eval(s, self); @@ -301,9 +292,7 @@ impl Scope, LogMemo> { insertions.sort_by_key(|kv| { let (key, _) = s.car_cdr(kv).unwrap(); - ScopeQuery::::from_ptr(s, &key) - .expect("invalid query") - .index() + Q::from_ptr(s, &key).expect("invalid query").index() }); for kv in self.toplevel_insertions.iter() { @@ -350,61 +339,14 @@ impl Scope, LogMemo> { (transcript, unique_keys) } - - pub fn synthesize>( - &mut self, - cs: &mut CS, - g: &mut GlobalAllocator, - s: &Store, - ) -> Result<(), SynthesisError> { - self.ensure_transcript_finalized(s); - - { - let circuit_scope = - &mut CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, self); - circuit_scope.init(cs, g, s); - { - self.synthesize_insert_toplevel_queries(circuit_scope, cs, g, s)?; - self.synthesize_prove_all_queries(circuit_scope, cs, g, s)?; - } - circuit_scope.finalize(cs, g); - Ok(()) - } - } - - fn synthesize_insert_toplevel_queries>( - &mut self, - circuit_scope: &mut CircuitScope, LogMemo>, - cs: &mut CS, - g: &mut GlobalAllocator, - s: &Store, - ) -> Result<(), SynthesisError> { - for (i, kv) in self.toplevel_insertions.iter().enumerate() { - circuit_scope.synthesize_toplevel_query(cs, g, s, i, kv)?; - } - Ok(()) - } - - fn synthesize_prove_all_queries>( - &mut self, - circuit_scope: &mut CircuitScope, LogMemo>, - cs: &mut CS, - g: &mut GlobalAllocator, - s: &Store, - ) -> Result<(), SynthesisError> { - for (i, kv) in self.all_insertions.iter().enumerate() { - circuit_scope.synthesize_prove_query(cs, g, s, i, kv)?; - } - Ok(()) - } } -impl> CircuitScope> { - fn from_scope>( +impl> CircuitScope> { + pub fn from_scope>( cs: &mut CS, g: &mut GlobalAllocator, s: &Store, - scope: &Scope>, + scope: &Scope>, ) -> Self { let queries = scope .queries @@ -434,6 +376,23 @@ impl> CircuitScope> { self.transcript = CircuitTranscript::new(cs, g, s); } + pub fn synthesize>( + &mut self, + scope: &mut Scope>, + cs: &mut CS, + g: &mut GlobalAllocator, + s: &Store, + ) -> Result<(), SynthesisError> { + scope.ensure_transcript_finalized(s); + self.init(cs, g, s); + { + self.synthesize_insert_toplevel_queries(scope, cs, g, s)?; + self.synthesize_prove_all_queries(scope, cs, g, s)?; + } + self.finalize(cs, g); + Ok(()) + } + fn synthesize_insert_query>( &self, cs: &mut CS, @@ -537,9 +496,20 @@ impl> CircuitScope> { Ok((value, new_acc, new_insertion_transcript)) } -} -impl CircuitScope, LogMemo> { + fn synthesize_insert_toplevel_queries>( + &mut self, + scope: &mut Scope>, + cs: &mut CS, + g: &mut GlobalAllocator, + s: &Store, + ) -> Result<(), SynthesisError> { + for (i, kv) in scope.toplevel_insertions.iter().enumerate() { + self.synthesize_toplevel_query(cs, g, s, i, kv)?; + } + Ok(()) + } + fn synthesize_toplevel_query>( &mut self, cs: &mut CS, @@ -577,6 +547,19 @@ impl CircuitScope, LogMemo> { Ok(()) } + fn synthesize_prove_all_queries>( + &mut self, + scope: &mut Scope>, + cs: &mut CS, + g: &mut GlobalAllocator, + s: &Store, + ) -> Result<(), SynthesisError> { + for (i, kv) in scope.all_insertions.iter().enumerate() { + self.synthesize_prove_query(cs, g, s, i, kv)?; + } + Ok(()) + } + fn synthesize_prove_query>( &mut self, cs: &mut CS, @@ -594,8 +577,7 @@ impl CircuitScope, LogMemo> { ) .unwrap(); - let circuit_query = - ScopeCircuitQuery::from_ptr(&mut cs.namespace(|| "circuit_query"), s, key).unwrap(); + let circuit_query = CQ::from_ptr(&mut cs.namespace(|| "circuit_query"), s, key).unwrap(); let acc = self.acc.clone().unwrap(); let transcript = self.transcript.clone(); @@ -763,10 +745,14 @@ mod test { use crate::state::State; use bellpepper_core::{test_cs::TestConstraintSystem, Comparable}; + use demo::DemoCircuitQuery; use expect_test::{expect, Expect}; use pasta_curves::pallas::Scalar as F; use std::default::Default; + type ScopeCircuitQuery = DemoCircuitQuery; + type ScopeQuery = as CircuitQuery>::Q; + #[test] fn test_query() { let s = &Store::::default(); @@ -797,8 +783,10 @@ mod test { let cs = &mut TestConstraintSystem::new(); let g = &mut GlobalAllocator::default(); + let mut circuit_scope: CircuitScope<_, ScopeCircuitQuery, _> = + CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, &scope); - scope.synthesize(cs, g, s).unwrap(); + circuit_scope.synthesize(&mut scope, cs, g, s).unwrap(); println!( "transcript: {}", @@ -836,8 +824,10 @@ mod test { let cs = &mut TestConstraintSystem::new(); let g = &mut GlobalAllocator::default(); + let mut circuit_scope: CircuitScope<_, ScopeCircuitQuery, _> = + CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, &scope); - scope.synthesize(cs, g, s).unwrap(); + circuit_scope.synthesize(&mut scope, cs, g, s).unwrap(); expect_eq(cs.num_constraints(), expect!["11408"]); expect_eq(cs.aux().len(), expect!["11445"]); diff --git a/src/coprocessor/memoset/query.rs b/src/coprocessor/memoset/query.rs index 87c80c8074..a2a8bb7b8f 100644 --- a/src/coprocessor/memoset/query.rs +++ b/src/coprocessor/memoset/query.rs @@ -9,7 +9,7 @@ use crate::symbol::Symbol; pub trait Query where - Self: Sized, + Self: Sized + Clone, { fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr; fn recursive_eval( @@ -31,7 +31,7 @@ where #[allow(unreachable_pub)] pub trait CircuitQuery where - Self: Sized, + Self: Sized + Clone, { type Q: Query; @@ -40,7 +40,7 @@ where cs: &mut CS, g: &GlobalAllocator, store: &Store, - scope: &mut CircuitScope>, + scope: &mut CircuitScope>, acc: &AllocatedPtr, transcript: &CircuitTranscript, ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError>; From 47db887c6a5269898a8fcfc08f434c69dc00d3c5 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 11 Jan 2024 21:24:54 -0300 Subject: [PATCH 03/10] scope synthesize --- src/coprocessor/memoset/mod.rs | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index fea600760f..717d31ae3d 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -339,6 +339,24 @@ impl> Scope> { (transcript, unique_keys) } + + pub fn synthesize, CQ: CircuitQuery>( + &mut self, + cs: &mut CS, + g: &mut GlobalAllocator, + s: &Store, + ) -> Result<(), SynthesisError> { + self.ensure_transcript_finalized(s); + let mut circuit_scope: CircuitScope<_, CQ, _> = + CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, self); + circuit_scope.init(cs, g, s); + { + circuit_scope.synthesize_insert_toplevel_queries(self, cs, g, s)?; + circuit_scope.synthesize_prove_all_queries(self, cs, g, s)?; + } + circuit_scope.finalize(cs, g); + Ok(()) + } } impl> CircuitScope> { @@ -824,10 +842,10 @@ mod test { let cs = &mut TestConstraintSystem::new(); let g = &mut GlobalAllocator::default(); - let mut circuit_scope: CircuitScope<_, ScopeCircuitQuery, _> = - CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, &scope); - circuit_scope.synthesize(&mut scope, cs, g, s).unwrap(); + scope + .synthesize::, ScopeCircuitQuery>(cs, g, s) + .unwrap(); expect_eq(cs.num_constraints(), expect!["11408"]); expect_eq(cs.aux().len(), expect!["11445"]); From 58357410f5c0e5ab7e43c7a8369f551c72c21890 Mon Sep 17 00:00:00 2001 From: porcuquine Date: Thu, 11 Jan 2024 16:55:50 -0800 Subject: [PATCH 04/10] Be more anonymous. --- src/coprocessor/memoset/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index 717d31ae3d..abb3712ee4 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -844,7 +844,7 @@ mod test { let g = &mut GlobalAllocator::default(); scope - .synthesize::, ScopeCircuitQuery>(cs, g, s) + .synthesize::<_, ScopeCircuitQuery>(cs, g, s) .unwrap(); expect_eq(cs.num_constraints(), expect!["11408"]); From 7f25be3a4b86aa60e7005dbbf6a9231fe86fc179 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 11 Jan 2024 23:27:00 -0300 Subject: [PATCH 05/10] removed circuit scope synthesize --- src/coprocessor/memoset/mod.rs | 25 ++++--------------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index abb3712ee4..892181bc5d 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -194,7 +194,7 @@ pub struct Scope { internal_insertions: Vec, /// unique keys all_insertions: Vec, - _p: PhantomData<(F, Q)>, + _p: PhantomData, } impl Default for Scope> { @@ -394,23 +394,6 @@ impl> CircuitScope> { self.transcript = CircuitTranscript::new(cs, g, s); } - pub fn synthesize>( - &mut self, - scope: &mut Scope>, - cs: &mut CS, - g: &mut GlobalAllocator, - s: &Store, - ) -> Result<(), SynthesisError> { - scope.ensure_transcript_finalized(s); - self.init(cs, g, s); - { - self.synthesize_insert_toplevel_queries(scope, cs, g, s)?; - self.synthesize_prove_all_queries(scope, cs, g, s)?; - } - self.finalize(cs, g); - Ok(()) - } - fn synthesize_insert_query>( &self, cs: &mut CS, @@ -801,10 +784,10 @@ mod test { let cs = &mut TestConstraintSystem::new(); let g = &mut GlobalAllocator::default(); - let mut circuit_scope: CircuitScope<_, ScopeCircuitQuery, _> = - CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, &scope); - circuit_scope.synthesize(&mut scope, cs, g, s).unwrap(); + scope + .synthesize::<_, ScopeCircuitQuery>(cs, g, s) + .unwrap(); println!( "transcript: {}", From 0f5441fa6c41f1ec443c253b343d870dbba5f489 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 12 Jan 2024 00:15:38 -0300 Subject: [PATCH 06/10] reverted associated types --- src/coprocessor/memoset/demo.rs | 21 +++++++++----------- src/coprocessor/memoset/mod.rs | 33 +++++++++++++------------------- src/coprocessor/memoset/query.rs | 12 ++++-------- 3 files changed, 26 insertions(+), 40 deletions(-) diff --git a/src/coprocessor/memoset/demo.rs b/src/coprocessor/memoset/demo.rs index 5165287483..3b76aad52f 100644 --- a/src/coprocessor/memoset/demo.rs +++ b/src/coprocessor/memoset/demo.rs @@ -26,6 +26,8 @@ pub(crate) enum DemoCircuitQuery { } impl Query for DemoQuery { + type CQ = DemoCircuitQuery; + // DemoQuery and Scope depend on each other. fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr { match self { @@ -95,14 +97,6 @@ impl Query for DemoQuery { } impl CircuitQuery for DemoCircuitQuery { - type Q = DemoQuery; - - fn dummy_query_variant(&self, s: &Store) -> Self::Q { - match self { - Self::Factorial(_) => Self::Q::Factorial(s.num(F::ZERO)), - } - } - fn synthesize_eval>( &self, cs: &mut CS, @@ -143,8 +137,7 @@ impl CircuitQuery for DemoCircuitQuery { ); let subquery = { - let symbol = - g.alloc_ptr(cs, &store.intern_symbol(&self.symbol(store)), store); + let symbol = g.alloc_ptr(cs, &self.symbol_ptr(store), store); let new_num = AllocatedPtr::alloc_tag( &mut cs.namespace(|| "new_num"), @@ -215,10 +208,10 @@ impl CircuitQuery for DemoCircuitQuery { s: &Store, ptr: &Ptr, ) -> Result, SynthesisError> { - let query = Self::Q::from_ptr(s, ptr); + let query = DemoQuery::from_ptr(s, ptr); Ok(if let Some(q) = query { match q { - Self::Q::Factorial(n) => Some(Self::Factorial(AllocatedPtr::alloc(cs, || { + DemoQuery::Factorial(n) => Some(Self::Factorial(AllocatedPtr::alloc(cs, || { Ok(s.hash_ptr(&n)) })?)), _ => unreachable!(), @@ -227,6 +220,10 @@ impl CircuitQuery for DemoCircuitQuery { None }) } + + fn symbol(&self) -> Symbol { + todo!() + } } #[cfg(test)] diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index 892181bc5d..816ad86434 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -340,14 +340,14 @@ impl> Scope> { (transcript, unique_keys) } - pub fn synthesize, CQ: CircuitQuery>( + pub fn synthesize>( &mut self, cs: &mut CS, g: &mut GlobalAllocator, s: &Store, ) -> Result<(), SynthesisError> { self.ensure_transcript_finalized(s); - let mut circuit_scope: CircuitScope<_, CQ, _> = + let mut circuit_scope: CircuitScope<_, Q::CQ, _> = CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, self); circuit_scope.init(cs, g, s); { @@ -360,11 +360,11 @@ impl> Scope> { } impl> CircuitScope> { - pub fn from_scope>( + fn from_scope, Q: Query>( cs: &mut CS, g: &mut GlobalAllocator, s: &Store, - scope: &Scope>, + scope: &Scope>, ) -> Self { let queries = scope .queries @@ -498,9 +498,9 @@ impl> CircuitScope> { Ok((value, new_acc, new_insertion_transcript)) } - fn synthesize_insert_toplevel_queries>( + fn synthesize_insert_toplevel_queries, Q: Query>( &mut self, - scope: &mut Scope>, + scope: &mut Scope>, cs: &mut CS, g: &mut GlobalAllocator, s: &Store, @@ -548,9 +548,9 @@ impl> CircuitScope> { Ok(()) } - fn synthesize_prove_all_queries>( + fn synthesize_prove_all_queries, Q: Query>( &mut self, - scope: &mut Scope>, + scope: &mut Scope>, cs: &mut CS, g: &mut GlobalAllocator, s: &Store, @@ -746,18 +746,15 @@ mod test { use crate::state::State; use bellpepper_core::{test_cs::TestConstraintSystem, Comparable}; - use demo::DemoCircuitQuery; + use demo::DemoQuery; use expect_test::{expect, Expect}; use pasta_curves::pallas::Scalar as F; use std::default::Default; - type ScopeCircuitQuery = DemoCircuitQuery; - type ScopeQuery = as CircuitQuery>::Q; - #[test] fn test_query() { let s = &Store::::default(); - let mut scope: Scope, LogMemo> = Scope::default(); + let mut scope: Scope, LogMemo> = Scope::default(); let state = State::init_lurk_state(); let fact_4 = s.read_with_default_state("(factorial 4)").unwrap(); @@ -785,9 +782,7 @@ mod test { let cs = &mut TestConstraintSystem::new(); let g = &mut GlobalAllocator::default(); - scope - .synthesize::<_, ScopeCircuitQuery>(cs, g, s) - .unwrap(); + scope.synthesize(cs, g, s).unwrap(); println!( "transcript: {}", @@ -810,7 +805,7 @@ mod test { assert!(cs.is_satisfied()); } { - let mut scope: Scope, LogMemo> = Scope::default(); + let mut scope: Scope, LogMemo> = Scope::default(); scope.query(s, fact_4); scope.query(s, fact_3); @@ -826,9 +821,7 @@ mod test { let cs = &mut TestConstraintSystem::new(); let g = &mut GlobalAllocator::default(); - scope - .synthesize::<_, ScopeCircuitQuery>(cs, g, s) - .unwrap(); + scope.synthesize(cs, g, s).unwrap(); expect_eq(cs.num_constraints(), expect!["11408"]); expect_eq(cs.aux().len(), expect!["11445"]); diff --git a/src/coprocessor/memoset/query.rs b/src/coprocessor/memoset/query.rs index a2a8bb7b8f..0ef04d9607 100644 --- a/src/coprocessor/memoset/query.rs +++ b/src/coprocessor/memoset/query.rs @@ -11,6 +11,8 @@ pub trait Query where Self: Sized + Clone, { + type CQ: CircuitQuery; + fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr; fn recursive_eval( &self, @@ -33,8 +35,6 @@ pub trait CircuitQuery where Self: Sized + Clone, { - type Q: Query; - fn synthesize_eval>( &self, cs: &mut CS, @@ -45,12 +45,10 @@ where transcript: &CircuitTranscript, ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError>; - fn symbol(&self, s: &Store) -> Symbol { - self.dummy_query_variant(s).symbol() - } + fn symbol(&self) -> Symbol; fn symbol_ptr(&self, s: &Store) -> Ptr { - self.dummy_query_variant(s).symbol_ptr(s) + s.intern_symbol(&self.symbol()) } fn from_ptr>( @@ -58,6 +56,4 @@ where s: &Store, ptr: &Ptr, ) -> Result, SynthesisError>; - - fn dummy_query_variant(&self, s: &Store) -> Self::Q; } From 1d40c7bbfe1c5373193409d3a4809e6aa3444db8 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 12 Jan 2024 00:19:21 -0300 Subject: [PATCH 07/10] removed unreachable_pub --- src/coprocessor/memoset/query.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/coprocessor/memoset/query.rs b/src/coprocessor/memoset/query.rs index 0ef04d9607..c6b58e069e 100644 --- a/src/coprocessor/memoset/query.rs +++ b/src/coprocessor/memoset/query.rs @@ -30,7 +30,6 @@ where fn index(&self) -> usize; } -#[allow(unreachable_pub)] pub trait CircuitQuery where Self: Sized + Clone, From c17bcc947369dca8b200063de608e727077a7e77 Mon Sep 17 00:00:00 2001 From: porcuquine Date: Thu, 11 Jan 2024 20:55:05 -0800 Subject: [PATCH 08/10] Reimplement symbol(). --- src/coprocessor/memoset/demo.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/coprocessor/memoset/demo.rs b/src/coprocessor/memoset/demo.rs index 3b76aad52f..53f04fe84a 100644 --- a/src/coprocessor/memoset/demo.rs +++ b/src/coprocessor/memoset/demo.rs @@ -222,7 +222,9 @@ impl CircuitQuery for DemoCircuitQuery { } fn symbol(&self) -> Symbol { - todo!() + match self { + Self::Factorial(_) => Symbol::sym(&["lurk", "user", "factorial"]), + } } } From 1a6d10b5c1d94266436e647b24866c659937c369 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 12 Jan 2024 08:18:09 -0300 Subject: [PATCH 09/10] removed commented lines --- src/coprocessor/memoset/mod.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index 816ad86434..99e599aec3 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -91,7 +91,6 @@ impl Transcript { #[allow(dead_code)] fn dbg(&self, s: &Store) { - //dbg!(self.acc.fmt_to_string_simple(s)); tracing::debug!("transcript: {}", self.acc.fmt_to_string_simple(s)); } @@ -173,7 +172,6 @@ impl CircuitTranscript { fn dbg(&self, s: &Store) { let z = self.acc.get_value::().unwrap(); let transcript = s.to_ptr(&z); - // dbg!(transcript.fmt_to_string_simple(s)); tracing::debug!("transcript: {}", transcript.fmt_to_string_simple(s)); } } From 5e0054198a4168642648ead6658043efa0af6ec7 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 12 Jan 2024 10:33:47 -0300 Subject: [PATCH 10/10] circuit_scope type can be inferred --- src/coprocessor/memoset/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coprocessor/memoset/mod.rs b/src/coprocessor/memoset/mod.rs index 99e599aec3..629a452cc7 100644 --- a/src/coprocessor/memoset/mod.rs +++ b/src/coprocessor/memoset/mod.rs @@ -345,7 +345,7 @@ impl> Scope> { s: &Store, ) -> Result<(), SynthesisError> { self.ensure_transcript_finalized(s); - let mut circuit_scope: CircuitScope<_, Q::CQ, _> = + let mut circuit_scope = CircuitScope::from_scope(&mut cs.namespace(|| "transcript"), g, s, self); circuit_scope.init(cs, g, s); {