Add BLS Elliptic Curve support in Cryptol #14

b13decker · 2024-09-18T21:59:05Z

Add the elliptic curve operations needed to continue to implement the Deneb Python spec BLS helper functions.

(Note for reviewers: I've made an effort to make this PR more easily reviewed on a per-commit basis. Hope this helps).

This will be needed for the `bls_modular_inverse` function.

These two functions are hardcoded to work for the BLS_MODULUS. There is currently no need to abstract them further. These functions match the implementations found in the Python specs: - https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#bls_modular_inverse - https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#div

See https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#compute_powers Note that because of the way Cryptol's type system and comprehensions work, we need to have the type constrain of `n >= 2`, whereas the Python spec only constrains `n >= 0`.

We need to use a GCD algorithm because Cryptol cannot perform expoentiation with negative exponents. This means we have an error in the BlsHelpers::bls_modular_inverse function. I'll fix that next.

Have bls_modular_inverse and bls_div call the corresponding utility functions with the hardcoded BLS_MODULUS. This fixes the previous error in the bls_modular_inverse function. This error was uncaught because the unit tests were wrong. The unit tests have now been confirmed with the following site: https://planetcalc.com/3298/

I switched the API to use the Integer type for these utility functions because it simplifies the code. The BlsHelper functions that call these utility functions have been updated and now handle the conversion of types (Integral <=> Integer) internally. This also exposed an error in the modular_inverse when a negative number was passed. A new test has been added to make sure we don't regress.

These were redundant and missed during the previous commit redesign of types.

And add note to the BlsHelpers::bls_modular_inverse about the inability to use pow and why that code now looks different than the Python spec.

These are needed as the building blocks as we start to implement the rest of the Deneb Python spec.

marsella

I've only partly reviewed this but I'm going to give some feedback now since I think you started getting similar feedback in a separate channel.

I'm seeing some mixing of types that I think is introducing more potential bugs than you need. Some code uses bit vectors (integers mod 2^n for the width n), but they are actually holding integers mod p for p =\= 2^n, and also in other places they are converted to Integers.

Unless you are trying to do produce highly optimized implementations of these functions that minimize memory usage or something, I think you are better off using the Z type to represent your numbers. I've flagged several overflow concerns; these will all be handled by Cryptol if you use Z. The EC implementation in cryptol-specs uses that type if you would like to see it in practice.

marsella · 2024-09-19T13:57:48Z

spec/Common/Utils.cry

+pow : {n} (fin n, n >= 1) => [n] -> [n] -> [n] -> [n]
+pow base exp modulus = (base ^^ exp) % modulus


todo: I think you need to be more careful here to prevent overflow messing with your modular reductions. If the exponentiation overflows [n], it'll get reduce mod 2^n, which might not be the same as your modulus.

E.g. take n = 3 and (2, 3, 3). I think what you want is $2^3 \mod 3 = 8 \mod 3 = 2$. What you'll get is $(2^3) :[3] \mod 3 = 8 : [3] \mod 3 = 0 \mod 3 = 0$.

I think the easiest solution will be something like use zext to increase the width of the parameters, then do your computation, then truncate back to n with confidence because the mod ensures that the result is no wider than n bits.

Note: I see this got removed eventually but here is a mod pow implementation using vectors in cryptol-specs.

Yeah, this was wrong, and I determined I need a faster implementation anyway, which is provided with Z.

Can I import from cryptol-specs without having to pull in that source?

marsella · 2024-09-19T14:08:08Z

spec/Spec/BlsHelpers.cry

+type BlsFieldSize = 256
+type BlsFieldElement = [BlsFieldSize]


question: BLS field elements are in the integers mod group w.r.t. the BLS modulus, right? Did you consider using Cryptol's integer mod group Z? I have a vague sense that it makes the SMT constraints a bit messier but it might simplify some of the code in here.

I just learned about Z. I had previously missed it in the manual.

marsella · 2024-09-19T14:10:10Z

spec/Spec/BlsHelpers.cry

+/**
+ * Compute the modular inverse of x
+ *  i.e. return y such that x * y % BLS_MODULUS == 1
+ * Precondition: x != 0


todo: specifically, x != 0 mod BLS_MODULUS.

marsella · 2024-09-19T14:25:40Z

spec/Spec/BlsHelpers.cry

+bls_div : BlsFieldElement -> BlsFieldElement -> BlsFieldElement
+bls_div x y = (x * (bls_modular_inverse y)) % BLS_MODULUS


todo: I'm worried about overflow here, too.

Here's an implementation of mod mul in cryptol specs, that uses an extension like I mentioned to do safe multiplication and mod.

I think you're running into this because of a language difference between Python's happily expandable integers and Cryptol's extremely fixed-width ones, so there will be some discrepancy between the spec and your implementation.

Yes, you are 💯% correct. I'll fix these.

marsella · 2024-09-19T14:29:13Z

spec/Spec/BlsHelpers.cry

+ */
+compute_powers : {n} (fin n, width n <= 64, n >= 2) => BlsFieldElement -> [n]BlsFieldElement
+compute_powers x = powers where
+        powers = [x] # [(powers@(i-1) * x) % BLS_MODULUS | i <- [1 .. n-1]]


todo: I remain worried about overflow!! Can you make a single modmul function somewhere and use it in all these places?

marsella · 2024-09-19T14:30:41Z

spec/Spec/BlsHelpers.cry

@@ -70,3 +80,15 @@ property test_bls_modular_inverse x expectedY =
 test_bls_div : BlsFieldElement -> BlsFieldElement -> BlsFieldElement -> Bit
 property test_bls_div x y expected =
    bls_div x y == expected
+
+/**
+ * Unit tests for `bls_modular_inverse`.


todo: I think this is implied for you but to make it explicit once: for each of my overflow comments, I suggest that you add a unit test that pokes at that upper bound, to make sure it's handled correctly.

marsella · 2024-09-20T13:35:45Z

spec/Spec/BlsEC.cry

+/**
+ * G1 elliptic curve point
+ */
+type G1Point =
+    { xCoord : Bytes48
+    , yCoord : Bytes48
+    }


How do you represent the point at infinity? It doesn't have a set of affine coordinates but there are often conditionals in various algorithms that require checking for it. For the prime field elliptic curves I used an enum but that is not supported by SAW yet so might not be an option for this project.

I'm using (0, 0) for infinity --- I think that gets added in a later commit.

As in my next PR.

marsella · 2024-09-20T13:38:26Z

spec/Spec/BlsEC.cry

+    x = toInteger point.xCoord
+    y = toInteger point.yCoord
+    modulus = toInteger Fp
+    m = div (3 * x^^2) (2 * y) modulus


suggestion: consider renaming div to div_mod if you keep this function. modulus is pretty clear but it's not immediately obvious why div has 3 parameters.

I like this suggestion. I'm thinking though if I change it to use Z then I don't need the extra parameter, so hopefully that is more clear. I only used the name div because it matches the Python spec, but I prefer your suggestion, even as I go with using Z.

b13decker · 2024-09-20T17:33:11Z

I've only partly reviewed this but I'm going to give some feedback now since I think you started getting similar feedback in a separate channel.

I'm seeing some mixing of types that I think is introducing more potential bugs than you need. Some code uses bit vectors (integers mod 2^n for the width n), but they are actually holding integers mod p for p =\= 2^n, and also in other places they are converted to Integers.

Unless you are trying to do produce highly optimized implementations of these functions that minimize memory usage or something, I think you are better off using the Z type to represent your numbers. I've flagged several overflow concerns; these will all be handled by Cryptol if you use Z. The EC implementation in cryptol-specs uses that type if you would like to see it in practice.

Thanks for pointing out the Z type. That would have saved me a lot of trouble and time, but at least I know now. I think what I'm going to do is create an issue to refactor the code to use Z. Since I already have tests for each function, this shouldn't be bad. Thanks so much for this review!

b13decker added 11 commits September 17, 2024 09:06

readme: Whitespace

51b9b45

utils: Add modular pow function

68ca478

This will be needed for the `bls_modular_inverse` function.

utils: Move pow tests into repl doc tests

707624a

utils: Add functions for division and modular inverse

52f42d0

We need to use a GCD algorithm because Cryptol cannot perform expoentiation with negative exponents. This means we have an error in the BlsHelpers::bls_modular_inverse function. I'll fix that next.

util: Remove unnecessary fromInteger conversions

3252d32

These were redundant and missed during the previous commit redesign of types.

utils: Remove unused pow function

96a76a5

And add note to the BlsHelpers::bls_modular_inverse about the inability to use pow and why that code now looks different than the Python spec.

blsec: Add module that handles BLS elliptic curve operations

1750405

These are needed as the building blocks as we start to implement the rest of the Deneb Python spec.

b13decker added this to the Milestone 2 milestone Sep 18, 2024

b13decker requested review from marsella and mccleeary-galois September 18, 2024 21:59

b13decker self-assigned this Sep 18, 2024

blshelper: Remove unused constant NEGATIVE_ONE

5aa3ce5

marsella reviewed Sep 20, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add BLS Elliptic Curve support in Cryptol #14

Add BLS Elliptic Curve support in Cryptol #14

b13decker commented Sep 18, 2024

marsella left a comment

marsella Sep 19, 2024

marsella Sep 20, 2024

b13decker Sep 20, 2024

marsella Sep 19, 2024

b13decker Sep 20, 2024

marsella Sep 19, 2024

marsella Sep 19, 2024

marsella Sep 19, 2024

b13decker Sep 20, 2024

marsella Sep 19, 2024

marsella Sep 19, 2024

marsella Sep 20, 2024

b13decker Sep 20, 2024

b13decker Sep 20, 2024

marsella Sep 20, 2024

b13decker Sep 20, 2024

b13decker commented Sep 20, 2024

		pow : {n} (fin n, n >= 1) => [n] -> [n] -> [n] -> [n]
		pow base exp modulus = (base ^^ exp) % modulus

		type BlsFieldSize = 256
		type BlsFieldElement = [BlsFieldSize]

		bls_div : BlsFieldElement -> BlsFieldElement -> BlsFieldElement
		bls_div x y = (x * (bls_modular_inverse y)) % BLS_MODULUS

Add BLS Elliptic Curve support in Cryptol #14

Are you sure you want to change the base?

Add BLS Elliptic Curve support in Cryptol #14

Conversation

b13decker commented Sep 18, 2024

marsella left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

b13decker commented Sep 20, 2024