index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
readme: dont say things I am not sure of
Andres Erbsen
2016-06-20
*
remove obsolete rep mechanism
Andres Erbsen
2016-06-20
*
GF25519: quiet
Andres Erbsen
2016-06-20
*
Remove anything incompatible with new algebraic hierarcy
Andres Erbsen
2016-06-20
*
Merge branch 'field-experiment'
Andres Erbsen
2016-06-20
|
\
*
|
Makefile: build on Arch Linux once again
Andres Erbsen
2016-06-20
|
*
[F q] is [Algebra.field]
Andres Erbsen
2016-06-20
|
*
port EdDSA spec
Andres Erbsen
2016-06-20
|
*
tuple tooling
Andres Erbsen
2016-06-20
|
*
port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...
Andres Erbsen
2016-06-18
*
|
Fix .mailmap (correct name on the left)
Jason Gross
2016-06-18
*
|
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
jadep
2016-06-17
|
\
\
*
|
|
Canonicalization is now automated in GF25519 and added to GF1305.
jadep
2016-06-17
*
|
|
Specific version of freeze for GF25519 (automation still needs a little work)
jadep
2016-06-17
|
|
*
move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems
Andres Erbsen
2016-06-17
|
*
|
Be a bit more quiet on make unless VERBOSE=1 is passed
Jason Gross
2016-06-16
|
|
*
Z is integral domain
Andres Erbsen
2016-06-16
|
|
*
port edwards curve spec
Andres Erbsen
2016-06-16
|
|
*
edwards curve addition respects field homomorphism
Andres Erbsen
2016-06-16
|
|
*
algebra: add homomorphisms
Andres Erbsen
2016-06-16
|
|
*
prove ring admits
Andres Erbsen
2016-06-16
|
|
*
edwards curve preliminaries: replace oncurve proof with nsatz
Andres Erbsen
2016-06-16
|
|
*
nsatz: reimplement, integrate, demonstrate
Andres Erbsen
2016-06-15
*
|
|
PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...
jadep
2016-06-15
*
|
|
changed representation definition to require digits vector to be the exact le...
jadep
2016-06-15
*
|
|
Added canonicalization to ModularBaseSystemOpt.
jadep
2016-06-15
|
*
|
Add .mailmap
Jason Gross
2016-06-15
|
*
|
Update README so it's good for both github.com and github.mit.edu
Jason Gross
2016-06-15
|
/
/
*
|
Merge
jadep
2016-06-14
|
\
\
*
|
|
Finished admits for canonicalization proofs.
jadep
2016-06-14
|
|
*
refactor nsatz wrappers into algebra file
Andres Erbsen
2016-06-14
|
|
*
[field] and [nsatz] do things now again
Andres Erbsen
2016-06-14
*
|
|
reversed modulus_digits and proved a few admits
jadep
2016-06-13
*
|
|
progress on second stage (conditional constant-time subtraction) of canonical...
jadep
2016-06-13
|
|
*
stuck because overloading-by-typeclasses sucks
Andres Erbsen
2016-06-13
|
|
*
indent
Andres Erbsen
2016-06-12
|
*
|
Another fix for an anomaly in 8.4pl2
Jason Gross
2016-06-11
|
*
|
More Coq 8.4pl2 fixes
Jason Gross
2016-06-11
|
*
|
Fix for Coq 8.4pl2
Jason Gross
2016-06-11
|
*
|
Work around bug #4811 (slow f_equal)
Jason Gross
2016-06-11
*
|
|
starting rewrite using different definition of map
jadep
2016-06-11
|
*
|
Minor 8.5 changes
Jason Gross
2016-06-10
|
*
|
More changes for 8.5
Jason Gross
2016-06-10
|
*
|
8.5 fixes
Jason Gross
2016-06-10
|
*
|
Set Asymmetric Patterns
Jason Gross
2016-06-10
|
*
|
Add coqprime that works with 8.5, bundle bedrock
Jason Gross
2016-06-10
|
/
/
|
*
improved generic field library
Andres Erbsen
2016-06-10
|
*
improve generic field library
Andres Erbsen
2016-06-10
|
*
experiment
Andres Erbsen
2016-06-07
|
*
generic field definition
Andres Erbsen
2016-06-07
[next]