Hi, this is my project, though I wasn't expecting to see it here just now. I gave some quick (probably too quick) answers below, and I'm happy to try to answer further questions anyone might have. It's a bit of a strange problem domain so might be hard to orient to what's even going on here if you're not already somewhat familiar. I have to step away for a little while now, but I'll check in later and try to address any questions/comments that emerge in the meantime.
noman-land 43 days ago [-]
I've been following this space with extreme fascination from the perspective of a software engineer with no formal mathematics study so please take my questions with a grain of salt.
My understanding is that a SNARK circuit is used to prove a series of computations without revealing any of the inputs or outputs.
For example some people submit their salaries in encrypted form through a compiled zk circuit and receive an encrypted answer on the other side that that tells them which person earns the most money without revealing who earns what.
Is my understanding correct that lurk would be used instead of something like circom where circom can create simple arithmetic zk circuits, whereas lurk can create circuits that can describe arbitrary computations?
> Lurk constructs compound data using SNARK-friendly Poseidon hashes (provided by Neptune), so its data is naturally content-addressable.
So lurk programs can point to previously proven (and published?) hashes to make provable claims about their calculations?
Is this like "merkle-izing" computation?
Sorry I'm just really trying to wrap my head around this.
sterlind 43 days ago [-]
not OP or a crypto expert, but:
yes, zk-SNARKs are useful because you can prove you executed a program without revealing inputs or outputs.
you can't send encrypted inputs to a zk-SNARK program and get encrypted outputs out, though. you're confusing this with homomorphic encryption.
iirc, with Lurk you could, say, convince someone you'd correctly solved a difficult NP-complete problem, by writing a Lurk program that validates a solution to that problem, and publishing the output (Solved) along with the proof steps without revealing your answer.
you could, theoretically, write an homomorphic encryption library in Lurk, and then when people send you their encrypted inputs you can send them encrypted outputs along with a proof you faithfully evaluated the FHE circuit.
this is actually missing from FHE - a malicious evaluator can do whatever the hell they want with your input data, or make up outputs completely, they just can't see what's inside.
that seems pretty neat to me actually, I wonder if the Lurk people are thinking about this. niche but it'd have its uses.
porcuquine 43 days ago [-]
> you can't send encrypted inputs to a zk-SNARK program and get encrypted outputs out, though. you're confusing this with homomorphic encryption.
Not encrypted, but they can be 'hidden'. For example the input to one computation might have been the output of another — and might be entirely opaque. (For example, the hash corresponding to `(this is a list of data 1 2 3 9873)` will include 32 bytes of data from which it's impossible to compute the original expression unless you already know it.
> that seems pretty neat to me actually, I wonder if the Lurk people are thinking about this. niche but it'd have its uses.
We are thinking about it, and Lurk would lend itself well to expressing FHE programs. One of our team members has an academic background in FHE, and we're interested in such problems. It's not our top priority right now, but it's a natural area to explore when the core language is more mature.
emmorais 43 days ago [-]
Proving correct evaluation of FHE circuits is indeed a nice example of how Lurk can help. We are considering different possibilities regarding FHE, but not as a priority.
porcuquine 43 days ago [-]
> My understanding is that a SNARK circuit is used to prove a series of computations without revealing any of the inputs or outputs.
Close: the so-called 'public inputs' must be revealed because these are checked by the verifier. What's neat is that many (even 'most') of the so-called 'private inputs' need not be revealed. This lets you prove statements that have the form, "I know of secret values x, y, z, etc. such that the following arithmetic relationship holds: [statement including public and private inputs]." One of Lurk's contributions is that this 'statement' can express arbitrary computation, including anything requiring unbounded recursion. That's what makes it Turing complete. A traditional SNARK circuit is expressive enough to describe any computation, but the limitation on requiring a fixed size means you have to know (and are limited by) an upper bound on the size of the computation in advance.
> Is my understanding correct that lurk would be used instead of something like circom where circom can create simple arithmetic zk circuits, whereas lurk can create circuits that can describe arbitrary computations?
Yes, exactly. You can construct an arbitrary program (say `((lambda (x) (* x x)) public-input)`) and pass that whole expression to the verifier. The prover can then provide the claimed result, which will also be a public input to the verifier, along with a proof that the 'input' evaluates (according to Lurk semantics) to the 'output'. Note that both what I called 'input' and 'output' will be public-inputs used by the verifier.
> So lurk programs can point to previously proven (and published?) hashes to make provable claims about their calculations?
Yes, that is one use case. Take the example above: the whole lambda expression I gave as an input example will actually be represented as a 'hash' (a content-address for the complete expression). But the 'interesting' part of the function doesn't actually have to have been given to the verifier. Instead, the prover might have committed to this function previously. The prover then 'opens' the commitment on the provided input. This is possible because the verifier can construct the 'hash' corresponding to the 'input' without knowing the internal hashes of the entire expression. The verifier might only know she is verifying a statement of the form `(<secret function> public-input)`. But she still knows that the claimed output is indeed an evaluation of the pre-committed secret function because she trusts the cryptographic proof.
The initial example took advantage of the fact that all compound Lurk data is produced by hashing anyway.
> Is this like "merkle-izing" computation?
You merkle-ize the recipe/program. The computation itself is performed normally (by the prover), but only needs to happen once. Thereafter any number of verifiers can 'check the prover's work' and see that it was performed correctly. Both the input and output to the computation proven can be merkle roots — so the amount of private versus public data can be tuned to the needs of the application.
> Sorry I'm just really trying to wrap my head around this.
It's a lot to grok and takes a while (but not too bad if you're really interested). If you follow us on Twitter (https://twitter.com/LurkLab) you'll see when we publish some blog posts in which I hope to walk through examples like this in a lot more detail. That should give a very concrete sense for what is possible and what is involved from a programmer perpsective.
porcuquine 43 days ago [-]
FYI, I will be in transit for much of today so may find further responses difficult (but I will try). I'm hoping others with knowledge of the project might pop in to answer more questions that might arise or provide other detail. If not, this was fun. Thank you, and do follow on Twitter (https://twitter.com/LurkLab) if you want to stay in the loop. We hope to publish some blog posts with concrete examples and usage soon.
tromp 43 days ago [-]
How hard would it be to prove correctness of the root HASH of a merkle tree of N signatures over some CURVE, in terms of proof size, proof construction time, proof verification time, in the following cases?
HASH = SHA256/blake2b, CURVE = secp256k1, N = 10^6
HASH = SHA256/blake2b, CURVE = secp256k1, N = 10^9
HASH = Poseidon, CURVE = SNARK-friendly, N = 10^9
emmorais 43 days ago [-]
Proof size and verification time would be constant (therefore efficient) for all cases. Not using a friendly signature scheme would in principle cause a big increase in proving time. The same situation happens if you want to use something different from Poseidon. But we are designing an improvement to the architecture that allows to deal with such cases, shortly by constructing specialized co-processors. However, it is not yet clear how it would affect performance in practice, but the goal is exactly to improve it significantly.
tromp 43 days ago [-]
Yes, I'm asking for the rough sizes of these constants, i.e. order of magnitude.
Is proof size for the first case closer to 1MB or 10MB? Is verification time closer to 1s, 10s, 100s, or 1000s?
emmorais 43 days ago [-]
It depends on which backend you want to use (currently Groth16 or Nova, but more options can be implemented). For example, Nova proof is roughly 8-9 KB. In this situation we have that verification is not constant, for instance, for 2^20 constraints it would take roughly 1s.
tromp 43 days ago [-]
And how many constraints would roughly be needed to represent the first case of a million secp256k1 signatures in a SHA256 Merkle tree?
medo-bear 43 days ago [-]
hi this is very interesting. why is there a common lisp and rust version? digging through i also found Alu [0], another common lisp project for zk circuits. since you are using common lisp and static typing is important to you are you aware of coalton [1]?
Nice, I'll have to take a look at Alu. I'm also aware of Coalton. It's very cool in principle, though I have not used it (yet?).
The original proof-of-concept was written in Common Lisp, and development of core language features often happens in that version. It's more flexible for rapid development, and the 'API' can be taken it at a glance a bit more simply. Having multiple implementations also has the benefit of keeping us honest (at the cost of some hopefully-ephemeral drift and maintenance).
ecesena 44 days ago [-]
Any reason to build from scratch vs contributing to arkworks?
porcuquine 44 days ago [-]
Arkworks isn't really addressing the core of what Lurk provides. In theory, we could use Arkworks to implement a backend — but we are targeting Nova (https://github.com/microsoft/Nova), and I don't think Arkworks supports Nova currently. So the part we are building from scratch (the language itself) is at a higher level of abstraction. We like Nova's characteristics and are actively helping with aspects of its implementation so we can use it as soon as possible.
ecesena 43 days ago [-]
Great, thank you for the details!
diggan 44 days ago [-]
Multiple interesting features:
- Lurk program execution can be proved in zero knowledge.
- Lurk proofs support multiple backend SNARK proving systems.
- Lurk enables incremental computation and proofs in unbounded loops.
- Lurk provides conditional control flow.
- Lurk programs are data and vice versa.
- Lurk data is content-addressable for compatibility with IPLD/IPFS.
That it's a lisp just makes it all better as well.
Here's a Fibonacci example:
;; (FIB TARGET) computes the element of the Fibonacci sequence at TARGET (zero-indexed).
(letrec ((next (lambda (a b n target)
(if (eq n target)
a
(next b
(+ a b)
(+ 1 n)
target))))
(fib (next 0 1 0)))
(fib 1))
tylersmith 44 days ago [-]
Generally recursive here means that the program is verifying previous proofs from the program. I'm trying to understand how this fits in here wrt to the recursive function.
porcuquine 44 days ago [-]
It's confusing because there are two distinct 'recursive things' involved. You may be noting that distinction.
On the one hand, Lurk allows expression of recursive computations (like in the cited example). This doesn't necessarily demand 'verifying previous proofs' (in proofs). However, recursive SNARKs (where proofs of proofs are verified ad infinitum) are useful for actually producing a single succinct proof of a potentially unbounded recursive computation.
So there is a practical relationship between the two recursive aspects, but they're not strictly the same thing. This is indeed a bit of a confusing subtlety.
noman-land 43 days ago [-]
So you could do a collaborative computation of a particular index in fibonacci by taking turns computing up to a certain index, getting the hash and handing it off like a baton to someone else who could prove the starting value they're given is correct for the starting index and then keep going?
porcuquine 43 days ago [-]
Yep, that's a perfect minimal example of the kind of thing we could do. Exactly how to 'extend' the computation depends on how it's set up. What you describe is possible, as are more elaborate applications in which the 'result so far' includes a log of all previous results (basically a memoized table of the recursive computation so far). If you have a proof that the merkle root of this table is correct, then you can just look up any so-far-known value.
Taken to its extreme, this could be used to produce a collective database reducing arbitrary deterministic functions to lookup — what I think of as 'compute-addressable' (riffing on content-addressable) data. Since Lurk can express arbitrary computation in its own data language, such a universal database wouldn't strictly require per-function circuits (though for performance, some customization will help).
noman-land 43 days ago [-]
So incredibly cool. I've been thinking about a use case for the 'result so far' mechanic and I've been trying to figure out how to build it. Perhaps I'll give lurk a try :). Are you on any zk chat channels on matrix/telegram/discord/etc? Would love to chat more about this.
tylersmith 43 days ago [-]
The term you want to look into is Incrementally Verifiable Computation.
I wonder how this compares to something like zexe (https://github.com/brucechin/zexe). This domain interests me although I have little practical knowledge/experience in it.
porcuquine 44 days ago [-]
ZEXE has one layer of recursive composition, so you can effectively verify proofs in a proof – but not proofs of those proofs. Lurk initially targets Nova for unbounded recursion.
0xcb0 43 days ago [-]
Just wow! This sounds very interesting and I can think of lots of applications this could be useful in. And even the facts that it is in LISP makes it so cool!
Thanks @porcuquine for the hard work you are putting in here!
masukomi 43 days ago [-]
for those of you who, like me, had no clue what a ZK-SNARK was/is
> Zk-SNARK is an acronym that stands for “Zero-Knowledge Succinct Non-Interactive Argument of Knowledge.” A zk-SNARK is a cryptographic proof that allows one party to prove it possesses certain information without revealing that information. This proof is made possible using a secret key created before the transaction takes place. It is used as part of the protocol for the cryptocurrency, Zcash.
I'm not otherwise familiar with it, but the landing page linked describes Pact as 'a Turing-incomplete smart contract language'. Lurk could be used to implement smart contracts (with some glue connecting it to a blockchain — as we plan to do for the FVM), and we believe its characteristics will allow interesting applications in that domain. However, it's not inherently a 'smart contract language'.
It looks like Pact considers Turing-incompleteness a benefit, since it makes it easier to reason about the cost of programs in a blockchain context. I don't see mention of zero-knowledge or succinct proofs, which are some of the more 'interesting' features of Lurk. For example, in a blockchain context, costs associated with program running time are less relevant for Lurk programs executed on chain because verification costs aren't affected by the running time of the program. All proofs created by a concrete instance of the language are verifiable in constant time. This is an example of how Turing-completeness and succinct proofs provide complementary benefits.
It looks like Pact has a Lispy syntax and immutable data, so they seem to have that in common.
osense 43 days ago [-]
Can someone provide a good real-world usecase for zero-knowledge proofs? I struggle a bit with grasping the usefulness of this concept.
b_fiive 43 days ago [-]
zero-knowledge proofs are a means of showing you know a thing without exposing the thing itself.
In the context of lurk, the "thing" is executed computation. That's useful because sometimes computation is expensive, and we'd like to run that expensive computation, anywhere, once, and be able to re-use the result.
osense 42 days ago [-]
Thank you!
sshine 43 days ago [-]
What’s a zk-SNARK without a trusted setup?
I thought zk-STARKs addressed this, but it seems like you’re continuing with a circuit model.
porcuquine 43 days ago [-]
Nova (for example) doesn't require a trusted setup. The circuit is just a schematic description of the underlying computation. In the case of the Lurk core language, this computation is 'one reduction step of a Lurk evaluation' (https://github.com/lurk-lang/lurk-rs/blob/master/spec/reduct...). Coming up with a 'fixed computation' that yields general computation is part of the design problem for Lurk (or any other Lurk-like language). Even if we did need a per-circuit trusted setup (which we don't), we could perform such a setup for our core circuit and use it to prove arbitrary programs. For example, although we have not actually performed the trusted setup, we do have an example using Groth16 (which does require a trusted setup to be secure) and aggregates the potentially many discrete reduction steps to produce a succinct proof.
emmorais 43 days ago [-]
Indeed zk-STARK addresses it, but it is not the only alternative (Bulletproofs, Nova, Halo2 also doesn't require a trusted setup). All zk-SNARKs need some kind of intermediate representation that looks like a circuit, then this characteristic has nothing to do with the trusted setup requirement.
My understanding is that a SNARK circuit is used to prove a series of computations without revealing any of the inputs or outputs.
For example some people submit their salaries in encrypted form through a compiled zk circuit and receive an encrypted answer on the other side that that tells them which person earns the most money without revealing who earns what.
Is my understanding correct that lurk would be used instead of something like circom where circom can create simple arithmetic zk circuits, whereas lurk can create circuits that can describe arbitrary computations?
> Lurk constructs compound data using SNARK-friendly Poseidon hashes (provided by Neptune), so its data is naturally content-addressable.
So lurk programs can point to previously proven (and published?) hashes to make provable claims about their calculations?
Is this like "merkle-izing" computation?
Sorry I'm just really trying to wrap my head around this.
yes, zk-SNARKs are useful because you can prove you executed a program without revealing inputs or outputs.
you can't send encrypted inputs to a zk-SNARK program and get encrypted outputs out, though. you're confusing this with homomorphic encryption.
iirc, with Lurk you could, say, convince someone you'd correctly solved a difficult NP-complete problem, by writing a Lurk program that validates a solution to that problem, and publishing the output (Solved) along with the proof steps without revealing your answer.
you could, theoretically, write an homomorphic encryption library in Lurk, and then when people send you their encrypted inputs you can send them encrypted outputs along with a proof you faithfully evaluated the FHE circuit.
this is actually missing from FHE - a malicious evaluator can do whatever the hell they want with your input data, or make up outputs completely, they just can't see what's inside.
that seems pretty neat to me actually, I wonder if the Lurk people are thinking about this. niche but it'd have its uses.
Not encrypted, but they can be 'hidden'. For example the input to one computation might have been the output of another — and might be entirely opaque. (For example, the hash corresponding to `(this is a list of data 1 2 3 9873)` will include 32 bytes of data from which it's impossible to compute the original expression unless you already know it.
> that seems pretty neat to me actually, I wonder if the Lurk people are thinking about this. niche but it'd have its uses.
We are thinking about it, and Lurk would lend itself well to expressing FHE programs. One of our team members has an academic background in FHE, and we're interested in such problems. It's not our top priority right now, but it's a natural area to explore when the core language is more mature.
Close: the so-called 'public inputs' must be revealed because these are checked by the verifier. What's neat is that many (even 'most') of the so-called 'private inputs' need not be revealed. This lets you prove statements that have the form, "I know of secret values x, y, z, etc. such that the following arithmetic relationship holds: [statement including public and private inputs]." One of Lurk's contributions is that this 'statement' can express arbitrary computation, including anything requiring unbounded recursion. That's what makes it Turing complete. A traditional SNARK circuit is expressive enough to describe any computation, but the limitation on requiring a fixed size means you have to know (and are limited by) an upper bound on the size of the computation in advance.
> Is my understanding correct that lurk would be used instead of something like circom where circom can create simple arithmetic zk circuits, whereas lurk can create circuits that can describe arbitrary computations?
Yes, exactly. You can construct an arbitrary program (say `((lambda (x) (* x x)) public-input)`) and pass that whole expression to the verifier. The prover can then provide the claimed result, which will also be a public input to the verifier, along with a proof that the 'input' evaluates (according to Lurk semantics) to the 'output'. Note that both what I called 'input' and 'output' will be public-inputs used by the verifier.
> So lurk programs can point to previously proven (and published?) hashes to make provable claims about their calculations?
Yes, that is one use case. Take the example above: the whole lambda expression I gave as an input example will actually be represented as a 'hash' (a content-address for the complete expression). But the 'interesting' part of the function doesn't actually have to have been given to the verifier. Instead, the prover might have committed to this function previously. The prover then 'opens' the commitment on the provided input. This is possible because the verifier can construct the 'hash' corresponding to the 'input' without knowing the internal hashes of the entire expression. The verifier might only know she is verifying a statement of the form `(<secret function> public-input)`. But she still knows that the claimed output is indeed an evaluation of the pre-committed secret function because she trusts the cryptographic proof.
We have an example project dealing with exactly this situation. The examples need a lot of work, but you can see the idea here: https://github.com/lurk-lang/lurk-rs/tree/master/fcomm
This WIP commit adapts the example to use a more explicit form of commitments and should make clearer what's going on: https://github.com/lurk-lang/lurk-rs/pull/112/files#diff-d6b...
The initial example took advantage of the fact that all compound Lurk data is produced by hashing anyway.
> Is this like "merkle-izing" computation?
You merkle-ize the recipe/program. The computation itself is performed normally (by the prover), but only needs to happen once. Thereafter any number of verifiers can 'check the prover's work' and see that it was performed correctly. Both the input and output to the computation proven can be merkle roots — so the amount of private versus public data can be tuned to the needs of the application.
> Sorry I'm just really trying to wrap my head around this.
It's a lot to grok and takes a while (but not too bad if you're really interested). If you follow us on Twitter (https://twitter.com/LurkLab) you'll see when we publish some blog posts in which I hope to walk through examples like this in a lot more detail. That should give a very concrete sense for what is possible and what is involved from a programmer perpsective.
HASH = SHA256/blake2b, CURVE = secp256k1, N = 10^6
HASH = SHA256/blake2b, CURVE = secp256k1, N = 10^9
HASH = Poseidon, CURVE = SNARK-friendly, N = 10^9
[0] https://github.com/heliaxdev/alu
[1] https://coalton-lang.github.io/
The original proof-of-concept was written in Common Lisp, and development of core language features often happens in that version. It's more flexible for rapid development, and the 'API' can be taken it at a glance a bit more simply. Having multiple implementations also has the benefit of keeping us honest (at the cost of some hopefully-ephemeral drift and maintenance).
- Lurk program execution can be proved in zero knowledge.
- Lurk proofs support multiple backend SNARK proving systems.
- Lurk enables incremental computation and proofs in unbounded loops.
- Lurk provides conditional control flow.
- Lurk programs are data and vice versa.
- Lurk data is content-addressable for compatibility with IPLD/IPFS.
That it's a lisp just makes it all better as well.
Here's a Fibonacci example:
On the one hand, Lurk allows expression of recursive computations (like in the cited example). This doesn't necessarily demand 'verifying previous proofs' (in proofs). However, recursive SNARKs (where proofs of proofs are verified ad infinitum) are useful for actually producing a single succinct proof of a potentially unbounded recursive computation.
So there is a practical relationship between the two recursive aspects, but they're not strictly the same thing. This is indeed a bit of a confusing subtlety.
Taken to its extreme, this could be used to produce a collective database reducing arbitrary deterministic functions to lookup — what I think of as 'compute-addressable' (riffing on content-addressable) data. Since Lurk can express arbitrary computation in its own data language, such a universal database wouldn't strictly require per-function circuits (though for performance, some customization will help).
Thanks @porcuquine for the hard work you are putting in here!
> Zk-SNARK is an acronym that stands for “Zero-Knowledge Succinct Non-Interactive Argument of Knowledge.” A zk-SNARK is a cryptographic proof that allows one party to prove it possesses certain information without revealing that information. This proof is made possible using a secret key created before the transaction takes place. It is used as part of the protocol for the cryptocurrency, Zcash.
more details here: https://www.investopedia.com/terms/z/zksnark.asp
[0] https://github.com/kadena-io/pact
It looks like Pact considers Turing-incompleteness a benefit, since it makes it easier to reason about the cost of programs in a blockchain context. I don't see mention of zero-knowledge or succinct proofs, which are some of the more 'interesting' features of Lurk. For example, in a blockchain context, costs associated with program running time are less relevant for Lurk programs executed on chain because verification costs aren't affected by the running time of the program. All proofs created by a concrete instance of the language are verifiable in constant time. This is an example of how Turing-completeness and succinct proofs provide complementary benefits.
It looks like Pact has a Lispy syntax and immutable data, so they seem to have that in common.
In the context of lurk, the "thing" is executed computation. That's useful because sometimes computation is expensive, and we'd like to run that expensive computation, anywhere, once, and be able to re-use the result.
I thought zk-STARKs addressed this, but it seems like you’re continuing with a circuit model.