index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
Commit message (
Expand
)
Author
Age
*
ed25519 spec: small cleanup
Andres Erbsen
2016-07-21
*
compute on [F q]!
Andres Erbsen
2016-07-20
*
experiments wd25519: simplify proof for a
Andres Erbsen
2016-07-20
*
Silence a warning
Jason Gross
2016-07-18
*
Remove a nested proof
Jason Gross
2016-07-18
*
ported IterAssocOp to use monoid rather than a billion context variables that...
jadep
2016-07-18
*
Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s
Andres Erbsen
2016-07-13
*
Merge of fixedlength and master
jadep
2016-07-11
|
\
|
*
added proofs about addition chain exponentiation for later use in ModularBase...
jadep
2016-07-10
*
|
stuck trying to figure out dependently typed continuation passing style
Andres Erbsen
2016-07-06
|
/
*
EdDSARefinement: work around rewrite_strat for 8.4
Andres Erbsen
2016-06-28
*
eddsa refinement setup
Andres Erbsen
2016-06-27
*
scalarmult support; EdDSA.sign produces valid signatures
Andres Erbsen
2016-06-27
*
first pass of scalarmult
Andres Erbsen
2016-06-27
*
Fix for Coq 8.4
Jason Gross
2016-06-25
*
EdDSA: prove things about spec
Andres Erbsen
2016-06-25
*
Fix a missing mod resolution
Jason Gross
2016-06-21
*
NPeano.modulo became Nat.modulo in 8.5
Jason Gross
2016-06-21
*
Import omega for 8.5
Jason Gross
2016-06-21
*
Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5
Jason Gross
2016-06-21
*
remove trailing whitespace from src/
Andres Erbsen
2016-06-20
*
Variosu 8.5 fixes
Jason Gross
2016-06-20
*
remove obsolete rep mechanism
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