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
*
removed now irrelevant commented-out code
jadep
2016-10-27
*
convert feEnc correctness proof to bounded type
jadep
2016-10-27
*
finished feEnc correctness
jadep
2016-10-27
*
most of feEnc correctness proof
jadep
2016-10-27
*
removed lingering TODO
jadep
2016-10-27
*
Fix for Coq 8.4 (f_equiv changed behavior)
Jason Gross
2016-10-26
*
Initial work on filling ed25519 with bounded things
Jason Gross
2016-10-25
*
prove SRepMul admit
Andres Erbsen
2016-10-25
*
Proved homomorphism between curve groups (Twisted Edwards Curve representatio...
jadep
2016-10-24
*
Freeze before packing to get canonical encodings
jadep
2016-10-24
*
ed25519: prove some admits
Andres Erbsen
2016-10-24
*
Modify point_phi (from PointEncodings) to use ref_phi
jadep
2016-10-23
*
Fix a typo
Jason Gross
2016-10-23
*
Prove onCurve_ERepB
Jason Gross
2016-10-23
*
Finish twedprm_ERep proof
Jason Gross
2016-10-23
*
Made field-element encodings canonicalize elements before encoding them
jadep
2016-10-22
*
Fix src/Experiments/Ed25519.v for Coq 8.4
Jason Gross
2016-10-22
*
final touches/fixes for freeze restructuring
jadep
2016-10-22
*
extraction: use more Haskell functions
Andres Erbsen
2016-10-21
*
fiddle with [rewrite <-!(field_div_definition)], maybe fix build
Andres Erbsen
2016-10-21
*
Edwards.Extended.to_twisted: only one inversion, improve extraction
Andres Erbsen
2016-10-21
*
Fix build failure
Jason Gross
2016-10-21
*
extraction of [sign] using Haskell [Integer]s for limbs
Andres Erbsen
2016-10-21
*
Merge branch 'master' into instantiation-rsloan-phoas
Jason Gross
2016-10-20
|
\
|
*
Fill in some things in Ed25519 from SC25519
Jason Gross
2016-10-19
|
*
Fix for change in precedence of <-> vs -> in 8.4/8.5
Jason Gross
2016-10-19
|
*
Work around out of memory error in 8.5, 8.5pl1
Jason Gross
2016-10-18
|
*
Fix for 8.4 unification being unhappy in Ed25519 (nats are terrible)
Jason Gross
2016-10-17
|
*
Various Ed25519 8.4 fixes
Jason Gross
2016-10-17
|
*
refactor scalar multiplication thoery, implement SRepERepMul
Andres Erbsen
2016-10-12
|
*
Fixed naming issue
jadep
2016-10-12
|
*
defined sign operation on field elements
jadep
2016-10-12
|
*
Fixing merge conflict
jadep
2016-10-12
|
*
integrate bitwise operations
Andres Erbsen
2016-10-12
|
*
remove Experiments.EncodingLemmas (superseded by Jade's recent work)
Andres Erbsen
2016-10-12
|
*
Add Ed25519 to _CoqProject
Jason Gross
2016-10-12
|
*
Starting to fill in Ed25519 context variables
jadep
2016-10-10
*
|
Merge _CoqProject
Rob Sloan
2016-10-06
|
\
\
|
|
/
|
/
|
*
|
Silence warnings about Require in GenericFieldPow
Jason Gross
2016-09-30
*
|
montgomery-curve
Andres Erbsen
2016-09-28
|
*
Fix merge with master
Robert Sloan
2016-09-24
|
|
\
|
|
/
|
/
|
|
*
Large-scale refactoring of src/Assembly
Robert Sloan
2016-09-24
*
|
move eddsa rep change
Andres Erbsen
2016-09-22
*
|
alternative signing derivation
Andres Erbsen
2016-09-22
*
|
deduplicate Let_In into src/Util/LetIn.v
Andres Erbsen
2016-09-17
*
|
Derive EdDSA.verify from equational specification
Andres Erbsen
2016-09-16
*
|
IterAssocOp: parameters before arguments
Andres Erbsen
2016-09-16
|
*
Most of a more efficient WordRangeOpt
Robert Sloan
2016-09-13
|
*
Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas
Robert Sloan
2016-08-30
|
|
\
|
*
|
Pieces of a correctness lemma
Robert Sloan
2016-08-30
[next]