search

GaloisInc / ckzg-eip-4844-verification

BSD 3-Clause "New" or "Revised" License
2 stars 1 forks source link

Add BLS Elliptic Curve support in Cryptol #14

Closed b13decker closed 1 month ago

b13decker commented 2 months ago

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).

b13decker commented 2 months ago

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 commented 1 month ago

@marsella Captured all these issues here: https://github.com/GaloisInc/ckzg-eip-4844-verification/issues/21

Thank you again for the thorough review!