feat: implicit begin

Make the bodies of `let`, `letrec` and `lambda` behave as if there were an implicit `begin` wrapping the code after the binding variables. Important: this patch makes the body of every `Fun` object a `Cons` such that `(lambda (x) x)` actually prints to `<Fun (x) (x)>`.
argumentcomputer · Oct 2, 2024 · bab4982 · bab4982
1 parent 372c093
commit bab4982
Show file tree

Hide file tree

Showing 15 changed files with 106 additions and 70 deletions.
diff --git 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 #0x9726fe649c4ca7efde87888798594e3c4f238ac1eca58e13f8c2f8b8b0793 '(1 0 2))
+!(call #0x5bb923b0d7c38df129ae4e4684691bfcf3516b129dfa18d7ba5c72abaeac2a '(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 "40294916397e5ea423aa708c82bddfb49a33000fcd3b178e57d99c96797a40")
+!(verify "89bab6ac62462298d0c90fa2ac7893db838402b95fcc26ce08bec2f806edc2")
 
 ;; 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 #0x7a49523464e129d017831021202b79e32b2125a807219c0a81980504afb825 '(1 0 2))
+!(chain #0x4b799ce1a9ddfaec4cac1db4f18bdeab3a43bc85ce67dc92a3f8634c043b70 '(1 0 2))
 
 !(prove)
 
-!(verify "7569e1a5aed0ba2e1298c2379b156eceecf7ce8ece311d0bdee8dec030264e")
+!(verify "e0bd82989a93b89c5b04cfd25f87d07c029550f0719b97a67163086b538a0")
 
 ;; Then we can transfer 5 more, proceeding from the new head of the chain.
 
-!(chain #0xb70280e9be899a4940e4b6b5d69b56423b09d402e307e9a9714dbd4c6f8fe '(5 0 2))
+!(chain #0x7122f393651f0e55f01c6805da851dc922c3937ef6e203cbf62e477e055872 '(5 0 2))
 
 !(prove)
 
-!(verify "4c943c0128ed71de52cc9631a90cdb2fcbde595992c3f6b69c4391855ea192")
+!(verify "68f57a430b626cf271ec0cfeb65ad47d8e6d8b21b5ba321ccd1573f44f988b")
 
 ;; And once more, this time we'll transfer 20 from Turing to Church.
 
-!(chain #0x5e7d7af3f1a4cffa54402b98f20e0caf420c32c85b07618dceaebfe989540b '(20 1 0))
+!(chain #0x5a3723ae5a02d84826f1ad237337b231b55b598ff9167de3529d6280ca952a '(20 1 0))
 
 !(prove)
 
-!(verify "7e465b97b59c3ab8ada3b203971b15a4dff812304c3533450ab25f6b01405e")
+!(verify "53b291171280518b20811c64f207ede4343ca2eeec3886c28a6c5e3c838671")
diff --git 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 #0x4b0eb13f048385909480e765f4eefec94c304edf9e01b2170869c9cdf8eb11 9)
+!(chain #0x8b0d8bd2feef87f7347a8d2dbe7cc74ba045ec0f14c1417266e3f46d0a0ac5 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 "2609e61d828611427781388bb243edff2d5837762605a576517ca8bdb80729")
+!(verify "253faf43befe62e751e71f85fb46dda4a9b65d37edba982e554bbb9f75f9ba")
 
 ;; Now let's chain another call to the new head, adding 12 to the counter.
 
-!(chain #0x82bfc47b9b430f5b2122157cb2ffc23514608aed3fdcad4280137b20b47893 12)
+!(chain #0x94fc9a9a9b8a2d6816161e452a59c3a9b1047105d22653337d5b389eacfcd5 12)
 
 ;; Now the counter is 21, and we have a new head commitment.
 
@@ -35,11 +35,11 @@
 
 ;; And verify.
 
-!(verify "23febcbd5eed7e04a1733364e319e7c99415ca8a556f5fb6376662f732979b")
+!(verify "3fb0e2eff4930e48be2ede81e4e7514c242bd9baa73a91a6eb5efe211d9784")
 
 ;; One more time, we'll add 14 to the head commitment's internal state.
 
-!(chain #0x7992fc230601060378202010780dc88d00321372cec452876d370f73fb3b84 14)
+!(chain #0x3fb9a15b0b729de67da4b86adc1d10062ce575a6057ba9f8c42038ce7882a4 14)
 
 ;; 21 + 14 = 35, as expected.
 
@@ -49,7 +49,7 @@
 
 ;; Verify.
 
-!(verify "5438ff9d40034f5e047d91fbe67ee56f13d26641b619e5e945595c954b7b2f")
+!(verify "1a8222c44d45e94534895c8fa657d9784dcf5ead185a8e98f6d9b771254560")
 
 ;; Repeat indefinitely.
 

diff --git a/demo/functional-commitment.lurk b/demo/functional-commitment.lurk
@@ -10,16 +10,16 @@
 
 ;; We open the functional commitment on input 5: Evaluate f(5).
 
-!(call #0x1aabc88a967eb6c0ab3e73eb5a9cb55380cdcfc8aaf6a488a4620bf67afb4b 5)
+!(call #0x197bb2c08ec58b6c84debb1c9d75b4d91c2b1be3a5337f6171d1f896d4c2c2 5)
 
 ;; We can prove the functional-commitment opening.
 
 !(prove)
 
 ;; We can inspect the input/output expressions of the proof.
 
-!(inspect "b68e59e1a971a9b02f79cb5073d7ff6b236f685f25ad3cc44890941e521d1")
+!(inspect "3863a71b55ec6f53d1547e503bc69491e87e57063143e7dc62b1a91de4ef7")
 
 ;; Finally, and most importantly, we can verify the proof.
 
-!(verify "b68e59e1a971a9b02f79cb5073d7ff6b236f685f25ad3cc44890941e521d1")
+!(verify "3863a71b55ec6f53d1547e503bc69491e87e57063143e7dc62b1a91de4ef7")
diff --git a/demo/protocol.lurk b/demo/protocol.lurk
@@ -10,13 +10,13 @@
   :description "hash opens to a pair (a, b) s.t. a+b=30 and a>10")
 
 ;; This is the prover's pair, whose hash is
-;; #c0x76c3537770d61633a76264596e9fdefcf3bca72ade7f9553d5b3e6bfacba3b
+;; #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350
 (commit '(13 . 17))
 
 ;; Let's prove it and write the proof to the file protocol-proof
 !(prove-protocol my-protocol
   "protocol-proof"
-  #c0x76c3537770d61633a76264596e9fdefcf3bca72ade7f9553d5b3e6bfacba3b
+  #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350
   '(13 . 17))
 
 ;; Now it can be verified

diff --git a/lib/util-test.lurk b/lib/util-test.lurk
@@ -71,8 +71,8 @@
 !(assert-eq '(1 4 9 16) (map (lambda (x) (* x x)) '(1 2 3 4)))
 
 ;; permute
-!(assert-eq '(e c a b d) (permute '(a b c d e) 123))
-!(assert-eq '(a d c b e) (permute '(a b c d e) 987))
+!(assert-eq '(b d e c a) (permute '(a b c d e) 123))
+!(assert-eq '(d a c e b) (permute '(a b c d e) 987))
 
 ;; expt
 !(assert-eq 32 (expt 2 5))

diff --git a/lib/util.lurk b/lib/util.lurk
@@ -26,9 +26,6 @@
               ;; this will error
               (break))))
 
-;; Unprovable -- guarantees a code path will not lead to a proof.
-!(def fail (lambda () (open #0x0)))
-
 ;; This should be a macro, so we can include the unevaluated form in the error.
 !(def assert (lambda (x) (if x x (error :assertion-failure nil))))
 

diff --git a/src/lurk/cli/meta.rs b/src/lurk/cli/meta.rs
@@ -488,7 +488,7 @@ impl<F: PrimeField32, C1: Chipset<F>, C2: Chipset<F>> MetaCmd<F, C1, C2> {
         info: &["It's also capable of opening persisted commitments."],
         example: &[
             "(commit (lambda (x) x))",
-            "!(call #c0x361877c9845ddda6aa16dd6c6bcd26fcea7b93930106a19f5d7d5cf10a9015 0)",
+            "!(call #c0x275439f3606672312cd1fd9caf95cfd5bc05c6b8d224819e2e8ea1a6c5808 0)",
         ],
         run: |repl, args, _path| {
             Self::call(repl, args, None)?;
@@ -527,7 +527,7 @@ impl<F: PrimeField32, C1: Chipset<F>, C2: Chipset<F>> MetaCmd<F, C1, C2> {
                        (let ((counter (+ counter x)))
                          (cons counter (commit (add counter)))))))
                (add 0)))",
-            "!(chain #c0x4b0eb13f048385909480e765f4eefec94c304edf9e01b2170869c9cdf8eb11 1)",
+            "!(chain #c0x8b0d8bd2feef87f7347a8d2dbe7cc74ba045ec0f14c1417266e3f46d0a0ac5 1)",
         ],
         run: |repl, args, _path| {
             let cons = Self::call(repl, args, None)?;
@@ -999,7 +999,7 @@ impl<C1: Chipset<F>, C2: Chipset<F>> MetaCmd<F, C1, C2> {
             "(commit '(13 . 17))",
             "!(prove-protocol my-protocol",
             "  \"protocol-proof\"",
-            "  #c0x76c3537770d61633a76264596e9fdefcf3bca72ade7f9553d5b3e6bfacba3b",
+            "  #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350",
             "  '(13 . 17))",
         ],
         run: |repl, args, _path| {

diff --git a/src/lurk/cli/tests/first.lurk b/src/lurk/cli/tests/first.lurk
@@ -35,17 +35,17 @@
 ;; test calling functional commitments
 !(call (lambda (x) x) 0)
 !(commit (eval '(lambda (x) x)))
-!(call #0x361877c9845ddda6aa16dd6c6bcd26fcea7b93930106a19f5d7d5cf10a9015 0)
-!(call (comm #0x361877c9845ddda6aa16dd6c6bcd26fcea7b93930106a19f5d7d5cf10a9015) 0)
+!(call #0x275439f3606672312cd1fd9caf95cfd5bc05c6b8d224819e2e8ea1a6c5808 0)
+!(call (comm #0x275439f3606672312cd1fd9caf95cfd5bc05c6b8d224819e2e8ea1a6c5808) 0)
 
 ;; test chain and transition
 !(commit (eval '(letrec ((add (lambda (counter x)
                        (let ((counter (+ counter x)))
                          (cons counter (commit (add counter)))))))
                (add 0))))
-!(chain #c0x4b0eb13f048385909480e765f4eefec94c304edf9e01b2170869c9cdf8eb11 1)
+!(chain #0x8b0d8bd2feef87f7347a8d2dbe7cc74ba045ec0f14c1417266e3f46d0a0ac5 1)
 
-!(def state0 (cons nil (comm #0x4b0eb13f048385909480e765f4eefec94c304edf9e01b2170869c9cdf8eb11)))
+!(def state0 (cons nil (comm #0x8b0d8bd2feef87f7347a8d2dbe7cc74ba045ec0f14c1417266e3f46d0a0ac5)))
 !(transition state1 state0 1)
 !(assert-eq (car state1) 1)
 !(fetch (cdr state1))

diff --git a/src/lurk/cli/tests/prove.lurk b/src/lurk/cli/tests/prove.lurk
@@ -1,5 +1,5 @@
 !(prove (cons 1 2))
-!(verify "1fe27d9ba542dbf6a82300a7ff3eb19c95c56eec112e095c16cec73d85c576")
+!(verify "3d8fad22afdde5643d55e9eaae4537bfc6d610c6b1bdf4c913560576cbe327")
 
 !(defprotocol my-protocol (hash pair)
   (cons
@@ -13,7 +13,7 @@
 
 !(prove-protocol my-protocol
   "repl-test-protocol-proof"
-  #c0x76c3537770d61633a76264596e9fdefcf3bca72ade7f9553d5b3e6bfacba3b
+  #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350
   '(13 . 17))
 
 !(verify-protocol my-protocol "repl-test-protocol-proof")

diff --git a/src/lurk/cli/tests/second.lurk b/src/lurk/cli/tests/second.lurk
@@ -7,11 +7,11 @@
 !(assert-eq (open #0x91542a0e943be900a067ecd113d8b3340e0aed1c3c00eb06768a318c17a885) 42)
 
 ;; test call/chain
-!(call #0x361877c9845ddda6aa16dd6c6bcd26fcea7b93930106a19f5d7d5cf10a9015 0)
-!(chain #0x4b0eb13f048385909480e765f4eefec94c304edf9e01b2170869c9cdf8eb11 1)
+!(call #0x275439f3606672312cd1fd9caf95cfd5bc05c6b8d224819e2e8ea1a6c5808 0)
+!(chain #0x8b0d8bd2feef87f7347a8d2dbe7cc74ba045ec0f14c1417266e3f46d0a0ac5 1)
 
 ;; test transition
-!(def state (cons nil #0x4b0eb13f048385909480e765f4eefec94c304edf9e01b2170869c9cdf8eb11))
+!(def state (cons nil #0x8b0d8bd2feef87f7347a8d2dbe7cc74ba045ec0f14c1417266e3f46d0a0ac5))
 !(transition state1 state 1)
 !(assert-eq (car state1) 1)
 

diff --git a/src/lurk/cli/tests/verify.lurk b/src/lurk/cli/tests/verify.lurk
@@ -1,5 +1,5 @@
-!(inspect "1fe27d9ba542dbf6a82300a7ff3eb19c95c56eec112e095c16cec73d85c576")
-!(verify "1fe27d9ba542dbf6a82300a7ff3eb19c95c56eec112e095c16cec73d85c576")
+!(inspect "3d8fad22afdde5643d55e9eaae4537bfc6d610c6b1bdf4c913560576cbe327")
+!(verify "3d8fad22afdde5643d55e9eaae4537bfc6d610c6b1bdf4c913560576cbe327")
 
 !(load-expr my-protocol "repl-test-protocol")
 !(verify-protocol my-protocol "repl-test-protocol-proof")
diff --git a/src/lurk/eval.rs b/src/lurk/eval.rs
@@ -859,7 +859,7 @@ pub fn eval<F: AbstractField>() -> FuncE<F> {
                     match res_tag {
                         Tag::Thunk => {
                             // In the case the result is a thunk we extend
-                            // its environment with itself and reduce its
+                            // its environment with it and reduce its
                             // body in the extended environment
                             let (body_tag, body, body_env) = load(res);
                             // `expr` is the symbol
@@ -910,7 +910,7 @@ pub fn eval_builtin_expr<F: AbstractField>(digests: &SymbolsDigests<F>) -> FuncE
             let err_tag = Tag::Err;
             let invalid_form = EvalErr::InvalidForm;
             match head [|name| digests.builtin_symbol_ptr(name).to_field()] {
-                "let", "letrec", "lambda", "cons", "strcons", "type-eq", "type-eqq", "apply" => {
+                "let", "letrec", "lambda" => {
                     let rest_not_cons = sub(rest_tag, cons_tag);
                     if rest_not_cons {
                         return (err_tag, invalid_form)
@@ -920,34 +920,46 @@ pub fn eval_builtin_expr<F: AbstractField>(digests: &SymbolsDigests<F>) -> FuncE
                     if rest_not_cons {
                         return (err_tag, invalid_form)
                     }
-                    let (snd_tag, snd, rest_tag, _rest) = load(rest);
-                    let rest_not_nil = sub(rest_tag, nil_tag);
-                    if rest_not_nil {
-                        return (err_tag, invalid_form)
-                    }
                     match head [|name| digests.builtin_symbol_ptr(name).to_field()] {
                         "let" => {
-                            // first element: let symbol
-                            // second element: binding list
-                            // third element: body
-                            let (res_tag, res) = call(eval_let, fst_tag, fst, snd_tag, snd, env);
+                            // fst: bindings list
+                            // rest: list-like body
+                            let (res_tag, res) = call(eval_let, fst_tag, fst, rest_tag, rest, env);
                             return (res_tag, res)
                         }
                         "letrec" => {
                             // analogous to `let`
-                            let (res_tag, res) = call(eval_letrec, fst_tag, fst, snd_tag, snd, env);
+                            let (res_tag, res) = call(eval_letrec, fst_tag, fst, rest_tag, rest, env);
                             return (res_tag, res)
                         }
                         "lambda" => {
-                            // first element: parameter list
-                            // second element: body
-                            // third element: env
+                            // fst: parameters list
+                            // rest: list-like body
+
                             // A function (more precisely, a closure) is an object with a
                             // parameter list, a body and an environment
                             let res_tag = Tag::Fun;
-                            let res = store(fst_tag, fst, snd_tag, snd, env);
+                            let res = store(fst_tag, fst, rest_tag, rest, env);
                             return (res_tag, res)
                         }
+                    }
+                }
+                "cons", "strcons", "type-eq", "type-eqq", "apply" => {
+                    let rest_not_cons = sub(rest_tag, cons_tag);
+                    if rest_not_cons {
+                        return (err_tag, invalid_form)
+                    }
+                    let (fst_tag, fst, rest_tag, rest) = load(rest);
+                    let rest_not_cons = sub(rest_tag, cons_tag);
+                    if rest_not_cons {
+                        return (err_tag, invalid_form)
+                    }
+                    let (snd_tag, snd, rest_tag, _rest) = load(rest);
+                    let rest_not_nil = sub(rest_tag, nil_tag);
+                    if rest_not_nil {
+                        return (err_tag, invalid_form)
+                    }
+                    match head [|name| digests.builtin_symbol_ptr(name).to_field()] {
                         "cons", "strcons" => {
                             let (res_tag, res) = call(eval_binop_misc, head, fst_tag, fst, snd_tag, snd, env);
                             return (res_tag, res)
@@ -1959,7 +1971,7 @@ pub fn eval_let<F: AbstractField>() -> FuncE<F> {
             let invalid_form = EvalErr::InvalidForm;
             match binds_tag {
                 InternalTag::Nil => {
-                    let (res_tag, res) = call(eval, body_tag, body, env);
+                    let (res_tag, res) = call(eval_begin, body_tag, body, env);
                     return (res_tag, res)
                 }
                 Tag::Cons => {
@@ -1997,7 +2009,7 @@ pub fn eval_let<F: AbstractField>() -> FuncE<F> {
                                 let (res_tag, res) = call(eval_let, rest_binds_tag, rest_binds, body_tag, body, ext_env);
                                 return (res_tag, res)
                             }
-                            let (res_tag, res) = call(eval, body_tag, body, ext_env);
+                            let (res_tag, res) = call(eval_begin, body_tag, body, ext_env);
                             return (res_tag, res)
                         }
                     };
@@ -2018,7 +2030,7 @@ pub fn eval_letrec<F: AbstractField>() -> FuncE<F> {
             let invalid_form = EvalErr::InvalidForm;
             match binds_tag {
                 InternalTag::Nil => {
-                    let (res_tag, res) = call(eval, body_tag, body, env);
+                    let (res_tag, res) = call(eval_begin, body_tag, body, env);
                     return (res_tag, res)
                 }
                 Tag::Cons => {
@@ -2061,7 +2073,7 @@ pub fn eval_letrec<F: AbstractField>() -> FuncE<F> {
                                 let (res_tag, res) = call(eval_letrec, rest_binds_tag, rest_binds, body_tag, body, ext_env);
                                 return (res_tag, res)
                             }
-                            let (res_tag, res) = call(eval, body_tag, body, ext_env);
+                            let (res_tag, res) = call(eval_begin, body_tag, body, ext_env);
                             return (res_tag, res)
                         }
                     };
@@ -2095,7 +2107,7 @@ pub fn apply<F: AbstractField>(digests: &SymbolsDigests<F>) -> FuncE<F> {
 
             match params_tag {
                 InternalTag::Nil => {
-                    let (res_tag, res) = call(eval, body_tag, body, func_env);
+                    let (res_tag, res) = call(eval_begin, body_tag, body, func_env);
                     match res_tag {
                         Tag::Err => {
                             return (res_tag, res)
@@ -2327,7 +2339,7 @@ mod test {
         expect_eq(preallocate_symbols.width(), expect!["180"]);
         expect_eq(eval_coroutine_expr.width(), expect!["10"]);
         expect_eq(eval.width(), expect!["77"]);
-        expect_eq(eval_builtin_expr.width(), expect!["144"]);
+        expect_eq(eval_builtin_expr.width(), expect!["146"]);
         expect_eq(eval_apply_builtin.width(), expect!["79"]);
         expect_eq(eval_opening_unop.width(), expect!["97"]);
         expect_eq(eval_hide.width(), expect!["115"]);

diff --git a/src/lurk/tag.rs b/src/lurk/tag.rs
@@ -30,12 +30,12 @@ pub enum Tag {
     Key,
     Fun,
     Builtin,
+    Coroutine,
     Sym,
     Cons,
     Env,
     Thunk,
     Err,
-    Coroutine,
 }
 
 impl Tag {