diff --git a/src/circuit/gadgets/macros.rs b/src/circuit/gadgets/macros.rs index 248a76330b..20cab0010f 100644 --- a/src/circuit/gadgets/macros.rs +++ b/src/circuit/gadgets/macros.rs @@ -1,5 +1,12 @@ #![allow(unused_macros)] +/// Simplify creating a namespace. +macro_rules! ns { + ($cs:ident, $e:expr) => { + &mut $cs.namespace(|| $e) + }; +} + // Enforces constraint that a implies b. macro_rules! if_then { ($cs:ident, $a:expr, $b:expr) => { diff --git a/src/coprocessor/gadgets.rs b/src/coprocessor/gadgets.rs index 35a5aed0e8..4e8ee3ae49 100644 --- a/src/coprocessor/gadgets.rs +++ b/src/coprocessor/gadgets.rs @@ -125,7 +125,7 @@ pub(crate) fn construct_list>( cs: &mut CS, g: &GlobalAllocator, store: &Store, - elts: &[&AllocatedPtr], + elts: &[AllocatedPtr], last: Option>, ) -> Result, SynthesisError> { let init = match last { @@ -173,11 +173,36 @@ pub(crate) fn construct_env>( Ok(AllocatedPtr::from_parts(tag, hash)) } +#[inline] +pub(crate) fn construct_provenance>( + cs: &mut CS, + g: &GlobalAllocator, + store: &Store, + query_hash: &AllocatedNum, + result: &AllocatedPtr, + deps: &AllocatedNum, +) -> Result, SynthesisError> { + // TODO: should there be a provenance tag? + let tag = g.alloc_tag_cloned(cs, &ExprTag::Env); + + let hash = hash_poseidon( + cs, + vec![ + query_hash.clone(), + result.tag().clone(), + result.hash().clone(), + deps.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, @@ -226,6 +251,65 @@ pub(crate) fn deconstruct_env>( Ok((key_sym_hash, val, new_env_hash)) } +#[allow(dead_code)] +pub(crate) fn deconstruct_provenance>( + cs: &mut CS, + s: &Store, + not_dummy: &Boolean, + provenance: &AllocatedNum, +) -> Result<(AllocatedNum, AllocatedPtr, AllocatedNum), SynthesisError> { + let prov_zptr = ZPtr::from_parts( + tag::Tag::Expr(ExprTag::Env), + provenance.get_value().unwrap(), + ); + let prov_ptr = s.to_ptr(&prov_zptr); + + let (a, b, c, d) = { + if let Some([q, res, deps]) = s.pop_provenance(prov_ptr) { + let q_zptr = s.hash_ptr(&q); + let res_zptr = s.hash_ptr(&res); + let deps_zptr = s.hash_ptr(&deps); + ( + *q_zptr.value(), + res_zptr.tag().to_field::(), + *res_zptr.value(), + *deps_zptr.value(), + ) + } else { + (F::ZERO, F::ZERO, F::ZERO, F::ZERO) + } + }; + + let query_cons_hash = + AllocatedNum::alloc_infallible(&mut cs.namespace(|| "query_cons_hash"), || a); + let res_tag = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "res_tag"), || b); + let res_hash = AllocatedNum::alloc_infallible(&mut cs.namespace(|| "res_hash"), || c); + let deps_tuple_hash = + AllocatedNum::alloc_infallible(&mut cs.namespace(|| "deps_tuple_hash"), || d); + + let hash = hash_poseidon( + &mut cs.namespace(|| "hash"), + vec![ + query_cons_hash.clone(), + res_tag.clone(), + res_hash.clone(), + deps_tuple_hash.clone(), + ], + s.poseidon_cache.constants.c4(), + )?; + + let res = AllocatedPtr::from_parts(res_tag, res_hash); + + implies_equal( + &mut cs.namespace(|| "hash equality"), + not_dummy, + provenance, + &hash, + ); + + Ok((query_cons_hash, res, deps_tuple_hash)) +} + /// Retrieves the `Ptr` that corresponds to `a_ptr` by using the `Store` as the /// hint provider #[allow(dead_code)] @@ -688,13 +772,20 @@ mod test { let a_one = g.alloc_ptr(&mut cs, &one, &store); // proper list - let a_list = construct_list(&mut cs, &g, &store, &[&a_one, &a_one], None).unwrap(); + let a_list = + construct_list(&mut cs, &g, &store, &[a_one.clone(), a_one.clone()], None).unwrap(); let z_list = store.hash_ptr(&store.list(vec![one, one])); assert_eq!(a_ptr_as_z_ptr(&a_list), Some(z_list)); // improper list - let a_list = - construct_list(&mut cs, &g, &store, &[&a_one, &a_one], Some(a_one.clone())).unwrap(); + let a_list = construct_list( + &mut cs, + &g, + &store, + &[a_one.clone(), a_one.clone()], + Some(a_one.clone()), + ) + .unwrap(); let z_list = store.hash_ptr(&store.improper_list(vec![one, one], one)); assert_eq!(a_ptr_as_z_ptr(&a_list), Some(z_list)); } diff --git a/src/coroutine/memoset/demo.rs b/src/coroutine/memoset/demo.rs index e373a07308..32bac904af 100644 --- a/src/coroutine/memoset/demo.rs +++ b/src/coroutine/memoset/demo.rs @@ -6,6 +6,7 @@ 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}; @@ -27,7 +28,7 @@ pub(crate) enum DemoCircuitQuery { impl Query for DemoQuery { type CQ = DemoCircuitQuery; - fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr { + fn eval(&self, s: &Store, scope: &mut Scope, F>) -> Ptr { match self { Self::Factorial(n) => { let n_zptr = s.hash_ptr(n); @@ -117,15 +118,11 @@ impl RecursiveQuery for DemoCircuitQuery { match self { Self::Factorial(n) => { let result_f = n.hash().mul( - &mut cs.namespace(|| "incremental multiplication"), + ns!(cs, "incremental multiplication"), subquery_result.hash(), )?; - AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "result"), - ExprTag::Num.to_field(), - result_f, - ) + AllocatedPtr::alloc_tag(ns!(cs, "result"), ExprTag::Num.to_field(), result_f) } } } @@ -140,20 +137,27 @@ impl CircuitQuery for DemoCircuitQuery { scope: &mut CircuitScope>, acc: &AllocatedPtr, transcript: &CircuitTranscript, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + ) -> Result< + ( + (AllocatedPtr, AllocatedPtr), + AllocatedPtr, + CircuitTranscript, + ), + SynthesisError, + > { match self { 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"), + ns!(cs, "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 n_is_zero = alloc_is_zero(ns!(cs, "n_is_zero"), n.hash())?; - let new_n = AllocatedNum::alloc(&mut cs.namespace(|| "new_n"), || { + let new_n = AllocatedNum::alloc(ns!(cs, "new_n"), || { n.hash() .get_value() .map(|n| n - F::ONE) @@ -168,17 +172,19 @@ impl CircuitQuery for DemoCircuitQuery { |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, - )?; + 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)?; self.recurse( cs, g, store, scope, + &query, &new_num, &n_is_zero.not(), (&base_case, acc, transcript), @@ -212,7 +218,7 @@ mod test { #[test] fn test_factorial() { let s = Store::default(); - let mut scope: Scope, LogMemo> = Scope::default(); + let mut scope: Scope, LogMemo, F> = Scope::default(); let zero = s.num(F::ZERO); let one = s.num(F::ONE); let two = s.num(F::from_u64(2)); diff --git a/src/coroutine/memoset/env.rs b/src/coroutine/memoset/env.rs index 86ee3130d6..30bf4a5147 100644 --- a/src/coroutine/memoset/env.rs +++ b/src/coroutine/memoset/env.rs @@ -28,7 +28,7 @@ pub(crate) enum EnvCircuitQuery { impl Query for EnvQuery { type CQ = EnvCircuitQuery; - fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr { + fn eval(&self, s: &Store, scope: &mut Scope, F>) -> Ptr { match self { Self::Lookup(var, env) => { if let Some([v, val, new_env]) = s.pop_binding(*env) { @@ -125,7 +125,14 @@ impl CircuitQuery for EnvCircuitQuery { scope: &mut CircuitScope>, acc: &AllocatedPtr, transcript: &CircuitTranscript, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + ) -> Result< + ( + (AllocatedPtr, AllocatedPtr), + AllocatedPtr, + CircuitTranscript, + ), + SynthesisError, + > { match self { Self::Lookup(var, env) => { let nil = store.intern_nil(); @@ -180,11 +187,35 @@ impl CircuitQuery for EnvCircuitQuery { &new_env_alloc, )?; + let env_alloc = AllocatedPtr::from_parts(env_tag.clone(), env.clone()); + let these_args = construct_cons( + &mut cs.namespace(|| "these_args"), + g, + store, + &var_alloc, + &env_alloc, + )?; + + let symbol = g.alloc_ptr( + &mut cs.namespace(|| "symbol_"), + &self.symbol_ptr(store), + store, + ); + + let query = construct_cons( + &mut cs.namespace(|| "query"), + g, + store, + &symbol, + &these_args, + )?; + self.recurse( cs, g, store, scope, + &query, &recursive_args, &is_immediate.not(), (&immediate_result, acc, transcript), @@ -242,7 +273,7 @@ mod test { #[test] fn test_env_lookup() { let s = Store::::default(); - let mut scope: Scope, LogMemo> = Scope::default(); + let mut scope: Scope, LogMemo, F> = Scope::default(); let a = s.intern_symbol(&sym!("a")); let b = s.intern_symbol(&sym!("b")); let c = s.intern_symbol(&sym!("c")); @@ -305,70 +336,25 @@ mod test { 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, empty, expect!["3524"], expect!["3541"]); - test_lookup_circuit_aux(s, a, a_env, false, expect!["2942"], expect!["2953"]); + test_lookup_circuit_aux(s, a, a_env, expect!["3524"], expect!["3541"]); 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, a_env, expect!["6457"], expect!["6485"]); - 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"]); + test_lookup_circuit_aux(s, b, b_env, expect!["3524"], expect!["3541"]); + test_lookup_circuit_aux(s, a, a2_env, expect!["3524"], expect!["3541"]); 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, b_env, expect!["9390"], expect!["9429"]); - 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"]); + test_lookup_circuit_aux(s, c, c_env, expect!["3524"], expect!["3541"]); + test_lookup_circuit_aux(s, c, a2_env, expect!["6457"], expect!["6485"]); let delta1_constraints = two_lookup_constraints - one_lookup_constraints; let delta2_constraints = three_lookup_constraints - two_lookup_constraints; @@ -377,10 +363,10 @@ mod test { assert_eq!(delta1_constraints, delta2_constraints); // This is the number of constraints per lookup. - expect_eq(delta1_constraints, expect!["2352"]); + expect_eq(delta1_constraints, expect!["2933"]); // This is the number of constraints in the constant overhead. - expect_eq(overhead_constraints, expect!["590"]); + expect_eq(overhead_constraints, expect!["591"]); let delta1_aux = two_lookup_aux - one_lookup_aux; let delta2_aux = three_lookup_aux - two_lookup_aux; @@ -389,10 +375,10 @@ mod test { assert_eq!(delta1_aux, delta2_aux); // This is the number of aux per lookup. - expect_eq(delta1_aux, expect!["2360"]); + expect_eq(delta1_aux, expect!["2944"]); // This is the number of aux in the constant overhead. - expect_eq(overhead_aux, expect!["593"]); + expect_eq(overhead_aux, expect!["597"]); } } @@ -400,7 +386,6 @@ mod test { s: &Store, sym: Ptr, env: Ptr, - transcribe_internal_insertions: bool, expected_constraints_simple: Expect, expected_aux_simple: Expect, ) -> (usize, usize) { @@ -409,8 +394,7 @@ mod test { expected.assert_eq(&computed.to_string()); }; - let mut scope: Scope, LogMemo> = - Scope::new(transcribe_internal_insertions, 1); + let mut scope: Scope, LogMemo, F> = Scope::new(1); let make_query = |sym, env| EnvQuery::Lookup(sym, env).to_ptr(s); diff --git a/src/coroutine/memoset/mod.rs b/src/coroutine/memoset/mod.rs index 7b9196f939..84528c477f 100644 --- a/src/coroutine/memoset/mod.rs +++ b/src/coroutine/memoset/mod.rs @@ -2,7 +2,7 @@ //! //! A `MemoSet` is an abstraction we use to memoize deferred proof of (potentially mutually-recursive) query results. //! Whenever a computation being proved needs the result of a query, the prover non-deterministically supplies the -//! correct response. The resulting key-value pair is then added to a multiset representing deferred proofs. The +//! correct result. The resulting key-value pair is then added to a multiset representing deferred proofs. The //! dependent proof now must not be accepted until every element in the deferred-proof multiset has been proved. //! //! Implementation depends on a cryptographic multiset -- for example, ECMH or LogUp (implemented here). This allows us @@ -28,7 +28,8 @@ //! prover will follow when provably maintaining the multiset accumulator and Fiat-Shamir transcript in the circuit. use itertools::Itertools; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; +use std::fmt::{Debug, Formatter}; use std::marker::PhantomData; use bellpepper_core::{boolean::Boolean, num::AllocatedNum, ConstraintSystem, SynthesisError}; @@ -39,11 +40,16 @@ use crate::circuit::gadgets::{ constraints::{enforce_equal, enforce_equal_zero, invert, sub}, pointer::AllocatedPtr, }; -use crate::coprocessor::gadgets::construct_cons; // FIXME: Move to common location. +use crate::coprocessor::gadgets::{ + construct_cons, construct_list, construct_provenance, deconstruct_provenance, +}; use crate::field::LurkField; use crate::lem::circuit::GlobalAllocator; use crate::lem::tag::Tag; -use crate::lem::{pointers::Ptr, store::Store}; +use crate::lem::{ + pointers::Ptr, + store::{Store, WithStore}, +}; use crate::tag::{ExprTag, Tag as XTag}; use crate::z_ptr::ZPtr; @@ -55,6 +61,12 @@ mod env; mod multiset; mod query; +#[derive(Debug)] +pub enum MemoSetError { + QueryDependenciesMissing, + QueryResultMissing, +} + #[derive(Clone, Debug)] pub struct Transcript { acc: Ptr, @@ -78,9 +90,9 @@ impl Transcript { s.cons(key, value) } - fn make_kv_count(s: &Store, kv: Ptr, count: usize) -> Ptr { + fn make_provenance_count(s: &Store, provenance: Ptr, count: usize) -> Ptr { let count_num = s.num(F::from_u64(count as u64)); - s.cons(kv, count_num) + s.cons(provenance, count_num) } /// Since the transcript is just a content-addressed Lurk list, its randomness is the hash value of the associated @@ -138,21 +150,11 @@ impl CircuitTranscript { Ok(Self { acc }) } - fn make_kv>( - cs: &mut CS, - g: &GlobalAllocator, - s: &Store, - key: &AllocatedPtr, - value: &AllocatedPtr, - ) -> Result, SynthesisError> { - construct_cons(cs, g, s, key, value) - } - - fn make_kv_count>( + fn make_provenance_count>( cs: &mut CS, g: &GlobalAllocator, s: &Store, - kv: &AllocatedPtr, + provenance: &AllocatedPtr, count: u64, ) -> Result<(AllocatedPtr, AllocatedNum), SynthesisError> { let allocated_count = @@ -163,7 +165,10 @@ impl CircuitTranscript { allocated_count.clone(), )?; - Ok((construct_cons(cs, g, s, kv, &count_ptr)?, allocated_count)) + Ok(( + construct_cons(cs, g, s, provenance, &count_ptr)?, + allocated_count, + )) } fn r(&self) -> &AllocatedNum { @@ -178,69 +183,222 @@ impl CircuitTranscript { } } +#[derive(Debug)] +pub struct Provenance { + ptr: OnceCell, + query: Ptr, + result: Ptr, + // Dependencies is an ordered list of provenance(Ptr)s on which this depends. + dependencies: Vec, +} + +impl Provenance { + fn new( + query: Ptr, + result: Ptr, + // Provenances on which this depends. + dependencies: Vec, + ) -> Self { + Self { + ptr: OnceCell::new(), + query, + result, + dependencies, + } + } + + fn to_ptr(&self, store: &Store) -> &Ptr { + self.ptr.get_or_init(|| { + let dependencies_list = if self.dependencies.len() == 1 { + self.dependencies[0] + } else { + store.list(self.dependencies.clone()) + }; + + store.push_provenance(self.query, self.result, dependencies_list) + }) + } +} + +#[derive(Debug)] +pub struct AllocatedProvenance { + ptr: OnceCell>, + query: AllocatedPtr, + result: AllocatedPtr, + // Dependencies is an ordered list of provenance(Ptr)s on which this depends. + dependencies: Vec>, +} + +impl AllocatedProvenance { + fn new( + query: AllocatedPtr, + result: AllocatedPtr, + // Provenances on which this depends. + dependencies: Vec>, + ) -> Self { + Self { + ptr: OnceCell::new(), + query, + result, + dependencies, + } + } + + fn to_ptr>( + &self, + cs: &mut CS, + g: &GlobalAllocator, + s: &Store, + ) -> Result<&AllocatedPtr, SynthesisError> { + self.ptr.get_or_try_init(|| { + let deps = { + let arity = self.dependencies.len(); + + if arity == 1 { + self.dependencies[0].clone() + } else { + // TODO: Use a hash of exactly `arity` instead of a Lurk list. + construct_list(ns!(cs, "dependencies_list"), g, s, &self.dependencies, None)? + } + }; + + construct_provenance( + ns!(cs, "provenance"), + g, + s, + self.query.hash(), + &self.result, + deps.hash(), + ) + }) + } +} + +type PW<'a, F> = WithStore<'a, F, Provenance>; + +impl<'a, F: LurkField> Debug for PW<'a, F> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), std::fmt::Error> { + let p = self.inner(); + let s = self.store(); + + f.debug_struct("Provenance") + .field("full", &p.to_ptr(s).fmt_to_string_simple(s)) + .field("query", &p.query.fmt_to_string_simple(s)) + .field( + "dependencies", + &p.dependencies + .iter() + .map(|ptr| ptr.fmt_to_string_simple(s)) + .join(", "), + ) + .finish() + } +} + #[derive(Clone, Debug)] /// A `Scope` tracks the queries made while evaluating, including the subqueries that result from evaluating other /// queries -- then makes use of the bookkeeping performed at evaluation time to synthesize proof of each query /// performed. -pub struct Scope { +pub struct Scope { memoset: M, /// k => v queries: HashMap, /// k => ordered subqueries dependencies: HashMap>, + /// inverse of dependencies + dependents: HashMap>, /// kv pairs toplevel_insertions: Vec, /// internally-inserted keys internal_insertions: Vec, /// unique keys: query-index -> [key] unique_inserted_keys: HashMap>, - transcribe_internal_insertions: bool, // This may become an explicit map or something allowing more fine-grained control. + provenances: OnceCell, ZPtr>>, default_rc: usize, } const DEFAULT_RC_FOR_QUERY: usize = 1; -const DEFAULT_TRANSCRIBE_INTERNAL_INSERTIONS: bool = false; -impl Default for Scope> { +impl> Default for Scope, F> { fn default() -> Self { - Self::new(DEFAULT_TRANSCRIBE_INTERNAL_INSERTIONS, DEFAULT_RC_FOR_QUERY) + Self::new(DEFAULT_RC_FOR_QUERY) } } -impl Scope> { - fn new(transcribe_internal_insertions: bool, default_rc: usize) -> Self { +impl> Scope, F> { + fn new(default_rc: usize) -> Self { Self { memoset: Default::default(), queries: Default::default(), dependencies: Default::default(), + dependents: Default::default(), toplevel_insertions: Default::default(), internal_insertions: Default::default(), unique_inserted_keys: Default::default(), - transcribe_internal_insertions, + provenances: Default::default(), default_rc, } } + + fn provenance(&self, store: &Store, query: Ptr) -> Result { + let query_dependencies = self.dependencies.get(&query); + let result = self + .queries + .get(&query) + .ok_or(MemoSetError::QueryResultMissing)?; + + let dependencies = if let Some(deps) = query_dependencies { + Ok(deps + .iter() + .map(|query| { + let ptr = query.to_ptr(store); + *self.provenance(store, ptr).unwrap().to_ptr(store) + }) + .collect()) + } else { + Err(MemoSetError::QueryDependenciesMissing) + }?; + + Ok(Provenance::new(query, *result, dependencies)) + } + + fn provenance_from_kv(&self, store: &Store, kv: Ptr) -> Result { + let (query, result) = store.car_cdr(&kv).expect("kv missing"); + let query_dependencies = self.dependencies.get(&query); + + let dependencies = if let Some(deps) = query_dependencies { + Ok(deps + .iter() + .map(|query| { + let ptr = query.to_ptr(store); + *self.provenance(store, ptr).unwrap().to_ptr(store) + }) + .collect()) + } else { + Ok(Vec::new()) + }?; + + Ok(Provenance::new(query, result, dependencies)) + } } #[derive(Debug, Clone)] pub struct CircuitScope { memoset: CM, // CircuitMemoSet - /// k -> v - queries: HashMap, ZPtr>, + /// k -> prov + provenances: HashMap, ZPtr>, /// k -> allocated v transcript: CircuitTranscript, acc: Option>, - transcribe_internal_insertions: bool, } pub struct CoroutineCircuit<'a, F: LurkField, CM, Q> { - queries: &'a HashMap, + provenances: HashMap, ZPtr>, memoset: CM, keys: Vec, query_index: usize, store: &'a Store, - transcribe_internal_insertions: bool, rc: usize, _p: PhantomData, } @@ -249,7 +407,7 @@ pub struct CoroutineCircuit<'a, F: LurkField, CM, Q> { // That will require a CircuitScopeTrait. impl<'a, F: LurkField, Q: Query> CoroutineCircuit<'a, F, LogMemoCircuit, Q> { fn new( - scope: &'a Scope>, + scope: &'a Scope, F>, memoset: LogMemoCircuit, keys: Vec, query_index: usize, @@ -259,11 +417,10 @@ impl<'a, F: LurkField, Q: Query> CoroutineCircuit<'a, F, LogMemoCircuit, Q assert!(keys.len() <= rc); Self { memoset, - queries: &scope.queries, + provenances: scope.provenances(store).clone(), // FIXME keys, query_index, store, - transcribe_internal_insertions: scope.transcribe_internal_insertions, rc, _p: Default::default(), } @@ -283,14 +440,8 @@ impl<'a, F: LurkField, Q: Query> CoroutineCircuit<'a, F, LogMemoCircuit, Q unreachable!() }; - let mut circuit_scope: CircuitScope> = CircuitScope::from_queries( - cs, - g, - self.store, - self.memoset.clone(), - self.queries, - self.transcribe_internal_insertions, - ); + let mut circuit_scope: CircuitScope> = + CircuitScope::new(cs, g, self.store, self.memoset.clone(), &self.provenances); circuit_scope.update_from_io(memoset_acc.clone(), transcript.clone(), r); for (i, key) in self @@ -300,7 +451,7 @@ impl<'a, F: LurkField, Q: Query> CoroutineCircuit<'a, F, LogMemoCircuit, Q .pad_using(self.rc, |_| None) .enumerate() { - let cs = &mut cs.namespace(|| format!("internal-{i}")); + let cs = ns!(cs, format!("internal-{i}")); circuit_scope.synthesize_prove_key_query::<_, Q>( cs, g, @@ -311,7 +462,7 @@ impl<'a, F: LurkField, Q: Query> CoroutineCircuit<'a, F, LogMemoCircuit, Q } let (memoset_acc, transcript, r_num) = circuit_scope.io(); - let r = AllocatedPtr::alloc_tag(&mut cs.namespace(|| "r"), ExprTag::Num.to_field(), r_num)?; + let r = AllocatedPtr::alloc_tag(ns!(cs, "r"), ExprTag::Num.to_field(), r_num)?; let z_out = vec![c.clone(), e.clone(), k.clone(), memoset_acc, transcript, r]; @@ -320,31 +471,51 @@ impl<'a, F: LurkField, Q: Query> CoroutineCircuit<'a, F, LogMemoCircuit, Q } } -impl> Scope> { +impl> Scope, F> { pub fn query(&mut self, s: &Store, form: Ptr) -> Ptr { - let (response, kv_ptr) = self.query_aux(s, form); + let (result, kv_ptr) = self.query_aux(s, form); self.toplevel_insertions.push(kv_ptr); - response + result } fn query_recursively(&mut self, s: &Store, parent: &Q, child: Q) -> Ptr { let form = child.to_ptr(s); + self.internal_insertions.push(form); - let (response, _) = self.query_aux(s, form); + let (result, _) = self.query_aux(s, form); + + self.register_dependency(s, parent, child); + result + } + + fn register_dependency(&mut self, s: &Store, parent: &Q, child: Q) { + let parent_ptr = parent.to_ptr(s); + + self.dependents + .entry(child.to_ptr(s)) + .and_modify(|parents| { + parents.insert(parent_ptr); + }) + .or_insert_with(|| { + let mut set = HashSet::new(); + set.insert(parent_ptr); + set + }); self.dependencies - .entry(parent.to_ptr(s)) + .entry(parent_ptr) .and_modify(|children| children.push(child.clone())) .or_insert_with(|| vec![child]); - - response } fn query_aux(&mut self, s: &Store, form: Ptr) -> (Ptr, Ptr) { - let response = self.queries.get(&form).cloned().unwrap_or_else(|| { + // Ensure base-case queries explicitly contain no dependencies. + self.dependencies.entry(form).or_insert_with(|| Vec::new()); + + let result = self.queries.get(&form).cloned().unwrap_or_else(|| { let query = Q::from_ptr(s, &form).expect("invalid query"); let evaluated = query.eval(s, self); @@ -353,19 +524,113 @@ impl> Scope> { evaluated }); - let kv = Transcript::make_kv(s, form, response); + let kv = Transcript::make_kv(s, form, result); + + // FIXME: The memoset should hold the provenances, not the kvs. self.memoset.add(kv); - (response, kv) + (result, kv) } fn finalize_transcript(&mut self, s: &Store) -> Transcript { let (transcript, insertions) = self.build_transcript(s); self.memoset.finalize_transcript(s, transcript.clone()); self.unique_inserted_keys = insertions; + transcript } + fn provenances(&self, store: &Store) -> &HashMap, ZPtr> { + self.provenances + .get_or_init(|| self.compute_provenances(store)) + } + + // Retain for use when debugging. + // + // fn dbg_provenances(&self, store: &Store) { + // Self::dbg_provenances_zptrs(store, self.provenances(store)); + // } + + // fn dbg_provenances_ptrs(store: &Store, provenances: &HashMap) { + // for provenance in provenances.values() { + // dbg!(provenance.fmt_to_string_simple(store)); + // } + // } + + // fn dbg_provenances_zptrs(store: &Store, provenances: &HashMap, ZPtr>) { + // for (q, provenance) in provenances { + // dbg!( + // store.to_ptr(q).fmt_to_string_simple(store), + // store.to_ptr(provenance).fmt_to_string_simple(store) + // ); + // } + // } + + fn compute_provenances(&self, store: &Store) -> HashMap, ZPtr> { + let base_cases = self + .queries + .keys() + .filter(|key| { + if let Some(deps) = self.dependencies.get(key) { + deps.is_empty() + } else { + true + } + }) + .collect::>(); + let mut todo = base_cases; + let mut provenances = HashMap::default(); + + while !todo.is_empty() { + todo = self.extend_provenances(store, &mut provenances, todo); + } + + provenances + .iter() + .map(|(k, v)| (store.hash_ptr(k), store.hash_ptr(v))) + .collect() + } + + fn extend_provenances( + &self, + store: &Store, + provenances: &mut HashMap, + todo: HashSet<&Ptr>, + ) -> HashSet<&Ptr> { + let mut next = HashSet::new(); + + for query in todo.into_iter() { + if provenances.get(query).is_some() { + continue; + }; + + let sub_provenances = self + .dependencies + .get(query) + .expect("dependencies missing") + .iter() + .map(|dep| provenances.get(&dep.to_ptr(store)).unwrap()) + .cloned() + .collect::>(); + + let result = self.queries.get(query).expect("result missing"); + let p = Provenance::new(*query, *result, sub_provenances.clone()); + let provenance = p.to_ptr(store); + + if let Some(dependents) = self.dependents.get(query) { + for dependent in dependents { + if provenances.get(dependent).is_none() { + next.insert(dependent); + } + } + }; + + provenances.insert(*query, *provenance); + } + + next + } + fn ensure_transcript_finalized(&mut self, s: &Store) { if !self.memoset.is_finalized() { self.finalize_transcript(s); @@ -409,7 +674,8 @@ impl> Scope> { insert(kv); } for kv in self.toplevel_insertions.iter() { - transcript.add(s, *kv); + let provenance = self.provenance_from_kv(s, *kv).unwrap(); + transcript.add(s, *provenance.to_ptr(s)); } // Then add insertions and removals interleaved, sorted by query type. We interleave insertions and removals @@ -419,29 +685,16 @@ impl> Scope> { for index in 0..Q::count() { for key in unique_keys.get(&index).expect("unreachable") { for kv in insertions.get(key).unwrap().iter() { - if let Some(dependencies) = self.dependencies.get(key) { - dependencies.iter().for_each(|dependency| { - let k = dependency.to_ptr(s); - let v = self - .queries - .get(&k) - .expect("value missing for dependency key"); - // Add an insertion for each dependency (subquery) of the query identified by `key`. Notice - // that these keys might already have been inserted before, but we need to repeat if so - // because the proof must do so each time a query is used. - let kv = Transcript::make_kv(s, k, *v); - if self.transcribe_internal_insertions { - transcript.add(s, kv) - } - }) - }; + let provenance = self.provenance_from_kv(s, *kv).unwrap(); + let prov = provenance.to_ptr(s); let count = self.memoset.count(kv); - let kv_count = Transcript::make_kv_count(s, *kv, count); + + let prov_count = Transcript::make_provenance_count(s, *prov, count); // Add removal for the query identified by `key`. The queries being removed here were deduplicated // above, so each is removed only once. However, we freely choose the multiplicity (`count`) of the // removal to match the total number of insertions actually made (considering dependencies). - transcript.add(s, kv_count); + transcript.add(s, prov_count); } } } @@ -457,29 +710,23 @@ impl> Scope> { self.ensure_transcript_finalized(s); // FIXME: Do we need to allocate a new GlobalAllocator here? // Is it okay for this memoset circuit to be shared between all CoroutineCircuits? - let memoset_circuit = self - .memoset - .to_circuit(&mut cs.namespace(|| "memoset_circuit")); + let memoset_circuit = self.memoset.to_circuit(ns!(cs, "memoset_circuit")); - let mut circuit_scope = CircuitScope::from_queries( - &mut cs.namespace(|| "transcript"), + let mut circuit_scope = CircuitScope::new( + ns!(cs, "transcript"), g, s, memoset_circuit.clone(), - &self.queries, - self.transcribe_internal_insertions, + self.provenances(s), ); + circuit_scope.init(cs, g, s); { circuit_scope.synthesize_insert_toplevel_queries(self, cs, g, s)?; { let (memoset_acc, transcript, r_num) = circuit_scope.io(); - let r = AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "r"), - ExprTag::Num.to_field(), - r_num, - )?; + let r = AllocatedPtr::alloc_tag(ns!(cs, "r"), ExprTag::Num.to_field(), r_num)?; let dummy = g.alloc_ptr(cs, &s.intern_nil(), s); let mut z = vec![ dummy.clone(), @@ -490,14 +737,14 @@ impl> Scope> { r, ]; for (index, keys) in self.unique_inserted_keys.iter() { - let cs = &mut cs.namespace(|| format!("query-index-{index}")); + let cs = ns!(cs, format!("query-index-{index}")); let rc = self.rc_for_query(*index); for (i, chunk) in keys.chunks(rc).enumerate() { // This namespace exists only because we are putting multiple 'chunks' into a single, larger circuit (as a stage in development). // It shouldn't exist, when instead we have only the single NIVC circuit repeated multiple times. - let cs = &mut cs.namespace(|| format!("chunk-{i}")); + let cs = ns!(cs, format!("chunk-{i}")); let mut circuit: CoroutineCircuit<'_, F, LogMemoCircuit, Q> = CoroutineCircuit::new( @@ -539,25 +786,18 @@ impl> Scope> { } impl CircuitScope> { - fn from_queries>( + fn new>( cs: &mut CS, g: &mut GlobalAllocator, s: &Store, memoset: LogMemoCircuit, - queries: &HashMap, - transcribe_internal_insertions: bool, + provenances: &HashMap, ZPtr>, ) -> Self { - let queries = queries - .iter() - .map(|(k, v)| (s.hash_ptr(k), s.hash_ptr(v))) - .collect(); - Self { memoset, - queries, + provenances: provenances.clone(), // FIXME transcript: CircuitTranscript::new(cs, g, s), acc: Default::default(), - transcribe_internal_insertions, } } @@ -567,10 +807,8 @@ impl CircuitScope> { g: &mut GlobalAllocator, s: &Store, ) { - self.acc = Some( - AllocatedPtr::alloc_constant(&mut cs.namespace(|| "acc"), s.hash_ptr(&s.num_u64(0))) - .unwrap(), - ); + self.acc = + Some(AllocatedPtr::alloc_constant(ns!(cs, "acc"), s.hash_ptr(&s.num_u64(0))).unwrap()); self.transcript = CircuitTranscript::new(cs, g, s); } @@ -601,28 +839,23 @@ impl CircuitScope> { s: &Store, acc: &AllocatedPtr, transcript: &CircuitTranscript, - key: &AllocatedPtr, - value: &AllocatedPtr, + provenance: &AllocatedPtr, is_toplevel: bool, ) -> Result<(AllocatedPtr, CircuitTranscript), SynthesisError> { - let kv = CircuitTranscript::make_kv(&mut cs.namespace(|| "kv"), g, s, key, value)?; - let new_transcript = if is_toplevel || self.transcribe_internal_insertions { - transcript.add(&mut cs.namespace(|| "new_transcript"), g, s, &kv)? + let new_transcript = if is_toplevel { + transcript.add(ns!(cs, "new_transcript"), g, s, provenance)? } else { transcript.clone() }; let acc_v = acc.hash(); - let new_acc_v = - self.memoset - .synthesize_add(&mut cs.namespace(|| "new_acc_v"), acc_v, &kv)?; + let new_acc_v = self + .memoset + .synthesize_add(ns!(cs, "new_acc_v"), acc_v, provenance)?; - let new_acc = AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "new_acc"), - ExprTag::Num.to_field(), - new_acc_v, - )?; + let new_acc = + AllocatedPtr::alloc_tag(ns!(cs, "new_acc"), ExprTag::Num.to_field(), new_acc_v)?; Ok((new_acc, new_transcript.clone())) } @@ -636,37 +869,37 @@ impl CircuitScope> { transcript: &CircuitTranscript, key: &AllocatedPtr, value: &AllocatedPtr, + provenance: &AllocatedPtr, ) -> Result<(AllocatedPtr, CircuitTranscript), SynthesisError> { - let kv = CircuitTranscript::make_kv(&mut cs.namespace(|| "kv"), g, s, key, value)?; - let zptr = kv.get_value().unwrap_or(s.hash_ptr(&s.intern_nil())); // dummy case: use nil - let raw_count = self.memoset.count(&s.to_ptr(&zptr)) as u64; // dummy case: count is meaningless + let raw_count = match (key.get_value(), value.get_value()) { + (Some(k), Some(v)) => { + // FIXME: Memoset should hold the actual provenances, not the kvs. + let kv = s.cons(s.to_ptr(&k), s.to_ptr(&v)); + self.memoset.count(&kv) as u64 + } + _ => 0, // dummy case: count is meaningless + }; - let (kv_count, count) = CircuitTranscript::make_kv_count( - &mut cs.namespace(|| "kv_count"), + let (provenance_count, count) = CircuitTranscript::make_provenance_count( + ns!(cs, "kv count"), g, s, - &kv, + provenance, raw_count, )?; - let new_transcript = transcript.add( - &mut cs.namespace(|| "new_removal_transcript"), - g, - s, - &kv_count, - )?; + + let new_transcript = + transcript.add(ns!(cs, "new_removal_transcript"), g, s, &provenance_count)?; let new_acc_v = self.memoset.synthesize_remove_n( - &mut cs.namespace(|| "new_acc_v"), + ns!(cs, "new_acc_v"), acc.hash(), - &kv, + provenance, &count, )?; - let new_acc = AllocatedPtr::alloc_tag( - &mut cs.namespace(|| "new_acc"), - ExprTag::Num.to_field(), - new_acc_v, - )?; + let new_acc = + AllocatedPtr::alloc_tag(ns!(cs, "new_acc"), ExprTag::Num.to_field(), new_acc_v)?; Ok((new_acc, new_transcript)) } @@ -685,7 +918,14 @@ impl CircuitScope> { acc: &AllocatedPtr, transcript: &CircuitTranscript, not_dummy: &Boolean, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + ) -> Result< + ( + (AllocatedPtr, AllocatedPtr), + AllocatedPtr, + CircuitTranscript, + ), + SynthesisError, + > { self.synthesize_query_aux(cs, g, store, key, acc, transcript, not_dummy, true) } @@ -698,7 +938,14 @@ impl CircuitScope> { acc: &AllocatedPtr, transcript: &CircuitTranscript, not_dummy: &Boolean, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + ) -> Result< + ( + (AllocatedPtr, AllocatedPtr), + AllocatedPtr, + CircuitTranscript, + ), + SynthesisError, + > { self.synthesize_query_aux(cs, g, store, key, acc, transcript, not_dummy, false) } @@ -712,11 +959,18 @@ impl CircuitScope> { transcript: &CircuitTranscript, not_dummy: &Boolean, // TODO: use this more deeply? is_toplevel: bool, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { - let value = AllocatedPtr::alloc(&mut cs.namespace(|| "value"), || { + ) -> Result< + ( + (AllocatedPtr, AllocatedPtr), + AllocatedPtr, + CircuitTranscript, + ), + SynthesisError, + > { + let provenance = AllocatedPtr::alloc(ns!(cs, "provenance"), || { Ok(if not_dummy.get_value() == Some(true) { *key.get_value() - .and_then(|k| self.queries.get(&k)) + .and_then(|k| self.provenances.get(&k)) .ok_or(SynthesisError::AssignmentMissing)? } else { // Dummy value that will not be used. @@ -724,15 +978,22 @@ impl CircuitScope> { }) })?; + let (_query, result, _deps) = deconstruct_provenance( + ns!(cs, "decons provenance"), + store, + not_dummy, + provenance.hash(), + )?; + let (new_acc, new_insertion_transcript) = - self.synthesize_insert_query(cs, g, store, acc, transcript, key, &value, is_toplevel)?; + self.synthesize_insert_query(cs, g, store, acc, transcript, &provenance, is_toplevel)?; - Ok((value, new_acc, new_insertion_transcript)) + Ok(((result, provenance), new_acc, new_insertion_transcript)) } fn synthesize_insert_toplevel_queries, Q: Query>( &mut self, - scope: &mut Scope>, + scope: &mut Scope, F>, cs: &mut CS, g: &mut GlobalAllocator, s: &Store, @@ -752,16 +1013,14 @@ impl CircuitScope> { kv: &Ptr, ) -> Result<(), SynthesisError> { let (key, value) = s.car_cdr(kv).unwrap(); - let cs = &mut cs.namespace(|| format!("toplevel-{i}")); - let allocated_key = AllocatedPtr::alloc(&mut cs.namespace(|| "allocated_key"), || { - Ok(s.hash_ptr(&key)) - }) - .unwrap(); + 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(); - let (val, new_acc, new_transcript) = self.synthesize_query( + let ((val, _provenance), new_acc, new_transcript) = self.synthesize_query( cs, g, s, @@ -788,7 +1047,7 @@ impl CircuitScope> { key: Option<&Ptr>, index: usize, ) -> Result<(), SynthesisError> { - let allocated_key = AllocatedPtr::alloc(&mut cs.namespace(|| "allocated_key"), || { + let allocated_key = AllocatedPtr::alloc(ns!(cs, "allocated_key"), || { if let Some(key) = key { Ok(s.hash_ptr(key)) } else { @@ -798,9 +1057,9 @@ impl CircuitScope> { .unwrap(); let circuit_query = if let Some(key) = key { - Q::CQ::from_ptr(&mut cs.namespace(|| "circuit_query"), s, key).unwrap() + Q::CQ::from_ptr(ns!(cs, "circuit_query"), s, key).unwrap() } else { - Q::CQ::dummy_from_index(&mut cs.namespace(|| "circuit_query"), s, index) + Q::CQ::dummy_from_index(ns!(cs, "circuit_query"), s, index) }; let not_dummy = key.is_some(); @@ -828,22 +1087,30 @@ impl CircuitScope> { let acc = self.acc.clone().unwrap(); let transcript = self.transcript.clone(); - let (val, new_acc, new_transcript) = circuit_query - .synthesize_eval(&mut cs.namespace(|| "eval"), g, s, self, &acc, &transcript) + let ((val, provenance), new_acc, new_transcript) = circuit_query + .synthesize_eval(ns!(cs, "eval"), g, s, self, &acc, &transcript) .unwrap(); - let (new_acc, new_transcript) = - self.synthesize_remove(cs, g, s, &new_acc, &new_transcript, allocated_key, &val)?; + let (new_acc, new_transcript) = self.synthesize_remove( + cs, + g, + s, + &new_acc, + &new_transcript, + allocated_key, + &val, + &provenance, + )?; // Prover can choose non-deterministically whether or not a given query is a dummy, to allow for padding. let final_acc = AllocatedPtr::pick( - &mut cs.namespace(|| "final_acc"), + ns!(cs, "final_acc"), &Boolean::Constant(not_dummy), &new_acc, self.acc.as_ref().expect("acc missing"), )?; let final_transcript = CircuitTranscript::pick( - &mut cs.namespace(|| "final_transcripot"), + ns!(cs, "final_transcript"), &Boolean::Constant(not_dummy), &new_transcript, &self.transcript, @@ -892,7 +1159,6 @@ pub trait CircuitMemoSet: Clone { pub trait MemoSet: Clone { type CM: CircuitMemoSet; - fn into_circuit>(self, cs: &mut CS) -> Self::CM; fn to_circuit>(&self, cs: &mut CS) -> Self::CM; fn is_finalized(&self) -> bool; @@ -905,6 +1171,7 @@ pub trait MemoSet: Clone { #[derive(Debug, Clone)] pub struct LogMemo { + // {kv, ...} multiset: MultiSet, r: OnceCell, transcript: OnceCell>, @@ -935,7 +1202,7 @@ impl LogMemo { self.allocated_r .get_or_init(|| { self.r() - .map(|r| AllocatedNum::alloc_infallible(&mut cs.namespace(|| "r"), || *r)) + .map(|r| AllocatedNum::alloc_infallible(ns!(cs, "r"), || *r)) }) .clone() .unwrap() @@ -945,14 +1212,6 @@ impl LogMemo { impl MemoSet for LogMemo { type CM = LogMemoCircuit; - fn into_circuit>(self, cs: &mut CS) -> Self::CM { - let r = self.allocated_r(cs); - LogMemoCircuit { - multiset: self.multiset, - r, - } - } - fn to_circuit>(&self, cs: &mut CS) -> Self::CM { let r = self.allocated_r(cs); LogMemoCircuit { @@ -972,7 +1231,6 @@ impl MemoSet for LogMemo { let r = transcript.r(s); self.r.set(r).expect("r has already been set"); - self.transcript .set(transcript) .expect("transcript already finalized"); @@ -1004,27 +1262,27 @@ impl CircuitMemoSet for LogMemoCircuit { &self, cs: &mut CS, acc: &AllocatedNum, - kv: &AllocatedPtr, + provenance: &AllocatedPtr, ) -> Result, SynthesisError> { - let kv_num = kv.hash().clone(); - let element = self.synthesize_map_to_element(&mut cs.namespace(|| "element"), kv_num)?; - acc.add(&mut cs.namespace(|| "add to acc"), &element) + let provenance_num = provenance.hash().clone(); + let element = self.synthesize_map_to_element(ns!(cs, "element"), provenance_num)?; + acc.add(ns!(cs, "add to acc"), &element) } fn synthesize_remove_n>( &self, cs: &mut CS, acc: &AllocatedNum, - kv: &AllocatedPtr, + provenance: &AllocatedPtr, count: &AllocatedNum, ) -> Result, SynthesisError> { - let kv_num = kv.hash().clone(); - let element = self.synthesize_map_to_element(&mut cs.namespace(|| "element"), kv_num)?; - let scaled = element.mul(&mut cs.namespace(|| "scaled"), count)?; - sub(&mut cs.namespace(|| "add to acc"), acc, &scaled) + let provenance_num = provenance.hash().clone(); + let element = self.synthesize_map_to_element(ns!(cs, "element"), provenance_num)?; + let scaled = element.mul(ns!(cs, "scaled"), count)?; + sub(ns!(cs, "add to acc"), acc, &scaled) } - // x is H(k,v) = hash part of (cons k v) + // x is H(provenance) = hash part of (cons (cons k v) sub-provenances) // 1 / r + x fn synthesize_map_to_element>( &self, @@ -1032,9 +1290,9 @@ impl CircuitMemoSet for LogMemoCircuit { x: AllocatedNum, ) -> Result, SynthesisError> { let r = self.r.clone(); - let r_plus_x = r.add(&mut cs.namespace(|| "r+x"), &x)?; + let r_plus_x = r.add(ns!(cs, "r+x"), &x)?; - invert(&mut cs.namespace(|| "invert(r+x)"), &r_plus_x) + invert(ns!(cs, "invert(r+x)"), &r_plus_x) } fn count(&self, form: &Ptr) -> usize { @@ -1054,63 +1312,31 @@ mod test { use std::default::Default; #[test] - fn test_query_with_internal_insertion_transcript() { - test_query_aux( - true, - expect!["9430"], - expect!["9463"], - expect!["10012"], - expect!["10049"], - 1, - ); - test_query_aux( - true, - expect!["11174"], - expect!["11213"], - expect!["11756"], - expect!["11799"], - 3, - ); - test_query_aux( - true, - expect!["18216"], - expect!["18279"], - expect!["18798"], - expect!["18865"], - 10, - ) - } - - #[test] - fn test_query_without_internal_insertion_transcript() { + fn test_query() { test_query_aux( - false, - expect!["7985"], - expect!["8018"], - expect!["8567"], - expect!["8604"], + expect!["9451"], + expect!["9502"], + expect!["10034"], + expect!["10092"], 1, ); test_query_aux( - false, - expect!["9440"], - expect!["9479"], - expect!["10022"], - expect!["10065"], + expect!["11195"], + expect!["11255"], + expect!["11778"], + expect!["11845"], 3, ); test_query_aux( - false, - expect!["15326"], - expect!["15389"], - expect!["15908"], - expect!["15975"], + expect!["18248"], + expect!["18344"], + expect!["18831"], + expect!["18934"], 10, ) } fn test_query_aux( - transcribe_internal_insertions: bool, expected_constraints_simple: Expect, expected_aux_simple: Expect, expected_constraints_compound: Expect, @@ -1118,8 +1344,7 @@ mod test { circuit_query_rc: usize, ) { let s = &Store::::default(); - let mut scope: Scope, LogMemo> = - Scope::new(transcribe_internal_insertions, circuit_query_rc); + let mut scope: Scope, LogMemo, F> = Scope::new(circuit_query_rc); let state = State::init_lurk_state(); let fact_4 = s.read_with_default_state("(factorial . 4)").unwrap(); @@ -1171,8 +1396,7 @@ mod test { } { - let mut scope: Scope, LogMemo> = - Scope::new(transcribe_internal_insertions, circuit_query_rc); + let mut scope: Scope, LogMemo, F> = Scope::new(circuit_query_rc); scope.query(s, fact_4); scope.query(s, fact_3); diff --git a/src/coroutine/memoset/query.rs b/src/coroutine/memoset/query.rs index 8a2eb95ce9..1ce082a392 100644 --- a/src/coroutine/memoset/query.rs +++ b/src/coroutine/memoset/query.rs @@ -1,6 +1,6 @@ use bellpepper_core::{boolean::Boolean, ConstraintSystem, SynthesisError}; -use super::{CircuitScope, CircuitTranscript, LogMemo, LogMemoCircuit, Scope}; +use super::{AllocatedProvenance, CircuitScope, CircuitTranscript, LogMemo, LogMemoCircuit, Scope}; use crate::circuit::gadgets::pointer::AllocatedPtr; use crate::coprocessor::gadgets::construct_cons; use crate::field::LurkField; @@ -14,10 +14,10 @@ where { type CQ: CircuitQuery; - fn eval(&self, s: &Store, scope: &mut Scope>) -> Ptr; + fn eval(&self, s: &Store, scope: &mut Scope, F>) -> Ptr; fn recursive_eval( &self, - scope: &mut Scope>, + scope: &mut Scope, F>, s: &Store, subquery: Self, ) -> Ptr { @@ -51,7 +51,14 @@ where scope: &mut CircuitScope>, acc: &AllocatedPtr, transcript: &CircuitTranscript, - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError>; + ) -> Result< + ( + (AllocatedPtr, AllocatedPtr), + AllocatedPtr, + CircuitTranscript, + ), + SynthesisError, + >; fn symbol(&self) -> Symbol; @@ -79,30 +86,35 @@ pub(crate) trait RecursiveQuery: CircuitQuery { g: &GlobalAllocator, store: &Store, scope: &mut CircuitScope>, + query: &AllocatedPtr, args: &AllocatedPtr, is_recursive: &Boolean, immediate: (&AllocatedPtr, &AllocatedPtr, &CircuitTranscript), - ) -> Result<(AllocatedPtr, AllocatedPtr, CircuitTranscript), SynthesisError> { + ) -> Result< + ( + (AllocatedPtr, 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 symbol = g.alloc_ptr(ns!(cs, "symbol"), &self.symbol_ptr(store), store); + construct_cons(ns!(cs, "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 ((sub_result, sub_provenance), new_acc, new_transcript) = scope + .synthesize_internal_query( + ns!(cs, "recursive query"), + g, + store, + &subquery, + immediate.1, + immediate.2, + is_recursive, + )?; let (recursive_result, recursive_acc, recursive_transcript) = ( self.post_recursion(cs, sub_result)?, @@ -111,26 +123,43 @@ pub(crate) trait RecursiveQuery: CircuitQuery { ); let value = AllocatedPtr::pick( - &mut cs.namespace(|| "pick value"), + ns!(cs, "pick value"), &is_immediate, immediate.0, &recursive_result, )?; let acc = AllocatedPtr::pick( - &mut cs.namespace(|| "pick acc"), + ns!(cs, "pick acc"), &is_immediate, immediate.1, &recursive_acc, )?; let transcript = CircuitTranscript::pick( - &mut cs.namespace(|| "pick recursive_transcript"), + ns!(cs, "pick recursive_transcript"), &is_immediate, immediate.2, &recursive_transcript, )?; - Ok((value, acc, transcript)) + let nil = g.alloc_ptr(ns!(cs, "nil"), &store.intern_nil(), store); + + let dependency_provenance = AllocatedPtr::pick( + ns!(cs, "dependency provenance"), + &is_immediate, + &nil, + &sub_provenance, + )?; + + let p = AllocatedProvenance::new( + query.clone(), + value.clone(), + vec![dependency_provenance.clone()], + ); + + let provenance = p.to_ptr(cs, g, store)?; + + Ok(((value, provenance.clone()), acc, transcript)) } } diff --git a/src/lem/store.rs b/src/lem/store.rs index 9053dcc7d0..f4ec902d10 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -67,6 +67,23 @@ pub struct Store { pub hash8zeros_idx: usize, } +/// `WithStore` provides a distinct type for coupling a store with a value of another type. +pub struct WithStore<'a, F: LurkField, T>(pub T, pub &'a Store); + +impl<'a, F: LurkField, T> WithStore<'a, F, T> { + pub fn store(&self) -> &Store { + self.1 + } + + pub fn inner(&self) -> &T { + &self.0 + } + + pub fn to_inner(self) -> T { + self.0 + } +} + impl Default for Store { fn default() -> Self { let poseidon_cache = PoseidonCache::default(); @@ -395,6 +412,27 @@ impl Store { Some([sym, val, env]) } + #[inline] + pub fn push_provenance(&self, sym: Ptr, val: Ptr, env: Ptr) -> Ptr { + assert_eq!(*sym.tag(), Tag::Expr(Cons)); + //assert_eq!(*env.tag(), Tag::Expr(Env)); + let raw = + self.intern_raw_ptrs::<4>([*sym.raw(), self.tag(*val.tag()), *val.raw(), *env.raw()]); + Ptr::new(Tag::Expr(Env), raw) + } + + #[inline] + pub fn pop_provenance(&self, env: Ptr) -> Option<[Ptr; 3]> { + assert_eq!(*env.tag(), Tag::Expr(Env)); + let idx = env.get_index2()?; + let [sym_pay, val_tag, val_pay, env_pay] = self.fetch_raw_ptrs::<4>(idx)?; + let val_tag = self.fetch_tag(val_tag)?; + let query = Ptr::new(Tag::Expr(Cons), *sym_pay); + let val = Ptr::new(val_tag, *val_pay); + let env = Ptr::new(Tag::Expr(Env), *env_pay); + Some([query, val, env]) + } + #[inline] pub fn intern_empty_env(&self) -> Ptr { self.intern_atom(Tag::Expr(Env), F::ZERO)