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
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 varible 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))
[54 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)))
[76 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
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] => #c0x4a902d7be96d1021a473353bd59247ea4c0f0688b5bae0c833a1f624b77ede
Now Lurk knows that #c0x4a902d7be96d1021a473353bd59247ea4c0f0688b5bae0c833a1f624b77ede is a commitment to 123 and can successfully open it.
lurk-user> (open #c0x4a902d7be96d1021a473353bd59247ea4c0f0688b5bae0c833a1f624b77ede)
[2 iterations] => 123
Lurk understands it if you use big nums in an open expression directly.
lurk-user> (open #0x4a902d7be96d1021a473353bd59247ea4c0f0688b5bae0c833a1f624b77ede)
[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] => #c0x2d42d50c445fe7021003b9d177e09e93008f97f74eea0f1c61c3f27aec104f
For when hiding is unimportant, commit creates commitments with a default secret of #0x0.
lurk-user> (hide #0x0 123)
[3 iterations] => #0x4a902d7be96d1021a473353bd59247ea4c0f0688b5bae0c833a1f624b77ede
And both hashes above open to the same value 123.
lurk-user> (open #0x4a902d7be96d1021a473353bd59247ea4c0f0688b5bae0c833a1f624b77ede)
[2 iterations] => 123
lurk-user> (open #c0x2d42d50c445fe7021003b9d177e09e93008f97f74eea0f1c61c3f27aec104f)
[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] => #c0x8b10a9e88372ee05aea4230b21d7ed9b9e4b1d7f9d2a056d125172ad07c4fc
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 #c0x8b10a9e88372ee05aea4230b21d7ed9b9e4b1d7f9d2a056d125172ad07c4fc) 5)
[8 iterations] => 32
lurk-user> ((open #c0x8b10a9e88372ee05aea4230b21d7ed9b9e4b1d7f9d2a056d125172ad07c4fc) 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] => #c0x759b94bccb5545915690c4e847e0f3e5e42c732eafcc02cbcd55ac50066c9b
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 #c0x759b94bccb5545915690c4e847e0f3e5e42c732eafcc02cbcd55ac50066c9b)
(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
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] => #0x8f1deaa5f6031277a6a5a7e0f35f15ef42da64b1e203769982da26038f1e25
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] => #c0x8f1deaa5f6031277a6a5a7e0f35f15ef42da64b1e203769982da26038f1e25
lurk-user> (open #c0x8f1deaa5f6031277a6a5a7e0f35f15ef42da64b1e203769982da26038f1e25)
[3 iterations] => 1
lurk-user> (secret #c0x8f1deaa5f6031277a6a5a7e0f35f15ef42da64b1e203769982da26038f1e25)
[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))
[3 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 is equal to y 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
type-eq
(type-eq x y) returns t if x and y 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 have the same type and nil otherwise. The difference is that x is treated as an un-evaluated form instead of eagerly evaluating it. This usually means x is be some constant value.
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] => #c0x7834e8081d1317cce4dd8c9098e417bbf248ac0b997772a96980c00686e7e0
lurk-user> (open #c0x7834e8081d1317cce4dd8c9098e417bbf248ac0b997772a96980c00686e7e0)
[3 iterations] => 456
lurk-user> (secret #c0x7834e8081d1317cce4dd8c9098e417bbf248ac0b997772a96980c00686e7e0)
[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.
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
let
(let ((var binding)...) body) extends the current environment with a set of variable bindings and then evaluate 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))>
letrec
(letrec ((var binding)...) body) is similar to let, but it enables recursion by allowing references to var inside its own binding. Generally, the binding is be a lambda expression representing a recursive function. See also the defrec REPL meta command.
lurk-user> (letrec ((x 1)) x)
[3 iterations] => 1
lurk-user> (letrec ((x 1)) (current-env))
[3 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)))
[19 iterations] => 3
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 (hide #0x123 2))
[4 iterations] => 2
lurk-user> (open #0x8f1deaa5f6031277a6a5a7e0f35f15ef42da64b1e203769982da26038f1e25)
[2 iterations] => 1
lurk-user> (open #c0x8f1deaa5f6031277a6a5a7e0f35f15ef42da64b1e203769982da26038f1e25)
[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 #0x7a9196fa4cb9236389fdbd2feb108986d4d668c8caad347f4334c6b147cb67)
[2 iterations] => #0x123
lurk-user> (secret #c0x7a9196fa4cb9236389fdbd2feb108986d4d668c8caad347f4334c6b147cb67)
[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 ArgNotNumber> 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 ArgNotNumber>
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 ArgNotNumber> 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 ArgNotNumber> 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 ArgNotNumber> 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 ArgNotNumber> 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 ArgNotNumber>
<
(< a b) returns t if a is strictly less than b and nil otherwise. The arguments must be numeric. Returns <Err ArgNotNumber> if the types are not compatible. Note that native field elements cannot be compared like this.
lurk-user> (< "a" "b")
[3 iterations] => <Err ArgNotNumber>
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 ArgNotNumber> 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 ArgNotNumber> 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 ArgNotNumber> 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.
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> <value>)) (current-env)).
The REPL's env is set to the result.
Usage: !(def <symbol> <value>)
Example:
!(def foo (lambda () 123))
However, we need to go over a few abstractions in order to understand some meta commands you may 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] => #c0x3a248e9776f7f49a5279269aae67a9a0eac50357406b1e1083b571fd5b2c5b
lurk-user> (#c0x3a248e9776f7f49a5279269aae67a9a0eac50357406b1e1083b571fd5b2c5b 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)))
[6 iterations] => #c0x5a34ed7712c5fd2f324feb0e1764b27bac9259c4b663e4601e678939a9363d
And let's see what happens when we provide the argument 5 to it.
lurk-user> (#c0x5a34ed7712c5fd2f324feb0e1764b27bac9259c4b663e4601e678939a9363d 5)
[13 iterations] => (5 . #c0x4a706d7701a9b79ddbffca887f38c60bd7eb38acc737b53ea631a10fff7e4b)
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> (#c0x4a706d7701a9b79ddbffca887f38c60bd7eb38acc737b53ea631a10fff7e4b 3)
[13 iterations] => (8 . #c0xf61e10e5c607c0fe0ef7cd879b6d2a6eb1ea7016fde6479e836b56ea27bf3)
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 an expensive 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 that receives a number n and proves that n = n 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 at simple-protocol-file
Some prover out there can download the protocol and load it from their file system.
lurk-user> !(load-expr simple-protocol "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: "299be6acd05ee9cc8e3687cb85b3b3cf32acf62f4be3c46995156136597966"
Protocol proof saved at protocol-proof
Let's inspect the (cached) proof we've just created.
lurk-user> !(inspect "299be6acd05ee9cc8e3687cb85b3b3cf32acf62f4be3c46995156136597966")
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: "14c6c98e3409c56139e2d3b096980bb5b6f380fc7582f69bbf61edccc13949"
lurk-user> !(inspect "14c6c98e3409c56139e2d3b096980bb5b6f380fc7582f69bbf61edccc13949")
Expr: (begin (open hash) t)
Env: <Env ((hash . #c0x51d1c3d0c5ea9d2d7d27eda6ef7ef48ad2ffd8dd80693adf06a4afeed6fd8a) (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.