3 ms·

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

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 4y 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 4y 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 4y 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 4y 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. 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 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-d6b7cb0011165792c926743571d238d105980d90d941cc97abf1f6821aa094db 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 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.

sterlind 4y 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 4y 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 4y 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 4y 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. 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 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-d6b7cb0011165792c926743571d238d105980d90d941cc97abf1f6821aa094db 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 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.