Milestone 5

What's Changed

• Keygen revisited by @msaaltink in #62
• Bls operations rebased by @nano-o in #64
• Bulk addition memory safety by @nano-o in #66
• Bulk add functional by @andreistefanescu in #69
• Add remaining BLS wrapper proofs by @bboston7 in #70
• Publish html-summary script output to Github pages by @bboston7 in #71

Full Changelog: milestone-4...milestone-5

Milestone 4

Correctness for x86_64 routines (#58)

* Functional correctness for some x86_64 routines

* modulus -> modulus384

* ctx_inverse_mod_384.saw

* Update README.md

* Update README.md

* Test CI time with aliased specs disabled

* Test CI with only functional proofs

* Test CI without addition proofs

* Separate addition proofs

* Run addition proofs in different SAW process

* Address comments, split CI job

Milestone 3

Add memory safety proofs for remaining x86_64 routines (#39)

* Add memory safety proofs for mulq implementations

* Include patch that avoids offloading return value pointer in XMM

* Add memory safety proof for ctx_inverse_mod_384

* Use new x86 What4 hash consing option

* Update README.md, document options in ctx_inverse_mod_384.saw

* Update SAW_URL

* Update Docker configuration

* Fix typo

* blst_patched -> blst_recent

* Expand upon comment in ctx_inverse_mod_384.saw

* Remove some now-redundant TODO comments

* Add comment to README.md

Milestone 2

Release 2 extra (#38)

Update the README and add some API-function proofs

10/2/2020 milestone

milestone-1

10/02/2020 milestone