From 94453ada9f03625aaf9c79cd24c68b53c72b316c Mon Sep 17 00:00:00 2001 From: porcuquine Date: Tue, 8 Aug 2023 16:31:03 -0700 Subject: [PATCH] Move Foil to its own crate. --- Cargo.lock | 120 ++-- Cargo.toml | 2 +- foil/Cargo.toml | 26 + {src/foil => foil/src}/circuit.rs | 4 +- foil/src/coil.rs | 780 +++++++++++++++++++++++++ {src/foil => foil/src}/congruence.rs | 0 {src/foil => foil/src}/constructors.rs | 9 +- src/foil/mod.rs => foil/src/lib.rs | 21 +- src/circuit/gadgets/constraints.rs | 2 +- src/foil/coil.rs | 6 +- src/lib.rs | 1 - 11 files changed, 897 insertions(+), 74 deletions(-) create mode 100644 foil/Cargo.toml rename {src/foil => foil/src}/circuit.rs (98%) create mode 100644 foil/src/coil.rs rename {src/foil => foil/src}/congruence.rs (100%) rename {src/foil => foil/src}/constructors.rs (98%) rename src/foil/mod.rs => foil/src/lib.rs (98%) diff --git a/Cargo.lock b/Cargo.lock index 6166eb8186..058da02d32 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -168,7 +168,7 @@ checksum = "cc6dde6e4ed435a4c1ee4e73592f5ba9da2151af10076cc04858746af9352d09" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -451,9 +451,12 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" [[package]] name = "cc" -version = "1.0.79" +version = "1.0.82" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f" +checksum = "305fe645edc1442a0fa8b6726ba61d422798d37a52e12eaecf4b022ebbb88f01" +dependencies = [ + "libc", +] [[package]] name = "cfg-if" @@ -490,12 +493,13 @@ dependencies = [ [[package]] name = "cl3" -version = "0.9.1" +version = "0.9.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e014961508a981c7ef28a65d0c965af7061593b4db50cff83952c62931b39ec" +checksum = "215a3aa32ab5d7928c539c4289d1cf144257c3cb05e05a4b7e61d5a6bb6583a5" dependencies = [ "libc", "opencl-sys", + "thiserror", ] [[package]] @@ -528,9 +532,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.3.19" +version = "4.3.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5fd304a20bff958a57f04c4e96a2e7594cc4490a0e809cbd48bb6437edaa452d" +checksum = "c27cdf28c0f604ba3f512b0c9a409f8de8513e4816705deb0498b627e7c3a3fd" dependencies = [ "clap_builder", "clap_derive 4.3.12", @@ -549,9 +553,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.19" +version = "4.3.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "01c6a3f08f1fe5662a35cfe393aec09c4df95f60ee93b7556505260f75eee9e1" +checksum = "08a9f1ab5e9f01a9b81f202e8562eb9a10de70abf9eaeac1be465c28b75aa4aa" dependencies = [ "anstream", "anstyle", @@ -581,7 +585,7 @@ dependencies = [ "heck 0.4.1", "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -617,7 +621,7 @@ dependencies = [ "anyhow", "assert_cmd", "blstrs", - "clap 4.3.19", + "clap 4.3.21", "fcomm", "ff", "lurk", @@ -937,9 +941,9 @@ dependencies = [ [[package]] name = "errno" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" +checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f" dependencies = [ "errno-dragonfly", "libc", @@ -994,7 +998,7 @@ checksum = "55a9a55d1dab3b07854648d48e366f684aefe2ac78ae28cec3bf65e3cd53d9a3" dependencies = [ "execute-command-tokens", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -1141,6 +1145,26 @@ version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" +[[package]] +name = "foil" +version = "0.1.0" +dependencies = [ + "anyhow", + "bellperson", + "env_logger 0.7.1", + "ff", + "generic-array 0.14.7", + "indexmap", + "log", + "lurk", + "lurk-macros", + "neptune", + "once_cell", + "pasta_curves", + "pretty_env_logger", + "test-log", +] + [[package]] name = "funty" version = "2.0.0" @@ -1455,9 +1479,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f" [[package]] name = "linux-raw-sys" -version = "0.4.3" +version = "0.4.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" +checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503" [[package]] name = "lock_api" @@ -1490,7 +1514,7 @@ dependencies = [ "bincode", "blstrs", "cfg-if", - "clap 4.3.19", + "clap 4.3.21", "config", "criterion", "dashmap", @@ -1895,9 +1919,9 @@ checksum = "9163e1259760e83d528d1b3171e5100c1767f10c52e1c4d6afad26e63d47d758" [[package]] name = "pest" -version = "2.7.1" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d2d1d55045829d65aad9d389139882ad623b33b904e7c9f1b10c5b8927298e5" +checksum = "1acb4a4365a13f749a93f1a094a7805e5cfa0955373a9de860d962eaa3a5fe5a" dependencies = [ "thiserror", "ucd-trie", @@ -1905,9 +1929,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.7.1" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f94bca7e7a599d89dea5dfa309e217e7906c3c007fb9c3299c40b10d6a315d3" +checksum = "666d00490d4ac815001da55838c500eafb0320019bbaa44444137c48b443a853" dependencies = [ "pest", "pest_generator", @@ -1915,22 +1939,22 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.7.1" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99d490fe7e8556575ff6911e45567ab95e71617f43781e5c05490dc8d75c965c" +checksum = "68ca01446f50dbda87c1786af8770d535423fa8a53aec03b8f4e3d7eb10e0929" dependencies = [ "pest", "pest_meta", "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] name = "pest_meta" -version = "2.7.1" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2674c66ebb4b4d9036012091b537aae5878970d6999f81a265034d85b136b341" +checksum = "56af0a30af74d0445c0bf6d9d051c979b516a1a5af790d251daee76005420a48" dependencies = [ "once_cell", "pest", @@ -2229,9 +2253,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.9.1" +version = "1.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" +checksum = "81bc1d4caf89fac26a70747fe603c130093b53c773888797a6329091246d651a" dependencies = [ "aho-corasick", "memchr", @@ -2241,9 +2265,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.3" +version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" +checksum = "fed1ceff11a1dddaee50c9dc8e4938bd106e9d89ae372f192311e7da498e3b69" dependencies = [ "aho-corasick", "memchr", @@ -2334,9 +2358,9 @@ checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" [[package]] name = "rustix" -version = "0.38.4" +version = "0.38.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" +checksum = "172891ebdceb05aa0005f533a6cbfca599ddd7d966f6f5d4d9b2e70478e70399" dependencies = [ "bitflags 2.3.3", "errno", @@ -2429,9 +2453,9 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.176" +version = "1.0.183" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "76dc28c9523c5d70816e393136b86d48909cfb27cecaa902d338c19ed47164dc" +checksum = "32ac8da02677876d532745a130fc9d8e6edfa81a269b107c5b00829b91d8eb3c" dependencies = [ "serde_derive", ] @@ -2456,13 +2480,13 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.176" +version = "1.0.183" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a4e7b8c5dc823e3b90651ff1d3808419cd14e5ad76de04feaf37da114e7a306f" +checksum = "aafe972d60b0b9bee71a91b92fee2d4fb3c9d7e8f6b179aa99f27203d99a4816" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -2478,13 +2502,13 @@ dependencies = [ [[package]] name = "serde_repr" -version = "0.1.15" +version = "0.1.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e168eaaf71e8f9bd6037feb05190485708e019f4fd87d161b3c0a0d37daf85e5" +checksum = "8725e1dfadb3a50f7e5ce0b1a540466f6ed3fe7a0fca2ac2b8b831d31316bd00" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -2654,9 +2678,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.27" +version = "2.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0" +checksum = "04361975b3f5e348b2189d8dc55bc942f278b2d482a6a0365de5bdd62d351567" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", @@ -2680,9 +2704,9 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.7.0" +version = "3.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5486094ee78b2e5038a6382ed7645bc084dc2ec433426ca4c3cb61e2007b8998" +checksum = "dc02fddf48964c42031a0b3fe0428320ecf3a73c401040fc0096f97794310651" dependencies = [ "cfg-if", "fastrand", @@ -2749,7 +2773,7 @@ checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -2897,7 +2921,7 @@ dependencies = [ "once_cell", "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", "wasm-bindgen-shared", ] @@ -2919,7 +2943,7 @@ checksum = "54681b18a46765f095758388f2d0cf16eb8d4169b639ab575a8f5693af210c7b" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -3159,5 +3183,5 @@ checksum = "ce36e65b0d2999d2aafac989fb249189a141aee1f53c612c1f37d72631959f69" dependencies = [ "proc-macro2 1.0.66", "quote 1.0.32", - "syn 2.0.27", + "syn 2.0.28", ] diff --git a/Cargo.toml b/Cargo.toml index aafe60de21..505195b2d8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -91,7 +91,7 @@ test-log = "0.2.12" [workspace] resolver = "2" members = ["clutch", - "fcomm", "lurk-macros" + "fcomm", "lurk-macros", "foil" ] # Dependencies that should be kept in sync through the whole workspace diff --git a/foil/Cargo.toml b/foil/Cargo.toml new file mode 100644 index 0000000000..a942254824 --- /dev/null +++ b/foil/Cargo.toml @@ -0,0 +1,26 @@ +[package] +name = "foil" +version = "0.1.0" +edition = "2021" +authors = ["porcuquine "] +description = "Flat Optimization Intermediate Language" +repository = "https://github.com/lurk-lab/lurk-rs" +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +anyhow = { workspace = true } +bellperson = { workspace = true } +ff = { workspace = true } +indexmap = { version = "1.9.3", features = ["rayon"] } +generic-array = "0.14.7" +lurk = { path = "../" } +lurk-macros = { path = "../lurk-macros" } +log = { workspace = true } +neptune = { workspace = true, features = ["arity2","arity4","arity8","arity16","pasta","bls"] } +once_cell = { workspace = true } +pasta_curves = { workspace = true, features = ["repr-c", "serde"] } +pretty_env_logger = "0.4" + +[dev-dependencies] +env_logger = "*" +test-log = "0.2.12" diff --git a/src/foil/circuit.rs b/foil/src/circuit.rs similarity index 98% rename from src/foil/circuit.rs rename to foil/src/circuit.rs index 5b118cb877..abc535ad4d 100644 --- a/src/foil/circuit.rs +++ b/foil/src/circuit.rs @@ -5,8 +5,8 @@ use std::fmt::Debug; use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError}; -use crate::field::LurkField; -use crate::foil::{Id, MappedFoil, MetaData, MetaMapper}; +use crate::{Id, MappedFoil, MetaData, MetaMapper}; +use lurk::field::LurkField; pub trait Relation: Debug { fn synthesize>( diff --git a/foil/src/coil.rs b/foil/src/coil.rs new file mode 100644 index 0000000000..d5f3dffb1d --- /dev/null +++ b/foil/src/coil.rs @@ -0,0 +1,780 @@ +use log::info; +use std::collections::{HashMap, HashSet}; +use std::marker::PhantomData; + +use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; + +use anyhow::{anyhow, bail, Result}; + +use crate::{Foil, Func, Id, Label, MetaData, MetaMapper, Relation, Schema, Var, Vert}; +use lurk::field::LurkField; +use lurk::ptr::Ptr; +use lurk::store::Store; +use lurk::sym; +use lurk::symbol::Symbol; +use lurk::tag::ExprTag; +use lurk::writer::Write; + +impl From for Func { + fn from(sym: Symbol) -> Self { + Self::from(&sym) + } +} + +impl From<&Symbol> for Func { + fn from(sym: &Symbol) -> Self { + Self::new_with_metadata(sym.to_string(), CoilMeta::from(sym.clone())) + } +} + +impl From for Var { + fn from(sym: Symbol) -> Self { + Self::from(&sym) + } +} + +impl From<&Symbol> for Var { + fn from(sym: &Symbol) -> Self { + Self::new(sym.to_string()) + } +} + +impl From for Label { + fn from(sym: Symbol) -> Self { + Self::from(&sym) + } +} + +impl From<&Symbol> for Label { + fn from(sym: &Symbol) -> Self { + Self::from(Var::from(sym)) + } +} + +#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] +pub struct CoilMeta { + name: Symbol, +} + +impl From for CoilMeta { + fn from(name: Symbol) -> Self { + Self { name } + } +} + +impl Default for CoilMeta { + fn default() -> Self { + let name = sym!("coil", "var"); + + Self { name } + } +} + +impl MetaData for CoilMeta {} + +#[derive(Clone, Debug, PartialEq)] +pub struct Context { + env: Ptr, +} + +/// Look up `var` in `env`, where `env` is a list of bindings from `Symbol` to `U64` representing bindings of variables to vertices +/// by id. +fn lookup_vertex_id( + store: &Store, + env: &Ptr, + var: &Ptr, +) -> Result> { + if let Some((binding, rest_env)) = store + .maybe_car_cdr(env) + .map_err(|_| anyhow!("env not a list"))? + { + if let Some((bound_var, id)) = store + .maybe_car_cdr(&binding) + .map_err(|_| anyhow!("binding not a pair"))? + { + if *var == bound_var { + match store.fetch_num(&id) { + Some(lurk::Num::U64(n)) => { + info!("found {n}"); + Ok(((*n) as Id).into()) + } + _ => { + bail!("binding Id could not be fetched"); + } + } + } else { + lookup_vertex_id(store, &rest_env, var) + } + } else { + info!("unbound"); + Ok(None) + } + } else { + info!("unbound"); + Ok(None) + } +} + +impl Context { + fn new(store: &mut Store) -> Self { + Self { + env: lurk::eval::empty_sym_env(store), + } + } + + fn lookup(&self, store: &Store, var: &Ptr) -> Result> { + info!( + "looking up {} in env: {}", + var.fmt_to_string(store), + self.env.fmt_to_string(store) + ); + lookup_vertex_id(store, &self.env, var) + } + + fn push_binding(&mut self, store: &mut Store, var: Ptr, id: Id) { + let num = store.intern_num(id as u64); + let binding = store.cons(var, num); + self.env = store.cons(binding, self.env); + } + + fn pop_binding(&mut self, store: &Store) -> Result { + let (car, cdr) = store + .car_cdr(&self.env) + .map_err(|_| anyhow!("failed to destructure env"))?; + self.env = cdr; + let (_var, id) = store + .car_cdr(&car) + .map_err(|_| anyhow!("failed to destrcture binding"))?; + + Ok(match store.fetch_num(&id) { + Some(lurk::Num::U64(n)) => (*n) as Id, + _ => { + bail!("binding Id could not be fetched"); + } + }) + } +} + +pub trait Syntax { + fn expand( + &self, + foil: &mut Foil, + store: &mut Store, + head: &Ptr, + rest: &[Ptr], + ) -> Result>> + where + Self: Sized; +} + +#[derive(Clone, Debug)] +pub struct CoilDef, S: Syntax> { + relations: HashMap, + syntax: HashMap, + constructors: HashMap>, + equivalences: HashSet, + _p: PhantomData, +} + +pub struct AsSyntax<'a, T>(&'a T); + +pub struct Let {} + +impl Syntax for Let { + fn expand( + &self, + _foil: &mut Foil, + store: &mut Store, + _head: &Ptr, + rest: &[Ptr], + ) -> Result>> { + let bind = store.intern_symbol(sym!("coil", "bind")); + let pop_binding = store.intern_symbol(sym!("coil", "pop-binding")); + + if rest.is_empty() { + bail!("Let bindings missing"); + } + + let bindings = store.fetch_list(&rest[0]).unwrap(); + + let mut result = Vec::with_capacity((2 * bindings.len()) + rest.len() - 1); + + result.extend(bindings.iter().map(|binding| { + let b = store.fetch_list(binding).unwrap(); + assert_eq!(2, b.len()); + // let var = b[0]; + // let val_form = b[1]; + + // This is also store.cons(bind, binding). + store.cons(bind, *binding) + //store.list(&[bind, var, val_form]) + })); + + result.extend(&rest[1..]); + + let pop_binding_form = store.list(&[pop_binding]); + result.extend(bindings.iter().map(|_| pop_binding_form)); + + Ok(result) + } +} + +#[derive(Default, Debug)] +struct BindRel {} + +#[derive(Default, Debug)] +struct VarRel {} + +impl Relation for BindRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // TODO: Actually implement constraints enforcing equality of the successors. Ideally, there would also exist a + // mechanism such that this could be implemented without allocating the head -- since the head is not required + // for this. Similarly, we should eventually allow for 'head' values to sometimes be unallocated + // linear-combinations. That is an optimization that can come later, when we focus on improving the generated + // R1CS based on the computation finally assembled. + Ok(()) + } +} +impl Relation for VarRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + assert!(successors.is_empty()); + Ok(()) + } +} + +pub enum CoilSyntax { + Let(Let), +} + +impl Syntax for CoilSyntax { + fn expand( + &self, + foil: &mut Foil, + store: &mut Store, + head: &Ptr, + rest: &[Ptr], + ) -> Result>> { + match self { + Self::Let(x) => x.expand(foil, store, head, rest), + } + } +} + +impl, S: Syntax> Default for CoilDef { + fn default() -> Self { + Self { + relations: Default::default(), + syntax: Default::default(), + constructors: Default::default(), + equivalences: Default::default(), + _p: Default::default(), + } + } +} + +impl> CoilDef { + fn new_std() -> Self { + let mut def = Self::default(); + + let let_sym = sym!("lurk", "let"); + let bind = sym!("coil", "bind"); + let _var = sym!("coil", "var"); + + def.register_equivalence(bind); + def.register_syntax(let_sym, CoilSyntax::Let(Let {})); + + def + } +} + +impl, S: Syntax> CoilDef { + fn register_relation(&mut self, sym: Symbol, rel: R) { + self.relations.insert(sym, rel); + } + fn register_syntax(&mut self, sym: Symbol, syn: S) { + self.syntax.insert(sym, syn); + } + fn register_constructor(&mut self, constructor: Symbol, projectors: Vec) { + self.constructors.insert(constructor, projectors); + } + fn register_equivalence(&mut self, equivalence: Symbol) { + self.equivalences.insert(equivalence); + } + fn symbol_func(&self, sym: Symbol) -> Func { + if let Some(projectors) = self.constructors.get(&sym) { + Func::constructor( + sym.to_string(), + projectors.iter().map(Func::from).collect(), + CoilMeta::from(sym), + ) + } else { + Func::from(sym) + } + } + + fn schema(&self) -> Schema { + let mut equivalences: Vec> = self + .equivalences + .iter() + .map(|sym| self.symbol_func(sym.clone())) + .collect(); + + equivalences.sort(); + + let mut constructors: Vec> = self + .constructors + .keys() + .map(|sym| self.symbol_func(sym.clone())) + .collect(); + constructors.sort(); + + Schema { + constructors, + equivalences, + } + } +} + +impl, S: Syntax> MetaMapper for CoilDef { + fn find(&self, meta: &CoilMeta) -> Option<&R> { + self.relations.get(&meta.name) + } +} + +impl<'a, F: LurkField, R: Relation, S: Syntax> MetaMapper + for AsSyntax<'a, CoilDef> +{ + fn find(&self, meta: &CoilMeta) -> Option<&S> { + self.0.syntax.get(&meta.name) + } +} + +impl, S: Syntax> CoilDef { + fn add_to_foil( + &self, + foil: &mut Foil, + store: &mut Store, + context: &mut Context, + expr: &Ptr, + ) -> Result> { + match expr.tag { + ExprTag::Cons => { + info!("adding sexp: {}", expr.fmt_to_string(store)); + + let list = store.fetch_list(expr).expect("sexps must be proper lists"); + let head = list.get(0).ok_or(anyhow!("missing head"))?; + let sym = store.fetch_sym(head).ok_or(anyhow!("sym not in store"))?; + let rest = &list[1..]; + let meta = CoilMeta::from(sym.clone()); + + if let Some(syntax) = AsSyntax::>(self).find(&meta) { + let expanded = syntax.expand(foil, store, head, rest)?; + + let mut last = None; + for (i, x) in expanded.iter().enumerate() { + info!( + "expanded ({} of {}): {}", + i + 1, + expanded.len(), + x.fmt_to_string(store) + ); + + if let Some(vert) = self.add_to_foil(foil, store, context, x)? { + last = Some(vert); + } + } + info!("completed expansion"); + Ok(last) + } else { + if sym == sym!("coil", "pop-binding") { + return self.handle_pop_binding(store, context, rest); + } + + // TODO: don't actually create these literal symbols here. + let successor_verts = if sym == sym!("coil", "bind") { + let var = store + .fetch_sym(&rest[0]) + .ok_or(anyhow!("bind var not in store"))?; + let var_vert = foil.alloc_unique_var(var.to_string()); + + let val_vert = self + .add_to_foil(foil, store, context, &rest[1])? + .ok_or(anyhow!("bind val missing"))?; + + self.handle_bind(store, context, rest, &[var_vert])?; + // return Ok(Some(self.handle_bind(store, context, rest, &[val_vert])?)); + + vec![Some(var_vert), Some(val_vert)] + } else { + rest.iter() + .map(|succ| self.add_to_foil(foil, store, context, succ)) + .collect::>>()? + }; + + info!("adding to foil: {sym:}, {meta:?}"); + let func = self.symbol_func(sym); + + Ok(Some(foil.add_with_meta( + func, + successor_verts.into_iter().flatten().collect(), + meta, + ))) + } + } + ExprTag::Sym => { + info!("adding symbol"); + + if let Some(bound_id) = context + .lookup(store, expr) + .map_err(|_| anyhow!("lookup error"))? + { + Ok(Some(Vert::new(bound_id))) + } else { + let sym = store.fetch_sym(expr).expect("missing sym"); + + Ok(Some(foil.alloc(sym))) + } + } + x => { + dbg!(x); + todo!("intern constant") + } + } + } + + fn handle_bind( + &self, + store: &mut Store, + context: &mut Context, + args: &[Ptr], + successors: &[Vert], + ) -> Result { + if args.len() != 2 { + bail!("bind needs exactly two args") + }; + if successors.len() != 1 { + bail!("bind needs exactly two successors") + }; + + let var = args[0]; + let vert = successors[0]; + info!("binding {} to {}", var.fmt_to_string(store), vert.id()); + + context.push_binding(store, var, vert.id()); + + Ok(vert) + } + fn handle_pop_binding( + &self, + store: &mut Store, + context: &mut Context, + args: &[Ptr], + ) -> Result> { + if !args.is_empty() { + bail!("pop-binding needs exactly zero args") + }; + + context + .pop_binding(store) + .map_err(|_| anyhow!("failed to pop binding"))?; + + Ok(None) + } +} + +impl, S: Syntax> From> for Schema { + fn from(coil_def: CoilDef) -> Self { + coil_def.schema() + } +} +impl, S: Syntax> From<&CoilDef> for Schema { + fn from(coil_def: &CoilDef) -> Self { + coil_def.schema() + } +} + +#[cfg(test)] +mod test { + use super::*; + use crate::congruence::test::assert_expected_classes; + use crate::{FoilConfig, MappedFoil}; + use bellperson::{ + gadgets::num::AllocatedNum, util_cs::test_cs::TestConstraintSystem, Circuit, + ConstraintSystem, SynthesisError, + }; + use generic_array::typenum::U2; + use lurk::circuit::gadgets::constraints::enforce_equal; + use lurk_macros::{let_store, lurk, store}; + use neptune::circuit2::poseidon_hash_allocated as poseidon_hash; + use neptune::poseidon::PoseidonConstants; + use once_cell::sync::Lazy; + use pasta_curves::pallas::Scalar as Fr; + + #[derive(Default, Debug)] + struct ConsRel {} + + #[derive(Default, Debug)] + struct CarRel {} + + #[derive(Default, Debug)] + struct CdrRel {} + + #[derive(Default, Debug)] + struct XxxRel {} + + #[derive(Debug)] + enum TestRel { + Bind(BindRel), + Var(VarRel), + Cons(ConsRel), + Car(CarRel), + Cdr(CdrRel), + Xxx(XxxRel), + } + + const P: Lazy> = Lazy::new(|| PoseidonConstants::new()); + + impl Relation for TestRel { + fn synthesize>( + &self, + cs: &mut CS, + allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + match self { + Self::Bind(x) => x.synthesize(cs, allocated_head, successors), + Self::Var(x) => x.synthesize(cs, allocated_head, successors), + Self::Cons(x) => x.synthesize(cs, allocated_head, successors), + Self::Car(x) => x.synthesize(cs, allocated_head, successors), + Self::Cdr(x) => x.synthesize(cs, allocated_head, successors), + Self::Xxx(x) => x.synthesize(cs, allocated_head, successors), + } + } + } + impl Relation for ConsRel { + fn synthesize>( + &self, + cs: &mut CS, + allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + let allocated_digest = + poseidon_hash(&mut cs.namespace(|| "poseidon hash"), successors, &*P)?; + enforce_equal(cs, || "digest equal", &allocated_head, &allocated_digest); + Ok(()) + } + } + impl Relation for CarRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // Nothing to do. The constraints are created by the corresponding ConsRel. + Ok(()) + } + } + impl Relation for CdrRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // Nothing to do. The constraints are created by the corresponding ConsRel. + Ok(()) + } + } + impl Relation for XxxRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // Nothing to do. The constraints are created by the corresponding ConsRel. + Ok(()) + } + } + + #[test_log::test] + fn test_coil_foil() { + let mut def = CoilDef::<_, _, CoilSyntax>::new_std(); + + //////////////////////////////////////////////////////////////////////////////// + // Set up the CoilDef and Schema + // + // TODO: derive all this from something simpler and declarative. + + // These shouldn't really be .lurk symbols, but until we have better package support, we need to use those. + let cons = sym!("lurk", "cons"); + let car = sym!("lurk", "car"); + let cdr = sym!("lurk", "cdr"); + + let bind = sym!("coil", "bind"); + let var = sym!("coil", "var"); + let xxx = sym!("xxx"); + + def.register_relation(var.clone(), TestRel::Var(VarRel {})); + def.register_relation(bind.clone(), TestRel::Bind(BindRel {})); + def.register_relation(cons.clone(), TestRel::Cons(ConsRel {})); + def.register_relation(car.clone(), TestRel::Car(CarRel {})); + def.register_relation(cdr.clone(), TestRel::Cdr(CdrRel {})); + def.register_relation(xxx.clone(), TestRel::Xxx(XxxRel {})); + + def.register_constructor(cons.clone(), vec![car, cdr]); + + let_store!(); // TODO: take field type parameter. This macro currently hard-codes Fr. + + let prog = lurk!((let ((x (cons q r))) + (let ((s (let ((x (cons a b))) + (car x) + (xxx qqq)))) + (car x)))) + .unwrap(); + + let mut foil = Foil::::new( + &def, + FoilConfig { + // This is necessary and should either be made the only option, or be required for Coil. + dedup_var_names: true, + }, + ); + + { + let f = &mut foil; + + let mut context = Context::new(store!()); + def.add_to_foil(f, store!(), &mut context, &prog).unwrap(); + + let classes = dbg!(f.graph.class_info(None)); + + let expected_classes = &[ + (0, vec!["Var(x)[0]: 0"], None), + (1, vec!["Var(q): 1"], None), + (2, vec!["Var(r): 2"], None), + (3, vec!["lurk.cons: 3"], Some(vec![1, 2])), + (4, vec!["coil.bind: 4"], Some(vec![0, 3])), + (5, vec!["Var(s)[1]: 5"], None), + (6, vec!["Var(x)[2]: 6"], None), + (7, vec!["Var(a): 7"], None), + (8, vec!["Var(b): 8"], None), + (9, vec!["lurk.cons: 9"], Some(vec![7, 8])), + (10, vec!["coil.bind: 10"], Some(vec![6, 9])), + (11, vec!["lurk.car: 11"], Some(vec![6])), + (12, vec!["Var(qqq): 12"], None), + (13, vec!["xxx: 13"], Some(vec![12])), + (14, vec!["coil.bind: 14"], Some(vec![5, 13])), + (15, vec!["lurk.car: 15"], Some(vec![0])), + ]; + assert_expected_classes(expected_classes, classes); + } + + { + foil.finalize(); + let classes = dbg!(foil.graph.class_info(None)); + let expected_classes = &[ + ( + 0, + vec!["Var(x)[0]: 0", "lurk.cons: 3", "lurk.cons: 19"], + Some(vec![20, 21]), + ), + (4, vec!["coil.bind: 4"], Some(vec![0, 0])), + (5, vec!["Var(s)[1]: 5", "xxx: 13"], Some(vec![12])), + ( + 6, + vec!["Var(x)[2]: 6", "lurk.cons: 9", "lurk.cons: 16"], + Some(vec![17, 18]), + ), + (10, vec!["coil.bind: 10"], Some(vec![6, 6])), + (12, vec!["Var(qqq): 12"], None), + (14, vec!["coil.bind: 14"], Some(vec![5, 5])), + ( + 17, + vec![ + "Var(a): 7", + "lurk.car: 11", + "Var(lurk.car)[3]: 17", + "lurk.car: 24", + "lurk.car: 26", + ], + Some(vec![6]), + ), + ( + 18, + vec![ + "Var(b): 8", + "Var(lurk.cdr)[4]: 18", + "lurk.cdr: 25", + "lurk.cdr: 27", + ], + Some(vec![6]), + ), + ( + 20, + vec![ + "Var(q): 1", + "lurk.car: 15", + "Var(lurk.car)[5]: 20", + "lurk.car: 22", + "lurk.car: 28", + ], + Some(vec![0]), + ), + ( + 21, + vec![ + "Var(r): 2", + "Var(lurk.cdr)[6]: 21", + "lurk.cdr: 23", + "lurk.cdr: 29", + ], + Some(vec![0]), + ), + ]; + assert_expected_classes(expected_classes, classes); + } + + info!("minimizing"); + + let minimized = foil.minimize(); + let classes = dbg!(minimized.graph.class_info(None)); + + let expected_classes = &[ + (0, vec!["lurk.cons: 0"], Some(vec![6, 7])), + (1, vec!["xxx: 1"], Some(vec![3])), + (2, vec!["lurk.cons: 2"], Some(vec![4, 5])), + (3, vec!["Var(qqq): 3"], None), + (4, vec!["lurk.car: 4"], Some(vec![2])), + (5, vec!["lurk.cdr: 5"], Some(vec![2])), + (6, vec!["lurk.car: 6"], Some(vec![0])), + (7, vec!["lurk.cdr: 7"], Some(vec![0])), + ]; + assert_expected_classes(expected_classes, classes); + + let fx = MappedFoil::new(minimized.clone(), def); + let cs = &mut TestConstraintSystem::::new(); + + fx.synthesize(cs).unwrap(); + + // Binary poseidon hash with standard strength is 237 constraints. + // This includes a constraint (and allocation) for the returned digest, + // and another to enforce equality with the `allocated_head` of the relation. + // One constraint and allocation could be optimized away by calling the unallocated + // poseidon-circuit function. However, that may add complexity to witness generation. + // + // 239 * 2 = 478, since there are two conses. + assert_eq!(478, cs.num_constraints()); + } +} diff --git a/src/foil/congruence.rs b/foil/src/congruence.rs similarity index 100% rename from src/foil/congruence.rs rename to foil/src/congruence.rs diff --git a/src/foil/constructors.rs b/foil/src/constructors.rs similarity index 98% rename from src/foil/constructors.rs rename to foil/src/constructors.rs index 7177047e8e..f54cc78d21 100644 --- a/src/foil/constructors.rs +++ b/foil/src/constructors.rs @@ -3,7 +3,7 @@ //! The enum-based implementation of `Fun` is not necessary, just a somewhat simple way to //! make a small, self-contained example. -use crate::foil::{Func, Label, Meta, Schema}; +use crate::{Func, Label, Meta, Schema}; #[derive(Clone, Copy, Eq, PartialEq, Hash)] enum Fun { @@ -54,8 +54,8 @@ impl From for Label { #[cfg(test)] mod test { use super::*; - use crate::foil::congruence::{test::assert_expected_classes, Graph}; - use crate::foil::{Foil, FoilConfig, Label, Meta, Var}; + use crate::congruence::{test::assert_expected_classes, Graph}; + use crate::{Foil, FoilConfig, Label, Meta, Var}; /* * In Lurk context, we can generalize the treatment of 'Quantifier-Free Theory of Equality' with 'Extensions to Theory of List Structure'. @@ -579,9 +579,6 @@ mod test { setup(f); setup(f2); - let initial_classes = dbg!(f.graph.class_info(None)); - let f2_initial_classes = dbg!(f2.graph.class_info(None)); - f.finalize(); f2.finalize(); diff --git a/src/foil/mod.rs b/foil/src/lib.rs similarity index 98% rename from src/foil/mod.rs rename to foil/src/lib.rs index 565188c236..cee8a0ee2d 100644 --- a/src/foil/mod.rs +++ b/foil/src/lib.rs @@ -366,19 +366,16 @@ impl Foil { } fn enqueue_merge<'a, U: Into<&'a Id>, V: Into<&'a Id>>(&mut self, u: Option, v: Option) { - match (u, v) { - (Some(u), Some(v)) => { - let u = u.into(); - let v = v.into(); - info!( - "will merge {} and {}", - self.graph.vertex(*u), - &self.graph.vertex(*v) - ); + if let (Some(u), Some(v)) = (u, v) { + let u = u.into(); + let v = v.into(); + info!( + "will merge {} and {}", + self.graph.vertex(*u), + &self.graph.vertex(*v) + ); - self.merge_queue.push_back((*u, *v)) - } - _ => (), + self.merge_queue.push_back((*u, *v)) } } fn merge_pending(&mut self) { diff --git a/src/circuit/gadgets/constraints.rs b/src/circuit/gadgets/constraints.rs index d2f13774ac..668a14a397 100644 --- a/src/circuit/gadgets/constraints.rs +++ b/src/circuit/gadgets/constraints.rs @@ -14,7 +14,7 @@ use ff::PrimeField; /// Adds a constraint to CS, enforcing an equality relationship between the allocated numbers a and b. /// /// a == b -pub(crate) fn enforce_equal>( +pub fn enforce_equal>( cs: &mut CS, annotation: A, a: &AllocatedNum, diff --git a/src/foil/coil.rs b/src/foil/coil.rs index 47c98e0977..fdb73fd332 100644 --- a/src/foil/coil.rs +++ b/src/foil/coil.rs @@ -7,13 +7,13 @@ use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; use anyhow::{anyhow, bail, Result}; use crate::field::LurkField; -use crate::foil::{Foil, Func, Id, Label, MetaData, MetaMapper, Relation, Schema, Var, Vert}; use crate::ptr::Ptr; use crate::store::Store; use crate::sym; use crate::symbol::Symbol; use crate::tag::ExprTag; use crate::writer::Write; +use crate::{Foil, Func, Id, Label, MetaData, MetaMapper, Relation, Schema, Var, Vert}; impl From for Func { fn from(sym: Symbol) -> Self { @@ -507,8 +507,8 @@ impl, S: Syntax> From<&CoilDef> for Sch mod test { use super::*; use crate::circuit::gadgets::constraints::enforce_equal; - use crate::foil::congruence::test::assert_expected_classes; - use crate::foil::{FoilConfig, MappedFoil}; + use crate::congruence::test::assert_expected_classes; + use crate::{FoilConfig, MappedFoil}; use bellperson::{ gadgets::num::AllocatedNum, util_cs::test_cs::TestConstraintSystem, Circuit, ConstraintSystem, SynthesisError, diff --git a/src/lib.rs b/src/lib.rs index 6cf52df0a4..fe4f206e89 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -12,7 +12,6 @@ pub mod coprocessor; pub mod eval; pub mod expr; pub mod field; -pub mod foil; pub mod hash; pub mod hash_witness; //pub mod package;