argumentcomputer / solidity-verifier

Solidity implementation of Nova proving system verifier
Apache License 2.0
56 stars 12 forks source link

Unit-testing field operations #11

Open huitseeker opened 1 year ago

huitseeker commented 1 year ago

in PRs such as #9, the topic came up of whether one operation was modulo the Pallas or the Vesta modulus. I'd like to suggest a general unit-testing practice for figuring it out.

Context:

In general here are remarks for working with any field, when receiving its elements as bytes:

From which I deduce a strategy for relieving confusion w.r.t field modulus:

storojs72 commented 1 year ago

A little bit more context. While porting Nova algorithms from Rust to Solidity, we used to deal with modulo multiplication/addition. While executing multiplication/addition you have two uint256 values and you don't know what modulo (p or q) to use. While debugging, if Rust implementation is at hand and you can extract input and output, it is usually sufficient to just try one modulus and if Solidity output is not equal to Rust one, opposite modulus should be used.

When we talked about this, my impression was that there is some "magic" algorithm that allows deducing whether particular uint256 value is either Pallas or Vesta field element without having reference Rust implementation to compare arithmetics output. If such algorithm would exist, we could add proper input validation (to any relevant function) that stops/reverts execution, if unexpected field element is detected. That would help to resolve the confusion. But I now think that without some additional context, we can't say anything about uint256 value which is less than p and q.

My understanding of mentioned strategy, is that it gives 100% detection whether it is Pallas or Vesta field element, while straightforward trying one or opposite modulus may potentially outcome to the situation, when they both give same output and it is still hard to say what type of field elements were used, isn't it?

cc @huitseeker

huitseeker commented 1 year ago

When we talked about this, my impression was that there is some "magic" algorithm that allows deducing whether particular uint256 value is either Pallas or Vesta field element without having reference Rust implementation to compare arithmetics output.

I confirm that this magic does not exist, essentially because the serialization format of those numbers as bytes is not self-describing. You can only recover the correct element if you know which field you are expecting.

Basically, if p = Pallas.P_MOD, q = Vesta.P_MOD, n = 2^ 256-1, we have 0 < p < q < n. So if you see a 256 bit number x that:

But there are two nuances here:

Same field randomized testing is still valuable

The fact that a function is meant to work with elements of a certain field also means it should give you some guarantees about what’s going to happen outside those elements.

For instance (and don’t take the following verbatim, I’m just riffing to convey a point here), here’s how I would draft a natspec for the documentation of the pallas decompress function:

/// @title Pallas Curve Point Decompression
/// @notice Takes a lower-endian, canonical form u256 as x-coordinate of a Pallas curve point. The highest bit represents the y-coordinate sign.
/// @dev Interprets 0u256 input as the infinity point. Reverts if input cannot represent a base field element in canonical form.
/// @param x A u256 representing the x-coordinate in lower-endian, canonical form. The highest bit is the sign bit for y-coordinate.
/// @return point A Point on the Pallas curve corresponding to x or the infinity point for null input.
function decompress(u256 x) public returns (Point memory point) {
  // function implementation goes here
}

Hopefully that gives more context as to the edge cases I expect to discover with randomized testing, even if the inputs is not of any wrong field. For example, the function above should revert on any input x s.t. p ≤ x < n.

Wrong field testing can (sometimes) detect more specific bugs in the implementation

Let’s assume I test the above function (pallas point decompression) with inputs x s.t. p < x < q, and y s.t. p < y <q. If I observe that my function reverts on y but not on x, there’s a good chance that I used a Vesta.P_MOD (== Pallas.R_MOD) where I should have used a Pallas.P_MOD in the implementation.

Does this make things more clear?

storojs72 commented 1 year ago

Yes. Kind of. So, you are hinting on paying more attention on implementing functionality (that operates with field elements) with stricter input validation against input uint256s, and supplying more "negative" testing, when for example non-canonical representations are passed, while canonical ones are expected or when Pallas field elements passed, while Vesta ones are expected. Am I correctly understanding your point?

huitseeker commented 1 year ago

@storojs72 Yep, I believe you got it. Negative testing of the u256 representation rocks, and by being careful about which "use cases" we generate in that negative testing we can sometimes notice not only a mistake, but a field mismatch.