index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
CompleteEdwardsCurve
Commit message (
Expand
)
Author
Age
*
proved an admit in field homomorphisms that turned out to be unprovable; I ad...
jadep
2016-07-15
*
s/conservative_common_denominator/common_denominator/g
Andres Erbsen
2016-07-11
*
remove field_algebra
Andres Erbsen
2016-07-11
*
port CompleteEdwardsCurveTheorems (builds again)
Andres Erbsen
2016-07-11
*
pose proof fails where specialize works (typeclass resolution / unification?)
Andres Erbsen
2016-07-11
*
wrap nsatz in Algebra
Andres Erbsen
2016-07-11
*
added proofs about addition chain exponentiation for later use in ModularBase...
jadep
2016-07-10
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
jadep
2016-06-27
|
\
|
*
scalarmult support; EdDSA.sign produces valid signatures
Andres Erbsen
2016-06-27
*
|
update new lemma in CompleteEdwardsCurve/Pre to match other changes to that file
jadep
2016-06-25
*
|
Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_port
jadep
2016-06-24
|
\
|
*
|
merging point encoding port
jadep
2016-06-24
|
\
\
*
|
|
Ported PointEncodings to parameterize over field rather than modulus.
jadep
2016-06-24
|
|
*
Remove a useless intro
Jason Gross
2016-06-24
|
|
/
|
*
ExtendedCoordinates: group.
Andres Erbsen
2016-06-24
|
*
Use Decidable machinery for is_eq_dec
Jason Gross
2016-06-24
|
*
Integrate Pseudize into Pipeline.v
Robert Sloan
2016-06-23
|
*
Pseudize Let_In
Robert Sloan
2016-06-23
|
*
Fix broken notations (hopefully)
Jason Gross
2016-06-22
|
*
Aggregate all level specifications not in Spec/*
Jason Gross
2016-06-22
|
*
Use Admitted, not Qed, when a proof has admit
Jason Gross
2016-06-21
|
*
Fix [Proper_add] in 8.5
Jason Gross
2016-06-21
|
*
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
|
*
move nsatz into tactics directory
Andres Erbsen
2016-06-20
|
*
Remove anything incompatible with new algebraic hierarcy
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
|
*
move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems
Andres Erbsen
2016-06-17
|
*
edwards curve addition respects field homomorphism
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
|
*
refactor nsatz wrappers into algebra file
Andres Erbsen
2016-06-14
|
*
[field] and [nsatz] do things now again
Andres Erbsen
2016-06-14
|
*
stuck because overloading-by-typeclasses sucks
Andres Erbsen
2016-06-13
*
|
Minor 8.5 changes
Jason Gross
2016-06-10
*
|
More changes for 8.5
Jason Gross
2016-06-10
|
*
generic field definition
Andres Erbsen
2016-06-07
|
*
ERep add
Andres Erbsen
2016-05-29
|
*
verify derivation: EdDSA layer
Andres Erbsen
2016-05-28
|
*
before changing SRep from N to F l
Andres Erbsen
2016-05-27
|
/
*
slightly nicer edwards curve extended coordinates addition
Andres Erbsen
2016-05-18
*
ed25519: solve elliptic curve math admits
Andres Erbsen
2016-04-25
*
consolidate and rename Edwards curve lemmas
Andres Erbsen
2016-04-25
*
point_eq_dec
Andres Erbsen
2016-04-22
*
finished last cases of nonzero proofs for associativity
jadep
2016-04-21
*
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
jadep
2016-04-19
|
\
|
*
Add a tactic for field inequalities
Jason Gross
2016-04-19
[next]