Use modified divsteps with initial delta=1/2 for constant-time

[sipa]

This updates the divsteps-based modular inverse code to use the modified version which starts with delta=1/2. For variable time, the delta=1 variant is still used as it appears to be faster.

See https://github.com/sipa/safegcd-bounds/tree/master/coq and https://medium.com/blockstream/a-formal-proof-of-safegcd-bounds-695e1735a348 for a proof of correctness of this variant.

TODO:

• Update unit tests to include edge cases specific to this variant

I'm still running the Coq proof verification for the 590 bound in non-native mode. It's unclear how long this will take.

[real-or-random]

Concept ACK

There's still this comment and the corresponding code:
/* Bounds on eta that follow from the bounds on iteration count (max 12*62 divsteps). */

The docs and the code might be more readable without eta having two different meanings. Maybe try another name for the new eta?

[sipa]

There's still this comment and the corresponding code:
/* Bounds on eta that follow from the bounds on iteration count (max 12*62 divsteps). */

Fixed. There was an equivalent in modinv32 as well.

The docs and the code might be more readable without eta having two different meanings. Maybe try another name for the new eta?

Renamed to zeta.

[roconnor-blockstream]

FWIW I don't believe that it is necessary to wait for the Coq proof checked in "paranoid mode" to complete. OTOH, I estimate the check will probably be completed before this gets merged anyways, so it doesn't really matter.

Edit: (23 days later) I no longer believe the check will be completed before this gets merged.

[real-or-random]

@sipa Is this ready for review?

[sipa]

@real-or-random I plan to add some more unit tests, but otherwise yes.

[sipa]

This PR is ready, I think.

coqc is still running:

  PID USER      PR  NI    VIRT    RES    SHR S  %CPU  %MEM     TIME+ COMMAND                                                                                 
25511 pw        20   0   10.6g  10.4g    204 R 100.0  88.6  59500:51 coqc

[sipa]

Added a selection of randomly generated inputs (with generic modulus, and for field/scalar) as tests that trigger the largest/smallest d and e values at various points during the execution over a few billion runs.

[sipa]

Update: coqc has been running for 8 weeks.

[real-or-random]

Hm, I think I'm in favor of not waiting any longer for Coq... We have the bounds analysis plus the Coq proof in native mode. This should be more than enough to be confident in the algorithm.

I'll try to review this soon.

[real-or-random]

ACK mod nit

[real-or-random]

ACK be0609f careful code review and some testing

[roconnor-blockstream]

I'm not really planning to review this PR myself at this time. But I do ACK the 590 constant. I have actually very carefully reviewed those three digits.

[gmaxwell]

ACK be0609f

[sanket1729]

crACK be0609f

[sipa]

Posthumous update: the paranoid-mode Coq proof finished succesfully 3 hours before this got merged.

[roconnor-blockstream]

For the record, the Coq runtime in paranoid-mode ended up being approximately 66 days.