index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Specific
/
GF25519Bounded.v
Commit message (
Expand
)
Author
Age
*
make 8.5 happy
Andres Erbsen
2017-03-02
*
Switch to fully uncurried form for reflection
Jason Gross
2017-03-01
*
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
*
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
*
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
*
Proved postfreezeW_correct_and_bounded
jadep
2016-11-11
*
Begin filling in @JasonGross's stubs
jadep
2016-11-11
*
Freeze stubs
Jason Gross
2016-11-11
*
separate Ed25519Extraction.v, add extraction to Makefile
Andres Erbsen
2016-11-03
*
fix lingering reference to old name of renamed lemma
jadep
2016-11-02
*
Fix GF25519Bounded in a different way
Jason Gross
2016-11-02
*
Fix [sqrtW_sig]
Jason Gross
2016-11-02
*
Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...
jadep
2016-11-02
*
Parameterize bounded things over the limb length
Jason Gross
2016-11-01
*
Make it easier to extract word64
Jason Gross
2016-10-31
*
Switch to reflective bounded word in Ed25519
Jason Gross
2016-10-31
*
Switch to bounded Z
Jason Gross
2016-10-25
*
Add pack, unpack, ge_modulus to axioms to be reified
Jason Gross
2016-10-24
*
Finish twedprm_ERep proof
Jason Gross
2016-10-23
*
Make some things instances
Jason Gross
2016-10-23
*
Generalize field_from_redundant_representation
Jason Gross
2016-10-23
*
Add decode to GF25519BoundedCommon
Jason Gross
2016-10-22
*
Fix divergence in src/Specific/GF25519Bounded.v
Jason Gross
2016-10-22
*
Unfold interp stuff in Assembly/GF25519BoundedInstantiation
Jason Gross
2016-10-22
*
Add bounded sqrt
Jason Gross
2016-10-22
*
Remove axioms from src/Specific/GF25519Bounded.v, plug assembly
Jason Gross
2016-10-21
*
Remove code that should have been removed
Jason Gross
2016-10-20
*
Split up GF25519Bounded to avoid circular dependencies
Jason Gross
2016-10-20
*
Add todo
Jason Gross
2016-10-20
*
Switch from bounded Z to bounded word
Jason Gross
2016-10-20
*
More specific bounded requirements, implement inv
Jason Gross
2016-10-19
*
First pass at bounded version of GF25519
Jason Gross
2016-10-19