index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Make [bash] tactic easier to debug
Jason Gross
2016-06-21
*
use Local Obligation Tactic (8.5-compat)
Andres Erbsen
2016-06-21
*
remove trailing whitespace from src/
Andres Erbsen
2016-06-20
*
Algebra: change a aliasing definition into an aliasing lemma to appease impli...
Andres Erbsen
2016-06-20
*
parenthesize Ltac [constr:] arguments
Andres Erbsen
2016-06-20
*
Fix nsatz_compute for 8.4
Jason Gross
2016-06-20
*
More missing scopes for 8.5?
Jason Gross
2016-06-20
*
More 8.5 fixes
Jason Gross
2016-06-20
*
Variosu 8.5 fixes
Jason Gross
2016-06-20
*
Fix for Coq 8.4pl2
Jason Gross
2016-06-20
*
move nsatz into tactics directory
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
|
\
|
*
[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
*
|
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
|
*
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
*
|
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
|
/
/
|
*
improved generic field library
Andres Erbsen
2016-06-10
|
*
improve generic field library
Andres Erbsen
2016-06-10
[next]