index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Curves
Commit message (
Expand
)
Author
Age
*
Combine the zero and non-zero cases together.
David Benjamin
2018-01-15
*
Factor out fsatz lemmas
Jason Gross
2018-01-09
*
Replace char_ge_12 with char_ge_3
Jason Gross
2018-01-09
*
Massively speed up Jacobian
Jason Gross
2018-01-09
*
Revert "Replace char_ge_12 with char_ge_3"
Jason Gross
2018-01-09
*
Replace char_ge_12 with char_ge_3
Jason Gross
2018-01-09
*
Jabobian.v: par -> all
Andres Erbsen
2018-01-09
*
src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_*
Andres Erbsen
2018-01-09
*
@davidben merged Jacobian+affine into Jacobian+Jacobian
Andres Erbsen
2018-01-09
*
Jacobian coordinates
Andres Erbsen
2018-01-09
*
Prove montladder correct in the zero case.
David Benjamin
2018-01-08
*
restore fastpath logic in Curves.Montgomery.XZProofs
Andres Erbsen
2017-12-22
*
prove montgomery ladder for non-zero inputs
Andres Erbsen
2017-12-22
*
Montgomery.XZ, Loops: montladder proof scaffolding
Andres Erbsen
2017-12-22
*
specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.v
Andres Erbsen
2017-12-22
*
expose missing proof in src/Curves/Montgomery/XZProofs.v
Andres Erbsen
2017-12-22
*
clean up src/Curves/Montgomery/XZProofs.v
Andres Erbsen
2017-12-22
*
Curves.Montgomery.XZ: add+check boringssl ladderstep (#278)
Andres Erbsen
2017-12-05
*
projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptional
Andres Erbsen
2017-10-18
*
Curves/Edwards/Affine: prove point compression admits
Andres Erbsen
2017-07-06
*
match C code in Jacobian addition
Andres Erbsen
2017-06-27
*
Weierstrass Jacobian mixed addition
Andres Erbsen
2017-06-23
*
Edwards coordinates precomputed addition formula
Andres Erbsen
2017-06-15
*
ScalarMult: Z -> G -> G (closes #193)
Andres Erbsen
2017-06-14
*
Don't rely on autogenerated names
Jason Gross
2017-06-05
*
Strip trailing whitespace
Jason Gross
2017-06-02
*
use ladderstep from donna (2% faster?)
Andres Erbsen
2017-05-15
*
Prove relationship between `xzladderstep` and M.add (#162)
Andres Erbsen
2017-04-28
*
clean elliptic curve proofs, use par: in WeierstrassAffineProofs
Andres Erbsen
2017-04-28
*
Respond to code review comments
Jason Gross
2017-04-17
*
Use the for-loop notation in Montgomery.XZ
Jason Gross
2017-04-17
*
lemmas about ladderstep on zero
Andres Erbsen
2017-04-14
*
stronger ladderstep correctness proof courtesy Teo
Andres Erbsen
2017-04-14
*
rename-everything
Andres Erbsen
2017-04-06
*
Finish seperating our specs: remove old non-specified code
Andres Erbsen
2016-02-15
*
port some edwards curve theorems
Andres Erbsen
2016-02-12
*
removed lingering Check/SearchAbout statements
Jade Philipoom
2016-02-07
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Jade Philipoom
2016-02-07
|
\
*
|
EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and th...
Jade Philipoom
2016-02-07
|
*
PointFormats: prove dangling admit
Andres Erbsen
2016-02-07
|
/
*
PointFOrmats,EdDSA: remove redundant axioms
Andres Erbsen
2016-01-16
*
remove duplicate axiom
Andres Erbsen
2016-01-16
*
PointFormats: extended coordinates equivalence proofs
Andres Erbsen
2016-01-16
*
fix merge conflicts + PointFormats proofs
Robert Sloan
2016-01-14
|
\
*
|
assumption lemmas in PointFormats
Rob Sloan
2016-01-11
*
|
simple refactor of makefile; comments
varomodt
2016-01-09
|
*
cleanup
Andres Erbsen
2016-01-08
|
/
*
PointFormats: factor out admits
Andres Erbsen
2016-01-08
*
PointFormats: no zero denominators in Edwards addition
Andres Erbsen
2016-01-08
*
PointFormats: addition produces points on curve
Andres Erbsen
2016-01-07
[next]