index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Spec
Commit message (
Expand
)
Author
Age
...
*
remove eq_dec from Monoid
Andres Erbsen
2016-08-23
*
[cbv beta] in the beginning of Obligation Tactic for 8.5
Andres Erbsen
2016-08-08
*
[F] has its own module now
Andres Erbsen
2016-08-05
*
Refactor ModularArithmetic into Zmod, expand Decidable
Andres Erbsen
2016-08-04
*
compute on [F q]!
Andres Erbsen
2016-07-20
*
remove field_algebra
Andres Erbsen
2016-07-11
*
added proofs about addition chain exponentiation for later use in ModularBase...
jadep
2016-07-10
*
Define the spec of Weierstrass curves (#6)
Jason Gross
2016-07-03
*
scalarmult support; EdDSA.sign produces valid signatures
Andres Erbsen
2016-06-27
*
EdDSA: prove things about spec
Andres Erbsen
2016-06-25
*
EdDSA.Notations: indentation
Andres Erbsen
2016-06-22
*
Fix broken notations (hopefully)
Jason Gross
2016-06-22
*
Handle renaming of NPeano.pow to Nat.pow (#3)
Jason Gross
2016-06-22
*
EdDSA.v: resolve ambiguity based on ed25519.py
Andres Erbsen
2016-06-21
*
Whitespace change
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
*
Remove anything incompatible with new algebraic hierarcy
Andres Erbsen
2016-06-20
*
Merge branch 'field-experiment'
Andres Erbsen
2016-06-20
|
\
|
*
port EdDSA spec
Andres Erbsen
2016-06-20
|
*
move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems
Andres Erbsen
2016-06-17
|
*
port edwards curve spec
Andres Erbsen
2016-06-16
*
|
Minor 8.5 changes
Jason Gross
2016-06-10
*
|
More changes for 8.5
Jason Gross
2016-06-10
|
*
before changing SRep from N to F l
Andres Erbsen
2016-05-27
|
/
*
Changed name of Encoding to CanonicalEncoding, and changed notation to match.
jadep
2016-04-29
*
Moved sign_bit definition to Spec.
jadep
2016-04-29
*
Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...
jadep
2016-04-28
*
Completed encoding reorganization; factored sign_bit out of PointEncodings an...
jadep
2016-04-28
*
consolidate and rename Edwards curve lemmas
Andres Erbsen
2016-04-25
*
Reorganization and revision of Encoding code and redefinition of sign_bit fun...
jadep
2016-04-25
*
point_eq_dec
Andres Erbsen
2016-04-22
*
ed25519: continue derivation
Andres Erbsen
2016-04-08
*
Drop second projections in Ed25519
Jason Gross
2016-03-29
*
ed25519 derivation: pair programming with jgross... slow progress
Andres Erbsen
2016-03-24
*
nicer verify() derivation starter
Andres Erbsen
2016-03-21
*
instantiate ed25519 sign in spec
Andres Erbsen
2016-03-20
*
Ed25519: d is nonsquare
Andres Erbsen
2016-03-20
*
Finish absolutizing imports
Jason Gross
2016-03-10
*
Factor out some bedrock dependencies into WordUtil
Jason Gross
2016-02-25
*
efficient powmod
Andres Erbsen
2016-02-17
*
removed Print Assumptions
Jade Philipoom
2016-02-16
*
moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ...
Jade Philipoom
2016-02-16
*
proved most of point encoding admits, fixed some build system issues (dead im...
Jade Philipoom
2016-02-16
*
added point encodings; some admits remain
Jade Philipoom
2016-02-16
*
EdDSA: tweaked l_bound
Jade Philipoom
2016-02-15
*
merge
Jade Philipoom
2016-02-15
|
\
*
|
instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ...
Jade Philipoom
2016-02-15
*
|
added generic encoding spec
Jade Philipoom
2016-02-15
|
*
Finish seperating our specs: remove old non-specified code
Andres Erbsen
2016-02-15
|
/
[prev]
[next]