index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Specific
/
GF25519Reflective
Commit message (
Expand
)
Author
Age
*
Split up Reflection/Z/Syntax and make it smaller
Jason Gross
2017-02-02
*
Split off some bits of Reflection.Syntax
Jason Gross
2017-01-26
*
Remove the Const constructor of exprf
Jason Gross
2017-01-19
*
Split out Reflection.Equality, change Tflat implicit argument
Jason Gross
2017-01-19
*
Add reified LadderStep without carries
Jason Gross
2017-01-07
*
Revert "Add apply10"
Jason Gross
2017-01-07
*
Add Common10_4Op
Jason Gross
2017-01-07
*
Add Expr10_4Op
Jason Gross
2017-01-07
*
Admit Common9_4Op.v
Jason Gross
2016-12-08
*
Various application lemmas
Jason Gross
2016-11-23
*
More GF25519ReflectiveCommon generalization
Jason Gross
2016-11-22
*
Copy bounds, fix a typo
Jason Gross
2016-11-22
*
Start work on a faster version of GF*Reflective/Common*
Jason Gross
2016-11-21
*
Fix missing import for List.repeat in 8.4
Jason Gross
2016-11-21
*
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
*
Move util definitions to util folder
Jason Gross
2016-11-17
*
Add reified mostly-bounds-checked add_coordinates
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
*
Speed up some GF25519 tactics
Jason Gross
2016-11-14
*
Support for 128-bit words
Jason Gross
2016-11-14
*
Remove dead code in rebuild-reified.py
Jason Gross
2016-11-11
*
Begin filling in @JasonGross's stubs
jadep
2016-11-11
*
8.4-compatible universe handling
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
*
Refactor various reflective things
Jason Gross
2016-11-06
*
The fix in 8.4 broke 8.5/8.6, so we fix that
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 proofs about boundedness to GF25519Reflective/Common.v
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
*
Shove Z.Interpretations into closer alignment
Jason Gross
2016-11-03
*
Fix build
Jason Gross
2016-11-03
*
Fix bounds that were reversed
Jason Gross
2016-11-03
*
Export strings in GF25519Reflective/Common
Jason Gross
2016-11-01
*
Print out the computed bounds on the various ops
Jason Gross
2016-11-01
*
Parameterize bounded things over the limb length
Jason Gross
2016-11-01
*
Add bounds type in Specific/GF25519Reflective/Common.v
Jason Gross
2016-10-31
*
Revert "Switch from word to Z"
Jason Gross
2016-10-31
*
Switch from word to Z
Jason Gross
2016-10-31
*
Switch to reflective bounded word in Ed25519
Jason Gross
2016-10-31
[next]