Skip to content

Commit

Permalink
chore: enable calls with comms and nums (#1163)
Browse files Browse the repository at this point in the history 
* exclude tests that can no longer be satisfied due to this change
* adapt `test_prove_head_with_sym_mimicking_value`
  • Loading branch information
@arthurpaulino
arthurpaulino authored Feb 22, 2024
1 parent 1df2666 commit 2837dfd
Show file tree
Hide file tree
Showing 5 changed files with 197 additions and 143 deletions.
2 changes: 1 addition & 1 deletion lurk-lib
Submodule lurk-lib updated from 845c7f to a4b187
33 changes: 25 additions & 8 deletions src/lem/eval.rs
View file
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());
}
}
112 changes: 95 additions & 17 deletions src/lem/tests/eval_tests.rs
View file
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 Expand Up @@ -1195,13 +1290,6 @@ fn evaluate_zero_arg_lambda_variants() {
let error = s.cont_error();
test_aux::<Coproc<Fr>>(s, expr, None, None, Some(error), None, &expect!["2"], &None);
}
{
let s = &Store::<Fr>::default();
let expr = "(123)";

let error = s.cont_error();
test_aux::<Coproc<Fr>>(s, expr, None, None, Some(error), None, &expect!["1"], &None);
}
}

#[test]
Expand Down Expand Up @@ -3383,16 +3471,6 @@ fn test_eval_quote_error() {
let s = &Store::<Fr>::default();
let error = s.cont_error();

test_aux::<Coproc<Fr>>(
s,
"(1)",
None,
None,
Some(error),
None,
&expect!["1"],
&None,
);
test_aux::<Coproc<Fr>>(
s,
"(quote . 1)",
Expand Down
55 changes: 55 additions & 0 deletions src/proof/tests/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,33 @@ fn test_aux<F: CurveCycleEquipped, C: Coprocessor<F>>(
}
}

fn test_aux_ptr<F: CurveCycleEquipped, C: Coprocessor<F>>(
s: &Store<F>,
expr: Ptr,
expected_result: Option<Ptr>,
expected_env: Option<Ptr>,
expected_cont: Option<Ptr>,
expected_emitted: Option<&[Ptr]>,
expected_iterations: &Expect,
lang: &Option<Arc<Lang<F, C>>>,
) {
for chunk_size in REDUCTION_COUNTS_TO_TEST {
nova_test_full_aux_ptr::<F, C>(
s,
expr,
expected_result,
expected_env,
expected_cont,
expected_emitted,
expected_iterations,
chunk_size,
false,
None,
lang,
)
}
}

fn nova_test_full_aux<F: CurveCycleEquipped, C: Coprocessor<F>>(
s: &Store<F>,
expr: &str,
Expand All @@ -75,6 +102,34 @@ fn nova_test_full_aux<F: CurveCycleEquipped, C: Coprocessor<F>>(
) {
let expr = EvaluationStore::read(s, expr).unwrap();

nova_test_full_aux_ptr(
s,
expr,
expected_result,
expected_env,
expected_cont,
expected_emitted,
expected_iterations,
reduction_count,
check_nova,
limit,
lang,
);
}

fn nova_test_full_aux_ptr<F: CurveCycleEquipped, C: Coprocessor<F>>(
s: &Store<F>,
expr: Ptr,
expected_result: Option<Ptr>,
expected_env: Option<Ptr>,
expected_cont: Option<Ptr>,
expected_emitted: Option<&[Ptr]>,
expected_iterations: &Expect,
reduction_count: usize,
check_nova: bool,
limit: Option<usize>,
lang: &Option<Arc<Lang<F, C>>>,
) {
let f = |l| {
nova_test_full_aux2::<F, C>(
s,
Expand Down
Loading

0 comments on commit 2837dfd

Please sign in to comment.