Skip to content

Commit

Permalink
Implement provenance.
Browse files Browse the repository at this point in the history
  • Loading branch information
porcuquine committed Feb 9, 2024
1 parent b694c16 commit 9f1a138
Show file tree
Hide file tree
Showing 7 changed files with 717 additions and 338 deletions.
7 changes: 7 additions & 0 deletions src/circuit/gadgets/macros.rs
Original file line number Diff line number Diff line change
@@ -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) => {
Expand Down
101 changes: 96 additions & 5 deletions src/coprocessor/gadgets.rs
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ pub(crate) fn construct_list<F: LurkField, CS: ConstraintSystem<F>>(
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
elts: &[&AllocatedPtr<F>],
elts: &[AllocatedPtr<F>],
last: Option<AllocatedPtr<F>>,
) -> Result<AllocatedPtr<F>, SynthesisError> {
let init = match last {
Expand Down Expand Up @@ -173,11 +173,36 @@ pub(crate) fn construct_env<F: LurkField, CS: ConstraintSystem<F>>(
Ok(AllocatedPtr::from_parts(tag, hash))
}

#[inline]
pub(crate) fn construct_provenance<F: LurkField, CS: ConstraintSystem<F>>(
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
query_hash: &AllocatedNum<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 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<F: LurkField, CS: ConstraintSystem<F>>(
cs: &mut CS,
s: &Store<F>,
Expand Down Expand Up @@ -226,6 +251,65 @@ pub(crate) fn deconstruct_env<F: LurkField, CS: ConstraintSystem<F>>(
Ok((key_sym_hash, val, new_env_hash))
}

#[allow(dead_code)]
pub(crate) fn deconstruct_provenance<F: LurkField, CS: ConstraintSystem<F>>(
cs: &mut CS,
s: &Store<F>,
not_dummy: &Boolean,
provenance: &AllocatedNum<F>,
) -> Result<(AllocatedNum<F>, AllocatedPtr<F>, AllocatedNum<F>), 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::<F>(),
*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)]
Expand Down Expand Up @@ -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));
}
Expand Down
40 changes: 23 additions & 17 deletions src/coroutine/memoset/demo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand All @@ -27,7 +28,7 @@ pub(crate) enum DemoCircuitQuery<F: LurkField> {
impl<F: LurkField> Query<F> for DemoQuery<F> {
type CQ = DemoCircuitQuery<F>;

fn eval(&self, s: &Store<F>, scope: &mut Scope<Self, LogMemo<F>>) -> Ptr {
fn eval(&self, s: &Store<F>, scope: &mut Scope<Self, LogMemo<F>, F>) -> Ptr {
match self {
Self::Factorial(n) => {
let n_zptr = s.hash_ptr(n);
Expand Down Expand Up @@ -117,15 +118,11 @@ impl<F: LurkField> RecursiveQuery<F> for DemoCircuitQuery<F> {
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)
}
}
}
Expand All @@ -140,20 +137,27 @@ impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
scope: &mut CircuitScope<F, LogMemoCircuit<F>>,
acc: &AllocatedPtr<F>,
transcript: &CircuitTranscript<F>,
) -> Result<(AllocatedPtr<F>, AllocatedPtr<F>, CircuitTranscript<F>), SynthesisError> {
) -> Result<
(
(AllocatedPtr<F>, AllocatedPtr<F>),
AllocatedPtr<F>,
CircuitTranscript<F>,
),
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)
Expand All @@ -168,17 +172,19 @@ impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
|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),
Expand Down Expand Up @@ -212,7 +218,7 @@ mod test {
#[test]
fn test_factorial() {
let s = Store::default();
let mut scope: Scope<DemoQuery<F>, LogMemo<F>> = Scope::default();
let mut scope: Scope<DemoQuery<F>, LogMemo<F>, F> = Scope::default();
let zero = s.num(F::ZERO);
let one = s.num(F::ONE);
let two = s.num(F::from_u64(2));
Expand Down
Loading

0 comments on commit 9f1a138

Please sign in to comment.