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
*
Import prim token notations before using them
Jason Gross
2018-08-24
*
minor updates needed to make it compile with bbv
Samuel Gruetter
2018-02-05
*
enforce use of [F.zero], [F.one]; prove Ed25519 admits
Andres Erbsen
2017-07-07
*
eddsa spec fix
Andres Erbsen
2017-06-14
*
ScalarMult: Z -> G -> G (closes #193)
Andres Erbsen
2017-06-14
*
Don't rely on autogenerated names
Jason Gross
2017-06-05
*
Strip trailing whitespace
Jason Gross
2017-06-02
*
Support destructuring dlet and slet
Jason Gross
2017-05-13
*
clean elliptic curve proofs, use par: in WeierstrassAffineProofs
Andres Erbsen
2017-04-28
*
Add commented out proof of equivalence in MxDH
Jason Gross
2017-04-12
*
rename-everything
Andres Erbsen
2017-04-06
*
remove Encoding stuff
Andres Erbsen
2017-04-06
*
Add [Proof using] to most proofs
Jason Gross
2017-04-04
*
More fine-grained tactic imports
Jason Gross
2017-04-03
*
use improved fsatz on various elliptic curve things
Andres Erbsen
2017-03-31
*
make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround
Andres Erbsen
2017-03-30
*
make 8.5 happy
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
*
address some code review comments
Andres Erbsen
2017-03-02
*
Weierstrass curve is a group
Andres Erbsen
2017-03-02
*
change weierstrass spec, prove most cases of associativity
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 changed qualified tactic name
Jason Gross
2017-01-17
*
Add ladderstep_other_assoc
Jason Gross
2017-01-07
*
Add more generic ladderstep
Jason Gross
2017-01-07
*
implement X25519
Andres Erbsen
2016-11-06
*
move B_order_l and prime_q
Andres Erbsen
2016-11-06
*
put EdDSA encoding sign bit at the MSB
Andres Erbsen
2016-11-04
*
Filled in point/scalar encoding definitions.
jadep
2016-10-10
*
Ed25519: add basepoint and prove most EdDSA preconditions
Andres Erbsen
2016-10-10
*
Spec.Ed25519: prove that Curve25519 is an elliptic curve
Andres Erbsen
2016-10-10
*
Spec.Ed25519: fix exponent field modulus
Andres Erbsen
2016-10-10
*
Moved PointEncoding out of Spec
jadep
2016-10-06
*
Fixed a lingering inappropriate use of Logic.eq
jadep
2016-10-06
*
fix 8.4 build
jadep
2016-10-03
*
A couple hotfixes; recent commits somehow broke things
jadep
2016-10-03
*
Wrote proofs necessary to fill in all point-encoding related context variable...
jadep
2016-10-03
*
Ed25519: use Global Instance
Andres Erbsen
2016-10-03
*
Spec: add ed25519
Andres Erbsen
2016-10-03
*
MxDH: do not depend on implicit import of list notations
Andres Erbsen
2016-09-26
*
add Montgomery x-coordinate Diffie-Hellman and Curve25519
Andres Erbsen
2016-09-26
*
alternative signing derivation
Andres Erbsen
2016-09-22
*
Derive EdDSA.verify from equational specification
Andres Erbsen
2016-09-16
*
ModularArithmetic: conversions between [F] and [nat]
Andres Erbsen
2016-09-16
*
Fully qualify [Require]s
Jason Gross
2016-09-08
[next]