Add Prov tag.

src/coprocessor/gadgets.rs

@@ -182,8 +182,7 @@ pub(crate) fn construct_provenance<F: LurkField, CS: ConstraintSystem<F>>(
     result: &AllocatedPtr<F>,
     deps: &AllocatedNum<F>,
 ) -> Result<AllocatedPtr<F>, 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<F: LurkField, CS: ConstraintSystem<F>>(
     provenance: &AllocatedNum<F>,
 ) -> Result<(AllocatedNum<F>, AllocatedPtr<F>, AllocatedNum<F>), 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);

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"]);

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<F: LurkField, Q: Query<F>> Scope<Q, LogMemo<F>, F> {
                 .collect::<Vec<_>>();
 
             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) {

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<F: LurkField> Store<F> {
     }
 
     #[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<F: LurkField> Store<F> {
             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<F: LurkField> Store<F> {
         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<F>) -> Ptr {
         match syn {
             Syntax::Num(_, x) => self.num(x.into_scalar()),
@@ -1266,6 +1301,27 @@ impl Ptr {
                         "<Opaque Env>".into()
                     }
                 }
+                Prov => {
+                    if let Some((query, val, deps)) = store.fetch_provenance(self) {
+                        let nil = store.intern_nil();
+                        if store.ptr_eq(&deps, &nil) {
+                            format!(
+                                "<Prov ({} . {})>",
+                                query.fmt_to_string(store, state),
+                                val.fmt_to_string(store, state),
+                            )
+                        } else {
+                            format!(
+                                "<Prov ({} . {}) . {}>",
+                                query.fmt_to_string(store, state),
+                                val.fmt_to_string(store, state),
+                                deps.fmt_to_string(store, state)
+                            )
+                        }
+                    } else {
+                        "<Opaque Prov>".into()
+                    }
+                }
             },
             Tag::Cont(t) => match t {
                 Outermost => "Outermost".into(),

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#"),
         }
     }