Skip to content

Commit

Permalink
chore: enable calls with comms and nums
Browse files Browse the repository at this point in the history
  • Loading branch information
arthurpaulino committed Feb 21, 2024
1 parent ce2f33a commit 7a5078c
Show file tree
Hide file tree
Showing 3 changed files with 120 additions and 42 deletions.
33 changes: 25 additions & 8 deletions src/lem/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -788,11 +788,14 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func {
let fun: Expr::Fun;
let cons: Expr::Cons;
let thunk: Expr::Thunk;
let num: Expr::Num;
let head_is_fun = eq_tag(head, fun);
let head_is_cons = eq_tag(head, cons);
let head_is_thunk = eq_tag(head, thunk);
let head_is_num = eq_tag(head, num);
let acc = or(head_is_fun, head_is_cons);
let acc = or(acc, head_is_thunk);
let acc = or(acc, head_is_num);
if acc {
let t = Symbol("t");
return (t)
Expand Down Expand Up @@ -1188,6 +1191,19 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func {
};
return (nil)
});
let open_if_num_or_comm = aux_func!(open_if_num_or_comm(input): 1 => {
let num: Expr::Num;
let comm: Expr::Comm;
let input_is_num = eq_tag(input, num);
let input_is_comm = eq_tag(input, comm);
let input_is_num_or_comm = or(input_is_num, input_is_comm);
if input_is_num_or_comm {
let cast = cast(input, Expr::Comm);
let (_secret, payload) = open(cast);
return (payload)
}
return (input)
});
let choose_cproc_call = choose_cproc_call(cprocs, ivc);
aux_func!(apply_cont(result, env, cont, ctrl): 4 => {
match symbol ctrl {
Expand Down Expand Up @@ -1217,20 +1233,21 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func {
return (result, env, cont, makethunk)
}
Cont::Call => {
match result.tag {
let (fun) = open_if_num_or_comm(result);
match fun.tag {
Expr::Fun => {
let (args, args_env, continuation, _foo) = decons4(cont);
let (vars, body, fun_env, _foo) = decons4(result);
let (vars, body, fun_env, _foo) = decons4(fun);
match args.tag {
Expr::Cons => {
match vars.tag {
Expr::Nil => {
// Cannot apply non-zero number of arguments to a zero argument function
return (result, env, err, errctrl)
return (fun, env, err, errctrl)
}
Expr::Cons => {
let (arg, rest_args) = decons2(args);
let newer_cont: Cont::Call2 = cons4(result, rest_args, args_env, continuation);
let newer_cont: Cont::Call2 = cons4(fun, rest_args, args_env, continuation);
return (arg, args_env, newer_cont, ret)
}
}
Expand All @@ -1243,14 +1260,14 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func {
Expr::Cons => {
// TODO should we not fail here in an analogous way to the non-zero application
// on a zero argument function case?
return (result, env, continuation, ret)
return (fun, env, continuation, ret)
}
}
}
}
}
};
return (result, env, err, errctrl)
return (fun, env, err, errctrl)
}
Cont::Call2 => {
let (function, args, args_env, continuation) = decons4(cont);
Expand Down Expand Up @@ -1742,8 +1759,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!["9095"]);
expect_eq(cs.num_constraints(), expect!["11025"]);
expect_eq(cs.aux().len(), expect!["9107"]);
expect_eq(cs.num_constraints(), expect!["11044"]);
assert_eq!(func.num_constraints(&store), cs.num_constraints());
}
}
95 changes: 95 additions & 0 deletions src/lem/tests/eval_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -352,6 +352,101 @@ fn evaluate_lambda5() {
);
}

#[test]
fn evaluate_comm_callable() {
let s = &Store::<Fr>::default();
let expr = "((commit (lambda (x) x)) nil)";

let expected = s.intern_nil();
let terminal = s.cont_terminal();
test_aux::<Coproc<Fr>>(
s,
expr,
Some(expected),
None,
Some(terminal),
None,
&expect!["6"],
&None,
);
}

#[test]
fn evaluate_comm_callable2() {
let s = &Store::<Fr>::default();
let expr = "(begin (commit (lambda (x) x)) ((comm 0x2f31ee658b82c09daebbd2bd976c9d6669ad3bd6065056763797d5aaf4a3001b) nil))";

let expected = s.intern_nil();
let terminal = s.cont_terminal();
test_aux::<Coproc<Fr>>(
s,
expr,
Some(expected),
None,
Some(terminal),
None,
&expect!["10"],
&None,
);
}

#[test]
fn evaluate_num_callable() {
let s = &Store::<Fr>::default();
let expr = "((num (commit (lambda (x) x))) nil)";

let expected = s.intern_nil();
let terminal = s.cont_terminal();
test_aux::<Coproc<Fr>>(
s,
expr,
Some(expected),
None,
Some(terminal),
None,
&expect!["8"],
&None,
);
}

#[test]
fn evaluate_num_callable2() {
let s = &Store::<Fr>::default();
let expr = "(begin (commit (lambda (x) x)) (0x2f31ee658b82c09daebbd2bd976c9d6669ad3bd6065056763797d5aaf4a3001b nil))";

let expected = s.intern_nil();
let terminal = s.cont_terminal();
test_aux::<Coproc<Fr>>(
s,
expr,
Some(expected),
None,
Some(terminal),
None,
&expect!["8"],
&None,
);
}

#[test]
fn evaluate_num_callable3() {
let s = &Store::<Fr>::default();
let expr = "(begin (commit (lambda () nil)) (0x1b1eaa8d0e216957c90a9a1d55784f0d9a4f84918d5a898a1ca74e6260cfd1e7))";

let expected = s.intern_nil();
let terminal = s.cont_terminal();
test_aux::<Coproc<Fr>>(
s,
expr,
Some(expected),
None,
Some(terminal),
None,
&expect!["7"],
&None,
);
}

#[test]
fn evaluate_sum() {
let s = &Store::<Fr>::default();
Expand Down
34 changes: 0 additions & 34 deletions src/proof/tests/nova_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1579,40 +1579,6 @@ fn test_prove_zero_arg_lambda4() {
);
}

#[test]
fn test_prove_zero_arg_lambda5() {
let s = &Store::<Fr>::default();
let expected = s.read_with_default_state("(123)").unwrap();
let error = s.cont_error();
test_aux::<_, Coproc<_>>(
s,
"(123)",
Some(expected),
None,
Some(error),
None,
&expect!["1"],
&None,
);
}

#[test]
fn test_prove_zero_arg_lambda6() {
let s = &Store::<Fr>::default();
let expected = s.num_u64(123);
let error = s.cont_error();
test_aux::<_, Coproc<_>>(
s,
"((emit 123))",
Some(expected),
None,
Some(error),
None,
&expect!["5"],
&None,
);
}

#[test]
fn test_prove_nested_let_closure_regression() {
let s = &Store::<Fr>::default();
Expand Down

0 comments on commit 7a5078c

Please sign in to comment.