Re: [zapps-wg] Zkproofs.org standards workshop
Hey Lucas, thanks for pointing this out, I've also found this to be a
missing part of C-S notation. Here's one more subtle reason to be explicit
about what are the public inputs. When you generate public parameters for a
snark scheme, some public values may be hardcoded in the circuit, while
others can be modified without changing the public parameters. Formally
speaking, the hardcoded parts define the "NP language", while the public
inputs define the "statement".
I like your suggestion. For signatures I mentioned earlier using the
bracket notation [m]. In LaTeX I have tried before using subscripts for
public inputs. So for example:
SoK[m]_H{ (x): H = hash(x) }
But this looks pretty bad in ascii compared to your suggestion. Really
curious if others have preferences, I don't have a strong opinion here.
On Sun, Apr 22, 2018 at 10:21 AM, Lucas Vogelsang via zapps-wg <
zapps...@lists.z.cash.foundation> wrote:
> Andrew, I wanted to follow up on your proposal of formulating ZkPoKs. One
> thing that was a bit counter intuitive to your notation is the fact that
> while it's very clear what private inputs a snark has, the public inputs
> are not clearly designated. E.g.:
>
> ZkPoK{ (R1, R2): H1 = sha256(R1) and H2 = sha256(R2) and R1 = R2 ^ X }
>
> This example is simple enough that a) X is easy to spot and given it's
> name it's easy to deduct that this is probably not a constant but a public
> input. However if the snark gets longer, intermediary variables (just local
> to the snark) and public inputs are hard to discern. Perhaps it would be
> convenient to write it with the following syntax:
>
> ZkPoK{ W = {R1, R2}, I = {X}: H1 = sha256(R1) and H2 = sha256(R2) and R1 =
> R2 ^ X }
>
> Have you put any thought into this already? Comparing your notation to
> Izaak's pseudocode, I think there is a right time and place for both.
> Although perhaps by the time you're using your proposed syntax, Izaak, it
> might be easier to just write it in snarky, don't you agree?
>
> Lucas
>
> On Mon, Mar 26, 2018 at 6:10 PM, Izaak Meckler via zapps-wg <
> zapps...@lists.z.cash.foundation> wrote:
>
>> One application that I like: sending ads with a proof proving they were
>> generated by some algorithm that is known not to have access to personal
>> data.
>>
>> And I like that notation Andrew -- there is a sort of extension to it
>> (which is basically the idea of snarky) which involves not having to
>> declare all your witnesses up front. The main advantage over
>> the Camenisch-Stadler notation to my mind is modularity/abstraction. (For
>> example, you can factor out the idea of opening a commitment).
>>
>> This is a bit of a contrived example but to get the idea across,
>> "sumCommitmentsIsZero" proves that you know openings to a bunch of
>> commitments such that the openings sum to 0, say.
>>
>> def openCommitment(c):
>> (value, nonce) = *exists* OpenCommitment(c);
>> *assert* SHA256(value, nonce) = c;
>> return value
>>
>> def sumCommitmentsIsZero(cs):
>> *assert* sum(map cs (fun c -> openCommitment(c))) = 0
>>
>> (sometimes I call exists "request" instead.)
>>
>> If this sort of notation was widely used, people would probably know what
>> you meant when you wrote openCommitment as a function, and so you could
>> just write the second definition in communicating. There are a bunch of
>> other reusable abstractions that arise in zk-proof programming that we
>> could build up a shared vocabulary for as well to make communicating this
>> stuff easier.
>>
>> On Sat, Mar 24, 2018 at 4:05 PM, Andrew Miller via zapps-wg <
>> zapps...@lists.z.cash.foundation> wrote:
>>
>>> Lucas's post reminded me of something I wanted to post about:
>>> If there's one thing I'd like to take up the torch for and advocate as a
>>> standard, it's to use a conventional pseudocode for describing snark
>>> application ideas. What I have in mind is Camenisch-Stadler proof
>>> notation. It looks like this:
>>>
>>> ZkPoK{ (witness): Predicate(statement, witness) }
>>>
>>> The idea is that "witness" is the private witness, "statement" is
>>> public information that the verifier provides, and you replace
>>> "Predicate" with whatever pseudocode you want to check.
>>> Here are some examples:
>>>
>>> 1. Pay-to-Sudoku:
>>> ZkPoK{ (solution, nonce):
>>> SHA2(nonce || solution) == H,
>>> CheckSudokuSolution(puzzleBoard, solution) == 1 }
>>>
>>> 2. Show two hashes have related preimages:
>>>
>>> ZkPoK{ (R1, R2): H1 = sha256(R1) and H2 = sha256(R2) and R1 = R2 ^ X }
>>>
>>> https://github.com/ebfull/lightning_circuit/blob/master/README.md
>>>
>>> This notation is a starting point, it can be extended to say a
>>> Signature-of-Knowledge, like in BabyZoe (a simplified form of ZSL,
>>> where the only shielded operation is to withdraw 1.0 coin from the
>>> shielded pool):
>>>
>>> 3. SoK[tx]{ (secretkey, Com, merkleProof):
>>>// Com is included in the commitment tree
>>>MerkleVerify(coinTree, merkleProof, Com),
>>>Com is a commitment
Re: [zapps-wg] Zkproofs.org standards workshop
Andrew, I wanted to follow up on your proposal of formulating ZkPoKs. One
thing that was a bit counter intuitive to your notation is the fact that
while it's very clear what private inputs a snark has, the public inputs
are not clearly designated. E.g.:
ZkPoK{ (R1, R2): H1 = sha256(R1) and H2 = sha256(R2) and R1 = R2 ^ X }
This example is simple enough that a) X is easy to spot and given it's name
it's easy to deduct that this is probably not a constant but a public
input. However if the snark gets longer, intermediary variables (just local
to the snark) and public inputs are hard to discern. Perhaps it would be
convenient to write it with the following syntax:
ZkPoK{ W = {R1, R2}, I = {X}: H1 = sha256(R1) and H2 = sha256(R2) and R1 =
R2 ^ X }
Have you put any thought into this already? Comparing your notation to
Izaak's pseudocode, I think there is a right time and place for both.
Although perhaps by the time you're using your proposed syntax, Izaak, it
might be easier to just write it in snarky, don't you agree?
Lucas
On Mon, Mar 26, 2018 at 6:10 PM, Izaak Meckler via zapps-wg <
zapps...@lists.z.cash.foundation> wrote:
> One application that I like: sending ads with a proof proving they were
> generated by some algorithm that is known not to have access to personal
> data.
>
> And I like that notation Andrew -- there is a sort of extension to it
> (which is basically the idea of snarky) which involves not having to
> declare all your witnesses up front. The main advantage over
> the Camenisch-Stadler notation to my mind is modularity/abstraction. (For
> example, you can factor out the idea of opening a commitment).
>
> This is a bit of a contrived example but to get the idea across,
> "sumCommitmentsIsZero" proves that you know openings to a bunch of
> commitments such that the openings sum to 0, say.
>
> def openCommitment(c):
> (value, nonce) = *exists* OpenCommitment(c);
> *assert* SHA256(value, nonce) = c;
> return value
>
> def sumCommitmentsIsZero(cs):
> *assert* sum(map cs (fun c -> openCommitment(c))) = 0
>
> (sometimes I call exists "request" instead.)
>
> If this sort of notation was widely used, people would probably know what
> you meant when you wrote openCommitment as a function, and so you could
> just write the second definition in communicating. There are a bunch of
> other reusable abstractions that arise in zk-proof programming that we
> could build up a shared vocabulary for as well to make communicating this
> stuff easier.
>
> On Sat, Mar 24, 2018 at 4:05 PM, Andrew Miller via zapps-wg <
> zapps...@lists.z.cash.foundation> wrote:
>
>> Lucas's post reminded me of something I wanted to post about:
>> If there's one thing I'd like to take up the torch for and advocate as a
>> standard, it's to use a conventional pseudocode for describing snark
>> application ideas. What I have in mind is Camenisch-Stadler proof
>> notation. It looks like this:
>>
>> ZkPoK{ (witness): Predicate(statement, witness) }
>>
>> The idea is that "witness" is the private witness, "statement" is
>> public information that the verifier provides, and you replace
>> "Predicate" with whatever pseudocode you want to check.
>> Here are some examples:
>>
>> 1. Pay-to-Sudoku:
>> ZkPoK{ (solution, nonce):
>> SHA2(nonce || solution) == H,
>> CheckSudokuSolution(puzzleBoard, solution) == 1 }
>>
>> 2. Show two hashes have related preimages:
>>
>> ZkPoK{ (R1, R2): H1 = sha256(R1) and H2 = sha256(R2) and R1 = R2 ^ X }
>>
>> https://github.com/ebfull/lightning_circuit/blob/master/README.md
>>
>> This notation is a starting point, it can be extended to say a
>> Signature-of-Knowledge, like in BabyZoe (a simplified form of ZSL,
>> where the only shielded operation is to withdraw 1.0 coin from the
>> shielded pool):
>>
>> 3. SoK[tx]{ (secretkey, Com, merkleProof):
>>// Com is included in the commitment tree
>>MerkleVerify(coinTree, merkleProof, Com),
>>Com is a commitment to (secretkey, Nullifier)
>> }
>>
>> Notes on BabyZoe:
>> https://github.com/zcash-hackworks/babyzoe/blob/master/talks
>> /2016-07-27-IC3---SNARKs-for-Ethereum.pdf
>>
>> To take a stab at translating the snark-based password authentication
>> idea into this pseudocode, I think it could look like this:
>>
>> 4. SoK[signedMessage]{ (derivedkey):
>> username = SHA256(addrContract, derivedkey)
>> }
>>
>> The user would then use standard PBKDF2 from something like:
>>derivedKey := Argon2(addrContract, password)
>>
>> so the snark circuit itself doesn't even have to have the expensive
>> hash. The smart contract would use the final password hash as the
>> username.
>>
>> On Sat, Mar 24, 2018 at 4:47 PM, Andrew Miller
>> wrote:
>> > That's awesome Lucas, thanks for this input, these are pretty cool
>> > application scenarios. They're all quite relevant to a standards effort
>> > because they seem to involve interfacing between zkSNARKs and other
>> > standardized primitives (password hash functions, anonymous credenti
