index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Specific
Commit message (
Expand
)
Author
Age
...
*
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
*
Work around bug #5205 (arguments naming weirdness)
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
*
Fix for Coq 8.5 (more unfolding)
Jason Gross
2016-11-15
*
Handle both kinds of sqrt
Jason Gross
2016-11-14
*
More generic sqrt
Jason Gross
2016-11-14
*
Fix postfreezeW_correct_and_bounded
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
*
Fix some sqrt things
Jason Gross
2016-11-14
*
Fix a missing unfold
Jason Gross
2016-11-14
*
Update bounds things with prefreeze
Jason Gross
2016-11-14
*
Add mulW_noinline
Jason Gross
2016-11-14
*
Work around bug #5198 (broken tc resolution)
Jason Gross
2016-11-12
*
More 8.4pl2 fixes
Jason Gross
2016-11-12
*
Fix for Coq 8.2
Jason Gross
2016-11-12
*
Fixes for 8.4 (instantiate)
Jason Gross
2016-11-12
*
GF25519: add ErepAdd
Andres Erbsen
2016-11-11
*
GF25519: add optimized addition chain
Andres Erbsen
2016-11-11
*
Proved postfreezeW_correct_and_bounded
jadep
2016-11-11
*
Remove dead code in rebuild-reified.py
Jason Gross
2016-11-11
*
Begin filling in @JasonGross's stubs
jadep
2016-11-11
*
separate freeze into two parts
jadep
2016-11-11
*
8.4-compatible universe handling
Jason Gross
2016-11-11
*
Remove 8.6 only syntax
Jason Gross
2016-11-11
*
Freeze stubs
Jason Gross
2016-11-11
*
Fix bug in 8.4 build
Jason Gross
2016-11-09
*
Split up GF25519Reflective.Common: faster+parallel
Jason Gross
2016-11-09
*
move B_order_l and prime_q
Andres Erbsen
2016-11-06
*
Refactor various reflective things
Jason Gross
2016-11-06
*
Connect [is_bounded] to [bounded_by]
Jason Gross
2016-11-06
*
The fix in 8.4 broke 8.5/8.6, so we fix that
Jason Gross
2016-11-06
*
Add syntactic tuples
Jason Gross
2016-11-06
*
Add support for dependent reification
Jason Gross
2016-11-06
*
Work around broken evars in 8.4
Jason Gross
2016-11-06
*
Plug in boundedness proofs
Jason Gross
2016-11-05
*
Add better bounded lemmas to reified things
Jason Gross
2016-11-05
*
Add eta-expansion in GF25519BoundedCommon.v
Jason Gross
2016-11-05
*
Add proofs about boundedness to GF25519Reflective/Common.v
Jason Gross
2016-11-05
*
Add unfold_is_bounded
Jason Gross
2016-11-05
*
Add code for overflow check (disabled bc freeze)
Jason Gross
2016-11-05
*
Split off some things from Interpretations
Jason Gross
2016-11-05
*
separate Ed25519Extraction.v, add extraction to Makefile
Andres Erbsen
2016-11-03
*
Shove Z.Interpretations into closer alignment
Jason Gross
2016-11-03
*
Fix build
Jason Gross
2016-11-03
*
Make [freeze] proofs consider machine integer width and hard input bounds sep...
jadep
2016-11-03
*
Fix bounds that were reversed
Jason Gross
2016-11-03
*
Clean up fe25519_word64ize, give examples
Jason Gross
2016-11-02
[prev]
[next]