Skip to content

Commit

Permalink
Multiple lookups, simpler rec environment (argumentcomputer#996)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@gabriel-barrett
gabriel-barrett committed Jan 10, 2024
1 parent 753bf71 commit 13850b2
Show file tree
Hide file tree
Showing 10 changed files with 173 additions and 180 deletions.
2 changes: 1 addition & 1 deletion benches/common/fib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
16 changes: 8 additions & 8 deletions demo/bank.lurk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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.
Expand All @@ -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")
12 changes: 6 additions & 6 deletions demo/chained-functional-commitment.lurk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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.

Expand All @@ -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.

Expand All @@ -49,7 +49,7 @@

;; Verify.

!(verify "Nova_Pallas_10_3fe9b0d562d982f0614cb96e4cbb88f56733442524f6c42a29ef8cf5ab8a6c7e")
!(verify "Nova_Pallas_10_034258d4a0c61bc5fff43cc2e912a88f341abca00c4149c0ed85ab02b33d45dc")

;; Repeat indefinitely.

Expand Down
2 changes: 1 addition & 1 deletion demo/vdf.lurk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
2 changes: 1 addition & 1 deletion lurk-lib
Submodule lurk-lib updated from 6c9bfb to 845c7f
174 changes: 79 additions & 95 deletions src/lem/eval.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 => {
Expand All @@ -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);
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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`
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 => {
Expand Down Expand Up @@ -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 => {
Expand Down Expand Up @@ -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());
}
}
9 changes: 8 additions & 1 deletion src/lem/store.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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())
Expand Down
Loading

0 comments on commit 13850b2

Please sign in to comment.