From 45145aa32e6b3821eaf9b07e465bc635a015f6cf Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Wed, 6 Dec 2023 21:08:31 -0300 Subject: [PATCH 01/14] letrec works differently letrec will now add thunk expressions which adds themselves to the environment before evaluating --- src/lem/eval.rs | 60 +++++++++++++++++++----------------------------- src/lem/store.rs | 9 +------- src/tag.rs | 2 -- 3 files changed, 25 insertions(+), 46 deletions(-) diff --git a/src/lem/eval.rs b/src/lem/eval.rs index f172d56f63..fea8536f50 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -802,14 +802,13 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (nil) }); let is_cproc = is_cproc(cprocs); - let lookup = func!(lookup(expr, env, found, binding): 4 => { - let rec = Symbol("rec"); - let non_rec = Symbol("non_rec"); - let error = Symbol("error"); + let lookup = func!(lookup(expr, env, state, binding): 4 => { + let found = Symbol("found"); let not_found = Symbol("not_found"); - let continue = eq_val(not_found, found); + let error = Symbol("error"); + let continue = eq_val(not_found, state); if !continue { - return (expr, env, found, binding) + return (expr, env, state, binding) } match env.tag { Expr::Nil => { @@ -827,14 +826,7 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { Expr::Sym => { let eq_val = eq_val(var, expr); if eq_val { - return (val, env, non_rec, binding) - } - return (expr, smaller_env, not_found, binding) - } - Expr::RecVar => { - let eq_val = eq_val(var, expr); - if eq_val { - return (val, env, rec, binding) + return (val, env, found, binding) } return (expr, smaller_env, not_found, binding) } @@ -888,25 +880,20 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (expr, env, cont, apply) } let not_found = Symbol("not_found"); - let (expr, env, found, binding) = lookup(expr, env, not_found, nil); - let (expr, env, found, binding) = lookup(expr, env, found, binding); - let (expr, env, found, binding) = lookup(expr, env, found, binding); - match symbol found { + let (expr, env, state, binding) = lookup(expr, env, not_found, nil); + let (expr, env, state, binding) = lookup(expr, env, state, binding); + let (expr, env, state, binding) = lookup(expr, env, state, binding); + let (expr, env, state, binding) = lookup(expr, env, state, binding); + match symbol state { "error" => { return (expr, env, err, errctrl) } - "non_rec" => { - return (expr, env, cont, apply) - } - "rec" => { + "found" => { match expr.tag { - Expr::Fun => { - // if `val2` is a closure, then extend its environment - let (arg, body, closed_env, _foo) = decons4(expr); - let extended: Expr::Cons = cons2(binding, closed_env); - // and return the extended closure - let fun: Expr::Fun = cons4(arg, body, extended, foo); - return (fun, env, cont, apply) + Expr::Thunk => { + let (body, body_env) = decons2(expr); + let env: Expr::Cons = cons2(binding, body_env); + return (body, env, cont, ret) } }; return (expr, env, cont, apply) @@ -963,8 +950,11 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let cont: Cont::Let = cons4(var, env, expanded, cont); return (val, env, cont, ret) } + let thunk: Expr::Thunk = cons2(val, env); + let binding: Expr::Cons = cons2(var, thunk); + let rec_env: Expr::Cons = cons2(binding, env); let cont: Cont::LetRec = cons4(var, env, expanded, cont); - return (val, env, cont, ret) + return (val, rec_env, cont, ret) } }; return (expr, env, err, errctrl) @@ -1298,8 +1288,6 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { } Cont::LetRec => { let (var, saved_env, body, cont) = decons4(cont); - // Since the variable came from a letrec, it is a recursive variable - let var = cast(var, Expr::RecVar); let binding: Expr::Cons = cons2(var, result); let extended_env: Expr::Cons = cons2(binding, saved_env); return (body, extended_env, cont, ret) @@ -1734,9 +1722,9 @@ mod tests { assert_eq!( func.slots_count, SlotsCounter { - hash4: 14, + hash4: 17, hash6: 0, - hash8: 6, + hash8: 5, commitment: 1, bit_decomp: 3, } @@ -1745,8 +1733,8 @@ mod tests { expected.assert_eq(&computed.to_string()); }; expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["8884"]); - expect_eq(cs.num_constraints(), expect!["10831"]); + expect_eq(cs.aux().len(), expect!["9377"]); + expect_eq(cs.num_constraints(), expect!["11318"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } } diff --git a/src/lem/store.rs b/src/lem/store.rs index 29cf756ad6..1724bff268 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -23,7 +23,7 @@ use crate::{ self, Binop, Binop2, Call, Call0, Call2, Dummy, Emit, If, Let, LetRec, Lookup, Outermost, Tail, Terminal, Unop, }, - tag::ExprTag::{Char, Comm, Cons, Cproc, Fun, Key, Nil, Num, RecVar, Str, Sym, Thunk, U64}, + tag::ExprTag::{Char, Comm, Cons, Cproc, Fun, Key, Nil, Num, Str, Sym, Thunk, U64}, }; use super::pointers::{Ptr, RawPtr, ZPtr}; @@ -1004,13 +1004,6 @@ impl Ptr { "".into() } } - RecVar => { - if let Some(sym) = store.fetch_sym(&self.cast(Tag::Expr(Sym))) { - state.fmt_to_string(&sym.into()) - } else { - "".into() - } - } Key => { if let Some(key) = store.fetch_key(self) { state.fmt_to_string(&key.into()) diff --git a/src/tag.rs b/src/tag.rs index bf6a644c1a..af2bc41673 100644 --- a/src/tag.rs +++ b/src/tag.rs @@ -51,7 +51,6 @@ pub enum ExprTag { U64, Key, Cproc, - RecVar, } impl From for u16 { @@ -81,7 +80,6 @@ impl fmt::Display for ExprTag { ExprTag::Comm => write!(f, "comm#"), ExprTag::U64 => write!(f, "u64#"), ExprTag::Cproc => write!(f, "cproc#"), - ExprTag::RecVar => write!(f, "rec_var#"), } } } From 1875061da0cb0e2531331c24249689e78a17a624 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sat, 6 Jan 2024 11:29:49 -0300 Subject: [PATCH 02/14] environment tag added --- src/lem/store.rs | 46 +++++++++++++++++++++++++++++++++++++++++++++- src/tag.rs | 2 ++ 2 files changed, 47 insertions(+), 1 deletion(-) diff --git a/src/lem/store.rs b/src/lem/store.rs index 1724bff268..d052d5a2b9 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -23,7 +23,7 @@ use crate::{ self, Binop, Binop2, Call, Call0, Call2, Dummy, Emit, If, Let, LetRec, Lookup, Outermost, Tail, Terminal, Unop, }, - tag::ExprTag::{Char, Comm, Cons, Cproc, Fun, Key, Nil, Num, Str, Sym, Thunk, U64}, + tag::ExprTag::{Char, Comm, Cons, Cproc, Env, Fun, Key, Nil, Num, Str, Sym, Thunk, U64}, }; use super::pointers::{Ptr, RawPtr, ZPtr}; @@ -374,6 +374,11 @@ impl Store { Some(Ptr::new(tag, *raw)) } + #[inline] + pub fn intern_empty_env(&self) -> Ptr { + self.intern_atom(Tag::Expr(Env), F::ZERO) + } + #[inline] pub fn num(&self, f: F) -> Ptr { self.intern_atom(Tag::Expr(Num), f) @@ -756,6 +761,28 @@ impl Store { } } + /// Fetches an environment + pub fn fetch_env(&self, ptr: &Ptr) -> Option> { + if *ptr.tag() != Tag::Expr(Env) { + return None; + } + if *ptr == self.intern_empty_env() { + return Some(vec![]); + } + let mut idx = ptr.raw().get_hash4()?; + let mut list = vec![]; + while let Some([sym_pay, val_tag, val_pay, env_pay]) = self.fetch_raw_ptrs(idx) { + let sym = Ptr::new(Tag::Expr(Sym), *sym_pay); + let val = self.raw_to_ptr(val_tag, val_pay)?; + list.push((sym, val)); + if env_pay == self.intern_empty_env().raw() { + break; + } + idx = env_pay.get_hash4().unwrap(); + } + Some(list) + } + pub fn intern_syntax(&self, syn: Syntax) -> Ptr { match syn { Syntax::Num(_, x) => self.num(x.into_scalar()), @@ -1133,6 +1160,23 @@ impl Ptr { } } }, + Env => { + if let Some(env) = store.fetch_env(self) { + let list = env + .iter() + .map(|(sym, val)| { + format!( + "({} . {})", + sym.fmt_to_string(store, state), + val.fmt_to_string(store, state) + ) + }) + .collect::>(); + format!("", list.join(" ")) + } else { + "".into() + } + } }, Tag::Cont(t) => match t { Outermost => "Outermost".into(), diff --git a/src/tag.rs b/src/tag.rs index af2bc41673..c27eaaf402 100644 --- a/src/tag.rs +++ b/src/tag.rs @@ -51,6 +51,7 @@ pub enum ExprTag { U64, Key, Cproc, + Env, } impl From for u16 { @@ -80,6 +81,7 @@ impl fmt::Display for ExprTag { ExprTag::Comm => write!(f, "comm#"), ExprTag::U64 => write!(f, "u64#"), ExprTag::Cproc => write!(f, "cproc#"), + ExprTag::Env => write!(f, "env#"), } } } From 7ea7f49f9023ba55efd1f82c7d880433099b0dfa Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sat, 6 Jan 2024 11:34:49 -0300 Subject: [PATCH 03/14] `Num`s now take arbitrary raw pointers This is so that we can delay hashing, much like `Ptr`s delay hashing --- src/lem/circuit.rs | 6 +++--- src/lem/interpreter.rs | 12 ++++++------ src/lem/slot.rs | 13 ++++++++----- 3 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/lem/circuit.rs b/src/lem/circuit.rs index ee3cc345f3..bab02643f4 100644 --- a/src/lem/circuit.rs +++ b/src/lem/circuit.rs @@ -260,11 +260,11 @@ pub(crate) fn allocate_slot>( || *z_ptr.value(), )); } - Val::Num(f) => { - let f = store.expect_f(*f); + Val::Num(raw) => { + let f = store.hash_raw_ptr(raw).0; preallocated_preimg.push(AllocatedNum::alloc_infallible( cs.namespace(|| format!("component {component_idx} slot {slot}")), - || *f, + || f, )); } Val::Boolean(b) => { diff --git a/src/lem/interpreter.rs b/src/lem/interpreter.rs index a656a86122..562d8919dd 100644 --- a/src/lem/interpreter.rs +++ b/src/lem/interpreter.rs @@ -284,13 +284,13 @@ impl Block { let g = *store.expect_f(g_idx); let diff = f - g; hints.bit_decomp.push(Some(SlotData { - vals: vec![Val::Num(store.intern_f(f + f).0)], + vals: vec![Val::Num(RawPtr::Atom(store.intern_f(f + f).0))], })); hints.bit_decomp.push(Some(SlotData { - vals: vec![Val::Num(store.intern_f(g + g).0)], + vals: vec![Val::Num(RawPtr::Atom(store.intern_f(g + g).0))], })); hints.bit_decomp.push(Some(SlotData { - vals: vec![Val::Num(store.intern_f(diff + diff).0)], + vals: vec![Val::Num(RawPtr::Atom(store.intern_f(diff + diff).0))], })); let f = BaseNum::Scalar(f); let g = BaseNum::Scalar(g); @@ -306,7 +306,7 @@ impl Block { let c = if let RawPtr::Atom(f_idx) = a { let f = *store.expect_f(f_idx); hints.bit_decomp.push(Some(SlotData { - vals: vec![Val::Num(f_idx)], + vals: vec![Val::Num(RawPtr::Atom(f_idx))], })); let b = if *n < 64 { (1 << *n) - 1 } else { u64::MAX }; store.intern_atom(Tag::Expr(Num), F::from_u64(f.to_u64_unchecked() & b)) @@ -419,7 +419,7 @@ impl Block { }; let secret = *store.expect_f(*secret_idx); let tgt_ptr = store.hide(secret, src_ptr); - let vals = vec![Val::Num(*secret_idx), Val::Pointer(src_ptr)]; + let vals = vec![Val::Num(RawPtr::Atom(*secret_idx)), Val::Pointer(src_ptr)]; hints.commitment.push(Some(SlotData { vals })); bindings.insert_ptr(tgt.clone(), tgt_ptr); } @@ -438,7 +438,7 @@ impl Block { store.intern_atom(Tag::Expr(Num), *secret), ); let secret_idx = store.intern_f(*secret).0; - let vals = vec![Val::Num(secret_idx), Val::Pointer(*ptr)]; + let vals = vec![Val::Num(RawPtr::Atom(secret_idx)), Val::Pointer(*ptr)]; hints.commitment.push(Some(SlotData { vals })); } Op::Unit(f) => f(), diff --git a/src/lem/slot.rs b/src/lem/slot.rs index 266688257d..8a3c9b2a35 100644 --- a/src/lem/slot.rs +++ b/src/lem/slot.rs @@ -103,7 +103,10 @@ //! STEP 2 will need as many iterations as it takes to evaluate the Lurk //! expression and so will STEP 3. -use super::{pointers::Ptr, Block, Ctrl, Op}; +use super::{ + pointers::{Ptr, RawPtr}, + Block, Ctrl, Op, +}; #[derive(Default, Debug, Clone, Copy, PartialEq, Eq)] pub struct SlotsCounter { @@ -234,12 +237,12 @@ impl Block { } #[derive(Clone, Debug)] -/// The values a variable can take. `Num`s are pure field elements, much like `Ptr::Atom`, -/// but missing the tag. `Boolean`s are also field elements, but they are guaranteed to be -/// constrained to take only 0 or 1 values. +/// The values a variable can take. `Num`s represent pure field elements, with no tags. +/// `Boolean`s are also field elements, but they are guaranteed to be constrained to +/// take only 0 or 1 values. pub enum Val { Pointer(Ptr), - Num(usize), + Num(RawPtr), Boolean(bool), } From a38310ab39f9764536d9a28197bca782ce0fab1b Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sat, 6 Jan 2024 13:14:48 -0300 Subject: [PATCH 04/14] added PushBinding/PopBinding operations --- src/lem/circuit.rs | 107 ++++++++++++++++++++++++++++++++++++++++- src/lem/interpreter.rs | 29 ++++++++++- src/lem/macros.rs | 29 +++++++++++ src/lem/mod.rs | 27 +++++++++++ src/lem/slot.rs | 4 +- src/lem/store.rs | 21 ++++++++ 6 files changed, 213 insertions(+), 4 deletions(-) diff --git a/src/lem/circuit.rs b/src/lem/circuit.rs index bab02643f4..ce20e0885f 100644 --- a/src/lem/circuit.rs +++ b/src/lem/circuit.rs @@ -47,7 +47,7 @@ use crate::{ eval::lang::Lang, field::{FWrap, LanguageField, LurkField}, tag::{ - ExprTag::{Comm, Num, Sym}, + ExprTag::{Comm, Env, Num, Sym}, Tag, }, }; @@ -437,6 +437,10 @@ impl Block { g.alloc_tag(cs, &Num); g.alloc_tag(cs, &Comm); } + Op::PushBinding(..) | Op::PopBinding(..) => { + g.alloc_tag(cs, &Sym); + g.alloc_tag(cs, &Env); + } _ => (), } } @@ -701,6 +705,100 @@ fn synthesize_block, C: Coprocessor>( Op::Decons4(preimg, img) => { decons_helper!(preimg, img, SlotType::Hash8); } + Op::PushBinding(img, preimg) => { + // Retrieve allocated preimage + let sym = bound_allocations.get_ptr(&preimg[0])?; + let val = bound_allocations.get_ptr(&preimg[1])?; + let env = bound_allocations.get_ptr(&preimg[2])?; + + // Retrieve the preallocated preimage and image for this slot + let (preallocated_preimg, preallocated_img_hash) = + &ctx.hash4_slots[next_slot.consume_hash4()]; + + // For each component of the preimage, add implication constraints + // for its tag and hash + let sym_tag = ctx.global_allocator.alloc_tag_cloned(&mut cs, &Sym); + let env_tag = ctx.global_allocator.alloc_tag_cloned(&mut cs, &Env); + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.tag", preimg[0])), + not_dummy, + sym.tag(), + &sym_tag, + ); + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.hash", preimg[0])), + not_dummy, + sym.hash(), + &preallocated_preimg[0], + ); + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.tag", preimg[1])), + not_dummy, + val.tag(), + &preallocated_preimg[1], + ); + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.hash", preimg[1])), + not_dummy, + val.hash(), + &preallocated_preimg[2], + ); + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.tag", preimg[2])), + not_dummy, + env.tag(), + &env_tag, + ); + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.hash", preimg[2])), + not_dummy, + env.hash(), + &preallocated_preimg[3], + ); + + // Allocate the image tag if it hasn't been allocated before, + // create the full image pointer and add it to bound allocations + let img_tag = ctx.global_allocator.alloc_tag_cloned(&mut cs, &Env); + let AllocatedVal::Number(img_hash) = preallocated_img_hash else { + bail!("Expected number") + }; + let img_ptr = AllocatedPtr::from_parts(img_tag, img_hash.clone()); + bound_allocations.insert_ptr(img.clone(), img_ptr); + } + Op::PopBinding(preimg, img) => { + // Retrieve allocated image + let allocated_img = bound_allocations.get_ptr(img)?; + + // Retrieve the preallocated preimage and image for this slot + let (preallocated_preimg, preallocated_img_hash) = + ctx.hash4_slots[next_slot.consume_hash4()]; + + // Add the implication constraint for the image + let AllocatedVal::Number(img_hash) = preallocated_img_hash else { + bail!("Expected number") + }; + implies_equal( + &mut cs.namespace(|| format!("implies equal {}.hash", img)), + not_dummy, + allocated_img.hash(), + img_hash, + ); + + // Retrieve preimage hashes and tags create the full preimage pointers + // and add them to bound allocations + let sym_tag = ctx.global_allocator.alloc_tag_cloned(&mut cs, &Sym); + let sym_hash = &preallocated_preimg[0]; + let sym_ptr = AllocatedPtr::from_parts(sym_tag, sym_hash.clone()); + bound_allocations.insert_ptr(preimg[0].clone(), sym_ptr); + let val_tag = &preallocated_preimg[1]; + let val_hash = &preallocated_preimg[2]; + let val_ptr = AllocatedPtr::from_parts(val_tag.clone(), val_hash.clone()); + bound_allocations.insert_ptr(preimg[1].clone(), val_ptr); + let env_tag = ctx.global_allocator.alloc_tag_cloned(&mut cs, &Env); + let env_hash = &preallocated_preimg[3]; + let env_ptr = AllocatedPtr::from_parts(env_tag, env_hash.clone()); + bound_allocations.insert_ptr(preimg[2].clone(), env_ptr); + } Op::Copy(tgt, src) => { bound_allocations.insert(tgt.clone(), bound_allocations.get_cloned(src)?); } @@ -1501,6 +1599,10 @@ impl Func { // tag and hash for 3 preimage pointers num_constraints += 6; } + Op::PushBinding(..) => { + globals.insert(FWrap(Env.to_field())); + num_constraints += 6; + } Op::Cons4(_, tag, _) => { // tag for the image globals.insert(FWrap(tag.to_field())); @@ -1511,7 +1613,8 @@ impl Func { | Op::Or(..) | Op::Decons2(..) | Op::Decons3(..) - | Op::Decons4(..) => { + | Op::Decons4(..) + | Op::PopBinding(..) => { // one constraint for the image's hash num_constraints += 1; } diff --git a/src/lem/interpreter.rs b/src/lem/interpreter.rs index 562d8919dd..0dc2b097b5 100644 --- a/src/lem/interpreter.rs +++ b/src/lem/interpreter.rs @@ -1,4 +1,4 @@ -use anyhow::{anyhow, bail, Result}; +use anyhow::{anyhow, bail, Context, Result}; use super::{ path::Path, @@ -411,6 +411,33 @@ impl Block { let vals = preimg_ptrs.into_iter().map(Val::Pointer).collect(); hints.hash8.push(Some(SlotData { vals })); } + Op::PushBinding(img, preimg) => { + let preimg_ptrs = bindings.get_many_ptr(preimg)?; + let tgt_ptr = + store.push_binding(preimg_ptrs[0], preimg_ptrs[1], preimg_ptrs[2]); + bindings.insert_ptr(img.clone(), tgt_ptr); + let vals = vec![ + Val::Num(*preimg_ptrs[0].raw()), + Val::Pointer(preimg_ptrs[1]), + Val::Num(*preimg_ptrs[2].raw()), + ]; + hints.hash4.push(Some(SlotData { vals })); + } + Op::PopBinding(preimg, img) => { + let img_ptr = bindings.get_ptr(img)?; + let preimg_ptrs = store + .pop_binding(img_ptr) + .context("cannot extract {img}'s binding")?; + for (var, ptr) in preimg.iter().zip(preimg_ptrs.iter()) { + bindings.insert_ptr(var.clone(), *ptr); + } + let vals = vec![ + Val::Num(*preimg_ptrs[0].raw()), + Val::Pointer(preimg_ptrs[1]), + Val::Num(*preimg_ptrs[2].raw()), + ]; + hints.hash4.push(Some(SlotData { vals })); + } Op::Hide(tgt, sec, src) => { let src_ptr = bindings.get_ptr(src)?; let sec_ptr = bindings.get_ptr(sec)?; diff --git a/src/lem/macros.rs b/src/lem/macros.rs index bac1d1e748..e9e16c5488 100644 --- a/src/lem/macros.rs +++ b/src/lem/macros.rs @@ -195,6 +195,15 @@ macro_rules! op { $crate::var!($src), ) }; + ( let $tgt:ident = push_binding($src1:ident, $src2:ident, $src3:ident) ) => { + $crate::lem::Op::PushBinding( + $crate::var!($tgt), + $crate::vars!($src1, $src2, $src3), + ) + }; + ( let ($tgt1:ident, $tgt2:ident, $tgt3:ident) = pop_binding($src:ident) ) => { + $crate::lem::Op::PopBinding($crate::vars!($tgt1, $tgt2, $tgt3), $crate::var!($src)) + }; ( let $tgt:ident = hide($sec:ident, $src:ident) ) => { $crate::lem::Op::Hide($crate::var!($tgt), $crate::var!($sec), $crate::var!($src)) }; @@ -574,6 +583,26 @@ macro_rules! block { $($tail)* ) }; + (@seq {$($limbs:expr)*}, let $tgt:ident = push_binding($src1:ident, $src2:ident, $src3:ident) ; $($tail:tt)*) => { + $crate::block! ( + @seq + { + $($limbs)* + $crate::op!(let $tgt = push_binding($src1, $src2, $src3) ) + }, + $($tail)* + ) + }; + (@seq {$($limbs:expr)*}, let ($tgt1:ident, $tgt2:ident, $tgt3:ident) = pop_binding($src:ident) ; $($tail:tt)*) => { + $crate::block! ( + @seq + { + $($limbs)* + $crate::op!(let ($tgt1, $tgt2, $tgt3) = pop_binding($src) ) + }, + $($tail)* + ) + }; (@seq {$($limbs:expr)*}, let $tgt:ident = hide($sec:ident, $src:ident) ; $($tail:tt)*) => { $crate::block! ( @seq diff --git a/src/lem/mod.rs b/src/lem/mod.rs index f6986c4bb1..0ba5fc1003 100644 --- a/src/lem/mod.rs +++ b/src/lem/mod.rs @@ -228,6 +228,15 @@ pub enum Op { Decons3([Var; 3], Var), /// `Decons4([a, b, c, d], x)` binds `a`, `b`, `c` and `d` to the 4 children of `x` Decons4([Var; 4], Var), + /// `PushBinding(x, ys)` is a Lurk specific operation. It binds `x` to a `Ptr` + /// with tag `Env` and 3 children `ys`. The first child is assumed to be a `Sym` + /// pointer, the last child is assumed to be an `Env` pointer. This is compiled + /// to an efficient representation, with 4 hashes instead of 6. This operation + /// might be deprecated when LEM is more expressive and is able to have variables + /// of other types other than pointers + PushBinding(Var, [Var; 3]), + /// `PopBinding(ys, x)` is the inverse of `PushBinding` + PopBinding([Var; 3], Var), /// `Hide(x, s, p)` binds `x` to a (comm) `Ptr` resulting from hiding the /// payload `p` with (num) secret `s` Hide(Var, Var, Var), @@ -380,6 +389,14 @@ impl Func { is_bound(img, map)?; preimg.iter().for_each(|var| is_unique(var, map)) } + Op::PushBinding(img, preimg) => { + preimg.iter().try_for_each(|arg| is_bound(arg, map))?; + is_unique(img, map); + } + Op::PopBinding(preimg, img) => { + is_bound(img, map)?; + preimg.iter().for_each(|var| is_unique(var, map)) + } Op::Hide(tgt, sec, src) => { is_bound(sec, map)?; is_bound(src, map)?; @@ -664,6 +681,16 @@ impl Block { let preimg = insert_many(map, uniq, &preimg); ops.push(Op::Decons4(preimg.try_into().unwrap(), img)) } + Op::PushBinding(img, preimg) => { + let preimg = map.get_many_cloned(&preimg)?.try_into().unwrap(); + let img = insert_one(map, uniq, &img); + ops.push(Op::PushBinding(img, preimg)) + } + Op::PopBinding(preimg, img) => { + let img = map.get_cloned(&img)?; + let preimg = insert_many(map, uniq, &preimg); + ops.push(Op::PopBinding(preimg.try_into().unwrap(), img)) + } Op::Hide(tgt, sec, pay) => { let sec = map.get_cloned(&sec)?; let pay = map.get_cloned(&pay)?; diff --git a/src/lem/slot.rs b/src/lem/slot.rs index 8a3c9b2a35..e3b27dd5bf 100644 --- a/src/lem/slot.rs +++ b/src/lem/slot.rs @@ -198,7 +198,9 @@ impl Block { pub fn count_slots(&self) -> SlotsCounter { let ops_slots = self.ops.iter().fold(SlotsCounter::default(), |acc, op| { let val = match op { - Op::Cons2(..) | Op::Decons2(..) => SlotsCounter::new((1, 0, 0, 0, 0)), + Op::Cons2(..) | Op::Decons2(..) | Op::PushBinding(..) | Op::PopBinding(..) => { + SlotsCounter::new((1, 0, 0, 0, 0)) + } Op::Cons3(..) | Op::Decons3(..) => SlotsCounter::new((0, 1, 0, 0, 0)), Op::Cons4(..) | Op::Decons4(..) => SlotsCounter::new((0, 0, 1, 0, 0)), Op::Hide(..) | Op::Open(..) => SlotsCounter::new((0, 0, 0, 1, 0)), diff --git a/src/lem/store.rs b/src/lem/store.rs index d052d5a2b9..fc1cd21537 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -374,6 +374,27 @@ impl Store { Some(Ptr::new(tag, *raw)) } + #[inline] + pub fn push_binding(&self, sym: Ptr, val: Ptr, env: Ptr) -> Ptr { + assert_eq!(*sym.tag(), Tag::Expr(Sym)); + assert_eq!(*env.tag(), Tag::Expr(Env)); + let raw = + self.intern_raw_ptrs::<4>([*sym.raw(), self.tag(*val.tag()), *val.raw(), *env.raw()]); + Ptr::new(Tag::Expr(Env), raw) + } + + #[inline] + pub fn pop_binding(&self, env: Ptr) -> Option<[Ptr; 3]> { + assert_eq!(*env.tag(), Tag::Expr(Env)); + let idx = env.get_index2()?; + let [sym_pay, val_tag, val_pay, env_pay] = self.fetch_raw_ptrs::<4>(idx)?; + let val_tag = self.fetch_tag(val_tag)?; + let sym = Ptr::new(Tag::Expr(Sym), *sym_pay); + let val = Ptr::new(val_tag, *val_pay); + let env = Ptr::new(Tag::Expr(Env), *env_pay); + Some([sym, val, env]) + } + #[inline] pub fn intern_empty_env(&self) -> Ptr { self.intern_atom(Tag::Expr(Env), F::ZERO) From 0344809f226f77b3b2d3ef10d05ec335633a763d Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sat, 6 Jan 2024 15:06:45 -0300 Subject: [PATCH 05/14] eval uses optimized environment --- src/cli/repl/mod.rs | 2 +- src/lem/eval.rs | 91 ++++++++++++++++++++----------------------- src/lem/multiframe.rs | 4 +- 3 files changed, 46 insertions(+), 51 deletions(-) diff --git a/src/cli/repl/mod.rs b/src/cli/repl/mod.rs index 84baa2bda0..c472ef4f08 100644 --- a/src/cli/repl/mod.rs +++ b/src/cli/repl/mod.rs @@ -185,7 +185,7 @@ where let current_dir = std::env::current_dir().expect("couldn't capture current directory"); let pwd_path = Utf8PathBuf::from_path_buf(current_dir).expect("path contains invalid Unicode"); - let env = store.intern_nil(); + let env = store.intern_empty_env(); let lurk_step = make_eval_step_from_config(&EvalConfig::new_ivc(&lang)); let cprocs = make_cprocs_funcs_from_lang(&lang); Repl { diff --git a/src/lem/eval.rs b/src/lem/eval.rs index fea8536f50..519c6cc98a 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -196,7 +196,7 @@ pub fn evaluate>( evaluate_with_env_and_cont( lang_setup, expr, - store.intern_nil(), + store.intern_empty_env(), store.cont_outermost(), store, limit, @@ -229,7 +229,7 @@ pub fn evaluate_simple>( store: &Store, limit: usize, ) -> Result<(Vec, usize, Vec)> { - evaluate_simple_with_env(lang_setup, expr, store.intern_nil(), store, limit) + evaluate_simple_with_env(lang_setup, expr, store.intern_empty_env(), store, limit) } pub struct EvalConfig<'a, F, C> { @@ -802,36 +802,25 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (nil) }); let is_cproc = is_cproc(cprocs); - let lookup = func!(lookup(expr, env, state, binding): 4 => { + let lookup = func!(lookup(expr, env, state, maybe_var): 4 => { let found = Symbol("found"); let not_found = Symbol("not_found"); let error = Symbol("error"); let continue = eq_val(not_found, state); if !continue { - return (expr, env, state, binding) + return (expr, env, state, maybe_var) } - match env.tag { - Expr::Nil => { - return (expr, env, error, binding) - } - }; - let (binding, smaller_env) = car_cdr(env); - match binding.tag { - Expr::Nil => { - return (expr, env, error, binding) - } - }; - let (var, val) = decons2(binding); - match var.tag { - Expr::Sym => { - let eq_val = eq_val(var, expr); - if eq_val { - return (val, env, found, binding) - } - return (expr, smaller_env, not_found, binding) - } - }; - return (expr, env, error, binding) + let zero = Num(0); + let env_is_zero = eq_val(env, zero); + if env_is_zero { + return (expr, env, error, maybe_var) + } + let (var, val, smaller_env) = pop_binding(env); + let eq_val = eq_val(var, expr); + if eq_val { + return (val, env, found, var) + } + return (expr, smaller_env, not_found, var) }); func!(reduce(expr, env, cont): 4 => { @@ -880,10 +869,15 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (expr, env, cont, apply) } let not_found = Symbol("not_found"); - let (expr, env, state, binding) = lookup(expr, env, not_found, nil); - let (expr, env, state, binding) = lookup(expr, env, state, binding); - let (expr, env, state, binding) = lookup(expr, env, state, binding); - let (expr, env, state, binding) = lookup(expr, env, state, binding); + let zero = Num(0); + let (expr, env, state, var) = lookup(expr, env, not_found, zero); + let (expr, env, state, var) = lookup(expr, env, state, var); + let (expr, env, state, var) = lookup(expr, env, state, var); + let (expr, env, state, var) = lookup(expr, env, state, var); + let (expr, env, state, var) = lookup(expr, env, state, var); + let (expr, env, state, var) = lookup(expr, env, state, var); + let (expr, env, state, var) = lookup(expr, env, state, var); + let (expr, env, state, var) = lookup(expr, env, state, var); match symbol state { "error" => { return (expr, env, err, errctrl) @@ -892,7 +886,7 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { match expr.tag { Expr::Thunk => { let (body, body_env) = decons2(expr); - let env: Expr::Cons = cons2(binding, body_env); + let env = push_binding(var, expr, body_env); return (body, env, cont, ret) } }; @@ -951,8 +945,7 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (val, env, cont, ret) } let thunk: Expr::Thunk = cons2(val, env); - let binding: Expr::Cons = cons2(var, thunk); - let rec_env: Expr::Cons = cons2(binding, env); + let rec_env = push_binding(var, thunk, env); let cont: Cont::LetRec = cons4(var, env, expanded, cont); return (val, rec_env, cont, ret) } @@ -1191,6 +1184,7 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { let t = Symbol("t"); let nil = Symbol("nil"); let nil = cast(nil, Expr::Nil); + let empty_env: Expr::Env; let empty_str = String(""); let zero = Num(0); let foo: Expr::Nil; @@ -1201,7 +1195,7 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { match cont.tag { Cont::Outermost => { // We erase the environment as to not leak any information about internal variables. - return (result, nil, term, ret) + return (result, empty_env, term, ret) } Cont::Emit => { let (cont, _rest, _foo, _foo) = decons4(cont); @@ -1250,8 +1244,7 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { let (vars, body, fun_env, _foo) = decons4(function); // vars must be non-empty, so: let (var, rest_vars) = decons2(vars); - let binding: Expr::Cons = cons2(var, result); - let ext_env: Expr::Cons = cons2(binding, fun_env); + let ext_env = push_binding(var, result, fun_env); let rest_vars_empty = eq_tag(rest_vars, nil); let args_empty = eq_tag(args, nil); if rest_vars_empty { @@ -1282,14 +1275,12 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { } Cont::Let => { let (var, saved_env, body, cont) = decons4(cont); - let binding: Expr::Cons = cons2(var, result); - let extended_env: Expr::Cons = cons2(binding, saved_env); + let extended_env = push_binding(var, result, saved_env); return (body, extended_env, cont, ret) } Cont::LetRec => { let (var, saved_env, body, cont) = decons4(cont); - let binding: Expr::Cons = cons2(var, result); - let extended_env: Expr::Cons = cons2(binding, saved_env); + let extended_env = push_binding(var, result, saved_env); return (body, extended_env, cont, ret) } Cont::Unop => { @@ -1413,7 +1404,7 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { return(result, env, err, errctrl) } Op1::Eval => { - return(result, nil, continuation, ret) + return(result, empty_env, continuation, ret) } }; return (result, env, err, errctrl) @@ -1448,7 +1439,12 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { let args_num_type_eq_nil = eq_tag(args_num_type, nil); match operator.tag { Op2::Eval => { - return (evaled_arg, result, continuation, ret) + match result.tag { + Expr::Env => { + return (evaled_arg, result, continuation, ret) + } + }; + return (result, env, err, errctrl) } Op2::Cons => { let val: Expr::Cons = cons2(evaled_arg, result); @@ -1685,10 +1681,9 @@ fn make_thunk() -> Func { "make-thunk" => { match cont.tag { Cont::Outermost => { - let nil = Symbol("nil"); - let nil = cast(nil, Expr::Nil); + let empty_env: Expr::Env; let cont: Cont::Terminal = HASH_8_ZEROS; - return (expr, nil, cont) + return (expr, empty_env, cont) } }; let thunk: Expr::Thunk = cons2(expr, cont); @@ -1722,7 +1717,7 @@ mod tests { assert_eq!( func.slots_count, SlotsCounter { - hash4: 17, + hash4: 15, hash6: 0, hash8: 5, commitment: 1, @@ -1733,8 +1728,8 @@ mod tests { expected.assert_eq(&computed.to_string()); }; expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["9377"]); - expect_eq(cs.num_constraints(), expect!["11318"]); + expect_eq(cs.aux().len(), expect!["8831"]); + expect_eq(cs.num_constraints(), expect!["10780"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } } diff --git a/src/lem/multiframe.rs b/src/lem/multiframe.rs index 00acebc5ef..f4099bebeb 100644 --- a/src/lem/multiframe.rs +++ b/src/lem/multiframe.rs @@ -404,7 +404,7 @@ impl EvaluationStore for Store { } fn initial_empty_env(&self) -> Self::Ptr { - self.intern_nil() + self.intern_empty_env() } fn get_cont_terminal(&self) -> Self::Ptr { @@ -1085,7 +1085,7 @@ mod tests { let mut frame = frames.pop().unwrap(); // faking a trivial evaluation frame - frame.output = vec![expr, store.intern_nil(), store.cont_terminal()]; + frame.output = vec![expr, store.intern_empty_env(), store.cont_terminal()]; let mut cs = TestConstraintSystem::::new(); From f631178b896fb041940ec00a30ae6f25c5f45fc5 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sat, 6 Jan 2024 14:13:52 -0300 Subject: [PATCH 06/14] updated tests to new environment --- src/lem/tests/eval_tests.rs | 14 +++++++------- src/proof/tests/nova_tests_lem.rs | 10 +++++----- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/lem/tests/eval_tests.rs b/src/lem/tests/eval_tests.rs index 63f494bc4c..44d29f566e 100644 --- a/src/lem/tests/eval_tests.rs +++ b/src/lem/tests/eval_tests.rs @@ -652,7 +652,7 @@ fn evaluate_arithmetic_let() { (/ (+ a b) c))"; let expected = s.num_u64(3); - let new_env = s.intern_nil(); + let new_env = s.intern_empty_env(); let terminal = s.cont_terminal(); test_aux::>( s, @@ -1147,7 +1147,7 @@ fn evaluate_zero_arg_lambda() { let expected = { let args = s.list(vec![s.intern_user_symbol("x")]); let num = s.num_u64(123); - let env = s.intern_nil(); + let env = s.intern_empty_env(); s.intern_fun(args, num, env) }; @@ -1687,7 +1687,7 @@ fn begin_current_env() { { let s = &Store::::default(); let expr = "(begin (current-env))"; - let expected = s.intern_nil(); + let expected = s.intern_empty_env(); test_aux::>( s, expr, @@ -1728,8 +1728,8 @@ fn begin_current_env1() { (begin 123 (current-env)))"; let a = s.intern_user_symbol("a"); let one = s.num_u64(1); - let binding = s.cons(a, one); - let expected = s.list(vec![binding]); + let env = s.intern_empty_env(); + let expected = s.push_binding(a, one, env); test_aux::>( s, expr, @@ -2576,7 +2576,7 @@ fn test_quoted_symbols() { fn test_eval() { let s = &Store::::default(); let expr = "(* 3 (eval (cons '+ (cons 1 (cons 2 nil)))))"; - let expr2 = "(* 5 (eval '(+ 1 a) '((a . 3))))"; // two-arg eval, optional second arg is env. + let expr2 = "(* 5 (eval '(+ 1 a) (let ((a 3)) (current-env))))"; // two-arg eval, optional second arg is env. let res = s.num_u64(9); let res2 = s.num_u64(20); let terminal = s.cont_terminal(); @@ -2598,7 +2598,7 @@ fn test_eval() { None, Some(terminal), None, - &expect!["9"], + &expect!["11"], &None, ); } diff --git a/src/proof/tests/nova_tests_lem.rs b/src/proof/tests/nova_tests_lem.rs index ba3760989b..356f6aa005 100644 --- a/src/proof/tests/nova_tests_lem.rs +++ b/src/proof/tests/nova_tests_lem.rs @@ -819,7 +819,7 @@ fn test_prove_adder() { #[test] fn test_prove_current_env_simple() { let s = &Store::::default(); - let expected = s.intern_nil(); + let expected = s.intern_empty_env(); let terminal = s.cont_terminal(); test_aux::<_, Coproc<_>>( s, @@ -1544,7 +1544,7 @@ fn test_prove_zero_arg_lambda3() { let expected = { let args = s.list(vec![s.intern_user_symbol("x")]); let num = s.num_u64(123); - let env = s.intern_nil(); + let env = s.intern_empty_env(); s.intern_fun(args, num, env) }; let terminal = s.cont_terminal(); @@ -3009,7 +3009,7 @@ fn test_relational_edge_case_identity() { fn test_prove_test_eval() { let s = &Store::::default(); let expr = "(* 3 (eval (cons '+ (cons 1 (cons 2 nil)))))"; - let expr2 = "(* 5 (eval '(+ 1 a) '((a . 3))))"; // two-arg eval, optional second arg is env. + let expr2 = "(* 5 (eval '(+ 1 a) (let ((a 3)) (current-env))))"; // two-arg eval, optional second arg is env. let res = s.num_u64(9); let res2 = s.num_u64(20); let terminal = s.cont_terminal(); @@ -3031,7 +3031,7 @@ fn test_prove_test_eval() { None, Some(terminal), None, - &expect!["9"], + &expect!["11"], &None, ); } @@ -3783,7 +3783,7 @@ fn test_prove_dotted_syntax_error() { #[test] fn test_prove_call_literal_fun() { let s = &Store::::default(); - let empty_env = s.intern_nil(); + let empty_env = s.intern_empty_env(); let args = s.list(vec![s.intern_user_symbol("x")]); let body = s.read_with_default_state("(+ x 1)").unwrap(); let fun = intern_ptrs!(s, Tag::Expr(ExprTag::Fun), args, body, empty_env, s.dummy()); From 340a3db669d913520d6032fb848b61ca4093cf4f Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sun, 7 Jan 2024 12:08:03 -0300 Subject: [PATCH 07/14] reverted `letrec` change Now `letrec` works as before, but updated to the new, changed, environment. The reason for reverting is that the iteration count increased in a bunch of tests. For thunks to work properly, we will need the memoset implementation of eval --- src/lem/eval.rs | 42 ++++++++++++++++++++++-------------------- src/lem/store.rs | 27 ++++++++++++++++++++++++++- src/tag.rs | 2 ++ 3 files changed, 50 insertions(+), 21 deletions(-) diff --git a/src/lem/eval.rs b/src/lem/eval.rs index 519c6cc98a..c6a03491bc 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -884,10 +884,12 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { } "found" => { match expr.tag { - Expr::Thunk => { - let (body, body_env) = decons2(expr); - let env = push_binding(var, expr, body_env); - return (body, env, cont, ret) + // if `val2` is a recursive closure, then extend its environment + Expr::Rec => { + let (args, body, closed_env, _foo) = decons4(expr); + let extended = push_binding(var, expr, closed_env); + let fun: Expr::Fun = cons4(args, body, extended, foo); + return (fun, env, cont, apply) } }; return (expr, env, cont, apply) @@ -944,10 +946,8 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let cont: Cont::Let = cons4(var, env, expanded, cont); return (val, env, cont, ret) } - let thunk: Expr::Thunk = cons2(val, env); - let rec_env = push_binding(var, thunk, env); let cont: Cont::LetRec = cons4(var, env, expanded, cont); - return (val, rec_env, cont, ret) + return (val, env, cont, ret) } }; return (expr, env, err, errctrl) @@ -1280,6 +1280,13 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { } Cont::LetRec => { let (var, saved_env, body, cont) = decons4(cont); + match result.tag { + Expr::Fun => { + let result = cast(result, Expr::Rec); + let extended_env = push_binding(var, result, saved_env); + return (body, extended_env, cont, ret) + } + }; let extended_env = push_binding(var, result, saved_env); return (body, extended_env, cont, ret) } @@ -1700,7 +1707,7 @@ mod tests { use super::*; use crate::{ eval::lang::{Coproc, Lang}, - lem::{slot::SlotsCounter, store::Store}, + lem::store::Store, }; use bellpepper_core::{test_cs::TestConstraintSystem, Comparable}; use expect_test::{expect, Expect}; @@ -1714,22 +1721,17 @@ mod tests { let mut cs = TestConstraintSystem::::new(); let lang: Lang> = Lang::new(); let _ = func.synthesize_frame_aux(&mut cs, &store, &frame, &lang); - assert_eq!( - func.slots_count, - SlotsCounter { - hash4: 15, - hash6: 0, - hash8: 5, - commitment: 1, - bit_decomp: 3, - } - ); let expect_eq = |computed: usize, expected: Expect| { expected.assert_eq(&computed.to_string()); }; + expect_eq(func.slots_count.hash4, expect!["14"]); + expect_eq(func.slots_count.hash6, expect!["0"]); + expect_eq(func.slots_count.hash8, expect!["6"]); + expect_eq(func.slots_count.commitment, expect!["1"]); + expect_eq(func.slots_count.bit_decomp, expect!["3"]); expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["8831"]); - expect_eq(cs.num_constraints(), expect!["10780"]); + expect_eq(cs.aux().len(), expect!["8938"]); + expect_eq(cs.num_constraints(), expect!["10897"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } } diff --git a/src/lem/store.rs b/src/lem/store.rs index fc1cd21537..a1d4ba735c 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -23,7 +23,7 @@ use crate::{ self, Binop, Binop2, Call, Call0, Call2, Dummy, Emit, If, Let, LetRec, Lookup, Outermost, Tail, Terminal, Unop, }, - tag::ExprTag::{Char, Comm, Cons, Cproc, Env, Fun, Key, Nil, Num, Str, Sym, Thunk, U64}, + tag::ExprTag::{Char, Comm, Cons, Cproc, Env, Fun, Key, Nil, Num, Rec, Str, Sym, Thunk, U64}, }; use super::pointers::{Ptr, RawPtr, ZPtr}; @@ -1142,6 +1142,31 @@ impl Ptr { } } }, + Rec => match self.raw().get_hash8() { + None => "".into(), + Some(idx) => { + if let Some([vars, body, _, _]) = fetch_ptrs!(store, 4, idx) { + match vars.tag() { + Tag::Expr(Nil) => { + format!( + "", + body.fmt_to_string(store, state) + ) + } + Tag::Expr(Cons) => { + format!( + "", + vars.fmt_to_string(store, state), + body.fmt_to_string(store, state) + ) + } + _ => "".into(), + } + } else { + "".into() + } + } + }, Thunk => match self.raw().get_hash4() { None => "".into(), Some(idx) => { diff --git a/src/tag.rs b/src/tag.rs index c27eaaf402..88154a7bcd 100644 --- a/src/tag.rs +++ b/src/tag.rs @@ -52,6 +52,7 @@ pub enum ExprTag { Key, Cproc, Env, + Rec, } impl From for u16 { @@ -82,6 +83,7 @@ impl fmt::Display for ExprTag { ExprTag::U64 => write!(f, "u64#"), ExprTag::Cproc => write!(f, "cproc#"), ExprTag::Env => write!(f, "env#"), + ExprTag::Rec => write!(f, "rec#"), } } } From 9a8e1d3354291d705c193682842df2c96a8c5f0f Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sun, 7 Jan 2024 14:25:48 -0300 Subject: [PATCH 08/14] test iterations updated --- src/lem/tests/eval_tests.rs | 14 +++++++------- src/proof/tests/nova_tests_lem.rs | 20 ++++++++++---------- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/lem/tests/eval_tests.rs b/src/lem/tests/eval_tests.rs index 44d29f566e..539f303f31 100644 --- a/src/lem/tests/eval_tests.rs +++ b/src/lem/tests/eval_tests.rs @@ -828,7 +828,7 @@ fn evaluate_recursion2() { None, Some(terminal), None, - &expect!["122"], + &expect!["117"], &None, ); } @@ -902,7 +902,7 @@ fn evaluate_tail_recursion() { None, Some(terminal), None, - &expect!["80"], + &expect!["77"], &None, ); } @@ -930,7 +930,7 @@ fn evaluate_tail_recursion_somewhat_optimized() { None, Some(terminal), None, - &expect!["73"], + &expect!["70"], &None, ); } @@ -1371,7 +1371,7 @@ fn dont_discard_rest_env() { None, Some(terminal), None, - &expect!["15"], + &expect!["14"], &None, ); } @@ -1677,7 +1677,7 @@ fn go_translate() { None, None, None, - &expect!["509"], + &expect!["443"], &None, ); } @@ -3340,7 +3340,7 @@ fn test_fold_cons_regression() { None, Some(terminal), None, - &expect!["67"], + &expect!["64"], &None, ); } @@ -3370,7 +3370,7 @@ fn test_eval_bad_form() { let expr = "(* 5 (eval '(+ 1 a) '((0 . 3))))"; // two-arg eval, optional second arg is env. let error = s.cont_error(); - test_aux::>(s, expr, None, None, Some(error), None, &expect!["8"], &None); + test_aux::>(s, expr, None, None, Some(error), None, &expect!["5"], &None); } #[test] diff --git a/src/proof/tests/nova_tests_lem.rs b/src/proof/tests/nova_tests_lem.rs index 356f6aa005..dd4a8d39d2 100644 --- a/src/proof/tests/nova_tests_lem.rs +++ b/src/proof/tests/nova_tests_lem.rs @@ -381,7 +381,7 @@ fn test_prove_recursion2() { None, Some(terminal), None, - &expect!["59"], + &expect!["57"], &None, ); } @@ -1324,7 +1324,7 @@ fn test_prove_tail_recursion() { None, Some(terminal), None, - &expect!["59"], + &expect!["57"], &None, ); } @@ -1350,7 +1350,7 @@ fn test_prove_tail_recursion_somewhat_optimized() { None, Some(terminal), None, - &expect!["55"], &None + &expect!["53"], &None ); } @@ -1855,7 +1855,7 @@ fn test_prove_dont_discard_rest_env() { None, Some(terminal), None, - &expect!["15"], + &expect!["14"], &None, ); } @@ -1881,7 +1881,7 @@ fn test_prove_fibonacci() { None, Some(terminal), None, - &expect!["40"], + &expect!["35"], 5, false, None, @@ -1945,7 +1945,7 @@ fn test_prove_chained_functional_commitment() { None, Some(terminal), None, - &expect!["24"], + &expect!["22"], &None, ); } @@ -3131,7 +3131,7 @@ fn test_prove_complicated_functional_commitment() { None, Some(terminal), None, - &expect!["69"], + &expect!["68"], &None, ); } @@ -3154,7 +3154,7 @@ fn test_prove_test_fold_cons_regression() { None, Some(terminal), None, - &expect!["67"], + &expect!["64"], &None, ); } @@ -3185,7 +3185,7 @@ fn test_prove_reduce_sym_contradiction_regression() { let expr = "(eval 'a '(nil))"; let error = s.cont_error(); - test_aux::<_, Coproc<_>>(s, expr, None, None, Some(error), None, &expect!["4"], &None); + test_aux::<_, Coproc<_>>(s, expr, None, None, Some(error), None, &expect!["3"], &None); } #[test] @@ -3248,7 +3248,7 @@ fn test_prove_test_eval_bad_form() { let expr = "(* 5 (eval '(+ 1 a) '((0 . 3))))"; // two-arg eval, optional second arg is env. This tests for error on malformed env. let error = s.cont_error(); - test_aux::<_, Coproc<_>>(s, expr, None, None, Some(error), None, &expect!["8"], &None); + test_aux::<_, Coproc<_>>(s, expr, None, None, Some(error), None, &expect!["5"], &None); } #[test] From dae5e0590b10c068c74a3d3de31212571e115189 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 9 Jan 2024 12:57:05 -0300 Subject: [PATCH 09/14] fixed repl and fib benchmark --- benches/common/fib.rs | 12 ++++++++---- src/cli/repl/meta_cmd.rs | 20 +++++++++++--------- src/cli/repl/mod.rs | 2 +- 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/benches/common/fib.rs b/benches/common/fib.rs index a403b14f9f..f32c1844b9 100644 --- a/benches/common/fib.rs +++ b/benches/common/fib.rs @@ -56,14 +56,18 @@ fn lurk_fib(store: &Store, n: usize) -> Ptr { // saved_env: (((.lurk.user.next . ))), // body: (.lurk.user.fib), continuation: Outermost } - let (_, rest_bindings) = store.car_cdr(target_env).unwrap(); - let (second_binding, _) = store.car_cdr(&rest_bindings).unwrap(); - store.car_cdr(&second_binding).unwrap().1 + let [_, _, rest_bindings] = store.pop_binding(*target_env).unwrap(); + let [_, val, _] = store.pop_binding(rest_bindings).unwrap(); + val } // Returns the linear and angular coefficients for the iteration count of fib fn compute_coeffs(store: &Store) -> (usize, usize) { - let mut input = vec![fib_expr(store), store.intern_nil(), store.cont_outermost()]; + let mut input = vec![ + fib_expr(store), + store.intern_empty_env(), + store.cont_outermost(), + ]; let lang: Lang> = Lang::new(); let mut coef_lin = 0; let coef_ang; diff --git a/src/cli/repl/meta_cmd.rs b/src/cli/repl/meta_cmd.rs index c0925bd96c..cfbd283942 100644 --- a/src/cli/repl/meta_cmd.rs +++ b/src/cli/repl/meta_cmd.rs @@ -313,7 +313,7 @@ where description: &[], example: &["!(def a 1)", "(current-env)", "!(clear)", "(current-env)"], run: |repl, _args, _path| { - repl.env = repl.store.intern_nil(); + repl.env = repl.store.intern_empty_env(); Ok(()) }, }; @@ -327,7 +327,11 @@ where run: |repl, args, _path| { let first = repl.peek1(args)?; let (first_io, ..) = repl.eval_expr(first)?; - repl.env = first_io[0]; + let env = first_io[0]; + if *env.tag() != Tag::Expr(ExprTag::Env) { + return Err(anyhow!("Value must be an environment")); + } + repl.env = env; Ok(()) }, }; @@ -660,8 +664,7 @@ where let path = get_path(repl, &path)?; let LurkData:: { z_ptr, z_dag } = load(&path)?; let ptr = z_dag.populate_store(&z_ptr, &repl.store, &mut Default::default())?; - let binding = repl.store.cons(sym, ptr); - repl.env = repl.store.cons(binding, repl.env); + repl.env = repl.store.push_binding(sym, ptr, repl.env); Ok(()) }, }; @@ -716,7 +719,7 @@ where } let lambda = repl.store.list(vec![repl.store.intern_lurk_symbol("lambda"), vars, body]); - let (io, ..) = repl.eval_expr_with_env(lambda, repl.store.intern_nil())?; + let (io, ..) = repl.eval_expr_with_env(lambda, repl.store.intern_empty_env())?; let fun = io[0]; if !fun.is_fun() { bail!( @@ -761,8 +764,7 @@ where // the standard format for a processed protocol as Lurk data let protocol = repl.store.list(vec![fun, rc, lang, description]); - let binding = repl.store.cons(name, protocol); - repl.env = repl.store.cons(binding, repl.env); + repl.env = repl.store.push_binding(name, protocol, repl.env); Ok(()) }, }; @@ -824,7 +826,7 @@ where .list(vec![*repl.get_apply_fn(), fun, quoted_args]); let (io, ..) = repl - .eval_expr_with_env(apply_call, repl.store.intern_nil()) + .eval_expr_with_env(apply_call, repl.store.intern_empty_env()) .with_context(|| "evaluating protocol function call")?; let (Tag::Expr(ExprTag::Cons), RawPtr::Hash4(idx)) = &io[0].parts() else { @@ -858,7 +860,7 @@ where if !post_verify.is_nil() { let call = repl.store.list(vec![post_verify]); let (io, ..) = repl - .eval_expr_with_env(call, repl.store.intern_nil()) + .eval_expr_with_env(call, repl.store.intern_empty_env()) .with_context(|| "evaluating post-verify call")?; if io[0].is_nil() { bail!("Post-verification predicate rejected the input") diff --git a/src/cli/repl/mod.rs b/src/cli/repl/mod.rs index c472ef4f08..32f19dd12c 100644 --- a/src/cli/repl/mod.rs +++ b/src/cli/repl/mod.rs @@ -224,7 +224,7 @@ where ) .unwrap(); let (io, ..) = self - .eval_expr_with_env(ptr, self.store.intern_nil()) + .eval_expr_with_env(ptr, self.store.intern_empty_env()) .unwrap(); io[0] }) From 825e1e303e9d0730de9333ac89caf6f319d8cbcc Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 9 Jan 2024 13:39:53 -0300 Subject: [PATCH 10/14] fixed zstore --- src/cli/zstore.rs | 73 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 59 insertions(+), 14 deletions(-) diff --git a/src/cli/zstore.rs b/src/cli/zstore.rs index 96a0ebad8d..303da66c2e 100644 --- a/src/cli/zstore.rs +++ b/src/cli/zstore.rs @@ -7,7 +7,9 @@ use crate::{ lem::{ pointers::{Ptr, RawPtr, ZPtr}, store::{expect_ptrs, intern_ptrs_hydrated, Store}, + tag::Tag, }, + tag::ExprTag::{Env, Sym}, }; use super::field_data::HasFieldModulus; @@ -21,6 +23,7 @@ pub(crate) enum ZPtrType { Tuple2(ZPtr, ZPtr), Tuple3(ZPtr, ZPtr, ZPtr), Tuple4(ZPtr, ZPtr, ZPtr, ZPtr), + Env(ZPtr, ZPtr, ZPtr), } /// Holds a mapping from `ZPtr`s to their `ZPtrType`s @@ -47,20 +50,44 @@ impl ZDag { z_ptr } RawPtr::Hash4(idx) => { - let [a, b] = expect_ptrs!(store, 2, *idx); - let a = self.populate_with(&a, store, cache); - let b = self.populate_with(&b, store, cache); - let z_ptr = ZPtr::from_parts( - *tag, - store.poseidon_cache.hash4(&[ - a.tag_field(), - *a.value(), - b.tag_field(), - *b.value(), - ]), - ); - self.0.insert(z_ptr, ZPtrType::Tuple2(a, b)); - z_ptr + if let Tag::Expr(Env) = tag { + let [sym_pay, val_tag, val_pay, env_pay] = store.expect_raw_ptrs(*idx); + let sym = Ptr::new(Tag::Expr(Sym), *sym_pay); + let val = Ptr::new( + store.fetch_tag(val_tag).expect("Couldn't fetch tag"), + *val_pay, + ); + let env = Ptr::new(Tag::Expr(Env), *env_pay); + let sym = self.populate_with(&sym, store, cache); + let val = self.populate_with(&val, store, cache); + let env = self.populate_with(&env, store, cache); + let z_ptr = ZPtr::from_parts( + *tag, + store.poseidon_cache.hash4(&[ + *sym.value(), + val.tag_field(), + *val.value(), + *env.value(), + ]), + ); + self.0.insert(z_ptr, ZPtrType::Env(sym, val, env)); + z_ptr + } else { + let [a, b] = expect_ptrs!(store, 2, *idx); + let a = self.populate_with(&a, store, cache); + let b = self.populate_with(&b, store, cache); + let z_ptr = ZPtr::from_parts( + *tag, + store.poseidon_cache.hash4(&[ + a.tag_field(), + *a.value(), + b.tag_field(), + *b.value(), + ]), + ); + self.0.insert(z_ptr, ZPtrType::Tuple2(a, b)); + z_ptr + } } RawPtr::Hash6(idx) => { let [a, b, c] = expect_ptrs!(store, 3, *idx); @@ -146,6 +173,18 @@ impl ZDag { let ptr4 = self.populate_store(z4, store, cache)?; intern_ptrs_hydrated!(store, *z_ptr.tag(), *z_ptr, ptr1, ptr2, ptr3, ptr4) } + Some(ZPtrType::Env(sym, val, env)) => { + let sym = self.populate_store(sym, store, cache)?; + let val = self.populate_store(val, store, cache)?; + let env = self.populate_store(env, store, cache)?; + let raw = store.intern_raw_ptrs([ + *sym.raw(), + store.tag(*val.tag()), + *val.raw(), + *env.raw(), + ]); + Ptr::new(Tag::Expr(Env), raw) + } }; cache.insert(*z_ptr, ptr); Ok(ptr) @@ -187,6 +226,12 @@ impl ZDag { self.populate_z_dag(z4, z_dag, cache)?; z_dag.0.insert(*z_ptr, ZPtrType::Tuple4(*z1, *z2, *z3, *z4)); } + Some(ZPtrType::Env(sym, val, env)) => { + self.populate_z_dag(sym, z_dag, cache)?; + self.populate_z_dag(val, z_dag, cache)?; + self.populate_z_dag(env, z_dag, cache)?; + z_dag.0.insert(*z_ptr, ZPtrType::Env(*sym, *val, *env)); + } }; cache.insert(*z_ptr); } From 7c86bca55ad842d49ba69933d9d4eace84456b74 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 9 Jan 2024 13:52:06 -0300 Subject: [PATCH 11/14] fixed demo, except for protocol.lurk --- demo/bank.lurk | 16 ++++++++-------- demo/chained-functional-commitment.lurk | 12 ++++++------ demo/functional-commitment.lurk | 8 ++++---- demo/vdf.lurk | 2 +- 4 files changed, 19 insertions(+), 19 deletions(-) diff --git a/demo/bank.lurk b/demo/bank.lurk index 6fabcd133d..97d8788cc6 100644 --- a/demo/bank.lurk +++ b/demo/bank.lurk @@ -192,7 +192,7 @@ ledger2 ;; Now we can open the committed ledger transfer function on a transaction. -!(call 0x3be53fdb5946af9449e4f7063fd8d60a6acc7ccdea8da8b575facedcb2b1291d '(1 0 2)) +!(call 0x348a2e97903fff808be52461d19c3192b6868830598be397b361a21bfc8a45f9 '(1 0 2)) ;; And the record reflects that Church sent one unit to Satoshi. @@ -202,7 +202,7 @@ ledger2 ;; We can verify the proof.. -!(verify "Nova_Pallas_10_0bac4e49ef06a34fd1a6a18d6d7bff8770e6acbf6a4624783af29ad8cd780b14") +!(verify "Nova_Pallas_10_398a87b5f99157b86abde88a67754791f72fed93ccd8db68d693bc9f7e26738c") ;; Unfortunately, this functional commitment doesn't let us maintain state. ;; Let's turn our single-transaction function into a chained function. @@ -219,24 +219,24 @@ ledger2 ;; Now we can transfer one unit from Church to Satoshi like before. -!(chain 0x01ad5587273aed89dca2527f7a9a235e1ee74ba2519d39adc7b4c521c66f9dbb '(1 0 2)) +!(chain 0x0e484bf02f72ad529ebb9ded8fc2f4c2b1519a758e0f0238973bf0cd8dd97f72 '(1 0 2)) !(prove) -!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a") +!(verify "Nova_Pallas_10_11df37aff14b2fc8c1fea85fcc07ebececa4ef3e974764c73c49a2ce64eeb8f1") ;; Then we can transfer 5 more, proceeding from the new head of the chain. -!(chain 0x07172fda01948387c25038beb5738a12bf88cfb3317180cf5894319c16276c78 '(5 0 2)) +!(chain 0x3cb56c66573d29a478b62ff6d59df557dd2e6a924ff408644e61e31c3847a9cd '(5 0 2)) !(prove) -!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a") +!(verify "Nova_Pallas_10_3541178de43221c6d12f82ff6da37807971079d11ced58e3564ba2f34e77cfc4") ;; And once more, this time we'll transfer 20 from Turing to Church. -!(chain 0x261e0afd81be78f88bc638c79d6530f341517ff5fdb368e575407bd701c712cc '(20 1 0)) +!(chain 0x38172b9b6212b557d94b9896ea569e77fa35ac979700bedcc97f711322169905 '(20 1 0)) !(prove) -!(verify "Nova_Pallas_10_2d3c73be45dce3971cf9208a6ec538238fc4a01328342d2b3aa501e5709ea2c5") +!(verify "Nova_Pallas_10_2dd41df4b593c4f8b4a0a058d94b8dbcded8343f829d1aaf2765f0b8e0eda03b") diff --git a/demo/chained-functional-commitment.lurk b/demo/chained-functional-commitment.lurk index 86ce3510ec..0eff5e57e1 100644 --- a/demo/chained-functional-commitment.lurk +++ b/demo/chained-functional-commitment.lurk @@ -9,7 +9,7 @@ ;; We chain a next commitment by applying the committed function to a value of 9. -!(chain 0x07978f48203798156497b7fdef995301644c10b16de71c98a9c3c5d5c80e5cb9 9) +!(chain 0x3e47de9fb674019306d566345ab360d92f955e29e015432b10ecb58476f42f01 9) ;; The new counter value is 9, and the function returns a new functional commitment. @@ -21,11 +21,11 @@ ;; We can verify the proof. -!(verify "Nova_Pallas_10_29077a93c626166dfe527acb4665eeaa0a2945965db1d984d111fdb04d7f6cb4") +!(verify "Nova_Pallas_10_1b894ae4e13a74970afb9ff982fd0e9c4dc439a8317ac85eeaf97ab6c3d8f35e") ;; Now let's chain another call to the new head, adding 12 to the counter. -!(chain 0x09d46102bcc9faaf2d8dbfabe72b5142a1788538129e4826e0e30015f594e035 12) +!(chain 0x17165f98bc83b64b47c4e030ae621c94edcb10cc3bd68e9dcc5c796283bda34c 12) ;; Now the counter is 21, and we have a new head commitment. @@ -35,11 +35,11 @@ ;; And verify. -!(verify "Nova_Pallas_10_18beccbc88887d27b074b782525d2c3d5cfafb7f553877513b167b8bb45017e4") +!(verify "Nova_Pallas_10_29a1a6b7ceca05a40f92883dc7d3c11dd8e7cca698665bc7a9faaaa96cdde96a") ;; One more time, we'll add 14 to the head commitment's internal state. -!(chain 0x3b0ed1000667da8ce73779a52e4dfe17638f359fcb77f0aad1a6322c1fcef599 14) +!(chain 0x2c4c9d86f79bb575a1427ead9c14cb5226b79a6339dd1f8f8dc00354da677bfa 14) ;; 21 + 14 = 35, as expected. @@ -49,7 +49,7 @@ ;; Verify. -!(verify "Nova_Pallas_10_034258d4a0c61bc5fff43cc2e912a88f341abca00c4149c0ed85ab02b33d45dc") +!(verify "Nova_Pallas_10_13f092af20ac415822a0528d41e5c1f5565bfa6d0ec376445e677f411eb3ddd4") ;; Repeat indefinitely. diff --git a/demo/functional-commitment.lurk b/demo/functional-commitment.lurk index 61edde7c18..17b5d2cb65 100644 --- a/demo/functional-commitment.lurk +++ b/demo/functional-commitment.lurk @@ -10,7 +10,7 @@ ;; We open the functional commitment on input 5: Evaluate f(5). -!(call 0x3636a3820b53c834ce46a2d608c3b732681ccbc343b5154862f11f989d1a41e5 5) +!(call 0x05adecdb07d3d8d4a9d8027c163a70ef66c18ec311abc8381c2df92c58e216b5 5) ;; We can prove the functional-commitment opening. @@ -18,12 +18,12 @@ ;; We can inspect the input/output expressions of the proof. -!(inspect "Nova_Pallas_10_2f90a649f3a2a7861fdf6499309edc0c8e72b61ff3f40f2a11bd027749df4b04") +!(inspect "Nova_Pallas_10_1c3654a2491282df9c31cba2d104649a496b3d1bac4bb5352004a21c94554027") ;; Or the full proof claim -!(inspect-full "Nova_Pallas_10_2f90a649f3a2a7861fdf6499309edc0c8e72b61ff3f40f2a11bd027749df4b04") +!(inspect-full "Nova_Pallas_10_1c3654a2491282df9c31cba2d104649a496b3d1bac4bb5352004a21c94554027") ;; Finally, and most importantly, we can verify the proof. -!(verify "Nova_Pallas_10_2f90a649f3a2a7861fdf6499309edc0c8e72b61ff3f40f2a11bd027749df4b04") +!(verify "Nova_Pallas_10_1c3654a2491282df9c31cba2d104649a496b3d1bac4bb5352004a21c94554027") diff --git a/demo/vdf.lurk b/demo/vdf.lurk index f339e8000e..b601c93299 100644 --- a/demo/vdf.lurk +++ b/demo/vdf.lurk @@ -51,7 +51,7 @@ !(prove) -!(verify "Nova_Pallas_10_04ebf402c8345327dbb271b393325f4d360372784e4d1e625e707235a8736dad") +!(verify "Nova_Pallas_10_3d385361e08449cad361ccbe45d4c41685bcee7ece87b33c47b8953309002f64") !(def timelock-encrypt (lambda (secret-key plaintext rounds) (let ((ciphertext (+ secret-key plaintext)) From 0d059380b324e0620b00169a7579ddb7b8866d99 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 9 Jan 2024 16:21:35 -0300 Subject: [PATCH 12/14] added empty-env operation and fixed protocol.lurk --- demo/protocol.lurk | 2 +- src/lem/eval.rs | 13 +++++++++++-- src/state.rs | 3 ++- 3 files changed, 14 insertions(+), 4 deletions(-) diff --git a/demo/protocol.lurk b/demo/protocol.lurk index 6b33779dca..0860517a4b 100644 --- a/demo/protocol.lurk +++ b/demo/protocol.lurk @@ -6,7 +6,7 @@ (mk-open-expr (lambda (hash) (cons 'open (cons hash nil))))) (cons (if (= (+ (car pair) (cdr pair)) 30) - (list6 (mk-open-expr hash) nil :outermost pair nil :terminal) + (list6 (mk-open-expr hash) (empty-env) :outermost pair (empty-env) :terminal) nil) (lambda () (> (car pair) 10)))) :rc 10 diff --git a/src/lem/eval.rs b/src/lem/eval.rs index c6a03491bc..a9c11e705e 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -1034,6 +1034,15 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let cont: Cont::If = cons4(more, env, cont, foo); return (condition, env, cont, ret) } + "empty-env" => { + match rest.tag { + Expr::Nil => { + let empty_env: Expr::Env; + return (empty_env, env, cont, apply) + } + }; + return (expr, env, err, errctrl) + } "current-env" => { match rest.tag { Expr::Nil => { @@ -1730,8 +1739,8 @@ mod tests { expect_eq(func.slots_count.commitment, expect!["1"]); expect_eq(func.slots_count.bit_decomp, expect!["3"]); expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["8938"]); - expect_eq(cs.num_constraints(), expect!["10897"]); + expect_eq(cs.aux().len(), expect!["8943"]); + expect_eq(cs.num_constraints(), expect!["10921"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } } diff --git a/src/state.rs b/src/state.rs index 1eef65c247..45c6c37b53 100644 --- a/src/state.rs +++ b/src/state.rs @@ -215,7 +215,7 @@ const LURK_PACKAGE_SYMBOL_NAME: &str = "lurk"; const USER_PACKAGE_SYMBOL_NAME: &str = "user"; const META_PACKAGE_SYMBOL_NAME: &str = "meta"; -const LURK_PACKAGE_SYMBOLS_NAMES: [&str; 35] = [ +const LURK_PACKAGE_SYMBOLS_NAMES: [&str; 36] = [ "atom", "begin", "car", @@ -226,6 +226,7 @@ const LURK_PACKAGE_SYMBOLS_NAMES: [&str; 35] = [ "cons", "current-env", "emit", + "empty-env", "eval", "eq", "hide", From e5779dc2fab17c4ff774dcc166c1105b48f595e5 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 9 Jan 2024 21:55:31 -0300 Subject: [PATCH 13/14] fixed cli test --- tests/lurk-cli-tests.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lurk-cli-tests.rs b/tests/lurk-cli-tests.rs index d025b19c5f..2a01c0810b 100644 --- a/tests/lurk-cli-tests.rs +++ b/tests/lurk-cli-tests.rs @@ -55,7 +55,7 @@ fn test_prove_and_verify() { let mut file = File::create(lurk_file.clone()).unwrap(); file.write_all(b"!(prove (+ 1 1))\n").unwrap(); - file.write_all(b"!(verify \"Nova_Pallas_10_3f2526abf20fc9006dd93c0d3ff49954ef070ef52d2e88426974de42cc27bdb2\")\n").unwrap(); + file.write_all(b"!(verify \"Nova_Pallas_10_090cee5a184bc9b76a965e59b87cd1a1eac30c2b0f243e7ee0232e51d14ebbf6\")\n").unwrap(); let mut cmd = lurk_cmd(); cmd.env("LURK_PERF", "max-parallel-simple"); From 55b5baa00602e138b3ec57965635905ca292ec43 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 11 Jan 2024 17:35:24 -0300 Subject: [PATCH 14/14] slightly more efficient lookup --- src/lem/eval.rs | 50 +++++++++++++++++++++++++++---------------------- 1 file changed, 28 insertions(+), 22 deletions(-) diff --git a/src/lem/eval.rs b/src/lem/eval.rs index a9c11e705e..ff44e14660 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -802,25 +802,25 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (nil) }); let is_cproc = is_cproc(cprocs); - let lookup = func!(lookup(expr, env, state, maybe_var): 4 => { + let lookup = func!(lookup(expr, env, state): 3 => { let found = Symbol("found"); let not_found = Symbol("not_found"); let error = Symbol("error"); let continue = eq_val(not_found, state); if !continue { - return (expr, env, state, maybe_var) + return (expr, env, state) } let zero = Num(0); let env_is_zero = eq_val(env, zero); if env_is_zero { - return (expr, env, error, maybe_var) + return (expr, env, error) } let (var, val, smaller_env) = pop_binding(env); let eq_val = eq_val(var, expr); if eq_val { - return (val, env, found, var) + return (val, env, found) } - return (expr, smaller_env, not_found, var) + return (expr, smaller_env, not_found) }); func!(reduce(expr, env, cont): 4 => { @@ -869,33 +869,39 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (expr, env, cont, apply) } let not_found = Symbol("not_found"); - let zero = Num(0); - let (expr, env, state, var) = lookup(expr, env, not_found, zero); - let (expr, env, state, var) = lookup(expr, env, state, var); - let (expr, env, state, var) = lookup(expr, env, state, var); - let (expr, env, state, var) = lookup(expr, env, state, var); - let (expr, env, state, var) = lookup(expr, env, state, var); - let (expr, env, state, var) = lookup(expr, env, state, var); - let (expr, env, state, var) = lookup(expr, env, state, var); - let (expr, env, state, var) = lookup(expr, env, state, var); + // `expr` is the symbol. If the lookup was succesful, it will + // return the result as `res` and a "found" state. If the lookup + // is incomplete, it will return the original symbol as `res` + // and a "not_found" state + let (res, res_env, state) = lookup(expr, env, not_found); + let (res, res_env, state) = lookup(res, res_env, state); + let (res, res_env, state) = lookup(res, res_env, state); + let (res, res_env, state) = lookup(res, res_env, state); + let (res, res_env, state) = lookup(res, res_env, state); + let (res, res_env, state) = lookup(res, res_env, state); + let (res, res_env, state) = lookup(res, res_env, state); + let (res, res_env, state) = lookup(res, res_env, state); match symbol state { "error" => { return (expr, env, err, errctrl) } "found" => { - match expr.tag { + match res.tag { // if `val2` is a recursive closure, then extend its environment Expr::Rec => { - let (args, body, closed_env, _foo) = decons4(expr); - let extended = push_binding(var, expr, closed_env); + let (args, body, closed_env, _foo) = decons4(res); + // remember `expr` is the original symbol, i.e. the symbol + // of the recursive closure + let extended = push_binding(expr, res, closed_env); let fun: Expr::Fun = cons4(args, body, extended, foo); - return (fun, env, cont, apply) + return (fun, res_env, cont, apply) } }; - return (expr, env, cont, apply) + return (res, res_env, cont, apply) } "not_found" => { - return (expr, env, cont, ret) + // if it's not yet found, we must keep reducing + return (res, res_env, cont, ret) } } } @@ -1739,8 +1745,8 @@ mod tests { expect_eq(func.slots_count.commitment, expect!["1"]); expect_eq(func.slots_count.bit_decomp, expect!["3"]); expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["8943"]); - expect_eq(cs.num_constraints(), expect!["10921"]); + expect_eq(cs.aux().len(), expect!["8927"]); + expect_eq(cs.num_constraints(), expect!["10857"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } }