diff --git a/src/circuit/gadgets/macros.rs b/src/circuit/gadgets/macros.rs index 74b1860050..248a76330b 100644 --- a/src/circuit/gadgets/macros.rs +++ b/src/circuit/gadgets/macros.rs @@ -195,7 +195,7 @@ macro_rules! equal_t { // Returns a Boolean which is true if any of its arguments are true. macro_rules! or { ($cs:expr, $a:expr, $b:expr) => { - or( + crate::circuit::gadgets::constraints::or( $cs.namespace(|| format!("{} or {}", stringify!($a), stringify!($b))), $a, $b, @@ -203,7 +203,7 @@ macro_rules! or { }; ($cs:expr, $a:expr, $b:expr, $c:expr, $($x:expr),+) => {{ let or_tmp_cs_ = &mut $cs.namespace(|| format!("or({})", stringify!(vec![$a, $b, $c, $($x),*]))); - or_v(or_tmp_cs_, &[$a, $b, $c, $($x),*]) + bellpepper::gadgets::boolean_utils::or_v(or_tmp_cs_, &[$a, $b, $c, $($x),*]) }}; ($cs:expr, $a:expr, $($x:expr),+) => {{ let or_tmp_cs_ = &mut $cs.namespace(|| format!("or {}", stringify!(vec![$a, $($x),*]))); diff --git a/src/coprocessor/gadgets.rs b/src/coprocessor/gadgets.rs index 43cbbc2413..35a5aed0e8 100644 --- a/src/coprocessor/gadgets.rs +++ b/src/coprocessor/gadgets.rs @@ -13,6 +13,7 @@ use crate::{ circuit::GlobalAllocator, pointers::{Ptr, ZPtr}, store::{expect_ptrs, Store}, + tag, }, tag::{ExprTag, Tag}, }; @@ -145,6 +146,86 @@ pub(crate) fn construct_list>( }) } +/// Constructs an `Env` pointer +#[allow(dead_code)] +#[inline] +pub(crate) fn construct_env>( + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + var_hash: &AllocatedNum, + val: &AllocatedPtr, + next_env: &AllocatedNum, +) -> Result, SynthesisError> { + let tag = g.alloc_tag_cloned(cs, &ExprTag::Env); + + let hash = hash_poseidon( + cs, + vec![ + var_hash.clone(), + val.tag().clone(), + val.hash().clone(), + next_env.clone(), + ], + store.poseidon_cache.constants.c4(), + )?; + + Ok(AllocatedPtr::from_parts(tag, hash)) +} + +/// Deconstructs `env`, assumed to be a composition of a symbol hash, a value `Ptr`, and a next `Env` hash. +/// +/// # Panics +/// Panics if the store can't deconstruct the env hash. +#[allow(dead_code)] +pub(crate) fn deconstruct_env>( + cs: &mut CS, + s: &Store, + not_dummy: &Boolean, + env: &AllocatedNum, +) -> Result<(AllocatedNum, AllocatedPtr, AllocatedNum), SynthesisError> { + let env_zptr = ZPtr::from_parts(tag::Tag::Expr(ExprTag::Env), env.get_value().unwrap()); + let env_ptr = s.to_ptr(&env_zptr); + + let (a, b, c, d) = { + if let Some([v, val, new_env]) = s.pop_binding(env_ptr) { + let v_zptr = s.hash_ptr(&v); + let val_zptr = s.hash_ptr(&val); + let new_env_zptr = s.hash_ptr(&new_env); + ( + *v_zptr.value(), + val_zptr.tag().to_field::(), + *val_zptr.value(), + *new_env_zptr.value(), + ) + } else { + (F::ZERO, F::ZERO, F::ZERO, F::ZERO) + } + }; + + let key_sym_hash = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "key_sym_hash"), || a); + let val_tag = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "val_tag"), || b); + let val_hash = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "val_hash"), || c); + let new_env_hash = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "new_env_hash"), || d); + + let hash = hash_poseidon( + &mut cs.namespace(|| "hash"), + vec![ + key_sym_hash.clone(), + val_tag.clone(), + val_hash.clone(), + new_env_hash.clone(), + ], + s.poseidon_cache.constants.c4(), + )?; + + let val = AllocatedPtr::from_parts(val_tag, val_hash); + + implies_equal(&mut cs.namespace(|| "hash equality"), not_dummy, env, &hash); + + Ok((key_sym_hash, val, new_env_hash)) +} + /// Retrieves the `Ptr` that corresponds to `a_ptr` by using the `Store` as the /// hint provider #[allow(dead_code)] diff --git a/src/coroutine/memoset/demo.rs b/src/coroutine/memoset/demo.rs index 09b6df15ca..e373a07308 100644 --- a/src/coroutine/memoset/demo.rs +++ b/src/coroutine/memoset/demo.rs @@ -1,12 +1,11 @@ use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; use super::{ - query::{CircuitQuery, Query}, + query::{CircuitQuery, Query, RecursiveQuery}, CircuitScope, CircuitTranscript, LogMemo, LogMemoCircuit, Scope, }; use crate::circuit::gadgets::constraints::alloc_is_zero; use crate::circuit::gadgets::pointer::AllocatedPtr; -use crate::coprocessor::gadgets::construct_list; use crate::field::LurkField; use crate::lem::circuit::GlobalAllocator; use crate::lem::{pointers::Ptr, store::Store}; @@ -28,7 +27,6 @@ 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 { Self::Factorial(n) => { @@ -49,15 +47,6 @@ impl Query for DemoQuery { } } - 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"]), @@ -70,7 +59,7 @@ impl Query for DemoQuery { 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"); + let num = body; Some(Self::Factorial(num)) } else { None @@ -82,7 +71,7 @@ impl Query for DemoQuery { Self::Factorial(n) => { let factorial = s.intern_symbol(&self.symbol()); - s.list(vec![factorial, *n]) + s.cons(factorial, *n) } _ => unreachable!(), } @@ -116,6 +105,32 @@ impl Query for DemoQuery { } } +impl RecursiveQuery for DemoCircuitQuery { + // It would be nice if this could be passed to `CircuitQuery::recurse` as an optional closure, rather than be a + // trait method. That would allow more generality. The types get complicated, though. For generality, we should + // support a context object that can be initialized once in `synthesize_eval` and be passed through for use here. + fn post_recursion>( + &self, + cs: &mut CS, + subquery_result: AllocatedPtr, + ) -> Result, SynthesisError> { + match self { + Self::Factorial(n) => { + let result_f = n.hash().mul( + &mut cs.namespace(|| "incremental multiplication"), + subquery_result.hash(), + )?; + + AllocatedPtr::alloc_tag( + &mut cs.namespace(|| "result"), + ExprTag::Num.to_field(), + result_f, + ) + } + } + } +} + impl CircuitQuery for DemoCircuitQuery { fn synthesize_eval>( &self, @@ -127,8 +142,6 @@ impl CircuitQuery for DemoCircuitQuery { 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); @@ -140,85 +153,36 @@ impl CircuitQuery for DemoCircuitQuery { 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, &self.symbol_ptr(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_internal_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, + 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 new_num = AllocatedPtr::alloc_tag( + &mut cs.namespace(|| "new_num"), + ExprTag::Num.to_field(), + new_n, )?; - Ok((value, acc, transcript)) + self.recurse( + cs, + g, + store, + scope, + &new_num, + &n_is_zero.not(), + (&base_case, acc, transcript), + ) } } } diff --git a/src/coroutine/memoset/env.rs b/src/coroutine/memoset/env.rs new file mode 100644 index 0000000000..86ee3130d6 --- /dev/null +++ b/src/coroutine/memoset/env.rs @@ -0,0 +1,457 @@ +use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; + +use super::{ + query::{CircuitQuery, Query, RecursiveQuery}, + CircuitScope, CircuitTranscript, LogMemo, LogMemoCircuit, Scope, +}; +use crate::circuit::gadgets::constraints::{alloc_equal, alloc_is_zero}; +use crate::circuit::gadgets::pointer::AllocatedPtr; +use crate::coprocessor::gadgets::{construct_cons, deconstruct_env}; +use crate::field::LurkField; +use crate::lem::circuit::GlobalAllocator; +use crate::lem::{pointers::Ptr, store::Store}; +use crate::symbol::Symbol; +use crate::tag::ExprTag; + +#[allow(dead_code)] +#[derive(Debug, Clone)] +pub(crate) enum EnvQuery { + Lookup(Ptr, Ptr), + Phantom(F), +} + +#[derive(Debug, Clone)] +pub(crate) enum EnvCircuitQuery { + Lookup(AllocatedNum, AllocatedNum), +} + +impl Query for EnvQuery { + type CQ = EnvCircuitQuery; + + fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr { + match self { + Self::Lookup(var, env) => { + if let Some([v, val, new_env]) = s.pop_binding(*env) { + if s.ptr_eq(var, &v) { + let t = s.intern_t(); + s.cons(val, t) + } else { + self.recursive_eval(scope, s, Self::Lookup(*var, new_env)) + } + } else { + let nil = s.intern_nil(); + s.cons(nil, nil) + } + } + _ => unreachable!(), + } + } + + fn symbol(&self) -> Symbol { + match self { + Self::Lookup(_, _) => Symbol::sym(&["lurk", "env", "lookup"]), + _ => 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", "env", "lookup"]) { + let (var, env) = s.car_cdr(&body).expect("query body should be cons"); + Some(Self::Lookup(var, env)) + } else { + None + } + } + + fn to_ptr(&self, s: &Store) -> Ptr { + match self { + Self::Lookup(var, env) => { + let lookup = s.intern_symbol(&self.symbol()); + // Since var and env will actually be single field elements in the circuit, we could reduce the cost of + // this to use a smaller hash. This could get ugly fast, but this possibility is a consequence of the + // optimized env-binding data structure we've adopted. + let args = s.cons(*var, *env); + s.cons(lookup, args) + } + _ => unreachable!(), + } + } + + fn to_circuit>(&self, cs: &mut CS, s: &Store) -> Self::CQ { + match self { + EnvQuery::Lookup(var, env) => { + let mut var_cs = cs.namespace(|| "var"); + let allocated_var = + AllocatedNum::alloc_infallible(&mut var_cs, || *s.hash_ptr(var).value()); + let mut env_cs = var_cs.namespace(|| "env"); + let allocated_env = + AllocatedNum::alloc_infallible(&mut env_cs, || *s.hash_ptr(env).value()); + Self::CQ::Lookup(allocated_var, allocated_env) + } + _ => unreachable!(), + } + } + + fn dummy_from_index(s: &Store, index: usize) -> Self { + match index { + 0 => Self::Lookup(s.num(0.into()), s.num(0.into())), + _ => unreachable!(), + } + } + + fn index(&self) -> usize { + match self { + Self::Lookup(_, _) => 0, + _ => unreachable!(), + } + } + + fn count() -> usize { + 1 + } +} + +impl RecursiveQuery for EnvCircuitQuery {} + +impl CircuitQuery for EnvCircuitQuery { + 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 { + Self::Lookup(var, env) => { + let nil = store.intern_nil(); + let t = store.intern_t(); + let allocated_nil = g.alloc_ptr(cs, &nil, store); + let allocated_t = g.alloc_ptr(cs, &t, store); + let sym_tag = g.alloc_tag(&mut cs.namespace(|| "sym_tag"), &ExprTag::Sym); + let env_tag = g.alloc_tag(&mut cs.namespace(|| "env_tag"), &ExprTag::Env); + + let env_is_empty = alloc_is_zero(&mut cs.namespace(|| "env_is_empty"), env)?; + + let (next_var, next_val, new_env) = deconstruct_env( + &mut cs.namespace(|| "deconstruct_env"), + store, + &env_is_empty.not(), + env, + )?; + + let var_matches = alloc_equal(&mut cs.namespace(|| "var_matches"), var, &next_var)?; + let is_immediate = or!(cs, &var_matches, &env_is_empty)?; + + let immediate_val = AllocatedPtr::pick( + &mut cs.namespace(|| "immediate_val"), + &var_matches, + &next_val, + &allocated_nil, + )?; + + let immediate_bound = AllocatedPtr::pick( + &mut cs.namespace(|| "immediate_bound"), + &var_matches, + &allocated_t, + &allocated_nil, + )?; + + let immediate_result = construct_cons( + &mut cs.namespace(|| "immediate_result"), + g, + store, + &immediate_val, + &immediate_bound, + )?; + + let new_env_alloc = AllocatedPtr::from_parts(env_tag.clone(), new_env); + let var_alloc = AllocatedPtr::from_parts(sym_tag.clone(), var.clone()); + + let recursive_args = construct_cons( + &mut cs.namespace(|| "recursive_args"), + g, + store, + &var_alloc, + &new_env_alloc, + )?; + + self.recurse( + cs, + g, + store, + scope, + &recursive_args, + &is_immediate.not(), + (&immediate_result, acc, transcript), + ) + } + } + } + + fn from_ptr>(cs: &mut CS, s: &Store, ptr: &Ptr) -> Option { + let query = EnvQuery::from_ptr(s, ptr); + if let Some(q) = query { + match q { + EnvQuery::Lookup(var, env) => { + let allocated_var = + AllocatedNum::alloc_infallible(&mut cs.namespace(|| "var"), || { + *s.hash_ptr(&var).value() + }); + let allocated_env = + AllocatedNum::alloc_infallible(&mut cs.namespace(|| "env"), || { + *s.hash_ptr(&env).value() + }); + Some(Self::Lookup(allocated_var, allocated_env)) + } + _ => unreachable!(), + } + } else { + None + } + } + + fn dummy_from_index>(cs: &mut CS, s: &Store, index: usize) -> Self { + EnvQuery::dummy_from_index(s, index).to_circuit(cs, s) + } + + fn symbol(&self) -> Symbol { + match self { + Self::Lookup(_, _) => Symbol::sym(&["lurk", "env", "lookup"]), + } + } +} + +#[cfg(test)] +mod test { + use super::*; + + use crate::state::State; + use crate::sym; + + use bellpepper_core::{test_cs::TestConstraintSystem, Comparable}; + use expect_test::{expect, Expect}; + use ff::Field; + use halo2curves::bn256::Fr as F; + use std::default::Default; + + #[test] + fn test_env_lookup() { + let s = Store::::default(); + let mut scope: Scope, LogMemo> = Scope::default(); + let a = s.intern_symbol(&sym!("a")); + let b = s.intern_symbol(&sym!("b")); + let c = s.intern_symbol(&sym!("c")); + + 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 empty = s.intern_empty_env(); + let a_env = s.push_binding(a, one, empty); + let b_env = s.push_binding(b, two, a_env); + let c_env = s.push_binding(c, three, b_env); + let a2_env = s.push_binding(a, four, c_env); + + let t = s.intern_t(); + let nil = s.intern_nil(); + + let mut test = |var, env, found| { + let expected = if let Some(val) = found { + s.cons(val, t) + } else { + s.cons(nil, nil) + }; + + let result = EnvQuery::Lookup(var, env).eval(&s, &mut scope); + assert!(s.ptr_eq(&expected, &result)) + }; + + test(a, empty, None); + test(a, a_env, Some(one)); + test(b, a_env, None); + test(b, b_env, Some(two)); + test(a, a2_env, Some(four)); + test(c, b_env, None); + test(c, c_env, Some(three)); + test(c, a2_env, Some(three)); + } + + #[test] + fn test_lookup_circuit() { + let expect_eq = |computed: usize, expected: Expect| { + expected.assert_eq(&computed.to_string()); + }; + + let s = &Store::::default(); + + let a = s.intern_symbol(&sym!("a")); + let b = s.intern_symbol(&sym!("b")); + let c = s.intern_symbol(&sym!("c")); + + 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 empty = s.intern_empty_env(); + let a_env = s.push_binding(a, one, empty); + let b_env = s.push_binding(b, two, a_env); + let c_env = s.push_binding(c, three, b_env); + let a2_env = s.push_binding(a, four, c_env); + + { + // With internal insertions transcribed. + + let (one_lookup_constraints, one_lookup_aux) = + test_lookup_circuit_aux(s, a, empty, true, expect!["3231"], expect!["3242"]); + + test_lookup_circuit_aux(s, a, a_env, true, expect!["3231"], expect!["3242"]); + + let (two_lookup_constraints, two_lookup_aux) = + test_lookup_circuit_aux(s, b, a_env, true, expect!["5872"], expect!["5891"]); + + test_lookup_circuit_aux(s, b, b_env, true, expect!["3231"], expect!["3242"]); + test_lookup_circuit_aux(s, a, a2_env, true, expect!["3231"], expect!["3242"]); + + let (three_lookup_constraints, three_lookup_aux) = + test_lookup_circuit_aux(s, c, b_env, true, expect!["8513"], expect!["8540"]); + + test_lookup_circuit_aux(s, c, c_env, true, expect!["3231"], expect!["3242"]); + test_lookup_circuit_aux(s, c, a2_env, true, expect!["5872"], expect!["5891"]); + + let delta1_constraints = two_lookup_constraints - one_lookup_constraints; + let delta2_constraints = three_lookup_constraints - two_lookup_constraints; + let overhead_constraints = one_lookup_constraints - delta1_constraints; + + assert_eq!(delta1_constraints, delta2_constraints); + + // This is the number of constraints per lookup. + expect_eq(delta1_constraints, expect!["2641"]); + + // This is the number of constraints in the constant overhead. + expect_eq(overhead_constraints, expect!["590"]); + + let delta1_aux = two_lookup_aux - one_lookup_aux; + let delta2_aux = three_lookup_aux - two_lookup_aux; + let overhead_aux = one_lookup_aux - delta1_aux; + + assert_eq!(delta1_aux, delta2_aux); + + // This is the number of aux per lookup. + expect_eq(delta1_aux, expect!["2649"]); + + // This is the number of aux in the constant overhead. + expect_eq(overhead_aux, expect!["593"]); + } + + { + // Without internal insertions transcribed. + + let (one_lookup_constraints, one_lookup_aux) = + test_lookup_circuit_aux(s, a, empty, false, expect!["2942"], expect!["2953"]); + + test_lookup_circuit_aux(s, a, a_env, false, expect!["2942"], expect!["2953"]); + + let (two_lookup_constraints, two_lookup_aux) = + test_lookup_circuit_aux(s, b, a_env, false, expect!["5294"], expect!["5313"]); + + test_lookup_circuit_aux(s, b, b_env, false, expect!["2942"], expect!["2953"]); + test_lookup_circuit_aux(s, a, a2_env, false, expect!["2942"], expect!["2953"]); + + let (three_lookup_constraints, three_lookup_aux) = + test_lookup_circuit_aux(s, c, b_env, false, expect!["7646"], expect!["7673"]); + + test_lookup_circuit_aux(s, c, c_env, false, expect!["2942"], expect!["2953"]); + test_lookup_circuit_aux(s, c, a2_env, false, expect!["5294"], expect!["5313"]); + + let delta1_constraints = two_lookup_constraints - one_lookup_constraints; + let delta2_constraints = three_lookup_constraints - two_lookup_constraints; + let overhead_constraints = one_lookup_constraints - delta1_constraints; + + assert_eq!(delta1_constraints, delta2_constraints); + + // This is the number of constraints per lookup. + expect_eq(delta1_constraints, expect!["2352"]); + + // This is the number of constraints in the constant overhead. + expect_eq(overhead_constraints, expect!["590"]); + + let delta1_aux = two_lookup_aux - one_lookup_aux; + let delta2_aux = three_lookup_aux - two_lookup_aux; + let overhead_aux = one_lookup_aux - delta1_aux; + + assert_eq!(delta1_aux, delta2_aux); + + // This is the number of aux per lookup. + expect_eq(delta1_aux, expect!["2360"]); + + // This is the number of aux in the constant overhead. + expect_eq(overhead_aux, expect!["593"]); + } + } + + fn test_lookup_circuit_aux( + s: &Store, + sym: Ptr, + env: Ptr, + transcribe_internal_insertions: bool, + expected_constraints_simple: Expect, + expected_aux_simple: Expect, + ) -> (usize, usize) { + let state = State::init_lurk_state(); + let expect_eq = |computed: usize, expected: Expect| { + expected.assert_eq(&computed.to_string()); + }; + + let mut scope: Scope, LogMemo> = + Scope::new(transcribe_internal_insertions, 1); + + let make_query = |sym, env| EnvQuery::Lookup(sym, env).to_ptr(s); + + { + let query = make_query(sym, env); + + scope.query(s, query); + + for (k, v) in scope.queries.iter() { + println!("k: {}", k.fmt_to_string(s, &state)); + println!("v: {}", v.fmt_to_string(s, &state)); + } + + scope.finalize_transcript(s); + + let cs = &mut TestConstraintSystem::new(); + let g = &mut GlobalAllocator::default(); + + scope.synthesize(cs, g, s).unwrap(); + + println!( + "transcript: {}", + scope + .memoset + .transcript + .get() + .unwrap() + .fmt_to_string_simple(s) + ); + + expect_eq(cs.num_constraints(), expected_constraints_simple); + expect_eq(cs.aux().len(), expected_aux_simple); + + let unsat = cs.which_is_unsatisfied(); + + if unsat.is_some() { + dbg!(unsat); + } + assert!(cs.is_satisfied()); + + (cs.num_constraints(), cs.aux().len()) + } + } +} diff --git a/src/coroutine/memoset/mod.rs b/src/coroutine/memoset/mod.rs index da8aa3bc4d..7b9196f939 100644 --- a/src/coroutine/memoset/mod.rs +++ b/src/coroutine/memoset/mod.rs @@ -51,6 +51,7 @@ use multiset::MultiSet; pub use query::{CircuitQuery, Query}; mod demo; +mod env; mod multiset; mod query; @@ -528,6 +529,7 @@ impl> Scope> { } circuit_scope.finalize(cs, g); + Ok(()) } @@ -1055,26 +1057,26 @@ mod test { fn test_query_with_internal_insertion_transcript() { test_query_aux( true, - expect!["10875"], - expect!["10908"], - expect!["11457"], - expect!["11494"], + expect!["9430"], + expect!["9463"], + expect!["10012"], + expect!["10049"], 1, ); test_query_aux( true, - expect!["12908"], - expect!["12947"], - expect!["13490"], - expect!["13533"], + expect!["11174"], + expect!["11213"], + expect!["11756"], + expect!["11799"], 3, ); test_query_aux( true, - expect!["21106"], - expect!["21169"], - expect!["21688"], - expect!["21755"], + expect!["18216"], + expect!["18279"], + expect!["18798"], + expect!["18865"], 10, ) } @@ -1083,26 +1085,26 @@ mod test { fn test_query_without_internal_insertion_transcript() { test_query_aux( false, - expect!["9430"], - expect!["9463"], - expect!["10012"], - expect!["10049"], + expect!["7985"], + expect!["8018"], + expect!["8567"], + expect!["8604"], 1, ); test_query_aux( false, - expect!["11174"], - expect!["11213"], - expect!["11756"], - expect!["11799"], + expect!["9440"], + expect!["9479"], + expect!["10022"], + expect!["10065"], 3, ); test_query_aux( false, - expect!["18216"], - expect!["18279"], - expect!["18798"], - expect!["18865"], + expect!["15326"], + expect!["15389"], + expect!["15908"], + expect!["15975"], 10, ) } @@ -1120,8 +1122,8 @@ mod test { Scope::new(transcribe_internal_insertions, circuit_query_rc); let state = State::init_lurk_state(); - let fact_4 = s.read_with_default_state("(factorial 4)").unwrap(); - let fact_3 = s.read_with_default_state("(factorial 3)").unwrap(); + let fact_4 = s.read_with_default_state("(factorial . 4)").unwrap(); + let fact_3 = s.read_with_default_state("(factorial . 3)").unwrap(); let expect_eq = |computed: usize, expected: Expect| { expected.assert_eq(&computed.to_string()); diff --git a/src/coroutine/memoset/query.rs b/src/coroutine/memoset/query.rs index cc19aaec10..8a2eb95ce9 100644 --- a/src/coroutine/memoset/query.rs +++ b/src/coroutine/memoset/query.rs @@ -1,7 +1,8 @@ -use bellpepper_core::{ConstraintSystem, SynthesisError}; +use bellpepper_core::{boolean::Boolean, ConstraintSystem, SynthesisError}; use super::{CircuitScope, CircuitTranscript, LogMemo, LogMemoCircuit, Scope}; use crate::circuit::gadgets::pointer::AllocatedPtr; +use crate::coprocessor::gadgets::construct_cons; use crate::field::LurkField; use crate::lem::circuit::GlobalAllocator; use crate::lem::{pointers::Ptr, store::Store}; @@ -19,7 +20,9 @@ where scope: &mut Scope>, s: &Store, subquery: Self, - ) -> Ptr; + ) -> Ptr { + scope.query_recursively(s, self, subquery) + } fn from_ptr(s: &Store, ptr: &Ptr) -> Option; fn to_ptr(&self, s: &Store) -> Ptr; fn to_circuit>(&self, cs: &mut CS, s: &Store) -> Self::CQ; @@ -60,3 +63,74 @@ where fn dummy_from_index>(cs: &mut CS, s: &Store, index: usize) -> Self; } + +pub(crate) trait RecursiveQuery: CircuitQuery { + fn post_recursion>( + &self, + _cs: &mut CS, + subquery_result: AllocatedPtr, + ) -> Result, SynthesisError> { + Ok(subquery_result) + } + + fn recurse>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + scope: &mut CircuitScope>, + args: &AllocatedPtr, + is_recursive: &Boolean, + immediate: (&AllocatedPtr, &AllocatedPtr, &CircuitTranscript), + ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + let is_immediate = is_recursive.not(); + + let subquery = { + let symbol = g.alloc_ptr( + &mut cs.namespace(|| "symbol"), + &self.symbol_ptr(store), + store, + ); + construct_cons(&mut cs.namespace(|| "subquery"), g, store, &symbol, args)? + }; + + let (sub_result, new_acc, new_transcript) = scope.synthesize_internal_query( + &mut cs.namespace(|| "recursive query"), + g, + store, + &subquery, + immediate.1, + immediate.2, + is_recursive, + )?; + + let (recursive_result, recursive_acc, recursive_transcript) = ( + self.post_recursion(cs, sub_result)?, + new_acc, + new_transcript, + ); + + let value = AllocatedPtr::pick( + &mut cs.namespace(|| "pick value"), + &is_immediate, + immediate.0, + &recursive_result, + )?; + + let acc = AllocatedPtr::pick( + &mut cs.namespace(|| "pick acc"), + &is_immediate, + immediate.1, + &recursive_acc, + )?; + + let transcript = CircuitTranscript::pick( + &mut cs.namespace(|| "pick recursive_transcript"), + &is_immediate, + immediate.2, + &recursive_transcript, + )?; + + Ok((value, acc, transcript)) + } +} diff --git a/src/lem/store.rs b/src/lem/store.rs index e5080cbe8b..9053dcc7d0 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -621,6 +621,11 @@ impl Store { self.intern_lurk_symbol("nil") } + #[inline] + pub fn intern_t(&self) -> Ptr { + self.intern_lurk_symbol("t") + } + #[inline] pub fn intern_user_symbol(&self, name: &str) -> Ptr { self.intern_symbol(&user_sym(name))