From 7420a6c9b4aa83d151870819e294c4bdbbcfad91 Mon Sep 17 00:00:00 2001 From: porcuquine <1746729+porcuquine@users.noreply.github.com> Date: Thu, 15 Feb 2024 14:41:35 -0800 Subject: [PATCH] Add Prov tag. (#1133) * Add Prov tag. * Clippy. * Remove clone. --------- Co-authored-by: porcuquine --- src/coprocessor/gadgets.rs | 5 +-- src/coroutine/memoset/env.rs | 20 +++++----- src/coroutine/memoset/mod.rs | 4 +- src/lem/store.rs | 74 +++++++++++++++++++++++++++++++----- src/tag.rs | 2 + 5 files changed, 81 insertions(+), 24 deletions(-) diff --git a/src/coprocessor/gadgets.rs b/src/coprocessor/gadgets.rs index 4e8ee3ae49..d2274af208 100644 --- a/src/coprocessor/gadgets.rs +++ b/src/coprocessor/gadgets.rs @@ -182,8 +182,7 @@ pub(crate) fn construct_provenance>( result: &AllocatedPtr, deps: &AllocatedNum, ) -> Result, SynthesisError> { - // TODO: should there be a provenance tag? - let tag = g.alloc_tag_cloned(cs, &ExprTag::Env); + let tag = g.alloc_tag_cloned(cs, &ExprTag::Prov); let hash = hash_poseidon( cs, @@ -259,7 +258,7 @@ pub(crate) fn deconstruct_provenance>( provenance: &AllocatedNum, ) -> Result<(AllocatedNum, AllocatedPtr, AllocatedNum), SynthesisError> { let prov_zptr = ZPtr::from_parts( - tag::Tag::Expr(ExprTag::Env), + tag::Tag::Expr(ExprTag::Prov), provenance.get_value().unwrap(), ); let prov_ptr = s.to_ptr(&prov_zptr); diff --git a/src/coroutine/memoset/env.rs b/src/coroutine/memoset/env.rs index 30bf4a5147..11394cfed7 100644 --- a/src/coroutine/memoset/env.rs +++ b/src/coroutine/memoset/env.rs @@ -340,21 +340,21 @@ mod test { // Without internal insertions transcribed. let (one_lookup_constraints, one_lookup_aux) = - test_lookup_circuit_aux(s, a, empty, expect!["3524"], expect!["3541"]); + test_lookup_circuit_aux(s, a, empty, expect!["3525"], expect!["3542"]); - test_lookup_circuit_aux(s, a, a_env, expect!["3524"], expect!["3541"]); + test_lookup_circuit_aux(s, a, a_env, expect!["3525"], expect!["3542"]); let (two_lookup_constraints, two_lookup_aux) = - test_lookup_circuit_aux(s, b, a_env, expect!["6457"], expect!["6485"]); + test_lookup_circuit_aux(s, b, a_env, expect!["6459"], expect!["6487"]); - test_lookup_circuit_aux(s, b, b_env, expect!["3524"], expect!["3541"]); - test_lookup_circuit_aux(s, a, a2_env, expect!["3524"], expect!["3541"]); + test_lookup_circuit_aux(s, b, b_env, expect!["3525"], expect!["3542"]); + test_lookup_circuit_aux(s, a, a2_env, expect!["3525"], expect!["3542"]); let (three_lookup_constraints, three_lookup_aux) = - test_lookup_circuit_aux(s, c, b_env, expect!["9390"], expect!["9429"]); + test_lookup_circuit_aux(s, c, b_env, expect!["9393"], expect!["9432"]); - test_lookup_circuit_aux(s, c, c_env, expect!["3524"], expect!["3541"]); - test_lookup_circuit_aux(s, c, a2_env, expect!["6457"], expect!["6485"]); + test_lookup_circuit_aux(s, c, c_env, expect!["3525"], expect!["3542"]); + test_lookup_circuit_aux(s, c, a2_env, expect!["6459"], expect!["6487"]); let delta1_constraints = two_lookup_constraints - one_lookup_constraints; let delta2_constraints = three_lookup_constraints - two_lookup_constraints; @@ -363,7 +363,7 @@ mod test { assert_eq!(delta1_constraints, delta2_constraints); // This is the number of constraints per lookup. - expect_eq(delta1_constraints, expect!["2933"]); + expect_eq(delta1_constraints, expect!["2934"]); // This is the number of constraints in the constant overhead. expect_eq(overhead_constraints, expect!["591"]); @@ -375,7 +375,7 @@ mod test { assert_eq!(delta1_aux, delta2_aux); // This is the number of aux per lookup. - expect_eq(delta1_aux, expect!["2944"]); + expect_eq(delta1_aux, expect!["2945"]); // 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 84528c477f..91fb23c3ae 100644 --- a/src/coroutine/memoset/mod.rs +++ b/src/coroutine/memoset/mod.rs @@ -215,7 +215,7 @@ impl Provenance { store.list(self.dependencies.clone()) }; - store.push_provenance(self.query, self.result, dependencies_list) + store.intern_provenance(self.query, self.result, dependencies_list) }) } } @@ -614,7 +614,7 @@ impl> Scope, F> { .collect::>(); let result = self.queries.get(query).expect("result missing"); - let p = Provenance::new(*query, *result, sub_provenances.clone()); + let p = Provenance::new(*query, *result, sub_provenances); let provenance = p.to_ptr(store); if let Some(dependents) = self.dependents.get(query) { diff --git a/src/lem/store.rs b/src/lem/store.rs index 28ba1e49b9..09110e7317 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -23,7 +23,9 @@ use crate::{ self, Binop, Binop2, Call, Call0, Call2, Dummy, Emit, If, Let, LetRec, Lookup, Outermost, Tail, Terminal, Unop, }, - tag::ExprTag::{Char, Comm, Cons, Cproc, Env, Fun, Key, Nil, Num, Rec, Str, Sym, Thunk, U64}, + tag::ExprTag::{ + Char, Comm, Cons, Cproc, Env, Fun, Key, Nil, Num, Prov, Rec, Str, Sym, Thunk, U64, + }, }; use super::pointers::{Ptr, RawPtr, ZPtr}; @@ -413,23 +415,31 @@ impl Store { } #[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) + pub fn intern_provenance(&self, query: Ptr, val: Ptr, deps: Ptr) -> Ptr { + assert_eq!(*query.tag(), Tag::Expr(Cons)); + // TODO: Deps must be a single Prov or a list (later, an N-ary tuple), but we discard the type tag. This is + // arguably okay, but it means that in order to recover the preimage we will need to know the expected arity + // based on the query. + assert!(matches!(*deps.tag(), Tag::Expr(Prov | Cons | Nil))); + let raw = self.intern_raw_ptrs::<4>([ + *query.raw(), + self.tag(*val.tag()), + *val.raw(), + *deps.raw(), + ]); + Ptr::new(Tag::Expr(Prov), raw) } #[inline] pub fn pop_provenance(&self, env: Ptr) -> Option<[Ptr; 3]> { - assert_eq!(*env.tag(), Tag::Expr(Env)); + assert_eq!(*env.tag(), Tag::Expr(Prov)); 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); + + let env = Ptr::new(Tag::Expr(Cons), *env_pay); Some([query, val, env]) } @@ -577,6 +587,7 @@ impl Store { assert_eq!(*car_tag, self.tag(Tag::Expr(Str))); assert_eq!(*cdr_tag, self.tag(Tag::Expr(Sym))); let string = self.fetch_string(&Ptr::new(Tag::Expr(Str), *car))?; + path.push(string); match cdr { RawPtr::Atom(idx) => { @@ -847,6 +858,30 @@ impl Store { Some(list) } + /// Fetches a provenance + pub fn fetch_provenance(&self, ptr: &Ptr) -> Option<(Ptr, Ptr, Ptr)> { + if *ptr.tag() != Tag::Expr(Prov) { + return None; + } + + let idx = ptr.raw().get_hash4()?; + if let Some([query_pay, val_tag, val_pay, deps_pay]) = self.fetch_raw_ptrs(idx) { + let query = Ptr::new(Tag::Expr(Cons), *query_pay); + let val = self.raw_to_ptr(val_tag, val_pay)?; + + let nil = self.intern_nil(); + let deps = if deps_pay == nil.raw() { + nil + } else { + Ptr::new(Tag::Expr(Prov), *deps_pay) + }; + + Some((query, val, deps)) + } else { + None + } + } + pub fn intern_syntax(&self, syn: Syntax) -> Ptr { match syn { Syntax::Num(_, x) => self.num(x.into_scalar()), @@ -1266,6 +1301,27 @@ impl Ptr { "".into() } } + Prov => { + if let Some((query, val, deps)) = store.fetch_provenance(self) { + let nil = store.intern_nil(); + if store.ptr_eq(&deps, &nil) { + format!( + "", + query.fmt_to_string(store, state), + val.fmt_to_string(store, state), + ) + } else { + format!( + "", + query.fmt_to_string(store, state), + val.fmt_to_string(store, state), + deps.fmt_to_string(store, state) + ) + } + } else { + "".into() + } + } }, Tag::Cont(t) => match t { Outermost => "Outermost".into(), diff --git a/src/tag.rs b/src/tag.rs index 88154a7bcd..d65d10e7a1 100644 --- a/src/tag.rs +++ b/src/tag.rs @@ -52,6 +52,7 @@ pub enum ExprTag { Key, Cproc, Env, + Prov, Rec, } @@ -83,6 +84,7 @@ impl fmt::Display for ExprTag { ExprTag::U64 => write!(f, "u64#"), ExprTag::Cproc => write!(f, "cproc#"), ExprTag::Env => write!(f, "env#"), + ExprTag::Prov => write!(f, "prov#"), ExprTag::Rec => write!(f, "rec#"), } }