Skip to content

Commit

Permalink
Refactor Query (#1146)
Browse files Browse the repository at this point in the history 
* Refactor Query to be more granular.

* Use allocated_key when proving query.

* Fixed `allocated_key` (#1156)

---------

Co-authored-by: porcuquine <porcuquine@users.noreply.github.com>
Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
  • Loading branch information
@porcuquine @gabriel-barrett
3 people authored Feb 20, 2024
1 parent cf65088 commit 6f838e0
Show file tree
Hide file tree
Showing 4 changed files with 124 additions and 76 deletions.
21 changes: 15 additions & 6 deletions src/coroutine/memoset/demo.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -129,13 +128,25 @@ impl<F: LurkField> RecursiveQuery<F> for DemoCircuitQuery<F> {
}

impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
fn synthesize_args<CS: ConstraintSystem<F>>(
&self,
_cs: &mut CS,
_g: &GlobalAllocator<F>,
_store: &Store<F>,
) -> Result<AllocatedPtr<F>, SynthesisError> {
match self {
Self::Factorial(n) => Ok(n.clone()),
}
}

fn synthesize_eval<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
scope: &mut CircuitScope<F, LogMemoCircuit<F>>,
acc: &AllocatedPtr<F>,
allocated_key: &AllocatedPtr<F>,
) -> Result<((AllocatedPtr<F>, AllocatedPtr<F>), AllocatedPtr<F>), SynthesisError> {
match self {
Self::Factorial(n) => {
Expand Down Expand Up @@ -167,19 +178,17 @@ impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
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,
)
}
}
Expand Down
62 changes: 31 additions & 31 deletions src/coroutine/memoset/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,22 +117,39 @@ impl<F: LurkField> Query<F> for EnvQuery<F> {
impl<F: LurkField> RecursiveQuery<F> for EnvCircuitQuery<F> {}

impl<F: LurkField> CircuitQuery<F> for EnvCircuitQuery<F> {
fn synthesize_args<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
) -> Result<AllocatedPtr<F>, 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<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
scope: &mut CircuitScope<F, LogMemoCircuit<F>>,
acc: &AllocatedPtr<F>,
allocated_key: &AllocatedPtr<F>,
) -> Result<((AllocatedPtr<F>, AllocatedPtr<F>), AllocatedPtr<F>), SynthesisError> {
match self {
Self::Lookup(var, env) => {
let nil = store.intern_nil();
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)?;

Expand Down Expand Up @@ -164,34 +181,17 @@ impl<F: LurkField> CircuitQuery<F> for EnvCircuitQuery<F> {
&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,
)
}
}
Expand Down Expand Up @@ -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;
Expand All @@ -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"]);
Expand Down
58 changes: 30 additions & 28 deletions src/coroutine/memoset/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1149,7 +1149,16 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
s: &Store<F>,
) -> 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(())
}
Expand All @@ -1160,12 +1169,10 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
g: &mut GlobalAllocator<F>,
s: &Store<F>,
i: usize,
kv: &Ptr,
) -> Result<(), SynthesisError> {
let (key, value) = s.car_cdr(kv).unwrap();
allocated_key: &AllocatedPtr<F>,
value: Ptr,
) -> Result<AllocatedPtr<F>, 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();
Expand All @@ -1174,7 +1181,7 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
cs,
g,
s,
&allocated_key,
allocated_key,
&acc,
&insertion_transcript,
&Boolean::Constant(true),
Expand All @@ -1186,7 +1193,7 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {

self.acc = Some(new_acc);
self.transcript = new_transcript;
Ok(())
Ok(val)
}

fn synthesize_prove_key_query<CS: ConstraintSystem<F>, Q: Query<F>>(
Expand All @@ -1197,25 +1204,20 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
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,
Expand All @@ -1240,7 +1242,7 @@ impl<F: LurkField> CircuitScope<F, LogMemoCircuit<F>> {
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(
Expand Down Expand Up @@ -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,
)
}
Expand Down
Loading

0 comments on commit 6f838e0

Please sign in to comment.