index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
_CoqProject
Commit message (
Expand
)
Author
Age
...
*
Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec
Jade Philipoom
2016-02-15
|
\
*
|
ported some of EdDSA25519 to new field framework
Jade Philipoom
2016-02-15
|
*
port bounded iter_op and Edwards doubleAndAdd
Andres Erbsen
2016-02-15
|
*
CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context
Andres Erbsen
2016-02-15
|
/
*
Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v
Andres Erbsen
2016-02-13
*
port some edwards curve theorems
Andres Erbsen
2016-02-12
*
Define F m, a replacement for GF with several benefits.
Andres Erbsen
2016-02-11
*
Update build process to use COQPATH & _CoqProject
Jason Gross
2016-02-05
*
simple refactor of makefile; comments
varomodt
2016-01-09
*
Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...
Jade Philipoom
2016-01-05
*
Code-reviewing EdDSA
Adam Chlipala
2015-12-29
*
reorganized lemmas; moved several to ListUtil and ZUtil.
Jade Philipoom
2015-11-24
*
ModularBaseSystem.carry: implement, state lemmas, some progress on proofs
Andres Erbsen
2015-11-17
*
Merge remote-tracking branch 'jadep/master'
Andres Erbsen
2015-11-06
|
\
*
|
instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)
Andres Erbsen
2015-11-06
|
/
*
Beautified BinGF.splitWords
Adam Chlipala
2015-10-30
*
word bound propagation examples
Andres Erbsen
2015-10-30
*
BaseSystem to Util.ListUtil: separate out generic list lemmas
Andres Erbsen
2015-10-29
*
Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto
Andres Erbsen
2015-10-29
|
\
|
*
patches for galois
Robert Sloan
2015-10-27
*
|
positional number system equivalence transcribed from pencil-and-paper proofs...
Andres Erbsen
2015-10-25
|
/
*
add morphism-based field impl
Robert Sloan
2015-10-22
*
fix the makefile to not rebuild + module renaming
Robert Sloan
2015-10-22
*
pull changes from desktop
Robert Sloan
2015-10-19
*
gfPlus abstraction
Robert Sloan
2015-10-16
*
make ring decidable + define constants
Robert Sloan
2015-09-19
*
makefile dependency order
Andres Erbsen
2015-09-18
*
Curves: elliptic curve point format record declarations and some invariants
Andres Erbsen
2015-09-18
*
import VerdiTactics
Andres Erbsen
2015-09-17
*
redo module structure + init curve25519
Robert Sloan
2015-09-16
*
init our centralized repo
Robert Sloan
2015-09-10
[prev]