Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Stable coprocessor order #665

Closed
wants to merge 1 commit into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ dashmap = "5.5.0"
ff = { workspace = true }
generic-array = "0.14.7"
hex = { version = "0.4.3", features = ["serde"] }
indexmap = { version = "1.9.3", features = ["rayon"] }
indexmap = { version = "1.9.3", features = ["rayon", "serde"] }
itertools = "0.9"
lurk-macros = { path = "lurk-macros" }
lurk-metrics = { path = "lurk-metrics" }
Expand Down
38 changes: 33 additions & 5 deletions src/eval/lang.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use std::collections::HashMap;
use std::fmt::Debug;
use std::marker::PhantomData;

use indexmap::IndexMap;
use lurk_macros::Coproc;
use serde::{Deserialize, Serialize};

Expand All @@ -10,6 +10,7 @@ use crate::field::LurkField;
use crate::ptr::Ptr;
use crate::store::Store;
use crate::symbol::Symbol;
use crate::tag::ExprTag;
use crate::z_ptr::ZExprPtr;

use crate::{self as lurk, lurk_sym_ptr};
Expand Down Expand Up @@ -76,10 +77,10 @@ pub enum Coproc<F: LurkField> {
/// exact set of coprocessors to be allowed in the `Lang` struct.
///
// TODO: Define a trait for the Hash and parameterize on that also.
#[derive(Debug, Default, Clone, Deserialize, Serialize)]
#[derive(Debug, Default, Clone, Serialize, Deserialize)]
pub struct Lang<F: LurkField, C: Coprocessor<F>> {
// A HashMap that stores coprocessors with their associated `Sym` keys.
coprocessors: HashMap<Symbol, (C, ZExprPtr<F>)>,
/// An IndexMap that stores coprocessors with their associated `Sym` keys
coprocessors: IndexMap<Symbol, (C, ZExprPtr<F>)>,
}

impl<F: LurkField, C: Coprocessor<F>> Lang<F, C> {
Expand Down Expand Up @@ -127,6 +128,13 @@ impl<F: LurkField, C: Coprocessor<F>> Lang<F, C> {
self.coprocessors.insert(name, (cproc.into(), z_ptr));
}

pub fn add_coprocessor_lem<T: Into<C>, S: Into<Symbol>>(&mut self, name: S, cproc: T) {
let name = name.into();
// TODO: eliminate this unecessary piece of data
let z_ptr = lurk::z_ptr::ZPtr(ExprTag::Nil, F::ZERO);
self.coprocessors.insert(name, (cproc.into(), z_ptr));
Comment on lines +133 to +134
Copy link
Collaborator

Choose a reason for hiding this comment

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

It's a little worse than this comment suggests. As far as I can see, this is adding the wrong data. Now, maybe in the LEM case, this wrong data is unnecessary. But a Lang is not specific to LEM or not-LEM. And consequently, it cannot be correct to construct one this way. This 'scalar ptr' must correspond to the symbol to which the coprocessor is bound. If LEM requires its own variant of Lang, then that would need to be formalized somehow.

This is not just academic. A Lang created as above could lead a non-LEM circuit to producing incorrect proofs. Such a Lang would be toxic and require very special handling. It shouldn't be possible to create such dangerous substances with the Lurk API.

Copy link
Member Author

@arthurpaulino arthurpaulino Sep 13, 2023

Choose a reason for hiding this comment

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

The LEM pipeline indeed doesn't need the cached ZPtr for this.

Would it be okay to have an add_coprocessor_with_zptr and allow the caller to provide the ZPtr? Then LEM would be able to feed it with whatever.

}

pub fn add_binding<B: Into<Binding<F, C>>>(&mut self, binding: B, store: &mut Store<F>) {
let Binding { name, coproc, _p } = binding.into();
let ptr = store.intern_symbol(&name);
Expand All @@ -135,7 +143,15 @@ impl<F: LurkField, C: Coprocessor<F>> Lang<F, C> {
self.coprocessors.insert(name, (coproc, z_ptr));
}

pub fn coprocessors(&self) -> &HashMap<Symbol, (C, ZExprPtr<F>)> {
pub fn add_binding_lem<B: Into<Binding<F, C>>>(&mut self, binding: B) {
let Binding { name, coproc, _p } = binding.into();
// TODO: eliminate this unecessary piece of data
let z_ptr = lurk::z_ptr::ZPtr(ExprTag::Nil, F::ZERO);
self.coprocessors.insert(name, (coproc, z_ptr));
}

#[inline]
pub fn coprocessors(&self) -> &IndexMap<Symbol, (C, ZExprPtr<F>)> {
&self.coprocessors
}

Expand All @@ -153,10 +169,22 @@ impl<F: LurkField, C: Coprocessor<F>> Lang<F, C> {
maybe_sym.and_then(|sym| self.coprocessors.get(&sym))
}

#[inline]
pub fn lookup_by_sym(&self, sym: &Symbol) -> Option<&C> {
self.coprocessors.get(sym).map(|(c, _)| c)
}

#[inline]
pub fn get_coprocessor_index(&self, sym: &Symbol) -> Option<usize> {
self.coprocessors.get_index_of(sym)
}

#[inline]
pub fn has_coprocessors(&self) -> bool {
!self.coprocessors.is_empty()
}

#[inline]
pub fn is_default(&self) -> bool {
!self.has_coprocessors()
}
Expand Down
Loading