Introduction
Lurk is a verifiable Lisp influenced by Scheme and Common Lisp. As an application, it's capable of generating zero-knowledge proofs for the evaluation of arbitrary Lurk expressions.
This book explores Lurk from an usability standpoint, without deep diving into its cryptographic primitives.
We will start from installation instructions and then go through a gentle introduction to Lisp while building up the Lurk dialect as a means of designing systems in which parties can provably display possession of knowledge without disclosing it.
The "Language reference" chapter can be used as a precise reference for experienced users.
Note: this book is still work in progress.
Getting started
Setup
Clone the lurk repository and run the following command inside its folder:
$ cargo install --path .
This will make the lurk binary globally accessible from your terminal:
$ lurk
Lurk REPL welcomes you.
lurk-user>
Having lurk installed can help the reader with experimentation while going through the book.
More detailed information on the features of the lurk app will be presented on a later chapter.
Recommended tooling
- lurk-vscode is an extension for VS Code that provides syntax highlighting and interactions with the Lurk REPL
Support
In case of any trouble, we are available on our Zulip server. Feel free to join us, start threads and ask questions.
Lurk is a Lisp
Since Lurk is a Lisp, it has practically no syntax and expressions can be formed with simple rules.
The expression 3 is self-evaluating.
lurk-user> 3
[1 iteration] => 3
When an expression is evaluated, you should see a response with the result and an iteration count, in this case, 1. You can think of this as representing the "cost" or number of "clock cycles" required to evaluate the expression. In the simplest case of a self-evaluating expression, only a single iteration is required.
Characters and strings are also self-evaluating.
lurk-user> 'a'
[1 iteration] => 'a'
lurk-user> "abc"
[1 iteration] => "abc"
Lists are evaluated by treating the first element as an operator and the rest as operands.
lurk-user> (+ 2 3)
[3 iterations] => 5
An operator can be either a built-in operator or an expression that evaluates to a function (more on this later).
A list whose first element is neither a built-in operator nor evaluates to a function yields an error when evaluated.
lurk-user> (1 2 3)
[2 iterations] => <Err ApplyNonFunc>
nil and t
nil and t are self-evaluating symbols.
lurk-user> nil
[1 iteration] => nil
lurk-user> t
[1 iteration] => t
nil carries the semantics of "false".
lurk-user> (= 1 2)
[3 iterations] => nil
lurk-user> (if nil 1 2)
[3 iterations] => 2
t carries the semantics of "true".
lurk-user> (= 1 1)
[2 iterations] => t
lurk-user> (if t 1 2)
[3 iterations] => 1
More on lists
Pairs are constructed with cons, and their elements are separated by a . when printed.
lurk-user> (cons 1 2)
[3 iterations] => (1 . 2)
A pair whose second element is nil is said to form a list with one element.
lurk-user> (cons 1 nil)
[3 iterations] => (1)
Note that nil is elided when printing lists.
We can left-expand this list by consing an element as its new head.
lurk-user> (cons 0 (cons 1 nil))
[5 iterations] => (0 1)
Thus, within this design, nil can be used to represent the empty list.
To deconstruct a pair, we can use car and cdr, which return the first and the second element respectively.
lurk-user> (car (cons 1 2))
[4 iterations] => 1
lurk-user> (cdr (cons 1 2))
[4 iterations] => 2
And in our abstraction of lists, we say that car and cdr return the list's head and tail respectively.
lurk-user> (car (cons 0 (cons 1 nil)))
[6 iterations] => 0
lurk-user> (cdr (cons 0 (cons 1 nil)))
[6 iterations] => (1)
By definition, (car nil) and (cdr nil) return nil.
lurk-user> (car nil)
[2 iterations] => nil
lurk-user> (cdr nil)
[2 iterations] => nil
Functions
A Lurk function can be created by using the lambda built-in operator, which requires a list of arguments and a body.
lurk-user> (lambda (x) (+ x 1))
[1 iteration] => <Fun (x) ((+ x 1))>
Then we can write function applications by using lists, as mentioned before.
lurk-user> ((lambda (x) (+ x 1)) 10)
[6 iterations] => 11
Functions with multiple arguments follow the same input design.
lurk-user> ((lambda (x y) (+ x y)) 3 5)
[7 iterations] => 8
Variadic functions are supported by adding &rest <var> at the end of the arguments list, which binds a list of all remaining parameters to <var>.
lurk-user> ((lambda (&rest x) x))
[3 iterations] => nil
lurk-user> ((lambda (&rest x) x) 1 2 3)
[6 iterations] => (1 2 3)
lurk-user> ((lambda (x y &rest z) z) 1 2 3)
[6 iterations] => (3)
lurk-user> ((lambda (x y &rest z) z) 1 2)
[5 iterations] => nil
Lurk supports partial applications, so we can apply arguments one by one if we want.
lurk-user> (((lambda (x y) (+ x y)) 3) 5)
[8 iterations] => 8
A function may also be defined to not need any arguments.
lurk-user> (lambda () nil)
[1 iteration] => <Fun () (nil)>
lurk-user> ((lambda () nil))
[3 iterations] => nil
Note that the second expression actually calls the function.
Functions can also be recursive and call themselves by their names. But how do we name functions?
Bindings
We'll come back to recursive functions in a bit.
First, let's see how let allows us to introduce variable bindings.
lurk-user> (let ((a 1)) a)
[3 iterations] => 1
let consumes a list of bindings and the final expression, which can use the introduced variables (or not).
lurk-user>
(let ((a 1)
(b 2)
(c 3))
(+ a b))
[7 iterations] => 3
When defining the value bound to a variable, we can use the variables that were previously bound.
lurk-user>
(let ((a 1)
(b (+ a 1)))
b)
[6 iterations] => 2
Later bindings shadow previous ones.
lurk-user>
(let ((a 1)
(a 2))
a)
[4 iterations] => 2
And inner bindings shadow outer ones.
lurk-user>
(let ((a 1))
(let ((a 2)) a))
[5 iterations] => 2
Now we can bind functions to variables.
lurk-user>
(let ((succ (lambda (x) (+ x 1))))
(succ 10))
[8 iterations] => 11
So, can we create a looping recursive function yet?
lurk-user>
(let ((loop (lambda () (loop))))
(loop))
[6 iterations] => <Err UnboundVar>
In a let expression, free variables are expected to be already available by, for instance, being defined on a previous binding.
If we try to call loop when defining loop, it will be unbound.
lurk-user>
(let ((not-a-loop (lambda () 42))
(not-a-loop (lambda () (not-a-loop))))
(not-a-loop))
[8 iterations] => 42
In the example above, the body of the second binding for not-a-loop simply calls the previous definition of not-a-loop.
If we want to define recursive functions, we need to use letrec.
lurk-user>
(letrec ((loop (lambda () (loop))))
(loop))
Error: Loop detected
And now we can finally write a recursive function that computes the sum of the first n numbers.
lurk-user>
(letrec ((sum-upto (lambda (n) (if (= n 0)
0
(+ n (sum-upto (- n 1)))))))
(sum-upto 5))
[55 iterations] => 15
Higher-order functions
Lurk supports Higher-order functions. That is, Lurk functions can receive functions as input and return functions as output, allowing for a wide range of expressive functional programming idioms.
lurk-user>
(letrec ((map (lambda (f list)
(if (eq list nil)
nil
(cons (f (car list))
(map f (cdr list))))))
(square (lambda (x) (* x x))))
(map square '(1 2 3 4 5)))
[78 iterations] => (1 4 9 16 25)
By the way, how was the list (1 2 3 4 5) produced so easily?
Quoting
The quote built-in operator skips the reduction of its argument and returns it as it is.
We've seen that trying to reduce (1 2 3) doesn't work.
But if we want Lurk not to face that list as a function application, we can use quoting.
lurk-user> (quote (1 2 3))
[1 iteration] => (1 2 3)
And we can use ' as syntax sugar for brevity.
lurk-user> '(1 2 3)
[1 iteration] => (1 2 3)
Data types
Even though Lurk is not statically typed, it is strongly typed.
Unsigned integers
The default numeric type in Lurk is u64, which roundtrips as one would expect:
lurk-user> (- 0 1)
[3 iterations] => 18446744073709551615
lurk-user> (+ 18446744073709551615 1)
[3 iterations] => 0
Finite field elements
Lurk also allows operating over finite field elements directly, which is cheaper than dealing with u64 in terms of proving costs.
lurk-user> (+ 1n 2n)
[3 iterations] => 3n
Beware, though, that different finite fields have different sizes. The current Lurk instantiation uses Baby Bear.
lurk-user> (- 0n 1n)
[3 iterations] => 2013265920n
So, to write stable Lurk code, use finite field elements only if you are sure that those values won't grow too much.
Big nums
Numbers large enough to represent the domain of approximately 256-bit hash digests.
lurk-user> #0x1
[1 iteration] => #0x1
lurk-user> #0x4668b9badf58209537dbb62e132badc5bb7bbaf137a8daeeef550046634da8
[1 iteration] => #0x4668b9badf58209537dbb62e132badc5bb7bbaf137a8daeeef550046634da8
Commitments
Actual cryptographic commitments to Lurk data, as we shall see in the next chapter. It has the same domain range of big nums.
lurk-user> (comm #0x0)
[2 iterations] => #c0x0
Characters
Lurk uses UTF-8 encoding to represent characters internally. Meaning that a wide range of characters are accepted.
lurk-user> 'a'
[1 iteration] => 'a'
lurk-user> '€'
[1 iteration] => '€'
lurk-user> 'ệ'
[1 iteration] => 'ệ'
Strings
Very briefly, strings are sequences of characters. We can even extract the head and the tail of a string.
lurk-user> (car "abc")
[2 iterations] => 'a'
lurk-user> (cdr "abc")
[2 iterations] => "bc"
Cons (pair)
We've already covered pairs, but it's important to mention that pairs are of their own type.
lurk-user> (type-eq (cons 1 2) (cons 'a' nil))
[7 iterations] => t
Symbols
These are the typical language entities we use to bind values to, as in (let ((a 1)) a).
lurk-user> (type-eq 'a 'x)
[3 iterations] => t
t and nil are of this same type.
lurk-user> (type-eq t 'x)
[3 iterations] => t
lurk-user> (type-eq t nil)
[3 iterations] => t
Keywords
Keywords are self-evaluating symbols without special semantics like t or nil.
lurk-user> :foo
[1 iteration] => :foo
lurk-user> (type-eq :foo :bar)
[3 iterations] => t
Built-ins
These are symbols in the .lurk.builtin package (more on packages later).
lurk-user> (type-eq 'cons 'let)
[3 iterations] => t
lurk-user> (type-eq 'cons 'x)
[3 iterations] => nil
Coroutines
Symbols specified in a Lang used to call coroutines (more on this later).
Functions
Functions are the result of evaluated lambda expressions.
lurk-user> (type-eq (lambda () nil) (lambda (x) (+ x 1)))
[3 iterations] => t
Undersaturated functions, that is, functions that have not been supplied all of their arguments, are still of the same type.
lurk-user>
(type-eq
(lambda (x) (+ x 1))
((lambda (x y) (+ x y)) 1))
[5 iterations] => t
Environments
Environments carry pairs of symbol/value bindings. Every expression evaluation in Lurk happens with respect to a certain environment.
The starting environment in the REPL is empty by default.
lurk-user> (current-env)
[1 iteration] => <Env ()>
The environment grows as we create new bindings.
lurk-user> (let ((a 1) (b 2)) (current-env))
[4 iterations] => <Env ((b . 2) (a . 1))>
Later, we will learn how to change the REPL's environment.
Commitments
Lurk has built-in support for cryptographic commitments.
We can create a commitment to any Lurk data with commit.
lurk-user> (commit 123)
[2 iterations] => #c0x944834111822843979ace19833d05ca9daf2f655230faec517433e72fe777b
Now Lurk knows that #c0x944834111822843979ace19833d05ca9daf2f655230faec517433e72fe777b is a commitment to 123 and can successfully open it.
lurk-user> (open #c0x944834111822843979ace19833d05ca9daf2f655230faec517433e72fe777b)
[2 iterations] => 123
Lurk understands it if you use big nums in an open expression directly.
lurk-user> (open #0x944834111822843979ace19833d05ca9daf2f655230faec517433e72fe777b)
[2 iterations] => 123
Because Lurk commitments are based on Poseidon hashes (just as all compound data in Lurk is), it is computationally infeasible to discover a second preimage to the digest represented by a commitment. This means that Lurk commitments are (computationally) binding.
Lurk also supports explicit hiding commitments. The hiding secret must be a big num.
lurk-user> (hide #0x1 123)
[3 iterations] => #c0x483cd4ed61cb38d4722743fe470c4c81abf1a568ceae9423864d5acf03739f
For when hiding is unimportant, commit creates commitments with a default secret of #0x0.
lurk-user> (hide #0x0 123)
[3 iterations] => #c0x944834111822843979ace19833d05ca9daf2f655230faec517433e72fe777b
And both hashes above open to the same value 123.
lurk-user> (open #c0x944834111822843979ace19833d05ca9daf2f655230faec517433e72fe777b)
[2 iterations] => 123
lurk-user> (open #c0x483cd4ed61cb38d4722743fe470c4c81abf1a568ceae9423864d5acf03739f)
[2 iterations] => 123
Functional commitments
Again, we can commit to any Lurk data, including functions.
lurk-user> (commit (lambda (x) (+ 7 (* x x))))
[2 iterations] => #c0x64411a93ff0183cdbe7c2d0dbbbd69ac7b47c75aa1124a901207f3f47d0ce4
The above is a commitment to a function that squares its input then adds seven. Then we can open it and apply arguments as usual.
lurk-user> ((open #c0x64411a93ff0183cdbe7c2d0dbbbd69ac7b47c75aa1124a901207f3f47d0ce4) 5)
[8 iterations] => 32
lurk-user> ((open #c0x64411a93ff0183cdbe7c2d0dbbbd69ac7b47c75aa1124a901207f3f47d0ce4) 9)
[8 iterations] => 88
Higher-order functional commitments
Higher-order functions are no exceptions and can be committed to in the same manner.
Here, we commit to a function that receives a function as input and applies it to a secret internal value.
lurk-user>
(let ((secret-data 222)
(data-interface (lambda (f) (f secret-data))))
(commit data-interface))
[5 iterations] => #c0x21aa7ddf7089aa62c98717d2634cf8d414f9b7b2d36c46d6a360ba754beff1
Now we can open it, applying it to a function that adds 111 to the secret value that the committed function hides.
lurk-user>
((open #c0x21aa7ddf7089aa62c98717d2634cf8d414f9b7b2d36c46d6a360ba754beff1)
(lambda (data) (+ data 111)))
[10 iterations] => 333
We coin the term Higher-Order Functional Commitments, and as far as we are aware, Lurk is the first and only extant system enabling this powerful usage in the bare language.
Packages
Language reference
This is a living specification of the current set of built-ins in the .lurk package.
Built-in atoms
nil
nil is boolean false and can also represent the empty list.
It has its own type differently from other symbols.
lurk-user> (eq nil '())
[3 iterations] => t
lurk-user> (cdr '(1))
[2 iterations] => nil
lurk-user> (if nil "true" "false")
[3 iterations] => "false"
t
t is boolean true. In boolean contexts like if, anything that isn't nil is considered false, but t is generally used.
lurk-user> (eq 1 1)
[2 iterations] => t
lurk-user> (if t "true" "false")
[3 iterations] => "true"
Built-in operators
atom
(atom x) returns nil if x is a pair, and t otherwise.
lurk-user> (atom nil)
[2 iterations] => t
lurk-user> (atom t)
[2 iterations] => t
lurk-user> (atom (cons 1 2))
[4 iterations] => nil
lurk-user> (atom '(1 2 3))
[2 iterations] => nil
apply
(apply f args) will call f with the argument list args and return its result. args must be a list.
lurk-user> (apply (lambda (x y z) (+ x (+ y z))) '(1 2 3))
[11 iterations] => 6
lurk-user> (apply (lambda (x y z) (+ x (+ y z))) (list 1 2 3))
[11 iterations] => 6
lurk-user> ((apply (lambda (x y z) (+ x (+ y z))) (list 1 2)) 3) ;; partial application also works
[12 iterations] => 6
lurk-user> (apply (lambda (x) x) 1)
[3 iterations] => <Err ArgsNotList>
begin
(begin e1 e2 ... en) evaluates e1, e2, ..., en and returns the reduced version of en.
It is particularly useful when we want to manifest side-effects when evaluating the inner expressions e1, e2, ...
lurk-user> (begin 1 2 3)
[4 iterations] => 3
lurk-user> ((lambda (x) (begin (emit x) (+ x x))) 1)
1
[7 iterations] => 2
bignum
(bignum x) tries to convert x to a big num. Can only be used with commitments currently. Returns <Err CantCastToBigNum> if the types are incompatible.
lurk-user> (bignum (commit 1))
[3 iterations] => #0xf99d96623838468091ce6590ccb3b829938823d964f3f5962f837f1400e2b
car
(car cons-cell) returns the first element of its argument if it is a pair. Also works with strings, returning its first character. Returns <Err NotCons> otherwise.
lurk-user> (car (cons 1 2))
[4 iterations] => 1
lurk-user> (car '(1 2 3))
[2 iterations] => 1
lurk-user> (car (strcons 'a' "b"))
[4 iterations] => 'a'
lurk-user> (car "abc")
[2 iterations] => 'a'
cdr
(cdr cons-cell) returns the second element of its argument if it is a pair. Also works with strings, returning its tail. Returns <Err NotCons> otherwise.
lurk-user> (cdr (cons 1 2))
[4 iterations] => 2
lurk-user> (cdr '(1 2 3))
[2 iterations] => (2 3)
lurk-user> (cdr (strcons 'a' "b"))
[4 iterations] => "b"
lurk-user> (cdr "ab")
[2 iterations] => "b"
char
(char x) tries to convert x to a character. Can be used with integers. Returns <Err CantCastToChar> if the types are incompatible.
A char can store 32-bits of data, and this conversion truncates 64-bit integers into its 32 least significant bits.
lurk-user> (char 0x41)
[2 iterations] => 'A'
lurk-user> (char 65)
[2 iterations] => 'A'
lurk-user> (char nil)
[2 iterations] => <Err CantCastToChar>
commit
(commit x) is equivalent to (hide #0x0 x). It creates a commitment to the result of evaluating x, but sets the secret to the default of zero.
lurk-user> (commit 1)
[2 iterations] => #c0xf99d96623838468091ce6590ccb3b829938823d964f3f5962f837f1400e2b
lurk-user> (open #c0xf99d96623838468091ce6590ccb3b829938823d964f3f5962f837f1400e2b)
[3 iterations] => 1
lurk-user> (secret #c0xf99d96623838468091ce6590ccb3b829938823d964f3f5962f837f1400e2b)
[3 iterations] => #0x0
comm
(comm x) tries to convert x to a commitment. Can only be used with big nums currently. Returns <Err CantCastToComm> if the types are incompatible.
lurk-user> (comm #0x0)
[2 iterations] => #c0x0
lurk-user> (bignum (comm #0x0))
[3 iterations] => #0x0
cons
(cons x y) creates a new pair with first element x and second element y. The result of (cons x y) is denoted by (x . y) or simply (x) if y is nil.
lurk-user> (eq (cons 1 nil) (cons 1 '()))
[6 iterations] => t
lurk-user> (cons 1 2)
[3 iterations] => (1 . 2)
lurk-user> (car (cons 1 2))
[4 iterations] => 1
lurk-user> (cdr (cons 1 2))
[4 iterations] => 2
lurk-user> (cons 1 '(2 3))
[3 iterations] => (1 2 3)
list
(list e1 e2 ... en) creates a list with the reduced versions of e1, e2, ..., en.
lurk-user> (list)
[1 iteration] => nil
lurk-user> (list (+ 1 1) "hi")
[4 iterations] => (2 "hi")
current-env
(current-env) returns the current environment. The current environment can be modified by let, letrec and lambda expressions.
See also the REPL meta-commands def, defrec and clear for interacting with the current REPL environment.
lurk-user> (current-env)
[1 iteration] => <Env ()>
lurk-user> (let ((x 1)) (current-env))
[3 iterations] => <Env ((x . 1))>
lurk-user> (letrec ((x 1)) (current-env))
[4 iterations] => <Env ((x . <Thunk 1>))>
lurk-user> ((lambda (x) (current-env)) 1)
[4 iterations] => <Env ((x . 1))>
emit
(emit x) prints x to the output and returns x.
lurk-user> (emit 1)
1
[2 iterations] => 1
lurk-user> (let ((f (lambda (x) (emit x)))) (begin (f 1) (f 2) (f 3)))
1
2
3
[16 iterations] => 3
empty-env
(empty-env) returns the canonical empty environment.
lurk-user> (empty-env)
[1 iteration] => <Env ()>
lurk-user> (eq (empty-env) (current-env))
[3 iterations] => t
lurk-user> (let ((x 1)) (eq (empty-env) (current-env)))
[5 iterations] => nil
eval
(eval form env) evaluates form using env as its environment. (eval form) is equivalent to (eval form (empty-env)). Here form must be a quoted syntax tree of Lurk code.
lurk-user> (eval 1)
[3 iterations] => 1
lurk-user> (eval (+ 1 2)) ;; this expands to `(eval 3)` -- probably not what was intended!
[5 iterations] => 3
lurk-user> (eval '(+ 1 2)) ;; this will actually call `eval` with `'(+ 1 2)` as its argument
[5 iterations] => 3
lurk-user> (eval (cons '+ (cons 1 (cons 2 nil))))
[11 iterations] => 3
lurk-user> (cons '+ (cons 1 (cons 2 nil)))
[7 iterations] => (+ 1 2)
lurk-user> (eval 'x)
[3 iterations] => <Err UnboundVar>
lurk-user> (eval 'x (let ((x 1)) (current-env)))
[6 iterations] => 1
eq
(eq x y) returns t if x and y, after both being reduced, are equal and nil otherwise.
lurk-user> (eq 1 (- 2 1))
[4 iterations] => t
lurk-user> (eq nil nil)
[2 iterations] => t
lurk-user> (eq 'a' 'b')
[3 iterations] => nil
lurk-user> (eq (+ 1 2) (+ 2 1))
[5 iterations] => t
lurk-user> (eq 'a' (char (+ (u64 'A') 32)))
[7 iterations] => t
lurk-user> (eq (cons 1 2) (cons 2 1))
[7 iterations] => nil
eqq
(eqq x y) returns t if x and y, after only reducing y, are equal and nil otherwise.
Note: the second "q" in eqq is a reference to "quote" because (eqq x y) is equivalent to (eq (quote x) y).
lurk-user> (eqq (1 . 2) (cons 1 2))
[4 iterations] => t
type-eq
(type-eq x y) returns t if x and y, after both being reduced, have the same type and nil otherwise.
lurk-user> (type-eq 1 2)
[3 iterations] => t
lurk-user> (type-eq (cons 1 2) (cons 3 4))
[7 iterations] => t
lurk-user> (type-eq 'x 'y)
[3 iterations] => t
lurk-user> (type-eq 'x t)
[3 iterations] => nil
lurk-user> (type-eq 'x nil)
[3 iterations] => nil
lurk-user> (type-eq t nil)
[3 iterations] => nil
lurk-user> (type-eq '() '(1 2)) ;; this is surprisingly the case because `'()` is `nil`, which is a different type from `cons`
[3 iterations] => nil
type-eqq
(type-eqq x y) returns t if x and y, after only reducing y, have the same type and nil otherwise.
Note: the second "q" in type-eqq is a reference to "quote" because (type-eqq x y) is equivalent to (type-eq (quote x) y).
lurk-user> (type-eqq 1 (+ 1 2))
[4 iterations] => t
lurk-user> (type-eqq (+ 1 2) 1)
[2 iterations] => nil
lurk-user> (type-eqq (+ 1 2) (cons 1 2))
[4 iterations] => t
hide
(hide secret value) creates a hiding commitment to value with secret as the salt. secret must be a big num.
lurk-user> (hide #0x123 456)
[3 iterations] => #c0x4420657169325d52f910f0ffe606b3a7b600a982691926b207f21350120d3d
lurk-user> (open #c0x4420657169325d52f910f0ffe606b3a7b600a982691926b207f21350120d3d)
[3 iterations] => 456
lurk-user> (secret #c0x4420657169325d52f910f0ffe606b3a7b600a982691926b207f21350120d3d)
[3 iterations] => #0x123
if
(if cond then else) returns then if cond is non-nil or else otherwise. Only nil values are considered false. (if cond then) is equivalent to (if cond then nil)
lurk-user> (if t "true" "false")
[3 iterations] => "true"
lurk-user> (if nil "true" "false")
[3 iterations] => "false"
lurk-user> (if nil "true")
[2 iterations] => nil
lurk-user> (if 0 "true") ;; note: `0` is *not* `nil`
[3 iterations] => "true"
lambda
(lambda (args...) body) creates a function that takes a list of arguments and returns the result of evaluating body by binding the variable bindings to the supplied arguments. A function is called when it is in the head of a list.
The list of arguments can optionally end with &rest <var>, which denotes that any remaining arguments, if present, are bound to <var> as a list.
lurk-user> (lambda () 1)
[1 iteration] => <Fun () (1)>
lurk-user> (lambda (x) x)
[1 iteration] => <Fun (x) (x)>
lurk-user> ((lambda () 1))
[3 iterations] => 1
lurk-user> ((lambda (x) x) 1)
[4 iterations] => 1
lurk-user> ((lambda (x y z) (+ x (+ y z))) 1 2 3)
[10 iterations] => 6
lurk-user> (let ((f (lambda (x y z) (+ x (+ y z))))) (+ (f 1 2 3) (f 3 2 1))) ;; here `f` is the variable bound to the `lambda`
[19 iterations] => 12
lurk-user> ((lambda (x y &rest z) z) 1 2 3)
[6 iterations] => (3)
lurk-user> ((lambda (x y &rest z) z) 1 2)
[5 iterations] => nil
lurk-user> ((lambda (&rest x) x))
[3 iterations] => nil
Evaluating the body happens as if there were a begin surrounding it.
lurk-user> ((lambda () (emit 1) (emit 2)))
1
2
[6 iterations] => 2
let
(let ((var binding) ...) body) extends the current environment with a set of variable bindings and then evaluates body in the updated environment.
let is used for binding values to names and modifying environments.
See also the def REPL meta command.
lurk-user> (let ((x 1) (y 2)) (+ x y))
[6 iterations] => 3
lurk-user> (let ((x 1) (y 2)) (current-env))
[4 iterations] => <Env ((y . 2) (x . 1))>
Similarly to lambda, the body is interpreted as if there were a begin surrounding it.
lurk-user> (let ((a 1) (b 2)) (emit a) (emit b))
1
2
[7 iterations] => 2
letrec
(letrec ((var binding) ...) body) is similar to let, but it enables mutually recursive bindings.
See also the defrec REPL meta command.
lurk-user> (letrec ((x 1)) x)
[4 iterations] => 1
lurk-user> (letrec ((x 1)) (current-env))
[4 iterations] => <Env ((x . <Thunk 1>))> ;; Thunks are the internal representation used for recursive evaluation
lurk-user>
(letrec ((last (lambda (x) (if (cdr x) (last (cdr x)) (car x)))))
(last '(1 2 3)))
[20 iterations] => 3
lurk-user>
(letrec ((odd? (lambda (n) (if (= n 0) nil (even? (- n 1)))))
(even? (lambda (n) (if (= n 0) t (odd? (- n 1))))))
(odd? 5))
[53 iterations] => t
Similarly to let, the body is interpreted as if there were a begin surrounding it.
lurk-user> (letrec ((a 1) (b 2)) (emit a) (emit b))
1
2
[9 iterations] => 2
u64
(u64 x) tries to convert x to a 64-bit unsigned integer. Can be used with characters. Returns <Err CantCastToU64> if the types are incompatible.
lurk-user> (u64 'A')
[2 iterations] => 65
lurk-user> (u64 100) ;; this is a no-op
[2 iterations] => 100
lurk-user> (u64 nil)
[2 iterations] => <Err CantCastToU64>
open
(open x) opens the commitment x and return its value. If y is a big num, then (open y) is equivalent to (open (comm y)).
lurk-user> (open (commit 1))
[3 iterations] => 1
lurk-user> (open #c0xf99d96623838468091ce6590ccb3b829938823d964f3f5962f837f1400e2b)
[2 iterations] => 1
lurk-user> (open #0xf99d96623838468091ce6590ccb3b829938823d964f3f5962f837f1400e2b)
[2 iterations] => 1
quote
(quote x) returns x as its un-evaluated syntax form. (quote x) is equivalent to 'x.
lurk-user> (quote 1)
[1 iteration] => 1
lurk-user> (quote (+ 1 2))
[1 iteration] => (+ 1 2)
lurk-user> (quote 1)
[1 iteration] => 1
lurk-user> (quote (+ 1 2))
[1 iteration] => (+ 1 2)
lurk-user> '(+ 1 2)
[1 iteration] => (+ 1 2)
lurk-user> (cdr (quote (+ 1 2)))
[2 iterations] => (1 2)
lurk-user> (eval (cdr '(- + 1 2)))
[6 iterations] => 3
secret
(secret x) opens the commitment x and return its secret. If y is a big num, then (secret y) is equivalent to (secret (comm y)).
lurk-user> (secret (commit 1))
[3 iterations] => #0x0
lurk-user> (secret (hide #0x123 2))
[4 iterations] => #0x123
lurk-user> (secret #c0x76cc74360d9492188f072ecdafd2ddf50fadac0ce2007c551c09fdcd556109)
[2 iterations] => #0x123
lurk-user> (secret #0x76cc74360d9492188f072ecdafd2ddf50fadac0ce2007c551c09fdcd556109)
[2 iterations] => #0x123
strcons
(strcons x y) creates a new string with first element x and rest y. x must be a character and y must be a string. Strings are represented as lists of characters, but because the type of strings and lists are different, strcons is used for constructing a string instead.
lurk-user> (strcons 'a' nil) ;; the empty list is not the same as the empty string
[3 iterations] => <Err NotString>
lurk-user> (strcons 'a' "")
[3 iterations] => "a"
lurk-user> (strcons 'a' "bc")
[3 iterations] => "abc"
lurk-user> (car (strcons 'a' "bc"))
[4 iterations] => 'a'
lurk-user> (cdr (strcons 'a' "bc"))
[4 iterations] => "bc"
lurk-user> (cons 'a' "bc")
[3 iterations] => ('a' . "bc") ;; note how the cons is not the same thing as "abc"
breakpoint
(breakpoint) places a debugger breakpoint at the current evaluation state and returns nil.
(breakpoint x) places a debugger breakpoint and returns x, reduced.
!(help debug) for more information on the native debugger.
fail
(fail) errors out from evaluation, unprovably.
Built-in numeric operators
+
(+ a b) returns the sum of a and b. Overflow can happen implicitly. Returns <Err InvalidArg> if the types are not compatible.
lurk-user> (+ 1 2)
[3 iterations] => 3
lurk-user> (+ 1n 2n)
[3 iterations] => 3n
lurk-user> (+ #0x1 #0x2) ;; no big num arithmetic yet
[3 iterations] => <Err InvalidArg>
lurk-user> (+ 18446744073709551615 18446744073709551615)
[2 iterations] => 18446744073709551614 ;; implicit overflow for u64
-
(- a b) returns the difference between a and b. Underflow can happen implicitly. Returns <Err InvalidArg> if the types are not compatible.
lurk-user> (- 2 1)
[3 iterations] => 1
lurk-user> (- 2n 1n)
[3 iterations] => 1n
lurk-user> (- 0 1)
[3 iterations] => 18446744073709551615
lurk-user> (- 0n 1n)
[3 iterations] => 2013265920n
*
(* a b) returns the product of a and b. Overflow can happen implicitly. Returns <Err InvalidArg> if the types are not compatible.
lurk-user> (* 2 3)
[3 iterations] => 6
lurk-user> (* 2n 3n)
[3 iterations] => 6n
lurk-user> (* 18446744073709551615 18446744073709551615)
[2 iterations] => 1
/
(/ a b) returns the quotient between a and b. Returns <Err InvalidArg> if the types are not compatible. Returns <Err DivByZero> if b is zero.
When a and b are integers, the fractional part of the result is truncated and the result is the usual integer division.
When a and b are native field elements, (/ a b) returns the field element c such that (eq a (* c b)). In other words, (/ 1n x) gives the multiplicative inverse of the native field element x.
lurk-user> (/ 10 2)
[3 iterations] => 5
lurk-user> (/ 9 2)
[3 iterations] => 4
lurk-user> (/ 10n 2n)
[3 iterations] => 5n
lurk-user> (/ 9n 2n)
[3 iterations] => 1006632965n
lurk-user> (* 1006632965n 2n)
[3 iterations] => 9n
lurk-user> (* (/ 9 2) 2)
[4 iterations] => 8
lurk-user> (/ 1 0)
[3 iterations] => <Err DivByZero>
%
(% a b) returns the remainder of dividing a by b. Returns <Err NotU64> if the arguments are not unsigned integers.
lurk-user> (% 15 7)
[3 iterations] => 1
lurk-user> (% 15 6)
[3 iterations] => 3
lurk-user> (/ 15 6)
[3 iterations] => 2
lurk-user> (+ (* 2 6) 3)
[5 iterations] => 15
=
(= a b) returns t if a and b are equal and nil otherwise. The arguments must be numeric. Returns <Err InvalidArg> if the types are not compatible.
lurk-user> (= 123 123)
[2 iterations] => t
lurk-user> (= 123n 123n)
[2 iterations] => t
lurk-user> (= #0x123 #0x123)
[2 iterations] => t
lurk-user> (= "abc" "abc")
[2 iterations] => <Err InvalidArg>
<
(< a b) returns t if a is strictly less than b and nil otherwise. The arguments must be numeric. Returns <Err InvalidArg> if the types are not compatible. Note that native field elements cannot be compared like this.
lurk-user> (< "a" "b")
[3 iterations] => <Err InvalidArg>
lurk-user> (< 1n 2n)
[3 iterations] => <Err NotU64>
lurk-user> (< #0x123 #0x456)
[3 iterations] => t
lurk-user> (< 123 456)
[3 iterations] => t
>
(> a b) returns t if a is strictly greater than b and nil otherwise. The arguments must be numeric. Returns <Err InvalidArg> if the types are not compatible. Note that native field elements cannot be compared like this.
lurk-user> (> #0x123 #0x456)
[3 iterations] => nil
lurk-user> (> 456 123)
[3 iterations] => t
<=
(<= a b) returns t if a is less than or equal to b and nil otherwise. The arguments must be numeric. Returns <Err InvalidArg> if the types are not compatible. Note that native field elements cannot be compared like this.
lurk-user> (<= #0x123 #0x456)
[3 iterations] => t
lurk-user> (<= 123 123)
[2 iterations] => t
>=
(>= a b) returns t if a is greater than or equal to b and nil otherwise. The arguments must be numeric. Returns <Err InvalidArg> if the types are not compatible. Note that native field elements cannot be compared like this.
lurk-user> (>= #0x123 #0x456)
[3 iterations] => nil
lurk-user> (>= 123 123)
[2 iterations] => t
The REPL
Let's explore more of this tool we've been interacting with, the Lurk REPL.
Meta commands
Until now, every Lurk expression we've evaluated was evaluated under an empty environment.
Trying to evaluate a dangling a would trigger an error indicating an unbound variable.
lurk-user> a
[1 iteration] => <Err UnboundVar>
But we can alter the REPL's environment by using what we call meta commands.
In particular, we can use the def meta command.
lurk-user> !(def a (+ 1 1))
a
lurk-user> a
[1 iteration] => 2
We mark meta commands with a ! before opening parentheses.
There are multiple meta commands available in the REPL.
We're not going to be exhaustive here because there's a help meta command.
lurk-user> !(help)
Available commands:
assert - Asserts that an expression doesn't reduce to nil.
assert-emitted - Asserts that the evaluation of an expr emits expected values
assert-eq - Assert that two expressions evaluate to the same value.
...
And it can also provide further help on specific meta commands.
lurk-user> !(help def)
def - Extends env with a non-recursive binding.
Info:
Gets macroexpanded to (let ((<symbol> <expr>)) (current-env)).
The REPL's env is set to the result.
Format: !(def <symbol> <expr>)
Example:
!(def foo (lambda () 123))
Returns: The binding symbol
As hinted above, meta commands have return values. That's because we can build expressions that contain meta commands. The meta commands will be evaluated first, having their occurrences in the original expression replaced by their respective return values. The resulting expression is then evaluated.
lurk-user> (+ !(def b 21) b)
b
[2 iterations] => 42
When processing (+ !(def b 21) b), !(def b 21) is evaluated, which adds b to the environment and returns the symbol b.
The resulting expression is (+ b b), which, once evaluated, results in 42.
To double check which expression was evaluated, you can enter the debug mode with !(debug) (make sure to check !(help debug)!).
This is what the debug mode shows:
?0: (+ b b)
?1: b
1: b ↦ 21
!1: b ↦ 21
0: (+ b b) ↦ 42
Now, let's go over a few abstractions in order to understand some meta commands you will encounter.
Chaining callables
A callable object is either a function or a commitment to a function. For example, the following is accepted by Lurk.
lurk-user> (commit (lambda (x) (+ x 1)))
[2 iterations] => #c0x1f4971f046cd9b037eadbc3fcde177431a712e8cef82fcec9e010fc5a65891
lurk-user> (#c0x1f4971f046cd9b037eadbc3fcde177431a712e8cef82fcec9e010fc5a65891 10)
[6 iterations] => 11
Now let's talk about a specific class of callable objects: ones that can be chained.
A chainable callable, once provided with all arguments, must return a pair such that
- The first component is the result of the computation
- The second component is the next callable
To illustrate it, let's define a chainable counter.
lurk-user>
(commit (letrec ((add (lambda (counter x)
(let ((counter (+ counter x)))
(cons counter (commit (add counter)))))))
(add 0)))
[7 iterations] => #c0x64fee21bad514ff18399dfc5066caebf34acc0441c9af675ba95a998077591
And let's see what happens when we provide the argument 5 to it.
lurk-user> (#c0x64fee21bad514ff18399dfc5066caebf34acc0441c9af675ba95a998077591 5)
[14 iterations] => (5 . #c0x73c6bd6ffb74c34b7c21e83aaaf71ddf919bb2a9c93ecb43c656f8dc67060a)
We get the current counter result and the next callable (a functional commitment in this example).
So let's provide the argument 3 to this next callable.
lurk-user> (#c0x73c6bd6ffb74c34b7c21e83aaaf71ddf919bb2a9c93ecb43c656f8dc67060a 3)
[14 iterations] => (8 . #c0x67dfd6673beec5f6758e3404d74af882f66b1084adabb97bc27cba554def07)
The new result is 8 and we also get the next callable, as expected.
This process can continue indefinitely.
The background provided above should be enough to understand the chain and transition meta commands.
Lurk protocol
The Lurk protocol API is useful when a verifier party wants to be specific about what a proof must claim before checking whether it verifies or not.
Broadly speaking, a Lurk protocol is an open declaration for how the public input of a proof will be constructed.
A claim of a Lurk reduction states that an expression expr, when evaluated under an environment env, results on res.
Shortly, (expr, env) -> res.
Or, using pairs, ((expr . env) . res).
A protocol may require arguments in order to construct the expected claim.
And a protocol may also reject a proof by returning nil instead of a claim.
The last bit of information before we go over a simple example is that a protocol can also define a post-verification predicate. That's a 0-arg function that uses the protocol arguments to validate a claim after verification happens. This is useful when there's a check that needs to happen that's more expensive than verifying the proof. Such a check would fit well as a post-verification predicate.
Now let's write a protocol in which a proof is accepted iff it proves that n = n for a given n.
In Lurk terms, the claim for such a proof is that (= n n) reduces to t under the empty environment.
This shouldn't be a hard task for any prover who accepts the challenge, but it's a good starting example.
lurk-user>
!(defprotocol simple-protocol (n)
(cons
;; claim definition
(cons (cons (list '= n n) (empty-env))
t)
;; post-verification predicate is not provided
nil)
:description "(= n n) reduces to t")
(list '= n n) creates the Lurk expression (= <n> <n>) on the fly.
More on this later.
That protocol can be persisted on the file system and shared.
lurk-user> !(dump-expr simple-protocol "simple-protocol-file")
Data persisted on file `simple-protocol-file`
Some prover out there can download the protocol and load it from their file system.
lurk-user> !(defq simple-protocol !(load-expr "simple-protocol-file"))
simple-protocol
And then prove it for, say, the number 3.
lurk-user> !(prove-protocol simple-protocol "protocol-proof" 3)
Proof key: "56b674aa77c68bdc916a01c122da092f7a5fdc9fd0b13646382f80bebcbe99"
Protocol proof saved on file `protocol-proof`
Let's inspect the (cached) proof we've just created.
lurk-user> !(inspect "56b674aa77c68bdc916a01c122da092f7a5fdc9fd0b13646382f80bebcbe99")
Expr: (= 3 3)
Env: <Env ()>
Result: t
Now the prover sends the protocol-proof file to the verifier, who can verify it.
lurk-user> !(verify-protocol simple-protocol "protocol-proof")
Proof accepted by the protocol
In the example above, the post-verification predicate was not defined (set to nil).
Also, there was no restriction on the number used by the prover.
A slight variation would be to require that the number must be an u64.
lurk-user>
!(defprotocol simple-protocol (n)
(cons
(if (type-eqq 0 n)
;; return a claim if n is indeed u64
(cons (cons (list '= n n) (empty-env))
t)
;; the following nil makes the protocol reject the proof
nil)
;; again, no post-verification predicate
nil)
:description "(= n n) reduces to t")
And if some prover tries to prove it with, say, a field element instead of an u64, the REPL won't allow it.
lurk-user> !(prove-protocol simple-protocol "protocol-proof" 3n)
!Error: Pre-verification predicate rejected the input
The same check happens on the verifier side (of course!), which would be able to reject a proof generated with a maliciously edited REPL on the prover side.
Sharing proofs
The proof files created with the prove meta command showcase Lurk's proving capabilities, but they may contain information that we don't want to disclose.
lurk-user> !(def password "some password")
password
lurk-user> !(def hash (hide (bignum (commit password)) "private data"))
hash
lurk-user> !(prove (begin (open hash) t))
[4 iterations] => t
Proof key: "6e45ffb851078d6abf90a5d9b434ae34f2aad64d0e5880ca9c0189737f4a9e"
lurk-user> !(inspect "6e45ffb851078d6abf90a5d9b434ae34f2aad64d0e5880ca9c0189737f4a9e")
Expr: (begin (open hash) t)
Env: <Env ((hash . #c0x145c99908adac10ee79eb5e1d74ad8fe42c10abe79f5ef3d5dbb96915cc7a3) (password . "some password"))>
Result: t
See above that the binding for password is visible in the claim's environment.
Thus, such proof files are not meant to be shared.
The safe way to share proofs is using the protocol API mentioned above, which creates proof files designed to be shared. This is because protocol proofs carry just enough information for the verifier to reconstruct the entire claim, and do not include unnecessary (and potentially private) information from the prover's REPL environment.