Multiple lookups, simpler rec environment (#996)

* two lookups per step

* let/letrec refactor

* recursive enviroments simplified

* fixed eval/proof iterations

* New tag for recursive variables

* fixed lurk-lib and demo tests

benches/common/fib.rs

@@ -23,7 +23,7 @@ pub(crate) fn fib_expr<F: LurkField>(store: &Store<F>) -> Ptr {
 }
 
 const LIN_COEF: usize = 7;
-const ANG_COEF: usize = 10;
+const ANG_COEF: usize = 7;
 
 // The env output in the `fib_frame`th frame of the above, infinite Fibonacci computation contains a binding of the
 // nth Fibonacci number to `a`.

demo/bank.lurk

@@ -192,7 +192,7 @@ ledger2
 
 ;; Now we can open the committed ledger transfer function on a transaction.
 
-!(call 0x30ee7657cfa11c0dc69160195540297c50176a27baf2b407d6bf16d6284abaea '(1 0 2))
+!(call 0x3be53fdb5946af9449e4f7063fd8d60a6acc7ccdea8da8b575facedcb2b1291d '(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_39457589f3ffd148aadaba23819641cdd914ab291a3c77d20dcb65f757c08925")
+!(verify "Nova_Pallas_10_0bac4e49ef06a34fd1a6a18d6d7bff8770e6acbf6a4624783af29ad8cd780b14")
 
 ;; 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 0x1aaf63ef4f853b935df9aad04424e0a8ba1e5bfd7220e5de842eca9d6e608f36 '(1 0 2))
+!(chain 0x01ad5587273aed89dca2527f7a9a235e1ee74ba2519d39adc7b4c521c66f9dbb '(1 0 2))
 
 !(prove)
 
-!(verify "Nova_Pallas_10_27cf734c3a663d0c09a62e4150fe4813ebd7db2fb038589facd7e48ba6c76e1e")
+!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a")
 
 ;; Then we can transfer 5 more, proceeding from the new head of the chain.
 
-!(chain 0x242e4fb1434ce1f6b4a19d8e96651e36ca5f7daa2fa2796f6f5924f66c35cd31 '(5 0 2))
+!(chain 0x07172fda01948387c25038beb5738a12bf88cfb3317180cf5894319c16276c78 '(5 0 2))
 
 !(prove)
 
-!(verify "Nova_Pallas_10_14a98bfb5ee8451accb717eca8dadaaeb1c21f95e7890d53bcd733b73224e0fc")
+!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a")
 
 ;; And once more, this time we'll transfer 20 from Turing to Church.
 
-!(chain 0x0f7247de19a2f52890cb4f165aaebe40934c09cc3466ab9ce2e03a8c21a32c7a '(20 1 0))
+!(chain 0x261e0afd81be78f88bc638c79d6530f341517ff5fdb368e575407bd701c712cc '(20 1 0))
 
 !(prove)
 
-!(verify "Nova_Pallas_10_21832c545de0ab0111c9006728ab9a1d4550d044b21c73f3076f60256a732db9")
+!(verify "Nova_Pallas_10_2d3c73be45dce3971cf9208a6ec538238fc4a01328342d2b3aa501e5709ea2c5")

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 0x14cb06e2d3c594af90d5b670e73595791d7462b20442c24cd56ba2919947d769 9)
+!(chain 0x07978f48203798156497b7fdef995301644c10b16de71c98a9c3c5d5c80e5cb9 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_38f55f6f5c92197e331c92971ba13514f621cf1e0de66133574fe3c1d2d71114")
+!(verify "Nova_Pallas_10_29077a93c626166dfe527acb4665eeaa0a2945965db1d984d111fdb04d7f6cb4")
 
 ;; Now let's chain another call to the new head, adding 12 to the counter.
 
-!(chain 0x26f9a6e61ea91163545a0472304d5ad42825ce1f6873ea10301e26dfd84f3ea6 12)
+!(chain 0x09d46102bcc9faaf2d8dbfabe72b5142a1788538129e4826e0e30015f594e035 12)
 
 ;; Now the counter is 21, and we have a new head commitment.
 
@@ -35,11 +35,11 @@
 
 ;; And verify.
 
-!(verify "Nova_Pallas_10_141e90709e746411b9d0b3557758fe7543aafc33ed9cc25ee22606adab7d8e6f")
+!(verify "Nova_Pallas_10_18beccbc88887d27b074b782525d2c3d5cfafb7f553877513b167b8bb45017e4")
 
 ;; One more time, we'll add 14 to the head commitment's internal state.
 
-!(chain 0x2adacaf2ae7983d45e6855fa6c6577e73ca4657c33e45286cbfb8e44d68e351c 14)
+!(chain 0x3b0ed1000667da8ce73779a52e4dfe17638f359fcb77f0aad1a6322c1fcef599 14)
 
 ;; 21 + 14 = 35, as expected.
 
@@ -49,7 +49,7 @@
 
 ;; Verify.
 
-!(verify "Nova_Pallas_10_3fe9b0d562d982f0614cb96e4cbb88f56733442524f6c42a29ef8cf5ab8a6c7e")
+!(verify "Nova_Pallas_10_034258d4a0c61bc5fff43cc2e912a88f341abca00c4149c0ed85ab02b33d45dc")
 
 ;; Repeat indefinitely.
 

demo/vdf.lurk

@@ -51,7 +51,7 @@
 
 !(prove)
 
-!(verify "Nova_Pallas_10_1955d9399a7174ffb6ecd9b558e260c746e42456018246335de9c22811282119")
+!(verify "Nova_Pallas_10_04ebf402c8345327dbb271b393325f4d360372784e4d1e625e707235a8736dad")
 
 !(def timelock-encrypt (lambda (secret-key plaintext rounds)
                           (let ((ciphertext (+ secret-key plaintext))

src/lem/eval.rs

@@ -660,15 +660,6 @@ fn match_and_run_cproc(cprocs: &[(&Symbol, usize)]) -> Func {
 fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
     // Auxiliary functions
     let car_cdr = car_cdr();
-    let env_to_use = func!(env_to_use(smaller_env, smaller_rec_env): 1 => {
-        match smaller_rec_env.tag {
-            Expr::Nil => {
-                return (smaller_env)
-            }
-        };
-        let env: Expr::Cons = cons2(smaller_rec_env, smaller_env);
-        return (env)
-    });
     let expand_bindings = func!(expand_bindings(head, body, body1, rest_bindings): 1 => {
         match rest_bindings.tag {
             Expr::Nil => {
@@ -679,18 +670,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
         let expanded: Expr::Cons = cons2(head, expanded_0);
         return (expanded)
     });
-    let choose_let_cont = func!(choose_let_cont(head, var, env, expanded, cont): 1 => {
-        match symbol head {
-            "let" => {
-                let cont: Cont::Let = cons4(var, env, expanded, cont);
-                return (cont)
-            }
-            "letrec" => {
-                let cont: Cont::LetRec = cons4(var, env, expanded, cont);
-                return (cont)
-            }
-        }
-    });
     let get_unop = func!(get_unop(head): 1 => {
         let nil = Symbol("nil");
         let nil = cast(nil, Expr::Nil);
@@ -823,6 +802,45 @@ 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 not_found = Symbol("not_found");
+        let continue = eq_val(not_found, found);
+        if !continue {
+            return (expr, env, found, binding)
+        }
+        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, 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 (expr, smaller_env, not_found, binding)
+            }
+        };
+        return (expr, env, error, binding)
+    });
 
     func!(reduce(expr, env, cont): 4 => {
         let ret = Symbol("return");
@@ -869,53 +887,34 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
                 if expr_is_nil_or_t {
                     return (expr, env, cont, apply)
                 }
-
-                match env.tag {
-                    Expr::Nil => {
+                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 {
+                    "error" => {
                         return (expr, env, err, errctrl)
                     }
-                };
-
-                let (binding, smaller_env) = car_cdr(env);
-                match binding.tag {
-                    Expr::Nil => {
-                        return (expr, env, err, errctrl)
+                    "non_rec" => {
+                        return (expr, env, cont, apply)
                     }
-                };
-
-                let (var_or_rec_binding, val_or_more_rec_env) =
-                    car_cdr(binding);
-                match var_or_rec_binding.tag {
-                    Expr::Sym => {
-                        let eq_val = eq_val(var_or_rec_binding, expr);
-                        if eq_val {
-                            return (val_or_more_rec_env, env, cont, apply)
-                        }
-                        return (expr, smaller_env, cont, ret)
+                    "rec" => {
+                        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)
+                            }
+                        };
+                        return (expr, env, cont, apply)
                     }
-                    Expr::Cons => {
-                        let (v2, val2) = decons2(var_or_rec_binding);
-
-                        let eq_val = eq_val(v2, expr);
-                        if eq_val {
-                            match val2.tag {
-                                Expr::Fun => {
-                                    // if `val2` is a closure, then extend its environment
-                                    let (arg, body, closed_env, _foo) = decons4(val2);
-                                    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)
-                                }
-                            };
-                            // otherwise return `val2`
-                            return (val2, env, cont, apply)
-                        }
-                        let (env_to_use) = env_to_use(smaller_env, val_or_more_rec_env);
-                        return (expr, env_to_use, cont, ret)
+                    "not_found" => {
+                        return (expr, env, cont, ret)
                     }
-                };
-                return (expr, env, err, errctrl)
+                }
             }
             Expr::Cons => {
                 // No need for `car_cdr` since the expression is already a `Cons`
@@ -955,14 +954,17 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
                                     match var.tag {
                                         Expr::Sym => {
                                             let (val, end) = car_cdr(vals);
-                                            match end.tag {
-                                                Expr::Nil => {
-                                                    let (expanded) = expand_bindings(head, body, body1, rest_bindings);
-                                                    let (cont) = choose_let_cont(head, var, env, expanded, cont);
-                                                    return (val, env, cont, ret)
-                                                }
-                                            };
-                                            return (expr, env, err, errctrl)
+                                            let end_is_nil = eq_tag(end, nil);
+                                            if !end_is_nil {
+                                                return (expr, env, err, errctrl)
+                                            }
+                                            let (expanded) = expand_bindings(head, body, body1, rest_bindings);
+                                            if head_is_let_sym {
+                                                let cont: Cont::Let = cons4(var, env, expanded, cont);
+                                                return (val, env, cont, ret)
+                                            }
+                                            let cont: Cont::LetRec = cons4(var, env, expanded, cont);
+                                            return (val, env, cont, ret)
                                         }
                                     };
                                     return (expr, env, err, errctrl)
@@ -1153,27 +1155,6 @@ fn choose_cproc_call(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func {
 
 fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func {
     let car_cdr = car_cdr();
-    let extend_rec = func!(extend_rec(env, var, result): 1 => {
-        let nil = Symbol("nil");
-        let nil = cast(nil, Expr::Nil);
-        let sym: Expr::Sym;
-        let (binding_or_env, rest) = car_cdr(env);
-        let (var_or_binding, _val_or_more_bindings) = car_cdr(binding_or_env);
-        let binding: Expr::Cons = cons2(var, result);
-        let var_or_binding_is_sym = eq_tag(var_or_binding, sym);
-        let var_or_binding_is_nil = eq_tag(var_or_binding, nil);
-        let var_or_binding_is_sym_or_nil = or(var_or_binding_is_sym, var_or_binding_is_nil);
-        if var_or_binding_is_sym_or_nil {
-            // It's a var, so we are extending a simple env with a recursive env.
-            let list: Expr::Cons = cons2(binding, nil);
-            let res: Expr::Cons = cons2(list, env);
-            return (res)
-        }
-        // It's a binding, so we are extending a recursive env.
-        let cons2: Expr::Cons = cons2(binding, binding_or_env);
-        let res: Expr::Cons = cons2(cons2, rest);
-        return (res)
-    });
     // Returns 0u64 if both arguments are U64, 0 (num) if the arguments are some kind of number (either U64 or Num),
     // and nil otherwise
     let args_num_type = func!(args_num_type(arg1, arg2): 1 => {
@@ -1317,7 +1298,10 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func {
                     }
                     Cont::LetRec => {
                         let (var, saved_env, body, cont) = decons4(cont);
-                        let (extended_env) = extend_rec(saved_env, var, result);
+                        // 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)
                     }
                     Cont::Unop => {
@@ -1761,8 +1745,8 @@ mod tests {
             expected.assert_eq(&computed.to_string());
         };
         expect_eq(cs.num_inputs(), expect!["1"]);
-        expect_eq(cs.aux().len(), expect!["8823"]);
-        expect_eq(cs.num_constraints(), expect!["10628"]);
+        expect_eq(cs.aux().len(), expect!["8884"]);
+        expect_eq(cs.num_constraints(), expect!["10831"]);
         assert_eq!(func.num_constraints(&store), cs.num_constraints());
     }
 }

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, Fun, Key, Nil, Num, RecVar, Str, Sym, Thunk, U64},
 };
 
 use super::pointers::{Ptr, RawPtr, ZPtr};
@@ -1004,6 +1004,13 @@ impl Ptr {
                         "<Opaque Sym>".into()
                     }
                 }
+                RecVar => {
+                    if let Some(sym) = store.fetch_sym(&self.cast(Tag::Expr(Sym))) {
+                        state.fmt_to_string(&sym.into())
+                    } else {
+                        "<Opaque RecVar>".into()
+                    }
+                }
                 Key => {
                     if let Some(key) = store.fetch_key(self) {
                         state.fmt_to_string(&key.into())