roconnor-blockstream

I've written [formal correctness proofs](https://htmlpreview.github.io/?https://github.com/ElementsProject/simplicity/blob/027e46ca91dc7eecf5a05707798edf17e72612c3/alectryon/verif_int128_impl.v.html) of the functions in the [`src/int128_struct_impl.h`](https://github.com/bitcoin-core/secp256k1/pull/1000/files#diff-c6a9f8563878e3e906666be1120021ae7ae49963c6f31b0af491e82c1c7339f1) file using [VST](https://vst.cs.princeton.edu/). The most relevant part is the function specifications which can be found at lines of the...

Is the generated asm different?

I have not updated the proofs, but I do plan to do so. I don't suggest waiting for them, but if you prefer to wait that's fine. I'm working on...

While I continue to refactor my proofs to automate the tedious bits, I have now got to the point where the revised code in the int128_struct file is now proved...

I'm done my pass at refactoring my proof. There isn't too much to say. The new proofs are less tedious than they were before. You are welcome to "browse" the...

Looking into it more closely it seems the sketchy cases of casting large signed int128 numbers to int64 is always then immediately masked with `& M62`, so it isn't so...

https://github.com/bitcoin-core/secp256k1/blob/1e78c18d5b80552d15aa2e2e58348fc1b89b1e3b/src/group_impl.h#L264 is the call to fe_normalize_weak I had in mind, but @real-or-random has another instance somewhere else.

To be clear, all the instances of magnitude are currently statically implied because all those "variables" that are dynamic are currently only ever passed integer literal values.

I wasn't aware of that one. (I'm less familiar with the non-verification related code.) Make sense to patch that case by always setting the magnitude to the max of the...

The whole point of the magnitude field is to have a check that the tested code paths would not overflow even if different values were used. It is a poor...