index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Better extraction
Jason Gross
2016-11-17
*
Copy bounds
Jason Gross
2016-11-17
*
Finish proofs about eliminating useless carries
Jason Gross
2016-11-17
*
Add add_coordinates_respectful_hetero
Jason Gross
2016-11-17
*
Remove an admit
Jason Gross
2016-11-17
*
Add fieldwise_map
Jason Gross
2016-11-17
*
Add another admitted lemma
Jason Gross
2016-11-17
*
Generalize add_coordinates
Jason Gross
2016-11-17
*
Add GF25519BoundedExtendedAddCoordinates
Jason Gross
2016-11-17
*
Add src/Specific/GF25519BoundedAddCoordinates.v
Jason Gross
2016-11-17
*
Add HList.mapt_Proper
Jason Gross
2016-11-17
*
Add ReflectiveAddCoordinates
Jason Gross
2016-11-17
*
Add some missing files
Jason Gross
2016-11-17
*
Fix some problems with previous commit
Jason Gross
2016-11-17
*
Remove admits, fill templates, copy bounds
Jason Gross
2016-11-17
*
Update AddCoordinates
Jason Gross
2016-11-17
*
Minor change in AddCoordinates
Jason Gross
2016-11-17
*
Add interpf_LetIn
Jason Gross
2016-11-17
*
Move util definitions to util folder
Jason Gross
2016-11-17
*
Copy reified add coordinates to various versions of curves
Jason Gross
2016-11-17
*
Add reified mostly-bounds-checked add_coordinates
Jason Gross
2016-11-17
*
Update field names in SpecificGen
Jason Gross
2016-11-17
*
Move ExtendedAddCoordinates to new file, SpecGen
Jason Gross
2016-11-17
*
Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry
Jason Gross
2016-11-17
*
: assert is not valid 8.4 syntax
Jason Gross
2016-11-17
*
Work around bug #5205 (arguments naming weirdness)
Jason Gross
2016-11-16
*
Copy bounds to specific_gen
Jason Gross
2016-11-16
*
Add Un{Return,Abs}_eta
Jason Gross
2016-11-16
*
Add : assert to a bunch of arguments
Jason Gross
2016-11-16
*
Split fixedpoint in interpf
Jason Gross
2016-11-16
*
Add more things to Reflective/Common
Jason Gross
2016-11-16
*
Arguments for Un{Return,Abs}
Jason Gross
2016-11-16
*
Add add_coordinates_gen
Jason Gross
2016-11-16
*
Add UnReturn, UnAbs
Jason Gross
2016-11-16
*
Fix for Coq 8.5 (more unfolding)
Jason Gross
2016-11-15
*
Fix sqrt handling in specificgen
Jason Gross
2016-11-14
*
Handle both kinds of sqrt
Jason Gross
2016-11-14
*
More generic sqrt in SpecificGen
Jason Gross
2016-11-14
*
More generic sqrt
Jason Gross
2016-11-14
*
Copy over better prefreeze
Jason Gross
2016-11-14
*
Fix postfreezeW_correct_and_bounded
Jason Gross
2016-11-14
*
Update SpecificGen to be faster
Jason Gross
2016-11-14
*
Speed up some GF25519 tactics
Jason Gross
2016-11-14
*
Support for 128-bit words
Jason Gross
2016-11-14
*
Add word-size-independent interpretations
Jason Gross
2016-11-14
*
Update sqrtm1 for 3mod4
Jason Gross
2016-11-14
*
Fix some sqrt things
Jason Gross
2016-11-14
*
Fix a missing unfold
Jason Gross
2016-11-14
*
Fix a missing unfold
Jason Gross
2016-11-14
*
Update bounds things with prefreeze
Jason Gross
2016-11-14
[next]