Refactor Public Inputs and add them to the transcript

[davidnevadoc]

In this PR we have added the Public Inputs to the transcript as the first step of the prove and verify algorithms. They have been added as the evaluations of the PI polynomial over the used domain (n field elements).

Close #133

[davidnevadoc]

This method may not be best way of solving the issue so discussions on alternative solutions are welcome!

[ghost]

Halo 2 also includes the circuit description in the transcript, which I think is another good level of defense in depth. In general, my understanding of the Trail of Bits recommendation is that pretty much everything the verifier has access to should go in the transcript.

[ghost]

Per Alistair's suggestion on ZK study club telegram, it's not a bad idea to add the first element of the KZG SRS to the transcript as well. This is a bit tricky as it's not generic over the poly commit scheme

[CPerezz]

I agree with @hdevalence since leaking memory on purpose is clearly an indicator that something is not correct.

I don't really see any other way anyways. The only thing that would mitigate the leaking stuff is to hash up all of the PI's and add that to the transcript. I agree that would make the verifier work more. But at the same time only forces us to leak a single Box which contains all of the PI's hashed instead of each one of them. Maybe we could even reserve a 32-byte array and unsafely modify it when PI's are passed so that no leaking happens.

Otherways we will need to allocate one byte-array slot for each PI which makes it much more complex.. WDYT @davidnevadoc @joebebel @bhgomes ?

[ghost]

I don't really see any other way anyways. The only thing that would mitigate the leaking stuff is to hash up all of the PI's and add that to the transcript. I agree that would make the verifier work more. But at the same time only forces us to leak a single Box which contains all of the PI's hashed instead of each one of them. Maybe we could even reserve a 32-byte array and unsafely modify it when PI's are passed so that no leaking happens.

We should to do something like @hdevalence suggested, which means that user configured parts of the proving system (including input length) are handled separately in some way before passing to merlin. This isn't really a "how to code it?" question; it's more a question of how we ensure that the protocol and transcript are well-formed, which merlin will handle for us to some extent.

For example, there is another problem with the code (besides the Box::leak distraction) - it violates the property that no label is a prefix of another label. While not necessarily being related to the runtime vs compile time issue, this is a good example of why this is rather difficult to get correct. Every time the "protocol" changes (which in merlin-terms includes the label set) there is potential risk, so merlin is designed (correctly) to nudge everyone away from "runtime" protocol changes, even ones that are technically safe, and to handle runtime variation above the merlin layer.

So instead the "static protocol" (from merlin's perspective) needs to be general enough to handle runtime variation. We have to verify that the whole proving system can handle all user configured variations anyway, so there is not really any downside (for now) to making sure that the merlin transcript protocol is also general enough.

(did I miss anything @hdevalence?)

In the specific case of what to do with this PR, maybe we should hash the public inputs to 32 or 64 bytes and use a single PI label (no leaking) for the hash. (EDIT: or @lopeetall's suggestion of serializing the whole PI) The circuit description should also be added to the transcript earlier, so there is no malleability of the input order, etc.

[CPerezz]

@joebebel makes sense.

Note that for the ordering, the hash will take care too. As we store the PI in a BTreeSet so therefore the order is preserved and therefore, ir prevents any order maleability.

[lopeetall]

The only issue I see with serializing the sparse form of the PI is that we would need to provide a spec for the serialization so that other implementations of the Verifier serialize PI in the same way.

Instead, why don't we just use the SRS to get a binding commitment the PI polynomial and add it to the transcript using the existing Merlin API wrapper? It may not be the most efficient solution as it requires doing another MSM, but we can still take advantage of the sparseness of the PI by skipping all the zeros. And since all we need is a binding commitment we won't need to use an FFT before MSM.

This method would use our existing tools without modification and is consistent with the rest of the protocol.

[bhgomes]

For example, there is another problem with the code (besides the Box::leak distraction) - it violates the property that no label is a prefix of another label.

Why is prefixing an issue? The documentation on merlin says that it's a requirement of the transcript being "parseable". What does this mean? We aren't parsing anything here.

[CPerezz]

The only issue I see with serializing the sparse form of the PI is that we would need to provide a spec for the serialization so that other implementations of the Verifier serialize PI in the same way.

In the verifier (Usually a Smart Contract) will probably be much more expensive to do the MSM than the hash. That's why I suggested that @lopeetall.

For now, we could start with something easy that solves the bug. And then move on into a better design.

Something like this as purposed by @davidnevadoc in private.

// For each PI != 0
transcript.append(b"pi_pos", &F::from(*pos));
transcript.append(b"pi_val", &F::from(val));

This is not the most optimal. But works for now. And we can discuss the approach we want to go for in a follow-up issue.

[lopeetall]

Can we reuse those labels pi_pos and pi_val though?

From the Merlin website:

The labels should be fixed, not defined at runtime, as runtime data should be in the message body, while the labels are part of the protocol definition. A sufficient condition for the transcript to be parseable is that the labels should be distinct and none should be a prefix of any other.

[ghost]

Why is prefixing an issue? The documentation on merlin says that it's a requirement of the transcript being "parseable". What does this mean? We aren't parsing anything here.

The absolute requirement is that the transcript is binding to the messages in it, that is, it is not feasible to find a different transcript with different labels/messages that gives the same challenges. The property that merlin promises is that if labels are prefix free, then the transcript is unambiguously parseable (a mathematical definition - there is no computation to parse the transcript), and if the transcript is parseable then it is message binding.

It could be that the transcript is message binding even if the labels are not prefix-free, but this requires an additional argument and can't be assumed from the guarantees that merlin provides. It's just much simpler to defer to merlin's requirements.

Instead, why don't we just use the SRS to get a binding commitment the PI polynomial and add it to the transcript using the existing Merlin API wrapper? It may not be the most efficient solution as it requires doing another MSM, but we can still take advantage of the sparseness of the PI by skipping all the zeros. And since all we need is a binding commitment we won't need to use an FFT before MSM.

Or, just serialize the PI polynomial? Though I think your original suggestion of serializing the PI directly is probably fine as well. I think the MSM is expensive.

[bhgomes]

Why is prefixing an issue? The documentation on merlin says that it's a requirement of the transcript being "parseable". What does this mean? We aren't parsing anything here.

The absolute requirement is that the transcript is binding to the messages in it, that is, it is not feasible to find a different transcript with different labels/messages that gives the same challenges. The property that merlin promises is that if labels are prefix free, then the transcript is unambiguously parseable (a mathematical definition - there is no computation to parse the transcript), and if the transcript is parseable then it is message binding.

It could be that the transcript is message binding even if the labels are not prefix-free, but this requires an additional argument and can't be assumed from the guarantees that merlin provides. It's just much simpler to defer to merlin's requirements.

If this is the case then why are we letting the user specify any labeling scheme at all, just choose a prefix-free sequence of labels and use each one in turn. From an engineering perspective, I don't want to have to think about these safety requirements if there exists a protocol that takes care of it for me, especially when these labels don't actually help me accomplish anything inside of my application (in this case PLONK). This is the API I actually care about:

trait Transcript {
    fn append<M>(&mut self, message: M);
    fn challenge<C>(&mut self) -> C;
}

In which scenarios is knowing or specifying the labels manually an important feature to have?

[ghost]

In which scenarios is knowing or specifying the labels manually an important feature to have?

Yeah, you are absolutely correct that from an implementation perspective, it is entirely possible to do without labels, or without 'static lifetimes on the labels, etc etc. It's probably entirely possible to use the exact "pi{}" format labels too.

The reason it's important, though, is because "Frozen Heart" is just the latest in a long history of Fiat-Shamir implementation mistakes (mostly of the "omit data" kind). The idea is that we should write down - very explicitly - the exact Plonk interactive protocol being used, and then duplicate it exactly with merlin, down to the labels and everything. The goal is not only 0 mistakes in converting the interactive proof to non-interactive, but not even the possibility of mistakes.

[davidnevadoc]

After reading the discussion and learning about the correct usage of labels in merlin I believe that we should open a different PR to tackle this issue, as there are several parts of the code where they are misused. For example we are adding the commitment for the permutation with the label z and also adding the challenge used for lookup table RLC with the label zeta, which breaks the prefix rule. We are also using Box::leak() in the same way I did in the first version of the PR when adding the evaluation of custom gate constraints.

Having the merlin requirements in mind I think the simplest solution is to serialize PI and add it to the transcript with the label "pi". This struct is responsible of holding a one-to-one representation of each possible public input vector. In particular we use BTreeMap to guarantee the inputs are stored in order and we only store non-zero values, as zeros are implicit when no value is provided.

[hdevalence]

After reading the discussion and learning about the correct usage of labels in merlin I believe that we should open a different PR to tackle this issue, as there are several parts of the code where they are misused.

The docs on Transcript Protocols might be helpful; the recommended way to use the library is for each protocol to define a protocol-specific extension trait that maps the protocol-level transcript actions ("do a domain separation", "append a public key", "append a commitment to whatever", etc) operating on higher-level types into the underlying calls to the byte-oriented Merlin API. So in this case, for instance, it might make sense to have a transcript protocol that handled the serialization and labeling, and presented higher-level methods to the rest of the crate.