diff --git a/src/coroutine/memoset/demo.rs b/src/coroutine/memoset/demo.rs index 0f9ac5eb0..ace6d5b2a 100644 --- a/src/coroutine/memoset/demo.rs +++ b/src/coroutine/memoset/demo.rs @@ -6,7 +6,6 @@ use super::{ }; use crate::circuit::gadgets::constraints::alloc_is_zero; 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}; @@ -129,6 +128,17 @@ impl RecursiveQuery for DemoCircuitQuery { } impl CircuitQuery for DemoCircuitQuery { + fn synthesize_args>( + &self, + _cs: &mut CS, + _g: &GlobalAllocator, + _store: &Store, + ) -> Result, SynthesisError> { + match self { + Self::Factorial(n) => Ok(n.clone()), + } + } + fn synthesize_eval>( &self, cs: &mut CS, @@ -136,6 +146,7 @@ impl CircuitQuery for DemoCircuitQuery { store: &Store, scope: &mut CircuitScope>, acc: &AllocatedPtr, + allocated_key: &AllocatedPtr, ) -> Result<((AllocatedPtr, AllocatedPtr), AllocatedPtr), SynthesisError> { match self { Self::Factorial(n) => { @@ -167,19 +178,17 @@ impl CircuitQuery for DemoCircuitQuery { let new_num = AllocatedPtr::alloc_tag(ns!(cs, "new_num"), ExprTag::Num.to_field(), new_n)?; - let symbol = g.alloc_ptr(ns!(cs, "symbol_"), &self.symbol_ptr(store), store); - - let query = construct_cons(ns!(cs, "query"), g, store, &symbol, n)?; + let subquery = Self::Factorial(new_num); self.recurse( cs, g, store, scope, - &query, - &new_num, + subquery, &n_is_zero.not(), (&base_case, acc), + allocated_key, ) } } diff --git a/src/coroutine/memoset/env.rs b/src/coroutine/memoset/env.rs index f08e6acca..810c34723 100644 --- a/src/coroutine/memoset/env.rs +++ b/src/coroutine/memoset/env.rs @@ -117,6 +117,24 @@ impl Query for EnvQuery { impl RecursiveQuery for EnvCircuitQuery {} impl CircuitQuery for EnvCircuitQuery { + fn synthesize_args>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + ) -> Result, SynthesisError> { + match self { + Self::Lookup(var, env) => { + let sym_tag = g.alloc_tag(ns!(cs, "sym_tag"), &ExprTag::Sym); + let env_tag = g.alloc_tag(ns!(cs, "env_tag"), &ExprTag::Env); + let var_alloc = AllocatedPtr::from_parts(sym_tag.clone(), var.clone()); + let env_alloc = AllocatedPtr::from_parts(env_tag.clone(), env.clone()); + + construct_cons(ns!(cs, "args"), g, store, &var_alloc, &env_alloc) + } + } + } + fn synthesize_eval>( &self, cs: &mut CS, @@ -124,6 +142,7 @@ impl CircuitQuery for EnvCircuitQuery { store: &Store, scope: &mut CircuitScope>, acc: &AllocatedPtr, + allocated_key: &AllocatedPtr, ) -> Result<((AllocatedPtr, AllocatedPtr), AllocatedPtr), SynthesisError> { match self { Self::Lookup(var, env) => { @@ -131,8 +150,6 @@ impl CircuitQuery for EnvCircuitQuery { 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(ns!(cs, "sym_tag"), &ExprTag::Sym); - let env_tag = g.alloc_tag(ns!(cs, "env_tag"), &ExprTag::Env); let env_is_empty = alloc_is_zero(ns!(cs, "env_is_empty"), env)?; @@ -164,34 +181,17 @@ impl CircuitQuery for EnvCircuitQuery { &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( - ns!(cs, "recursive_args"), - g, - store, - &var_alloc, - &new_env_alloc, - )?; - - let env_alloc = AllocatedPtr::from_parts(env_tag.clone(), env.clone()); - let these_args = - construct_cons(ns!(cs, "these_args"), g, store, &var_alloc, &env_alloc)?; - - let symbol = g.alloc_ptr(ns!(cs, "symbol_"), &self.symbol_ptr(store), store); - - let query = construct_cons(ns!(cs, "query"), g, store, &symbol, &these_args)?; + let subquery = Self::Lookup(var.clone(), new_env); self.recurse( cs, g, store, scope, - &query, - &recursive_args, + subquery, &is_immediate.not(), (&immediate_result, acc), + allocated_key, ) } } @@ -305,21 +305,21 @@ mod test { // Without internal insertions transcribed. let (one_lookup_constraints, one_lookup_aux) = - test_lookup_circuit_aux(s, a, empty, expect!["3525"], expect!["3543"]); + test_lookup_circuit_aux(s, a, empty, expect!["3525"], expect!["3541"]); - test_lookup_circuit_aux(s, a, a_env, expect!["3525"], expect!["3543"]); + test_lookup_circuit_aux(s, a, a_env, expect!["3525"], expect!["3541"]); let (two_lookup_constraints, two_lookup_aux) = - test_lookup_circuit_aux(s, b, a_env, expect!["6459"], expect!["6489"]); + test_lookup_circuit_aux(s, b, a_env, expect!["6459"], expect!["6485"]); - test_lookup_circuit_aux(s, b, b_env, expect!["3525"], expect!["3543"]); - test_lookup_circuit_aux(s, a, a2_env, expect!["3525"], expect!["3543"]); + test_lookup_circuit_aux(s, b, b_env, expect!["3525"], expect!["3541"]); + test_lookup_circuit_aux(s, a, a2_env, expect!["3525"], expect!["3541"]); let (three_lookup_constraints, three_lookup_aux) = - test_lookup_circuit_aux(s, c, b_env, expect!["9393"], expect!["9435"]); + test_lookup_circuit_aux(s, c, b_env, expect!["9393"], expect!["9429"]); - test_lookup_circuit_aux(s, c, c_env, expect!["3525"], expect!["3543"]); - test_lookup_circuit_aux(s, c, a2_env, expect!["6459"], expect!["6489"]); + test_lookup_circuit_aux(s, c, c_env, expect!["3525"], expect!["3541"]); + test_lookup_circuit_aux(s, c, a2_env, expect!["6459"], expect!["6485"]); let delta1_constraints = two_lookup_constraints - one_lookup_constraints; let delta2_constraints = three_lookup_constraints - two_lookup_constraints; @@ -340,7 +340,7 @@ mod test { assert_eq!(delta1_aux, delta2_aux); // This is the number of aux per lookup. - expect_eq(delta1_aux, expect!["2946"]); + expect_eq(delta1_aux, expect!["2944"]); // This is the number of aux in the constant overhead. expect_eq(overhead_aux, expect!["597"]); diff --git a/src/coroutine/memoset/mod.rs b/src/coroutine/memoset/mod.rs index 97577642b..b6d4ffa86 100644 --- a/src/coroutine/memoset/mod.rs +++ b/src/coroutine/memoset/mod.rs @@ -1149,7 +1149,16 @@ impl CircuitScope> { s: &Store, ) -> Result<(), SynthesisError> { for (i, kv) in scope.toplevel_insertions.iter().enumerate() { - self.synthesize_toplevel_query(cs, g, s, i, kv)?; + let cs = ns!(cs, format!("toplevel_insertion-{i}")); + let (key, value) = s.car_cdr(kv).expect("kv missing"); + // NOTE: This is an unconstrained allocation, but when actually hooked up to Lurk reduction, it must be + // constrained appropriately. + let allocated_key = + AllocatedPtr::alloc(ns!(cs, "allocated_key"), || Ok(s.hash_ptr(&key))).unwrap(); + // NOTE: The returned value is unused here, but when actually hooked up to Lurk reduction, it must be used + // as the result of evaluating the query. + let _allocated_value = + self.synthesize_toplevel_query(cs, g, s, i, &allocated_key, value)?; } Ok(()) } @@ -1160,12 +1169,10 @@ impl CircuitScope> { g: &mut GlobalAllocator, s: &Store, i: usize, - kv: &Ptr, - ) -> Result<(), SynthesisError> { - let (key, value) = s.car_cdr(kv).unwrap(); + allocated_key: &AllocatedPtr, + value: Ptr, + ) -> Result, SynthesisError> { let cs = ns!(cs, format!("toplevel-{i}")); - let allocated_key = - AllocatedPtr::alloc(ns!(cs, "allocated_key"), || Ok(s.hash_ptr(&key))).unwrap(); let acc = self.acc.clone().unwrap(); let insertion_transcript = self.transcript.clone(); @@ -1174,7 +1181,7 @@ impl CircuitScope> { cs, g, s, - &allocated_key, + allocated_key, &acc, &insertion_transcript, &Boolean::Constant(true), @@ -1186,7 +1193,7 @@ impl CircuitScope> { self.acc = Some(new_acc); self.transcript = new_transcript; - Ok(()) + Ok(val) } fn synthesize_prove_key_query, Q: Query>( @@ -1197,25 +1204,20 @@ impl CircuitScope> { key: Option<&Ptr>, index: usize, ) -> Result<(), SynthesisError> { - let allocated_key = AllocatedPtr::alloc(ns!(cs, "allocated_key"), || { - if let Some(key) = key { - Ok(s.hash_ptr(key)) - } else { - Ok(s.hash_ptr(&s.intern_nil())) - } - }) - .unwrap(); + let not_dummy = Boolean::Is(AllocatedBit::alloc( + cs.namespace(|| "not_dummy"), + Some(key.is_some()), + )?); let circuit_query = if let Some(key) = key { - Q::CQ::from_ptr(ns!(cs, "circuit_query"), s, key).unwrap() + let query = Q::from_ptr(s, key).unwrap(); + assert_eq!(index, query.index()); + query.to_circuit(ns!(cs, "circuit_query"), s) } else { Q::CQ::dummy_from_index(ns!(cs, "circuit_query"), s, index) }; - let not_dummy = Boolean::Is(AllocatedBit::alloc( - cs.namespace(|| "not_dummy"), - Some(key.is_some()), - )?); + let allocated_key = circuit_query.synthesize_query(ns!(cs, "allocated_key"), g, s)?; self.synthesize_prove_query::<_, Q::CQ>( cs, @@ -1240,7 +1242,7 @@ impl CircuitScope> { let acc = self.acc.clone().unwrap(); let ((val, provenance), new_acc) = circuit_query - .synthesize_eval(ns!(cs, "eval"), g, s, self, &acc) + .synthesize_eval(ns!(cs, "eval"), g, s, self, &acc, allocated_key) .unwrap(); let (new_acc, new_transcript) = self.synthesize_remove( @@ -1468,23 +1470,23 @@ mod test { fn test_query() { test_query_aux( expect!["9451"], - expect!["9507"], + expect!["9497"], expect!["10034"], - expect!["10097"], + expect!["10087"], 1, ); test_query_aux( expect!["11191"], - expect!["11253"], + expect!["11241"], expect!["11774"], - expect!["11843"], + expect!["11831"], 3, ); test_query_aux( expect!["18239"], - expect!["18336"], + expect!["18316"], expect!["18822"], - expect!["18926"], + expect!["18906"], 10, ) } diff --git a/src/coroutine/memoset/query.rs b/src/coroutine/memoset/query.rs index 105eff836..3afd4f0da 100644 --- a/src/coroutine/memoset/query.rs +++ b/src/coroutine/memoset/query.rs @@ -50,6 +50,7 @@ where store: &Store, scope: &mut CircuitScope>, acc: &AllocatedPtr, + allocated_key: &AllocatedPtr, ) -> Result<((AllocatedPtr, AllocatedPtr), AllocatedPtr), SynthesisError>; fn symbol(&self) -> Symbol; @@ -61,6 +62,43 @@ where fn from_ptr>(cs: &mut CS, s: &Store, ptr: &Ptr) -> Option; fn dummy_from_index>(cs: &mut CS, s: &Store, index: usize) -> Self; + + fn synthesize_args>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + ) -> Result, SynthesisError>; + + fn synthesize_query>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + ) -> Result, SynthesisError> { + let symbol = g.alloc_ptr(ns!(cs, "symbol_"), &self.symbol_ptr(store), store); + let args = self.synthesize_args(ns!(cs, "args"), g, store)?; + construct_cons(ns!(cs, "query"), g, store, &symbol, &args) + } + + fn synthesize_provenance>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + result: AllocatedPtr, + dependency_provenances: Vec>, + allocated_key: Option<&AllocatedPtr>, + ) -> Result, SynthesisError> { + let query = if let Some(q) = allocated_key { + q.clone() + } else { + self.synthesize_query(ns!(cs, "query"), g, store)? + }; + let p = AllocatedProvenance::new(query, result, dependency_provenances.clone()); + + Ok(p.to_ptr(cs, g, store)?.clone()) + } } pub(crate) trait RecursiveQuery: CircuitQuery { @@ -69,6 +107,7 @@ pub(crate) trait RecursiveQuery: CircuitQuery { _cs: &mut CS, subquery_result: AllocatedPtr, ) -> Result, SynthesisError> { + // The default implementation provides tail recursion. Ok(subquery_result) } @@ -78,17 +117,14 @@ pub(crate) trait RecursiveQuery: CircuitQuery { g: &GlobalAllocator, store: &Store, scope: &mut CircuitScope>, - query: &AllocatedPtr, - args: &AllocatedPtr, + subquery: Self, is_recursive: &Boolean, immediate: (&AllocatedPtr, &AllocatedPtr), + allocated_key: &AllocatedPtr, ) -> Result<((AllocatedPtr, AllocatedPtr), AllocatedPtr), SynthesisError> { let is_immediate = is_recursive.not(); - let subquery = { - let symbol = g.alloc_ptr(ns!(cs, "symbol"), &self.symbol_ptr(store), store); - construct_cons(ns!(cs, "subquery"), g, store, &symbol, args)? - }; + let subquery = subquery.synthesize_query(cs, g, store)?; let ((sub_result, sub_provenance), new_acc) = scope.synthesize_internal_query( ns!(cs, "recursive query"), @@ -124,13 +160,14 @@ pub(crate) trait RecursiveQuery: CircuitQuery { &sub_provenance, )?; - let p = AllocatedProvenance::new( - query.clone(), + let provenance = self.synthesize_provenance( + ns!(cs, "provenance"), + g, + store, value.clone(), vec![dependency_provenance.clone()], - ); - - let provenance = p.to_ptr(cs, g, store)?; + Some(allocated_key), + )?; Ok(((value, provenance.clone()), acc)) }