index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
FixedWordSizesEquality.v
Commit message (
Expand
)
Author
Age
*
Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil
Jason Gross
2018-08-23
*
minor updates needed to make it compile with bbv
Samuel Gruetter
2018-02-05
*
Add eq_ZToWord
Jason Gross
2017-06-17
*
Don't rely on autogenerated names
Jason Gross
2017-06-05
*
Use Z.max 0, not an if statement
Jason Gross
2017-04-08
*
Add wordToZ_ZToWord_mod_full
Jason Gross
2017-04-08
*
Add wordToZ_ZToWord_mod
Jason Gross
2017-04-08
*
Add ZToWord_wordToZ_ZToWord_small
Jason Gross
2017-04-08
*
Add wordToZ{_gen,}_range
Jason Gross
2017-03-30
*
Add log and non-log versions of FixedWordSizes lem
Jason Gross
2017-02-23
*
Move things from WordUtil to ZUtil, add word lemma
Jason Gross
2017-02-06
*
Split off non-unfolding version of fixed_size_op_to_word
Jason Gross
2017-02-03
*
Add valid_update lemmas about FixedWordSizes
Jason Gross
2017-02-03
*
Don't unfold wordToZ_gen in fixed_Size_op_to_word
Jason Gross
2017-02-03
*
Fix a missing argument
Jason Gross
2017-02-03
*
Fix a typo
Jason Gross
2017-02-03
*
Handle more kinds of ops in fixed_size_op_to_word
Jason Gross
2017-02-03
*
Add fixed_size_op_to_word tactic
Jason Gross
2017-02-03
*
Add wordToZ_ZToWord_wordToZ
Jason Gross
2017-02-01
*
Add ZToWord_wordToZ_ZToWord
Jason Gross
2017-02-01
*
Add wordToZ_ZToWord, ZToWord_wordToZ
Jason Gross
2017-02-01
*
Add transparent equality proofs for fixed wordT
Jason Gross
2017-01-21