constantine/formal_verification
Mamy Ratsimbazafy 2613356281
Endomorphism acceleration for Scalar Multiplication (#44)
* Add MultiScalar recoding from "Efficient and Secure Algorithms for GLV-Based Scalar Multiplication" by Faz et al

* precompute cube root of unity - Add VM precomputation of Fp - workaround upstream bug https://github.com/nim-lang/Nim/issues/14585

* Add the φ-accelerated lookup table builder

* Add a dedicated bithacks file

* cosmetic import consistency

* Build the φ precompute table with n-1 EC additions instead of 2^(n-1) additions

* remove binary

* Add the GLV precomputations to the sage scripts

* You can't avoid it, bigint multiplication is needed at one point

* Add bigint multiplication discarding some low words

* Implement the lattice decomposition in sage

* Proper decomposition for BN254

* Prepare the code for a new scalar mul

* We compile, and now debugging hunt

* More helpers to debug GLV scalar Mul

* Fix conditional negation

* Endomorphism accelerated scalar mul working for BN254 curve

* Implement endomorphism acceleration for BLS12-381 (needed cofactor clearing of the point)

* fix nimble test script after bench rename
2020-06-14 15:39:06 +02:00
..
README.md Add formally verified and prover generated BLS12_381 implementation 2020-03-19 00:22:00 +01:00
bls12_381_q_64.c Add formally verified and prover generated BLS12_381 implementation 2020-03-19 00:22:00 +01:00
bls12_381_q_64.nim Endomorphism acceleration for Scalar Multiplication (#44) 2020-06-14 15:39:06 +02:00

README.md

Formal verification

This folder will hold code related to formal verification.

References