index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
WordUtil.v
Commit message (
Expand
)
Author
Age
*
move lemmas from Ed25519 to WordUtil
jadep
2017-02-22
*
Move things from WordUtil to ZUtil, add word lemma
Jason Gross
2017-02-06
*
More zutil
Jason Gross
2017-02-03
*
Add wordToZ_ZToWord_wordToZ
Jason Gross
2017-02-01
*
Add NToWord_wordToN_NToWord
Jason Gross
2017-02-01
*
Add transparent equality proofs for fixed wordT
Jason Gross
2017-01-21
*
Revert "Fix a missing qualification"
Jason Gross
2017-01-21
*
Fix a missing qualification
Jason Gross
2017-01-21
*
Move weqb_hetero to Bedrock.Word
Jason Gross
2017-01-21
*
Add weqb_hetero
Jason Gross
2017-01-21
*
Lemmas about winit, wlast
Rob Sloan
2016-11-11
*
Fix for Coq 8.4
Jason Gross
2016-11-11
*
Most of the admits in Ed25519.v
Rob Sloan
2016-11-11
*
Fix for 8.4
Jason Gross
2016-11-10
*
Hint Rewrite is section-local; move to top-level
Jason Gross
2016-11-10
*
Remove WordizeUtil dependency from WordUtil
Rob Sloan
2016-11-09
*
Rebase + remove WordizeUtil dependency from Z/Interpretations
Rob Sloan
2016-11-09
|
\
|
*
Rewrite cast_word so that it's extracted better
Jason Gross
2016-11-09
*
|
Finished WordUtil, word operations in Z/Interpretation
Rob Sloan
2016-11-09
*
|
Not quite done with WordUtil lemmas.
Robert Sloan
2016-11-08
|
\
|
|
*
put EdDSA encoding sign bit at the MSB
Andres Erbsen
2016-11-04
*
|
More of jgross admits, less neg and the cmovs
Rob Sloan
2016-11-01
*
|
most of jgross' admits
Rob Sloan
2016-10-31
|
/
*
Some work on proofs in src/Reflection/Z/Interpretations.v
Jason Gross
2016-10-27
*
Add some rewrites and admitted lemmas
Jason Gross
2016-10-27
*
Add beginnings of various interpretations of expression trees
Jason Gross
2016-10-27
*
More 8.4 fixes
Jason Gross
2016-10-23
*
Prove more things in WordUtil
Jason Gross
2016-10-23
*
Fill in some word util admitted lemmas
Jason Gross
2016-10-23
*
Add word64eqb_Zeqb
Jason Gross
2016-10-21
*
integrate bitwise operations
Andres Erbsen
2016-10-12
*
Generalize and simplify cast_word_refl
Jason Gross
2016-10-12
*
word manipulation functions for secret key formatting (#74)
Andres Erbsen
2016-10-12
*
Derive EdDSA.verify from equational specification
Andres Erbsen
2016-09-16
*
Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to
jadep
2016-04-29
*
Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...
jadep
2016-04-28
*
Finish absolutizing imports
Jason Gross
2016-03-10
*
Factor out some bedrock dependencies into WordUtil
Jason Gross
2016-02-25