Skip to content

Commit

Permalink
Toplevel query (#1187)
Browse files Browse the repository at this point in the history 
* `ToplevelQuery` added

* Progress on `ToplevelQuery`

* Content added to Query and Scope

* WIP toplevel

* WIP eval

* More toplevel methods

* Progress on eval

* Finished eval

* Coroutine eval test

* Toplevel synthesize started

* Some progress on synthesize

* More progress on synthesize

* Synthesize `Ctrl`

* Prove refactor

* LEM coroutine prove

* Bugfixes, test assertions

* Coroutine size test

* synthesis file added

* More operations

* Synthesis done

* Use MatchValue

* `from_ptr` now takes content

Fixed toplevel's from_ptr

* Prove sum list test

* Rebase fixes

* Renaming
  • Loading branch information
@gabriel-barrett
gabriel-barrett authored Mar 8, 2024
1 parent a1cf4f3 commit c333fa4
Show file tree
Hide file tree
Showing 14 changed files with 1,931 additions and 171 deletions.
18 changes: 10 additions & 8 deletions src/coroutine/memoset/demo.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ pub(crate) enum DemoCircuitQuery<F: LurkField> {

impl<F: LurkField> Query<F> for DemoQuery<F> {
type CQ = DemoCircuitQuery<F>;
type RD = ();

fn eval(&self, scope: &mut Scope<Self, LogMemo<F>, F>) -> Ptr {
match self {
Expand Down Expand Up @@ -55,7 +56,7 @@ impl<F: LurkField> Query<F> for DemoQuery<F> {
}
}

fn from_ptr(s: &Store<F>, ptr: &Ptr) -> Option<Self> {
fn from_ptr(_: &Self::RD, s: &Store<F>, ptr: &Ptr) -> Option<Self> {
let (head, body) = s.car_cdr(ptr).expect("query should be cons");
let sym = s.fetch_sym(&head).expect("head should be sym");

Expand Down Expand Up @@ -87,21 +88,21 @@ impl<F: LurkField> Query<F> for DemoQuery<F> {
}
}

fn dummy_from_index(s: &Store<F>, index: usize) -> Self {
fn dummy_from_index(_: &Self::RD, s: &Store<F>, index: usize) -> Self {
match index {
0 => Self::Factorial(s.num(0.into())),
_ => unreachable!(),
}
}

fn index(&self) -> usize {
fn index(&self, _: &Self::RD) -> usize {
match self {
Self::Factorial(_) => 0,
_ => unreachable!(),
}
}

fn count() -> usize {
fn count(_: &Self::RD) -> usize {
1
}
}
Expand Down Expand Up @@ -131,6 +132,7 @@ impl<F: LurkField> RecursiveQuery<F> for DemoCircuitQuery<F> {
}

impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
type RD = ();
fn synthesize_args<CS: ConstraintSystem<F>>(
&self,
_cs: &mut CS,
Expand All @@ -147,7 +149,7 @@ impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
scope: &mut CircuitScope<F, LogMemoCircuit<F>>,
scope: &mut CircuitScope<F, LogMemoCircuit<F>, Self::RD>,
acc: &AllocatedPtr<F>,
allocated_key: &AllocatedPtr<F>,
) -> Result<((AllocatedPtr<F>, AllocatedPtr<F>), AllocatedPtr<F>), SynthesisError> {
Expand Down Expand Up @@ -198,11 +200,11 @@ impl<F: LurkField> CircuitQuery<F> for DemoCircuitQuery<F> {
}

fn from_ptr<CS: ConstraintSystem<F>>(cs: &mut CS, s: &Store<F>, ptr: &Ptr) -> Option<Self> {
DemoQuery::from_ptr(s, ptr).map(|q| q.to_circuit(cs, s))
DemoQuery::from_ptr(&(), s, ptr).map(|q| q.to_circuit(cs, s))
}

fn dummy_from_index<CS: ConstraintSystem<F>>(cs: &mut CS, s: &Store<F>, index: usize) -> Self {
DemoQuery::dummy_from_index(s, index).to_circuit(cs, s)
DemoQuery::dummy_from_index(&(), s, index).to_circuit(cs, s)
}

fn symbol(&self) -> Symbol {
Expand Down Expand Up @@ -230,7 +232,7 @@ mod test {
let four = s.num(F::from_u64(4));
let six = s.num(F::from_u64(6));
let twenty_four = s.num(F::from_u64(24));
let mut scope: Scope<DemoQuery<F>, LogMemo<F>, F> = Scope::new(1, s);
let mut scope: Scope<DemoQuery<F>, LogMemo<F>, F> = Scope::new(1, s, ());
assert_eq!(one, DemoQuery::Factorial(zero).eval(&mut scope));
assert_eq!(one, DemoQuery::Factorial(one).eval(&mut scope));
assert_eq!(two, DemoQuery::Factorial(two).eval(&mut scope));
Expand Down
20 changes: 11 additions & 9 deletions src/coroutine/memoset/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ pub(crate) enum EnvCircuitQuery<F: LurkField> {

impl<F: LurkField> Query<F> for EnvQuery<F> {
type CQ = EnvCircuitQuery<F>;
type RD = ();

fn eval(&self, scope: &mut Scope<Self, LogMemo<F>, F>) -> Ptr {
let s = scope.store.as_ref();
Expand Down Expand Up @@ -55,7 +56,7 @@ impl<F: LurkField> Query<F> for EnvQuery<F> {
}
}

fn from_ptr(s: &Store<F>, ptr: &Ptr) -> Option<Self> {
fn from_ptr(_: &Self::RD, s: &Store<F>, ptr: &Ptr) -> Option<Self> {
let (head, body) = s.car_cdr(ptr).expect("query should be cons");
let sym = s.fetch_sym(&head).expect("head should be sym");

Expand Down Expand Up @@ -94,21 +95,21 @@ impl<F: LurkField> Query<F> for EnvQuery<F> {
}
}

fn dummy_from_index(s: &Store<F>, index: usize) -> Self {
fn dummy_from_index(_: &Self::RD, s: &Store<F>, index: usize) -> Self {
match index {
0 => Self::Lookup(s.num(0.into()), s.num(0.into())),
_ => unreachable!(),
}
}

fn index(&self) -> usize {
fn index(&self, _: &Self::RD) -> usize {
match self {
Self::Lookup(_, _) => 0,
_ => unreachable!(),
}
}

fn count() -> usize {
fn count(_: &Self::RD) -> usize {
1
}
}
Expand All @@ -125,6 +126,7 @@ impl<F: LurkField> RecursiveQuery<F> for EnvCircuitQuery<F> {
}

impl<F: LurkField> CircuitQuery<F> for EnvCircuitQuery<F> {
type RD = ();
fn synthesize_args<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
Expand All @@ -148,7 +150,7 @@ impl<F: LurkField> CircuitQuery<F> for EnvCircuitQuery<F> {
cs: &mut CS,
g: &GlobalAllocator<F>,
store: &Store<F>,
scope: &mut CircuitScope<F, LogMemoCircuit<F>>,
scope: &mut CircuitScope<F, LogMemoCircuit<F>, Self::RD>,
acc: &AllocatedPtr<F>,
allocated_key: &AllocatedPtr<F>,
) -> Result<((AllocatedPtr<F>, AllocatedPtr<F>), AllocatedPtr<F>), SynthesisError> {
Expand Down Expand Up @@ -206,11 +208,11 @@ impl<F: LurkField> CircuitQuery<F> for EnvCircuitQuery<F> {
}

fn from_ptr<CS: ConstraintSystem<F>>(cs: &mut CS, s: &Store<F>, ptr: &Ptr) -> Option<Self> {
EnvQuery::from_ptr(s, ptr).map(|q| q.to_circuit(cs, s))
EnvQuery::from_ptr(&(), s, ptr).map(|q| q.to_circuit(cs, s))
}

fn dummy_from_index<CS: ConstraintSystem<F>>(cs: &mut CS, s: &Store<F>, index: usize) -> Self {
EnvQuery::dummy_from_index(s, index).to_circuit(cs, s)
EnvQuery::dummy_from_index(&(), s, index).to_circuit(cs, s)
}

fn symbol(&self) -> Symbol {
Expand Down Expand Up @@ -255,7 +257,7 @@ mod test {
let t = s.intern_t();
let nil = s.intern_nil();

let mut scope: Scope<EnvQuery<F>, LogMemo<F>, F> = Scope::new(1, s);
let mut scope: Scope<EnvQuery<F>, LogMemo<F>, F> = Scope::new(1, s, ());
let mut test = |var, env, found| {
let expected = if let Some(val) = found {
scope.store.cons(val, t)
Expand Down Expand Up @@ -358,7 +360,7 @@ mod test {
expected.assert_eq(&computed.to_string());
};

let mut scope: Scope<EnvQuery<F>, LogMemo<F>, F> = Scope::new(1, s.clone());
let mut scope: Scope<EnvQuery<F>, LogMemo<F>, F> = Scope::new(1, s.clone(), ());

let make_query = |sym, env| EnvQuery::Lookup(sym, env).to_ptr(s);

Expand Down
Loading

1 comment on commit c333fa4

@github-actions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Benchmarks

Table of Contents

Overview

This benchmark report shows the Fibonacci GPU benchmark.
NVIDIA L4
Intel(R) Xeon(R) CPU @ 2.20GHz
32 vCPUs
125 GB RAM
Workflow run: https://github.com/lurk-lab/lurk-rs/actions/runs/8196483110

Benchmark Results

LEM Fibonacci Prove - rc = 100

ref=a1cf4f3c8b79298edf9fb4df01df06ec398b8c2b ref=c333fa4f69b8f2f403c37f2a7491aed1b37b2c1c
num-100 1.46 s (✅ 1.00x) 1.45 s (✅ 1.00x faster)
num-200 2.77 s (✅ 1.00x) 2.76 s (✅ 1.00x faster)

LEM Fibonacci Prove - rc = 600

ref=a1cf4f3c8b79298edf9fb4df01df06ec398b8c2b ref=c333fa4f69b8f2f403c37f2a7491aed1b37b2c1c
num-100 1.82 s (✅ 1.00x) 1.85 s (✅ 1.01x slower)
num-200 3.01 s (✅ 1.00x) 3.06 s (✅ 1.02x slower)

Made with criterion-table

Please sign in to comment.