index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Algebra
Commit message (
Expand
)
Author
Age
*
fsatz tests: 1/(1/x) = x
Andres Erbsen
2017-09-11
*
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
*
Prove relationship between `xzladderstep` and M.add (#162)
Andres Erbsen
2017-04-28
*
clean elliptic curve proofs, use par: in WeierstrassAffineProofs
Andres Erbsen
2017-04-28
*
rename-everything
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
*
make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround
Andres Erbsen
2017-03-30
*
make 8.5 happy
Andres Erbsen
2017-03-02
*
PrimeFieldTheorems: inv for isomorphic fields
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
*
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
*
Fix a missing section close in ZToRing
Jason Gross
2017-02-10
*
Accidentally pushed wrong file in last commit; this is the correct one
jadep
2017-02-10
*
Added ZToRing lemmas
jadep
2017-02-09