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
*
CompleteEdwardsCurveTheorems: point compression
Andres Erbsen
2017-03-02
*
use [positive] for [F] modulus, char_ge_C instead of char_gt_C
Andres Erbsen
2017-03-02
*
rewrite ExtendedCoordinates, fix Ed25519
Andres Erbsen
2017-03-02
*
edwards curves over isomorphic fields
Andres Erbsen
2017-03-02
*
WIP
Andres Erbsen
2017-03-02
*
split the algebra library; use fsatz more
Andres Erbsen
2017-03-02
*
fsatz, nsatz_solve_nonzero
Andres Erbsen
2017-03-02
*
use field_nsatz in CompleteEdwardsCurve.Pre
Andres Erbsen
2017-03-02
*
Fix for 8.6
Jason Gross
2016-11-22
*
Fix for Coq 8.4
Jason Gross
2016-11-21
*
Add add_coordinates_respectful_hetero
Jason Gross
2016-11-17
*
Generalize add_coordinates
Jason Gross
2016-11-17
*
Add add_coordinates_gen
Jason Gross
2016-11-16
*
framework for l_order_B
Andres Erbsen
2016-10-30
*
CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l...
Andres Erbsen
2016-10-27
*
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
*
Be more hesitant to [pose proof E.char_gt_2]
Jason Gross
2016-10-17
*
refactor scalar multiplication thoery, implement SRepERepMul
Andres Erbsen
2016-10-12
*
remove eq_dec from Monoid
Andres Erbsen
2016-08-23
*
Refactor ModularArithmetic into Zmod, expand Decidable
Andres Erbsen
2016-08-04
*
Move most notation level declarations into Util
Jason Gross
2016-07-27
*
Make the library 20% faster: [auto with *] is evil
Jason Gross
2016-07-22
*
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
[next]